diff --git a/.changelog/unreleased/breaking-changes/156-connection-crossing-hellos b/.changelog/unreleased/breaking-changes/156-connection-crossing-hellos new file mode 100644 index 000000000..445cffc90 --- /dev/null +++ b/.changelog/unreleased/breaking-changes/156-connection-crossing-hellos @@ -0,0 +1,3 @@ +- Remove crossing hellos logic from connection handshake. Breaking changes in + connection message types. + ([#156](https://github.com/cosmos/ibc-rs/issues/156)). diff --git a/.changelog/unreleased/bug-fixes/168-consensus-height.md b/.changelog/unreleased/bug-fixes/168-consensus-height.md new file mode 100644 index 000000000..8c87ef3bd --- /dev/null +++ b/.changelog/unreleased/bug-fixes/168-consensus-height.md @@ -0,0 +1,2 @@ +- Connection consensus state proof verification now properly uses `consensus_height` + ([#168](https://github.com/cosmos/ibc-rs/issues/168)). diff --git a/.changelog/unreleased/improvements/165-refactor-connection-proofs b/.changelog/unreleased/improvements/165-refactor-connection-proofs new file mode 100644 index 000000000..15410b2dc --- /dev/null +++ b/.changelog/unreleased/improvements/165-refactor-connection-proofs @@ -0,0 +1,2 @@ +- Refactor connection proofs + ([#165](https://github.com/cosmos/ibc-rs/issues/165)). diff --git a/crates/ibc/Cargo.toml b/crates/ibc/Cargo.toml index a43834823..cb72d53ab 100644 --- a/crates/ibc/Cargo.toml +++ b/crates/ibc/Cargo.toml @@ -72,8 +72,3 @@ modelator = "0.4.2" sha2 = { version = "0.10.6" } tendermint-rpc = { version = "=0.25.0", features = ["http-client", "websocket-client"] } tendermint-testgen = { version = "=0.25.0" } # Needed for generating (synthetic) light blocks. - -[[test]] -name = "mbt" -path = "tests/mbt.rs" -required-features = ["mocks"] diff --git a/crates/ibc/src/core/ics02_client/client_state.rs b/crates/ibc/src/core/ics02_client/client_state.rs index 1128c2221..4cf5f9725 100644 --- a/crates/ibc/src/core/ics02_client/client_state.rs +++ b/crates/ibc/src/core/ics02_client/client_state.rs @@ -101,11 +101,11 @@ pub trait ClientState: #[allow(clippy::too_many_arguments)] fn verify_client_consensus_state( &self, - height: Height, - prefix: &CommitmentPrefix, + proof_height: Height, + counterparty_prefix: &CommitmentPrefix, proof: &CommitmentProofBytes, root: &CommitmentRoot, - client_id: &ClientId, + counterparty_client_id: &ClientId, consensus_height: Height, expected_consensus_state: &dyn ConsensusState, ) -> Result<(), Error>; @@ -114,11 +114,11 @@ pub trait ClientState: #[allow(clippy::too_many_arguments)] fn verify_connection_state( &self, - height: Height, - prefix: &CommitmentPrefix, + proof_height: Height, + counterparty_prefix: &CommitmentPrefix, proof: &CommitmentProofBytes, root: &CommitmentRoot, - connection_id: &ConnectionId, + counterparty_connection_id: &ConnectionId, expected_connection_end: &ConnectionEnd, ) -> Result<(), Error>; @@ -139,8 +139,8 @@ pub trait ClientState: #[allow(clippy::too_many_arguments)] fn verify_client_full_state( &self, - height: Height, - prefix: &CommitmentPrefix, + proof_height: Height, + counterparty_prefix: &CommitmentPrefix, proof: &CommitmentProofBytes, root: &CommitmentRoot, client_id: &ClientId, diff --git a/crates/ibc/src/core/ics03_connection/context.rs b/crates/ibc/src/core/ics03_connection/context.rs index d4a49a095..06c4569c2 100644 --- a/crates/ibc/src/core/ics03_connection/context.rs +++ b/crates/ibc/src/core/ics03_connection/context.rs @@ -6,7 +6,7 @@ use crate::core::ics02_client::client_state::ClientState; use crate::core::ics02_client::consensus_state::ConsensusState; use crate::core::ics03_connection::connection::ConnectionEnd; use crate::core::ics03_connection::error::Error; -use crate::core::ics03_connection::handler::{ConnectionIdState, ConnectionResult}; +use crate::core::ics03_connection::handler::ConnectionResult; use crate::core::ics03_connection::version::{get_compatible_versions, pick_version, Version}; use crate::core::ics23_commitment::commitment::CommitmentPrefix; use crate::core::ics24_host::identifier::{ClientId, ConnectionId}; @@ -14,6 +14,8 @@ use crate::prelude::*; use crate::Height; use ibc_proto::google::protobuf::Any; +use super::handler::ConnectionIdState; + /// A context supplying all the necessary read-only dependencies for processing any `ConnectionMsg`. pub trait ConnectionReader { /// Returns the ConnectionEnd for the given identifier `conn_id`. @@ -28,6 +30,7 @@ pub trait ConnectionReader { /// Returns the current height of the local chain. fn host_current_height(&self) -> Height; + #[deprecated(since = "0.20.0")] /// Returns the oldest height available on the local chain. fn host_oldest_height(&self) -> Height; diff --git a/crates/ibc/src/core/ics03_connection/handler.rs b/crates/ibc/src/core/ics03_connection/handler.rs index b096c32e1..5c9d67993 100644 --- a/crates/ibc/src/core/ics03_connection/handler.rs +++ b/crates/ibc/src/core/ics03_connection/handler.rs @@ -1,4 +1,5 @@ -//! This module implements the processing logic for ICS3 (connection open handshake) messages. +//! This module implements the processing logic for ICS3 (connection open +//! handshake) messages. use crate::core::ics03_connection::connection::ConnectionEnd; use crate::core::ics03_connection::context::ConnectionReader; @@ -12,8 +13,6 @@ pub mod conn_open_confirm; pub mod conn_open_init; pub mod conn_open_try; -pub mod verify; - /// Defines the possible states of a connection identifier in a `ConnectionResult`. #[derive(Clone, Debug)] pub enum ConnectionIdState { diff --git a/crates/ibc/src/core/ics03_connection/handler/conn_open_ack.rs b/crates/ibc/src/core/ics03_connection/handler/conn_open_ack.rs index 40d2f2660..ae6e39335 100644 --- a/crates/ibc/src/core/ics03_connection/handler/conn_open_ack.rs +++ b/crates/ibc/src/core/ics03_connection/handler/conn_open_ack.rs @@ -4,92 +4,135 @@ use crate::core::ics03_connection::connection::{ConnectionEnd, Counterparty, Sta use crate::core::ics03_connection::context::ConnectionReader; use crate::core::ics03_connection::error::Error; use crate::core::ics03_connection::events::Attributes; -use crate::core::ics03_connection::handler::verify::{ - check_client_consensus_height, verify_proofs, -}; -use crate::core::ics03_connection::handler::{ConnectionIdState, ConnectionResult}; +use crate::core::ics03_connection::handler::ConnectionResult; use crate::core::ics03_connection::msgs::conn_open_ack::MsgConnectionOpenAck; use crate::events::IbcEvent; use crate::handler::{HandlerOutput, HandlerResult}; use crate::prelude::*; +use super::ConnectionIdState; + +/// Per our convention, this message is processed on chain A. pub(crate) fn process( - ctx: &dyn ConnectionReader, + ctx_a: &dyn ConnectionReader, msg: MsgConnectionOpenAck, ) -> HandlerResult { let mut output = HandlerOutput::builder(); - // If a consensus proof is present, check that the consensus height (for - // client proof) in the message is not too advanced nor too old. - if let Some(consensus_height) = msg.consensus_height() { - check_client_consensus_height(ctx, consensus_height)?; + if msg.consensus_height_of_a_on_b > ctx_a.host_current_height() { + return Err(Error::invalid_consensus_height( + msg.consensus_height_of_a_on_b, + ctx_a.host_current_height(), + )); } - // Validate the connection end. - let mut conn_end = ctx.connection_end(&msg.connection_id)?; - // A connection end must be Init or TryOpen; otherwise we return an error. - let state_is_consistent = conn_end.state_matches(&State::Init) - && conn_end.versions().contains(&msg.version) - || conn_end.state_matches(&State::TryOpen) - && conn_end.versions().get(0).eq(&Some(&msg.version)); - - if !state_is_consistent { - // Old connection end is in incorrect state, propagate the error. - return Err(Error::connection_mismatch(msg.connection_id)); - } + /////////////////////////////////////////////////////////// + // validate_self_client() verification goes here + // See [issue](https://github.com/cosmos/ibc-rs/issues/162) + /////////////////////////////////////////////////////////// - // Set the connection ID of the counterparty - let prev_counterparty = conn_end.counterparty(); - let counterparty = Counterparty::new( - prev_counterparty.client_id().clone(), - Some(msg.counterparty_connection_id.clone()), - prev_counterparty.prefix().clone(), - ); - conn_end.set_state(State::Open); - conn_end.set_version(msg.version.clone()); - conn_end.set_counterparty(counterparty); + let conn_end_on_a = ctx_a.connection_end(&msg.conn_id_on_a)?; + if !(conn_end_on_a.state_matches(&State::Init) + && conn_end_on_a.versions().contains(&msg.version)) + { + return Err(Error::connection_mismatch(msg.conn_id_on_a)); + } // Proof verification. - let expected_conn = { - // The counterparty is the local chain. - let counterparty = Counterparty::new( - conn_end.client_id().clone(), // The local client identifier. - Some(msg.connection_id.clone()), // This chain's connection id as known on counterparty. - ctx.commitment_prefix(), // Local commitment prefix. - ); + { + let client_state_of_b_on_a = ctx_a.client_state(conn_end_on_a.client_id())?; + let consensus_state_of_b_on_a = + ctx_a.client_consensus_state(conn_end_on_a.client_id(), msg.proofs_height_on_b)?; - ConnectionEnd::new( - State::TryOpen, - conn_end.counterparty().client_id().clone(), - counterparty, - vec![msg.version.clone()], - conn_end.delay_period(), - ) - }; + let prefix_on_a = ctx_a.commitment_prefix(); + let prefix_on_b = conn_end_on_a.counterparty().prefix(); + let client_id_on_a = conn_end_on_a.client_id(); + let client_id_on_b = conn_end_on_a.counterparty().client_id(); + + { + let conn_id_on_b = conn_end_on_a + .counterparty() + .connection_id() + .ok_or_else(Error::invalid_counterparty)?; + let expected_conn_end_on_b = ConnectionEnd::new( + State::TryOpen, + client_id_on_b.clone(), + Counterparty::new( + client_id_on_a.clone(), + Some(msg.conn_id_on_a.clone()), + prefix_on_a, + ), + vec![msg.version.clone()], + conn_end_on_a.delay_period(), + ); + + client_state_of_b_on_a + .verify_connection_state( + msg.proofs_height_on_b, + prefix_on_b, + &msg.proof_conn_end_on_b, + consensus_state_of_b_on_a.root(), + conn_id_on_b, + &expected_conn_end_on_b, + ) + .map_err(Error::verify_connection_state)?; + } - // 2. Pass the details to the verification function. - verify_proofs( - ctx, - msg.client_state, - msg.proofs.height(), - &conn_end, - &expected_conn, - &msg.proofs, - )?; - - output.log("success: connection verification passed"); - - let result = ConnectionResult { - connection_id: msg.connection_id, - connection_id_state: ConnectionIdState::Reused, - connection_end: conn_end, + client_state_of_b_on_a + .verify_client_full_state( + msg.proofs_height_on_b, + prefix_on_b, + &msg.proof_client_state_of_a_on_b, + consensus_state_of_b_on_a.root(), + client_id_on_b, + msg.client_state_of_a_on_b, + ) + .map_err(|e| { + Error::client_state_verification_failure(conn_end_on_a.client_id().clone(), e) + })?; + + let expected_consensus_state_of_a_on_b = + ctx_a.host_consensus_state(msg.consensus_height_of_a_on_b)?; + client_state_of_b_on_a + .verify_client_consensus_state( + msg.proofs_height_on_b, + prefix_on_b, + &msg.proof_consensus_state_of_a_on_b, + consensus_state_of_b_on_a.root(), + conn_end_on_a.counterparty().client_id(), + msg.consensus_height_of_a_on_b, + expected_consensus_state_of_a_on_b.as_ref(), + ) + .map_err(|e| Error::consensus_state_verification_failure(msg.proofs_height_on_b, e))?; + } + + // Success + let result = { + let new_conn_end_on_a = { + let mut counterparty = conn_end_on_a.counterparty().clone(); + counterparty.connection_id = Some(msg.conn_id_on_b.clone()); + + let mut new_conn_end_on_a = conn_end_on_a; + new_conn_end_on_a.set_state(State::Open); + new_conn_end_on_a.set_version(msg.version.clone()); + new_conn_end_on_a.set_counterparty(counterparty); + new_conn_end_on_a + }; + + ConnectionResult { + connection_id: msg.conn_id_on_a, + connection_id_state: ConnectionIdState::Reused, + connection_end: new_conn_end_on_a, + } }; let event_attributes = Attributes { connection_id: Some(result.connection_id.clone()), ..Default::default() }; + output.emit(IbcEvent::OpenAckConnection(event_attributes.into())); + output.log("success: conn_open_ack verification passed"); Ok(output.with_result(result)) } @@ -126,12 +169,12 @@ mod tests { let msg_ack = MsgConnectionOpenAck::try_from(get_dummy_raw_msg_conn_open_ack(10, 10)).unwrap(); - let conn_id = msg_ack.connection_id.clone(); - let counterparty_conn_id = msg_ack.counterparty_connection_id.clone(); + let conn_id = msg_ack.conn_id_on_a.clone(); + let counterparty_conn_id = msg_ack.conn_id_on_b.clone(); // Client parameters -- identifier and correct height (matching the proof height) let client_id = ClientId::from_str("mock_clientid").unwrap(); - let proof_height = msg_ack.proofs.height(); + let proof_height = msg_ack.proofs_height_on_b; // Parametrize the host chain to have a height at least as recent as the // the height of the proofs in the Ack msg. @@ -150,7 +193,7 @@ mod tests { client_id.clone(), Counterparty::new( client_id.clone(), - Some(msg_ack.counterparty_connection_id.clone()), + Some(msg_ack.conn_id_on_b.clone()), CommitmentPrefix::try_from(b"ibc".to_vec()).unwrap(), ), vec![msg_ack.version.clone()], diff --git a/crates/ibc/src/core/ics03_connection/handler/conn_open_confirm.rs b/crates/ibc/src/core/ics03_connection/handler/conn_open_confirm.rs index a9b844638..6a840893a 100644 --- a/crates/ibc/src/core/ics03_connection/handler/conn_open_confirm.rs +++ b/crates/ibc/src/core/ics03_connection/handler/conn_open_confirm.rs @@ -4,66 +4,86 @@ use crate::core::ics03_connection::connection::{ConnectionEnd, Counterparty, Sta use crate::core::ics03_connection::context::ConnectionReader; use crate::core::ics03_connection::error::Error; use crate::core::ics03_connection::events::Attributes; -use crate::core::ics03_connection::handler::verify; use crate::core::ics03_connection::handler::{ConnectionIdState, ConnectionResult}; use crate::core::ics03_connection::msgs::conn_open_confirm::MsgConnectionOpenConfirm; use crate::events::IbcEvent; use crate::handler::{HandlerOutput, HandlerResult}; use crate::prelude::*; +/// Per our convention, this message is processed on chain B. pub(crate) fn process( - ctx: &dyn ConnectionReader, + ctx_b: &dyn ConnectionReader, msg: MsgConnectionOpenConfirm, ) -> HandlerResult { let mut output = HandlerOutput::builder(); - // Validate the connection end. - let mut conn_end = ctx.connection_end(&msg.connection_id)?; - // A connection end must be in TryOpen state; otherwise return error. - if !conn_end.state_matches(&State::TryOpen) { - // Old connection end is in incorrect state, propagate the error. - return Err(Error::connection_mismatch(msg.connection_id)); + let conn_end_on_b = ctx_b.connection_end(&msg.conn_id_on_b)?; + if !conn_end_on_b.state_matches(&State::TryOpen) { + return Err(Error::connection_mismatch(msg.conn_id_on_b)); } - // Verify proofs. Assemble the connection end as we expect to find it on the counterparty. - let expected_conn = ConnectionEnd::new( - State::Open, - conn_end.counterparty().client_id().clone(), - Counterparty::new( - // The counterparty is the local chain. - conn_end.client_id().clone(), // The local client identifier. - Some(msg.connection_id.clone()), // Local connection id. - ctx.commitment_prefix(), // Local commitment prefix. - ), - conn_end.versions().to_vec(), - conn_end.delay_period(), - ); - - verify::verify_connection_proof( - ctx, - msg.proofs.height(), - &conn_end, - &expected_conn, - msg.proofs.height(), - msg.proofs.object_proof(), - )?; - - output.log("success: connection verification passed"); - - // Transition our own end of the connection to state OPEN. - conn_end.set_state(State::Open); - - let result = ConnectionResult { - connection_id: msg.connection_id, - connection_id_state: ConnectionIdState::Reused, - connection_end: conn_end, + // Verify proofs + { + let client_state_of_a_on_b = ctx_b.client_state(conn_end_on_b.client_id())?; + let consensus_state_of_a_on_b = + ctx_b.client_consensus_state(conn_end_on_b.client_id(), msg.proof_height_on_a)?; + + let client_id_on_a = conn_end_on_b.counterparty().client_id(); + let client_id_on_b = conn_end_on_b.client_id(); + let conn_id_on_a = conn_end_on_b + .counterparty() + .connection_id() + .ok_or_else(Error::invalid_counterparty)?; + let prefix_on_a = conn_end_on_b.counterparty().prefix(); + let prefix_on_b = ctx_b.commitment_prefix(); + + let expected_conn_end_on_a = ConnectionEnd::new( + State::Open, + client_id_on_a.clone(), + Counterparty::new( + client_id_on_b.clone(), + Some(msg.conn_id_on_b.clone()), + prefix_on_b, + ), + conn_end_on_b.versions().to_vec(), + conn_end_on_b.delay_period(), + ); + + client_state_of_a_on_b + .verify_connection_state( + msg.proof_height_on_a, + prefix_on_a, + &msg.proof_conn_end_on_a, + consensus_state_of_a_on_b.root(), + conn_id_on_a, + &expected_conn_end_on_a, + ) + .map_err(Error::verify_connection_state)?; + } + + // Success + let result = { + let new_conn_end_on_b = { + let mut new_conn_end_on_b = conn_end_on_b; + + new_conn_end_on_b.set_state(State::Open); + new_conn_end_on_b + }; + + ConnectionResult { + connection_id: msg.conn_id_on_b, + connection_id_state: ConnectionIdState::Reused, + connection_end: new_conn_end_on_b, + } }; let event_attributes = Attributes { connection_id: Some(result.connection_id.clone()), ..Default::default() }; + output.emit(IbcEvent::OpenConfirmConnection(event_attributes.into())); + output.log("success: conn_open_confirm verification passed"); Ok(output.with_result(result)) } @@ -102,7 +122,7 @@ mod tests { MsgConnectionOpenConfirm::try_from(get_dummy_raw_msg_conn_open_confirm()).unwrap(); let counterparty = Counterparty::new( client_id.clone(), - Some(msg_confirm.connection_id.clone()), + Some(msg_confirm.conn_id_on_b.clone()), CommitmentPrefix::try_from(b"ibc".to_vec()).unwrap(), ); @@ -131,7 +151,7 @@ mod tests { ctx: context .clone() .with_client(&client_id, Height::new(0, 10).unwrap()) - .with_connection(msg_confirm.connection_id.clone(), incorrect_conn_end_state), + .with_connection(msg_confirm.conn_id_on_b.clone(), incorrect_conn_end_state), msg: ConnectionMsg::ConnectionOpenConfirm(msg_confirm.clone()), want_pass: false, }, @@ -139,7 +159,7 @@ mod tests { name: "Processing successful".to_string(), ctx: context .with_client(&client_id, Height::new(0, 10).unwrap()) - .with_connection(msg_confirm.connection_id.clone(), correct_conn_end), + .with_connection(msg_confirm.conn_id_on_b.clone(), correct_conn_end), msg: ConnectionMsg::ConnectionOpenConfirm(msg_confirm), want_pass: true, }, diff --git a/crates/ibc/src/core/ics03_connection/handler/conn_open_init.rs b/crates/ibc/src/core/ics03_connection/handler/conn_open_init.rs index 12e934246..dffe27493 100644 --- a/crates/ibc/src/core/ics03_connection/handler/conn_open_init.rs +++ b/crates/ibc/src/core/ics03_connection/handler/conn_open_init.rs @@ -4,61 +4,63 @@ use crate::core::ics03_connection::connection::{ConnectionEnd, State}; use crate::core::ics03_connection::context::ConnectionReader; use crate::core::ics03_connection::error::Error; use crate::core::ics03_connection::events::Attributes; -use crate::core::ics03_connection::handler::{ConnectionIdState, ConnectionResult}; +use crate::core::ics03_connection::handler::ConnectionResult; use crate::core::ics03_connection::msgs::conn_open_init::MsgConnectionOpenInit; use crate::core::ics24_host::identifier::ConnectionId; use crate::events::IbcEvent; use crate::handler::{HandlerOutput, HandlerResult}; use crate::prelude::*; +use super::ConnectionIdState; + +/// Per our convention, this message is processed on chain A. pub(crate) fn process( - ctx: &dyn ConnectionReader, + ctx_a: &dyn ConnectionReader, msg: MsgConnectionOpenInit, ) -> HandlerResult { let mut output = HandlerOutput::builder(); // An IBC client running on the local (host) chain should exist. - ctx.client_state(&msg.client_id)?; + ctx_a.client_state(&msg.client_id_on_a)?; let versions = match msg.version { Some(version) => { - if ctx.get_compatible_versions().contains(&version) { + if ctx_a.get_compatible_versions().contains(&version) { Ok(vec![version]) } else { Err(Error::version_not_supported(version)) } } - None => Ok(ctx.get_compatible_versions()), + None => Ok(ctx_a.get_compatible_versions()), }?; - let new_connection_end = ConnectionEnd::new( + let conn_end_on_a = ConnectionEnd::new( State::Init, - msg.client_id.clone(), + msg.client_id_on_a.clone(), msg.counterparty.clone(), versions, msg.delay_period, ); // Construct the identifier for the new connection. - let id_counter = ctx.connection_counter()?; - let conn_id = ConnectionId::new(id_counter); - - output.log(format!( - "success: generated new connection identifier: {}", - conn_id - )); + let conn_id_on_a = ConnectionId::new(ctx_a.connection_counter()?); let result = ConnectionResult { - connection_id: conn_id.clone(), + connection_id: conn_id_on_a.clone(), + connection_end: conn_end_on_a, connection_id_state: ConnectionIdState::Generated, - connection_end: new_connection_end, }; let event_attributes = Attributes { - connection_id: Some(conn_id), + connection_id: Some(conn_id_on_a.clone()), ..Default::default() }; + output.emit(IbcEvent::OpenInitConnection(event_attributes.into())); + output.log(format!( + "success: conn_open_init: generated new connection identifier: {}", + conn_id_on_a + )); Ok(output.with_result(result)) } @@ -108,7 +110,7 @@ mod tests { }; let default_context = MockContext::default(); let good_context = default_context.clone().with_client( - &msg_conn_init_default.client_id, + &msg_conn_init_default.client_id_on_a, Height::new(0, 10).unwrap(), ); diff --git a/crates/ibc/src/core/ics03_connection/handler/conn_open_try.rs b/crates/ibc/src/core/ics03_connection/handler/conn_open_try.rs index 954d8e115..e4f425935 100644 --- a/crates/ibc/src/core/ics03_connection/handler/conn_open_try.rs +++ b/crates/ibc/src/core/ics03_connection/handler/conn_open_try.rs @@ -4,120 +4,128 @@ use crate::core::ics03_connection::connection::{ConnectionEnd, Counterparty, Sta use crate::core::ics03_connection::context::ConnectionReader; use crate::core::ics03_connection::error::Error; use crate::core::ics03_connection::events::Attributes; -use crate::core::ics03_connection::handler::verify::{ - check_client_consensus_height, verify_proofs, -}; -use crate::core::ics03_connection::handler::{ConnectionIdState, ConnectionResult}; +use crate::core::ics03_connection::handler::ConnectionResult; use crate::core::ics03_connection::msgs::conn_open_try::MsgConnectionOpenTry; use crate::core::ics24_host::identifier::ConnectionId; use crate::events::IbcEvent; use crate::handler::{HandlerOutput, HandlerResult}; use crate::prelude::*; +use super::ConnectionIdState; + +/// Per our convention, this message is processed on chain B. pub(crate) fn process( - ctx: &dyn ConnectionReader, + ctx_b: &dyn ConnectionReader, msg: MsgConnectionOpenTry, ) -> HandlerResult { let mut output = HandlerOutput::builder(); - // If a consensus proof is present, check that the consensus height (for - // client proof) in the message is not too advanced nor too old. - if let Some(consensus_height) = msg.consensus_height() { - check_client_consensus_height(ctx, consensus_height)?; - } - - // Unwrap the old connection end (if any) and its identifier. - let (mut new_connection_end, conn_id) = match &msg.previous_connection_id { - // A connection with this id should already exist. Search & validate. - Some(prev_id) => { - let old_connection_end = ctx.connection_end(prev_id)?; + let conn_id_on_b = ConnectionId::new(ctx_b.connection_counter()?); - // Validate that existing connection end matches with the one we're trying to establish. - if old_connection_end.state_matches(&State::Init) - && old_connection_end.counterparty_matches(&msg.counterparty) - && old_connection_end.client_id_matches(&msg.client_id) - && old_connection_end.delay_period() == msg.delay_period - { - // A ConnectionEnd already exists and all validation passed. - output.log(format!( - "success: `previous_connection_id` {} validation passed", - prev_id - )); - Ok((old_connection_end, prev_id.clone())) - } else { - // A ConnectionEnd already exists and validation failed. - Err(Error::connection_mismatch(prev_id.clone())) - } - } - // No prev. connection id was supplied, create a new connection end and conn id. - None => { - // Build a new connection end as well as an identifier. - let conn_end = ConnectionEnd::new( - State::Init, - msg.client_id.clone(), - msg.counterparty.clone(), - msg.counterparty_versions.clone(), - msg.delay_period, - ); - let id_counter = ctx.connection_counter()?; - let conn_id = ConnectionId::new(id_counter); + /////////////////////////////////////////////////////////// + // validate_self_client() verification goes here + // See [issue](https://github.com/cosmos/ibc-rs/issues/162) + /////////////////////////////////////////////////////////// - output.log(format!( - "success: new connection end and identifier {} generated", - conn_id - )); - Ok((conn_end, conn_id)) - } - }?; + if msg.consensus_height_of_b_on_a > ctx_b.host_current_height() { + // Fail if the consensus height is too advanced. + return Err(Error::invalid_consensus_height( + msg.consensus_height_of_b_on_a, + ctx_b.host_current_height(), + )); + } - // Proof verification in two steps: - // 1. Setup: build the ConnectionEnd as we expect to find it on the other party. - let expected_conn = ConnectionEnd::new( - State::Init, - msg.counterparty.client_id().clone(), - Counterparty::new(msg.client_id.clone(), None, ctx.commitment_prefix()), + let version_on_b = ctx_b.pick_version( + ctx_b.get_compatible_versions(), msg.counterparty_versions.clone(), + )?; + + let conn_end_on_b = ConnectionEnd::new( + State::TryOpen, + msg.client_id_on_b.clone(), + msg.counterparty.clone(), + vec![version_on_b], msg.delay_period, ); - // 2. Pass the details to the verification function. - verify_proofs( - ctx, - msg.client_state, - msg.proofs.height(), - &new_connection_end, - &expected_conn, - &msg.proofs, - )?; + // Verify proofs + { + let client_state_of_a_on_b = ctx_b.client_state(conn_end_on_b.client_id())?; + let consensus_state_of_a_on_b = + ctx_b.client_consensus_state(conn_end_on_b.client_id(), msg.proofs_height_on_a)?; - // Transition the connection end to the new state & pick a version. - new_connection_end.set_state(State::TryOpen); + let client_id_on_a = msg.counterparty.client_id(); + let prefix_on_a = conn_end_on_b.counterparty().prefix(); + let prefix_on_b = ctx_b.commitment_prefix(); - // Pick the version. - new_connection_end.set_version(ctx.pick_version( - ctx.get_compatible_versions(), - msg.counterparty_versions.clone(), - )?); + { + let conn_id_on_a = conn_end_on_b + .counterparty() + .connection_id() + .ok_or_else(Error::invalid_counterparty)?; + let versions_on_a = msg.counterparty_versions; + let expected_conn_end_on_a = ConnectionEnd::new( + State::Init, + client_id_on_a.clone(), + Counterparty::new(msg.client_id_on_b.clone(), None, prefix_on_b), + versions_on_a, + msg.delay_period, + ); - assert_eq!(new_connection_end.versions().len(), 1); + client_state_of_a_on_b + .verify_connection_state( + msg.proofs_height_on_a, + prefix_on_a, + &msg.proof_conn_end_on_a, + consensus_state_of_a_on_b.root(), + conn_id_on_a, + &expected_conn_end_on_a, + ) + .map_err(Error::verify_connection_state)?; + } - output.log("success: connection verification passed"); + client_state_of_a_on_b + .verify_client_full_state( + msg.proofs_height_on_a, + prefix_on_a, + &msg.proof_client_state_of_b_on_a, + consensus_state_of_a_on_b.root(), + client_id_on_a, + msg.client_state_of_b_on_a, + ) + .map_err(|e| { + Error::client_state_verification_failure(conn_end_on_b.client_id().clone(), e) + })?; + let expected_consensus_state_of_b_on_a = + ctx_b.host_consensus_state(msg.consensus_height_of_b_on_a)?; + client_state_of_a_on_b + .verify_client_consensus_state( + msg.proofs_height_on_a, + prefix_on_a, + &msg.proof_consensus_state_of_b_on_a, + consensus_state_of_a_on_b.root(), + client_id_on_a, + msg.consensus_height_of_b_on_a, + expected_consensus_state_of_b_on_a.as_ref(), + ) + .map_err(|e| Error::consensus_state_verification_failure(msg.proofs_height_on_a, e))?; + } + + // Success let result = ConnectionResult { - connection_id: conn_id.clone(), - connection_id_state: if matches!(msg.previous_connection_id, None) { - ConnectionIdState::Generated - } else { - ConnectionIdState::Reused - }, - connection_end: new_connection_end, + connection_id: conn_id_on_b.clone(), + connection_end: conn_end_on_b, + connection_id_state: ConnectionIdState::Generated, }; let event_attributes = Attributes { - connection_id: Some(conn_id), + connection_id: Some(conn_id_on_b), ..Default::default() }; + output.emit(IbcEvent::OpenTryConnection(event_attributes.into())); + output.log("success: conn_open_try verification passed"); Ok(output.with_result(result)) } @@ -210,20 +218,20 @@ mod tests { }, Test { name: "Processing fails because the client misses the consensus state targeted by the proof".to_string(), - ctx: context.clone().with_client(&msg_proof_height_missing.client_id, Height::new(0, client_consensus_state_height).unwrap()), + ctx: context.clone().with_client(&msg_proof_height_missing.client_id_on_b, Height::new(0, client_consensus_state_height).unwrap()), msg: ConnectionMsg::ConnectionOpenTry(Box::new(msg_proof_height_missing)), want_pass: false, }, Test { - name: "Good parameters but has previous_connection_id".to_string(), - ctx: context.clone().with_client(&msg_conn_try.client_id, Height::new(0, client_consensus_state_height).unwrap()), + name: "Good parameters (no previous_connection_id)".to_string(), + ctx: context.clone().with_client(&msg_conn_try.client_id_on_b, Height::new(0, client_consensus_state_height).unwrap()), msg: ConnectionMsg::ConnectionOpenTry(Box::new(msg_conn_try.clone())), - want_pass: false, + want_pass: true, }, Test { name: "Good parameters".to_string(), - ctx: context.with_client(&msg_conn_try.client_id, Height::new(0, client_consensus_state_height).unwrap()), - msg: ConnectionMsg::ConnectionOpenTry(Box::new(msg_conn_try.with_previous_connection_id(None))), + ctx: context.with_client(&msg_conn_try.client_id_on_b, Height::new(0, client_consensus_state_height).unwrap()), + msg: ConnectionMsg::ConnectionOpenTry(Box::new(msg_conn_try)), want_pass: true, }, ] diff --git a/crates/ibc/src/core/ics03_connection/handler/verify.rs b/crates/ibc/src/core/ics03_connection/handler/verify.rs deleted file mode 100644 index 65a23b58c..000000000 --- a/crates/ibc/src/core/ics03_connection/handler/verify.rs +++ /dev/null @@ -1,186 +0,0 @@ -//! ICS3 verification functions, common across all four handlers of ICS3. - -use ibc_proto::google::protobuf::Any; - -use crate::core::ics03_connection::connection::ConnectionEnd; -use crate::core::ics03_connection::context::ConnectionReader; -use crate::core::ics03_connection::error::Error; -use crate::core::ics23_commitment::commitment::CommitmentProofBytes; -use crate::proofs::{ConsensusProof, Proofs}; -use crate::Height; - -/// Entry point for verifying all proofs bundled in any ICS3 message. -pub fn verify_proofs( - ctx: &dyn ConnectionReader, - expected_client_state: Any, - height: Height, - connection_end: &ConnectionEnd, - expected_conn: &ConnectionEnd, - proofs: &Proofs, -) -> Result<(), Error> { - verify_connection_proof( - ctx, - height, - connection_end, - expected_conn, - proofs.height(), - proofs.object_proof(), - )?; - - // If the message includes a client state, then verify the proof for that state. - verify_client_proof( - ctx, - height, - connection_end, - expected_client_state, - proofs.height(), - proofs - .client_proof() - .as_ref() - .ok_or_else(Error::null_client_proof)?, - )?; - - // If a consensus proof is attached to the message, then verify it. - if let Some(proof) = proofs.consensus_proof() { - Ok(verify_consensus_proof(ctx, height, connection_end, &proof)?) - } else { - Ok(()) - } -} - -/// Verifies the authenticity and semantic correctness of a commitment `proof`. The commitment -/// claims to prove that an object of type connection exists on the source chain (i.e., the chain -/// which created this proof). This object must match the state of `expected_conn`. -pub fn verify_connection_proof( - ctx: &dyn ConnectionReader, - height: Height, - connection_end: &ConnectionEnd, - expected_conn: &ConnectionEnd, - proof_height: Height, - proof: &CommitmentProofBytes, -) -> Result<(), Error> { - // Fetch the client state (IBC client on the local/host chain). - let client_state = ctx.client_state(connection_end.client_id())?; - - // The client must not be frozen. - if client_state.is_frozen() { - return Err(Error::frozen_client(connection_end.client_id().clone())); - } - - // The client must have the consensus state for the height where this proof was created. - let consensus_state = ctx.client_consensus_state(connection_end.client_id(), proof_height)?; - - // A counterparty connection id of None causes `unwrap()` below and indicates an internal - // error as this is the connection id on the counterparty chain that must always be present. - let connection_id = connection_end - .counterparty() - .connection_id() - .ok_or_else(Error::invalid_counterparty)?; - - // Verify the proof for the connection state against the expected connection end. - client_state - .verify_connection_state( - height, - connection_end.counterparty().prefix(), - proof, - consensus_state.root(), - connection_id, - expected_conn, - ) - .map_err(Error::verify_connection_state) -} - -/// Verifies the client `proof` from a connection handshake message, typically from a -/// `MsgConnectionOpenTry` or a `MsgConnectionOpenAck`. The `expected_client_state` argument is a -/// representation for a client of the current chain (the chain handling the current message), which -/// is running on the counterparty chain (the chain which sent this message). This method does a -/// complete verification: that the client state the counterparty stores is valid (i.e., not frozen, -/// at the same revision as the current chain, with matching chain identifiers, etc) and that the -/// `proof` is correct. -pub fn verify_client_proof( - ctx: &dyn ConnectionReader, - height: Height, - connection_end: &ConnectionEnd, - expected_client_state: Any, - proof_height: Height, - proof: &CommitmentProofBytes, -) -> Result<(), Error> { - // Fetch the local client state (IBC client running on the host chain). - let client_state = ctx.client_state(connection_end.client_id())?; - - if client_state.is_frozen() { - return Err(Error::frozen_client(connection_end.client_id().clone())); - } - - let consensus_state = ctx.client_consensus_state(connection_end.client_id(), proof_height)?; - - client_state - .verify_client_full_state( - height, - connection_end.counterparty().prefix(), - proof, - consensus_state.root(), - connection_end.counterparty().client_id(), - expected_client_state, - ) - .map_err(|e| { - Error::client_state_verification_failure(connection_end.client_id().clone(), e) - }) -} - -pub fn verify_consensus_proof( - ctx: &dyn ConnectionReader, - height: Height, - connection_end: &ConnectionEnd, - proof: &ConsensusProof, -) -> Result<(), Error> { - // Fetch the client state (IBC client on the local chain). - let client_state = ctx.client_state(connection_end.client_id())?; - - if client_state.is_frozen() { - return Err(Error::frozen_client(connection_end.client_id().clone())); - } - - // Fetch the expected consensus state from the historical (local) header data. - let expected_consensus = ctx.host_consensus_state(proof.height())?; - - let consensus_state = ctx.client_consensus_state(connection_end.client_id(), height)?; - - client_state - .verify_client_consensus_state( - height, - connection_end.counterparty().prefix(), - proof.proof(), - consensus_state.root(), - connection_end.counterparty().client_id(), - proof.height(), - expected_consensus.as_ref(), - ) - .map_err(|e| Error::consensus_state_verification_failure(proof.height(), e)) -} - -/// Checks that `claimed_height` is within normal bounds, i.e., fresh enough so that the chain has -/// not pruned it yet, but not newer than the current (actual) height of the local chain. -pub fn check_client_consensus_height( - ctx: &dyn ConnectionReader, - claimed_height: Height, -) -> Result<(), Error> { - if claimed_height > ctx.host_current_height() { - // Fail if the consensus height is too advanced. - return Err(Error::invalid_consensus_height( - claimed_height, - ctx.host_current_height(), - )); - } - - if claimed_height < ctx.host_oldest_height() { - // Fail if the consensus height is too old (has been pruned). - return Err(Error::stale_consensus_height( - claimed_height, - ctx.host_oldest_height(), - )); - } - - // Height check is within normal bounds, check passes. - Ok(()) -} diff --git a/crates/ibc/src/core/ics03_connection/msgs/conn_open_ack.rs b/crates/ibc/src/core/ics03_connection/msgs/conn_open_ack.rs index 1bbd5bc1a..b929d4da0 100644 --- a/crates/ibc/src/core/ics03_connection/msgs/conn_open_ack.rs +++ b/crates/ibc/src/core/ics03_connection/msgs/conn_open_ack.rs @@ -8,32 +8,36 @@ use crate::core::ics03_connection::error::Error; use crate::core::ics03_connection::version::Version; use crate::core::ics23_commitment::commitment::CommitmentProofBytes; use crate::core::ics24_host::identifier::ConnectionId; -use crate::proofs::{ConsensusProof, Proofs}; use crate::signer::Signer; use crate::tx_msg::Msg; use crate::Height; pub const TYPE_URL: &str = "/ibc.core.connection.v1.MsgConnectionOpenAck"; -/// Message definition `MsgConnectionOpenAck` (i.e., `ConnOpenAck` datagram). +/// Per our convention, this message is sent to chain A. +/// The handler will check proofs of chain B. #[derive(Clone, Debug, PartialEq, Eq)] pub struct MsgConnectionOpenAck { - pub connection_id: ConnectionId, - pub counterparty_connection_id: ConnectionId, - pub client_state: Any, - pub proofs: Proofs, + /// ConnectionId that chain A has chosen for it's ConnectionEnd + pub conn_id_on_a: ConnectionId, + /// ConnectionId that chain B has chosen for it's ConnectionEnd + pub conn_id_on_b: ConnectionId, + /// ClientState of client tracking chain A on chain B + pub client_state_of_a_on_b: Any, + /// proof of ConnectionEnd stored on Chain B during ConnOpenTry + pub proof_conn_end_on_b: CommitmentProofBytes, + /// proof of ClientState tracking chain A on chain B + pub proof_client_state_of_a_on_b: CommitmentProofBytes, + /// proof that chain B has stored ConsensusState of chain A on its client + pub proof_consensus_state_of_a_on_b: CommitmentProofBytes, + /// Height at which all proofs in this message were taken + pub proofs_height_on_b: Height, + /// height of latest header of chain A that updated the client on chain B + pub consensus_height_of_a_on_b: Height, pub version: Version, pub signer: Signer, } -impl MsgConnectionOpenAck { - /// Getter for accessing the `consensus_height` field from this message. - /// Returns `None` if this field is not set. - pub fn consensus_height(&self) -> Option { - self.proofs.consensus_proof().map(|proof| proof.height()) - } -} - impl Msg for MsgConnectionOpenAck { type ValidationError = Error; type Raw = RawMsgConnectionOpenAck; @@ -53,73 +57,52 @@ impl TryFrom for MsgConnectionOpenAck { type Error = Error; fn try_from(msg: RawMsgConnectionOpenAck) -> Result { - let consensus_height = msg - .consensus_height - .and_then(|raw_height| raw_height.try_into().ok()) - .ok_or_else(Error::missing_consensus_height)?; - let consensus_proof_obj = ConsensusProof::new( - msg.proof_consensus - .try_into() - .map_err(Error::invalid_proof)?, - consensus_height, - ) - .map_err(Error::invalid_proof)?; - - let proof_height = msg - .proof_height - .and_then(|raw_height| raw_height.try_into().ok()) - .ok_or_else(Error::missing_proof_height)?; - - let client_proof = - CommitmentProofBytes::try_from(msg.proof_client).map_err(Error::invalid_proof)?; - Ok(Self { - connection_id: msg + conn_id_on_a: msg .connection_id .parse() .map_err(Error::invalid_identifier)?, - counterparty_connection_id: msg + conn_id_on_b: msg .counterparty_connection_id .parse() .map_err(Error::invalid_identifier)?, - client_state: msg.client_state.ok_or_else(Error::missing_client_state)?, + client_state_of_a_on_b: msg.client_state.ok_or_else(Error::missing_client_state)?, version: msg.version.ok_or_else(Error::empty_versions)?.try_into()?, - proofs: Proofs::new( - msg.proof_try.try_into().map_err(Error::invalid_proof)?, - Some(client_proof), - Option::from(consensus_proof_obj), - None, - proof_height, - ) - .map_err(Error::invalid_proof)?, + proof_conn_end_on_b: msg.proof_try.try_into().map_err(Error::invalid_proof)?, + proof_client_state_of_a_on_b: msg + .proof_client + .try_into() + .map_err(Error::invalid_proof)?, + proof_consensus_state_of_a_on_b: msg + .proof_consensus + .try_into() + .map_err(Error::invalid_proof)?, + proofs_height_on_b: msg + .proof_height + .and_then(|raw_height| raw_height.try_into().ok()) + .ok_or_else(Error::missing_proof_height)?, + consensus_height_of_a_on_b: msg + .consensus_height + .and_then(|raw_height| raw_height.try_into().ok()) + .ok_or_else(Error::missing_consensus_height)?, signer: msg.signer.parse().map_err(Error::signer)?, }) } } impl From for RawMsgConnectionOpenAck { - fn from(ics_msg: MsgConnectionOpenAck) -> Self { + fn from(msg: MsgConnectionOpenAck) -> Self { RawMsgConnectionOpenAck { - connection_id: ics_msg.connection_id.as_str().to_string(), - counterparty_connection_id: ics_msg.counterparty_connection_id.as_str().to_string(), - client_state: Some(ics_msg.client_state), - proof_height: Some(ics_msg.proofs.height().into()), - proof_try: ics_msg.proofs.object_proof().clone().into(), - proof_client: ics_msg - .proofs - .client_proof() - .clone() - .map_or_else(Vec::new, |v| v.into()), - proof_consensus: ics_msg - .proofs - .consensus_proof() - .map_or_else(Vec::new, |v| v.proof().clone().into()), - consensus_height: ics_msg - .proofs - .consensus_proof() - .map_or_else(|| None, |h| Some(h.height().into())), - version: Some(ics_msg.version.into()), - signer: ics_msg.signer.to_string(), + connection_id: msg.conn_id_on_a.as_str().to_string(), + counterparty_connection_id: msg.conn_id_on_b.as_str().to_string(), + client_state: Some(msg.client_state_of_a_on_b), + proof_height: Some(msg.proofs_height_on_b.into()), + proof_try: msg.proof_conn_end_on_b.into(), + proof_client: msg.proof_client_state_of_a_on_b.into(), + proof_consensus: msg.proof_consensus_state_of_a_on_b.into(), + consensus_height: Some(msg.consensus_height_of_a_on_b.into()), + version: Some(msg.version.into()), + signer: msg.signer.to_string(), } } } diff --git a/crates/ibc/src/core/ics03_connection/msgs/conn_open_confirm.rs b/crates/ibc/src/core/ics03_connection/msgs/conn_open_confirm.rs index 750b8ec16..a52673e11 100644 --- a/crates/ibc/src/core/ics03_connection/msgs/conn_open_confirm.rs +++ b/crates/ibc/src/core/ics03_connection/msgs/conn_open_confirm.rs @@ -1,4 +1,5 @@ -use crate::prelude::*; +use crate::core::ics23_commitment::commitment::CommitmentProofBytes; +use crate::{prelude::*, Height}; use ibc_proto::protobuf::Protobuf; @@ -6,19 +7,21 @@ use ibc_proto::ibc::core::connection::v1::MsgConnectionOpenConfirm as RawMsgConn use crate::core::ics03_connection::error::Error; use crate::core::ics24_host::identifier::ConnectionId; -use crate::proofs::Proofs; use crate::signer::Signer; use crate::tx_msg::Msg; pub const TYPE_URL: &str = "/ibc.core.connection.v1.MsgConnectionOpenConfirm"; -/// -/// Message definition for `MsgConnectionOpenConfirm` (i.e., `ConnOpenConfirm` datagram). -/// +/// Per our convention, this message is sent to chain B. +/// The handler will check proofs of chain A. #[derive(Clone, Debug, PartialEq, Eq)] pub struct MsgConnectionOpenConfirm { - pub connection_id: ConnectionId, - pub proofs: Proofs, + /// ConnectionId that chain B has chosen for it's ConnectionEnd + pub conn_id_on_b: ConnectionId, + /// proof of ConnectionEnd stored on Chain A during ConnOpenInit + pub proof_conn_end_on_a: CommitmentProofBytes, + /// Height at which `proof_conn_end_on_a` in this message was taken + pub proof_height_on_a: Height, pub signer: Signer, } @@ -41,36 +44,28 @@ impl TryFrom for MsgConnectionOpenConfirm { type Error = Error; fn try_from(msg: RawMsgConnectionOpenConfirm) -> Result { - let proof_height = msg - .proof_height - .and_then(|raw_height| raw_height.try_into().ok()) - .ok_or_else(Error::missing_proof_height)?; - Ok(Self { - connection_id: msg + conn_id_on_b: msg .connection_id .parse() .map_err(Error::invalid_identifier)?, - proofs: Proofs::new( - msg.proof_ack.try_into().map_err(Error::invalid_proof)?, - None, - None, - None, - proof_height, - ) - .map_err(Error::invalid_proof)?, + proof_conn_end_on_a: msg.proof_ack.try_into().map_err(Error::invalid_proof)?, + proof_height_on_a: msg + .proof_height + .and_then(|raw_height| raw_height.try_into().ok()) + .ok_or_else(Error::missing_proof_height)?, signer: msg.signer.parse().map_err(Error::signer)?, }) } } impl From for RawMsgConnectionOpenConfirm { - fn from(ics_msg: MsgConnectionOpenConfirm) -> Self { + fn from(msg: MsgConnectionOpenConfirm) -> Self { RawMsgConnectionOpenConfirm { - connection_id: ics_msg.connection_id.as_str().to_string(), - proof_ack: ics_msg.proofs.object_proof().clone().into(), - proof_height: Some(ics_msg.proofs.height().into()), - signer: ics_msg.signer.to_string(), + connection_id: msg.conn_id_on_b.as_str().to_string(), + proof_ack: msg.proof_conn_end_on_a.into(), + proof_height: Some(msg.proof_height_on_a.into()), + signer: msg.signer.to_string(), } } } diff --git a/crates/ibc/src/core/ics03_connection/msgs/conn_open_init.rs b/crates/ibc/src/core/ics03_connection/msgs/conn_open_init.rs index b48bf3f2c..a3ae47e50 100644 --- a/crates/ibc/src/core/ics03_connection/msgs/conn_open_init.rs +++ b/crates/ibc/src/core/ics03_connection/msgs/conn_open_init.rs @@ -14,12 +14,12 @@ use crate::tx_msg::Msg; pub const TYPE_URL: &str = "/ibc.core.connection.v1.MsgConnectionOpenInit"; -/// -/// Message definition `MsgConnectionOpenInit` (i.e., the `ConnOpenInit` datagram). -/// +/// Per our convention, this message is sent to chain A. +/// The handler will check proofs of chain B. #[derive(Clone, Debug, PartialEq, Eq)] pub struct MsgConnectionOpenInit { - pub client_id: ClientId, + /// ClientId on chain A that the connection is being opened for + pub client_id_on_a: ClientId, pub counterparty: Counterparty, pub version: Option, pub delay_period: Duration, @@ -46,7 +46,7 @@ impl TryFrom for MsgConnectionOpenInit { fn try_from(msg: RawMsgConnectionOpenInit) -> Result { Ok(Self { - client_id: msg.client_id.parse().map_err(Error::invalid_identifier)?, + client_id_on_a: msg.client_id.parse().map_err(Error::invalid_identifier)?, counterparty: msg .counterparty .ok_or_else(Error::missing_counterparty)? @@ -61,7 +61,7 @@ impl TryFrom for MsgConnectionOpenInit { impl From for RawMsgConnectionOpenInit { fn from(ics_msg: MsgConnectionOpenInit) -> Self { RawMsgConnectionOpenInit { - client_id: ics_msg.client_id.as_str().to_string(), + client_id: ics_msg.client_id_on_a.as_str().to_string(), counterparty: Some(ics_msg.counterparty.into()), version: ics_msg.version.map(|version| version.into()), delay_period: ics_msg.delay_period.as_nanos() as u64, @@ -85,7 +85,10 @@ pub mod test_util { impl MsgConnectionOpenInit { /// Setter for `client_id`. Amenable to chaining, since it consumes the input message. pub fn with_client_id(self, client_id: ClientId) -> Self { - MsgConnectionOpenInit { client_id, ..self } + MsgConnectionOpenInit { + client_id_on_a: client_id, + ..self + } } } diff --git a/crates/ibc/src/core/ics03_connection/msgs/conn_open_try.rs b/crates/ibc/src/core/ics03_connection/msgs/conn_open_try.rs index 70a79b886..4a9ee8bf5 100644 --- a/crates/ibc/src/core/ics03_connection/msgs/conn_open_try.rs +++ b/crates/ibc/src/core/ics03_connection/msgs/conn_open_try.rs @@ -2,7 +2,6 @@ use crate::prelude::*; use core::{ convert::{TryFrom, TryInto}, - str::FromStr, time::Duration, }; @@ -14,35 +13,41 @@ use crate::core::ics03_connection::connection::Counterparty; use crate::core::ics03_connection::error::Error; use crate::core::ics03_connection::version::Version; use crate::core::ics23_commitment::commitment::CommitmentProofBytes; -use crate::core::ics24_host::identifier::{ClientId, ConnectionId}; -use crate::proofs::{ConsensusProof, Proofs}; +use crate::core::ics24_host::identifier::ClientId; use crate::signer::Signer; use crate::tx_msg::Msg; use crate::Height; pub const TYPE_URL: &str = "/ibc.core.connection.v1.MsgConnectionOpenTry"; -/// -/// Message definition `MsgConnectionOpenTry` (i.e., `ConnOpenTry` datagram). -/// +/// Per our convention, this message is sent to chain B. +/// The handler will check proofs of chain A. #[derive(Clone, Debug, PartialEq, Eq)] pub struct MsgConnectionOpenTry { - pub previous_connection_id: Option, - pub client_id: ClientId, - pub client_state: Any, + /// ClientId on B that the connection is being opened for + pub client_id_on_b: ClientId, + /// ClientState of client tracking chain B on chain A + pub client_state_of_b_on_a: Any, + /// ClientId, ConnectionId and prefix of chain A pub counterparty: Counterparty, + /// Versions supported by chain A pub counterparty_versions: Vec, - pub proofs: Proofs, + /// proof of ConnectionEnd stored on Chain A during ConnOpenInit + pub proof_conn_end_on_a: CommitmentProofBytes, + /// proof that chain A has stored ClientState of chain B on its client + pub proof_client_state_of_b_on_a: CommitmentProofBytes, + /// proof that chain A has stored ConsensusState of chain B on its client + pub proof_consensus_state_of_b_on_a: CommitmentProofBytes, + /// Height at which all proofs in this message were taken + pub proofs_height_on_a: Height, + /// height of latest header of chain A that updated the client on chain B + pub consensus_height_of_b_on_a: Height, pub delay_period: Duration, pub signer: Signer, -} -impl MsgConnectionOpenTry { - /// Getter for accessing the `consensus_height` field from this message. - /// Returns `None` if this field is not set. - pub fn consensus_height(&self) -> Option { - self.proofs.consensus_proof().map(|proof| proof.height()) - } + #[deprecated(since = "0.21.0")] + /// Only kept here for proper conversion to/from the raw type + previous_connection_id: String, } impl Msg for MsgConnectionOpenTry { @@ -64,33 +69,6 @@ impl TryFrom for MsgConnectionOpenTry { type Error = Error; fn try_from(msg: RawMsgConnectionOpenTry) -> Result { - let previous_connection_id = Some(msg.previous_connection_id) - .filter(|x| !x.is_empty()) - .map(|v| FromStr::from_str(v.as_str())) - .transpose() - .map_err(Error::invalid_identifier)?; - - let consensus_height = msg - .consensus_height - .and_then(|raw_height| raw_height.try_into().ok()) - .ok_or_else(Error::missing_consensus_height)?; - - let consensus_proof_obj = ConsensusProof::new( - msg.proof_consensus - .try_into() - .map_err(Error::invalid_proof)?, - consensus_height, - ) - .map_err(Error::invalid_proof)?; - - let proof_height = msg - .proof_height - .and_then(|raw_height| raw_height.try_into().ok()) - .ok_or_else(Error::missing_proof_height)?; - - let client_proof = - CommitmentProofBytes::try_from(msg.proof_client).map_err(Error::invalid_proof)?; - let counterparty_versions = msg .counterparty_versions .into_iter() @@ -102,22 +80,31 @@ impl TryFrom for MsgConnectionOpenTry { } Ok(Self { - previous_connection_id, - client_id: msg.client_id.parse().map_err(Error::invalid_identifier)?, - client_state: msg.client_state.ok_or_else(Error::missing_client_state)?, + previous_connection_id: msg.previous_connection_id, + client_id_on_b: msg.client_id.parse().map_err(Error::invalid_identifier)?, + client_state_of_b_on_a: msg.client_state.ok_or_else(Error::missing_client_state)?, counterparty: msg .counterparty .ok_or_else(Error::missing_counterparty)? .try_into()?, counterparty_versions, - proofs: Proofs::new( - msg.proof_init.try_into().map_err(Error::invalid_proof)?, - Some(client_proof), - Some(consensus_proof_obj), - None, - proof_height, - ) - .map_err(Error::invalid_proof)?, + proof_conn_end_on_a: msg.proof_init.try_into().map_err(Error::invalid_proof)?, + proof_client_state_of_b_on_a: msg + .proof_client + .try_into() + .map_err(Error::invalid_proof)?, + proof_consensus_state_of_b_on_a: msg + .proof_consensus + .try_into() + .map_err(Error::invalid_proof)?, + proofs_height_on_a: msg + .proof_height + .and_then(|raw_height| raw_height.try_into().ok()) + .ok_or_else(Error::missing_proof_height)?, + consensus_height_of_b_on_a: msg + .consensus_height + .and_then(|raw_height| raw_height.try_into().ok()) + .ok_or_else(Error::missing_consensus_height)?, delay_period: Duration::from_nanos(msg.delay_period), signer: msg.signer.parse().map_err(Error::signer)?, }) @@ -125,36 +112,24 @@ impl TryFrom for MsgConnectionOpenTry { } impl From for RawMsgConnectionOpenTry { - fn from(ics_msg: MsgConnectionOpenTry) -> Self { + fn from(msg: MsgConnectionOpenTry) -> Self { RawMsgConnectionOpenTry { - client_id: ics_msg.client_id.as_str().to_string(), - previous_connection_id: ics_msg - .previous_connection_id - .map_or_else(|| "".to_string(), |v| v.as_str().to_string()), - client_state: Some(ics_msg.client_state), - counterparty: Some(ics_msg.counterparty.into()), - delay_period: ics_msg.delay_period.as_nanos() as u64, - counterparty_versions: ics_msg + client_id: msg.client_id_on_b.as_str().to_string(), + previous_connection_id: msg.previous_connection_id, + client_state: Some(msg.client_state_of_b_on_a), + counterparty: Some(msg.counterparty.into()), + delay_period: msg.delay_period.as_nanos() as u64, + counterparty_versions: msg .counterparty_versions .iter() .map(|v| v.clone().into()) .collect(), - proof_height: Some(ics_msg.proofs.height().into()), - proof_init: ics_msg.proofs.object_proof().clone().into(), - proof_client: ics_msg - .proofs - .client_proof() - .clone() - .map_or_else(Vec::new, |v| v.into()), - proof_consensus: ics_msg - .proofs - .consensus_proof() - .map_or_else(Vec::new, |v| v.proof().clone().into()), - consensus_height: ics_msg - .proofs - .consensus_proof() - .map_or_else(|| None, |h| Some(h.height().into())), - signer: ics_msg.signer.to_string(), + proof_height: Some(msg.proofs_height_on_a.into()), + proof_init: msg.proof_conn_end_on_a.into(), + proof_client: msg.proof_client_state_of_b_on_a.into(), + proof_consensus: msg.proof_consensus_state_of_b_on_a.into(), + consensus_height: Some(msg.consensus_height_of_b_on_a.into()), + signer: msg.signer.to_string(), } } } @@ -176,21 +151,13 @@ pub mod test_util { /// Testing-specific helper methods. impl MsgConnectionOpenTry { - /// Moves the given message into another one, and updates the `previous_connection_id` field. - pub fn with_previous_connection_id( - self, - previous_connection_id: Option, - ) -> MsgConnectionOpenTry { + /// Setter for `client_id`. + pub fn with_client_id(self, client_id: ClientId) -> MsgConnectionOpenTry { MsgConnectionOpenTry { - previous_connection_id, + client_id_on_b: client_id, ..self } } - - /// Setter for `client_id`. - pub fn with_client_id(self, client_id: ClientId) -> MsgConnectionOpenTry { - MsgConnectionOpenTry { client_id, ..self } - } } /// Returns a dummy `RawMsgConnectionOpenTry` with parametrized heights. The parameter diff --git a/crates/ibc/src/core/ics04_channel/handler/chan_open_ack.rs b/crates/ibc/src/core/ics04_channel/handler/chan_open_ack.rs index 94a2f0582..dd4e622a2 100644 --- a/crates/ibc/src/core/ics04_channel/handler/chan_open_ack.rs +++ b/crates/ibc/src/core/ics04_channel/handler/chan_open_ack.rs @@ -154,7 +154,7 @@ mod tests { let conn_end = ConnectionEnd::new( ConnectionState::Open, - msg_conn_init.client_id.clone(), + msg_conn_init.client_id_on_a.clone(), ConnectionCounterparty::new( msg_conn_init.counterparty.client_id().clone(), Some(ConnectionId::from_str("defaultConnection-1").unwrap()), @@ -225,7 +225,7 @@ mod tests { ctx: context .clone() .with_client( - &msg_conn_try.client_id, + &msg_conn_try.client_id_on_b, Height::new(0, client_consensus_state_height).unwrap(), ) .with_channel( @@ -241,7 +241,7 @@ mod tests { ctx: context .clone() .with_client( - &msg_conn_try.client_id, + &msg_conn_try.client_id_on_b, Height::new(0, client_consensus_state_height).unwrap(), ) .with_channel( @@ -269,7 +269,7 @@ mod tests { name: "Good parameters".to_string(), ctx: context // .clone() .with_client( - &msg_conn_try.client_id, + &msg_conn_try.client_id_on_b, Height::new(0, client_consensus_state_height).unwrap(), ) .with_connection(cid, conn_end) diff --git a/crates/ibc/src/core/ics04_channel/handler/chan_open_init.rs b/crates/ibc/src/core/ics04_channel/handler/chan_open_init.rs index 2530e37c7..40365fa66 100644 --- a/crates/ibc/src/core/ics04_channel/handler/chan_open_init.rs +++ b/crates/ibc/src/core/ics04_channel/handler/chan_open_init.rs @@ -116,7 +116,7 @@ mod tests { let init_conn_end = ConnectionEnd::new( ConnectionState::Init, - msg_conn_init.client_id.clone(), + msg_conn_init.client_id_on_a.clone(), msg_conn_init.counterparty.clone(), get_compatible_versions(), msg_conn_init.delay_period, diff --git a/crates/ibc/src/core/mod.rs b/crates/ibc/src/core/mod.rs index ef9cc9468..6b489066b 100644 --- a/crates/ibc/src/core/mod.rs +++ b/crates/ibc/src/core/mod.rs @@ -1,5 +1,23 @@ //! The designs and logic pertaining to the transport, authentication, and //! ordering layers of the IBC protocol. +//! +//! Naming is hard in the IBC handlers, since we deal with a client on a +//! *counterparty* chain, which is itself a light client of *self* (the chain +//! the handler is currently running on). So depending on the frame of reference +//! chosen, e.g. counterparty_client_state could mean: +//! +//! 1. the client state of the client running on the counterparty chain +//! 2. or the state of the "counterparty client" (that is, the client that we +//! run of the counterparty chain) running on the host chain +//! +//! We remove such ambiguity by adopting the following conventions: +//! + we call "chain A" the chain that runs `OpenInit` and `OpenAck` +//! + we call "chain B" the chain that runs `OpenTry` and `OpenConfirm` +//! + In variable names, +//! + `on_a` implies "stored on chain A" +//! + `of_a` implies "of light client for chain A" So +//! `client_state_of_a_on_b` means "the client state of light client for chain A +//! stored on chain B" pub mod ics02_client; pub mod ics03_connection; diff --git a/crates/ibc/tests/README.md b/crates/ibc/tests/README.md deleted file mode 100644 index b606f1457..000000000 --- a/crates/ibc/tests/README.md +++ /dev/null @@ -1,61 +0,0 @@ -## Model-based tests for IBC modules - -### The model - -This directory contains the model-based tests for the IBC modules. They are "model-based" because they are generated from a `TLA+` model of the IBC modules (see [IBC.tla](support/model_based/IBC.tla)). - -To instantiate the model, we define in [IBC.cfg](support/model_based/IBC.cfg) the following model constants: - -- `ChainIds = {"chain-A", "chain-B"}`, indicating that two chains, `chain-A` and `chain-B`, will be created -- `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 -INVARIANTS - TypeOK - ModelNeverErrors -``` - -Then, we can ask [`TLC`](https://github.com/tlaplus/tlaplus), a model checker for `TLA+`, to check that these invariants hold: - -```bash -wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -java -cp tla2tools.jar tlc2.TLC IBC.tla -modelcheck -config IBC.cfg -workers auto -``` - -### The tests - -Tests are `TLA+` assertions that describe the desired shape of the test (see [IBCTests.tla](support/model_based/IBCTests.tla)). One of the assertions in [IBCTests.tla](support/model_based/IBCTests.tla) is the following: - -```tla -ICS02UpdateOKTest == - /\ actionOutcome = "ICS02UpdateOK" -``` - -This very simple assertion describes a test where the [model](support/model_based/IBC.tla) variable `actionOutcome` reaches the value `"ICS02UpdateOK"`, which occurs when a client is successfully updated to a new height (see [ICS02.tla](support/model_based/ICS02.tla)). - -To generate a test from the `ICS02UpdateOKTest` assertion, we first define an invariant negating it: -```tla -ICS02UpdateOKTestNeg == ~ICS02UpdateOKTest -``` - -Then, we ask `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. - -### Running the model-based tests - -The model-based tests can be run with the following command: - -```bash -cd modules/ -cargo test --features mocks -- mbt -``` - -The above uses [`modelator`](https://github.com/informalsystems/modelator), a model-based testing tool. -One of the steps automated by `modelator` is the negation of TLA+ tests assertions mentioned earlier. - -To debug possible issues with `modelator`, run instead: -```bash -RUST_LOG=modelator=trace cargo test --features mocks -- mbt -``` diff --git a/crates/ibc/tests/mbt.rs b/crates/ibc/tests/mbt.rs deleted file mode 100644 index 1c505dbc2..000000000 --- a/crates/ibc/tests/mbt.rs +++ /dev/null @@ -1,30 +0,0 @@ -extern crate alloc; - -mod runner; - -use modelator::{ - model::checker::{ModelChecker, ModelCheckerRuntime}, - Error, -}; -use runner::IbcTestRunner; - -#[test] -fn mbt() { - // 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) = run_tests() { - panic!("{}", e); - } -} - -fn run_tests() -> Result<(), Error> { - // run the test - let tla_tests_file = "tests/support/model_based/IBCTests.tla"; - let tla_config_file = "tests/support/model_based/IBCTests.cfg"; - let runtime = modelator::ModelatorRuntime::default() - .model_checker_runtime(ModelCheckerRuntime::default().model_checker(ModelChecker::Tlc)); - - let mut runner = IbcTestRunner::new(); - runtime.run_tla_steps(tla_tests_file, tla_config_file, &mut runner)?; - Ok(()) -} diff --git a/crates/ibc/tests/runner/mod.rs b/crates/ibc/tests/runner/mod.rs deleted file mode 100644 index ae6c19a01..000000000 --- a/crates/ibc/tests/runner/mod.rs +++ /dev/null @@ -1,528 +0,0 @@ -pub mod step; - -use alloc::collections::btree_map::BTreeMap as HashMap; -use core::convert::TryInto; -use core::fmt::Debug; -use core::time::Duration; - -use ibc::core::ics02_client::client_type::ClientType; -use ibc::core::ics02_client::context::ClientReader; -use ibc::core::ics02_client::error as client_error; -use ibc::core::ics02_client::msgs::create_client::MsgCreateClient; -use ibc::core::ics02_client::msgs::update_client::MsgUpdateClient; -use ibc::core::ics02_client::msgs::upgrade_client::MsgUpgradeClient; -use ibc::core::ics02_client::msgs::ClientMsg; -use ibc::core::ics03_connection::connection::{Counterparty, State as ConnectionState}; -use ibc::core::ics03_connection::error as connection_error; -use ibc::core::ics03_connection::msgs::conn_open_ack::MsgConnectionOpenAck; -use ibc::core::ics03_connection::msgs::conn_open_confirm::MsgConnectionOpenConfirm; -use ibc::core::ics03_connection::msgs::conn_open_init::MsgConnectionOpenInit; -use ibc::core::ics03_connection::msgs::conn_open_try::MsgConnectionOpenTry; -use ibc::core::ics03_connection::msgs::ConnectionMsg; -use ibc::core::ics03_connection::version::Version; -use ibc::core::ics04_channel::context::ChannelReader; -use ibc::core::ics23_commitment::commitment::{CommitmentPrefix, CommitmentProofBytes}; -use ibc::core::ics24_host::identifier::{ChainId, ClientId, ConnectionId}; -use ibc::core::ics26_routing::error as routing_error; -use ibc::core::ics26_routing::msgs::Ics26Envelope; -use ibc::mock::client_state::MockClientState; -use ibc::mock::consensus_state::MockConsensusState; -use ibc::mock::context::MockContext; -use ibc::mock::header::MockHeader; -use ibc::mock::host::HostType; -use ibc::proofs::{ConsensusProof, Proofs}; -use ibc::relayer::ics18_relayer::context::Ics18Context; -use ibc::relayer::ics18_relayer::error as relayer_error; -use ibc::signer::Signer; -use ibc::timestamp::ZERO_DURATION; -use ibc::Height; - -use step::{Action, ActionOutcome, Chain, Step}; - -#[derive(Debug, Clone)] -pub struct IbcTestRunner { - // mapping from chain identifier to its context - contexts: HashMap, -} - -impl IbcTestRunner { - pub fn new() -> Self { - Self { - contexts: Default::default(), - } - } - - /// Create a `MockContext` for a given `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_struct, - HostType::Mock, - max_history_size, - initial_height, - ); - self.contexts.insert(chain_id, ctx); - } - - /// Returns a reference to the `MockContext` of a given `chain_id`. - /// Panic if the context for `chain_id` is not found. - pub fn chain_context(&self, chain_id: String) -> &MockContext { - self.contexts - .get(&chain_id) - .expect("chain context should have been initialized") - } - - /// Returns a mutable reference to the `MockContext` of a given `chain_id`. - /// Panic if the context for `chain_id` is not found. - pub fn chain_context_mut(&mut self, chain_id: String) -> &mut MockContext { - self.contexts - .get_mut(&chain_id) - .expect("chain context should have been initialized") - } - - pub fn extract_ics02_error_kind( - ics18_result: Result<(), relayer_error::Error>, - ) -> client_error::ErrorDetail { - let ics18_error = ics18_result.expect_err("ICS18 error expected"); - match ics18_error.0 { - relayer_error::ErrorDetail::TransactionFailed(e) => match e.source { - routing_error::ErrorDetail::Ics02Client(e) => e.source, - e => { - panic!("Expected Ics02Client error, instead got {:?}", e); - } - }, - e => { - panic!("Expected TransactionFailed error, instead got {:?}", e); - } - } - } - - pub fn extract_ics03_error_kind( - ics18_result: Result<(), relayer_error::Error>, - ) -> connection_error::ErrorDetail { - let ics18_error = ics18_result.expect_err("ICS18 error expected"); - - match ics18_error.0 { - relayer_error::ErrorDetail::TransactionFailed(e) => match e.source { - routing_error::ErrorDetail::Ics03Connection(e) => e.source, - e => { - panic!("Expected Ics02Client error, instead got {:?}", e); - } - }, - e => { - panic!("Expected TransactionFailed error, instead got {:?}", e); - } - } - } - - pub fn chain_id(chain_id: String, height: Height) -> ChainId { - ChainId::new(chain_id, height.revision_number()) - } - - 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") - } - - pub fn connection_id(connection_id: u64) -> ConnectionId { - ConnectionId::new(connection_id) - } - - pub fn height(height: Height) -> Height { - Height::new(height.revision_number(), height.revision_height()).unwrap() - } - - fn mock_header(height: Height) -> MockHeader { - MockHeader::new(Self::height(height)) - } - - pub fn client_state(height: Height) -> MockClientState { - MockClientState::new(Self::mock_header(height)) - } - - fn signer() -> Signer { - "cosmos1wxeyh7zgn4tctjzs0vtqpc6p5cxq5t2muzl7ng" - .parse() - .unwrap() - } - - pub fn counterparty(client_id: u64, connection_id: Option) -> Counterparty { - let client_id = Self::client_id(client_id); - let connection_id = connection_id.map(Self::connection_id); - let prefix = Self::commitment_prefix(); - Counterparty::new(client_id, connection_id, prefix) - } - - pub fn delay_period() -> Duration { - ZERO_DURATION - } - - pub fn commitment_prefix() -> CommitmentPrefix { - vec![0].try_into().unwrap() - } - - pub fn commitment_proof_bytes() -> CommitmentProofBytes { - vec![0].try_into().unwrap() - } - - 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: Height) -> 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 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() == chain.height; - - // check that clients match - let clients_match = chain.clients.into_iter().all(|(client_id, client)| { - // compute the highest consensus state in the model and check - // that it matches the client state - let client_state = ClientReader::client_state(ctx, &Self::client_id(client_id)); - let client_state_matches = match client.heights.iter().max() { - Some(max_height) => { - // if the model has consensus states (encoded simply as - // heights in the model), then the highest one should - // match the height in the client state - client_state.is_ok() && client_state.unwrap().latest_height() == *max_height - } - None => { - // if the model doesn't have any consensus states - // (heights), then the client state should not exist - client_state.is_err() - } - }; - - // check that each consensus state from the model exists - // TODO: check that no other consensus state exists (i.e. the - // 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), height) - .is_ok() - }); - - client_state_matches && consensus_states_match - }); - - // 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 Ok(connection_end) = - ctx.connection_end(&Self::connection_id(connection_id)) - { - // 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(Self::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 - }) - } - - pub fn apply(&mut self, action: Action) -> Result<(), relayer_error::Error> { - 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(MsgCreateClient { - client_state: Self::client_state(client_state).into(), - consensus_state: MockConsensusState::new(Self::mock_header(consensus_state)) - .into(), - signer: Self::signer(), - })); - ctx.deliver(msg) - } - 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(MsgUpdateClient { - client_id: Self::client_id(client_id), - header: Self::mock_header(header).into(), - signer: Self::signer(), - })); - ctx.deliver(msg) - } - Action::Ics07UpgradeClient { - 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::UpgradeClient(MsgUpgradeClient { - client_id: Self::client_id(client_id), - client_state: MockClientState::new(MockHeader::new(header)).into(), - consensus_state: MockConsensusState::new(MockHeader::new(header)).into(), - proof_upgrade_client: Default::default(), - proof_upgrade_consensus_state: Default::default(), - signer: Self::signer(), - })); - 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: Some(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: Self::client_state(client_state).into(), - 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: Self::client_state(client_state).into(), - 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::step_runner::StepRunner for IbcTestRunner { - fn initial_step(&mut self, step: Step) -> Result<(), String> { - 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); - } - Ok(()) - } - - fn next_step(&mut self, step: Step) -> Result<(), String> { - let show = step.action.clone(); - 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_ics02_error_kind(result), - client_error::ErrorDetail::ClientNotFound(_) - ), - ActionOutcome::Ics02ConsensusStateNotFound => matches!( - Self::extract_ics02_error_kind(result), - client_error::ErrorDetail::ConsensusStateNotFound(_) - ), - 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::ClientNotFound(_) - ), - ActionOutcome::Ics07HeaderVerificationFailure => { - matches!( - Self::extract_ics02_error_kind(result), - client_error::ErrorDetail::LowUpgradeHeight(_) - ) - } - ActionOutcome::Ics03ConnectionOpenInitOk => result.is_ok(), - ActionOutcome::Ics03ConnectionOpenTryOk => result.is_ok(), - ActionOutcome::Ics03InvalidConsensusHeight => matches!( - Self::extract_ics03_error_kind(result), - connection_error::ErrorDetail::InvalidConsensusHeight(_) - ), - ActionOutcome::Ics03ConnectionNotFound => matches!( - Self::extract_ics03_error_kind(result), - connection_error::ErrorDetail::ConnectionNotFound(_) - ), - ActionOutcome::Ics03ConnectionMismatch => matches!( - Self::extract_ics03_error_kind(result), - connection_error::ErrorDetail::ConnectionMismatch(_) - ), - ActionOutcome::Ics03InvalidProof => matches!( - Self::extract_ics03_error_kind(result), - connection_error::ErrorDetail::InvalidProof(_) - ), - ActionOutcome::Ics03ConnectionOpenAckOk => result.is_ok(), - ActionOutcome::Ics03ConnectionOpenConfirmOk => result.is_ok(), - }; - - // Validate chains - for ctx in self.contexts.values() { - ctx.validate()? - } - - if !outcome_matches { - return Err(format!("Action outcome did not match expected: {:?}", show)); - } - - if !self.check_chain_states(step.chains) { - return Err("Chain states do not match".into()); - } - - Ok(()) - } -} diff --git a/crates/ibc/tests/runner/step.rs b/crates/ibc/tests/runner/step.rs deleted file mode 100644 index df434e4c6..000000000 --- a/crates/ibc/tests/runner/step.rs +++ /dev/null @@ -1,192 +0,0 @@ -use alloc::collections::btree_map::BTreeMap as HashMap; -use core::fmt::Debug; -use ibc::core::ics03_connection::connection::State as ConnectionState; -use serde::{Deserialize, Deserializer}; - -use ibc::Height; - -#[derive(Debug, Clone, Deserialize)] -pub struct Step { - pub action: Action, - - #[serde(alias = "actionOutcome")] - pub action_outcome: ActionOutcome, - - pub chains: HashMap, -} - -#[derive(Debug, Clone, PartialEq, Eq, Deserialize)] -#[serde(tag = "type")] -pub enum Action { - None, - Ics02CreateClient { - #[serde(alias = "chainId")] - chain_id: String, - - #[serde(alias = "clientState")] - client_state: Height, - - #[serde(alias = "consensusState")] - consensus_state: Height, - }, - Ics02UpdateClient { - #[serde(alias = "chainId")] - chain_id: String, - - #[serde(alias = "clientId")] - client_id: u64, - - header: Height, - }, - Ics07UpgradeClient { - #[serde(alias = "chainId")] - chain_id: String, - - #[serde(alias = "clientId")] - client_id: u64, - - header: Height, - }, - 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_id")] - previous_connection_id: Option, - - #[serde(alias = "clientId")] - client_id: u64, - - #[serde(alias = "clientState")] - client_state: Height, - - #[serde(alias = "counterpartyChainId")] - counterparty_chain_id: String, - - #[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: Height, - - #[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: Height, - - #[serde(alias = "counterpartyChainId")] - counterparty_chain_id: String, - - #[serde(alias = "counterpartyConnectionId")] - counterparty_connection_id: u64, - }, -} - -#[derive(Debug, Clone, PartialEq, Eq, Deserialize)] -pub enum ActionOutcome { - None, - Ics02CreateOk, - Ics02UpdateOk, - Ics02ClientNotFound, - Ics02ConsensusStateNotFound, - Ics02HeaderVerificationFailure, - - Ics07UpgradeOk, - Ics07ClientNotFound, - Ics07HeaderVerificationFailure, - - Ics03ConnectionOpenInitOk, - Ics03ConnectionOpenTryOk, - Ics03InvalidConsensusHeight, - Ics03ConnectionNotFound, - Ics03ConnectionMismatch, - Ics03InvalidProof, - Ics03ConnectionOpenAckOk, - Ics03ConnectionOpenConfirmOk, -} - -#[derive(Debug, Clone, PartialEq, Eq, Deserialize)] -pub struct Chain { - pub height: Height, - - pub clients: HashMap, - - pub connections: HashMap, -} - -#[derive(Debug, Clone, PartialEq, Eq, Deserialize)] -pub struct Client { - pub heights: Vec, -} - -#[derive(Debug, Clone, PartialEq, Eq, 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/crates/ibc/tests/support/model_based/.gitignore b/crates/ibc/tests/support/model_based/.gitignore deleted file mode 100644 index 1bc316a16..000000000 --- a/crates/ibc/tests/support/model_based/.gitignore +++ /dev/null @@ -1,13 +0,0 @@ -# Files generated by TLC/Apalache. -*.out -states/ -x/ -detailed.log -bfs.csv -log0.smt -profile-rules.txt -counterexample.json -counterexample.tla - -# Files genereated by modelator. -IBCTests_* diff --git a/crates/ibc/tests/support/model_based/IBC.cfg b/crates/ibc/tests/support/model_based/IBC.cfg deleted file mode 100644 index 14a26f820..000000000 --- a/crates/ibc/tests/support/model_based/IBC.cfg +++ /dev/null @@ -1,13 +0,0 @@ -CONSTANTS - ChainIds = {"chainA", "chainB"} - MaxRevisionHeight = 4 - MaxRevisionNumber = 2 - MaxClientsPerChain = 1 - MaxConnectionsPerChain = 1 - -INIT Init -NEXT Next - -INVARIANTS - TypeOK - ModelNeverErrors diff --git a/crates/ibc/tests/support/model_based/IBC.tla b/crates/ibc/tests/support/model_based/IBC.tla deleted file mode 100644 index e89af5517..000000000 --- a/crates/ibc/tests/support/model_based/IBC.tla +++ /dev/null @@ -1,590 +0,0 @@ ---------------------------------- MODULE IBC ---------------------------------- - -EXTENDS ICS02, ICS03 - -CONSTANTS - \* ids of existing chains - \* @type: Set(CHAIN_ID); - ChainIds, - \* max height which chains can reach - \* @type: Int; - MaxRevisionHeight, - \* max revision which chains can reach - \* @type: Int; - MaxRevisionNumber, - \* max number of client to be created per chain - \* @type: Int; - MaxClientsPerChain, - \* max number of connections to be created per chain - \* @type: Int; - MaxConnectionsPerChain - -ASSUME MaxRevisionHeight >= 0 -ASSUME MaxRevisionNumber >= 0 -ASSUME MaxClientsPerChain >= 0 -ASSUME MaxConnectionsPerChain >= 0 - -VARIABLES - \* mapping from chain id to its data - \* @type: CHAINS; - chains, - \* last action performed - \* @type: ACTION; - action, - \* string with the outcome of the last operation - \* @type: Str; - actionOutcome - -vars == <> - -\* 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) -\* set of possible connection states -ConnectionStates == { - "Uninitialized", - "Init", - "TryOpen", - "Open" -} - -\* set of possible actions -NoneActions == [ - type: {"None"} -] - -CreateClientActions == [ - type: {"Ics02CreateClient"}, - chainId: ChainIds, - \* `clientState` contains simply a height - clientState: Heights, - \* `consensusState` contains simply a height - consensusState: Heights -] -UpdateClientActions == [ - type: {"Ics02UpdateClient"}, - chainId: ChainIds, - clientId: ClientIds, - \* `header` contains simply a height - header: Heights -] -UpgradeClientActions == [ - type: {"Ics07UpgradeClient"}, - chainId: ChainIds, - clientId: ClientIds, - \* `header` contains simply a height - header: Heights -] -ClientActions == - CreateClientActions \union - UpdateClientActions \union - UpgradeClientActions - -ConnectionOpenInitActions == [ - type: {"Ics03ConnectionOpenInit"}, - chainId: ChainIds, - clientId: ClientIds, - counterpartyChainId: ChainIds, - counterpartyClientId: ClientIds -] -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 -] -ConnectionOpenAckActions == [ - type: {"Ics03ConnectionOpenAck"}, - chainId: ChainIds, - connectionId: ConnectionIds, - \* `clientState` contains simply a height - clientState: Heights, - counterpartyChainId: ChainIds, - counterpartyConnectionId: ConnectionIds -] -ConnectionOpenConfirmActions == [ - type: {"Ics03ConnectionOpenConfirm"}, - chainId: ChainIds, - connectionId: ConnectionIds, - \* `clientState` contains simply a height - clientState: Heights, - counterpartyChainId: ChainIds, - counterpartyConnectionId: ConnectionIds -] -ConnectionActions == - ConnectionOpenInitActions \union - ConnectionOpenTryActions \union - ConnectionOpenAckActions \union - ConnectionOpenConfirmActions - -Actions == - NoneActions \union - ClientActions \union - ConnectionActions - -\* set of possible action outcomes -ActionOutcomes == { - "None", - "ModelError", - \* ICS02_CreateClient outcomes: - "Ics02CreateOk", - \* ICS02_UpdateClient outcomes: - "Ics02UpdateOk", - "Ics02ClientNotFound", - "Ics02HeaderVerificationFailure", - \* ICS07_UpgradeClient outcomes: - "Ics07UpgradeOk", - "Ics07ClientNotFound", - "Ics07HeaderVerificationFailure", - \* ICS03_ConnectionOpenInit outcomes: - "Ics03ConnectionOpenInitOk", - \* ICS03_ConnectionOpenTry outcomes: - "Ics03ConnectionOpenTryOk", - "Ics03InvalidConsensusHeight", - "Ics03ConnectionNotFound", - "Ics03ConnectionMismatch", - "Ics03InvalidProof", - \* ICS03_ConnectionOpenAck outcomes: - "Ics03ConnectionOpenAckOk", - \* 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 block height if outcome was ok -\* @type: (HEIGHT, [outcome: Str], Str) => HEIGHT; -UpdateRevisionHeight(height, result, okOutcome) == - IF result.outcome = okOutcome THEN - \* <> - [ revision_number |-> height.revision_number, revision_height |-> height.revision_height + 1 ] - ELSE - height - -\* update revision height if outcome was ok -\* @type: (HEIGHT, [outcome: Str], Str) => HEIGHT; -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 -\* @type: (Set(ACTION), [outcome: Str], Str) => Set(ACTION); -UpdateConnectionProofs(connectionProofs, result, okOutcome) == - IF result.outcome = okOutcome THEN - connectionProofs \union {result.action} - ELSE - connectionProofs - -CreateClient(chainId, height) == - LET chain == chains[chainId] IN - LET result == ICS02_CreateClient(chain, chainId, height) IN - \* update the chain - LET updatedChain == [chain EXCEPT - !.height = UpdateRevisionHeight(@, result, "Ics02CreateOk"), - !.clients = result.clients, - !.clientIdCounter = result.clientIdCounter - ] IN - \* update `chains`, set the `action` and its `actionOutcome` - /\ chains' = [chains EXCEPT ![chainId] = updatedChain] - /\ action' = result.action - /\ actionOutcome' = result.outcome - -UpdateClient(chainId, clientId, height) == - LET chain == chains[chainId] IN - LET result == ICS02_UpdateClient(chain, chainId, clientId, height) IN - \* update the chain - LET updatedChain == [chain EXCEPT - !.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` - /\ chains' = [chains EXCEPT ![chainId] = updatedChain] - /\ action' = result.action - /\ actionOutcome' = result.outcome - -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 = UpdateRevisionHeight(@, 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 = UpdateRevisionHeight(@, 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 = UpdateRevisionHeight(@, 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 = UpdateRevisionHeight(@, 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 height \in Heights: - \* only create client if the model constant `MaxClientsPerChain` allows - \* it - LET allowed == chains[chainId].clientIdCounter < MaxClientsPerChain IN - IF allowed THEN - CreateClient(chainId, height) - ELSE - UNCHANGED vars - -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 - \* 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 - \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 - \* 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 - \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 - \* 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 - \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 - \* 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 - \E counterpartyConnectionId \in ConnectionIds: - IF chainId /= counterpartyChainId THEN - ConnectionOpenConfirm( - chainId, - connectionId, - height, - counterpartyChainId, - counterpartyConnectionId - ) - ELSE - UNCHANGED vars - -Init == - \* create a client and a connection with none values - LET - \* @type: CLIENT; - clientNone == [ - heights |-> {} - ] IN - LET - \* @type: CONNECTION; - connectionNone == [ - state |-> "Uninitialized", - chainId |-> ChainIdNone, - clientId |-> ClientIdNone, - connectionId |-> ConnectionIdNone, - counterpartyChainId |-> ChainIdNone, - counterpartyClientId |-> ClientIdNone, - counterpartyConnectionId |-> ConnectionIdNone - ] IN - \* create an empty chain - LET - \* @type: CHAIN; - emptyChain == [ - height |-> [ revision_number |-> 1, revision_height |-> 1 ], - clients |-> [clientId \in ClientIds |-> clientNone], - clientIdCounter |-> 0, - connections |-> [connectionId \in ConnectionIds |-> connectionNone], - connectionIdCounter |-> 0, - connectionProofs |-> {} - ] IN - /\ chains = [chainId \in ChainIds |-> emptyChain] - /\ action = [type |-> "None"] - /\ actionOutcome = "None" - -Next == - \* select a chain id - \E chainId \in ChainIds: - \* perform action on chain if the model constant `MaxChainHeight` allows - \* it - \* 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) - \/ ConnectionOpenConfirmAction(chainId) - \/ UNCHANGED vars - ELSE - \/ UNCHANGED vars - -(******************************** Invariants *********************************) - -TypeOK == - /\ chains \in Chains - /\ action \in Actions - /\ actionOutcome \in ActionOutcomes - -\* the model never erros -ModelNeverErrors == - actionOutcome /= "ModelError" - -=============================================================================== diff --git a/crates/ibc/tests/support/model_based/IBCDefinitions.tla b/crates/ibc/tests/support/model_based/IBCDefinitions.tla deleted file mode 100644 index a98dfbe82..000000000 --- a/crates/ibc/tests/support/model_based/IBCDefinitions.tla +++ /dev/null @@ -1,89 +0,0 @@ ---------------------------- MODULE IBCDefinitions ----------------------------- - -EXTENDS Integers, FiniteSets, TLC - -(********************** TYPE ANNOTATIONS FOR APALACHE ************************) - -\* @typeAlias: CHAIN_ID = Str; -\* @typeAlias: CLIENT_ID = Int; -\* @typeAlias: CONNECTION_ID = Int; -\* @typeAlias: HEIGHT = [ revision_number: Int, revision_height: Int ]; -\* @typeAlias: CLIENT = [ heights: Set(HEIGHT) ]; -\* @typeAlias: CLIENTS = CLIENT_ID -> CLIENT; -\* -\* @typeAlias: CONNECTION = [ state: Str, chainId: CHAIN_ID, clientId: CLIENT_ID, -\* connectionId: CONNECTION_ID, counterpartyChainId: CHAIN_ID, -\* counterpartyClientId: CLIENT_ID, counterpartyConnectionId: CONNECTION_ID ]; -\* @typeAlias: CONNECTIONS = CONNECTION_ID -> CONNECTION; -\* -\* @typeAlias: ACTION = [ type: Str, chainId: CHAIN_ID, clientState: HEIGHT, consensusState: HEIGHT, -\* clientId: CLIENT_ID, header: HEIGHT, previousConnectionId: Int, counterpartyChainId: CHAIN_ID, -\* counterpartyClientId: CLIENT_ID, counterpartyConnectionId: Int]; -\* -\* @typeAlias: CHAIN = [ height: HEIGHT, clients: CLIENTS, clientIdCounter: Int, -\* connections: CONNECTIONS, connectionIdCounter: Int, connectionProofs: Set(ACTION) ]; -\* @typeAlias: CHAINS = CHAIN_ID -> CHAIN; -\* -Typedefs == TRUE - - - -(******************* 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. -\* @type: (HEIGHT, HEIGHT) => Bool; -HeightLT(a, b) == - \/ a.revision_number < b.revision_number - \/ (a.revision_number = b.revision_number /\ a.revision_height < b.revision_height) - -\* @type: (HEIGHT, HEIGHT) => Bool; -HeightLTE(a, b) == - \/ a.revision_number < b.revision_number - \/ (a.revision_number = b.revision_number /\ a.revision_height < b.revision_height) - \/ a = b - -\* @type: (HEIGHT, HEIGHT) => Bool; -HeightGT(a, b) == - \/ a.revision_number > b.revision_number - \/ (a.revision_number = b.revision_number /\ a.revision_height > b.revision_height) - -\* @type: (HEIGHT, HEIGHT) => Bool; -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 -\* @type: (HEIGHT, HEIGHT) => Bool; -HigherRevisionHeight(a, b) == - /\ a.revision_number = b.revision_number - /\ a.revision_height > b.revision_height - -\* Checks if the revision is higher -\* @type: (HEIGHT, HEIGHT) => Bool; -HigherRevisionNumber(a, b) == - /\ a.revision_number > b.revision_number - -Max(S) == CHOOSE x \in S: \A y \in S: y <= x - -\* @type: (Set(HEIGHT)) => HEIGHT; -FindMaxHeight(S) == CHOOSE x \in S: \A y \in S: HeightLTE(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 connection identifier is not set then it is -1 -ConnectionIdNone == -1 - -=============================================================================== diff --git a/crates/ibc/tests/support/model_based/IBCTests.cfg b/crates/ibc/tests/support/model_based/IBCTests.cfg deleted file mode 100644 index 6a34c0466..000000000 --- a/crates/ibc/tests/support/model_based/IBCTests.cfg +++ /dev/null @@ -1,9 +0,0 @@ -CONSTANTS - ChainIds = {"chainA", "chainB"} - MaxRevisionHeight = 4 - MaxRevisionNumber = 2 - MaxClientsPerChain = 1 - MaxConnectionsPerChain = 1 - -INIT Init -NEXT Next diff --git a/crates/ibc/tests/support/model_based/IBCTests.tla b/crates/ibc/tests/support/model_based/IBCTests.tla deleted file mode 100644 index cc26338ca..000000000 --- a/crates/ibc/tests/support/model_based/IBCTests.tla +++ /dev/null @@ -1,60 +0,0 @@ ------------------------------- MODULE IBCTests -------------------------------- - -EXTENDS IBC - -\* ICS02CreateClient tests -ICS02CreateOKTest == - /\ actionOutcome = "Ics02CreateOk" - -\* ICS02UpdateClient tests -ICS02UpdateOKTest == - /\ actionOutcome = "Ics02UpdateOk" - -ICS02ClientNotFoundTest == - /\ actionOutcome = "Ics02ClientNotFound" - -ICS02HeaderVerificationFailureTest == - /\ actionOutcome = "Ics02HeaderVerificationFailure" - -\* ICS07UpgradeClient tests -ICS07UpgradeOkTest == - /\ actionOutcome = "Ics07UpgradeOk" - -ICS07ClientNotFoundTest == - /\ actionOutcome = "Ics07ClientNotFound" - -ICS07HeaderVerificationFailureTest == - /\ actionOutcome = "Ics07HeaderVerificationFailure" - - -\* ICS03ConnectionOpenInit tests -ICS03ConnectionOpenInitOKTest == - /\ actionOutcome = "Ics03ConnectionOpenInitOk" - -\* ICS03ConnectionOpenTry tests -ICS03ConnectionOpenTryOKTest == - /\ actionOutcome = "Ics03ConnectionOpenTryOk" - -ICS03InvalidConsensusHeightTest == - /\ actionOutcome = "Ics03InvalidConsensusHeight" - -ICS03ConnectionNotFoundTest == - /\ actionOutcome = "Ics03ConnectionNotFound" - -ICS03ConnectionMismatchTest == - /\ actionOutcome = "Ics03ConnectionMismatch" - -\* TODO: the following test should fail but doesn't because proofs are not yet -\* verified in the implementation -\* Test is replaced with to avoid triggering Modelator -\* ICS03InvalidProof == -\* /\ actionOutcome = "Ics03InvalidProof" - -\* ICS03ConnectionOpenAck tests -ICS03ConnectionOpenAckOKTest == - /\ actionOutcome = "Ics03ConnectionOpenAckOk" - -\* ICS03ConnectionOpenConfirm tests -ICS03ConnectionOpenConfirmOKTest == - /\ actionOutcome = "Ics03ConnectionOpenConfirmOk" -=============================================================================== diff --git a/crates/ibc/tests/support/model_based/ICS02.tla b/crates/ibc/tests/support/model_based/ICS02.tla deleted file mode 100644 index 0e5430e3b..000000000 --- a/crates/ibc/tests/support/model_based/ICS02.tla +++ /dev/null @@ -1,147 +0,0 @@ -------------------------------- MODULE ICS02 ---------------------------------- - -EXTENDS IBCDefinitions - -\* retrieves `clientId`'s data -\* @type: (CLIENTS, CLIENT_ID) => CLIENT; -ICS02_GetClient(clients, clientId) == - clients[clientId] - -\* check if `clientId` exists -\* @type: (CLIENTS, CLIENT_ID) => Bool; -ICS02_ClientExists(clients, clientId) == - ICS02_GetClient(clients, clientId).heights /= {} - -\* update `clientId`'s data -\* @type: (CLIENTS, CLIENT_ID, CLIENT) => CLIENTS; -ICS02_SetClient(clients, clientId, client) == - [clients EXCEPT ![clientId] = client] - -\* @type: (CHAIN, CHAIN_ID, HEIGHT) => [clients: CLIENTS, clientIdCounter: Int, action: ACTION, outcome: Str]; -ICS02_CreateClient(chain, chainId, height) == - \* TODO: rename `action_` to `action` once the following issue is fixed: - \* https://github.com/informalsystems/apalache/issues/593 - LET action_ == [ - type |-> "Ics02CreateClient", - chainId |-> chainId, - clientState |-> height, - consensusState |-> height - ] IN - \* check if the client exists (it shouldn't) - 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 |-> chain.clients, - clientIdCounter |-> chain.clientIdCounter, - action |-> action_, - outcome |-> "ModelError" - ] - ELSE - \* if it doesn't, create it - LET client == [ - heights|-> {height} - ] IN - \* return result with updated state - [ - clients |-> ICS02_SetClient( - chain.clients, - chain.clientIdCounter, - client - ), - clientIdCounter |-> chain.clientIdCounter + 1, - action |-> action_, - outcome |-> "Ics02CreateOk" - ] - -\* @type: (CHAIN, CHAIN_ID, CLIENT_ID, HEIGHT) => [clients: CLIENTS, action: ACTION, outcome: Str]; -ICS02_UpdateClient(chain, chainId, clientId, height) == - LET action_ == [ - type |-> "Ics02UpdateClient", - 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 |-> "Ics02ClientNotFound" - ] - ELSE - \* if the client exists, check its height - LET client == ICS02_GetClient(chain.clients, clientId) IN - 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_, - outcome |-> "Ics02HeaderVerificationFailure" - ] - 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 |-> "Ics02UpdateOk" - ] - -\* @type: (CHAIN, CHAIN_ID, CLIENT_ID, HEIGHT) => [clients: CLIENTS, action: ACTION, outcome: Str]; -ICS07_UpgradeClient(chain, chainId, clientId, height) == - LET action_ == [ - 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/crates/ibc/tests/support/model_based/ICS03.tla b/crates/ibc/tests/support/model_based/ICS03.tla deleted file mode 100644 index 620d3fdd7..000000000 --- a/crates/ibc/tests/support/model_based/ICS03.tla +++ /dev/null @@ -1,438 +0,0 @@ ------------------------------- MODULE ICS03 ----------------------------------- - -EXTENDS ICS02 - -\* retrieves `connectionId`'s data -\* @type: (CONNECTIONS, CONNECTION_ID) => CONNECTION; -ICS03_GetConnection(connections, connectionId) == - connections[connectionId] - -\* check if `connectionId` exists -\* @type: (CONNECTIONS, CONNECTION_ID) => Bool; -ICS03_ConnectionExists(connections, connectionId) == - ICS03_GetConnection(connections, connectionId).state /= "Uninitialized" - -\* update `connectionId`'s data -\* @type: (CONNECTIONS, CONNECTION_ID, CONNECTION) => CONNECTIONS; -ICS03_SetConnection(connections, connectionId, connection) == - [connections EXCEPT ![connectionId] = connection] - -\* @type: (CHAIN, CHAIN_ID, CLIENT_ID, CHAIN_ID, CLIENT_ID) -\* => [connections: CONNECTIONS, connectionIdCounter: Int, action: ACTION, outcome: Str]; -ICS03_ConnectionOpenInit( - chain, - chainId, - clientId, - counterpartyChainId, - counterpartyClientId -) == - LET action_ == [ - 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 |-> "Ics02ClientNotFound" - ] - 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" - ] - -\* @type: (CHAIN, CHAIN_ID, CLIENT_ID, CONNECTION_ID, HEIGHT, CHAIN_ID, CLIENT_ID, CONNECTION_ID) -\* => [connections: CONNECTIONS, connectionIdCounter: Int, action: ACTION, outcome: Str]; -ICS03_ConnectionOpenTry( - chain, - chainId, - clientId, - previousConnectionId, - height, - counterpartyChainId, - counterpartyClientId, - counterpartyConnectionId -) == - LET action_ == [ - 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 HeightGT(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 |-> "Ics02ClientNotFound" - ] - 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 |-> "Ics02ConsensusStateNotFound" - ] - 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" - ] - -\* @type: (CHAIN, CHAIN_ID, CONNECTION_ID, HEIGHT, CHAIN_ID, CONNECTION_ID) -\* => [connections: CONNECTIONS, action: ACTION, outcome: Str]; -ICS03_ConnectionOpenAck( - chain, - chainId, - connectionId, - height, - counterpartyChainId, - counterpartyConnectionId -) == - LET action_ == [ - 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 HeightGT(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 - [ - connections |-> connections, - action |-> action_, - outcome |-> "Ics03ConnectionNotFound" - ] - 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 |-> "Ics02ConsensusStateNotFound" - ] - 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", - !.counterpartyConnectionId = counterpartyConnectionId - ] IN - \* return result with updated state - [ - connections |-> ICS03_SetConnection( - connections, - connectionId, - updatedConnection - ), - action |-> action_, - outcome |-> "Ics03ConnectionOpenAckOk" - ] - -\* @type: (CHAIN, CHAIN_ID, CONNECTION_ID, HEIGHT, CHAIN_ID, CONNECTION_ID) -\* => [connections: CONNECTIONS, action: ACTION, outcome: Str]; -ICS03_ConnectionOpenConfirm( - chain, - chainId, - connectionId, - height, - counterpartyChainId, - counterpartyConnectionId -) == - LET action_ == [ - 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 - [ - connections |-> connections, - action |-> action_, - outcome |-> "Ics03ConnectionNotFound" - ] - 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 |-> "Ics02ConsensusStateNotFound" - ] - 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" - ] - -===============================================================================