When checking refinement, prevent TLC from enumerating the set of suf…

…fixes by expressing abs!Extend and abs!CopyMaxAndExtend axiomatically. Signed-off-by: Markus Alexander Kuppe <[email protected]>
microsoft · Sep 27, 2024 · 6a41bd4 · 6a41bd4
1 parent 5fa6c46
commit 6a41bd4
Show file tree

Hide file tree

Showing 9 changed files with 56 additions and 0 deletions.
diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
@@ -14,6 +14,8 @@ INVARIANTS
 
 PROPERTIES 
     AppendOnlyProp
+    \* EquivExtendProp
+    \* EquivCopyMaxAndExtendProp
 
 SYMMETRY 
     Symmetry

diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -51,6 +51,8 @@ CONSTANTS
     NodeThree = n3
 
     RefinementToAbsProp <- MCRefinementToAbsProp
+    Extend <- [abs]ABSExtend
+    CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
 
 SYMMETRY Symmetry
 VIEW View

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -136,4 +136,6 @@ MaxLogLength ==
 
 MCRefinementToAbsProp == MappingToAbs(StartTerm..MaxTermLimit, MaxLogLength)!AbsSpec
 
+ABSExtend(i) == MappingToAbs(StartTerm..MaxTermLimit, MaxLogLength)!ExtendAxiom(i)
+ABSCopyMaxAndExtend(i) == MappingToAbs(StartTerm..MaxTermLimit, MaxLogLength)!CopyMaxAndExtendAxiom(i)
 ===================================
diff --git a/tla/consensus/MCccfraft2Nodes.cfg b/tla/consensus/MCccfraft2Nodes.cfg
@@ -51,6 +51,8 @@ CONSTANTS
     NodeThree = n3
 
     RefinementToAbsProp <- MCRefinementToAbsProp
+    Extend <- [abs]ABSExtend
+    CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
 
 SYMMETRY Symmetry
 VIEW View

diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg
@@ -53,6 +53,8 @@ CONSTANTS
     NodeThree = n3
 
     RefinementToAbsProp <- MCRefinementToAbsProp
+    Extend <- [abs]ABSExtend
+    CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
 
 SYMMETRY Symmetry
 VIEW View

diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -52,6 +52,8 @@ CONSTANTS
     NodeThree = n3
 
     RefinementToAbsProp <- MCRefinementToAbsProp
+    Extend <- [abs]ABSExtend
+    CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
 
 SYMMETRY Symmetry
 VIEW View

diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -49,6 +49,8 @@ CONSTANTS
     InitReconfigurationVars <- SIMInitReconfigurationVars
 
     RefinementToAbsProp <- MCRefinementToAbsProp
+    Extend <- [abs]ABSExtend
+    CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
 
 CONSTRAINT
     StopAfter

diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -50,6 +50,9 @@ DebugInvUpToDepth ==
 
 MCRefinementToAbsProp == MappingToAbs(StartTerm..100, 100)!AbsSpec
 
+ABSExtend(i) == MappingToAbs(Nat \ 0..StartTerm-1, 100)!ExtendAxiom(i)
+ABSCopyMaxAndExtend(i) == MappingToAbs(Nat \ 0..StartTerm-1, 100)!CopyMaxAndExtendAxiom(i)
+
 =============================================================================
 
 ------------------------------- MODULE SIMPostCondition -------------------------------

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
@@ -49,6 +49,22 @@ Extend(i) ==
     /\ \E s \in BoundedSeq(Terms, MaxUncommittedCount) :
             cLogs' = [cLogs EXCEPT ![i] = @ \o s]
 
+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 by at most k entries.
+    /\ Len(cLogs'[i]) <= Len(cLogs[i]) + MaxUncommittedCount
+    \* i *extends* its log
+    /\ IsPrefix(cLogs[i], cLogs'[i])
+    \* The other logs remain the same.
+    /\ \A j \in Servers \ {i} : cLogs'[j] = cLogs[j]
+
+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)  ,
@@ -59,6 +75,22 @@ CopyMaxAndExtend(i) ==
         /\ \E s \in BoundedSeq(Terms, MaxUncommittedCount) :
             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 by at most k entries.
+        /\ Len(cLogs'[i]) <= Len(cLogs[s]) + MaxUncommittedCount
+        \* 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.
@@ -78,4 +110,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
 ====