diff --git a/modules/src/ics03_connection/connection.rs b/modules/src/ics03_connection/connection.rs index 3bfb0624ea..c8afe69038 100644 --- a/modules/src/ics03_connection/connection.rs +++ b/modules/src/ics03_connection/connection.rs @@ -1,7 +1,7 @@ use std::convert::{TryFrom, TryInto}; use std::str::FromStr; -use serde::Serialize; +use serde::{Deserialize, Serialize}; use tendermint_proto::Protobuf; use ibc_proto::ibc::core::connection::v1::{ @@ -248,7 +248,7 @@ impl Counterparty { } } -#[derive(Clone, Debug, PartialEq, Eq, Serialize)] +#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum State { Uninitialized = 0, Init = 1, diff --git a/modules/tests/Makefile b/modules/tests/Makefile new file mode 100644 index 0000000000..9e67ed6690 --- /dev/null +++ b/modules/tests/Makefile @@ -0,0 +1,5 @@ +mbt: + cargo t --features mocks -- --nocapture mbt + +stateright: + cargo t --features mocks -- --nocapture stateright diff --git a/modules/tests/executor/mod.rs b/modules/tests/executor/mod.rs index 3f37619e98..68ce0da329 100644 --- a/modules/tests/executor/mod.rs +++ b/modules/tests/executor/mod.rs @@ -2,12 +2,12 @@ pub mod modelator; pub mod step; use ibc::ics02_client::client_def::{AnyClientState, AnyConsensusState, AnyHeader}; -use ibc::ics02_client::client_type::ClientType; +use ibc::ics02_client::context::ClientReader; use ibc::ics02_client::error::Kind as ICS02ErrorKind; use ibc::ics02_client::msgs::create_client::MsgCreateAnyClient; use ibc::ics02_client::msgs::update_client::MsgUpdateAnyClient; use ibc::ics02_client::msgs::ClientMsg; -use ibc::ics03_connection::connection::Counterparty; +use ibc::ics03_connection::connection::{Counterparty, State as ConnectionState}; use ibc::ics03_connection::error::Kind as ICS03ErrorKind; use ibc::ics03_connection::msgs::conn_open_ack::MsgConnectionOpenAck; use ibc::ics03_connection::msgs::conn_open_confirm::MsgConnectionOpenConfirm; @@ -27,6 +27,7 @@ use ibc::mock::header::MockHeader; use ibc::mock::host::HostType; use ibc::proofs::{ConsensusProof, Proofs}; use ibc::Height; +use ibc::{ics02_client::client_type::ClientType, ics04_channel::context::ChannelReader}; use std::collections::HashMap; use std::error::Error; use std::fmt::{Debug, Display}; @@ -200,11 +201,72 @@ impl IBCTestExecutor { self.contexts.values().all(|ctx| ctx.validate().is_ok()) } - /// Check that chain heights match the ones in the model. - pub fn check_chain_heights(&self, chains: HashMap) -> bool { + /// Check that chain states match the ones in the model. + pub fn check_chain_states(&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) + // check that heights match + let heights_match = ctx.query_latest_height() == Self::height(chain.height); + + // check that clients match + let clients_match = chain.clients.into_iter().all(|(client_id, client)| { + client.heights.into_iter().all(|height| { + // check that each consensus state from the model exists + ctx.consensus_state(&Self::client_id(client_id), Self::height(height)) + .is_some() + }) + }); + + // check that connections match + let connections_match = + chain + .connections + .into_iter() + .all(|(connection_id, connection)| { + if connection.state == ConnectionState::Uninitialized { + // if the connection has not yet been initialized, then + // there's nothing to check + true + } else { + if let Some(connection_end) = + ctx.connection_end(&Self::connection_id(connection_id)) + { + println!("END: {:?}", connection_end); + // states must match + let states_match = *connection_end.state() == connection.state; + + // client ids must match + let client_ids = *connection_end.client_id() + == Self::client_id(connection.client_id.unwrap()); + + // counterparty client ids must match + let counterparty_client_ids = *connection_end + .counterparty() + .client_id() + == Self::client_id(connection.counterparty_client_id.unwrap()); + + // counterparty connection ids must match + let counterparty_connection_ids = + connection_end.counterparty().connection_id() + == connection + .counterparty_connection_id + .map(|connection_id| Self::connection_id(connection_id)) + .as_ref(); + + states_match + && client_ids + && counterparty_client_ids + && counterparty_connection_ids + } else { + // if the connection exists in the model, then it must + // also exist in the implementation; in this case it + // doesn't, so we fail the verification + false + } + } + }); + + heights_match && clients_match && connections_match }) } @@ -360,6 +422,7 @@ impl modelator::TestExecutor for IBCTestExecutor { fn next_step(&mut self, step: Step) -> bool { let result = self.apply(step.action); + println!("{:?} vs {:?}", result, step.action_outcome); let outcome_matches = match step.action_outcome { ActionOutcome::None => panic!("unexpected action outcome"), ActionOutcome::ICS02CreateOK => result.is_ok(), @@ -406,6 +469,6 @@ impl modelator::TestExecutor for IBCTestExecutor { ActionOutcome::ICS03ConnectionOpenConfirmOK => result.is_ok(), }; // also check the state of chains - outcome_matches && self.validate_chains() && self.check_chain_heights(step.chains) + outcome_matches && self.validate_chains() && self.check_chain_states(step.chains) } } diff --git a/modules/tests/executor/modelator.rs b/modules/tests/executor/modelator.rs index 6c7f9a43df..5b4dd39f38 100644 --- a/modules/tests/executor/modelator.rs +++ b/modules/tests/executor/modelator.rs @@ -48,6 +48,7 @@ where let step_count = steps.len(); for (i, step) in steps.iter().enumerate() { + println!("({}/{}) {:?}", i + 1, step_count, step); // check the step let ok = if i == 0 { executor.initial_step(step.clone()) diff --git a/modules/tests/executor/step.rs b/modules/tests/executor/step.rs index 7e0593025c..d8794d013a 100644 --- a/modules/tests/executor/step.rs +++ b/modules/tests/executor/step.rs @@ -1,3 +1,4 @@ +use ibc::ics03_connection::connection::State as ConnectionState; use serde::{Deserialize, Deserializer}; use std::collections::HashMap; use std::fmt::Debug; @@ -53,7 +54,7 @@ pub enum Action { chain_id: String, #[serde(alias = "previousConnectionId")] - #[serde(default, deserialize_with = "deserialize_connection_id")] + #[serde(default, deserialize_with = "deserialize_id")] previous_connection_id: Option, #[serde(alias = "clientId")] @@ -105,21 +106,6 @@ pub enum Action { }, } -/// On the model, a non-existing `connection_id` is represented with -1. -/// For this reason, this function maps a `Some(-1)` to a `None`. -fn deserialize_connection_id<'de, D>(deserializer: D) -> Result, 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)] pub enum ActionOutcome { None, @@ -143,4 +129,50 @@ pub enum ActionOutcome { #[derive(Debug, Clone, PartialEq, Deserialize)] pub struct Chain { pub height: u64, + + pub clients: HashMap, + + pub connections: HashMap, +} + +#[derive(Debug, Clone, PartialEq, Deserialize)] +pub struct Client { + pub heights: Vec, +} + +#[derive(Debug, Clone, PartialEq, Deserialize)] +pub struct Connection { + #[serde(alias = "clientId")] + #[serde(default, deserialize_with = "deserialize_id")] + pub client_id: Option, + + #[serde(alias = "connectionId")] + #[serde(default, deserialize_with = "deserialize_id")] + pub connection_id: Option, + + #[serde(alias = "counterpartyClientId")] + #[serde(default, deserialize_with = "deserialize_id")] + pub counterparty_client_id: Option, + + #[serde(alias = "counterpartyConnectionId")] + #[serde(default, deserialize_with = "deserialize_id")] + pub counterparty_connection_id: Option, + + pub state: ConnectionState, +} + +/// On the model, a non-existing `client_id` and a `connection_id` is +/// represented with -1. +/// For this reason, this function maps a `Some(-1)` to a `None`. +fn deserialize_id<'de, D>(deserializer: D) -> Result, D::Error> +where + D: Deserializer<'de>, +{ + let id: Option = Deserialize::deserialize(deserializer)?; + let id = if id == Some(-1) { + None + } else { + id.map(|id| id as u64) + }; + Ok(id) } diff --git a/modules/tests/gen_tests_loop.sh b/modules/tests/gen_tests_loop.sh new file mode 100755 index 0000000000..9cd06acc9b --- /dev/null +++ b/modules/tests/gen_tests_loop.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash + +cd support/model_based/ +gen_tests.py +cd - +make + diff --git a/modules/tests/mbt.rs b/modules/tests/mbt.rs index a97f0ff736..3d240295fa 100644 --- a/modules/tests/mbt.rs +++ b/modules/tests/mbt.rs @@ -5,23 +5,25 @@ const TESTS_DIR: &str = "tests/support/model_based/tests"; #[test] fn mbt() { let tests = vec![ - "ICS02CreateOKTest", - "ICS02UpdateOKTest", - "ICS02ClientNotFoundTest", - "ICS02HeaderVerificationFailureTest", - "ICS03ConnectionOpenInitOKTest", - "ICS03MissingClientTest", - "ICS03ConnectionOpenTryOKTest", - "ICS03InvalidConsensusHeightTest", - "ICS03ConnectionNotFoundTest", - "ICS03ConnectionMismatchTest", - "ICS03MissingClientConsensusStateTest", + // "ICS02CreateOKTest", + // "ICS02UpdateOKTest", + // "ICS02ClientNotFoundTest", + // "ICS02HeaderVerificationFailureTest", + // "ICS03ConnectionOpenInitOKTest", + // "ICS03MissingClientTest", + // "ICS03ConnectionOpenTryOKTest", + "ICS03ConnectionOpenTryStateInitTest", + // "ICS03InvalidConsensusHeightTest", + // "ICS03ConnectionNotFoundTest", + // "ICS03ConnectionMismatchTest", + // "ICS03MissingClientConsensusStateTest", // TODO: the following test should fail but doesn't because proofs are // not yet verified // "ICS03InvalidProofTest", - "ICS03ConnectionOpenAckOKTest", - "ICS03UninitializedConnectionTest", - "ICS03ConnectionOpenConfirmOKTest", + // "ICS03ConnectionOpenAckOKTest", + // "ICS03UninitializedConnectionTest", + // "ICS03ConnectionOpenAckTryOpenStateTest", + // "ICS03ConnectionOpenConfirmOKTest", ]; for test in tests { diff --git a/modules/tests/support/model_based/IBCTests.cfg b/modules/tests/support/model_based/IBCTests.cfg new file mode 100644 index 0000000000..8f4cb2787a --- /dev/null +++ b/modules/tests/support/model_based/IBCTests.cfg @@ -0,0 +1,11 @@ + +CONSTANTS + ChainIds = {"chainA", "chainB"} + MaxChainHeight = 5 + MaxClientsPerChain = 1 + MaxConnectionsPerChain = 1 + +INIT InitTest +NEXT NextTest + +INVARIANT ICS03ConnectionOpenTryStateInitTestNeg \ No newline at end of file diff --git a/modules/tests/support/model_based/IBCTests.tla b/modules/tests/support/model_based/IBCTests.tla index 52a4978340..980198822e 100644 --- a/modules/tests/support/model_based/IBCTests.tla +++ b/modules/tests/support/model_based/IBCTests.tla @@ -1,6 +1,20 @@ ------------------------------ MODULE IBCTests -------------------------------- -EXTENDS IBC +EXTENDS IBC, Sequences + +VARIABLE + previousChains + +PreviousConnectionState(chainId, connectionId) == + previousChains[chainId].connections[connectionId].state + +InitTest == + /\ Init + /\ previousChains = chains + +NextTest == + /\ Next + /\ previousChains' = chains ICS02CreateOKTest == /\ actionOutcome = "ICS02CreateOK" @@ -23,6 +37,12 @@ ICS03MissingClientTest == ICS03ConnectionOpenTryOKTest == /\ actionOutcome = "ICS03ConnectionOpenTryOK" +ICS03ConnectionOpenTryStateInitTest == + /\ action.type = "ICS03ConnectionOpenTry" + /\ action.previousConnectionId /= -1 + /\ PreviousConnectionState(action.chainId, action.previousConnectionId) = "Init" + /\ actionOutcome = "ICS03ConnectionOpenTryOK" + ICS03InvalidConsensusHeightTest == /\ actionOutcome = "ICS03InvalidConsensusHeight" @@ -41,6 +61,11 @@ ICS03InvalidProofTest == ICS03ConnectionOpenAckOKTest == /\ actionOutcome = "ICS03ConnectionOpenAckOK" +ICS03ConnectionOpenAckStateTryOpenTest == + /\ action.type = "ICS03ConnectionOpenAck" + /\ PreviousConnectionState(action.chainId, action.connectionId) = "TryOpen" + /\ actionOutcome = "ICS03ConnectionOpenAckOK" + ICS03UninitializedConnectionTest == /\ actionOutcome = "ICS03UninitializedConnection" @@ -61,6 +86,7 @@ ICS03MissingClientTestNeg == ~ICS03MissingClientTest \* ICS03ConnectionOpenTry tests ICS03ConnectionOpenTryOKTestNeg == ~ICS03ConnectionOpenTryOKTest +ICS03ConnectionOpenTryStateInitTestNeg == ~ICS03ConnectionOpenTryStateInitTest ICS03InvalidConsensusHeightTestNeg == ~ICS03InvalidConsensusHeightTest ICS03ConnectionNotFoundTestNeg == ~ICS03ConnectionNotFoundTest ICS03ConnectionMismatchTestNeg == ~ICS03ConnectionMismatchTest @@ -69,6 +95,7 @@ ICS03InvalidProofTestNeg == ~ICS03InvalidProofTest \* ICS03ConnectionOpenAck tests ICS03ConnectionOpenAckOKTestNeg == ~ICS03ConnectionOpenAckOKTest +ICS03ConnectionOpenAckStateTryOpenTestNeg == ~ICS03ConnectionOpenAckStateTryOpenTest ICS03UninitializedConnectionTestNeg == ~ICS03UninitializedConnectionTest \* ICS03ConnectionOpenConfirm tests diff --git a/modules/tests/support/model_based/Makefile b/modules/tests/support/model_based/Makefile new file mode 100644 index 0000000000..079b71b458 --- /dev/null +++ b/modules/tests/support/model_based/Makefile @@ -0,0 +1,5 @@ +check: + apalache-mc check --length=16 --nworkers=12 --inv=ModelNeverErrors IBC.tla + +test: + apalache-mc check --inv=ICS03ConnectionMismatchTestNeg IBCTests.tla diff --git a/modules/tests/support/model_based/gen_tests.py b/modules/tests/support/model_based/gen_tests.py index 7797fb24aa..c7bc353e72 100755 --- a/modules/tests/support/model_based/gen_tests.py +++ b/modules/tests/support/model_based/gen_tests.py @@ -5,31 +5,33 @@ CFG = """ CONSTANTS ChainIds = {"chainA", "chainB"} - MaxChainHeight = 4 + MaxChainHeight = 5 MaxClientsPerChain = 1 MaxConnectionsPerChain = 1 -INIT Init -NEXT Next +INIT InitTest +NEXT NextTest """ tests = [ - "ICS02CreateOKTest", - "ICS02UpdateOKTest", - "ICS02ClientNotFoundTest", - "ICS02HeaderVerificationFailureTest", - "ICS03ConnectionOpenInitOKTest", - "ICS03MissingClientTest", - "ICS03ConnectionOpenTryOKTest", - "ICS03InvalidConsensusHeightTest", - "ICS03ConnectionNotFoundTest", - "ICS03ConnectionMismatchTest", - "ICS03MissingClientConsensusStateTest", - "ICS03InvalidProofTest", - "ICS03ConnectionOpenAckOKTest", - "ICS03UninitializedConnectionTest", - "ICS03ConnectionOpenConfirmOKTest", + # "ICS02CreateOKTest", + # "ICS02UpdateOKTest", + # "ICS02ClientNotFoundTest", + # "ICS02HeaderVerificationFailureTest", + # "ICS03ConnectionOpenInitOKTest", + # "ICS03MissingClientTest", + # "ICS03ConnectionOpenTryOKTest", + "ICS03ConnectionOpenTryStateInitTest", + # "ICS03InvalidConsensusHeightTest", + # "ICS03ConnectionNotFoundTest", + # "ICS03ConnectionMismatchTest", + # "ICS03MissingClientConsensusStateTest", + # "ICS03InvalidProofTest", + # "ICS03ConnectionOpenAckOKTest", + # "ICS03UninitializedConnectionTest", + # "ICS03ConnectionOpenAckStateTryOpenTest", + # "ICS03ConnectionOpenConfirmOKTest", ] for test in tests: @@ -40,4 +42,4 @@ # run tlc-json print("> generating " + test) os.system("tlc-json IBCTests.tla") - os.system("mv counterexample.json tests/" + test + ".json") + os.system("mv counterexample0.json tests/" + test + ".json") diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckStateTryOpenTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckStateTryOpenTest.json new file mode 100644 index 0000000000..3b4f0a4d88 --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckStateTryOpenTest.json @@ -0,0 +1,276 @@ +[ + { + "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 + } + }, + "history": [ + { + "actionOutcome_": "None", + "action_": { + "type": "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, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + }, + "actionOutcome": "ICS03UninitializedConnection", + "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 + } + }, + "history": [ + { + "actionOutcome_": "None", + "action_": { + "type": "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 + } + } + }, + { + "actionOutcome_": "ICS03UninitializedConnection", + "action_": { + "chainId": "chainA", + "clientState": 1, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + }, + "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 + } + } + } + ] + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckTryOpenStateTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckTryOpenStateTest.json new file mode 100644 index 0000000000..48950fb12a --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionOpenAckTryOpenStateTest.json @@ -0,0 +1,219 @@ +[ + { + "action": { + "type": "None" + }, + "actionOutcome": "None", + "chains": { + "chainA": { + "clients": {}, + "connections": {}, + "height": 1 + }, + "chainB": { + "clients": {}, + "connections": {}, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clients": {}, + "connections": {}, + "height": 2 + }, + "chainB": { + "clients": {}, + "connections": {}, + "height": 1 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientState": 1, + "consensusState": 1, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clients": {}, + "connections": {}, + "height": 2 + }, + "chainB": { + "clients": {}, + "connections": {}, + "height": 2 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03ConnectionOpenInitOK", + "chains": { + "chainA": { + "clients": {}, + "connections": {}, + "height": 3 + }, + "chainB": { + "clients": {}, + "connections": {}, + "height": 2 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientId": 0, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "type": "ICS03ConnectionOpenInit" + }, + "actionOutcome": "ICS03ConnectionOpenInitOK", + "chains": { + "chainA": { + "clients": {}, + "connections": {}, + "height": 3 + }, + "chainB": { + "clients": {}, + "connections": {}, + "height": 3 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03ConnectionOpenTryOK", + "chains": { + "chainA": { + "clients": {}, + "connections": {}, + "height": 4 + }, + "chainB": { + "clients": {}, + "connections": {}, + "height": 3 + } + } + }, + { + "action": { + "chainId": "chainB", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": -1, + "type": "ICS03ConnectionOpenTry" + }, + "actionOutcome": "ICS03ConnectionOpenTryOK", + "chains": { + "chainA": { + "clients": {}, + "connections": { + "0": { + "chainId": "chainA", + "clientId": 1, + "connectionId": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 1, + "counterpartyConnectionId": 1, + "state": "TryOpen" + } + }, + "height": 4 + }, + "chainB": { + "clients": {}, + "connections": { + "0": { + "chainId": "chainB", + "clientId": 1, + "connectionId": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 1, + "counterpartyConnectionId": 1, + "state": "TryOpen" + } + }, + "height": 4 + } + } + }, + { + "action": { + "chainId": "chainA", + "clientState": 1, + "connectionId": 0, + "counterpartyChainId": "chainB", + "counterpartyConnectionId": 0, + "type": "ICS03ConnectionOpenAck" + }, + "actionOutcome": "ICS03ConnectionOpenAckOK", + "chains": { + "chainA": { + "clients": {}, + "connections": { + "0": { + "chainId": "chainA", + "clientId": 1, + "connectionId": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 1, + "counterpartyConnectionId": 1, + "state": "Open" + } + }, + "height": 5 + }, + "chainB": { + "clients": {}, + "connections": { + "0": { + "chainId": "chainB", + "clientId": 1, + "connectionId": 1, + "counterpartyChainId": "chainA", + "counterpartyClientId": 1, + "counterpartyConnectionId": 1, + "state": "TryOpen" + } + }, + "height": 4 + } + } + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tests/ICS03ConnectionOpenTryStateInitTest.json b/modules/tests/support/model_based/tests/ICS03ConnectionOpenTryStateInitTest.json new file mode 100644 index 0000000000..797e608a9d --- /dev/null +++ b/modules/tests/support/model_based/tests/ICS03ConnectionOpenTryStateInitTest.json @@ -0,0 +1,479 @@ +[ + { + "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 + } + }, + "history": [ + { + "actionOutcome_": "None", + "action_": { + "type": "None" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + } + ] + }, + { + "action": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "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 + } + }, + "history": [ + { + "actionOutcome_": "None", + "action_": { + "type": "None" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + }, + { + "actionOutcome_": "ICS02CreateOK", + "action_": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + } + ] + }, + { + "action": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "actionOutcome": "ICS02CreateOK", + "chains": { + "chainA": { + "clientIdCounter": 1, + "clients": { + "0": { + "heights": [ + 2 + ] + } + }, + "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 + } + }, + "history": [ + { + "actionOutcome_": "None", + "action_": { + "type": "None" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + }, + { + "actionOutcome_": "ICS02CreateOK", + "action_": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + }, + { + "actionOutcome_": "ICS02CreateOK", + "action_": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + } + ] + }, + { + "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": [ + 2 + ] + } + }, + "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 + } + }, + "history": [ + { + "actionOutcome_": "None", + "action_": { + "type": "None" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + }, + { + "actionOutcome_": "ICS02CreateOK", + "action_": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + }, + { + "actionOutcome_": "ICS02CreateOK", + "action_": { + "chainId": "chainA", + "clientState": 2, + "consensusState": 2, + "type": "ICS02CreateClient" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + }, + { + "actionOutcome_": "ICS03ConnectionNotFound", + "action_": { + "chainId": "chainA", + "clientId": 0, + "clientState": 1, + "counterpartyChainId": "chainB", + "counterpartyClientId": 0, + "counterpartyConnectionId": 0, + "previousConnectionId": 0, + "type": "ICS03ConnectionOpenTry" + }, + "chains_": { + "chainA": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + }, + "chainB": { + "connections": { + "0": { + "state": "Uninitialized" + } + } + } + } + } + ] + } +] \ No newline at end of file diff --git a/modules/tests/support/model_based/tlc.log b/modules/tests/support/model_based/tlc.log new file mode 100644 index 0000000000..c714ec84c0 --- /dev/null +++ b/modules/tests/support/model_based/tlc.log @@ -0,0 +1,66 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.15 of Day Month 20?? (rev: c730bc1) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 96 and seed -5647707086248889665 with 12 workers on 12 cores with 7127MB heap and 64MB offheap memory [pid: 25072] (Linux 4.19.0-13-amd64 amd64, Debian 11.0.9.1 x86_64, MSBDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /home/vitor.enes/ibc-rs/modules/tests/support/model_based/IBCTests.tla +Parsing file /home/vitor.enes/ibc-rs/modules/tests/support/model_based/IBC.tla +Parsing file /tmp/Sequences.tla (jar:file:/home/vitor.enes/.tlc-json/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) +Parsing file /home/vitor.enes/ibc-rs/modules/tests/support/model_based/ICS02.tla +Parsing file /home/vitor.enes/ibc-rs/modules/tests/support/model_based/ICS03.tla +Parsing file /home/vitor.enes/ibc-rs/modules/tests/support/model_based/IBCDefinitions.tla +Parsing file /tmp/Integers.tla (jar:file:/home/vitor.enes/.tlc-json/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) +Parsing file /tmp/FiniteSets.tla (jar:file:/home/vitor.enes/.tlc-json/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) +Parsing file /tmp/TLC.tla (jar:file:/home/vitor.enes/.tlc-json/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) +Parsing file /tmp/Naturals.tla (jar:file:/home/vitor.enes/.tlc-json/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) +Semantic processing of module Naturals +Semantic processing of module Integers +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module TLC +Semantic processing of module IBCDefinitions +Semantic processing of module ICS02 +Semantic processing of module ICS03 +Semantic processing of module IBC +Semantic processing of module IBCTests +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2021-03-02 17:45:20) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 1 distinct state generated at 2021-03-02 17:45:21. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(7) at 2021-03-02 17:45:24: 1,290,904 states generated (1,290,904 s/min), 37,827 distinct states found (37,827 ds/min), 25,575 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2193:0 @!@!@ +Model checking completed. No error has been found. + Estimates of the probability that TLC did not check all reachable states + because two distinct states had the same fingerprint: + calculated (optimistic): val = 1.4E-7 + based on the actual fingerprints: val = 1.0E-9 +@!@!@ENDMSG 2193 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(11) at 2021-03-02 17:45:39: 14,627,943 states generated (46,125,529 s/min), 182,639 distinct states found (575,906 ds/min), 0 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2199:0 @!@!@ +14627943 states generated, 182639 distinct states found, 0 states left on queue. +@!@!@ENDMSG 2199 @!@!@ +@!@!@STARTMSG 2194:0 @!@!@ +The depth of the complete state graph search is 11. +@!@!@ENDMSG 2194 @!@!@ +@!@!@STARTMSG 2268:0 @!@!@ +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 1). +@!@!@ENDMSG 2268 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 19032ms at (2021-03-02 17:45:39) +@!@!@ENDMSG 2186 @!@!@