Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Model-based tests for ICS02 #601

Merged
merged 57 commits into from
Feb 12, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
57 commits
Select commit Hold shift + click to select a range
413d3f4
Add ICS02 model
vitorenesduarte Feb 2, 2021
065631e
Add MBT test driver
vitorenesduarte Feb 2, 2021
b98c7d3
Add ICS02TestExecutor
vitorenesduarte Feb 2, 2021
6685cc1
Add another apalache counterexample
vitorenesduarte Feb 2, 2021
f863486
Fix ICS02.tla: client counter starts at 0
vitorenesduarte Feb 2, 2021
cd0d0a6
Check for errors in MockContext.deliver
vitorenesduarte Feb 2, 2021
02c020b
Handle errors in MBT tests
vitorenesduarte Feb 2, 2021
a5d06c5
Remove SyntheticTendermint mock context
vitorenesduarte Feb 2, 2021
356c6d2
More idiomatic check_next_state
vitorenesduarte Feb 2, 2021
6ab8611
Buffered file reads
vitorenesduarte Feb 3, 2021
490d77b
Make extract_handler_error_kind generic over the IBC handler
vitorenesduarte Feb 3, 2021
92b843c
Support multiple chains in MBT
vitorenesduarte Feb 3, 2021
d57cf41
Make eyre a dev-dependency
vitorenesduarte Feb 3, 2021
f4dbe00
s/ICS0/IBC on TLA files
vitorenesduarte Feb 3, 2021
20867a5
Initial support for conn open init
vitorenesduarte Feb 3, 2021
e5e2f7b
Start connection and channel identifiers at 0
vitorenesduarte Feb 3, 2021
b9ca90a
Add conn open init to TLA spec
vitorenesduarte Feb 3, 2021
f3cd434
Represent clients with a record in TLA spec
vitorenesduarte Feb 3, 2021
4167d29
Finish connection open init
vitorenesduarte Feb 3, 2021
7755fec
s/state/step
vitorenesduarte Feb 3, 2021
70e70f6
Minimize diff
vitorenesduarte Feb 4, 2021
44747d3
Merge branch 'master' into vitor/ics02_mbt
vitorenesduarte Feb 4, 2021
41d34d3
Modularize TLA spec
vitorenesduarte Feb 4, 2021
1f9881c
TLA format convention
vitorenesduarte Feb 4, 2021
e2605bb
s/Null/None
vitorenesduarte Feb 4, 2021
5b98a7e
Sketch conn open try; Model chain's height
vitorenesduarte Feb 4, 2021
244efa6
Bound model space
vitorenesduarte Feb 4, 2021
7d9202a
Only update chain height upon success
vitorenesduarte Feb 4, 2021
28879f0
Check that chain heights match the ones in the model
vitorenesduarte Feb 4, 2021
a870537
Sketch conn open try
vitorenesduarte Feb 4, 2021
a533def
Sketch conn open try
vitorenesduarte Feb 4, 2021
1cdb02a
Model missing connections and connection mismatches in conn open try
vitorenesduarte Feb 4, 2021
0186a1c
Trigger bug in conn open try
vitorenesduarte Feb 4, 2021
f777144
Merge branch 'master' into vitor/ics02_mbt
vitorenesduarte Feb 4, 2021
6b6cd43
Go back to previous way of generating connection and channel ids
vitorenesduarte Feb 4, 2021
6186bec
Disable failing MBT test
vitorenesduarte Feb 4, 2021
a7b50d7
Fix panic in conn open try when no connection id is provided
vitorenesduarte Feb 5, 2021
5b66aac
ICS02TestExecutor -> IBCTestExecutor
vitorenesduarte Feb 5, 2021
095433e
Merge branch 'vitor/conn_open_try' into vitor/ics02_mbt
vitorenesduarte Feb 5, 2021
f2194cf
Failing MBT test now passes with #615
vitorenesduarte Feb 5, 2021
7bdd3b6
Add notes on MBT
vitorenesduarte Feb 8, 2021
9ee48bd
Remove ICS02
vitorenesduarte Feb 8, 2021
035651e
Add README
vitorenesduarte Feb 8, 2021
b6854ce
Improve README
vitorenesduarte Feb 8, 2021
cd484a6
Remove MBT intro
vitorenesduarte Feb 8, 2021
d69d15e
new lines
vitorenesduarte Feb 8, 2021
b4aea95
Merge branch 'master' into vitor/ics02_mbt
vitorenesduarte Feb 9, 2021
5e9dd63
Make MBT README more easily discoverable
vitorenesduarte Feb 9, 2021
fb20ce0
IBCTestExecutor: Map from ChainId (instead of String) to MockContext
vitorenesduarte Feb 9, 2021
75db6bb
s/epoch/revision
vitorenesduarte Feb 9, 2021
a102863
Move from eyre to thiserror
vitorenesduarte Feb 9, 2021
2e5d6de
Improve README
vitorenesduarte Feb 9, 2021
dfb683d
Improve README
vitorenesduarte Feb 9, 2021
7e24841
Improve arguments order in modelator::test
vitorenesduarte Feb 9, 2021
5d6bf08
Improve chain identifiers
vitorenesduarte Feb 10, 2021
60e4aba
Improve README
vitorenesduarte Feb 10, 2021
3a991e7
Merge branch 'master' into vitor/ics02_mbt
vitorenesduarte Feb 11, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions modules/src/ics02_client/msgs/create_client.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@ pub const TYPE_URL: &str = "/ibc.core.client.v1.MsgCreateClient";
/// A type of message that triggers the creation of a new on-chain (IBC) client.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct MsgCreateAnyClient {
client_state: AnyClientState,
consensus_state: AnyConsensusState,
signer: AccountId,
pub client_state: AnyClientState,
vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
pub consensus_state: AnyConsensusState,
pub signer: AccountId,
}

