Light Client model-based testing

docs/spec/lightclient/verification/Blockchain_A_1.tla

@@ -75,7 +75,7 @@ LBT == [header |-> BT, Commits |-> {NT}]
 
 (* the header is still within the trusting period *)
 InTrustingPeriod(header) ==
-    now <= header.time + TRUSTING_PERIOD
+    now < header.time + TRUSTING_PERIOD
 
 (*
  Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes
@@ -110,7 +110,7 @@ FaultAssumption(pFaultyNodes, pNow, pBlockchain) ==
 (* Can a block be produced by a correct peer, or an authenticated Byzantine peer *)
 IsLightBlockAllowedByDigitalSignatures(ht, block) == 
     \/ block.header = blockchain[ht] \* signed by correct and faulty (maybe)
-    \/ block.Commits \subseteq Faulty /\ block.header.height = ht \* signed only by faulty
+    \/ block.Commits \subseteq Faulty /\ block.header.height = ht /\ block.header.time > 0 \* signed only by faulty
 
 (*
  Initialize the blockchain to the ultimate height right in the initial states.

docs/spec/lightclient/verification/Lightclient_A_1.tla

@@ -29,8 +29,28 @@ VARIABLES
   lightBlockStatus,   (* a function from heights to block statuses *)
   latestVerified      (* the latest verified block *)
 
-(* the variables of the lite client *)  
-lcvars == <<state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified>>  
+(* the variables of the lite client *)
+lcvars == <<state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified>>
+
+(* The light client history, which is the function mapping states (0 .. nprobes) to the record with fields:
+   - verified: the latest verified block in this state
+   - current: the block that is being checked in this state
+   - now: the time point in this state
+   - verdict: the light client verdict for the `current` block in this state
+*)
+VARIABLE
+  history
+
+InitHistory(verified, current, now, verdict) ==
+  LET first == [ verified |-> verified, current |-> current, now |-> now, verdict |-> verdict ]
+  IN history = [ n \in {0} |-> first ]
+
+NextHistory(verified, current, now, verdict) ==
+  LET last == [ verified |-> verified, current |-> current, now |-> now, verdict |-> verdict ]
+      np == nprobes+1
+  IN history' = [ n \in DOMAIN history \union {np} |->
+      IF n = np THEN last ELSE history[n]]
+
 
 (******************* Blockchain instance ***********************************)
 
@@ -74,7 +94,7 @@ ValidAndVerifiedPre(trusted, untrusted) ==
   /\ BC!InTrustingPeriod(thdr)
   /\ thdr.height < uhdr.height
      \* the trusted block has been created earlier (no drift here)
-  /\ thdr.time <= uhdr.time
+  /\ thdr.time < uhdr.time
   /\ untrusted.Commits \subseteq uhdr.VS
   /\ LET TP == Cardinality(uhdr.VS)
          SP == Cardinality(untrusted.Commits)
@@ -106,7 +126,7 @@ SignedByOneThirdOfTrusted(trusted, untrusted) ==
  *)   
 ValidAndVerified(trusted, untrusted) ==
     IF ~ValidAndVerifiedPre(trusted, untrusted)
-    THEN "FAILED_VERIFICATION"
+    THEN "INVALID"
     ELSE IF ~BC!InTrustingPeriod(untrusted.header)
     (* We leave the following test for the documentation purposes.
        The implementation should do this test, as signature verification may be slow.
@@ -115,8 +135,8 @@ ValidAndVerified(trusted, untrusted) ==
     THEN "FAILED_TRUSTING_PERIOD" 
     ELSE IF untrusted.header.height = trusted.header.height + 1
              \/ SignedByOneThirdOfTrusted(trusted, untrusted)
-         THEN "OK"
-         ELSE "CANNOT_VERIFY"
+         THEN "SUCCESS"
+         ELSE "NOT_ENOUGH_TRUST"
 
 (*
  Initial states of the light client.
@@ -135,6 +155,7 @@ LCInit ==
         /\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"]
         \* the latest verified block the the trusted block
         /\ latestVerified = trustedLightBlock
+        /\ InitHistory(trustedLightBlock, trustedLightBlock, now, "SUCCESS")
 
 \* block should contain a copy of the block from the reference chain, with a matching commit
 CopyLightBlockFromChain(block, height) ==
@@ -207,8 +228,9 @@ VerifyToTargetLoop ==
         /\ nprobes' = nprobes + 1
         \* Verify the current block
         /\ LET verdict == ValidAndVerified(latestVerified, current) IN
+           NextHistory(latestVerified, current, now, verdict) /\
            \* Decide whether/how to continue
-           CASE verdict = "OK" ->
+           CASE verdict = "SUCCESS" ->
               /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified")
               /\ latestVerified' = current
               /\ state' =
@@ -219,7 +241,7 @@ VerifyToTargetLoop ==
                  /\ CanScheduleTo(newHeight, current, nextHeight, TARGET_HEIGHT)
                  /\ nextHeight' = newHeight
 
-           [] verdict = "CANNOT_VERIFY" ->
+           [] verdict = "NOT_ENOUGH_TRUST" ->
               (*
                 do nothing: the light block current passed validation, but the validator
                 set is too different to verify it. We keep the state of
@@ -244,7 +266,8 @@ VerifyToTargetLoop ==
 VerifyToTargetDone ==
     /\ latestVerified.header.height >= TARGET_HEIGHT
     /\ state' = "finishedSuccess"
-    /\ UNCHANGED <<nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, latestVerified>>  
+    /\ UNCHANGED <<nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, latestVerified>>
+    /\ UNCHANGED <<history>>
 
 (********************* Lite client + Blockchain *******************)
 Init ==
@@ -310,7 +333,7 @@ CorrectnessInv ==
             fetchedLightBlocks[h].header = blockchain[h]
 
 (**
- Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "OK" pairwise
+ Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "SUCCESS" pairwise
  This property is easily violated, whenever a header cannot be trusted anymore.
  *)
 StoredHeadersAreVerifiedInv ==
@@ -322,7 +345,7 @@ StoredHeadersAreVerifiedInv ==
             \/ \E mh \in DOMAIN fetchedLightBlocks:
                 lh < mh /\ mh < rh
                \* or we can verify the right one using the left one
-            \/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
+            \/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
 
 \* An improved version of StoredHeadersAreSound, assuming that a header may be not trusted.
 \* This invariant candidate is also violated,
@@ -336,7 +359,7 @@ StoredHeadersAreVerifiedOrNotTrustedInv ==
             \/ \E mh \in DOMAIN fetchedLightBlocks:
                 lh < mh /\ mh < rh
                \* or we can verify the right one using the left one
-            \/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
+            \/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
                \* or the left header is outside the trusting period, so no guarantees
             \/ ~BC!InTrustingPeriod(fetchedLightBlocks[lh].header) 
 
@@ -359,7 +382,7 @@ ProofOfChainOfTrustInv ==
                \* or the left header is outside the trusting period, so no guarantees
             \/ ~(BC!InTrustingPeriod(fetchedLightBlocks[lh].header))
                \* or we can verify the right one using the left one
-            \/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
+            \/ "SUCCESS" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh])
 
 (**
  * When the light client terminates, there are no failed blocks. (Otherwise, someone lied to us.) 

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();
 }