Check refinement of high-level spec abs with all models (#6509)

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>

tla/consensus/MCabs.cfg

@@ -6,14 +6,23 @@ CONSTANTS
     NodeThree = n3
     Servers <- MCServers
     Terms <- MCTerms
-    MaxLogLength <- MCMaxLogLength
+    Seq <- MCSeq
+    TypeOK <- MCTypeOK
 
 INVARIANTS
     NoConflicts
     TypeOK
 
 PROPERTIES 
     AppendOnlyProp
+    \* EquivExtendProp
+    \* EquivCopyMaxAndExtendProp
 
 SYMMETRY 
-    Symmetry
+    Symmetry
+
+CONSTRAINT 
+    MaxLogLengthConstraint
+
+CHECK_DEADLOCK 
+    FALSE

tla/consensus/MCabs.tla

@@ -1,6 +1,6 @@
 ---- MODULE MCabs ----
 
-EXTENDS abs, TLC
+EXTENDS abs, TLC, SequencesExt
 
 Symmetry ==
       Permutations(Servers)
@@ -9,6 +9,17 @@ CONSTANTS NodeOne, NodeTwo, NodeThree
 
 MCServers == {NodeOne, NodeTwo, NodeThree}
 MCTerms == 2..4
-MCMaxLogLength == 7
+MaxExtend == 3
 
+MCTypeOK ==
+    \* 4 because of the initial log.
+    cLogs \in [Servers -> BoundedSeq(Terms, 4 + MaxExtend)]
+
+MCSeq(S) ==
+    BoundedSeq(S, MaxExtend)
+
+\* Limit length of logs to terminate model checking.
+MaxLogLengthConstraint ==
+    \A i \in Servers :
+        Len(cLogs[i]) <= 7
 ====

tla/consensus/MCccfraft.cfg

@@ -44,6 +44,10 @@ CONSTANTS
     NodeTwo = n2
     NodeThree = n3
 
+    RefinementToAbsProp <- MCRefinementToAbsProp
+    Extend <- [abs]ABSExtend
+    CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
+
 SYMMETRY Symmetry
 VIEW View
 
@@ -68,8 +72,7 @@ PROPERTIES
     MembershipStateTransitionsProp
     PendingBecomesFollowerProp
     NeverCommitEntryPrevTermsProp
-    \* Will be checked after https://github.com/microsoft/CCF/pull/6509
-    \* RefinementToAbsProp
+    RefinementToAbsProp
 
 INVARIANTS
     LogInv

tla/consensus/MCccfraft.tla

@@ -174,17 +174,8 @@ PostConditions ==
 ----
 \* Refinement
 
-\* The inital log is up to 4 entries long + one log entry per request/reconfiguration + one signature per request/reconfiguration or new view (no consecutive sigs except across views)
-MaxLogLength == 
-    4 + ((RequestCount + Len(Configurations)) * 2) + TermCount
-
-MappingToAbs == 
-  INSTANCE abs WITH
-    Servers <- Servers,
-    Terms <- StartTerm..(StartTerm + TermCount),
-    MaxLogLength <- MaxLogLength,
-    cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
-
-RefinementToAbsProp == MappingToAbs!AbsSpec
+MCRefinementToAbsProp == MappingToAbs(StartTerm..StartTerm + TermCount)!AbsSpec
 
+ABSExtend(i) == MappingToAbs(StartTerm..StartTerm + TermCount)!ExtendAxiom(i)
+ABSCopyMaxAndExtend(i) == MappingToAbs(StartTerm..StartTerm + TermCount)!CopyMaxAndExtendAxiom(i)
 ===================================

tla/consensus/SIMccfraft.cfg

@@ -48,6 +48,10 @@ CONSTANTS
 
     InitReconfigurationVars <- SIMInitReconfigurationVars
 
+    RefinementToAbsProp <- MCRefinementToAbsProp
+    Extend <- [abs]ABSExtend
+    CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
+
 CONSTRAINT
     StopAfter
 
@@ -63,6 +67,7 @@ PROPERTIES
     MembershipStateTransitionsProp
     PendingBecomesFollowerProp
     NeverCommitEntryPrevTermsProp
+    RefinementToAbsProp
 
 POSTCONDITION
     WriteStatsFile

tla/consensus/SIMccfraft.tla

@@ -44,6 +44,15 @@ DebugInvUpToDepth ==
     \* The following invariant causes TLC to terminate with a counterexample of length
     \* -depth after generating the first trace.
     TLCGet("level") < TLCGet("config").depth
+
+----
+\* Refinement
+
+MCRefinementToAbsProp == MappingToAbs(Nat \ 0..StartTerm-1)!AbsSpec
+
+ABSExtend(i) == MappingToAbs(Nat \ 0..StartTerm-1)!ExtendAxiom(i)
+ABSCopyMaxAndExtend(i) == MappingToAbs(Nat \ 0..StartTerm-1)!CopyMaxAndExtendAxiom(i)
+
 =============================================================================
 
 ------------------------------- MODULE SIMPostCondition -------------------------------

tla/consensus/abs.tla

@@ -12,9 +12,6 @@ CONSTANT Terms
 ASSUME /\ IsStrictlyTotallyOrderedUnder(<, Terms) 
        /\ \E min \in Terms : \A t \in Terms : t <= min
 
-CONSTANT MaxLogLength
-ASSUME MaxLogLength \in Nat
-
 \* Commit logs from each node
 \* Each log is append-only and the logs will never diverge.
 VARIABLE cLogs
@@ -37,22 +34,65 @@ Copy(i) ==
         /\ \E l \in 1..(Len(cLogs[j]) - Len(cLogs[i])) : 
                 cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]
 
