something is working

docs/spec/lightclient/Lightclient_A_1.tla

@@ -70,7 +70,7 @@ ValidAndVerifiedPre(trusted, untrusted) ==
   IN
   /\ BC!InTrustingPeriod(thdr)
   /\ thdr.height < uhdr.height
-  /\ thdr.height = uhdr.height + 1 =>
+  /\ thdr.height + 1 = uhdr.height =>
      /\ thdr.NextVS = uhdr.VS
      /\ untrusted.Commits \subseteq uhdr.VS
      /\ LET TP == Cardinality(uhdr.VS)
@@ -127,15 +127,20 @@ LCInit ==
         /\ latestVerified = trustedLightBlock
 
 LightStoreGetInto(block, height) ==
+    block = fetchedLightBlocks[height]
+
+IsCanonicalLightBlock(block, height) ==
     LET ref == blockchain[height]
         lastCommit ==
-          IF height > 0 THEN blockchain[height - 1].VS ELSE AllNodes
+          IF height < ULTIMATE_HEIGHT
+          THEN blockchain[height + 1].lastCommit
+          ELSE blockchain[height].VS \* for the ultimate block 
     IN
     block = [header |-> ref, Commits |-> lastCommit]      
 
 FetchLightBlockInto(block, height) ==
     IF IS_PRIMARY_CORRECT
-    THEN LightStoreGetInto(block, height)
+    THEN IsCanonicalLightBlock(block, height)
     ELSE BC!IsProducableByFaulty(height, block)
 
 LightStoreUpdateBlocks(lightBlocks, block) ==
@@ -144,7 +149,7 @@ LightStoreUpdateBlocks(lightBlocks, block) ==
         IF h = ht THEN block ELSE lightBlocks[h]]
 
 LightStoreUpdateStates(statuses, ht, blockState) ==
-    [h \in DOMAIN statuses |->
+    [h \in DOMAIN statuses \union {ht} |->
         IF h = ht THEN blockState ELSE statuses[h]]      
 
 ScheduleTo(newHeight, pNextHeight, pTargetHeight, pLatestVerified) ==
@@ -158,7 +163,6 @@ ScheduleTo(newHeight, pNextHeight, pTargetHeight, pLatestVerified) ==
        /\ ht < newHeight
        /\ newHeight < pNextHeight
     \/ /\ ht = pTargetHeight
-       /\ ht < newHeight
        /\ newHeight = pTargetHeight
 
 LightLoop ==
@@ -178,7 +182,7 @@ LightLoop ==
                     THEN "working"
                     ELSE "finishedSuccess"
               /\ \E newHeight \in HEIGHTS:
-                 /\ ScheduleTo(newHeight, nextHeight, TARGET_HEIGHT, latestVerified')
+                 /\ ScheduleTo(newHeight, nextHeight, TARGET_HEIGHT, current)
                  /\ nextHeight' = newHeight 
            \/ /\ verdict = "CANNOT_VERIFY"
               /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateUnverified")
@@ -200,7 +204,7 @@ LightFinish ==
  Actions of the light client: start or do bisection when receiving response.
  *)
 LCNext ==
-  \/ state /= "working" /\ UNCHANGED lcvars
+  \*\/ state /= "working" /\ UNCHANGED lcvars
   \/ /\ state = "working"
      /\ LightLoop \/ LightFinish 
 
@@ -235,23 +239,31 @@ TypeOK ==
 (************************* Properties ******************************************)
 
 (* The properties to check *)
+NeverFinish ==
+    state = "working"
+
 \* check this property to get an example of a terminating light client
 NeverFinishNegative ==
     state /= "finishedFailure"
+
+NeverFinishNegativeWhenTrusted ==
+    (minTrustedHeight <= TRUSTED_HEIGHT) => state /= "finishedFailure"     
 
 NeverFinishPositive ==
     state /= "finishedSuccess"
 
-(*
 \* Correctness states that all the obtained headers are exactly like in the blockchain.
 \* This formula is equivalent to Accuracy in the English spec, that is, A => B iff ~B => ~A.
 \*
 \* Lite Client Accuracy: If header h was not generated by an instance of Tendermint consensus,
 \* then the lite client should never set trust(h) to true.
 CorrectnessInv ==
-    (outEvent.type = "finished" /\ outEvent.verdict = TRUE)
-        => (\A shdr \in storedLightBlocks: shdr.header = blockchain[shdr.header.height])
+    state = "finishedSuccess"
+        => \A h \in DOMAIN fetchedLightBlocks:
+             lightBlockStatus[h] = "StateVerified" =>
+                fetchedLightBlocks[h].header = blockchain[h]
 
+(*
 \* CorrectnessInv holds only under the assumption of the Tendermint security model.
 \* Hence, Correctness is restricted to the case when there are less than 1/3 of faulty validators.
 Correctness ==
@@ -347,5 +359,5 @@ Completeness ==
 *)    
 =============================================================================
 \* Modification History
-\* Last modified Wed Jun 03 12:30:07 CEST 2020 by igor
+\* Last modified Wed Jun 03 17:21:30 CEST 2020 by igor
 \* Created Wed Oct 02 16:39:42 CEST 2019 by igor

docs/spec/lightclient/MC4_1_3_correct.tla

@@ -0,0 +1,13 @@
+------------------------- MODULE MC4_1_3_correct ---------------------------
+
+AllNodes == {"n1", "n2", "n3", "n4"}
+TRUSTED_HEIGHT == 1
+TARGET_HEIGHT == 3
+IS_PRIMARY_CORRECT == TRUE
+
+VARIABLES
+  state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified,
+  tooManyFaults, chainHeight, minTrustedHeight, blockchain, Faulty
+
+INSTANCE Lightclient_A_1
+============================================================================