cometbft · josef-widder · Jun 13, 2023 · Jun 12, 2023 · Jun 12, 2023 · Jun 12, 2023
@@ -0,0 +1 @@
+- Update Apalache type annotations in the light client spec ([#955](https://github.com/cometbft/cometbft/pull/955))
@@ -6,17 +6,23 @@
   voting powers, introduce multiple copies of the same validator
   (do not forget to give them unique names though).
  *)
-EXTENDS Integers, FiniteSets
+EXTENDS Integers, FiniteSets, typedefs
 
 Min(a, b) == IF a < b THEN a ELSE b
 
 CONSTANT
+  \* a set of all nodes that can act as validators (correct and faulty)
+  \*
+  \* @type: Set($node);
   AllNodes,
-    (* a set of all nodes that can act as validators (correct and faulty) *)
+  \* a maximal height that can be ever reached (modelling artifact)
+  \*
+  \* @type: Int;
   ULTIMATE_HEIGHT,
-    (* a maximal height that can be ever reached (modelling artifact) *)
+  \* the period within which the validators are trusted
+  \*
+  \* @type: Int;
   TRUSTING_PERIOD
-    (* the period within which the validators are trusted *)
 
 Heights == 1..ULTIMATE_HEIGHT   (* possible heights *)
 
@@ -44,36 +50,29 @@ BlockHeaders == [
 LightBlocks == [header: BlockHeaders, Commits: Commits]
 
 VARIABLES
+    \* the current global time in integer units as perceived by the reference chain
+    \* @type: Int;
     refClock,
-        (* the current global time in integer units as perceived by the reference chain *)
+    \* A sequence of BlockHeaders, which gives us a bird view of the blockchain
+    \* @type: Int -> $header;
     blockchain,
-    (* A sequence of BlockHeaders, which gives us a bird view of the blockchain. *)
+    \* A set of faulty nodes, which can act as validators.
+    \* We assume that the set of faulty processes is non-decreasing.
+    \* If a process has recovered, it should connect using a different id.
+    \* @type: Set($node);
     Faulty
-    (* A set of faulty nodes, which can act as validators. We assume that the set
-       of faulty processes is non-decreasing. If a process has recovered, it should
-       connect using a different id. *)
 
 (* all variables, to be used with UNCHANGED *)       
 vars == <<refClock, blockchain, Faulty>>         
 
 (* The set of all correct nodes in a state *)
 Corr == AllNodes \ Faulty
 
-(* APALACHE annotations *)
-a <: b == a \* type annotation
-
-NT == STRING
-NodeSet(S) == S <: {NT}
-EmptyNodeSet == NodeSet({})
-
-BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}]
-
-LBT == [header |-> BT, Commits |-> {NT}]
-(* end of APALACHE annotations *)       
-
 (****************************** BLOCKCHAIN ************************************)
 
-(* the header is still within the trusting period *)
+\* the header is still within the trusting period
+\*
+\* @type: $header => Bool;
 InTrustingPeriod(header) ==
     refClock < header.time + TRUSTING_PERIOD
 
@@ -97,6 +96,8 @@ TwoThirds(pVS, pNodes) ==
    - pVS is a set of all validators, maybe including Faulty, intersecting with it, etc.
    - pMaxFaultRatio is a pair <<a, b>> that limits the ratio a / b of the faulty
      validators from above (exclusive)
+
+ @type: (Set($node), Set($node), <<Int, Int>>) => Bool;
  *)
 FaultyValidatorsFewerThan(pFaultyNodes, pVS, maxRatio) ==
     LET FN == pFaultyNodes \intersect pVS   \* faulty nodes in pNodes
@@ -108,7 +109,9 @@ FaultyValidatorsFewerThan(pFaultyNodes, pVS, maxRatio) ==
     LET TP == CP + FP IN
     FP * maxRatio[2] < TP * maxRatio[1]
 
-(* Can a block be produced by a correct peer, or an authenticated Byzantine peer *)
+\* Can a block be produced by a correct peer, or an authenticated Byzantine peer
+\*
+\* @type: (Int, $lightHeader) => Bool;
 IsLightBlockAllowedByDigitalSignatures(ht, block) == 
     \/ block.header = blockchain[ht] \* signed by correct and faulty (maybe)
     \/ /\ block.Commits \subseteq Faulty