-\* A node i with the longest log can extend its log upto length k.
-Extend(i, k) ==
+\* A node i with the longest log can non-deterministically extend
+\* its log by any finite number of log entries.  An implementation
+\* may choose a particular number of log entries by which to extend
+\* the log to prevent the leader from racing ahead of the followers.
+Extend(i) ==
     /\ \A j \in Servers : Len(cLogs[j]) \leq Len(cLogs[i])
-    /\ \E l \in 0..(k - Len(cLogs[i])) : 
-        \E s \in [1..l -> Terms] :
+    /\ \E s \in Seq(Terms) :
             cLogs' = [cLogs EXCEPT ![i] = @ \o s]
 
-ExtendToMax(i) == Extend(i, MaxLogLength)
+ExtendAxiom(i) ==
+    \* i has the longest log.
+    /\ \A j \in Servers : Len(cLogs[j]) \leq Len(cLogs[i])
+    \* cLogs remains a function mapping from servers to logs.
+    /\ cLogs' \in [Servers -> Seq(Terms)]
+    \* i *extends* its log
+    /\ IsPrefix(cLogs[i], cLogs'[i])
+    \* The other logs remain the same.
+    /\ \A j \in Servers \ {i} : cLogs'[j] = cLogs[j]
+
+\* Extend and ExtendAxiom are logically equivalent definitions.  However,
+\* TLC can check ExtendAxiom more efficiently when checking refinement,
+\* due to the absence of the existential quantifier in the definition.
+\* The same is true for CopyMaxAndExtend and CopyMaxAndExtendAxiom below.
+LEMMA ASSUME NEW i \in Servers PROVE
+    ExtendAxiom(i) <=> Extend(i)
+OMITTED 
+
+\* Copy one of the longest logs (from whoever server
+\* has it) and extend it further upto length k. This
+\* is equivalent to  Copy(i) \cdot Extend(i, k)  ,
+\* that TLC cannot handle.
+CopyMaxAndExtend(i) ==
+    \E j \in Servers :
+        /\ \A r \in Servers: Len(cLogs[r]) \leq Len(cLogs[j])
+        /\ \E s \in Seq(Terms) :
+            cLogs' = [cLogs EXCEPT ![i] = cLogs[j] \o s]
+
+CopyMaxAndExtendAxiom(i) ==
+    \E s \in Servers :
+        /\ \A r \in Servers: Len(cLogs[r]) \leq Len(cLogs[s])
+        \* cLogs remains a function mapping from servers to logs.
+        /\ cLogs' \in [Servers -> Seq(Terms)]
+        \* i *extends* s' log
+        /\ IsPrefix(cLogs[s], cLogs'[i])
+        \* The other logs remain the same.
+        /\ \A j \in Servers \ {i} : cLogs'[j] = cLogs[j]
+
+LEMMA ASSUME NEW i \in Servers PROVE
+    CopyMaxAndExtendAxiom(i) <=> CopyMaxAndExtend(i)
+OMITTED 
 
 \* The only possible actions are to append log entries.
 \* By construction there cannot be any conflicting log entries
 \* Log entries are copied if the node's log is not the longest.
 Next ==
     \E i \in Servers : 
         \/ Copy(i) 
-        \/ ExtendToMax(i)
+        \/ ExtendAxiom(i)
+        \/ CopyMaxAndExtendAxiom(i)
 
 AbsSpec == Init /\ [][Next]_cLogs
 
@@ -64,4 +104,11 @@ NoConflicts ==
         \/ IsPrefix(cLogs[i], cLogs[j]) 
         \/ IsPrefix(cLogs[j], cLogs[i])
 
+EquivExtendProp ==
+    [][\A i \in Servers : 
+        Extend(i) <=> ExtendAxiom(i)]_cLogs
+
+EquivCopyMaxAndExtendProp ==
+    [][\A i \in Servers : 
+        CopyMaxAndExtend(i) <=> CopyMaxAndExtendAxiom(i)]_cLogs
 ====

tla/consensus/ccfraft.tla

@@ -1620,6 +1620,20 @@ LogMatchingProp ==
 LeaderProp ==
     []<><<\E i \in Servers : leadershipState[i] = Leader>>_vars
 
+------------------------------------------------------------------------------
+\* Refinement of the more high-level specification abs.tla that abstracts the
+\* asynchronous network and the message passing between nodes.  Instead, any
+\* node may atomically observe the state of any other node.
+
+MappingToAbs(T) == 
+  INSTANCE abs WITH
+    Servers <- Servers,
+    Terms <- T,
+    cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
+
+RefinementToAbsProp == \EE T : MappingToAbs(T)!AbsSpec
+THEOREM Spec => RefinementToAbsProp
+
 ------------------------------------------------------------------------------
 \* Debugging invariants
 \* These invariants should give error traces and are useful for debugging to see if important situations are possible