TLA+: Updating the fastsync spec after model checking

docs/spec/fastsync/Tinychain.tla

@@ -0,0 +1,110 @@
+-------------------------- MODULE Tinychain ----------------------------------
+(* A very abstract model of Tendermint blockchain. Its only purpose is to highlight
+   the relation between validator sets, next validator sets, and last commits.
+ *)
+
+EXTENDS Integers
+
+\* type annotation
+a <: b == a
+
+\* the type of validator sets, e.g., STRING
+VST == STRING
+
+\* LastCommit type.
+\* It contains:
+\* 1) the flag of whether the block id equals to the hash of the previous block, and
+\* 2) the set of the validators who have committed the block.
+\* In the implementation, blockId is the hash of the previous block, which cannot be forged.
+\* We abstract block id into whether it equals to the hash of the previous block or not.
+LCT == [blockIdEqRef |-> BOOLEAN, committers |-> VST]
+
+\* Block type.
+\* A block contains its height, validator set, next validator set, and last commit.
+\* Moreover, it contains the flag that tells us whether the block is equal to the one
+\* on the reference chain (this is an abstraction of hash).
+BT == [height |-> Int, hashEqRef |-> BOOLEAN, wellFormed |-> BOOLEAN,
+       VS |-> VST, NextVS |-> VST, lastCommit |-> LCT]
+
+CONSTANTS
+    (*
+       A set of abstract values, each value representing a set of validators.
+       For the purposes of this specification, they can be any values,
+       e.g., "s1", "s2", etc.
+     *)
+    VALIDATOR_SETS,
+    (* a nil validator set that is outside of VALIDATOR_SETS *)
+    NIL_VS,
+    (* The maximal height, up to which the blockchain may grow *)
+    MAX_HEIGHT
+
+Heights == 1..MAX_HEIGHT    
+
+\* the set of all possible commits
+Commits == [blockIdEqRef: BOOLEAN, committers: VALIDATOR_SETS]
+
+\* the set of all possible blocks, not necessarily valid ones
+Blocks ==
+  [height: Heights, hashEqRef: BOOLEAN, wellFormed: BOOLEAN,
+   VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: Commits]
+
+\* Does the chain contain a sound sequence of blocks that could be produced by
+\* a 2/3 of faulty validators. This operator can be used to initialise the chain!
+IsCorrectChain(chain) ==
+    \* restrict the structure of the blocks, to decrease the TLC search space
+    LET OkCommits == [blockIdEqRef: {TRUE}, committers: VALIDATOR_SETS]
+        OkBlocks == [height: Heights, hashEqRef: {TRUE}, wellFormed: {TRUE},
+                     VS: VALIDATOR_SETS, NextVS: VALIDATOR_SETS, lastCommit: OkCommits]
+    IN
+    /\ chain \in [1..MAX_HEIGHT -> OkBlocks]
+    /\ \A h \in 1..MAX_HEIGHT:
+        LET b == chain[h] IN
+        /\ b.height = h     \* the height is correct
+        /\ h > 1 =>
+             LET p == chain[h - 1] IN
+             /\ b.VS = p.NextVS     \* the validators propagate from the previous block
+             /\ b.lastCommit.committers = p.VS  \* and they are the committers
+
+
+\* The basic properties of blocks on the blockchain:
+\* They should pass the validity check and they may verify the next block.    
+
+\* Does the block pass the consistency check against the next validators of the previous block
+IsMatchingValidators(block, nextVS) ==
+    \* simply check that the validator set is propagated correctly.
+    \* (the implementation tests hashes and the application state)
+    block.VS = nextVS
+
+\* Does the block verify the commit (of the next block)
+PossibleCommit(block, commit) ==
+    \* the commits are signed by the block validators
+    /\ commit.committers = block.VS
+    \* The block id in the commit matches the block hash (abstract comparison).
+    \* (The implementation has extensive tests for that.)
+    \* this is an abstraction of: commit.blockId = hash(block)
+    \* 
+    \* These are possible scenarios on the concrete hashes:
+    \*
+    \* scenario 1: commit.blockId = 10 /\ hash(block) = 10 /\ hash(ref) = 10
+    \* scenario 2: commit.blockId = 20 /\ hash(block) = 20 /\ block.VS /= ref.VS
+    \* scenario 3: commit.blockId = 50 /\ hash(block) = 100
+    \* scenario 4: commit.blockId = 10 /\ hash(block) = 100
+    \* scenario 5: commit.blockId = 100 /\ hash(block) = 10
+    /\ commit.blockIdEqRef = block.hashEqRef
+    \* the following test would be cheating, as we do not have access to the
+    \* reference chain:
+    \* /\ commit.blockIdEqRef
+
+\* Basic invariants
+
+\* every block has the validator set that is chosen by its predecessor
+ValidBlockInv(chain) ==
+    \A h \in 2..MAX_HEIGHT:
+        IsMatchingValidators(chain[h], chain[h - 1].NextVS)
+
+\* last commit of every block is signed by the validators of the predecessor     
+VerifiedBlockInv(chain) ==
+    \A h \in 2..MAX_HEIGHT:
+        PossibleCommit(chain[h - 1], chain[h].lastCommit)
+
+==================================================================================