Inductive invariant validation.

.github/workflows/tla.yml

@@ -8,7 +8,7 @@ on:
   workflow_dispatch:
 
 jobs:
-  apalache:
+  apalache-check:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
@@ -20,20 +20,114 @@ jobs:
         run: |
           wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
           tar zxvf apalache.tgz
-      - name: Typecheck
+      - name: Type- and (ordinary) invariant checking with Apalache
         run: |
-          ./apalache/bin/apalache-mc typecheck APApbft.tla
-  tlc:
+          ## -length=4 to finish in reasonable time.
+          ./apalache/bin/apalache-mc check --config=APApbft.cfg --length=4 APApbft.tla
+      - name: Upload Apalache's counterexample (if any)
+        uses: actions/upload-artifact@v4
+        if: always()
+        with:
+            name: apalache-check
+            path: |
+              _apalache-out/
+
+  ## Too expensive as of now.
+  # apalache-check-inductive:
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     - uses: actions/checkout@v4
+  #     - uses: actions/setup-java@v4
+  #       with:
+  #         distribution: 'microsoft'
+  #         java-version: '17'
+  #     - name: Setup
+  #       run: |
+  #         wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
+  #         tar zxvf apalache.tgz
+  #     - name: Partial inductive invariant checking with Apalache
+  #       if: always()
+  #       run: |
+  #         # Check that Init => SafetyInv
+  #         ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=0 APAIndpbft.tla
+  #         # Check that SafetyInv /\ Next => SafetyInv'
+  #         ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=1 APAIndpbft.tla
+  #     - name: Upload Apalache's counterexample (if any)
+  #       uses: actions/upload-artifact@v4
+  #       if: always()
+  #       with:
+  #           name: apalache-check-inductive
+  #           path: |
+  #             _apalache-out/
+
+  apalache-simulate:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'microsoft'
+          java-version: '17'
+      - name: Setup
+        run: |
+          wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
+          tar zxvf apalache.tgz
+      - name: Simulation with Apalache
+        run: |
+          ./apalache/bin/apalache-mc simulate --config=APApbft.cfg --max-run=20 --length=25 APApbft.tla
+      - name: Upload Apalache's counterexample (if any)
+        uses: actions/upload-artifact@v4
+        if: always()
+        with:
+            name: apalache-simulate
+            path: |
+              _apalache-out/
+
+  apalache-simulate-geninit:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'microsoft'
+          java-version: '17'
+      - name: Setup
+        run: |
+          wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
+          tar zxvf apalache.tgz
+      - name: Simulation GenInit predicate with Apalache
+        run: |
+          ./apalache/bin/apalache-mc simulate --config=APApbft.cfg --init=GenInit --max-run=1 --length=1 APAIndpbft.tla
+      - name: Upload Apalache's counterexample (if any)
+        uses: actions/upload-artifact@v4
+        if: always()
+        with:
+            name: apalache-simulate-geninit
+            path: |
+              _apalache-out/
+
+  tlc-generate:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install TLA+ Tools
+        run: |
+          git clone https://github.com/pmer/tla-bin.git
+          cd tla-bin
+          ./download_or_update_tla.sh --nightly
+          sudo ./install.sh
+      - name: Random generation with TLC
+        run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -generate MCpbft.tla
+
+  tlc-simulate:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - name: Install TLA+ Tools
         run: |
           git clone https://github.com/pmer/tla-bin.git
           cd tla-bin
-          ./download_or_update_tla.sh
+          ./download_or_update_tla.sh --nightly
           sudo ./install.sh
-      - name: Sany
-        run: sany *.tla
-      - name: Random exploration with TLC
-        run: tlc -workers auto -simulate num=1000 MCpbft.tla
+      - name: Random simulation with TLC
+        run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -simulate MCpbft.tla

.gitignore

@@ -1,6 +1,7 @@
 ## TLA tools
 states/
 _apalache-out/
+.tlacache
 
 ## Core latex/pdflatex auxiliary files:
 *.aux

APAIndpbft.tla

