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 47 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
1 change: 1 addition & 0 deletions modules/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -54,5 +54,6 @@ version = "=0.18.0"
optional = true

[dev-dependencies]
eyre = "0.6.5"
tokio = { version = "1.0", features = ["macros"] }
tendermint-testgen = { version = "=0.18.0" } # Needed for generating (synthetic) light blocks.
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
266 changes: 266 additions & 0 deletions modules/tests/model_based.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,266 @@
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<String, MockContext>,
vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
}

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 max_history_size = 1;
let ctx = MockContext::new(
ChainId::new(chain_id.clone(), Self::epoch()),
HostType::Mock,
max_history_size,
Height::new(Self::epoch(), 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(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(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()
}

// TODO: this is sometimes called version/revision number but seems
vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
// unrelated with the `Version` type; is that so?
fn epoch() -> 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::epoch(), 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 path = 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_driver(executor, path) {
panic!("{:?}", e);
}
}
}
49 changes: 49 additions & 0 deletions modules/tests/modelator.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
use eyre::{eyre, Context, Result};
adizere marked this conversation as resolved.
Show resolved Hide resolved
use serde::de::DeserializeOwned;
use std::fmt::Debug;
use std::fs::File;
use std::io::BufReader;
use std::path::Path;

pub trait TestExecutor<S> {
fn initial_step(&mut self, step: S) -> bool;
fn next_step(&mut self, step: S) -> bool;
}

pub fn test_driver<Executor, Step, P>(mut executor: Executor, path: P) -> Result<()>
where
Executor: TestExecutor<Step> + Debug,
Step: DeserializeOwned + Debug + Clone,
P: AsRef<Path>,
{
// open test file
let file = File::open(path.as_ref())
.wrap_err_with(|| format!("test {:?} not found.", path.as_ref()))?;
let reader = BufReader::new(file);

// parse test file
let steps: Vec<Step> = serde_json::de::from_reader(reader)
.wrap_err_with(|| format!("test {:?} could not be deserialized", path.as_ref()))?;
let step_count = steps.len();

for (i, step) in steps.into_iter().enumerate() {
// check the step
let ok = if i == 0 {
executor.initial_step(step.clone())
} else {
executor.next_step(step.clone())
};

if !ok {
return Err(eyre!(
vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
"test {:?} failed on step {}/{}:\n{:#?}\n\nexecutor:\n{:#?}",
path.as_ref(),
i + 1,
step_count,
step,
executor
));
}
}
Ok(())
}
49 changes: 49 additions & 0 deletions modules/tests/step.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
use serde::Deserialize;
use std::collections::HashMap;
use std::fmt::Debug;

#[derive(Debug, Clone, Deserialize)]
pub struct Step {
pub action: Action,

#[serde(alias = "actionOutcome")]
pub action_outcome: ActionOutcome,

pub chains: HashMap<String, Chain>,
}

#[derive(Debug, Clone, Deserialize)]
pub struct Action {
#[serde(alias = "type")]
pub action_type: ActionType,

#[serde(alias = "chainId")]
pub chain_id: Option<String>,

#[serde(alias = "clientId")]
pub client_id: Option<u64>,

#[serde(alias = "clientHeight")]
pub client_height: Option<u64>,
}

vitorenesduarte marked this conversation as resolved.
Show resolved Hide resolved
#[derive(Debug, Clone, PartialEq, Deserialize)]
pub enum ActionType {
None,
ICS02CreateClient,
ICS02UpdateClient,
}

#[derive(Debug, Clone, PartialEq, Deserialize)]
pub enum ActionOutcome {
None,
ICS02CreateOK,
ICS02UpdateOK,
ICS02ClientNotFound,
ICS02HeaderVerificationFailure,
}

#[derive(Debug, Clone, PartialEq, Deserialize)]
pub struct Chain {
pub height: u64,
}
9 changes: 9 additions & 0 deletions modules/tests/support/model_based/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
*.out
states/
x/
detailed.log
bfs.csv
log0.smt
profile-rules.txt
counterexample.json
counterexample.tla
Loading