MBT: check that clients and connections match those in the model

modules/src/ics03_connection/connection.rs

@@ -1,7 +1,7 @@
 use std::convert::{TryFrom, TryInto};
 use std::str::FromStr;
 
-use serde::Serialize;
+use serde::{Deserialize, Serialize};
 use tendermint_proto::Protobuf;
 
 use ibc_proto::ibc::core::connection::v1::{
@@ -248,7 +248,7 @@ impl Counterparty {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, Serialize)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
 pub enum State {
     Uninitialized = 0,
     Init = 1,

modules/tests/Makefile

@@ -0,0 +1,5 @@
+mbt:
+	cargo t --features mocks -- --nocapture mbt
+
+stateright:
+	cargo t --features mocks -- --nocapture stateright

modules/tests/executor/mod.rs

@@ -2,12 +2,12 @@ pub mod modelator;
 pub mod step;
 
 use ibc::ics02_client::client_def::{AnyClientState, AnyConsensusState, AnyHeader};
-use ibc::ics02_client::client_type::ClientType;
+use ibc::ics02_client::context::ClientReader;
 use ibc::ics02_client::error::Kind as ICS02ErrorKind;
 use ibc::ics02_client::msgs::create_client::MsgCreateAnyClient;
 use ibc::ics02_client::msgs::update_client::MsgUpdateAnyClient;
 use ibc::ics02_client::msgs::ClientMsg;
-use ibc::ics03_connection::connection::Counterparty;
+use ibc::ics03_connection::connection::{Counterparty, State as ConnectionState};
 use ibc::ics03_connection::error::Kind as ICS03ErrorKind;
 use ibc::ics03_connection::msgs::conn_open_ack::MsgConnectionOpenAck;
 use ibc::ics03_connection::msgs::conn_open_confirm::MsgConnectionOpenConfirm;
@@ -27,6 +27,7 @@ use ibc::mock::header::MockHeader;
 use ibc::mock::host::HostType;
 use ibc::proofs::{ConsensusProof, Proofs};
 use ibc::Height;
+use ibc::{ics02_client::client_type::ClientType, ics04_channel::context::ChannelReader};
 use std::collections::HashMap;
 use std::error::Error;
 use std::fmt::{Debug, Display};
@@ -200,11 +201,72 @@ impl IBCTestExecutor {
         self.contexts.values().all(|ctx| ctx.validate().is_ok())
     }
 
-    /// Check that chain heights match the ones in the model.
-    pub fn check_chain_heights(&self, chains: HashMap<String, Chain>) -> bool {
+    /// Check that chain states match the ones in the model.
+    pub fn check_chain_states(&self, chains: HashMap<String, Chain>) -> bool {
         chains.into_iter().all(|(chain_id, chain)| {
             let ctx = self.chain_context(chain_id);
-            ctx.query_latest_height() == Self::height(chain.height)
+            // check that heights match
+            let heights_match = ctx.query_latest_height() == Self::height(chain.height);
+
+            // check that clients match
+            let clients_match = chain.clients.into_iter().all(|(client_id, client)| {
+                client.heights.into_iter().all(|height| {
+                    // check that each consensus state from the model exists
+                    ctx.consensus_state(&Self::client_id(client_id), Self::height(height))
+                        .is_some()
+                })
+            });
+
+            // check that connections match
+            let connections_match =
+                chain
+                    .connections
+                    .into_iter()
+                    .all(|(connection_id, connection)| {
+                        if connection.state == ConnectionState::Uninitialized {
+                            // if the connection has not yet been initialized, then
+                            // there's nothing to check
+                            true
+                        } else {
+                            if let Some(connection_end) =
+                                ctx.connection_end(&Self::connection_id(connection_id))
+                            {
+                                println!("END: {:?}", connection_end);
+                                // states must match
+                                let states_match = *connection_end.state() == connection.state;
+
+                                // client ids must match
+                                let client_ids = *connection_end.client_id()
+                                    == Self::client_id(connection.client_id.unwrap());
+
+                                // counterparty client ids must match
+                                let counterparty_client_ids = *connection_end
+                                    .counterparty()
+                                    .client_id()
+                                    == Self::client_id(connection.counterparty_client_id.unwrap());
+
+                                // counterparty connection ids must match
+                                let counterparty_connection_ids =
+                                    connection_end.counterparty().connection_id()
+                                        == connection
+                                            .counterparty_connection_id
+                                            .map(|connection_id| Self::connection_id(connection_id))
+                                            .as_ref();
+
+                                states_match
+                                    && client_ids
+                                    && counterparty_client_ids
+                                    && counterparty_connection_ids
+                            } else {
+                                // if the connection exists in the model, then it must
+                                // also exist in the implementation; in this case it
+                                // doesn't, so we fail the verification
+                                false
+                            }
+                        }
+                    });
+
+            heights_match && clients_match && connections_match
         })
     }
 
@@ -360,6 +422,7 @@ impl modelator::TestExecutor<Step> for IBCTestExecutor {
 
     fn next_step(&mut self, step: Step) -> bool {
         let result = self.apply(step.action);
+        println!("{:?} vs {:?}", result, step.action_outcome);
         let outcome_matches = match step.action_outcome {
             ActionOutcome::None => panic!("unexpected action outcome"),
             ActionOutcome::ICS02CreateOK => result.is_ok(),
@@ -406,6 +469,6 @@ impl modelator::TestExecutor<Step> for IBCTestExecutor {
             ActionOutcome::ICS03ConnectionOpenConfirmOK => result.is_ok(),
         };
         // also check the state of chains
-        outcome_matches && self.validate_chains() && self.check_chain_heights(step.chains)
+        outcome_matches && self.validate_chains() && self.check_chain_states(step.chains)
     }
 }

modules/tests/executor/modelator.rs

@@ -48,6 +48,7 @@ where
     let step_count = steps.len();
 
     for (i, step) in steps.iter().enumerate() {
+        println!("({}/{}) {:?}", i + 1, step_count, step);
         // check the step
         let ok = if i == 0 {
             executor.initial_step(step.clone())

modules/tests/executor/step.rs

@@ -1,3 +1,4 @@
+use ibc::ics03_connection::connection::State as ConnectionState;
 use serde::{Deserialize, Deserializer};
 use std::collections::HashMap;
 use std::fmt::Debug;
@@ -53,7 +54,7 @@ pub enum Action {
         chain_id: String,
 
         #[serde(alias = "previousConnectionId")]
-        #[serde(default, deserialize_with = "deserialize_connection_id")]
+        #[serde(default, deserialize_with = "deserialize_id")]
         previous_connection_id: Option<u64>,
 
         #[serde(alias = "clientId")]
@@ -105,21 +106,6 @@ pub enum Action {
     },
 }
 
-/// On the model, a non-existing `connection_id` is represented with -1.
-/// For this reason, this function maps a `Some(-1)` to a `None`.
-fn deserialize_connection_id<'de, D>(deserializer: D) -> Result<Option<u64>, D::Error>
-where
-    D: Deserializer<'de>,
-{
-    let connection_id: Option<i64> = Deserialize::deserialize(deserializer)?;
-    let connection_id = if connection_id == Some(-1) {
-        None
-    } else {
-        connection_id.map(|connection_id| connection_id as u64)
-    };
-    Ok(connection_id)
-}
-
 #[derive(Debug, Clone, PartialEq, Deserialize)]
 pub enum ActionOutcome {
     None,
@@ -143,4 +129,50 @@ pub enum ActionOutcome {
 #[derive(Debug, Clone, PartialEq, Deserialize)]
 pub struct Chain {
     pub height: u64,
+
+    pub clients: HashMap<u64, Client>,
+
+    pub connections: HashMap<u64, Connection>,
+}
+
+#[derive(Debug, Clone, PartialEq, Deserialize)]
+pub struct Client {
+    pub heights: Vec<u64>,
+}
+
+#[derive(Debug, Clone, PartialEq, Deserialize)]
+pub struct Connection {
+    #[serde(alias = "clientId")]
+    #[serde(default, deserialize_with = "deserialize_id")]
+    pub client_id: Option<u64>,
+
+    #[serde(alias = "connectionId")]
+    #[serde(default, deserialize_with = "deserialize_id")]
+    pub connection_id: Option<u64>,
+
+    #[serde(alias = "counterpartyClientId")]
+    #[serde(default, deserialize_with = "deserialize_id")]
+    pub counterparty_client_id: Option<u64>,
+
+    #[serde(alias = "counterpartyConnectionId")]
+    #[serde(default, deserialize_with = "deserialize_id")]
+    pub counterparty_connection_id: Option<u64>,
+
+    pub state: ConnectionState,
+}
+
+/// On the model, a non-existing `client_id` and a `connection_id` is
+/// represented with -1.
+/// For this reason, this function maps a `Some(-1)` to a `None`.
+fn deserialize_id<'de, D>(deserializer: D) -> Result<Option<u64>, D::Error>
+where
+    D: Deserializer<'de>,
+{
+    let id: Option<i64> = Deserialize::deserialize(deserializer)?;
+    let id = if id == Some(-1) {
+        None
+    } else {
+        id.map(|id| id as u64)
+    };
+    Ok(id)
 }

modules/tests/gen_tests_loop.sh

@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+
+cd support/model_based/
+gen_tests.py
+cd -
+make
+

modules/tests/mbt.rs

@@ -5,23 +5,25 @@ const TESTS_DIR: &str = "tests/support/model_based/tests";
 #[test]
 fn mbt() {
     let tests = vec![
-        "ICS02CreateOKTest",
-        "ICS02UpdateOKTest",
-        "ICS02ClientNotFoundTest",
-        "ICS02HeaderVerificationFailureTest",
-        "ICS03ConnectionOpenInitOKTest",
-        "ICS03MissingClientTest",
-        "ICS03ConnectionOpenTryOKTest",
-        "ICS03InvalidConsensusHeightTest",
-        "ICS03ConnectionNotFoundTest",
-        "ICS03ConnectionMismatchTest",
-        "ICS03MissingClientConsensusStateTest",
+        // "ICS02CreateOKTest",
+        // "ICS02UpdateOKTest",
+        // "ICS02ClientNotFoundTest",
+        // "ICS02HeaderVerificationFailureTest",
+        // "ICS03ConnectionOpenInitOKTest",
+        // "ICS03MissingClientTest",
+        // "ICS03ConnectionOpenTryOKTest",
+        "ICS03ConnectionOpenTryStateInitTest",
+        // "ICS03InvalidConsensusHeightTest",
+        // "ICS03ConnectionNotFoundTest",
+        // "ICS03ConnectionMismatchTest",
+        // "ICS03MissingClientConsensusStateTest",
         // TODO: the following test should fail but doesn't because proofs are
         // not yet verified
         // "ICS03InvalidProofTest",
-        "ICS03ConnectionOpenAckOKTest",
-        "ICS03UninitializedConnectionTest",
-        "ICS03ConnectionOpenConfirmOKTest",
+        // "ICS03ConnectionOpenAckOKTest",
+        // "ICS03UninitializedConnectionTest",
+        // "ICS03ConnectionOpenAckTryOpenStateTest",
+        // "ICS03ConnectionOpenConfirmOKTest",
     ];
 
     for test in tests {

modules/tests/support/model_based/IBCTests.cfg

@@ -0,0 +1,11 @@
+
+CONSTANTS
+    ChainIds = {"chainA", "chainB"}
+    MaxChainHeight = 5
+    MaxClientsPerChain = 1
+    MaxConnectionsPerChain = 1
+
+INIT InitTest
+NEXT NextTest
+
+INVARIANT ICS03ConnectionOpenTryStateInitTestNeg

modules/tests/support/model_based/IBCTests.tla

@@ -1,6 +1,20 @@
 ------------------------------ MODULE IBCTests --------------------------------
 
-EXTENDS IBC
+EXTENDS IBC, Sequences
+
+VARIABLE
+    previousChains
+
+PreviousConnectionState(chainId, connectionId) ==
+    previousChains[chainId].connections[connectionId].state
+
+InitTest ==
+    /\ Init
+    /\ previousChains = chains
+
+NextTest ==
+    /\ Next
+    /\ previousChains' = chains
 
 ICS02CreateOKTest ==
     /\ actionOutcome = "ICS02CreateOK"
@@ -23,6 +37,12 @@ ICS03MissingClientTest ==
 ICS03ConnectionOpenTryOKTest ==
     /\ actionOutcome = "ICS03ConnectionOpenTryOK"
 
+ICS03ConnectionOpenTryStateInitTest ==
+    /\ action.type = "ICS03ConnectionOpenTry"
+    /\ action.previousConnectionId /= -1
+    /\ PreviousConnectionState(action.chainId, action.previousConnectionId) = "Init"
+    /\ actionOutcome = "ICS03ConnectionOpenTryOK"
+
 ICS03InvalidConsensusHeightTest ==
     /\ actionOutcome = "ICS03InvalidConsensusHeight"
 
@@ -41,6 +61,11 @@ ICS03InvalidProofTest ==
 ICS03ConnectionOpenAckOKTest ==
     /\ actionOutcome = "ICS03ConnectionOpenAckOK"
 
+ICS03ConnectionOpenAckStateTryOpenTest ==
+    /\ action.type = "ICS03ConnectionOpenAck"
+    /\ PreviousConnectionState(action.chainId, action.connectionId) = "TryOpen"
+    /\ actionOutcome = "ICS03ConnectionOpenAckOK"
+
 ICS03UninitializedConnectionTest ==
     /\ actionOutcome = "ICS03UninitializedConnection"
 
@@ -61,6 +86,7 @@ ICS03MissingClientTestNeg == ~ICS03MissingClientTest
 
 \* ICS03ConnectionOpenTry tests
 ICS03ConnectionOpenTryOKTestNeg == ~ICS03ConnectionOpenTryOKTest
+ICS03ConnectionOpenTryStateInitTestNeg == ~ICS03ConnectionOpenTryStateInitTest
 ICS03InvalidConsensusHeightTestNeg == ~ICS03InvalidConsensusHeightTest
 ICS03ConnectionNotFoundTestNeg == ~ICS03ConnectionNotFoundTest
 ICS03ConnectionMismatchTestNeg == ~ICS03ConnectionMismatchTest
@@ -69,6 +95,7 @@ ICS03InvalidProofTestNeg == ~ICS03InvalidProofTest
 
 \* ICS03ConnectionOpenAck tests
 ICS03ConnectionOpenAckOKTestNeg == ~ICS03ConnectionOpenAckOKTest
+ICS03ConnectionOpenAckStateTryOpenTestNeg == ~ICS03ConnectionOpenAckStateTryOpenTest
 ICS03UninitializedConnectionTestNeg == ~ICS03UninitializedConnectionTest
 
 \* ICS03ConnectionOpenConfirm tests

modules/tests/support/model_based/Makefile

@@ -0,0 +1,5 @@
+check:
+	apalache-mc check --length=16 --nworkers=12 --inv=ModelNeverErrors IBC.tla
+
+test:
+	apalache-mc check --inv=ICS03ConnectionMismatchTestNeg IBCTests.tla