Model-based tests for ICS02 (#601)

* Add ICS02 model

* Add MBT test driver

* Add ICS02TestExecutor

* Add another apalache counterexample

* Fix ICS02.tla: client counter starts at 0

* Check for errors in MockContext.deliver

* Handle errors in MBT tests

* Remove SyntheticTendermint mock context

* More idiomatic check_next_state

* Buffered file reads

* Make extract_handler_error_kind generic over the IBC handler

* Support multiple chains in MBT

* Make eyre a dev-dependency

* s/ICS0/IBC on TLA files

* Initial support for conn open init

* Start connection and channel identifiers at 0

* Add conn open init to TLA spec

* Represent clients with a record in TLA spec

* Finish connection open init

* s/state/step

* Minimize diff

* Modularize TLA spec

* TLA format convention

* s/Null/None

* Sketch conn open try; Model chain's height

* Bound model space

* Only update chain height upon success

* Check that chain heights match the ones in the model

* Sketch conn open try

* Sketch conn open try

* Model missing connections and connection mismatches in conn open try

* Trigger bug in conn open try

* Go back to previous way of generating connection and channel ids

* Disable failing MBT test

* Fix panic in conn open try when no connection id is provided

* ICS02TestExecutor -> IBCTestExecutor

* Failing MBT test now passes with #615

* Add notes on MBT

* Remove ICS02

* Add README

* Improve README

* Remove MBT intro

* new lines

* Make MBT README more easily discoverable

* IBCTestExecutor: Map from ChainId (instead of String) to MockContext

* s/epoch/revision

* Move from eyre to thiserror

* Improve README

* Improve README

* Improve arguments order in modelator::test

* Improve chain identifiers

* Improve README

modules/src/ics02_client/msgs/create_client.rs

@@ -22,9 +22,9 @@ pub const TYPE_URL: &str = "/ibc.core.client.v1.MsgCreateClient";
 /// A type of message that triggers the creation of a new on-chain (IBC) client.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct MsgCreateAnyClient {
- client_state: AnyClientState,
- consensus_state: AnyConsensusState,
- signer: AccountId,
+ pub client_state: AnyClientState,
+ pub consensus_state: AnyConsensusState,
+ pub signer: AccountId,
 }
 
 impl MsgCreateAnyClient {

modules/tests/README.md

@@ -0,0 +1,63 @@
+## Model-based tests for IBC modules
+
+### The model
+
+This directory contains the model-based tests for the IBC modules. They are "model-based" because they are generated from a `TLA+` model of the IBC modules (see [IBC.tla](support/model_based/IBC.tla)).
+
+To instantiate the model, we define in [IBC.cfg](support/model_based/IBC.cfg) the following model constants:
+ - `ChainIds = {"chain-A", "chain-B"}`, indicating that two chains, `chain-A` and `chain-B`, will be created
+ - `MaxClientsPerChain = 1`, indicating that at most 1 client per chain will be created
+ - `MaxClientHeight = 2`, indicating that clients will reach at most height 2
+
+The [IBC.cfg](support/model_based/IBC.cfg) file also defines two simple invariants:
+```tla
+INVARIANTS
+ TypeOK
+ ModelNeverErrors
+```
+
+Then, we can ask [`Apalache`](https://apalache.informal.systems), a model checker for `TLA+`, to check that these invariants hold:
+```bash
+apalache-mc check --inv=ICS02UpdateOKTestNeg IBC.tla
+```
+
+The above command automatically reads what we have defined in [IBC.cfg](support/model_based/IBC.cfg).
+
+### The tests
+
+Tests are `TLA+` assertions that describe the desired shape of the test (see [IBCTests.tla](support/model_based/IBCTests.tla)). One of the assertions in [IBCTests.tla](support/model_based/IBCTests.tla) is the following:
+
+```tla
+ICS02UpdateOKTest ==
+ /\ actionOutcome = "ICS02UpdateOK"
+```
+
+This very simple assertion describes a test where the [model](support/model_based/IBC.tla) variable `actionOutcome` reaches the value `"ICS02UpdateOK"`, which occurs when a client is successfully updated to a new height (see [ICS02.tla](support/model_based/ICS02.tla)).
+
+To generate a test from the `ICS02UpdateOKTest` assertion, we first define an invariant negating it:
+```tla
+ICS02UpdateOKTestNeg == ~ICS02UpdateOKTest
+```
+
+Then, we ask `Apalache`, to prove it:
+
+```bash
+apalache-mc check --inv=ICS02UpdateOKTestNeg IBCTests.tla
+```
+
+(Again, the above command automatically reads what we have defined in [IBCTests.cfg](support/model_based/IBCTests.cfg).)
+
+Because the invariant is wrong, `Apalache` will find a counterexample showing that it is indeed possible that a client is sucessfully updated to a new height. This counterexample is our test.
+
+### Current limitations
+
+The counterexamples currently produced by `Apalache` are not easy to parse and have traditionally required tools like [`jsonatr`](https://github.com/informalsystems/jsonatr). Fortunately, [that will change soon](https://github.com/informalsystems/apalache/issues/530), and `Apalache` will be able to produce counterexamples like those in [support/model_based/tests/](support/model_based/tests/).
+These are currently generated manually, but can be easily mapped to Rust (see [step.rs](step.rs)).
+
+### Running the model-based tests
+
+The model-based tests can be run with the following command:
+
+```bash
+cargo test -p ibc --features mocks -- model_based
+```

modules/tests/model_based.rs

@@ -0,0 +1,269 @@
+mod modelator;
+mod step;
+
+use ibc::ics02_client::client_def::{AnyClientState, AnyConsensusState, AnyHeader};
+use ibc::ics02_client::client_type::ClientType;
+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::ics18_relayer::context::ICS18Context;
+use ibc::ics18_relayer::error::{Error as ICS18Error, Kind as ICS18ErrorKind};
+use ibc::ics24_host::identifier::{ChainId, ClientId};
+use ibc::ics26_routing::error::{Error as ICS26Error, Kind as ICS26ErrorKind};
+use ibc::ics26_routing::msgs::ICS26Envelope;
+use ibc::mock::client_state::{MockClientState, MockConsensusState};
+use ibc::mock::context::MockContext;
+use ibc::mock::header::MockHeader;
+use ibc::mock::host::HostType;
+use ibc::Height;
+use std::collections::HashMap;
+use std::error::Error;
+use std::fmt::{Debug, Display};
+use step::{ActionOutcome, ActionType, Chain, Step};
+use tendermint::account::Id as AccountId;
+
+#[derive(Debug)]
+struct IBCTestExecutor {
+ // mapping from chain identifier to its context
+ contexts: HashMap<ChainId, MockContext>,
+}
+
+impl IBCTestExecutor {
+ fn new() -> Self {
+ Self {
+ contexts: Default::default(),
+ }
+ }
+
+ /// Create a `MockContext` for a given `chain_id`.
+ /// Panic if a context for `chain_id` already exists.
+ fn init_chain_context(&mut self, chain_id: String, initial_height: u64) {
+ let chain_id = Self::chain_id(chain_id);
+ let max_history_size = 1;
+ let ctx = MockContext::new(
+ chain_id.clone(),
+ HostType::Mock,
+ max_history_size,
+ Height::new(Self::revision(), initial_height),
+ );
+ assert!(self.contexts.insert(chain_id, ctx).is_none());
+ }
+
+ /// Returns a reference to the `MockContext` of a given `chain_id`.
+ /// Panic if the context for `chain_id` is not found.
+ fn chain_context(&self, chain_id: String) -> &MockContext {
+ self.contexts
+ .get(&Self::chain_id(chain_id))
+ .expect("chain context should have been initialized")
+ }
+
+ /// Returns a mutable reference to the `MockContext` of a given `chain_id`.
+ /// Panic if the context for `chain_id` is not found.
+ fn chain_context_mut(&mut self, chain_id: String) -> &mut MockContext {
+ self.contexts
+ .get_mut(&Self::chain_id(chain_id))
+ .expect("chain context should have been initialized")
+ }
+
+ fn extract_handler_error_kind<K>(ics18_result: Result<(), ICS18Error>) -> K
+ where
+ K: Clone + Debug + Display + Into<anomaly::BoxError> + 'static,
+ {
+ let ics18_error = ics18_result.expect_err("ICS18 error expected");
+ assert!(matches!(
+ ics18_error.kind(),
+ ICS18ErrorKind::TransactionFailed
+ ));
+ let ics26_error = ics18_error
+ .source()
+ .expect("expected source in ICS18 error")
+ .downcast_ref::<ICS26Error>()
+ .expect("ICS18 source should be an ICS26 error");
+ assert!(matches!(
+ ics26_error.kind(),
+ ICS26ErrorKind::HandlerRaisedError,
+ ));
+ ics26_error
+ .source()
+ .expect("expected source in ICS26 error")
+ .downcast_ref::<anomaly::Error<K>>()
+ .expect("ICS26 source should be an handler error")
+ .kind()
+ .clone()
+ }
+
+ fn chain_id(chain_id: String) -> ChainId {
+ ChainId::new(chain_id, Self::revision())
+ }
+
+ fn revision() -> u64 {
+ 0
+ }
+
+ fn client_id(client_id: u64) -> ClientId {
+ ClientId::new(ClientType::Mock, client_id)
+ .expect("it should be possible to create the client identifier")
+ }
+
+ fn height(height: u64) -> Height {
+ Height::new(Self::revision(), height)
+ }
+
+ fn mock_header(height: u64) -> MockHeader {
+ MockHeader(Self::height(height))
+ }
+
+ fn header(height: u64) -> AnyHeader {
+ AnyHeader::Mock(Self::mock_header(height))
+ }
+
+ fn client_state(height: u64) -> AnyClientState {
+ AnyClientState::Mock(MockClientState(Self::mock_header(height)))
+ }
+
+ fn consensus_state(height: u64) -> AnyConsensusState {
+ AnyConsensusState::Mock(MockConsensusState(Self::mock_header(height)))
+ }
+
+ fn signer() -> AccountId {
+ AccountId::new([0; 20])
+ }
+
+ /// Check that chain heights match the ones in the model.
+ fn check_chain_heights(&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)
+ })
+ }
+}
+
+impl modelator::TestExecutor<Step> for IBCTestExecutor {
+ fn initial_step(&mut self, step: Step) -> bool {
+ assert_eq!(
+ step.action.action_type,
+ ActionType::None,
+ "unexpected action type"
+ );
+ assert_eq!(
+ step.action_outcome,
+ ActionOutcome::None,
+ "unexpected action outcome"
+ );
+ // initiliaze all chains
+ for (chain_id, chain) in step.chains {
+ self.init_chain_context(chain_id, chain.height);
+ }
+ true
+ }
+
+ fn next_step(&mut self, step: Step) -> bool {
+ let outcome_matches = match step.action.action_type {
+ ActionType::None => panic!("unexpected action type"),
+ ActionType::ICS02CreateClient => {
+ // get action parameters
+ let chain_id = step
+ .action
+ .chain_id
+ .expect("create client action should have a chain identifier");
+ let client_height = step
+ .action
+ .client_height
+ .expect("create client action should have a client height");
+
+ // get chain's context
+ let ctx = self.chain_context_mut(chain_id);
+
+ // create ICS26 message and deliver it
+ let msg = ICS26Envelope::ICS2Msg(ClientMsg::CreateClient(MsgCreateAnyClient {
+ client_state: Self::client_state(client_height),
+ consensus_state: Self::consensus_state(client_height),
+ signer: Self::signer(),
+ }));
+ let result = ctx.deliver(msg);
+
+ // check the expected outcome: client create always succeeds
+ match step.action_outcome {
+ ActionOutcome::ICS02CreateOK => {
+ // the implementaion matches the model if no error occurs
+ result.is_ok()
+ }
+ action => panic!("unexpected action outcome {:?}", action),
+ }
+ }
+ ActionType::ICS02UpdateClient => {
+ // get action parameters
+ let chain_id = step
+ .action
+ .chain_id
+ .expect("update client action should have a chain identifier");
+ let client_id = step
+ .action
+ .client_id
+ .expect("update client action should have a client identifier");
+ let client_height = step
+ .action
+ .client_height
+ .expect("update client action should have a client height");
+
+ // get chain's context
+ let ctx = self.chain_context_mut(chain_id);
+
+ // create ICS26 message and deliver it
+ let msg = ICS26Envelope::ICS2Msg(ClientMsg::UpdateClient(MsgUpdateAnyClient {
+ client_id: Self::client_id(client_id),
+ header: Self::header(client_height),
+ signer: Self::signer(),
+ }));
+ let result = ctx.deliver(msg);
+
+ // check the expected outcome
+ match step.action_outcome {
+ ActionOutcome::ICS02UpdateOK => {
+ // the implementaion matches the model if no error occurs
+ result.is_ok()
+ }
+ ActionOutcome::ICS02ClientNotFound => {
+ let handler_error_kind =
+ Self::extract_handler_error_kind::<ICS02ErrorKind>(result);
+ // the implementaion matches the model if there's an
+ // error matching the expected outcome
+ matches!(
+ handler_error_kind,
+ ICS02ErrorKind::ClientNotFound(error_client_id)
+ if error_client_id == Self::client_id(client_id)
+ )
+ }
+ ActionOutcome::ICS02HeaderVerificationFailure => {
+ let handler_error_kind =
+ Self::extract_handler_error_kind::<ICS02ErrorKind>(result);
+ // the implementaion matches the model if there's an
+ // error matching the expected outcome
+ handler_error_kind == ICS02ErrorKind::HeaderVerificationFailure
+ }
+ action => panic!("unexpected action outcome {:?}", action),
+ }
+ }
+ };
+ // also check that chain heights match
+ outcome_matches && self.check_chain_heights(step.chains)
+ }
+}
+
+const TESTS_DIR: &str = "tests/support/model_based/tests";
+
+#[test]
+fn model_based() {
+ let tests = vec!["ICS02UpdateOKTest", "ICS02HeaderVerificationFailureTest"];
+
+ for test in tests {
+ let test = format!("{}/{}.json", TESTS_DIR, test);
+ let executor = IBCTestExecutor::new();
+ // we should be able to just return the `Result` once the following issue
+ // is fixed: https://github.com/rust-lang/rust/issues/43301
+ if let Err(e) = modelator::test(&test, executor) {
+ panic!("{:?}", e);
+ }
+ }
+}