@@ -122,6 +125,8 @@ IsLightBlockAllowedByDigitalSignatures(ht, block) ==
  Parameters:
     - pMaxFaultyRatioExclusive is a pair <<a, b>> that bound the number of
         faulty validators in each block by the ratio a / b (exclusive)
+
+ @type: <<Int, Int>> => Bool;
  *)            
 InitToHeight(pMaxFaultyRatioExclusive) ==
   /\ Faulty \in SUBSET AllNodes \* some nodes may fail
@@ -133,7 +138,7 @@ InitToHeight(pMaxFaultyRatioExclusive) ==
         \* the genesis starts on day 1     
         /\ timestamp[1] = 1
         /\ vs[1] = AllNodes
-        /\ lastCommit[1] = EmptyNodeSet
+        /\ lastCommit[1] = {}
         /\ \A h \in Heights \ {1}:
           /\ lastCommit[h] \subseteq vs[h - 1]   \* the non-validators cannot commit 
           /\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes

@@ -2,30 +2,43 @@
 (**
  * The common interface of the light client verification and detection.
  *) 
-EXTENDS Integers, FiniteSets
+EXTENDS Integers, FiniteSets, typedefs
 
 \* the parameters of Light Client
 CONSTANTS
+  \* the period within which the validators are trusted
+  \* @type: Int;
   TRUSTING_PERIOD,
-    (* the period within which the validators are trusted *)
+  \* the assumed precision of the clock
+  \* @type: Int;
   CLOCK_DRIFT,
-    (* the assumed precision of the clock *)
+  \* the actual clock drift, which under normal circumstances should not
+  \* be larger than CLOCK_DRIFT (otherwise, there will be a bug)
+  \*
+  \* @type: Int;
   REAL_CLOCK_DRIFT,
-    (* the actual clock drift, which under normal circumstances should not
-       be larger than CLOCK_DRIFT (otherwise, there will be a bug) *)
+  \* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
+  \* from above (exclusive). Cosmos security model prescribes 1 / 3
+  \* @type: <<Int, Int>>;
   FAULTY_RATIO
-    (* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
-       from above (exclusive). Cosmos security model prescribes 1 / 3. *)
 
 VARIABLES  
-  localClock (* current time as measured by the light client *)
+  \* current time as measured by the light client
+  \* @type: Int;
+  localClock
 
-(* the header is still within the trusting period *)
+\* The header is still within the trusting period.
+\* @type: $header => Bool;
 InTrustingPeriodLocal(header) ==
     \* note that the assumption about the drift reduces the period of trust
     localClock < header.time + TRUSTING_PERIOD - CLOCK_DRIFT
 
-(* the header is still within the trusting period, even if the clock can go backwards *)
+(*
+  The header is still within the trusting period, even if the clock can go
+  backwards.
+
+  @type: $header => Bool;
+  *)
 InTrustingPeriodLocalSurely(header) ==
     \* note that the assumption about the drift reduces the period of trust
     localClock < header.time + TRUSTING_PERIOD - 2 * CLOCK_DRIFT
@@ -36,8 +49,10 @@ IsLocalClockWithinDrift(local, global) ==
     /\ local <= global + REAL_CLOCK_DRIFT
 
 (**
-  * Check that the commits in an untrusted block form 1/3 of the next validators
-  * in a trusted header.
+  Check that the commits in an untrusted block form 1/3 of the next validators
+  in a trusted header.
+
+  @type: ($lightHeader, $lightHeader) => Bool;
  *)
 SignedByOneThirdOfTrusted(trusted, untrusted) ==
   LET TP == Cardinality(trusted.header.NextVS)
@@ -50,6 +65,8 @@ SignedByOneThirdOfTrusted(trusted, untrusted) ==
  the current time into account.
 
  [LCV-FUNC-VALID.1::TLA-PRE-UNTIMED.1]
+
+     @type: ($lightHeader, $lightHeader) => Bool;
  *)
 ValidAndVerifiedPreUntimed(trusted, untrusted) ==
   LET thdr == trusted.header
