Inductive invariant validation with Apalache.

* https://github.com/apalache-mc/apalache/blob/main/docs/src/apalache/known-issues.md#integer-ranges-with-non-constant-bounds
* apalache-mc/apalache#425
* apalache-mc/apalache#1431

Github issue #5
#5

[Apalache]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

APApbft.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION SpecByz
+
+CONSTANTS
+    R <- MC_R
+    ByzR <- MC_ByzR
+    Tstamps <- MC_Tstamps
+    Views <- MC_Views
+    Checkpoints <- MC_Checkpoints
+
+INVARIANTS
+    TypeOK
+    SafetyInv
+    CommittedInv

APApbft.tla

@@ -8,7 +8,7 @@ MC_R == 0..3
 
 \* Set of requests which are byzantine
 \* @type: Set(Int);
-MC_ByzR == {}
+MC_ByzR == MC_R
 
 MC_Tstamps == 1..3
 

MCpbft.cfg

@@ -3,6 +3,7 @@ SPECIFICATION SpecByz
 CONSTANT 
 \*  Init <- MCInit
     ViewChange <- MCViewChange
+    GenerateO <- MC_GenerateO
 
 CONSTANTS
     R <- MC_R

MCpbft.tla

@@ -89,4 +89,19 @@ MCInit ==
        \/ RInit
     /\ Inv
 
+-------
+
+\* This is Heidi's definition of GenerateO moved out of pbft. However, Apalache
+\* does not support  (mins+1)..maxs  when mins and maxs are non-constant.
+\* Moreover, Apalache does not support re-defining this non-zero arity operator,
+\* which is why the more complex definition is now in pbft and the simpler one
+\* below.
+\* @type: (Set ($viewchangeMsgs), Int, Int) => Set ($preprepareMsgs);
+MC_GenerateO(V,i,v) ==
+    LET mins == Max0(UNION {{cp.n: cp \in vcm.c}: vcm \in V}) 
+        ppms == UNION {{pp.preprepare: pp \in vcm.p}: vcm \in V}
+        maxs == Max0({ppm.n: ppm \in ppms}) IN
+    {[v |-> v, p |-> i, n |-> sn, d |-> GetDigest(ppms,sn)] : sn \in (mins+1)..maxs}
+
+
 =====

pbft.tla

@@ -591,8 +591,11 @@ GetDigest(ppms, sn) ==
 GenerateO(V,i,v) ==
     LET mins == Max0(UNION {{cp.n: cp \in vcm.c}: vcm \in V}) 
         ppms == UNION {{pp.preprepare: pp \in vcm.p}: vcm \in V}
-        maxs == Max0({ppm.n: ppm \in ppms}) IN
-    {[v |-> v, p |-> i, n |-> sn, d |-> GetDigest(ppms,sn)] : sn \in (mins+1)..maxs}
+        maxs == Max0({ppm.n: ppm \in ppms}) 
+        \* Apalache does not yet support integer ranges with non-constant bounds:
+        \* https://github.com/apalache-mc/apalache/blob/main/docs/src/apalache/known-issues.md#integer-ranges-with-non-constant-bounds
+        apa == { j \in Views : mins+1 <= j /\ j <= maxs} IN
+    {[v |-> v, p |-> i, n |-> sn, d |-> GetDigest(ppms,sn)] : sn \in apa }
 
 \* Castro & Liskov S4.4: 
     \* When the primary p of view v+1 receives 2f valid view-change messages for view v+1 from other replicas, it multicasts a (NEW-VIEW,v+1,V,O) message to all other replicas, where V is a set containing the valid view-change messages received by the primary plus the view-change message for v+1 the primary sent (or would have sent), and is a set of pre-prepare messages (without the piggybacked request).