Model-based tests for ICS02

modules/Cargo.toml

@@ -37,6 +37,8 @@ dyn-clonable = "0.9.0"
 regex = "1"
 bech32 = "0.7.2"
 
+eyre = "0.6.5"
+
 [dependencies.tendermint]
 version = "=0.18.0"
 

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/Makefile

@@ -0,0 +1,2 @@
+test:
+ cargo t --features mocks -- --nocapture main

modules/tests/model_based.rs

@@ -0,0 +1,198 @@
+mod modelator;
+mod state;
+
+use ibc::ics02_client::client_def::AnyHeader;
+use ibc::ics02_client::client_def::{AnyClientState, AnyConsensusState};
+use ibc::ics02_client::client_type::ClientType;
+use ibc::ics02_client::error::{Error as ICS02Error, 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::error::{Error as ICS18Error, Kind as ICS18ErrorKind};
+use ibc::ics24_host::identifier::ChainId;
+use ibc::ics24_host::identifier::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 state::{ActionOutcome, ActionType, State};
+use std::error::Error;
+use std::fmt::Debug;
+use tendermint::account::Id as AccountId;
+
+#[derive(Debug)]
+struct ICS02TestExecutor {
+ version: u64,
+ ctx: MockContext,
+}
+
+impl ICS02TestExecutor {
+ fn new() -> Self {
+ let version = 1;
+ let max_history_size = 1;
+ let initial_height = 0;
+ let ctx = MockContext::new(
+ ChainId::new("mock".to_string(), version),
+ HostType::Mock,
+ // HostType::SyntheticTendermint,
+ max_history_size,
+ Height::new(version, initial_height),
+ );
+ Self { version, ctx }
+ }
+}
+
+impl modelator::TestExecutor<State> for ICS02TestExecutor {
+ fn check_initial_state(&mut self, state: State) -> bool {
+ assert_eq!(
+ state.action.action_type,
+ ActionType::Null,
+ "unexpected action type"
+ );
+ assert_eq!(
+ state.action_outcome,
+ ActionOutcome::Null,
+ "unexpected action outcome"
+ );
+ true
+ }
+
+ fn check_next_state(&mut self, state: State) -> bool {
+ match state.action.action_type {
+ ActionType::Null => panic!("unexpected action type"),
+ ActionType::CreateClient => {
+ // get action parameters
+ let height = state
+ .action
+ .height
+ .expect("create client action should have a height");
+
+ // create client and consensus state from parameters
+ let client_state = AnyClientState::Mock(MockClientState(self.mock_header(height)));
+ let consensus_state =
+ AnyConsensusState::Mock(MockConsensusState(self.mock_header(height)));
+
+ // create dummy signer
+ let signer = self.dummy_signer();
+
+ // create ICS26 message and deliver it
+ let msg = ICS26Envelope::ICS2Msg(ClientMsg::CreateClient(MsgCreateAnyClient {
+ client_state,
+ consensus_state,
+ signer,
+ }));
+ let result = self.ctx.deliver(msg);
+
+ // check the expected outcome: client create always succeeds
+ assert_eq!(
+ state.action_outcome,
+ ActionOutcome::CreateOK,
+ "unexpected action outcome"
+ );
+ result.is_ok()
+ }
+ ActionType::UpdateClient => {
+ // get action parameters
+ let client_id = state
+ .action
+ .client_id
+ .expect("update client action should have a client identifier");
+ let height = state
+ .action
+ .height
+ .expect("update client action should have a height");
+
+ // create client id and header from action parameters
+ let client_id = ClientId::new(ClientType::Mock, client_id)
+ .expect("it should be possible to create the client identifier");
+ let header = AnyHeader::Mock(self.mock_header(height));
+
+ // create dummy signer
+ let signer = self.dummy_signer();
+
+ // create ICS26 message and deliver it
+ let msg = ICS26Envelope::ICS2Msg(ClientMsg::UpdateClient(MsgUpdateAnyClient {
+ client_id: client_id.clone(),
+ header,
+ signer,
+ }));
+ let result = self.ctx.deliver(msg);
+
+ match state.action_outcome {
+ ActionOutcome::Null | ActionOutcome::CreateOK => {
+ panic!("unexpected action outcome")
+ }
+ ActionOutcome::UpdateOK => {
+ // check that there were no errors
+ result.is_ok()
+ }
+ ActionOutcome::UpdateClientNotFound => {
+ let handler_error_kind = self.extract_ics02_handler_error_kind(result);
+ matches!(
+ handler_error_kind,
+ ICS02ErrorKind::ClientNotFound(id) if id == client_id
+ )
+ }
+ ActionOutcome::UpdateHeightVerificationFailure => {
+ let handler_error_kind = self.extract_ics02_handler_error_kind(result);
+ handler_error_kind == ICS02ErrorKind::HeaderVerificationFailure
+ }
+ }
+ }
+ }
+ }
+}
+
+impl ICS02TestExecutor {
+ fn dummy_signer(&self) -> AccountId {
+ AccountId::new([0; 20])
+ }
+
+ fn mock_header(&self, height: u64) -> MockHeader {
+ MockHeader(Height::new(self.version, height))
+ }
+
+ fn extract_ics02_handler_error_kind(&self, result: Result<(), ICS18Error>) -> ICS02ErrorKind {
+ let ics18_error = 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::<ICS02Error>()
+ .expect("ICS26 source should be an ICS02 error")
+ .kind()
+ .clone()
+ }
+}
+
+const TESTS_DIR: &str = "tests/support/model_based";
+
+#[test]
+fn main() {
+ let tests = vec!["UpdateOKTest", "UpdateHeightVerificationFailureTest"];
+
+ for test in tests {
+ let path = format!("{}/{}.json", TESTS_DIR, test);
+ let test_executor = ICS02TestExecutor::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_driver(test_executor, path) {
+ panic!("{:?}", e);
+ }
+ }
+}

modules/tests/modelator.rs

@@ -0,0 +1,52 @@
+use eyre::{eyre, Context, Result};
+use serde::de::DeserializeOwned;
+use std::fmt::Debug;
+use std::fs::File;
+use std::io::BufReader;
+use std::path::Path;
+
+pub trait TestExecutor<S> {
+ fn check_initial_state(&mut self, state: S) -> bool;
+
+ fn check_next_state(&mut self, state: S) -> bool;
+}
+
+pub fn test_driver<E, S, P>(mut executor: E, path: P) -> Result<()>
+where
+ E: TestExecutor<S> + Debug,
+ S: DeserializeOwned + Debug + Clone,
+ P: AsRef<Path>,
+{
+ // open test file
+ let file = File::open(path.as_ref())
+ .wrap_err_with(|| format!("test file {:?} not found.", path.as_ref()))?;
+ let reader = BufReader::new(file);
+
+ // parse test file
+ let states: Vec<S> = serde_json::de::from_reader(reader)
+ .wrap_err_with(|| format!("test file {:?} could not be deserialized", path.as_ref()))?;
+
+ let mut states = states.into_iter();
+
+ // check the initial state
+ if let Some(state) = states.next() {
+ if !executor.check_initial_state(state.clone()) {
+ return Err(eyre!("check failed on initial state:\n{:#?}", state));
+ }
+ } else {
+ println!("WARNING: test file {:?} had 0 states", path.as_ref());
+ return Ok(());
+ }
+
+ // check all the remaining states
+ for state in states {
+ if !executor.check_next_state(state.clone()) {
+ return Err(eyre!(
+ "check failed on state:\n{:#?}\n\nexecutor:\n{:#?}",
+ state,
+ executor
+ ));
+ }
+ }
+ Ok(())
+}

modules/tests/state.rs

@@ -0,0 +1,37 @@
+use serde::Deserialize;
+use std::fmt::Debug;
+
+#[derive(Debug, Clone, Deserialize)]
+pub struct State {
+ pub action: Action,
+
+ #[serde(alias = "actionOutcome")]
+ pub action_outcome: ActionOutcome,
+}
+
+#[derive(Debug, Clone, Deserialize)]
+pub struct Action {
+ #[serde(alias = "type")]
+ pub action_type: ActionType,
+
+ #[serde(alias = "clientId")]
+ pub client_id: Option<u64>,
+
+ pub height: Option<u64>,
+}
+
+#[derive(Debug, Clone, PartialEq, Deserialize)]
+pub enum ActionType {
+ Null,
+ CreateClient,
+ UpdateClient,
+}
+
+#[derive(Debug, Clone, PartialEq, Deserialize)]
+pub enum ActionOutcome {
+ Null,
+ CreateOK,
+ UpdateOK,
+ UpdateClientNotFound,
+ UpdateHeightVerificationFailure,
+}

modules/tests/support/model_based/.gitignore

@@ -0,0 +1,9 @@
+*.out
+states/
+x/
+detailed.log
+bfs.csv
+log0.smt
+profile-rules.txt
+counterexample.json
+counterexample.tla

modules/tests/support/model_based/ICS02.cfg

@@ -0,0 +1,10 @@
+CONSTANTS
+ MaxClients = 5
+ MaxHeight = 5
+
+INIT Init
+NEXT Next
+
+INVARIANTS
+ TypeOK
+ ModelNeverErrors