@@ -76,6 +93,8 @@ ValidAndVerifiedPreUntimed(trusted, untrusted) ==
  Check the precondition of ValidAndVerified, including the time checks.
 
  [LCV-FUNC-VALID.1::TLA-PRE.1]
+
+ @type: ($lightHeader, $lightHeader, Bool) => Bool;
  *)
 ValidAndVerifiedPre(trusted, untrusted, checkFuture) ==
   LET thdr == trusted.header
@@ -124,6 +143,8 @@ ValidAndVerified(trusted, untrusted, checkFuture) ==
 
 (**
   The invariant of the light store that is not related to the blockchain
+
+  @type: (Int -> $lightHeader, Int -> Str) => Bool;
  *)
 LightStoreInv(fetchedLightBlocks, lightBlockStatus) ==
     \A lh, rh \in DOMAIN fetchedLightBlocks:
@@ -148,6 +169,8 @@ LightStoreInv(fetchedLightBlocks, lightBlockStatus) ==
   an instance of Tendermint consensus.
 
   [LCV-DIST-SAFE.1::CORRECTNESS-INV.1]
+
+  @type: ($blockchain, Int -> $lightHeader, Int -> Str) => Bool;
  *)  
 CorrectnessInv(blockchain, fetchedLightBlocks, lightBlockStatus) ==
     \A h \in DOMAIN fetchedLightBlocks:
@@ -157,13 +180,18 @@ CorrectnessInv(blockchain, fetchedLightBlocks, lightBlockStatus) ==
 (**
  * When the light client terminates, there are no failed blocks.
  * (Otherwise, someone lied to us.) 
+ *
+ * @type: (Int -> $lightHeader, Int -> Str) => Bool;
  *)            
 NoFailedBlocksOnSuccessInv(fetchedLightBlocks, lightBlockStatus) ==
      \A h \in DOMAIN fetchedLightBlocks:
-        lightBlockStatus[h] /= "StateFailed"            
+        lightBlockStatus[h] /= "StateFailed"
 
 (**
  The expected post-condition of VerifyToTarget.
+
+ @type: ($blockchain, Bool,
+         Int -> $lightHeader, Int -> Str, Int, Int, Str) => Bool;
  *)
 VerifyToTargetPost(blockchain, isPeerCorrect,
                    fetchedLightBlocks, lightBlockStatus,

@@ -6,48 +6,74 @@
  * https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md
  *) 
 
-EXTENDS Integers, FiniteSets
+EXTENDS Integers, FiniteSets, typedefs
 
 \* the parameters of Light Client
 CONSTANTS
+  \* an index of the block header that the light client trusts by social consensus
+  \* @type: Int;
   TRUSTED_HEIGHT,
-    (* an index of the block header that the light client trusts by social consensus *)
+  \* an index of the block header that the light client tries to verify
+  \* @type: Int;
   TARGET_HEIGHT,
-    (* an index of the block header that the light client tries to verify *)
+  \* the period within which the validators are trusted
+  \* @type: Int;
   TRUSTING_PERIOD,
-    (* the period within which the validators are trusted *)
+  \* the assumed precision of the clock
+  \* @type: Int;
   CLOCK_DRIFT,
-    (* the assumed precision of the clock *)
+  \* the actual clock drift, which under normal circumstances should not
+  \* be larger than CLOCK_DRIFT (otherwise, there will be a bug)
+  \*
+  \* @type: Int;
   REAL_CLOCK_DRIFT,
-    (* the actual clock drift, which under normal circumstances should not
-       be larger than CLOCK_DRIFT (otherwise, there will be a bug) *)
+  \* is primary correct?
+  \* @type: Bool;
   IS_PRIMARY_CORRECT,
-    (* is primary correct? *)  
+  \* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
+  \* from above (exclusive). Cosmos security model prescribes 1 / 3
+  \* @type: <<Int, Int>>;
   FAULTY_RATIO
