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

Enable MBT on master #686

Merged
merged 6 commits into from
Nov 19, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
27 changes: 22 additions & 5 deletions light-client/tests/model_based.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ use serde::{Deserialize, Serialize};
use std::convert::TryFrom;
use std::str::FromStr;
use std::time::Duration;
use tendermint::validator::Set;
use tendermint_light_client::components::verifier::Verdict;
use tendermint_light_client::types::ValidatorSet;
use tendermint_light_client::{
Expand Down Expand Up @@ -446,18 +447,33 @@ fn single_step_test(
let trusting_period: Duration = tc.initial.trusting_period.into();
for (i, input) in tc.input.iter().enumerate() {
output_env.logln(&format!(" > step {}, expecting {:?}", i, input.verdict));

// ------------------->
// Below is a temporary work around to get rid of bug-gy validator sorting
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there an issue for this sorting bug? Could you point us to any specific line where the bug occurs or you don't know?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, but yes there should be one. I think the problem is somewhere with ser/de, it somehow changes the sequence of validators in the set which then produces a wrong valset hash. I'm not sure how this is happening. But I'm sure this is not coming from Testgen at least. Currently, these tests were disabled on master because of this and re-sorting seemed to be a quick solution. I need to dig further to know where this problem is coming from.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Issue for this: #687

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I think I know what is happening here. When we transform tests from Apalache counterexamples, the validators are in no particular order. At the same time new deserialization requires them to be sorted according to the power, and then lexicographically. Therefore the validation fails. One more point for implementing #665.

// which was making all the tests fail
let current_vals = input.block.validators.clone();
let current_resorted = Set::new_simple(current_vals.validators().to_vec());

let current_next_vals = input.block.next_validators.clone();
let current_next_resorted = Set::new_simple(current_next_vals.validators().to_vec());

let mut mutated_block = input.block.clone();
mutated_block.validators = current_resorted;
mutated_block.next_validators = current_next_resorted;
// ------------------->

let now = input.now;
match verify_single(
latest_trusted.clone(),
input.block.clone().into(),
mutated_block.clone().into(),
TrustThreshold::default(),
trusting_period,
clock_drift,
now,
) {
Ok(new_state) => {
assert_eq!(input.verdict, LiteVerdict::Success);
let expected_state: LightBlock = input.block.clone().into();
let expected_state: LightBlock = mutated_block.clone().into();
assert_eq!(new_state, expected_state);
latest_trusted = Trusted::new(new_state.signed_header, new_state.next_validators);
}
Expand Down Expand Up @@ -609,7 +625,7 @@ fn model_based_test(
let mut tc: SingleStepTestCase = env.parse_file("test.json").unwrap();
tc.description = json_test.clone();
output_env.write_file(json_test, &serde_json::to_string_pretty(&tc).unwrap());
fuzz_single_step_test(tc, env, root_env, output_env);
single_step_test(tc, env, root_env, output_env);
}

fn model_based_test_batch(batch: ApalacheTestBatch) -> Vec<(String, String)> {
Expand All @@ -629,10 +645,11 @@ fn model_based_test_batch(batch: ApalacheTestBatch) -> Vec<(String, String)> {
const TEST_DIR: &str = "./tests/support/model_based";

#[test]
#[ignore]
fn run_model_based_single_step_tests() {
let mut tester = Tester::new("test_run", TEST_DIR);
tester.add_test_with_env("static model-based single-step test", fuzz_single_step_test);
// Disabled fuzzing for now because more restrictive data structure construction is breaking it
// Will be fixed in a follow-up PR
tester.add_test_with_env("static model-based single-step test", single_step_test);
tester.add_test_with_env("full model-based single-step test", model_based_test);
tester.add_test_batch(model_based_test_batch);
tester.run_foreach_in_dir("");
Expand Down
2 changes: 0 additions & 2 deletions light-client/tests/support/model_based/MC10_3_faulty.json
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@
"TestFailure",
"TestNonMonotonicHeight",
"TestHeaderFromFuture",
"TestUntrustedBeforeTrusted",
"TestHeaderNotWithinTrustingPeriod",
"TestValsetDifferentAllSteps",
"TestHalfValsetChanges",
Expand All @@ -20,7 +19,6 @@
"TestMoreThanTwoThirdsValsetChanges",
"TestOneThirdValsetChanges",
"TestTwoThirdsValsetChanges",
"TestLessThanTwoThirdsSign",
"TestMoreThanTwoThirdsSign"
]
}
1 change: 0 additions & 1 deletion light-client/tests/support/model_based/MC4_4_faulty.json
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
"Test3NotEnoughTrustFailure",
"TestNonMonotonicHeight",
"TestHeaderFromFuture",
"TestUntrustedBeforeTrusted",
"TestHeaderNotWithinTrustingPeriod",
"TestValsetDifferentAllSteps",
"TestHalfValsetChanges",
Expand Down
5,538 changes: 2,444 additions & 3,094 deletions light-client/tests/support/model_based/single_step/MC100_2_faulty_TestFailure.json

Large diffs are not rendered by default.

Loading