@@ -0,0 +1,178 @@
+---- MODULE APAIndpbft ----
+\* PBFT model for checking with Apalache
+
+EXTENDS APApbft, Apalache
+
+MsgsConstraintEmpty ==
+    /\ msgs = [ 
+        request |-> [t : Tstamps],
+        preprepare |-> {},
+        prepare |-> {},
+        commit |-> {},
+        reply |-> {},
+        checkpoint |-> {},
+        viewchange |-> {},
+        newview |-> {}]
+
+MsgsConstraint ==
+    /\ \A r \in msgs.request :
+        /\ r.t \in Tstamps
+    /\ \A pp \in msgs.preprepare :
+        /\ pp.v \in Views
+        /\ pp.p \in R
+        /\ pp.n \in SeqNums
+        /\ pp.d \in RequestDigests
+    /\ \A p \in msgs.prepare :
+        /\ p.v \in Views
+        /\ p.i \in R
+        /\ p.n \in SeqNums
+        /\ p.d \in RequestDigests
+    /\ \A c \in msgs.commit :
+        /\ c.v \in Views
+        /\ c.i \in R
+        /\ c.n \in SeqNums
+        /\ c.d \in RequestDigests
+    /\ \A r \in msgs.reply :
+        /\ r.v \in Views
+        /\ r.i \in R
+        /\ r.t \in Tstamps
+        /\ r.r \in Results
+    /\ \A c \in msgs.checkpoint :
+        /\ c.n \in SeqNums
+        /\ c.d \in StateDigests
+        /\ c.i \in R
+    /\ \A v \in msgs.viewchange :
+        /\ v.v \in Views
+        /\ v.i \in R
+        /\ v.n \in SeqNums \union {0}
+        /\ \A c \in v.c : \* SUBSET CheckpointMessages
+            /\ c.n \in SeqNums
+            /\ c.d \in StateDigests
+            /\ c.i \in R
+        /\ \A p \in v.p : \* SUBSET PrepareProof
+                /\ p.preprepare.v \in Views
+                /\ p.preprepare.p \in R
+                /\ p.preprepare.n \in SeqNums
+                /\ p.preprepare.d \in RequestDigests
+                /\ \A p1 \in p.prepare : \* SUBSET PrepareMessages
+                    /\ p1.v \in Views
+                    /\ p1.i \in R
+                    /\ p1.n \in SeqNums
+                    /\ p1.d \in RequestDigests
+    /\ \A n \in msgs.newview :
+        /\ n.v \in Views
+        /\ n.p \in R
+        /\ \A v \in n.vc : \* SUBSET ViewChangeMessages
+            /\ v.v \in Views
+            /\ v.i \in R
+            /\ v.n \in SeqNums
+            /\ \A c \in v.c : \* SUBSET CheckpointMessages
+                /\ c.n \in SeqNums
+                /\ c.d \in StateDigests
+                /\ c.i \in R
+            /\ \A p \in v.p : \* SUBSET PrepareProof
+                /\ p.preprepare.v \in Views
+                /\ p.preprepare.p \in R
+                /\ p.preprepare.n \in SeqNums
+                /\ p.preprepare.d \in RequestDigests
+                /\ \A p1 \in p.prepare : \* SUBSET PrepareMessages
+                    /\ p1.v \in Views
+                    /\ p1.i \in R
+                    /\ p1.n \in SeqNums
+                    /\ p1.d \in RequestDigests
+        /\ \A pp \in n.o : \* SUBEST PrePrepareMessages
+            /\ pp.v \in Views
+            /\ pp.p \in R
+            /\ pp.n \in SeqNums
+            /\ pp.d \in RequestDigests    
+
+MlogsConstraintEmpty ==
+    /\ mlogs = [r \in R |-> [
+        request |-> {},
+        preprepare |-> {},
+        prepare |-> {},
+        commit |-> {},
+        reply |-> {},
+        checkpoint |-> {},
+        viewchange |-> {}]
+        ]
+
+MlogsConstraint ==
+    \* mlogs is defined for all replicas (outside of TLA+, one would call it a total function). Without this constraint, 
+    \* Apalache!Gen may generate a function that is not defined for all replicas.
+    /\ DOMAIN mlogs = R  
+    /\ \A rr \in DOMAIN mlogs :
+        /\ \A r \in mlogs[rr].request :
+            /\ r.t \in Tstamps
+        /\ \A pp \in mlogs[rr].preprepare :
+            /\ pp.v \in Views
+            /\ pp.p \in R
+            /\ pp.n \in SeqNums
+            /\ pp.d \in RequestDigests
+        /\ \A p \in mlogs[rr].prepare :
+            /\ p.v \in Views
+            /\ p.i \in R
+            /\ p.n \in SeqNums
+            /\ p.d \in RequestDigests
+        /\ \A c \in mlogs[rr].commit :
+            /\ c.v \in Views
+            /\ c.i \in R
+            /\ c.n \in SeqNums
+            /\ c.d \in RequestDigests
+        /\ \A r \in mlogs[rr].reply :
+            /\ r.v \in Views
+            /\ r.i \in R
+            /\ r.t \in Tstamps
+            /\ r.r \in Results
+        /\ \A c \in mlogs[rr].checkpoint :
+            /\ c.n \in SeqNums
+            /\ c.d \in StateDigests
+            /\ c.i \in R
+        /\ \A v \in mlogs[rr].viewchange :
+            /\ v.v \in Views
+            /\ v.i \in R
+            /\ v.n \in SeqNums \union {0}
+            /\ \A c \in v.c : \* SUBSET CheckpointMessages
+                /\ c.n \in SeqNums
+                /\ c.d \in StateDigests
+                /\ c.i \in R
+            /\ \A p \in v.p : \* SUBSET PrepareProof
+                    /\ p.preprepare.v \in Views
+                    /\ p.preprepare.p \in R
+                    /\ p.preprepare.n \in SeqNums
+                    /\ p.preprepare.d \in RequestDigests
+                    /\ \A p1 \in p.prepare : \* SUBSET PrepareMessages
+                        /\ p1.v \in Views
+                        /\ p1.i \in R
+                        /\ p1.n \in SeqNums
+                        /\ p1.d \in RequestDigests
+
+GenInit ==
+    /\ msgs = Gen(5)
+    /\ mlogs = Gen(5)
+    /\ views = Gen(10)
+    /\ states = Gen(10)
+    /\ sCheckpoint = Gen(10)
+    /\ vChange = Gen(10)
+
+    \* Apalache's documentation advises to conjoin TypeOK to GenInit to further constraint
+    \* the values generated by Gen.  This is necessary because Gen generates values that
+    \* satisfy Apalache's type system, but not necessarily the spec's TypeOK predicate.
+    \* /\ TypeOK
+    \* Unfortunately, Apalache explodes when it encounters the spec's TypeOK predicate 
+    \* because of multiple levels of nested subsets.  Therefore, we inline and partially
+    \* rewrite the definition of TypeOK into the following abomination.
+    /\ MsgsConstraint
+    /\ MlogsConstraint
+    \* TypeOK!3 to TypeOK!6 are inlined from the original TypeOK predicate
+    \* (! not supported by Apalache).
+    /\ views \in [R -> Views]
+    /\ states \in [R -> States]
+    /\ sCheckpoint \in [R -> SUBSET CheckpointMessages]
+    /\ vChange \in [R -> BOOLEAN]
+
+    /\ SafetyInv
+    \* /\ CommittedInv  \* Conjoining CommittedInv to GenInit causes a huge slowdown in Apalache.
+    \* /\ Inv    \* Inv is defined in terms of TypeOK and, thus, cannot be used in combination with Gen.
+
+====