-    (* a pair <<a, b>> that limits that ratio of faulty validator in the blockchain
-       from above (exclusive). Cosmos security model prescribes 1 / 3. *)
-
-VARIABLES       (* see TypeOK below for the variable types *)
-  localClock,   (* the local clock of the light client *)
-  state,        (* the current state of the light client *)
-  nextHeight,   (* the next height to explore by the light client *)
-  nprobes       (* the lite client iteration, or the number of block tests *)
+
+VARIABLES
+  \* current time as measured by the light client
+  \* @type: Int;
+  localClock,
+  \* the current state of the light client
+  \* @type: Str;
+  state,
+  \* the next height to explore by the light client
+  \* @type: Int;
+  nextHeight,
+  \* the lite client iteration, or the number of block tests
+  \* @type: Int;
+  nprobes
 
 (* the light store *)
 VARIABLES  
-  fetchedLightBlocks, (* a function from heights to LightBlocks *)
-  lightBlockStatus,   (* a function from heights to block statuses *)
-  latestVerified      (* the latest verified block *)
+  \* a function from heights to LightBlocks
+  \* @type: Int -> $lightHeader;
+  fetchedLightBlocks,
+  \* a function from heights to block statuses
+  \* @type: Int -> Str;
+  lightBlockStatus,
+  \* the latest verified block
+  \* @type: $lightHeader;
+  latestVerified
 
 (* the variables of the lite client *)
 lcvars == <<localClock, state, nextHeight,
             fetchedLightBlocks, lightBlockStatus, latestVerified>>
 
 (* the light client previous state components, used for monitoring *)
 VARIABLES
+  \* @type: $lightHeader;
   prevVerified,
+  \* @type: $lightHeader;
   prevCurrent,
+  \* @type: Int;
   prevLocalClock,
+  \* @type: Str;
   prevVerdict
 
 InitMonitor(verified, current, pLocalClock, verdict) ==
@@ -67,11 +93,23 @@ NextMonitor(verified, current, pLocalClock, verdict) ==
 
 \* the parameters that are propagated into Blockchain
 CONSTANTS
+  \* a set of all nodes that can act as validators (correct and faulty)
+  \* @type: Set($node);
   AllNodes
-    (* a set of all nodes that can act as validators (correct and faulty) *)
 
 \* the state variables of Blockchain, see Blockchain.tla for the details
-VARIABLES refClock, blockchain, Faulty
+VARIABLES
+    \* the current global time in integer units as perceived by the reference chain
+    \* @type: Int;
+    refClock,
+    \* A sequence of BlockHeaders, which gives us a bird view of the blockchain
+    \* @type: Int -> $header;
+    blockchain,
+    \* A set of faulty nodes, which can act as validators.
+    \* We assume that the set of faulty processes is non-decreasing.
+    \* If a process has recovered, it should connect using a different id.
+    \* @type: Set($node);
+    Faulty
 
 \* All the variables of Blockchain. For some reason, BC!vars does not work
 bcvars == <<refClock, blockchain, Faulty>>
@@ -141,6 +179,8 @@ FetchLightBlockInto(block, height) ==
 \* add a block into the light store    
 \*
 \* [LCV-FUNC-UPDATE.1::TLA.1]
+\*
+\* @type: (Int -> $lightHeader, $lightHeader) => (Int -> $lightHeader);
 LightStoreUpdateBlocks(lightBlocks, block) ==
     LET ht == block.header.height IN    
     [h \in DOMAIN lightBlocks \union {ht} |->
@@ -149,13 +189,17 @@ LightStoreUpdateBlocks(lightBlocks, block) ==
 \* update the state of a light block      
 \*
 \* [LCV-FUNC-UPDATE.1::TLA.1]
+\*
+\* @type: (Int -> Str, Int, Str) => (Int -> Str);
 LightStoreUpdateStates(statuses, ht, blockState) ==
     [h \in DOMAIN statuses \union {ht} |->
         IF h = ht THEN blockState ELSE statuses[h]]      
 
 \* Check, whether newHeight is a possible next height for the light client.
 \*
 \* [LCV-FUNC-SCHEDULE.1::TLA.1]
+\*
+\* @type: (Int, $lightHeader, Int, Int) => Bool;
 CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) ==
     LET ht == pLatestVerified.header.height IN
     \/ /\ ht = pNextHeight
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		- Update Apalache type annotations in the light client spec ([#955](https://github.com/cometbft/cometbft/pull/955))