diff --git a/.changelog/unreleased/improvements/1311-mbt-test-client-upgrade.md b/.changelog/unreleased/improvements/1311-mbt-test-client-upgrade.md new file mode 100644 index 0000000000..d93be65047 --- /dev/null +++ b/.changelog/unreleased/improvements/1311-mbt-test-client-upgrade.md @@ -0,0 +1,4 @@ +- Add MBT tests for ICS 07 Client Upgrade ([#1311]) + +[#1311]: https://github.com/informalsystems/ibc-rs/issues/1311 + diff --git a/modules/src/ics26_routing/handler.rs b/modules/src/ics26_routing/handler.rs index 65e9673a68..ef2221f309 100644 --- a/modules/src/ics26_routing/handler.rs +++ b/modules/src/ics26_routing/handler.rs @@ -56,7 +56,6 @@ where let output = match msg { Ics2Msg(msg) => { let handler_output = ics2_msg_dispatcher(ctx, msg).map_err(Error::ics02_client)?; - // Apply the result to the context (host chain store). ctx.store_client_result(handler_output.result) .map_err(Error::ics02_client)?; diff --git a/modules/tests/mbt.rs b/modules/tests/mbt.rs index 4165aa02f5..9f4f30ac67 100644 --- a/modules/tests/mbt.rs +++ b/modules/tests/mbt.rs @@ -18,8 +18,8 @@ fn run_tests() -> Result<(), TestError> { let tla_config_file = "tests/support/model_based/IBCTests.cfg"; let mut opts = modelator::Options::default(); opts.model_checker_options.model_checker = ModelChecker::Tlc; + let mut runner = IbcTestRunner::new(); run_tla_steps(tla_tests_file, tla_config_file, &opts, &mut runner)?; - Ok(()) } diff --git a/modules/tests/runner/mod.rs b/modules/tests/runner/mod.rs index 798abd8459..c1c6153e8e 100644 --- a/modules/tests/runner/mod.rs +++ b/modules/tests/runner/mod.rs @@ -1,6 +1,7 @@ pub mod step; use std::collections::HashMap; +use std::convert::TryFrom; use std::fmt::Debug; use std::time::Duration; @@ -12,6 +13,7 @@ use ibc::ics02_client::error as client_error; use ibc::ics02_client::header::AnyHeader; use ibc::ics02_client::msgs::create_client::MsgCreateAnyClient; use ibc::ics02_client::msgs::update_client::MsgUpdateAnyClient; +use ibc::ics02_client::msgs::upgrade_client::MsgUpgradeAnyClient; use ibc::ics02_client::msgs::ClientMsg; use ibc::ics03_connection::connection::{Counterparty, State as ConnectionState}; use ibc::ics03_connection::error as connection_error; @@ -36,12 +38,14 @@ use ibc::proofs::{ConsensusProof, Proofs}; use ibc::signer::Signer; use ibc::timestamp::ZERO_DURATION; use ibc::Height; +use ibc_proto::ibc::core::commitment::v1::MerkleProof; + use step::{Action, ActionOutcome, Chain, Step}; #[derive(Debug, Clone)] pub struct IbcTestRunner { // mapping from chain identifier to its context - contexts: HashMap, + contexts: HashMap, } impl IbcTestRunner { @@ -52,15 +56,16 @@ impl IbcTestRunner { } /// Create a `MockContext` for a given `chain_id`. - pub fn init_chain_context(&mut self, chain_id: String, initial_height: u64) { - let chain_id = Self::chain_id(chain_id); + /// Panic if a context for `chain_id` already exists. + pub fn init_chain_context(&mut self, chain_id: String, initial_height: Height) { + let chain_id_struct = Self::chain_id(chain_id.clone(), initial_height); // never GC blocks let max_history_size = usize::MAX; let ctx = MockContext::new( - chain_id.clone(), + chain_id_struct, HostType::Mock, max_history_size, - Height::new(Self::revision(), initial_height), + initial_height, ); self.contexts.insert(chain_id, ctx); } @@ -69,7 +74,7 @@ impl IbcTestRunner { /// Panic if the context for `chain_id` is not found. pub fn chain_context(&self, chain_id: String) -> &MockContext { self.contexts - .get(&Self::chain_id(chain_id)) + .get(&chain_id) .expect("chain context should have been initialized") } @@ -77,7 +82,7 @@ impl IbcTestRunner { /// Panic if the context for `chain_id` is not found. pub fn chain_context_mut(&mut self, chain_id: String) -> &mut MockContext { self.contexts - .get_mut(&Self::chain_id(chain_id)) + .get_mut(&chain_id) .expect("chain context should have been initialized") } @@ -116,12 +121,8 @@ impl IbcTestRunner { } } - pub fn chain_id(chain_id: String) -> ChainId { - ChainId::new(chain_id, Self::revision()) - } - - pub fn revision() -> u64 { - 0 + pub fn chain_id(chain_id: String, height: Height) -> ChainId { + ChainId::new(chain_id, height.revision_number) } pub fn version() -> Version { @@ -141,23 +142,23 @@ impl IbcTestRunner { ConnectionId::new(connection_id) } - pub fn height(height: u64) -> Height { - Height::new(Self::revision(), height) + pub fn height(height: Height) -> Height { + Height::new(height.revision_number, height.revision_height) } - fn mock_header(height: u64) -> MockHeader { + fn mock_header(height: Height) -> MockHeader { MockHeader::new(Self::height(height)) } - pub fn header(height: u64) -> AnyHeader { + pub fn header(height: Height) -> AnyHeader { AnyHeader::Mock(Self::mock_header(height)) } - pub fn client_state(height: u64) -> AnyClientState { + pub fn client_state(height: Height) -> AnyClientState { AnyClientState::Mock(MockClientState(Self::mock_header(height))) } - pub fn consensus_state(height: u64) -> AnyConsensusState { + pub fn consensus_state(height: Height) -> AnyConsensusState { AnyConsensusState::Mock(MockConsensusState::new(Self::mock_header(height))) } @@ -184,14 +185,14 @@ impl IbcTestRunner { vec![0].into() } - pub fn consensus_proof(height: u64) -> ConsensusProof { + pub fn consensus_proof(height: Height) -> 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 { + pub fn proofs(height: Height) -> Proofs { let object_proof = Self::commitment_proof_bytes(); let client_proof = None; let consensus_proof = Some(Self::consensus_proof(height)); @@ -207,17 +208,12 @@ impl IbcTestRunner { .expect("it should be possible to create the proofs") } - /// Check that chain heights match the ones in the model. - pub fn validate_chains(&self) -> bool { - self.contexts.values().all(|ctx| ctx.validate().is_ok()) - } - /// 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); // check that heights match - let heights_match = ctx.query_latest_height() == Self::height(chain.height); + let heights_match = ctx.query_latest_height() == chain.height; // check that clients match let clients_match = chain.clients.into_iter().all(|(client_id, client)| { @@ -230,7 +226,7 @@ impl IbcTestRunner { // heights in the model), then the highest one should // match the height in the client state client_state.is_some() - && client_state.unwrap().latest_height() == Self::height(*max_height) + && client_state.unwrap().latest_height() == *max_height } None => { // if the model doesn't have any consensus states @@ -244,7 +240,7 @@ impl IbcTestRunner { // only existing consensus states are those in that also // exist in the model) let consensus_states_match = client.heights.into_iter().all(|height| { - ctx.consensus_state(&Self::client_id(client_id), Self::height(height)) + ctx.consensus_state(&Self::client_id(client_id), height) .is_some() }); @@ -335,6 +331,31 @@ impl IbcTestRunner { })); ctx.deliver(msg) } + Action::Ics07UpgradeClient { + chain_id, + client_id, + header, + } => { + // get chain's context + let ctx = self.chain_context_mut(chain_id); + + let buf: Vec = Vec::new(); + let buf2: Vec = Vec::new(); + + let c_bytes = CommitmentProofBytes::from(buf); + let cs_bytes = CommitmentProofBytes::from(buf2); + + // create ICS26 message and deliver it + let msg = Ics26Envelope::Ics2Msg(ClientMsg::UpgradeClient(MsgUpgradeAnyClient { + client_id: Self::client_id(client_id), + client_state: MockClientState(MockHeader::new(header)).into(), + consensus_state: MockConsensusState::new(MockHeader::new(header)).into(), + proof_upgrade_client: MerkleProof::try_from(c_bytes).unwrap(), + proof_upgrade_consensus_state: MerkleProof::try_from(cs_bytes).unwrap(), + signer: Self::signer(), + })); + ctx.deliver(msg) + } Action::Ics03ConnectionOpenInit { chain_id, client_id, @@ -460,10 +481,23 @@ impl modelator::step_runner::StepRunner for IbcTestRunner { Self::extract_ics02_error_kind(result), client_error::ErrorDetail::ClientNotFound(_) ), - ActionOutcome::Ics02HeaderVerificationFailure => matches!( + ActionOutcome::Ics02HeaderVerificationFailure => { + matches!( + Self::extract_ics02_error_kind(result), + client_error::ErrorDetail::HeaderVerificationFailure(_) + ) + } + ActionOutcome::Ics07UpgradeOk => result.is_ok(), + ActionOutcome::Ics07ClientNotFound => matches!( Self::extract_ics02_error_kind(result), - client_error::ErrorDetail::HeaderVerificationFailure(_) + client_error::ErrorDetail::ClientNotFound(_) ), + ActionOutcome::Ics07HeaderVerificationFailure => { + matches!( + Self::extract_ics02_error_kind(result), + client_error::ErrorDetail::LowUpgradeHeight(_) + ) + } ActionOutcome::Ics03ConnectionOpenInitOk => result.is_ok(), ActionOutcome::Ics03MissingClient => matches!( Self::extract_ics03_error_kind(result), @@ -497,11 +531,20 @@ impl modelator::step_runner::StepRunner for IbcTestRunner { ), ActionOutcome::Ics03ConnectionOpenConfirmOk => result.is_ok(), }; - // also check the state of chains - if outcome_matches && self.validate_chains() && self.check_chain_states(step.chains) { - Ok(()) - } else { - Err("next_step did not conclude successfully".into()) + + // Validate chains + for ctx in self.contexts.values() { + ctx.validate()? + } + + if !outcome_matches { + return Err("Action outcome did not match expected".into()); } + + if !self.check_chain_states(step.chains) { + return Err("Chain states do not match".into()); + } + + Ok(()) } } diff --git a/modules/tests/runner/step.rs b/modules/tests/runner/step.rs index 01d433e9bd..408a7d32b4 100644 --- a/modules/tests/runner/step.rs +++ b/modules/tests/runner/step.rs @@ -1,8 +1,11 @@ -use ibc::ics03_connection::connection::State as ConnectionState; -use serde::{Deserialize, Deserializer}; use std::collections::HashMap; use std::fmt::Debug; +use serde::{Deserialize, Deserializer}; + +use ibc::ics03_connection::connection::State as ConnectionState; +use ibc::Height; + #[derive(Debug, Clone, Deserialize)] pub struct Step { pub action: Action, @@ -22,10 +25,10 @@ pub enum Action { chain_id: String, #[serde(alias = "clientState")] - client_state: u64, + client_state: Height, #[serde(alias = "consensusState")] - consensus_state: u64, + consensus_state: Height, }, Ics02UpdateClient { #[serde(alias = "chainId")] @@ -34,7 +37,16 @@ pub enum Action { #[serde(alias = "clientId")] client_id: u64, - header: u64, + header: Height, + }, + Ics07UpgradeClient { + #[serde(alias = "chainId")] + chain_id: String, + + #[serde(alias = "clientId")] + client_id: u64, + + header: Height, }, Ics03ConnectionOpenInit { #[serde(alias = "chainId")] @@ -61,7 +73,7 @@ pub enum Action { client_id: u64, #[serde(alias = "clientState")] - client_state: u64, + client_state: Height, #[serde(alias = "counterpartyChainId")] counterparty_chain_id: String, @@ -80,7 +92,7 @@ pub enum Action { connection_id: u64, #[serde(alias = "clientState")] - client_state: u64, + client_state: Height, #[serde(alias = "counterpartyChainId")] counterparty_chain_id: String, @@ -96,7 +108,7 @@ pub enum Action { connection_id: u64, #[serde(alias = "clientState")] - client_state: u64, + client_state: Height, #[serde(alias = "counterpartyChainId")] counterparty_chain_id: String, @@ -113,6 +125,11 @@ pub enum ActionOutcome { Ics02UpdateOk, Ics02ClientNotFound, Ics02HeaderVerificationFailure, + + Ics07UpgradeOk, + Ics07ClientNotFound, + Ics07HeaderVerificationFailure, + Ics03ConnectionOpenInitOk, Ics03MissingClient, Ics03ConnectionOpenTryOk, @@ -128,7 +145,7 @@ pub enum ActionOutcome { #[derive(Debug, Clone, PartialEq, Deserialize)] pub struct Chain { - pub height: u64, + pub height: Height, pub clients: HashMap, @@ -137,7 +154,7 @@ pub struct Chain { #[derive(Debug, Clone, PartialEq, Deserialize)] pub struct Client { - pub heights: Vec, + pub heights: Vec, } #[derive(Debug, Clone, PartialEq, Deserialize)] diff --git a/modules/tests/support/model_based/IBC.cfg b/modules/tests/support/model_based/IBC.cfg index d2997417ae..14a26f8201 100644 --- a/modules/tests/support/model_based/IBC.cfg +++ b/modules/tests/support/model_based/IBC.cfg @@ -1,6 +1,7 @@ CONSTANTS ChainIds = {"chainA", "chainB"} - MaxChainHeight = 4 + MaxRevisionHeight = 4 + MaxRevisionNumber = 2 MaxClientsPerChain = 1 MaxConnectionsPerChain = 1 diff --git a/modules/tests/support/model_based/IBC.tla b/modules/tests/support/model_based/IBC.tla index ef18736967..c7194cad39 100644 --- a/modules/tests/support/model_based/IBC.tla +++ b/modules/tests/support/model_based/IBC.tla @@ -5,8 +5,11 @@ EXTENDS ICS02, ICS03 \* ids of existing chains CONSTANT ChainIds \* max height which chains can reach -CONSTANT MaxChainHeight -ASSUME MaxChainHeight >= 0 +CONSTANT MaxRevisionHeight +ASSUME MaxRevisionHeight >= 0 +\* max revision which chains can reach +CONSTANT MaxRevisionNumber +ASSUME MaxRevisionNumber >= 0 \* max number of client to be created per chain CONSTANT MaxClientsPerChain ASSUME MaxClientsPerChain >= 0 @@ -22,12 +25,13 @@ VARIABLE action VARIABLE actionOutcome vars == <> -\* set of possible chain heights -Heights == 1..MaxChainHeight +\* set of possible height tuples +Heights == [ revision_number: (1..MaxRevisionNumber), revision_height: (1..MaxRevisionHeight) ] +MaxHeight == [ revision_number |-> MaxRevisionNumber, revision_height |-> MaxRevisionHeight ] \* set of possible client identifiers ClientIds == 0..(MaxClientsPerChain - 1) \* set of possible connection identifiers -ConnectionIds == 0..(MaxConnectionsPerChain- 1) +ConnectionIds == 0..(MaxConnectionsPerChain - 1) \* set of possible connection states ConnectionStates == { "Uninitialized", @@ -56,9 +60,17 @@ UpdateClientActions == [ \* `header` contains simply a height header: Heights ] <: {ActionType} +UpgradeClientActions == [ + type: {"Ics07UpgradeClient"}, + chainId: ChainIds, + clientId: ClientIds, + \* `header` contains simply a height + header: Heights +] <: {ActionType} ClientActions == CreateClientActions \union - UpdateClientActions + UpdateClientActions \union + UpgradeClientActions ConnectionOpenInitActions == [ type: {"Ics03ConnectionOpenInit"}, @@ -105,7 +117,7 @@ ConnectionActions == Actions == NoneActions \union - ClientActions \union + ClientActions \union ConnectionActions \* set of possible action outcomes @@ -118,6 +130,10 @@ ActionOutcomes == { "Ics02UpdateOk", "Ics02ClientNotFound", "Ics02HeaderVerificationFailure", + \* ICS07_UpgradeClient outcomes: + "Ics07UpgradeOk", + "Ics07ClientNotFound", + "Ics07HeaderVerificationFailure", \* ICS03_ConnectionOpenInit outcomes: "Ics03ConnectionOpenInitOk", "Ics03MissingClient", @@ -180,13 +196,22 @@ Chains == [ (***************************** Specification *********************************) -\* update chain height if outcome was ok -UpdateChainHeight(height, result, okOutcome) == +\* update block height if outcome was ok +UpdateRevisionHeight(height, result, okOutcome) == IF result.outcome = okOutcome THEN - height + 1 + \* <> + [ revision_number |-> height.revision_number, revision_height |-> height.revision_height + 1 ] ELSE height +\* update revision height if outcome was ok +UpdateRevisionNumber(height, result, okOutcome) == + IF result.outcome = okOutcome THEN + [ revision_number |-> height.revision_number + 1, revision_height |-> height.revision_height ] + ELSE + height + + \* update connection proofs if outcome was ok UpdateConnectionProofs(connectionProofs, result, okOutcome) == IF result.outcome = okOutcome THEN @@ -199,7 +224,7 @@ CreateClient(chainId, height) == LET result == ICS02_CreateClient(chain, chainId, height) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result, "Ics02CreateOk"), + !.height = UpdateRevisionHeight(@, result, "Ics02CreateOk"), !.clients = result.clients, !.clientIdCounter = result.clientIdCounter ] IN @@ -213,7 +238,20 @@ UpdateClient(chainId, clientId, height) == LET result == ICS02_UpdateClient(chain, chainId, clientId, height) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result, "Ics02UpdateOk"), + !.height = UpdateRevisionHeight(@, result, "Ics02UpdateOk"), + !.clients = result.clients + ] IN + \* update `chains`, set the `action` and its `actionOutcome` + /\ chains' = [chains EXCEPT ![chainId] = updatedChain] + /\ action' = result.action + /\ actionOutcome' = result.outcome + +UpgradeClient(chainId, clientId, height) == + LET chain == chains[chainId] IN + LET result == ICS07_UpgradeClient(chain, chainId, clientId, height) IN + \* update the chain + LET updatedChain == [chain EXCEPT + !.height = UpdateRevisionHeight(@, result, "Ics07UpgradeOk"), !.clients = result.clients ] IN \* update `chains`, set the `action` and its `actionOutcome` @@ -237,7 +275,7 @@ ConnectionOpenInit( ) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result, "Ics03ConnectionOpenInitOk"), + !.height = UpdateRevisionHeight(@, result, "Ics03ConnectionOpenInitOk"), !.connections = result.connections, !.connectionIdCounter = result.connectionIdCounter ] IN @@ -275,7 +313,7 @@ ConnectionOpenTry( ) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result, "Ics03ConnectionOpenTryOk"), + !.height = UpdateRevisionHeight(@, result, "Ics03ConnectionOpenTryOk"), !.connections = result.connections, !.connectionIdCounter = result.connectionIdCounter ] IN @@ -309,7 +347,7 @@ ConnectionOpenAck( ) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result, "Ics03ConnectionOpenAckOk"), + !.height = UpdateRevisionHeight(@, result, "Ics03ConnectionOpenAckOk"), !.connections = result.connections ] IN \* update the counterparty chain with a proof @@ -342,7 +380,7 @@ ConnectionOpenConfirm( ) IN \* update the chain LET updatedChain == [chain EXCEPT - !.height = UpdateChainHeight(@, result, "Ics03ConnectionOpenConfirmOk"), + !.height = UpdateRevisionHeight(@, result, "Ics03ConnectionOpenConfirmOk"), !.connections = result.connections ] IN \* no need to update the counterparty chain with a proof (as in the other @@ -365,10 +403,19 @@ CreateClientAction(chainId) == UpdateClientAction(chainId) == \* select a client to be updated (which may not exist) - \E clientId \in ClientIds: + \E clientId \in ClientIds: \* select a height for the client to be updated - \E height \in Heights: + \* We only use heights at the same revision number to save on state space + \E height \in {height \in Heights: height.revision_number = chains[chainId].height.revision_number}: UpdateClient(chainId, clientId, height) + +UpgradeClientAction(chainId) == + \* select a client to be upgraded (which may not exist) + \E clientId \in ClientIds: + \* select a height for the client to be upgraded + \* We only try to upgrade to heights with a height of one to save on state space + \E height \in {height \in Heights: height.revision_height = 1}: + UpgradeClient(chainId, clientId, height) ConnectionOpenInitAction(chainId) == \* select a client id @@ -397,7 +444,8 @@ ConnectionOpenTryAction(chainId) == \* 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: + \* Only use heights whose revision number is 1 (this covers updates) OR whose revision height <= 2 (this allows for an upgrade and an update, but no updates after that) + \E height \in {height \in Heights: height.revision_number <= 2 /\ height.revision_height <= 2}: \* select a counterparty chain id \E counterpartyChainId \in ChainIds: \* select a counterparty client id @@ -427,7 +475,8 @@ ConnectionOpenAckAction(chainId) == \* select a connection id \E connectionId \in ConnectionIds: \* select a claimed height for the client - \E height \in Heights: + \* Only use heights whose revision number is 1 (this covers updates) OR whose revision height <= 2 (this allows for an upgrade but no updates after that) + \E height \in {height \in Heights: height.revision_number <= 2 /\ height.revision_height <= 2}: \* select a counterparty chain id \E counterpartyChainId \in ChainIds: \* select a counterparty connection id @@ -447,7 +496,8 @@ ConnectionOpenConfirmAction(chainId) == \* select a connection id \E connectionId \in ConnectionIds: \* select a claimed height for the client - \E height \in Heights: + \* Only use heights whose revision number is 1 (this covers updates) OR whose revision height <= 2 (this allows for an upgrade but no updates after that) + \E height \in {height \in Heights: height.revision_number <= 2 /\ height.revision_height <= 2}: \* select a counterparty chain id \E counterpartyChainId \in ChainIds: \* select a counterparty connection id @@ -479,7 +529,7 @@ Init == ] IN \* create an empty chain LET emptyChain == [ - height |-> 1, + height |-> [ revision_number |-> 1, revision_height |-> 1 ], clients |-> [clientId \in ClientIds |-> clientNone], clientIdCounter |-> 0, connections |-> [connectionId \in ConnectionIds |-> connectionNone], @@ -495,9 +545,11 @@ Next == \E chainId \in ChainIds: \* perform action on chain if the model constant `MaxChainHeight` allows \* it - IF chains[chainId].height < MaxChainHeight THEN + \* The line below checks if chains[chainId].height < MaxHeight + IF chains[chainId].height.revision_number < MaxHeight.revision_number /\ chains[chainId].height.revision_height < MaxHeight.revision_height THEN \/ CreateClientAction(chainId) \/ UpdateClientAction(chainId) + \/ UpgradeClientAction(chainId) \/ ConnectionOpenInitAction(chainId) \/ ConnectionOpenTryAction(chainId) \/ ConnectionOpenAckAction(chainId) diff --git a/modules/tests/support/model_based/IBCDefinitions.tla b/modules/tests/support/model_based/IBCDefinitions.tla index 6c1712bd6b..9fffba58df 100644 --- a/modules/tests/support/model_based/IBCDefinitions.tla +++ b/modules/tests/support/model_based/IBCDefinitions.tla @@ -24,7 +24,44 @@ AsSetInt(S) == S <: {Int} (******************* END OF TYPE ANNOTATIONS FOR APALACHE ********************) (******************************** Utils **************************************) +\* This is an implementation of the height comparison for Tendermint heights, +\* which include a revision (client version) and a block height. +\* - If height x's revision is higher than y's, x is higher. +\* - If x's revision is lower than y's, x is lower +\* - If x and y's revision's are equal, then we look at the block number +\* - - If x's block number is higher, x is higher. +\* - - If x's block number is lower, x is lower. +\* - - If x and y have the same revision and block number, the heights are equal. +HeightLT(a, b) == + \/ a.revision_number < b.revision_number + \/ (a.revision_number = b.revision_number /\ a.revision_height < b.revision_height) + +HeightLTE(a, b) == + \/ a.revision_number < b.revision_number + \/ (a.revision_number = b.revision_number /\ a.revision_height < b.revision_height) + \/ a = b + +HeightGT(a, b) == + \/ a.revision_number > b.revision_number + \/ (a.revision_number = b.revision_number /\ a.revision_height > b.revision_height) + +HeightGTE(a, b) == + \/ a.revision_number > b.revision_number + \/ (a.revision_number = b.revision_number /\ a.revision_height > b.revision_height) + \/ a = b + +\* Checks if the block is higher but the revision is the same +HigherRevisionHeight(a, b) == + /\ a.revision_number = b.revision_number + /\ a.revision_height > b.revision_height + +\* Checks if the revision is higher +HigherRevisionNumber(a, b) == + /\ a.revision_number > b.revision_number + Max(S) == CHOOSE x \in S: \A y \in S: y <= x +FindMaxHeight(S) == CHOOSE x \in S: \A y \in S: HeightLTE(y, x) + (*****************************************************************************) \* if a chain identifier is not set then it is "-1" diff --git a/modules/tests/support/model_based/IBCTests.cfg b/modules/tests/support/model_based/IBCTests.cfg index cb0afe47f7..17f90db1bd 100644 --- a/modules/tests/support/model_based/IBCTests.cfg +++ b/modules/tests/support/model_based/IBCTests.cfg @@ -1,9 +1,9 @@ CONSTANTS ChainIds = {"chainA", "chainB"} - MaxChainHeight = 4 + MaxRevisionHeight = 4 + MaxRevisionNumber = 2 MaxClientsPerChain = 1 MaxConnectionsPerChain = 1 INIT Init -NEXT Next - +NEXT Next \ 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 ba6f3a9d47..d9e86b23a5 100644 --- a/modules/tests/support/model_based/IBCTests.tla +++ b/modules/tests/support/model_based/IBCTests.tla @@ -16,6 +16,17 @@ ICS02ClientNotFoundTest == ICS02HeaderVerificationFailureTest == /\ actionOutcome = "Ics02HeaderVerificationFailure" +\* ICS07UpgradeClient tests +ICS07UpgradeOkTest == + /\ actionOutcome = "Ics07UpgradeOk" + +ICS07ClientNotFoundTest == + /\ actionOutcome = "Ics07ClientNotFound" + +ICS07HeaderVerificationFailureTest == + /\ actionOutcome = "Ics07HeaderVerificationFailure" + + \* ICS03ConnectionOpenInit tests ICS03ConnectionOpenInitOKTest == /\ actionOutcome = "Ics03ConnectionOpenInitOk" @@ -54,5 +65,4 @@ ICS03UninitializedConnectionTest == \* ICS03ConnectionOpenConfirm tests ICS03ConnectionOpenConfirmOKTest == /\ actionOutcome = "Ics03ConnectionOpenConfirmOk" - =============================================================================== diff --git a/modules/tests/support/model_based/ICS02.tla b/modules/tests/support/model_based/ICS02.tla index b0831fed11..5c3ff16ce9 100644 --- a/modules/tests/support/model_based/ICS02.tla +++ b/modules/tests/support/model_based/ICS02.tla @@ -68,10 +68,10 @@ ICS02_UpdateClient(chain, chainId, clientId, height) == ELSE \* if the client exists, check its height 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 + LET highestHeight == FindMaxHeight(client.heights) IN + IF ~HigherRevisionHeight(height, highestHeight) THEN + \* if the client's new height is not at the same revision number and a higher + \* block height than the highest client height, then set an error outcome [ clients |-> chain.clients, action |-> action_, @@ -94,4 +94,48 @@ ICS02_UpdateClient(chain, chainId, clientId, height) == outcome |-> "Ics02UpdateOk" ] +ICS07_UpgradeClient(chain, chainId, clientId, height) == + LET action_ == AsAction([ + type |-> "Ics07UpgradeClient", + chainId |-> chainId, + clientId |-> clientId, + header |-> height + ]) IN + \* check if the client exists + IF ~ICS02_ClientExists(chain.clients, clientId) THEN + \* if the client does not exist, then set an error outcome + [ + clients |-> chain.clients, + action |-> action_, + outcome |-> "Ics07ClientNotFound" + ] + ELSE + \* if the client exists, check its height + LET client == ICS02_GetClient(chain.clients, clientId) IN + LET highestHeight == FindMaxHeight(client.heights) IN + IF ~HigherRevisionNumber(height, highestHeight) THEN + \* if the client's new height is not at a higher revision than the highest client + \* height, then set an error outcome + [ + clients |-> chain.clients, + action |-> action_, + outcome |-> "Ics07HeaderVerificationFailure" + ] + ELSE + \* if the client's new height is higher than the highest client + \* height, then update the client + LET updatedClient == [client EXCEPT + !.heights = client.heights \union {height} + ] IN + \* return result with updated state + [ + clients |-> ICS02_SetClient( + chain.clients, + clientId, + updatedClient + ), + action |-> action_, + outcome |-> "Ics07UpgradeOk" + ] + =============================================================================== diff --git a/modules/tests/support/model_based/ICS03.tla b/modules/tests/support/model_based/ICS03.tla index 35d2000faf..c7533f7b0d 100644 --- a/modules/tests/support/model_based/ICS03.tla +++ b/modules/tests/support/model_based/ICS03.tla @@ -94,7 +94,7 @@ ICS03_ConnectionOpenTry( counterpartyConnectionId |-> counterpartyConnectionId ]) IN \* check if client's claimed height is higher than the chain's height - IF height > chain.height THEN + IF HeightGT(height, chain.height) THEN \* if client's height is too advanced, then set an error outcome [ connections |-> chain.connections, @@ -251,7 +251,7 @@ ICS03_ConnectionOpenAck( 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 HeightGT(height, chain.height) THEN \* if client's height is too advanced, then set an error outcome [ connections |-> connections,