TLA+: Updating the fastsync spec after model checking (#466)

* adapted fastsync for apalache * bugfix for CorrectBlocks * the minimalistic model of blockchain for fastsync * fixed safety * introduced height again * fixed CorrectBlocks * simplified the blockchain spec * decreasing the search space, to give TLC a chance * added Termination2 * a few fixes * a better way of using the abstract hashes * configuration files for the repeatable experiments * INVARIANT -> PROPERTY * increased apalache timeout * doubled the timeouts for apalache and tlc * formatting * new timeouts for the experiments * fixed termination after the example by tlc * comment on hash abstraction * TerminationCorr * added comments on the properties * increase tlc timeout to 12 hrs * increased tlc timeout to 24h * simplifying block execution + comments * the experiments with 2 faulty processes * a model for 2 faulty processes * cleaning up the spec a bit * updates from verification/fastsync_apalache.tla after model checking * copied Tinychain.tla from verification * updated the spec name * Update docs/spec/fastsync/Tinychain.tla Co-authored-by: Josef Widder <[email protected]> * Update docs/spec/fastsync/fastsync.tla Co-authored-by: Josef Widder <[email protected]> * Update docs/spec/fastsync/fastsync.tla Co-authored-by: Josef Widder <[email protected]> * addressing Josef's comments Co-authored-by: Josef Widder <[email protected]>
informalsystems · Aug 7, 2020 · a124e21 · a124e21
1 parent 0657d27
commit a124e21
Show file tree

Hide file tree

Showing 21 changed files with 1,507 additions and 123 deletions.
diff --git a/docs/spec/fastsync/Tinychain.tla b/docs/spec/fastsync/Tinychain.tla
@@ -0,0 +1,113 @@
+-------------------------- 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 potential commits
+Commits == [blockIdEqRef: BOOLEAN, committers: VALIDATOR_SETS]
+
+\* the set of all potential blocks, not necessarily coming from the blockchain
+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!
+\* Since we are abstracting validator sets with VALIDATOR_SETS, which are
+\* 2/3 quorums, we just compare committers to those sets. In a more detailed
+\* specification, one would write the \subseteq operator instead of equality.
+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)
+
+==================================================================================