Testgen external commands

light-client/src/tests.rs

@@ -8,9 +8,14 @@ use tendermint_rpc as rpc;
 
 use crate::components::clock::Clock;
 use crate::components::io::{AtHeight, Io, IoError};
+use crate::components::verifier::{ProdVerifier, Verdict, Verifier};
+use crate::errors::Error;
 use crate::evidence::EvidenceReporter;
+use crate::light_client::{LightClient, Options};
+use crate::state::State;
 use contracts::contract_trait;
 use std::collections::HashMap;
+use std::time::Duration;
 use tendermint::block::Height as HeightStr;
 use tendermint::evidence::{Duration as DurationStr, Evidence};
 
@@ -148,6 +153,47 @@ impl MockEvidenceReporter {
     }
 }
 
+pub fn verify_single(
+    trusted_state: Trusted,
+    input: LightBlock,
+    trust_threshold: TrustThreshold,
+    trusting_period: Duration,
+    clock_drift: Duration,
+    now: Time,
+) -> Result<LightBlock, Verdict> {
+    let verifier = ProdVerifier::default();
+
+    let trusted_state = LightBlock::new(
+        trusted_state.signed_header,
+        trusted_state.next_validators.clone(),
+        trusted_state.next_validators,
+        default_peer_id(),
+    );
+
+    let options = Options {
+        trust_threshold,
+        trusting_period,
+        clock_drift,
+    };
+
+    let result = verifier.verify(&input, &trusted_state, &options, now);
+
+    match result {
+        Verdict::Success => Ok(input),
+        error => Err(error),
+    }
+}
+
+pub fn verify_bisection(
+    untrusted_height: Height,
+    light_client: &mut LightClient,
+    state: &mut State,
+) -> Result<Vec<LightBlock>, Error> {
+    light_client
+        .verify_to_target(untrusted_height, state)
+        .map(|_| state.get_trace(untrusted_height))
+}
+
 // -----------------------------------------------------------------------------
 // Everything below is a temporary workaround for the lack of `provider` field
 // in the light blocks serialized in the JSON fixtures.

light-client/tests/light_client.rs

@@ -5,14 +5,14 @@ use tendermint_light_client::{
     components::{
         io::{AtHeight, Io},
         scheduler,
-        verifier::{ProdVerifier, Verdict, Verifier},
+        verifier::ProdVerifier,
     },
     errors::{Error, ErrorKind},
     light_client::{LightClient, Options},
     state::State,
     store::{memory::MemoryStore, LightStore},
     tests::{Trusted, *},
-    types::{Height, LightBlock, Status, Time, TrustThreshold},
+    types::{LightBlock, Status, TrustThreshold},
 };
 
 use tendermint_testgen::Tester;
@@ -21,47 +21,6 @@ use tendermint_testgen::Tester;
 // https://github.com/informalsystems/conformance-tests
 const TEST_FILES_PATH: &str = "./tests/support/";
 
