diff --git a/modules/tests/README.md b/modules/tests/README.md index 670f5b521e..d6839c3c60 100644 --- a/modules/tests/README.md +++ b/modules/tests/README.md @@ -5,9 +5,11 @@ 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 + +- `ChainIds = {"chain-A", "chain-B"}`, indicating that two chains, `chain-A` and `chain-B`, will be created +- `MaxChainHeight = 4`, indicating that each chain will reach at most height 4 +- `MaxClientsPerChain = 1`, indicating that at most 1 client per chain will be created +- `MaxConnectionsPerChain = 1`, indicating that at most 1 connection per chain will be created The [IBC.cfg](support/model_based/IBC.cfg) file also defines two simple invariants: ```tla @@ -16,13 +18,13 @@ INVARIANTS ModelNeverErrors ``` -Then, we can ask [`Apalache`](https://apalache.informal.systems), a model checker for `TLA+`, to check that these invariants hold: +Then, we can ask [`TLC`](https://github.com/tlaplus/tlaplus), a model checker for `TLA+`, to check that these invariants hold: + ```bash -apalache-mc check --inv=ICS02UpdateOKTestNeg IBC.tla +wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar +java -cp tla2tools.jar tlc2.TLC IBC.tla -tool -modelcheck -config IBC.cfg -workers auto ``` -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: @@ -39,25 +41,21 @@ To generate a test from the `ICS02UpdateOKTest` assertion, we first define an in ICS02UpdateOKTestNeg == ~ICS02UpdateOKTest ``` -Then, we ask `Apalache`, to prove it: +Then, we ask `TLC`, to prove it. Because the invariant is wrong, `TLC` 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. + +The [`gen_tests.py`](support/model_based/gen_tests.py) script can be used to generate the tests. This script assumes the existence of [`tlc-json`](https://github.com/vitorenesduarte/tlc-json), which can be installed with the following commands: ```bash -apalache-mc check --inv=ICS02UpdateOKTestNeg IBCTests.tla +git clone https://github.com/vitorenesduarte/tlc-json +cd tlc-json/ +cargo install --path . ``` -(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 +cd modules/ cargo test --features mocks -- mbt ``` diff --git a/modules/tests/executor/mod.rs b/modules/tests/executor/mod.rs index 77954c2236..3f37619e98 100644 --- a/modules/tests/executor/mod.rs +++ b/modules/tests/executor/mod.rs @@ -7,20 +7,30 @@ 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::error::Kind as ICS03ErrorKind; +use ibc::ics03_connection::msgs::conn_open_ack::MsgConnectionOpenAck; +use ibc::ics03_connection::msgs::conn_open_confirm::MsgConnectionOpenConfirm; +use ibc::ics03_connection::msgs::conn_open_init::MsgConnectionOpenInit; +use ibc::ics03_connection::msgs::conn_open_try::MsgConnectionOpenTry; +use ibc::ics03_connection::msgs::ConnectionMsg; +use ibc::ics03_connection::version::Version; 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::ics23_commitment::commitment::{CommitmentPrefix, CommitmentProofBytes}; +use ibc::ics24_host::identifier::{ChainId, ClientId, ConnectionId}; 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::proofs::{ConsensusProof, Proofs}; use ibc::Height; use std::collections::HashMap; use std::error::Error; use std::fmt::{Debug, Display}; -use step::{ActionOutcome, ActionType, Chain, Step}; +use step::{Action, ActionOutcome, Chain, Step}; use tendermint::account::Id as AccountId; #[derive(Debug)] @@ -38,9 +48,10 @@ impl IBCTestExecutor { /// 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) { + pub 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; + // never GC blocks + let max_history_size = usize::MAX; let ctx = MockContext::new( chain_id.clone(), HostType::Mock, @@ -52,7 +63,7 @@ impl IBCTestExecutor { /// 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 { + pub fn chain_context(&self, chain_id: String) -> &MockContext { self.contexts .get(&Self::chain_id(chain_id)) .expect("chain context should have been initialized") @@ -60,13 +71,13 @@ impl IBCTestExecutor { /// 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 { + pub 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(ics18_result: Result<(), ICS18Error>) -> K + pub fn extract_handler_error_kind(ics18_result: Result<(), ICS18Error>) -> K where K: Clone + Debug + Display + Into + 'static, { @@ -93,160 +104,308 @@ impl IBCTestExecutor { .clone() } - fn chain_id(chain_id: String) -> ChainId { + pub fn chain_id(chain_id: String) -> ChainId { ChainId::new(chain_id, Self::revision()) } - fn revision() -> u64 { + pub fn revision() -> u64 { 0 } - fn client_id(client_id: u64) -> ClientId { + pub fn version() -> Version { + Version::default() + } + + pub fn versions() -> Vec { + vec![Self::version()] + } + + pub 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 { + pub fn connection_id(connection_id: u64) -> ConnectionId { + ConnectionId::new(connection_id) + } + + pub fn height(height: u64) -> Height { Height::new(Self::revision(), height) } - fn mock_header(height: u64) -> MockHeader { + pub fn mock_header(height: u64) -> MockHeader { MockHeader(Self::height(height)) } - fn header(height: u64) -> AnyHeader { + pub fn header(height: u64) -> AnyHeader { AnyHeader::Mock(Self::mock_header(height)) } - fn client_state(height: u64) -> AnyClientState { + pub fn client_state(height: u64) -> AnyClientState { AnyClientState::Mock(MockClientState(Self::mock_header(height))) } - fn consensus_state(height: u64) -> AnyConsensusState { + pub fn consensus_state(height: u64) -> AnyConsensusState { AnyConsensusState::Mock(MockConsensusState(Self::mock_header(height))) } - fn signer() -> AccountId { + pub fn signer() -> AccountId { AccountId::new([0; 20]) } + pub fn counterparty(client_id: u64, connection_id: Option) -> Counterparty { + let client_id = Self::client_id(client_id); + let connection_id = connection_id.map(|connection_id| Self::connection_id(connection_id)); + let prefix = Self::commitment_prefix(); + Counterparty::new(client_id, connection_id, prefix) + } + + pub fn delay_period() -> u64 { + 0 + } + + pub fn commitment_prefix() -> CommitmentPrefix { + vec![0].into() + } + + pub fn commitment_proof_bytes() -> CommitmentProofBytes { + vec![0].into() + } + + pub fn consensus_proof(height: u64) -> ConsensusProof { + let consensus_proof = Self::commitment_proof_bytes(); + let consensus_height = Self::height(height); + ConsensusProof::new(consensus_proof, consensus_height) + .expect("it should be possible to create the consensus proof") + } + + pub fn proofs(height: u64) -> Proofs { + let object_proof = Self::commitment_proof_bytes(); + let client_proof = None; + let consensus_proof = Some(Self::consensus_proof(height)); + let other_proof = None; + let height = Self::height(height); + Proofs::new( + object_proof, + client_proof, + consensus_proof, + other_proof, + height, + ) + .expect("it should be possible to create the proofs") + } + /// Check that chain heights match the ones in the model. - fn check_chain_heights(&self, chains: HashMap) -> bool { + pub fn validate_chains(&self) -> bool { + 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) -> 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 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"); + pub fn apply(&mut self, action: Action) -> Result<(), ICS18Error> { + match action { + Action::None => panic!("unexpected action type"), + Action::ICS02CreateClient { + chain_id, + client_state, + consensus_state, + } => { // 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), + client_state: Self::client_state(client_state), + consensus_state: Self::consensus_state(consensus_state), 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), - } + ctx.deliver(msg) } - 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"); - + Action::ICS02UpdateClient { + chain_id, + client_id, + header, + } => { // 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), + header: Self::header(header), 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::(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::(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), - } + ctx.deliver(msg) + } + Action::ICS03ConnectionOpenInit { + chain_id, + client_id, + counterparty_chain_id: _, + counterparty_client_id, + } => { + // get chain's context + let ctx = self.chain_context_mut(chain_id); + + // create ICS26 message and deliver it + let msg = Ics26Envelope::Ics3Msg(ConnectionMsg::ConnectionOpenInit( + MsgConnectionOpenInit { + client_id: Self::client_id(client_id), + counterparty: Self::counterparty(counterparty_client_id, None), + version: Self::version(), + delay_period: Self::delay_period(), + signer: Self::signer(), + }, + )); + ctx.deliver(msg) + } + Action::ICS03ConnectionOpenTry { + chain_id, + previous_connection_id, + client_id, + client_state, + counterparty_chain_id: _, + counterparty_client_id, + counterparty_connection_id, + } => { + // get chain's context + let ctx = self.chain_context_mut(chain_id); + + // create ICS26 message and deliver it + let msg = Ics26Envelope::Ics3Msg(ConnectionMsg::ConnectionOpenTry(Box::new( + MsgConnectionOpenTry { + previous_connection_id: previous_connection_id.map(Self::connection_id), + client_id: Self::client_id(client_id), + // TODO: is this ever needed? + client_state: None, + counterparty: Self::counterparty( + counterparty_client_id, + Some(counterparty_connection_id), + ), + counterparty_versions: Self::versions(), + proofs: Self::proofs(client_state), + delay_period: Self::delay_period(), + signer: Self::signer(), + }, + ))); + ctx.deliver(msg) + } + Action::ICS03ConnectionOpenAck { + chain_id, + connection_id, + client_state, + counterparty_chain_id: _, + counterparty_connection_id, + } => { + // get chain's context + let ctx = self.chain_context_mut(chain_id); + + // create ICS26 message and deliver it + let msg = Ics26Envelope::Ics3Msg(ConnectionMsg::ConnectionOpenAck(Box::new( + MsgConnectionOpenAck { + connection_id: Self::connection_id(connection_id), + counterparty_connection_id: Self::connection_id(counterparty_connection_id), + // TODO: is this ever needed? + client_state: None, + proofs: Self::proofs(client_state), + version: Self::version(), + signer: Self::signer(), + }, + ))); + ctx.deliver(msg) + } + Action::ICS03ConnectionOpenConfirm { + chain_id, + connection_id, + client_state, + counterparty_chain_id: _, + counterparty_connection_id: _, + } => { + // get chain's context + let ctx = self.chain_context_mut(chain_id); + + // create ICS26 message and deliver it + let msg = Ics26Envelope::Ics3Msg(ConnectionMsg::ConnectionOpenConfirm( + MsgConnectionOpenConfirm { + connection_id: Self::connection_id(connection_id), + proofs: Self::proofs(client_state), + signer: Self::signer(), + }, + )); + ctx.deliver(msg) } + } + } +} + +impl modelator::TestExecutor for IBCTestExecutor { + fn initial_step(&mut self, step: Step) -> bool { + assert_eq!(step.action, Action::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 result = self.apply(step.action); + let outcome_matches = match step.action_outcome { + ActionOutcome::None => panic!("unexpected action outcome"), + ActionOutcome::ICS02CreateOK => result.is_ok(), + ActionOutcome::ICS02UpdateOK => result.is_ok(), + ActionOutcome::ICS02ClientNotFound => matches!( + Self::extract_handler_error_kind::(result), + ICS02ErrorKind::ClientNotFound(_) + ), + ActionOutcome::ICS02HeaderVerificationFailure => matches!( + Self::extract_handler_error_kind::(result), + ICS02ErrorKind::HeaderVerificationFailure + ), + ActionOutcome::ICS03ConnectionOpenInitOK => result.is_ok(), + ActionOutcome::ICS03MissingClient => matches!( + Self::extract_handler_error_kind::(result), + ICS03ErrorKind::MissingClient(_) + ), + ActionOutcome::ICS03ConnectionOpenTryOK => result.is_ok(), + ActionOutcome::ICS03InvalidConsensusHeight => matches!( + Self::extract_handler_error_kind::(result), + ICS03ErrorKind::InvalidConsensusHeight(_, _) + ), + ActionOutcome::ICS03ConnectionNotFound => matches!( + Self::extract_handler_error_kind::(result), + ICS03ErrorKind::ConnectionNotFound(_) + ), + ActionOutcome::ICS03ConnectionMismatch => matches!( + Self::extract_handler_error_kind::(result), + ICS03ErrorKind::ConnectionMismatch(_) + ), + ActionOutcome::ICS03MissingClientConsensusState => matches!( + Self::extract_handler_error_kind::(result), + ICS03ErrorKind::MissingClientConsensusState(_, _) + ), + ActionOutcome::ICS03InvalidProof => matches!( + Self::extract_handler_error_kind::(result), + ICS03ErrorKind::InvalidProof + ), + ActionOutcome::ICS03ConnectionOpenAckOK => result.is_ok(), + ActionOutcome::ICS03UninitializedConnection => matches!( + Self::extract_handler_error_kind::(result), + ICS03ErrorKind::UninitializedConnection(_) + ), + ActionOutcome::ICS03ConnectionOpenConfirmOK => result.is_ok(), }; - // also check that chain heights match - outcome_matches && self.check_chain_heights(step.chains) + // also check the state of chains + outcome_matches && self.validate_chains() && self.check_chain_heights(step.chains) } } diff --git a/modules/tests/executor/modelator.rs b/modules/tests/executor/modelator.rs index cbd15b18e3..6c7f9a43df 100644 --- a/modules/tests/executor/modelator.rs +++ b/modules/tests/executor/modelator.rs @@ -10,12 +10,12 @@ pub enum ModelatorError { TestNotFound { path: String, error: String }, #[error("test '{path}' could not be deserialized: {error}")] InvalidTest { path: String, error: String }, - #[error("test '{path}' failed on step {step_index}/{step_count}:\nstep:\n{step:#?}\nexecutor:\n{executor:#?}")] + #[error("test '{path}' failed on step {step_index}/{step_count}:\nsteps: {steps:#?}\nexecutor: {executor:#?}")] FailedTest { path: String, step_index: usize, step_count: usize, - step: Step, + steps: Vec, executor: Executor, }, } @@ -47,7 +47,7 @@ where })?; let step_count = steps.len(); - for (i, step) in steps.into_iter().enumerate() { + for (i, step) in steps.iter().enumerate() { // check the step let ok = if i == 0 { executor.initial_step(step.clone()) @@ -60,7 +60,7 @@ where path: path.to_string(), step_index: i + 1, step_count, - step, + steps, executor, }); } diff --git a/modules/tests/executor/step.rs b/modules/tests/executor/step.rs index 98c831e050..7e0593025c 100644 --- a/modules/tests/executor/step.rs +++ b/modules/tests/executor/step.rs @@ -1,4 +1,4 @@ -use serde::Deserialize; +use serde::{Deserialize, Deserializer}; use std::collections::HashMap; use std::fmt::Debug; @@ -12,26 +12,112 @@ pub struct Step { pub chains: HashMap, } -#[derive(Debug, Clone, Deserialize)] -pub struct Action { - #[serde(alias = "type")] - pub action_type: ActionType, +#[derive(Debug, Clone, PartialEq, Deserialize)] +#[serde(tag = "type")] +pub enum Action { + None, + ICS02CreateClient { + #[serde(alias = "chainId")] + chain_id: String, + + #[serde(alias = "clientState")] + client_state: u64, + + #[serde(alias = "consensusState")] + consensus_state: u64, + }, + ICS02UpdateClient { + #[serde(alias = "chainId")] + chain_id: String, + + #[serde(alias = "clientId")] + client_id: u64, + + header: u64, + }, + ICS03ConnectionOpenInit { + #[serde(alias = "chainId")] + chain_id: String, + + #[serde(alias = "clientId")] + client_id: u64, + + #[serde(alias = "counterpartyChainId")] + counterparty_chain_id: String, + + #[serde(alias = "counterpartyClientId")] + counterparty_client_id: u64, + }, + ICS03ConnectionOpenTry { + #[serde(alias = "chainId")] + chain_id: String, + + #[serde(alias = "previousConnectionId")] + #[serde(default, deserialize_with = "deserialize_connection_id")] + previous_connection_id: Option, + + #[serde(alias = "clientId")] + client_id: u64, - #[serde(alias = "chainId")] - pub chain_id: Option, + #[serde(alias = "clientState")] + client_state: u64, - #[serde(alias = "clientId")] - pub client_id: Option, + #[serde(alias = "counterpartyChainId")] + counterparty_chain_id: String, - #[serde(alias = "clientHeight")] - pub client_height: Option, + #[serde(alias = "counterpartyClientId")] + counterparty_client_id: u64, + + #[serde(alias = "counterpartyConnectionId")] + counterparty_connection_id: u64, + }, + ICS03ConnectionOpenAck { + #[serde(alias = "chainId")] + chain_id: String, + + #[serde(alias = "connectionId")] + connection_id: u64, + + #[serde(alias = "clientState")] + client_state: u64, + + #[serde(alias = "counterpartyChainId")] + counterparty_chain_id: String, + + #[serde(alias = "counterpartyConnectionId")] + counterparty_connection_id: u64, + }, + ICS03ConnectionOpenConfirm { + #[serde(alias = "chainId")] + chain_id: String, + + #[serde(alias = "connectionId")] + connection_id: u64, + + #[serde(alias = "clientState")] + client_state: u64, + + #[serde(alias = "counterpartyChainId")] + counterparty_chain_id: String, + + #[serde(alias = "counterpartyConnectionId")] + counterparty_connection_id: u64, + }, } -#[derive(Debug, Clone, PartialEq, Deserialize)] -pub enum ActionType { - None, - ICS02CreateClient, - ICS02UpdateClient, +/// 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, D::Error> +where + D: Deserializer<'de>, +{ + let connection_id: Option = 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)] @@ -41,6 +127,17 @@ pub enum ActionOutcome { ICS02UpdateOK, ICS02ClientNotFound, ICS02HeaderVerificationFailure, + ICS03ConnectionOpenInitOK, + ICS03MissingClient, + ICS03ConnectionOpenTryOK, + ICS03InvalidConsensusHeight, + ICS03ConnectionNotFound, + ICS03ConnectionMismatch, + ICS03MissingClientConsensusState, + ICS03InvalidProof, + ICS03ConnectionOpenAckOK, + ICS03UninitializedConnection, + ICS03ConnectionOpenConfirmOK, } #[derive(Debug, Clone, PartialEq, Deserialize)] diff --git a/modules/tests/mbt.rs b/modules/tests/mbt.rs index 4ac8059990..a97f0ff736 100644 --- a/modules/tests/mbt.rs +++ b/modules/tests/mbt.rs @@ -4,15 +4,34 @@ const TESTS_DIR: &str = "tests/support/model_based/tests"; #[test] fn mbt() { - let tests = vec!["ICS02UpdateOKTest", "ICS02HeaderVerificationFailureTest"]; + let tests = vec![ + "ICS02CreateOKTest", + "ICS02UpdateOKTest", + "ICS02ClientNotFoundTest", + "ICS02HeaderVerificationFailureTest", + "ICS03ConnectionOpenInitOKTest", + "ICS03MissingClientTest", + "ICS03ConnectionOpenTryOKTest", + "ICS03InvalidConsensusHeightTest", + "ICS03ConnectionNotFoundTest", + "ICS03ConnectionMismatchTest", + "ICS03MissingClientConsensusStateTest", + // TODO: the following test should fail but doesn't because proofs are + // not yet verified + // "ICS03InvalidProofTest", + "ICS03ConnectionOpenAckOKTest", + "ICS03UninitializedConnectionTest", + "ICS03ConnectionOpenConfirmOKTest", + ]; for test in tests { let test = format!("{}/{}.json", TESTS_DIR, test); + println!("> running {}", test); let executor = 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 + // 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) = executor::modelator::test(&test, executor) { - panic!("{:?}", e); + panic!("{}", e); } } } diff --git a/modules/tests/support/model_based/IBC.cfg b/modules/tests/support/model_based/IBC.cfg index 73976184c4..d2997417ae 100644 --- a/modules/tests/support/model_based/IBC.cfg +++ b/modules/tests/support/model_based/IBC.cfg @@ -1,7 +1,8 @@ CONSTANTS - ChainIds = {"chainA-0", "chainB-0"} + ChainIds = {"chainA", "chainB"} + MaxChainHeight = 4 MaxClientsPerChain = 1 - MaxClientHeight = 2 + MaxConnectionsPerChain = 1 INIT Init NEXT Next diff --git a/modules/tests/support/model_based/IBC.tla b/modules/tests/support/model_based/IBC.tla index 7586626558..8376f0b89d 100644 --- a/modules/tests/support/model_based/IBC.tla +++ b/modules/tests/support/model_based/IBC.tla @@ -1,15 +1,18 @@ --------------------------------- MODULE IBC ---------------------------------- -EXTENDS Integers, FiniteSets, ICS02 +EXTENDS ICS02, ICS03 \* ids of existing chains CONSTANT ChainIds +\* max height which chains can reach +CONSTANT MaxChainHeight +ASSUME MaxChainHeight >= 0 \* max number of client to be created per chain CONSTANT MaxClientsPerChain ASSUME MaxClientsPerChain >= 0 -\* max height which clients can reach -CONSTANT MaxClientHeight -ASSUME MaxClientHeight >= 0 +\* max number of connections to be created per chain +CONSTANT MaxConnectionsPerChain +ASSUME MaxConnectionsPerChain >= 0 \* mapping from chain id to its data VARIABLE chains @@ -19,65 +22,92 @@ VARIABLE action VARIABLE actionOutcome vars == <> -(********************** TYPE ANNOTATIONS FOR APALACHE ************************) -\* operator for type annotations -a <: b == a - -ActionType == [ - type |-> STRING, - chainId |-> STRING, - clientHeight |-> Int, - clientId |-> Int -] -AsAction(a) == a <: ActionType -(******************* END OF TYPE ANNOTATIONS FOR APALACHE ********************) - \* set of possible chain heights -ChainHeights == Int +Heights == 1..MaxChainHeight \* set of possible client identifiers ClientIds == 0..(MaxClientsPerChain - 1) -\* set of possible client heights -ClientHeights == 1..MaxClientHeight - -\* data kept per cliennt -Client == [ - height: ClientHeights \union {HeightNone} -] -\* mapping from client identifier to its height -Clients == [ - ClientIds -> Client -] -\* data kept per chain -Chain == [ - height: ChainHeights, - clients: Clients, - clientIdCounter: 0..MaxClientsPerChain -] -\* mapping from chain identifier to its data -Chains == [ - ChainIds -> Chain -] +\* set of possible connection identifiers +ConnectionIds == 0..(MaxConnectionsPerChain- 1) +\* set of possible connection states +ConnectionStates == { + "Uninitialized", + "Init", + "TryOpen", + "Open" +} \* set of possible actions NoneActions == [ type: {"None"} ] <: {ActionType} + CreateClientActions == [ type: {"ICS02CreateClient"}, chainId: ChainIds, - clientHeight: ClientHeights + \* `clientState` contains simply a height + clientState: Heights, + \* `consensusState` contains simply a height + consensusState: Heights ] <: {ActionType} UpdateClientActions == [ type: {"ICS02UpdateClient"}, chainId: ChainIds, - clientHeight: ClientHeights, - clientId: ClientIds + clientId: ClientIds, + \* `header` contains simply a height + header: Heights ] <: {ActionType} -Actions == - NoneActions \union +ClientActions == CreateClientActions \union UpdateClientActions +ConnectionOpenInitActions == [ + type: {"ICS03ConnectionOpenInit"}, + chainId: ChainIds, + clientId: ClientIds, + counterpartyChainId: ChainIds, + counterpartyClientId: ClientIds +] <: {ActionType} +ConnectionOpenTryActions == [ + type: {"ICS03ConnectionOpenTry"}, + chainId: ChainIds, + clientId: ClientIds, + \* `previousConnectionId` can be none + previousConnectionId: ConnectionIds \union {ConnectionIdNone}, + \* `clientState` contains simply a height + clientState: Heights, + counterpartyChainId: ChainIds, + counterpartyClientId: ClientIds, + counterpartyConnectionId: ConnectionIds +] <: {ActionType} +ConnectionOpenAckActions == [ + type: {"ICS03ConnectionOpenAck"}, + chainId: ChainIds, + connectionId: ConnectionIds, + \* `clientState` contains simply a height + clientState: Heights, + counterpartyChainId: ChainIds, + counterpartyConnectionId: ConnectionIds +] <: {ActionType} +ConnectionOpenConfirmActions == [ + type: {"ICS03ConnectionOpenConfirm"}, + chainId: ChainIds, + connectionId: ConnectionIds, + \* `clientState` contains simply a height + clientState: Heights, + counterpartyChainId: ChainIds, + counterpartyConnectionId: ConnectionIds +] <: {ActionType} +ConnectionActions == + ConnectionOpenInitActions \union + ConnectionOpenTryActions \union + ConnectionOpenAckActions \union + ConnectionOpenConfirmActions + +Actions == + NoneActions \union + ClientActions \union + ConnectionActions + \* set of possible action outcomes ActionOutcomes == { "None", @@ -87,92 +117,394 @@ ActionOutcomes == { \* ICS02_UpdateClient outcomes: "ICS02UpdateOK", "ICS02ClientNotFound", - "ICS02HeaderVerificationFailure" + "ICS02HeaderVerificationFailure", + \* ICS03_ConnectionOpenInit outcomes: + "ICS03ConnectionOpenInitOK", + "ICS03MissingClient", + \* ICS03_ConnectionOpenTry outcomes: + "ICS03ConnectionOpenTryOK", + "ICS03InvalidConsensusHeight", + "ICS03ConnectionNotFound", + "ICS03ConnectionMismatch", + "ICS03MissingClientConsensusState", + "ICS03InvalidProof", + \* ICS03_ConnectionOpenAck outcomes: + "ICS03ConnectionOpenAckOK", + "ICS03UninitializedConnection", + \* ICS03_ConnectionOpenConfirm outcomes: + "ICS03ConnectionOpenConfirmOK" } +\* TODO: the current generation of tests cannot distinguish between a +\* "ICS03ConnectionMismatch" generated in conn open try, one generated +\* in conn open ack, or one genereted in conn open confirm; +\* (there are other cases like "ICS03InvalidProof") +\* we can solve this with in a variable 'history', like in the light +\* client tests. + +\* data kept per client +Client == [ + heights: SUBSET Heights +] +\* mapping from client identifier to its height +Clients == [ + ClientIds -> Client +] +\* data kept per connection +Connection == [ + state: ConnectionStates, + \* `chainId` is not strictly necessary but it's kept for consistency + chainId: ChainIds \union {ChainIdNone}, + clientId: ClientIds \union {ClientIdNone}, + connectionId: ConnectionIds \union {ConnectionIdNone}, + counterpartyChainId: ChainIds \union {ChainIdNone}, + counterpartyClientId: ClientIds \union {ClientIdNone}, + counterpartyConnectionId: ConnectionIds \union {ConnectionIdNone} +] +\* mapping from connection identifier to its data +Connections == [ + ConnectionIds -> Connection +] +\* data kept per chain +Chain == [ + height: Heights, + clients: Clients, + clientIdCounter: 0..MaxClientsPerChain, + connections: Connections, + connectionIdCounter: 0..MaxConnectionsPerChain, + connectionProofs: SUBSET ConnectionActions +] +\* mapping from chain identifier to its data +Chains == [ + ChainIds -> Chain +] (***************************** Specification *********************************) \* update chain height if outcome was ok -UpdateChainHeight(height, outcome, okOutcome) == - IF outcome = okOutcome THEN height + 1 ELSE height +UpdateChainHeight(height, result, okOutcome) == + IF result.outcome = okOutcome THEN + height + 1 + ELSE + height -CreateClient(chainId, clientHeight) == +\* update connection proofs if outcome was ok +UpdateConnectionProofs(connectionProofs, result, okOutcome) == + IF result.outcome = okOutcome THEN + connectionProofs \union {result.action} + ELSE + connectionProofs + +CreateClient(chainId, height) == LET chain == chains[chainId] IN - LET clients == chain.clients IN - LET clientIdCounter == chain.clientIdCounter IN - LET result == ICS02_CreateClient(clients, clientIdCounter, clientHeight) IN + LET result == ICS02_CreateClient(chain, chainId, height) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result.outcome, "ICS02CreateOK"), + !.height = UpdateChainHeight(@, result, "ICS02CreateOK"), !.clients = result.clients, !.clientIdCounter = result.clientIdCounter ] IN \* update `chains`, set the `action` and its `actionOutcome` /\ chains' = [chains EXCEPT ![chainId] = updatedChain] - /\ action' = AsAction([ - type |-> "ICS02CreateClient", - chainId |-> chainId, - clientHeight |-> clientHeight]) + /\ action' = result.action /\ actionOutcome' = result.outcome -UpdateClient(chainId, clientId, clientHeight) == +UpdateClient(chainId, clientId, height) == LET chain == chains[chainId] IN - LET clients == chain.clients IN - LET result == ICS02_UpdateClient(clients, clientId, clientHeight) IN + LET result == ICS02_UpdateClient(chain, chainId, clientId, height) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result.outcome, "ICS03CreateOK"), + !.height = UpdateChainHeight(@, result, "ICS02UpdateOK"), !.clients = result.clients ] IN \* update `chains`, set the `action` and its `actionOutcome` /\ chains' = [chains EXCEPT ![chainId] = updatedChain] - /\ action' = AsAction([ - type |-> "ICS02UpdateClient", - chainId |-> chainId, - clientId |-> clientId, - clientHeight |-> clientHeight]) + /\ action' = result.action /\ actionOutcome' = result.outcome -CreateClientAction == - \* select a chain id - \E chainId \in ChainIds: +ConnectionOpenInit( + chainId, + clientId, + counterpartyChainId, + counterpartyClientId +) == + LET chain == chains[chainId] IN + LET result == ICS03_ConnectionOpenInit( + chain, + chainId, + clientId, + counterpartyChainId, + counterpartyClientId + ) IN + \* update the chain + LET updatedChain == [chain EXCEPT + !.height = UpdateChainHeight(@, result, "ICS03ConnectionOpenInitOK"), + !.connections = result.connections, + !.connectionIdCounter = result.connectionIdCounter + ] IN + \* update the counterparty chain with a proof + LET counterpartyChain == chains[counterpartyChainId] IN + LET updatedCounterpartyChain == [counterpartyChain EXCEPT + !.connectionProofs = UpdateConnectionProofs(@, result, "ICS03ConnectionOpenInitOK") + ] IN + \* update `chains`, set the `action` and its `actionOutcome` + /\ chains' = [chains EXCEPT + ![chainId] = updatedChain, + ![counterpartyChainId] = updatedCounterpartyChain] + /\ action' = result.action + /\ actionOutcome' = result.outcome + +ConnectionOpenTry( + chainId, + clientId, + previousConnectionId, + height, + counterpartyChainId, + counterpartyClientId, + counterpartyConnectionId +) == + LET chain == chains[chainId] IN + LET result == ICS03_ConnectionOpenTry( + chain, + chainId, + clientId, + previousConnectionId, + height, + counterpartyChainId, + counterpartyClientId, + counterpartyConnectionId + ) IN + \* update the chain + LET updatedChain == [chain EXCEPT + !.height = UpdateChainHeight(@, result, "ICS03ConnectionOpenTryOK"), + !.connections = result.connections, + !.connectionIdCounter = result.connectionIdCounter + ] IN + \* update the counterparty chain with a proof + LET counterpartyChain == chains[counterpartyChainId] IN + LET updatedCounterpartyChain == [counterpartyChain EXCEPT + !.connectionProofs = UpdateConnectionProofs(@, result, "ICS03ConnectionOpenTryOK") + ] IN + \* update `chains`, set the `action` and its `actionOutcome` + /\ chains' = [chains EXCEPT + ![chainId] = updatedChain, + ![counterpartyChainId] = updatedCounterpartyChain] + /\ action' = result.action + /\ actionOutcome' = result.outcome + +ConnectionOpenAck( + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId +) == + LET chain == chains[chainId] IN + LET result == ICS03_ConnectionOpenAck( + chain, + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId + ) IN + \* update the chain + LET updatedChain == [chain EXCEPT + !.height = UpdateChainHeight(@, result, "ICS03ConnectionOpenAckOK"), + !.connections = result.connections + ] IN + \* update the counterparty chain with a proof + LET counterpartyChain == chains[counterpartyChainId] IN + LET updatedCounterpartyChain == [counterpartyChain EXCEPT + !.connectionProofs = UpdateConnectionProofs(@, result, "ICS03ConnectionOpenAckOK") + ] IN + \* update `chains`, set the `action` and its `actionOutcome` + /\ chains' = [chains EXCEPT + ![chainId] = updatedChain, + ![counterpartyChainId] = updatedCounterpartyChain] + /\ action' = result.action + /\ actionOutcome' = result.outcome + +ConnectionOpenConfirm( + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId +) == + LET chain == chains[chainId] IN + LET result == ICS03_ConnectionOpenConfirm( + chain, + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId + ) IN + \* update the chain + LET updatedChain == [chain EXCEPT + !.height = UpdateChainHeight(@, result, "ICS03ConnectionOpenConfirmOK"), + !.connections = result.connections + ] IN + \* no need to update the counterparty chain with a proof (as in the other + \* connection open handlers) + \* update `chains`, set the `action` and its `actionOutcome` + /\ chains' = [chains EXCEPT ![chainId] = updatedChain] + /\ action' = result.action + /\ actionOutcome' = result.outcome + +CreateClientAction(chainId) == \* select a height for the client to be created at - \E clientHeight \in ClientHeights: + \E height \in Heights: \* only create client if the model constant `MaxClientsPerChain` allows \* it - IF chains[chainId].clientIdCounter \in ClientIds THEN - CreateClient(chainId, clientHeight) + LET allowed == chains[chainId].clientIdCounter < MaxClientsPerChain IN + IF allowed THEN + CreateClient(chainId, height) ELSE UNCHANGED vars -UpdateClientAction == - \* select a chain id - \E chainId \in ChainIds: +UpdateClientAction(chainId) == \* select a client to be updated (which may not exist) \E clientId \in ClientIds: \* select a height for the client to be updated - \E clientHeight \in ClientHeights: - UpdateClient(chainId, clientId, clientHeight) + \E height \in Heights: + UpdateClient(chainId, clientId, height) + +ConnectionOpenInitAction(chainId) == + \* select a client id + \E clientId \in ClientIds: + \* select a counterparty chain id + \E counterpartyChainId \in ChainIds: + \* select a counterparty client id + \E counterpartyClientId \in ClientIds: + \* only create connection if the model constant `MaxConnectionsPerChain` + \* allows it + LET allowed == + chains[chainId].connectionIdCounter < MaxConnectionsPerChain IN + IF chainId /= counterpartyChainId /\ allowed THEN + ConnectionOpenInit( + chainId, + clientId, + counterpartyChainId, + counterpartyClientId + ) + ELSE + UNCHANGED vars + +ConnectionOpenTryAction(chainId) == + \* select a client id + \E clientId \in ClientIds: + \* select a previous connection id (which can be none) + \E previousConnectionId \in ConnectionIds \union {ConnectionIdNone}: + \* select a claimed height for the client + \E height \in Heights: + \* select a counterparty chain id + \E counterpartyChainId \in ChainIds: + \* select a counterparty client id + \E counterpartyClientId \in ClientIds: + \* select a counterparty connection id + \E counterpartyConnectionId \in ConnectionIds: + \* only perform action if there was a previous connection or if the + \* model constant `MaxConnectionsPerChain` allows that a new connection + \* is created + LET allowed == + \/ previousConnectionId /= ConnectionIdNone + \/ chains[chainId].connectionIdCounter < MaxConnectionsPerChain IN + IF chainId /= counterpartyChainId /\ allowed THEN + ConnectionOpenTry( + chainId, + clientId, + previousConnectionId, + height, + counterpartyChainId, + counterpartyClientId, + counterpartyConnectionId + ) + ELSE + UNCHANGED vars + +ConnectionOpenAckAction(chainId) == + \* select a connection id + \E connectionId \in ConnectionIds: + \* select a claimed height for the client + \E height \in Heights: + \* select a counterparty chain id + \E counterpartyChainId \in ChainIds: + \* select a counterparty connection id + \E counterpartyConnectionId \in ConnectionIds: + IF chainId /= counterpartyChainId THEN + ConnectionOpenAck( + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId + ) + ELSE + UNCHANGED vars + +ConnectionOpenConfirmAction(chainId) == + \* select a connection id + \E connectionId \in ConnectionIds: + \* select a claimed height for the client + \E height \in Heights: + \* select a counterparty chain id + \E counterpartyChainId \in ChainIds: + \* select a counterparty connection id + \E counterpartyConnectionId \in ConnectionIds: + IF chainId /= counterpartyChainId THEN + ConnectionOpenConfirm( + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId + ) + ELSE + UNCHANGED vars Init == - \* create a client with none values + \* create a client and a connection with none values LET clientNone == [ - height |-> HeightNone + heights |-> AsSetInt({}) + ] IN + LET connectionNone == [ + state |-> "Uninitialized", + chainId |-> ChainIdNone, + clientId |-> ClientIdNone, + connectionId |-> ConnectionIdNone, + counterpartyChainId |-> ChainIdNone, + counterpartyClientId |-> ClientIdNone, + counterpartyConnectionId |-> ConnectionIdNone ] IN \* create an empty chain LET emptyChain == [ - height |-> 0, + height |-> 1, clients |-> [clientId \in ClientIds |-> clientNone], - clientIdCounter |-> 0 + clientIdCounter |-> 0, + connections |-> [connectionId \in ConnectionIds |-> connectionNone], + connectionIdCounter |-> 0, + connectionProofs |-> AsSetAction({}) ] IN /\ chains = [chainId \in ChainIds |-> emptyChain] /\ action = AsAction([type |-> "None"]) /\ actionOutcome = "None" Next == - \/ CreateClientAction - \/ UpdateClientAction - \/ UNCHANGED vars + \* select a chain id + \E chainId \in ChainIds: + \* perform action on chain if the model constant `MaxChainHeight` allows + \* it + IF chains[chainId].height < MaxChainHeight THEN + \/ CreateClientAction(chainId) + \/ UpdateClientAction(chainId) + \/ ConnectionOpenInitAction(chainId) + \/ ConnectionOpenTryAction(chainId) + \/ ConnectionOpenAckAction(chainId) + \/ ConnectionOpenConfirmAction(chainId) + \/ UNCHANGED vars + ELSE + \/ UNCHANGED vars (******************************** Invariants *********************************) diff --git a/modules/tests/support/model_based/IBCDefinitions.tla b/modules/tests/support/model_based/IBCDefinitions.tla index 0d5e8e2385..6c1712bd6b 100644 --- a/modules/tests/support/model_based/IBCDefinitions.tla +++ b/modules/tests/support/model_based/IBCDefinitions.tla @@ -1,11 +1,36 @@ --------------------------- MODULE IBCDefinitions ----------------------------- -EXTENDS Integers, FiniteSets +EXTENDS Integers, FiniteSets, TLC +(********************** TYPE ANNOTATIONS FOR APALACHE ************************) +\* operator for type annotations +a <: b == a + +ActionType == [ + type |-> STRING, + chainId |-> STRING, + clientState |-> Int, + consensusState |-> Int, + clientId |-> Int, + header |-> Int, + previousConnectionId |-> Int, + counterpartyChainId |-> STRING, + counterpartyClientId |-> Int, + counterpartyConnectionId |-> Int +] +AsAction(a) == a <: ActionType +AsSetAction(S) == S <: {ActionType} +AsSetInt(S) == S <: {Int} +(******************* END OF TYPE ANNOTATIONS FOR APALACHE ********************) + +(******************************** Utils **************************************) +Max(S) == CHOOSE x \in S: \A y \in S: y <= x +(*****************************************************************************) + +\* if a chain identifier is not set then it is "-1" +ChainIdNone == "-1" \* if a client identifier is not set then it is -1 ClientIdNone == -1 -\* if a client identifier is not set then it is -1 -HeightNone == -1 \* if a connection identifier is not set then it is -1 ConnectionIdNone == -1 diff --git a/modules/tests/support/model_based/IBCTests.cfg b/modules/tests/support/model_based/IBCTests.cfg deleted file mode 100644 index e4c28bc288..0000000000 --- a/modules/tests/support/model_based/IBCTests.cfg +++ /dev/null @@ -1,7 +0,0 @@ -CONSTANTS - ChainIds = {"chainA-0", "chainB-0"} - MaxClientsPerChain = 1 - MaxClientHeight = 2 - -INIT Init -NEXT Next diff --git a/modules/tests/support/model_based/IBCTests.tla b/modules/tests/support/model_based/IBCTests.tla index 245461c3c9..52a4978340 100644 --- a/modules/tests/support/model_based/IBCTests.tla +++ b/modules/tests/support/model_based/IBCTests.tla @@ -14,9 +14,64 @@ ICS02ClientNotFoundTest == ICS02HeaderVerificationFailureTest == /\ actionOutcome = "ICS02HeaderVerificationFailure" +ICS03ConnectionOpenInitOKTest == + /\ actionOutcome = "ICS03ConnectionOpenInitOK" + +ICS03MissingClientTest == + /\ actionOutcome = "ICS03MissingClient" + +ICS03ConnectionOpenTryOKTest == + /\ actionOutcome = "ICS03ConnectionOpenTryOK" + +ICS03InvalidConsensusHeightTest == + /\ actionOutcome = "ICS03InvalidConsensusHeight" + +ICS03ConnectionNotFoundTest == + /\ actionOutcome = "ICS03ConnectionNotFound" + +ICS03ConnectionMismatchTest == + /\ actionOutcome = "ICS03ConnectionMismatch" + +ICS03MissingClientConsensusStateTest == + /\ actionOutcome = "ICS03MissingClientConsensusState" + +ICS03InvalidProofTest == + /\ actionOutcome = "ICS03InvalidProof" + +ICS03ConnectionOpenAckOKTest == + /\ actionOutcome = "ICS03ConnectionOpenAckOK" + +ICS03UninitializedConnectionTest == + /\ actionOutcome = "ICS03UninitializedConnection" + +ICS03ConnectionOpenConfirmOKTest == + /\ actionOutcome = "ICS03ConnectionOpenConfirmOK" + +\* ICS02CreateClient tests ICS02CreateOKTestNeg == ~ICS02CreateOKTest + +\* ICS02UpdateClient tests ICS02UpdateOKTestNeg == ~ICS02UpdateOKTest ICS02ClientNotFoundTestNeg == ~ICS02ClientNotFoundTest ICS02HeaderVerificationFailureTestNeg == ~ICS02HeaderVerificationFailureTest +\* ICS03ConnectionOpenInit tests +ICS03ConnectionOpenInitOKTestNeg == ~ICS03ConnectionOpenInitOKTest +ICS03MissingClientTestNeg == ~ICS03MissingClientTest + +\* ICS03ConnectionOpenTry tests +ICS03ConnectionOpenTryOKTestNeg == ~ICS03ConnectionOpenTryOKTest +ICS03InvalidConsensusHeightTestNeg == ~ICS03InvalidConsensusHeightTest +ICS03ConnectionNotFoundTestNeg == ~ICS03ConnectionNotFoundTest +ICS03ConnectionMismatchTestNeg == ~ICS03ConnectionMismatchTest +ICS03MissingClientConsensusStateTestNeg == ~ICS03MissingClientConsensusStateTest +ICS03InvalidProofTestNeg == ~ICS03InvalidProofTest + +\* ICS03ConnectionOpenAck tests +ICS03ConnectionOpenAckOKTestNeg == ~ICS03ConnectionOpenAckOKTest +ICS03UninitializedConnectionTestNeg == ~ICS03UninitializedConnectionTest + +\* ICS03ConnectionOpenConfirm tests +ICS03ConnectionOpenConfirmOKTestNeg == ~ICS03ConnectionOpenConfirmOKTest + =============================================================================== diff --git a/modules/tests/support/model_based/ICS02.tla b/modules/tests/support/model_based/ICS02.tla index 84fa0c4727..658cc2f9c1 100644 --- a/modules/tests/support/model_based/ICS02.tla +++ b/modules/tests/support/model_based/ICS02.tla @@ -1,6 +1,6 @@ ------------------------------- MODULE ICS02 ---------------------------------- -EXTENDS Integers, FiniteSets, IBCDefinitions +EXTENDS IBCDefinitions \* retrieves `clientId`'s data ICS02_GetClient(clients, clientId) == @@ -8,64 +8,88 @@ ICS02_GetClient(clients, clientId) == \* check if `clientId` exists ICS02_ClientExists(clients, clientId) == - ICS02_GetClient(clients, clientId).height /= HeightNone + ICS02_GetClient(clients, clientId).heights /= AsSetInt({}) \* update `clientId`'s data ICS02_SetClient(clients, clientId, client) == [clients EXCEPT ![clientId] = client] -ICS02_CreateClient(clients, clientIdCounter, clientHeight) == +ICS02_CreateClient(chain, chainId, height) == + LET action == AsAction([ + type |-> "ICS02CreateClient", + chainId |-> chainId, + clientState |-> height, + consensusState |-> height + ]) IN \* check if the client exists (it shouldn't) - IF ICS02_ClientExists(clients, clientIdCounter) THEN + IF ICS02_ClientExists(chain.clients, chain.clientIdCounter) THEN \* if the client to be created already exists, \* then there's an error in the model [ - clients |-> clients, - clientIdCounter |-> clientIdCounter, + clients |-> chain.clients, + clientIdCounter |-> chain.clientIdCounter, + action |-> action, outcome |-> "ModelError" ] ELSE \* if it doesn't, create it LET client == [ - height |-> clientHeight + heights|-> {height} ] IN \* return result with updated state [ - clients |-> ICS02_SetClient(clients, clientIdCounter, client), - clientIdCounter |-> clientIdCounter + 1, + clients |-> ICS02_SetClient( + chain.clients, + chain.clientIdCounter, + client + ), + clientIdCounter |-> chain.clientIdCounter + 1, + action |-> action, outcome |-> "ICS02CreateOK" ] -ICS02_UpdateClient(clients, clientId, clientHeight) == +ICS02_UpdateClient(chain, chainId, clientId, height) == + LET action == AsAction([ + type |-> "ICS02UpdateClient", + chainId |-> chainId, + clientId |-> clientId, + header |-> height + ]) IN \* check if the client exists - IF ICS02_ClientExists(clients, clientId) THEN + IF ~ICS02_ClientExists(chain.clients, clientId) THEN + \* if the client does not exist, then set an error outcome + [ + clients |-> chain.clients, + action |-> action, + outcome |-> "ICS02ClientNotFound" + ] + ELSE \* if the client exists, check its height - LET client == ICS02_GetClient(clients, clientId) IN - IF client.height < clientHeight THEN - \* if the client's height is lower than the one being updated to - \* then, update the client + LET client == ICS02_GetClient(chain.clients, clientId) IN + LET highestHeight == Max(client.heights) IN + IF highestHeight >= height THEN + \* if the client's new height is not higher than the highest client + \* height, then set an error outcome + [ + clients |-> chain.clients, + action |-> action, + outcome |-> "ICS02HeaderVerificationFailure" + ] + ELSE + \* if the client's new height is higher than the highest client + \* height, then update the client LET updatedClient == [client EXCEPT - !.height = clientHeight + !.heights = client.heights \union {height} ] IN \* return result with updated state [ - clients |-> ICS02_SetClient(clients, clientId, updatedClient), + clients |-> ICS02_SetClient( + chain.clients, + clientId, + updatedClient + ), + action |-> action, outcome |-> "ICS02UpdateOK" ] - ELSE - \* if the client's height is at least as high as the one being - \* updated to, then set an error outcome - [ - clients |-> clients, - outcome |-> "ICS02HeaderVerificationFailure" - ] - ELSE - \* if the client does not exist, then set an error outcome - [ - clients |-> clients, - outcome |-> "ICS02ClientNotFound" - ] - \* TODO: distinguish between client state and consensus state to also be - \* able to return a `ConsensusStateNotFound` error outcome =============================================================================== diff --git a/modules/tests/support/model_based/ICS03.tla b/modules/tests/support/model_based/ICS03.tla new file mode 100644 index 0000000000..f89d9341ed --- /dev/null +++ b/modules/tests/support/model_based/ICS03.tla @@ -0,0 +1,430 @@ +------------------------------ MODULE ICS03 ----------------------------------- + +EXTENDS ICS02 + +\* retrieves `connectionId`'s data +ICS03_GetConnection(connections, connectionId) == + connections[connectionId] + +\* check if `connectionId` exists +ICS03_ConnectionExists(connections, connectionId) == + ICS03_GetConnection(connections, connectionId).state /= "Uninitialized" + +\* update `connectionId`'s data +ICS03_SetConnection(connections, connectionId, connection) == + [connections EXCEPT ![connectionId] = connection] + +ICS03_ConnectionOpenInit( + chain, + chainId, + clientId, + counterpartyChainId, + counterpartyClientId +) == + LET action == AsAction([ + type |-> "ICS03ConnectionOpenInit", + chainId |-> chainId, + clientId |-> clientId, + counterpartyChainId |-> counterpartyChainId, + counterpartyClientId |-> counterpartyClientId + ]) IN + \* check if the client exists + IF ~ICS02_ClientExists(chain.clients, clientId) THEN + \* if the client does not exist, then set an error outcome + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03MissingClient" + ] + ELSE + \* if the client exists, + \* then check if the connection exists (it shouldn't) + IF ICS03_ConnectionExists(chain.connections, chain.connectionIdCounter) THEN + \* if the connection to be created already exists, + \* then there's an error in the model + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ModelError" + ] + ELSE + \* if it doesn't, create it + LET connection == [ + state |-> "Init", + chainId |-> chainId, + clientId |-> clientId, + \* generate a new connection identifier + connectionId |-> chain.connectionIdCounter, + counterpartyChainId |-> counterpartyChainId, + counterpartyClientId |-> counterpartyClientId, + counterpartyConnectionId |-> ConnectionIdNone + ] IN + \* return result with updated state + [ + connections |-> ICS03_SetConnection( + chain.connections, + chain.connectionIdCounter, + connection + ), + connectionIdCounter |-> chain.connectionIdCounter + 1, + action |-> action, + outcome |-> "ICS03ConnectionOpenInitOK" + ] + +ICS03_ConnectionOpenTry( + chain, + chainId, + clientId, + previousConnectionId, + height, + counterpartyChainId, + counterpartyClientId, + counterpartyConnectionId +) == + LET action == AsAction([ + type |-> "ICS03ConnectionOpenTry", + chainId |-> chainId, + clientId |-> clientId, + previousConnectionId |-> previousConnectionId, + clientState |-> height, + counterpartyChainId |-> counterpartyChainId, + counterpartyClientId |-> counterpartyClientId, + counterpartyConnectionId |-> counterpartyConnectionId + ]) IN + \* check if client's claimed height is higher than the chain's height + IF height > chain.height THEN + \* if client's height is too advanced, then set an error outcome + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03InvalidConsensusHeight" + ] + \* TODO: add `chain_max_history_size` to the model to be able to also + \* return a `ICS03StaleConsensusHeight` error outcome + ELSE + \* check if there's a `previousConnectionId`. this situation can happen + \* where there are two concurrent open init's establishing a connection + \* between the same two chains, say chainA and chainB; then, when chainB + \* sees the open init from chainA, instead of creating a new connection + \* identifier, it can reuse the identifier created by its own open init. + IF previousConnectionId /= ConnectionIdNone THEN + \* if so, check if the connection exists + IF ~ICS03_ConnectionExists(chain.connections, previousConnectionId) THEN + \* if the connection does not exist, then set an error outcome + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03ConnectionNotFound" + ] + ELSE + \* if the connection exists, verify that is matches the the + \* parameters provided + LET connection == ICS03_GetConnection( + chain.connections, + previousConnectionId + ) IN + LET validConnection == + /\ connection.state = "Init" + /\ connection.clientId = clientId + /\ connection.counterpartyClientId = counterpartyClientId + /\ connection.counterpartyConnectionId = counterpartyConnectionId IN + IF ~validConnection THEN + \* if the existing connection does not match, then set an + \* error outcome + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03ConnectionMismatch" + ] + ELSE + \* verification passed; update the connection state to + \* "TryOpen" + LET updatedConnection == [connection EXCEPT + !.state = "TryOpen" + ] IN + \* return result with updated state + [ + connections |-> ICS03_SetConnection( + chain.connections, + previousConnectionId, + updatedConnection + ), + \* as the connection identifier has already been + \* created, here we do not update the + \* `connectionIdCounter` + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03ConnectionOpenTryOK" + ] + ELSE + \* in this case, `previousConnectionId` was not set; check if the + \* client exists + IF ~ICS02_ClientExists(chain.clients, clientId) THEN + \* if the client does not exist, then set an error outcome + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03MissingClient" + ] + ELSE + \* check if the client has a consensus state with this height + LET client == ICS02_GetClient(chain.clients, clientId) IN + LET consensusStateExists == height \in client.heights IN + IF ~consensusStateExists THEN + \* if the client does have a consensus state with this + \* height, then set an error outcome + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03MissingClientConsensusState" + ] + ELSE + \* check if there was an open init at the remote chain + LET openInitProofs == { + proof \in chain.connectionProofs : + /\ proof.type = "ICS03ConnectionOpenInit" + /\ proof.chainId = counterpartyChainId + /\ proof.clientId = counterpartyClientId + /\ proof.counterpartyChainId = chainId + /\ proof.counterpartyClientId = clientId + } IN + LET proofExists == Cardinality(openInitProofs) > 0 IN + IF ~proofExists THEN + \* if there wasn't an open init at the remote chain, + \* then set an error outcome + [ + connections |-> chain.connections, + connectionIdCounter |-> chain.connectionIdCounter, + action |-> action, + outcome |-> "ICS03InvalidProof" + ] + ELSE + \* verification passed; create connection + LET connection == [ + state |-> "TryOpen", + chainId |-> chainId, + clientId |-> clientId, + \* generate a new connection identifier + connectionId |-> chain.connectionIdCounter, + counterpartyChainId |-> counterpartyChainId, + counterpartyClientId |-> counterpartyClientId, + counterpartyConnectionId |-> counterpartyConnectionId + ] IN + \* return result with updated state + [ + connections |-> ICS03_SetConnection( + chain.connections, + chain.connectionIdCounter, + connection + ), + \* since a new connection identifier has been + \* created, here we update the `connectionIdCounter` + connectionIdCounter |-> chain.connectionIdCounter + 1, + action |-> action, + outcome |-> "ICS03ConnectionOpenTryOK" + ] + +ICS03_ConnectionOpenAck( + chain, + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId +) == + LET action == AsAction([ + type |-> "ICS03ConnectionOpenAck", + chainId |-> chainId, + connectionId |-> connectionId, + clientState |-> height, + counterpartyChainId |-> counterpartyChainId, + counterpartyConnectionId |-> counterpartyConnectionId + ]) IN + LET clients == chain.clients IN + LET connections == chain.connections IN + LET connectionProofs == chain.connectionProofs IN + \* check if client's claimed height is higher than the chain's height + IF height > chain.height THEN + \* if client's height is too advanced, then set an error outcome + [ + connections |-> connections, + action |-> action, + outcome |-> "ICS03InvalidConsensusHeight" + ] + \* TODO: add `chain_max_history_size` to the model to be able to also + \* return a `ICS03StaleConsensusHeight` error outcome + ELSE + \* check if the connection exists + IF ~ICS03_ConnectionExists(connections, connectionId) THEN + \* if the connection does not exist, then set an error outcome + \* TODO: can't we reuse the same error "ICS03ConnectionNotFound" + \* from conn open try? + [ + connections |-> connections, + action |-> action, + outcome |-> "ICS03UninitializedConnection" + ] + ELSE + \* if the connection exists, verify that is either Init or TryOpen; + \* also check that the counterparty connection id matches + LET connection == ICS03_GetConnection(connections, connectionId) IN + LET validConnection == + /\ connection.state \in {"Init", "TryOpen"} + \* TODO: the implementation is not checking the following; + \* should it? + /\ connection.counterpartyChainId = counterpartyChainId IN + IF ~validConnection THEN + \* if the existing connection does not match, then set an + \* error outcome + [ + connections |-> connections, + action |-> action, + outcome |-> "ICS03ConnectionMismatch" + ] + ELSE + \* check if the client has a consensus state with this height + LET client == ICS02_GetClient(clients, connection.clientId) IN + LET consensusStateExists == height \in client.heights IN + IF ~consensusStateExists THEN + \* if the client does have a consensus state with this + \* height, then set an error outcome + [ + connections |-> connections, + action |-> action, + outcome |-> "ICS03MissingClientConsensusState" + ] + ELSE + \* check if there was an open try at the remote chain + LET openTryProofs == { + proof \in chain.connectionProofs : + /\ proof.type = "ICS03ConnectionOpenTry" + /\ proof.chainId = connection.counterpartyChainId + /\ proof.clientId = connection.counterpartyClientId + /\ proof.counterpartyChainId = connection.chainId + /\ proof.counterpartyClientId = connection.clientId + /\ proof.counterpartyConnectionId = connectionId + } IN + LET proofExists == Cardinality(openTryProofs) > 0 IN + IF ~proofExists THEN + \* if there wasn't an open try at the remote chain, + \* then set an error outcome + [ + connections |-> chain.connections, + action |-> action, + outcome |-> "ICS03InvalidProof" + ] + ELSE + \* verification passed; update the connection state to + \* "Open" + LET updatedConnection == [connection EXCEPT + !.state = "Open" + ] IN + \* return result with updated state + [ + connections |-> ICS03_SetConnection( + connections, + connectionId, + updatedConnection + ), + action |-> action, + outcome |-> "ICS03ConnectionOpenAckOK" + ] + +ICS03_ConnectionOpenConfirm( + chain, + chainId, + connectionId, + height, + counterpartyChainId, + counterpartyConnectionId +) == + LET action == AsAction([ + type |-> "ICS03ConnectionOpenConfirm", + chainId |-> chainId, + connectionId |-> connectionId, + clientState |-> height, + counterpartyChainId |-> counterpartyChainId, + counterpartyConnectionId |-> counterpartyConnectionId + ]) IN + LET clients == chain.clients IN + LET connections == chain.connections IN + LET connectionProofs == chain.connectionProofs IN + \* check if the connection exists + IF ~ICS03_ConnectionExists(connections, connectionId) THEN + \* if the connection does not exist, then set an error outcome + \* TODO: can't we reuse the same error "ICS03ConnectionNotFound" + \* from conn open try? + [ + connections |-> connections, + action |-> action, + outcome |-> "ICS03UninitializedConnection" + ] + ELSE + \* if the connection exists, verify that is either Init or TryOpen; + \* also check that the counterparty connection id matches + LET connection == ICS03_GetConnection(connections, connectionId) IN + LET validConnection == connection.state = "TryOpen" IN + IF ~validConnection THEN + \* if the existing connection does not match, then set an + \* error outcome + [ + connections |-> connections, + action |-> action, + outcome |-> "ICS03ConnectionMismatch" + ] + ELSE + \* check if the client has a consensus state with this height + LET client == ICS02_GetClient(clients, connection.clientId) IN + LET consensusStateExists == height \in client.heights IN + IF ~consensusStateExists THEN + \* if the client does have a consensus state with this + \* height, then set an error outcome + [ + connections |-> connections, + action |-> action, + outcome |-> "ICS03MissingClientConsensusState" + ] + ELSE + \* check if there was an open ack at the remote chain + LET openAckProofs == { + proof \in chain.connectionProofs : + /\ proof.type = "ICS03ConnectionOpenAck" + /\ proof.chainId = connection.counterpartyChainId + /\ proof.connectionId = connection.counterpartyConnectionId + /\ proof.counterpartyChainId = connection.chainId + /\ proof.counterpartyConnectionId = connectionId + } IN + LET proofExists == Cardinality(openAckProofs) > 0 IN + IF ~proofExists THEN + \* if there wasn't an open ack at the remote chain, + \* then set an error outcome + [ + connections |-> chain.connections, + action |-> action, + outcome |-> "ICS03InvalidProof" + ] + ELSE + \* verification passed; update the connection state to + \* "Open" + LET updatedConnection == [connection EXCEPT + !.state = "Open" + ] IN + \* return result with updated state + [ + connections |-> ICS03_SetConnection( + connections, + connectionId, + updatedConnection + ), + action |-> action, + outcome |-> "ICS03ConnectionOpenConfirmOK" + ] + +=============================================================================== diff --git a/modules/tests/support/model_based/gen_tests.py b/modules/tests/support/model_based/gen_tests.py new file mode 100755 index 0000000000..7797fb24aa --- /dev/null +++ b/modules/tests/support/model_based/gen_tests.py @@ -0,0 +1,43 @@ +#!/usr/bin/env python3 + +import os + +CFG = """ +CONSTANTS + ChainIds = {"chainA", "chainB"} + MaxChainHeight = 4 + MaxClientsPerChain = 1 + MaxConnectionsPerChain = 1 + +INIT Init +NEXT Next + +""" + +tests = [ + "ICS02CreateOKTest", + "ICS02UpdateOKTest", + "ICS02ClientNotFoundTest", + "ICS02HeaderVerificationFailureTest", + "ICS03ConnectionOpenInitOKTest", + "ICS03MissingClientTest", + "ICS03ConnectionOpenTryOKTest", + "ICS03InvalidConsensusHeightTest", + "ICS03ConnectionNotFoundTest", + "ICS03ConnectionMismatchTest", + "ICS03MissingClientConsensusStateTest", + "ICS03InvalidProofTest", + "ICS03ConnectionOpenAckOKTest", + "ICS03UninitializedConnectionTest", + "ICS03ConnectionOpenConfirmOKTest", +] + +for test in tests: + # create IBCTests.cfg file + with open("IBCTests.cfg", "w") as file: + file.write(CFG + "INVARIANT " + test + "Neg") + + # run tlc-json + print("> generating " + test) + os.system("tlc-json IBCTests.tla") + os.system("mv counterexample.json tests/" + test + ".json") diff --git a/modules/tests/support/model_based/tests/ICS02ClientNotFoundTest.json b/modules/tests/support/model_based/tests/ICS02ClientNotFoundTest.json new file mode 100644 index 0000000000..f0908502b3 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS02ClientNotFoundTest.json @@ -0,0 +1,101 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "header": 1, + "type": "ICS02UpdateClient" + }, + "actionOutcome": "ICS02ClientNotFound", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS02CreateOKTest.json b/modules/tests/support/model_based/tests/ICS02CreateOKTest.json new file mode 100644 index 0000000000..8101454208 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS02CreateOKTest.json @@ -0,0 +1,103 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS02HeaderVerificationFailureTest.json b/modules/tests/support/model_based/tests/ICS02HeaderVerificationFailureTest.json index 32a85c138a..5295bc24be 100644 --- a/modules/tests/support/model_based/tests/ICS02HeaderVerificationFailureTest.json +++ b/modules/tests/support/model_based/tests/ICS02HeaderVerificationFailureTest.json @@ -1,49 +1,156 @@ [ - { - "action": { - "type": "None" - }, - "actionOutcome": "None", - "chains": { - "chainA-0": { - "height": 0 - }, - "chainB-0": { - "height": 0 - } - } + { + "action": { + "type": "None" }, - { - "action": { - "chainId": "chainB-0", - "clientHeight": 1, - "type": "ICS02CreateClient" - }, - "actionOutcome": "ICS02CreateOK", - "chains": { - "chainA-0": { - "height": 0 - }, - "chainB-0": { - "height": 1 - } - } + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" }, - { - "action": { - "chainId": "chainB-0", - "clientHeight": 1, - "clientId": 0, - "type": "ICS02UpdateClient" - }, - "actionOutcome": "ICS02HeaderVerificationFailure", - "chains": { - "chainA-0": { - "height": 0 - }, - "chainB-0": { - "height": 1 - } - } + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "header": 1, + "type": "ICS02UpdateClient" + }, + "actionOutcome": "ICS02HeaderVerificationFailure", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } } -] + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS02UpdateOKTest.json b/modules/tests/support/model_based/tests/ICS02UpdateOKTest.json index 5275bfcda3..aa0b59f950 100644 --- a/modules/tests/support/model_based/tests/ICS02UpdateOKTest.json +++ b/modules/tests/support/model_based/tests/ICS02UpdateOKTest.json @@ -1,115 +1,157 @@ [ - { - "action": { - "type": "None" - }, - "actionOutcome": "None", - "chains": { - "chainA-0": { - "height": 0 - }, - "chainB-0": { - "height": 0 - } - } + { + "action": { + "type": "None" }, - { - "action": { - "chainId": "chainB-0", - "clientHeight": 1, - "type": "ICS02CreateClient" + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } }, - "actionOutcome": "ICS02CreateOK", - "chains": { - "chainA-0": { - "height": 0 - }, - "chainB-0": { - "height": 1 - } - } - }, - { - "action": { - "chainId": "chainB-0", - "clientHeight": 2, - "clientId": 0, - "type": "ICS02UpdateClient" + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } }, - "actionOutcome": "ICS02UpdateOK", - "chains": { - "chainA-0": { - "height": 0 - }, - "chainB-0": { - "height": 2 - } - } - }, - { - "action": { - "chainId": "chainA-0", - "clientHeight": 1, - "type": "ICS02CreateClient" + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } }, - "actionOutcome": "ICS02CreateOK", - "chains": { - "chainA-0": { - "height": 1 - }, - "chainB-0": { - "height": 2 - } - } - }, - { - "action": { - "chainId": "chainA-0", - "clientHeight": 2, - "clientId": 0, - "type": "ICS02UpdateClient" + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } }, - "actionOutcome": "ICS02UpdateOK", - "chains": { - "chainA-0": { - "height": 2 - }, - "chainB-0": { - "height": 2 - } - } + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" }, - { - "action": { - "chainId": "chainA-0", - "clientHeight": 1, - "type": "ICS02CreateClient" + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } }, - "actionOutcome": "ICS02CreateOK", - "chains": { - "chainA-0": { - "height": 3 - }, - "chainB-0": { - "height": 2 - } - } + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "header": 2, + "type": "ICS02UpdateClient" }, - { - "action": { - "chainId": "chainA-0", - "clientHeight": 2, - "clientId": 1, - "type": "ICS02UpdateClient" + "actionOutcome": "ICS02UpdateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1, + 2 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } }, - "actionOutcome": "ICS02UpdateOK", - "chains": { - "chainA-0": { - "height": 4 - }, - "chainB-0": { - "height": 2 - } - } + "height": 1 + } } -] + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionMismatchTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionMismatchTest.json new file mode 100644 index 0000000000..830032c4cc --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionMismatchTest.json @@ -0,0 +1,230 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03ConnectionOpenInitOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "clientId": 0, + "connectionId": 0, + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": 0, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03ConnectionMismatch", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "clientId": 0, + "connectionId": 0, + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionNotFoundTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionNotFoundTest.json new file mode 100644 index 0000000000..db9ab2f953 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionNotFoundTest.json @@ -0,0 +1,160 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 3, + "consensusState": 3, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": 0, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03ConnectionNotFound", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckOKTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckOKTest.json new file mode 100644 index 0000000000..80db392a89 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckOKTest.json @@ -0,0 +1,414 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03ConnectionOpenInitOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03ConnectionOpenTryOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + } + ], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "chainId": "chainB", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "state": "TryOpen" + } + }, + "height": 3 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + }, + "actionOutcome": "ICS03ConnectionOpenAckOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + } + ], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Open" + } + }, + "height": 4 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + { + "chainId": "chainA", + "clientState": 1, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + } + ], + "connections": { + "0": { + "chainId": "chainB", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "state": "TryOpen" + } + }, + "height": 3 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionOpenConfirmOKTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionOpenConfirmOKTest.json new file mode 100644 index 0000000000..ad9d75ed14 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionOpenConfirmOKTest.json @@ -0,0 +1,502 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 3, + "consensusState": 3, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03ConnectionOpenInitOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03ConnectionOpenTryOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + } + ], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "chainId": "chainB", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "state": "TryOpen" + } + }, + "height": 3 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 3, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + }, + "actionOutcome": "ICS03ConnectionOpenAckOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + } + ], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Open" + } + }, + "height": 4 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + { + "chainId": "chainA", + "clientState": 3, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + } + ], + "connections": { + "0": { + "chainId": "chainB", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "state": "TryOpen" + } + }, + "height": 3 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientState": 1, + "connectionId": 0, + "counterpartyChainId": "chainA", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenConfirm" + }, + "actionOutcome": "ICS03ConnectionOpenConfirmOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + } + ], + "connections": { + "0": { + "chainId": "chainA", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Open" + } + }, + "height": 4 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + { + "chainId": "chainA", + "clientState": 3, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + } + ], + "connections": { + "0": { + "chainId": "chainB", + "clientId": 0, + "connectionId": 0, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "state": "Open" + } + }, + "height": 4 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionOpenInitOKTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionOpenInitOKTest.json new file mode 100644 index 0000000000..0f8f565ddb --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionOpenInitOKTest.json @@ -0,0 +1,165 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03ConnectionOpenInitOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "clientId": 0, + "connectionId": 0, + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionOpenTryOKTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionOpenTryOKTest.json new file mode 100644 index 0000000000..2fe2db8dee --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionOpenTryOKTest.json @@ -0,0 +1,306 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03ConnectionOpenInitOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "clientId": 0, + "connectionId": 0, + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [], + "connections": { + "0": { + "clientId": 0, + "connectionId": 0, + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03ConnectionOpenTryOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + } + ], + "connections": { + "0": { + "clientId": 0, + "connectionId": 0, + "counterpartyClientId": 0, + "counterpartyConnectionId": -1, + "state": "Init" + } + }, + "height": 3 + }, + "chainB": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 1, + "connectionProofs": [ + { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + } + ], + "connections": { + "0": { + "clientId": 0, + "connectionId": 0, + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "state": "TryOpen" + } + }, + "height": 3 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03InvalidConsensusHeightTest.json b/modules/tests/support/model_based/tests/ICS03InvalidConsensusHeightTest.json new file mode 100644 index 0000000000..9b2b2c84c7 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03InvalidConsensusHeightTest.json @@ -0,0 +1,105 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "clientState": 2, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03InvalidConsensusHeight", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03InvalidProofTest.json b/modules/tests/support/model_based/tests/ICS03InvalidProofTest.json new file mode 100644 index 0000000000..dd3df3cd39 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03InvalidProofTest.json @@ -0,0 +1,160 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03InvalidProof", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 1 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03MissingClientConsensusStateTest.json b/modules/tests/support/model_based/tests/ICS03MissingClientConsensusStateTest.json new file mode 100644 index 0000000000..58e8d1c3c5 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03MissingClientConsensusStateTest.json @@ -0,0 +1,160 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 3, + "consensusState": 3, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03MissingClientConsensusState", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03MissingClientTest.json b/modules/tests/support/model_based/tests/ICS03MissingClientTest.json new file mode 100644 index 0000000000..0c865ae8a2 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03MissingClientTest.json @@ -0,0 +1,102 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03MissingClient", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "clientId": -1, + "connectionId": -1, + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03UninitializedConnectionTest.json b/modules/tests/support/model_based/tests/ICS03UninitializedConnectionTest.json new file mode 100644 index 0000000000..3dcdd3b2f8 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03UninitializedConnectionTest.json @@ -0,0 +1,170 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 3, + "consensusState": 3, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + }, + "actionOutcome": "ICS03UninitializedConnection", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 3 + ] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 2 + }, + "chainB": { + "clientIdCounter": 0, + "clients": { + "0": { + "heights": [] + } + }, + "connectionIdCounter": 0, + "connectionProofs": [], + "connections": { + "0": { + "chainId": "-1", + "clientId": -1, + "connectionId": -1, + "counterpartyChainId": "-1", + "counterpartyClientId": -1, + "counterpartyConnectionId": -1, + "state": "Uninitialized" + } + }, + "height": 1 + } + } + } +] \ No newline at end of file