APApbft.cfg

@@ -0,0 +1,20 @@
+\* Switched form  SPECIFICATION SpecByz  to  INIT/NEXT  because Apalache's command-line parameter
+\* --init  are no-ops with  SPECIFICATION SpecByz  .  However, our automation in tla.yml uses
+\* --init  to *redefine* the initial predicate.
+INIT Init
+NEXT NextByz
+
+CONSTANTS
+    R <- MC_R
+    ByzR <- MC_ByzR
+    Checkpoints <- MC_Checkpoints
+
+    \* Tstamp and Views have to be redefined to be small, finite sets due to Apalache limitations.
+    \* (compare https://github.com/heidihoward/pbft-tlaplus/issues/5#issuecomment-2315767599)
+    Tstamps <- MC_Tstamps
+    Views <- MC_Views
+
+INVARIANTS
+    TypeOK
+    SafetyInv
+    CommittedInv

APApbft.tla

@@ -1,3 +1,7 @@
+
+
+$ bin/apalache-mc check --config=APApbft.cfg --no-deadlock APApbft.tla
+
 ---- MODULE APApbft ----
 \* PBFT model for checking with Apalache
 
@@ -8,7 +12,7 @@ MC_R == 0..3
 
 \* Set of requests which are byzantine
 \* @type: Set(Int);
-MC_ByzR == {}
+MC_ByzR == {0}  \* Choose one replica to be byzantine.
 
 MC_Tstamps == 1..3
 
@@ -17,9 +21,8 @@ MC_Views == 0..2
 \* @type: Set(Int);
 MC_Checkpoints == {2}
 
-ConstInit ==
-    /\ ByzR = MC_ByzR
-    /\ R = MC_R
-    /\ Checkpoints = MC_Checkpoints
+\* Assume that the number of byzantine replicas is less than what the protocol can tolerate.
+\* See note of pbft!ByzR.
+ASSUME Cardinality(ByzR) <= F
 
 ====

MCpbft.cfg

@@ -1,8 +1,14 @@
 SPECIFICATION SpecByz
 
 CONSTANT 
-\*  Init <- MCInit
+    Init <- MCInit
     ViewChange <- MCViewChange
+    GenerateO <- MC_GenerateO
+
+    \* -simulate and -generate will encounter too large sets (subsets) unless those two
+    \* actions are redefined to randomly choose a smaller number of subsets.
+    InjectViewChange <- SimInjectViewChange
+    InjectNewView <- SimInjectNewView
 
 CONSTANTS
     R <- MC_R