impl MsgCreateAnyClient {
Expand Down
63 changes: 63 additions & 0 deletions modules/tests/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
## 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
- `MaxClientsPerChain = 1`, indicating that at most 1 client per chain will be created
- `MaxClientHeight = 2`, indicating that clients will reach at most height 2

The [IBC.cfg](support/model_based/IBC.cfg) file also defines two simple invariants:
```tla
INVARIANTS
TypeOK
ModelNeverErrors
```

Then, we can ask [`Apalache`](https://apalache.informal.systems), a model checker for `TLA+`, to check that these invariants hold:
```bash
apalache-mc check --inv=ICS02UpdateOKTestNeg IBC.tla
```

The above command automatically reads what we have defined in [IBC.cfg](support/model_based/IBC.cfg).

### The tests

Tests are `TLA+` assertions that describe the desired shape of the test (see [IBCTests.tla](support/model_based/IBCTests.tla)). One of the assertions in [IBCTests.tla](support/model_based/IBCTests.tla) is the following:

```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 `Apalache`, to prove it:

```bash
apalache-mc check --inv=ICS02UpdateOKTestNeg IBCTests.tla
```

(Again, the above command automatically reads what we have defined in [IBCTests.cfg](support/model_based/IBCTests.cfg).)

Because the invariant is wrong, `Apalache` will find a counterexample showing that it is indeed possible that a client is sucessfully updated to a new height. This counterexample is our test.

### Current limitations

The counterexamples currently produced by `Apalache` are not easy to parse and have traditionally required tools like [`jsonatr`](https://github.com/informalsystems/jsonatr). Fortunately, [that will change soon](https://github.com/informalsystems/apalache/issues/530), and `Apalache` will be able to produce counterexamples like those in [support/model_based/tests/](support/model_based/tests/).
These are currently generated manually, but can be easily mapped to Rust (see [step.rs](step.rs)).

### Running the model-based tests

The model-based tests can be run with the following command:

```bash
cargo test -p ibc --features mocks -- model_based
```
269 changes: 269 additions & 0 deletions modules/tests/model_based.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,269 @@
mod modelator;
mod step;

use ibc::ics02_client::client_def::{AnyClientState, AnyConsensusState, AnyHeader};
use ibc::ics02_client::client_type::ClientType;
use ibc::ics02_client::error::Kind as ICS02ErrorKind;
use ibc::ics02_client::msgs::create_client::MsgCreateAnyClient;
use ibc::ics02_client::msgs::update_client::MsgUpdateAnyClient;
use ibc::ics02_client::msgs::ClientMsg;
use ibc::ics18_relayer::context::ICS18Context;
use ibc::ics18_relayer::error::{Error as ICS18Error, Kind as ICS18ErrorKind};
use ibc::ics24_host::identifier::{ChainId, ClientId};
use ibc::ics26_routing::error::{Error as ICS26Error, Kind as ICS26ErrorKind};
use ibc::ics26_routing::msgs::ICS26Envelope;
use ibc::mock::client_state::{MockClientState, MockConsensusState};
use ibc::mock::context::MockContext;
use ibc::mock::header::MockHeader;
use ibc::mock::host::HostType;
use ibc::Height;
use std::collections::HashMap;
use std::error::Error;
use std::fmt::{Debug, Display};
use step::{ActionOutcome, ActionType, Chain, Step};
use tendermint::account::Id as AccountId;

#[derive(Debug)]
struct IBCTestExecutor {
// mapping from chain identifier to its context
contexts: HashMap<ChainId, MockContext>,
}

impl IBCTestExecutor {
fn new() -> Self {
Self {
contexts: Default::default(),
}
}

/// Create a `MockContext` for a given `chain_id`.
/// Panic if a context for `chain_id` already exists.
fn init_chain_context(&mut self, chain_id: String, initial_height: u64) {
let chain_id = Self::chain_id(chain_id);
let max_history_size = 1;
let ctx = MockContext::new(
chain_id.clone(),
HostType::Mock,
max_history_size,
Height::new(Self::revision(), initial_height),
);
assert!(self.contexts.insert(chain_id, ctx).is_none());
}

/// Returns a reference to the `MockContext` of a given `chain_id`.
/// Panic if the context for `chain_id` is not found.
fn chain_context(&self, chain_id: String) -> &MockContext {
self.contexts
.get(&Self::chain_id(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.
fn chain_context_mut(&mut self, chain_id: String) -> &mut MockContext {
self.contexts
.get_mut(&Self::chain_id(chain_id))
.expect("chain context should have been initialized")
}

fn extract_handler_error_kind<K>(ics18_result: Result<(), ICS18Error>) -> K
where
K: Clone + Debug + Display + Into<anomaly::BoxError> + 'static,
{
let ics18_error = ics18_result.expect_err("ICS18 error expected");
assert!(matches!(
ics18_error.kind(),
ICS18ErrorKind::TransactionFailed
));
let ics26_error = ics18_error
.source()
.expect("expected source in ICS18 error")
.downcast_ref::<ICS26Error>()
.expect("ICS18 source should be an ICS26 error");
assert!(matches!(
ics26_error.kind(),
ICS26ErrorKind::HandlerRaisedError,
));
ics26_error
.source()
.expect("expected source in ICS26 error")
.downcast_ref::<anomaly::Error<K>>()
.expect("ICS26 source should be an handler error")
.kind()
.clone()
}

fn chain_id(chain_id: String) -> ChainId {
ChainId::new(chain_id, Self::revision())
}

fn revision() -> u64 {
0
}

fn client_id(client_id: u64) -> ClientId {
ClientId::new(ClientType::Mock, client_id)
.expect("it should be possible to create the client identifier")
}

fn height(height: u64) -> Height {
Height::new(Self::revision(), height)
}

fn mock_header(height: u64) -> MockHeader {
MockHeader(Self::height(height))
}

fn header(height: u64) -> AnyHeader {
AnyHeader::Mock(Self::mock_header(height))
}

fn client_state(height: u64) -> AnyClientState {
AnyClientState::Mock(MockClientState(Self::mock_header(height)))
}

fn consensus_state(height: u64) -> AnyConsensusState {
AnyConsensusState::Mock(MockConsensusState(Self::mock_header(height)))
}

fn signer() -> AccountId {
AccountId::new([0; 20])
}

/// Check that chain heights match the ones in the model.
fn check_chain_heights(&self, chains: HashMap<String, Chain>) -> bool {
chains.into_iter().all(|(chain_id, chain)| {
let ctx = self.chain_context(chain_id);
ctx.query_latest_height() == Self::height(chain.height)
})
}
}

impl modelator::TestExecutor<Step> for IBCTestExecutor {
fn initial_step(&mut self, step: Step) -> bool {
assert_eq!(
step.action.action_type,
ActionType::None,
"unexpected action type"
);
assert_eq!(
step.action_outcome,
ActionOutcome::None,
"unexpected action outcome"
);
// initiliaze all chains
for (chain_id, chain) in step.chains {
self.init_chain_context(chain_id, chain.height);
}
true
}

fn next_step(&mut self, step: Step) -> bool {
let outcome_matches = match step.action.action_type {
ActionType::None => panic!("unexpected action type"),
ActionType::ICS02CreateClient => {
// get action parameters
let chain_id = step
.action
.chain_id
.expect("create client action should have a chain identifier");
let client_height = step
.action
.client_height
.expect("create client action should have a client height");

// get chain's context
let ctx = self.chain_context_mut(chain_id);

// create ICS26 message and deliver it
let msg = ICS26Envelope::ICS2Msg(ClientMsg::CreateClient(MsgCreateAnyClient {
client_state: Self::client_state(client_height),
consensus_state: Self::consensus_state(client_height),
signer: Self::signer(),
}));
let result = ctx.deliver(msg);

// check the expected outcome: client create always succeeds
match step.action_outcome {
ActionOutcome::ICS02CreateOK => {
// the implementaion matches the model if no error occurs
result.is_ok()
vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
}
action => panic!("unexpected action outcome {:?}", action),
}
}
ActionType::ICS02UpdateClient => {
// get action parameters
let chain_id = step
.action
.chain_id
.expect("update client action should have a chain identifier");
let client_id = step
.action
.client_id
.expect("update client action should have a client identifier");
let client_height = step
.action
.client_height
.expect("update client action should have a client height");

// get chain's context
let ctx = self.chain_context_mut(chain_id);

// create ICS26 message and deliver it
let msg = ICS26Envelope::ICS2Msg(ClientMsg::UpdateClient(MsgUpdateAnyClient {
client_id: Self::client_id(client_id),
header: Self::header(client_height),
signer: Self::signer(),
}));
let result = ctx.deliver(msg);

// check the expected outcome
match step.action_outcome {
ActionOutcome::ICS02UpdateOK => {
// the implementaion matches the model if no error occurs
result.is_ok()
vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
}
ActionOutcome::ICS02ClientNotFound => {
let handler_error_kind =
Self::extract_handler_error_kind::<ICS02ErrorKind>(result);
// the implementaion matches the model if there's an
// error matching the expected outcome
matches!(
handler_error_kind,
ICS02ErrorKind::ClientNotFound(error_client_id)
if error_client_id == Self::client_id(client_id)
)
}
ActionOutcome::ICS02HeaderVerificationFailure => {
let handler_error_kind =
Self::extract_handler_error_kind::<ICS02ErrorKind>(result);
// the implementaion matches the model if there's an
// error matching the expected outcome
handler_error_kind == ICS02ErrorKind::HeaderVerificationFailure
vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
}
action => panic!("unexpected action outcome {:?}", action),
}
}
};
// also check that chain heights match
outcome_matches && self.check_chain_heights(step.chains)
}
}

const TESTS_DIR: &str = "tests/support/model_based/tests";

#[test]
fn model_based() {
let tests = vec!["ICS02UpdateOKTest", "ICS02HeaderVerificationFailureTest"];

for test in tests {
let test = format!("{}/{}.json", TESTS_DIR, test);
let executor = IBCTestExecutor::new();
// we should be able to just return the `Result` once the following issue
// is fixed: https://github.com/rust-lang/rust/issues/43301
if let Err(e) = modelator::test(&test, executor) {
panic!("{:?}", e);
}
}
}
Loading