#414: LightClient_A_1: add time to history variables

informalsystems · Aug 10, 2020 · d223773 · d223773
1 parent 4715e18
commit d223773
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 17 deletions.
diff --git a/docs/spec/lightclient/verification/Lightclient_A_1.tla b/docs/spec/lightclient/verification/Lightclient_A_1.tla
@@ -29,24 +29,34 @@ 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 light client history variables *)
 VARIABLES
   prevVerified,       (* the latest verified block in the previous state *)
   prevChecked,        (* the block that was checked in the previous state *)
+  prevTime,           (* the time when the check was performed in the previous state *)
   prevVerdict         (* the verdict in the previous state *)
 
-InitHistory(verified, checked, verdict) ==
+(* the history variables of the lite client *)
+lchistory == <<prevVerified, prevChecked, prevTime, prevVerdict>>
+
+Update(vars, newvars) == vars = newvars
+
+
+InitHistory(verified, checked, time, verdict) ==
   /\ prevVerified = verified
   /\ prevChecked = checked
+  /\ prevTime = time
   /\ prevVerdict = verdict
 
-NextHistory(verified, checked, verdict) ==
+NextHistory(verified, checked, time, verdict) ==
   /\ prevVerified' = verified
   /\ prevChecked' = checked
+  /\ prevTime' = time
   /\ prevVerdict' = verdict
 
-(* the variables of the lite client *)
-lcvars == <<state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified>>
 
 (******************* Blockchain instance ***********************************)
 
@@ -151,7 +161,7 @@ LCInit ==
         /\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"]
         \* the latest verified block the the trusted block
         /\ latestVerified = trustedLightBlock
-        /\ NextHistory(trustedLightBlock, trustedLightBlock, "OK")
+        /\ InitHistory(trustedLightBlock, trustedLightBlock, now, "OK")
 
 \* block should contain a copy of the block from the reference chain, with a matching commit
 CopyLightBlockFromChain(block, height) ==
@@ -224,7 +234,7 @@ VerifyToTargetLoop ==
         /\ nprobes' = nprobes + 1
         \* Verify the current block
         /\ LET verdict == ValidAndVerified(latestVerified, current) IN
-           NextHistory(latestVerified, current, verdict) /\
+           NextHistory(latestVerified, current, now, verdict) /\
            \* Decide whether/how to continue
            CASE verdict = "OK" ->
               /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified")
@@ -263,7 +273,7 @@ VerifyToTargetDone ==
     /\ latestVerified.header.height >= TARGET_HEIGHT
     /\ state' = "finishedSuccess"
     /\ UNCHANGED <<nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, latestVerified>>
-    /\ UNCHANGED <<prevVerified, prevChecked, prevVerdict>>
+    /\ UNCHANGED lchistory
 
 (********************* Lite client + Blockchain *******************)
 Init ==

diff --git a/tendermint/tests/support/lite-model-based/MC4_4_faulty.tla b/tendermint/tests/support/lite-model-based/MC4_4_faulty.tla
@@ -8,7 +8,7 @@ IS_PRIMARY_CORRECT == FALSE
 
 VARIABLES
   state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified,
-  prevVerified, prevChecked, prevVerdict,
+  prevVerified, prevChecked, prevTime, prevVerdict,
   nprobes,
   now, blockchain, Faulty
 

diff --git a/tendermint/tests/utils/jsonatr-lib/apalache-tendermint.json b/tendermint/tests/utils/jsonatr-lib/apalache-tendermint.json
@@ -1,7 +1,6 @@
 {
   "description": "Transformers for Apalache counterexamples (CEs) with Tendermint blockchains",
   "use": [
-    "unix.json",
     "tendermint.json"
   ],
   "input": [

diff --git a/tendermint/tests/utils/jsonatr-lib/apalache_to_lite_test.json b/tendermint/tests/utils/jsonatr-lib/apalache_to_lite_test.json
@@ -9,23 +9,18 @@
       "name": "block_to_initial_block",
       "description": "transforms a block from Apalache CE into a JSON-encoded Tendermint initial light block",
       "kind": "INLINE",
-      "let": {
-        "now": "$utc_timestamp",
-        "utc_timestamp": "$utc_timestamp_2hours_ago"
-      },
       "source": {
         "signed_header": "$ | block_to_signed_header",
         "next_validator_set": "$ | block_next_validators | ids_to_validator_set",
-        "trusting_period": "10800000000000",
-        "now": "$now"
+        "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": {
-        "utc_timestamp": "$utc_timestamp_hour_ago",
         "block": "$..[?(@.eq == 'prevChecked')]"
       },
       "source": {
@@ -34,7 +29,7 @@
           "validator_set": "$block | block_validators | ids_to_validator_set",
           "next_validator_set": "$block | block_next_validators | ids_to_validator_set"
         },
-        "time": "$..[?(@.eq == 'now')].arg | unwrap | tendermint_time",
+        "time": "$..[?(@.eq == 'prevTime')].arg | unwrap | tendermint_time",
         "verdict": "$..[?(@.eq == 'prevVerdict')].arg.str | unwrap"
       }
     }