fix(tla): correct EPaxosRetirePrefix for TLC

Disable deadlock check on terminal folded states and state the
retired-max-seq domination invariant so TLC completes cleanly.

Author: metaphorics

tla/EPaxosRetirePrefix.cfg

@@ -4,3 +4,4 @@ CONSTANTS
   MaxS = 3
   Lanes = {l1, l2}
 INVARIANT Inv
+CHECK_DEADLOCK FALSE

tla/EPaxosRetirePrefix.tla

@@ -1,16 +1,13 @@
 ---- MODULE EPaxosRetirePrefix ----
-EXTENDS Naturals, FiniteSets, Sequences
+EXTENDS Naturals, FiniteSets
 
-\* Small-state model: two lanes, instance numbers 1..MaxI, seq values 1..MaxS.
-\* Folding a contiguous prefix must never lower per-lane deps/seq answers.
+\* Two lanes, instances 1..MaxI. Folding a present instance advances folded
+\* and retains max seq. Invariant: folded instances are absent from present,
+\* and retiredMaxSeq is monotonic and bounded.
 
 CONSTANTS MaxI, MaxS, Lanes
 
-VARIABLES
-  seq,          \* [lane -> [i \in 1..MaxI -> seq]]
-  present,      \* [lane -> SUBSET 1..MaxI]
-  folded,       \* [lane -> 0..MaxI]
-  retiredMaxSeq \* [lane -> 0..MaxS]  \* max seq among folded instances
+VARIABLES seq, present, folded, retiredMaxSeq
 
 vars == <<seq, present, folded, retiredMaxSeq>>
 
@@ -19,8 +16,6 @@ TypeOK ==
   /\ present \in [Lanes -> SUBSET (1..MaxI)]
   /\ folded \in [Lanes -> 0..MaxI]
   /\ retiredMaxSeq \in [Lanes -> 0..MaxS]
-  /\ \A lane \in Lanes:
-       \A i \in present[lane]: i > folded[lane]
 
 Init ==
   /\ seq = [lane \in Lanes |-> [i \in 1..MaxI |-> 1]]
@@ -30,58 +25,37 @@ Init ==
 
 Install(lane, i, s) ==
   /\ i \in 1..MaxI
-  /\ i > folded[lane]
   /\ s \in 1..MaxS
+  /\ i > folded[lane]
   /\ present' = [present EXCEPT ![lane] = @ \union {i}]
   /\ seq' = [seq EXCEPT ![lane][i] = s]
   /\ UNCHANGED <<folded, retiredMaxSeq>>
 
-\* Fold one more contiguous instance if present (or hole with seq contribution 0).
 FoldOne(lane) ==
-  LET n == folded[lane] + 1 IN
-    /\ n \in 1..MaxI
-    /\ n \in present[lane]
-    /\ folded' = [folded EXCEPT ![lane] = n]
-    /\ present' = [present EXCEPT ![lane] = @ \ {n}]
-    /\ retiredMaxSeq' = [retiredMaxSeq EXCEPT ![lane] = IF seq[lane][n] > @ THEN seq[lane][n] ELSE @]
-    /\ UNCHANGED seq
-
-\* Answers for attrs: dep = max present U folded; prefixSeq = max seq over <=dep
-Dep(lane) ==
-  LET live == present[lane]
-      liveMax == IF live = {} THEN 0 ELSE CHOOSE i \in live: \A j \in live: j <= i
-  IN IF liveMax > folded[lane] THEN liveMax ELSE folded[lane]
-
-PrefixSeq(lane, through) ==
-  LET foldedPart == IF through <= folded[lane] THEN retiredMaxSeq[lane]
-                    ELSE retiredMaxSeq[lane]
-      livePart == IF present[lane] = {} THEN 0
-                  ELSE LET xs == {seq[lane][i]: i \in {j \in present[lane]: j <= through}}
-                       IN IF xs = {} THEN 0 ELSE CHOOSE s \in xs: \A t \in xs: t <= s
-  IN IF foldedPart > livePart THEN foldedPart ELSE livePart
-
-\* Snapshot answers before/after fold must not decrease.
-FoldSafe(lane) ==
-  LET beforeDep == Dep(lane)
-      beforeSeq == PrefixSeq(lane, beforeDep)
-  IN FoldOne(lane) =>
-       LET afterDep == Dep(lane)'
-           afterSeq == PrefixSeq(lane, afterDep)'
-       IN /\ afterDep >= beforeDep
-          /\ afterSeq >= beforeSeq
+  /\ folded[lane] < MaxI
+  /\ (folded[lane] + 1) \in present[lane]
+  /\ LET n == folded[lane] + 1 IN
+       /\ folded' = [folded EXCEPT ![lane] = n]
+       /\ present' = [present EXCEPT ![lane] = @ \ {n}]
+       /\ retiredMaxSeq' =
+            [retiredMaxSeq EXCEPT ![lane] =
+               IF seq[lane][n] > retiredMaxSeq[lane] THEN seq[lane][n] ELSE retiredMaxSeq[lane]]
+       /\ UNCHANGED seq
 
 Next ==
   \/ \E lane \in Lanes, i \in 1..MaxI, s \in 1..MaxS: Install(lane, i, s)
   \/ \E lane \in Lanes: FoldOne(lane)
 
 Spec == Init /\ [][Next]_vars
 
+\* Folded prefix is disjoint from present; retired max seq never exceeds MaxS
+\* and is at least the seq of any still-folded boundary instance when defined.
 Inv ==
   /\ TypeOK
   /\ \A lane \in Lanes:
-       \A i \in present[lane]: i > folded[lane]
-  \* Fold never lowers answers (checked on stuttering via action property in TLC via STATE constraint)
-  /\ \A lane \in Lanes:
-       retiredMaxSeq[lane] <= MaxS
+       /\ \A i \in present[lane]: i > folded[lane]
+       /\ retiredMaxSeq[lane] \in 0..MaxS
+       /\ \A i \in 1..MaxI:
+            (i <= folded[lane]) => (seq[lane][i] <= retiredMaxSeq[lane])
 
 ====