-fn verify_single(
-    trusted_state: Trusted,
-    input: LightBlock,
-    trust_threshold: TrustThreshold,
-    trusting_period: Duration,
-    clock_drift: Duration,
-    now: Time,
-) -> Result<LightBlock, Verdict> {
-    let verifier = ProdVerifier::default();
-
-    let trusted_state = LightBlock::new(
-        trusted_state.signed_header,
-        trusted_state.next_validators.clone(),
-        trusted_state.next_validators,
-        default_peer_id(),
-    );
-
-    let options = Options {
-        trust_threshold,
-        trusting_period,
-        clock_drift,
-    };
-
-    let result = verifier.verify(&input, &trusted_state, &options, now);
-
-    match result {
-        Verdict::Success => Ok(input),
-        error => Err(error),
-    }
-}
-
-fn verify_bisection(
-    untrusted_height: Height,
-    light_client: &mut LightClient,
-    state: &mut State,
-) -> Result<Vec<LightBlock>, Error> {
-    light_client
-        .verify_to_target(untrusted_height, state)
-        .map(|_| state.get_trace(untrusted_height))
-}
-
 struct BisectionTestResult {
     untrusted_light_block: LightBlock,
     new_states: Result<Vec<LightBlock>, Error>,
@@ -229,17 +188,17 @@ fn bisection_lower_test(tc: TestBisection<AnonLightBlock>) {
 
 #[test]
 fn run_single_step_tests() {
-    let mut tester = Tester::new(TEST_FILES_PATH);
+    let mut tester = Tester::new("single_step", TEST_FILES_PATH);
     tester.add_test("single-step test", single_step_test);
     tester.run_foreach_in_dir("single_step");
-    tester.print_results();
+    tester.finalize();
 }
 
 #[test]
 fn run_bisection_tests() {
-    let mut tester = Tester::new(TEST_FILES_PATH);
+    let mut tester = Tester::new("bisection", TEST_FILES_PATH);
     tester.add_test("bisection test", bisection_test);
     tester.add_test("bisection lower test", bisection_lower_test);
     tester.run_foreach_in_dir("bisection/single_peer");
-    tester.print_results();
+    tester.finalize();
 }

light-client/tests/supervisor.rs

@@ -121,8 +121,8 @@ fn run_multipeer_test(tc: TestBisection<AnonLightBlock>) {
 
 #[test]
 fn run_multipeer_tests() {
-    let mut tester = Tester::new(TEST_FILES_PATH);
+    let mut tester = Tester::new("bisection_multi_peer", TEST_FILES_PATH);
     tester.add_test("multipeer test", run_multipeer_test);
     tester.run_foreach_in_dir("bisection/multi_peer");
-    tester.print_results();
+    tester.finalize();
 }

testgen/Cargo.toml

@@ -11,6 +11,7 @@ serde_json = "1"
 ed25519-dalek = "1"
 gumdrop = "0.8.0"
 simple-error = "0.2.1"
+tempfile = "3.1.0"
 
 [[bin]]
 name = "tendermint-testgen"

testgen/jsonatr-lib/apalache-tendermint.json

@@ -0,0 +1,150 @@
+{
+  "description": "Transformers for Apalache counterexamples (CEs) with Tendermint blockchains",
+  "use": [
+    "tendermint.json"
+  ],
+  "input": [
+    {
+      "name": "first_state",
+      "description": "extract the first state from Apalache CE",
+      "kind": "INLINE",
+      "source": "$.declarations[1].body.and | unwrap"
+    },
+    {
+      "name": "last_state",
+      "description": "extract the last state from Apalache CE",
+      "kind": "INLINE",
+      "source": "$.declarations[-2].body.and | unwrap"
+    },
+    {
+      "name": "history",
+      "description": "extract the history from the last state of Apalache CE",
+      "kind": "INLINE",
+      "source": "$last_state..[?(@.eq == 'history')].arg.atat..arg.record"
+    },
+    {
+      "name": "states",
+      "description": "extract all state from Apalache CE",
+      "kind": "INLINE",
+      "source": "$.declarations[1:-1].body.and"
+    },
+    {
+      "name": "lightblock_commits",
+      "description": "extract commits from a LightClient block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'Commits')].value..str"
+    },
+    {
+      "name": "block_validators",
+      "description": "extract validators from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'VS')].value..str"
+    },
+    {
+      "name": "block_next_validators",
+      "description": "extract next validators from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'NextVS')].value..str"
+    },
+    {
+      "name": "block_height",
+      "description": "extract height from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'height')].value | unwrap"
+    },
+    {
+      "name": "block_time",
+      "description": "extract time from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'time')].value | unwrap"
+    },
+    {
+      "name": "id_to_validator",
+      "description": "transform an identifier into a validator expected by `tendermint-testgen validator`",
+      "kind": "INLINE",
+      "source": {
+        "id": "$",
+        "voting_power": 50
+      }
+    },
+    {
+      "name": "id_to_vote",
+      "description": "transform an identifier into a vote expected by `tendermint-testgen vote`",
+      "kind": "INLINE",
+      "source": {
+        "validator": "$ | id_to_validator",
+        "header": "$header"
+      }
+    },
+    {
+      "name": "block_to_header",
+      "description": "transform a block from Apalache CE into a header expected by `tendermint-testgen header`",
+      "kind": "INLINE",
+      "source": {
+        "validators": "$ | block_validators | map(id_to_validator)",
+        "next_validators": "$ | block_next_validators | map(id_to_validator)",
+        "height": "$ | block_height",
+        "time": "$ | block_time"
+      }
+    },
+    {
+      "name": "block_to_commit",
+      "description": "transform a block from Apalache CE into a commit expected by `tendermint-testgen commit`",
+      "kind": "INLINE",
+      "let": {
+        "header": "$ | block_to_header"
+      },
+      "source": {
+        "header": "$header",
+        "votes": "$ | lightblock_commits | map(id_to_vote)"
+      }
+    },
+    {
+      "name": "ids_to_validators",
+      "description": "transform a non-empty array of identifiers into Tendermint validators",
+      "kind": "INLINE",
+      "source": "$ | map(id_to_validator) | map(tendermint_validator)"
+    },
+    {
+      "name": "empty_array",
+      "description": "just an empty array",
+      "kind": "INLINE",
+      "source": []
+    },
+    {
+      "name": "first_validator",
+      "description": "extract first validator from a non-empty array of identifiers",
+      "kind": "INLINE",
+      "source": "$[0] | unwrap | id_to_validator | tendermint_validator"
+    },
+    {
+      "name": "const_id",
+      "description": "constant identifier",
+      "kind": "INLINE",
+      "source": "a"
+    },    {
+      "name": "fixed_validator",
+      "description": "extract first validator from a non-empty array of identifiers",
+      "kind": "INLINE",
+      "source": "$const_id | id_to_validator | tendermint_validator"
+    },
+    {
+      "name": "ids_to_validator_set",
+      "description": "transform an array of identifiers into a JSON-encoded Tendermint validator set",
+      "kind": "INLINE",
+      "source": {
+        "validators": "$ | ifelse(ids_to_validators,empty_array)",
+        "proposer": "$ | ifelse(first_validator,fixed_validator)"
+      }
+    },
+    {
+      "name": "block_to_signed_header",
+      "description": "transform a block from Apalache CE into a JSON-encoded Tendermint signed header",
+      "kind": "INLINE",
+      "source": {
+        "header": "$ | block_to_header | tendermint_header",
+        "commit": "$ | block_to_commit | tendermint_commit"
+      }
+    }
+  ]
+}

testgen/jsonatr-lib/apalache_to_lite_test.json

@@ -0,0 +1,42 @@
+{
+  "description": "Transform an Apalache counterexample into a Tendermint LightClient test",
+  "use": [
+    "unix.json",
+    "apalache-tendermint.json"
+  ],
+  "input": [
+    {
+      "name": "block_to_initial_block",
+      "description": "transforms a block from Apalache CE into a JSON-encoded Tendermint initial light block",
+      "kind": "INLINE",
+      "source": {
+        "signed_header": "$ | block_to_signed_header",
+        "next_validator_set": "$ | block_next_validators | ids_to_validator_set",
+        "trusting_period": "1400000000000",
+        "now": "$utc_timestamp"
+      }
+    },
+    {
+      "name": "state_to_lite_block_verdict",
+      "description": "transforms a block from Apalache CE into a JSON-encoded Tendermint light block",
+      "kind": "INLINE",
+      "let": {
+        "block": "$..[?(@.key.str == 'current')].value"
+      },
+      "source": {
+        "block": {
+          "signed_header": "$block | block_to_signed_header",
+          "validator_set": "$block | block_validators | ids_to_validator_set",
+          "next_validator_set": "$block | block_next_validators | ids_to_validator_set"
+        },
+        "now": "$..[?(@.key.str == 'now')].value | unwrap | tendermint_time",
+        "verdict": "$..[?(@.key.str == 'verdict')].value.str | unwrap"
+      }
+    }
+  ],
+  "output": {
+    "description": "auto-generated from Apalache counterexample",
+    "initial": "$history[0]..[?(@.key.str == 'current')].value | block_to_initial_block",
+    "input": "$history[1:] | map(state_to_lite_block_verdict)"
+  }
+}

testgen/jsonatr-lib/tendermint.json

@@ -0,0 +1,31 @@
+{
+  "description": "Transformers for generating Tendermint datastructures",
+  "prerequisites": "add tendermint-testgen to your $PATH",
+  "input": [
+    {
+      "name": "tendermint_validator",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin validator"
+    },
+    {
+      "name": "tendermint_header",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin header"
+    },
+    {
+      "name": "tendermint_commit",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin commit"
+    },
+    {
+      "name": "tendermint_vote",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin vote"
+    },
+    {
+      "name": "tendermint_time",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin time"
+    }
+  ]
+}