THEOREM L_12 — H_StateMachineSafety

Status: ALL 138 OBLIGATIONS PROVED  |  54 unique proof steps  |  Prover: SMT (all)

TypeOK /\ H_CommittedEntryIsOnQuorum /\ H_StateMachineSafety /\ Next => H_StateMachineSafety'

THEOREM L_12 proved L1599
<1>. USE A0..A6 L1600
<1>1. ClientRequestAction smt proved L1602
<1>2. GetEntriesAction smt proved L1604
<1>3. RollbackEntriesAction smt proved L1606
<1>4. BecomeLeaderAction smt proved L1608
<1>5. CommitEntryAction proved L1610
<2>. SUFFICES ASSUME ... PROVE c1 = c2 smt L1611
<2>1. immediatelyCommitted' = ... ∪ {«Len(log[i]), currentTerm[i]»} smt L1619
<2>2. UNCHANGED «currentTerm, state, log» smt L1621
<2>3. CASE both old → by H_StateMachineSafety smt L1623
<2>4. CASE both new → trivially equal smt L1626
<2>5. CASE c1 old, c2 new → quorum intersection proved L1629
<3>1. ∃ Q: ∀ n ∈ Q: InLog(c1, n) smt L1631
<3>2. PICK Q1 smt L1633
<3>3. ∀ n ∈ commitQuorum: InLog(new, n) smt L1636
<3>4. IsFiniteSet(Server) smt L1639
<3>5. Q1, commitQuorum ⊆ Server smt L1640
<3>6. IsFiniteSet(Q1) ∧ IsFiniteSet(commitQuorum) smt L1642
<3>7. Cardinality types ∈ Nat smt L1644
<3>8. Quorum cardinality > |Server|/2 smt L1646
<3>9. |Q1| + |commitQuorum| > |Server| smt L1648
<3>10. Q1 ∩ commitQuorum ≠ {} smt L1650
<3>11. PICK n ∈ Q1 ∩ commitQuorum smt L1653
<3>12-16. InLog facts + index equality smt L1655-L1660
<3>17. c1[2] = currentTerm[i] smt L1661
<3>18-19. Tuple reconstruction from TypeOK smt L1662-L1663
<3>20. c1 = c2 smt L1664
<3>. QED smt L1665
<2>6. CASE c2 old, c1 new → symmetric quorum intersection proved L1667
<3>1-20. (symmetric to <2>5) smt L1669-L1698
<2>7. QED (exhaustive case split) smt L1700
<1>6. UpdateTermsAction smt proved L1702
<1>7. QED smt L1703

Proof Strategy

The key challenge is the CommitEntry action, which adds a new entry to immediatelyCommitted. The proof decomposes into four cases based on whether c1 and c2 are old (pre-existing) or new (just committed):

  1. Both old: Direct from induction hypothesis (H_StateMachineSafety).
  2. Both new: Trivially equal (same entry added).
  3. One old, one new: Quorum intersection argument. H_CommittedEntryIsOnQuorum provides a quorum for the old entry; the commit quorum witnesses the new entry. FS_MajoritiesIntersect gives a node in both quorums, where InLog forces the terms at the shared index to match, making the entries equal.

The tuple reconstruction step (c \in LogIndices × Terms ⇒ c = «c[1], c[2]») is needed because TLAPM cannot automatically reconstruct tuple equality from component equality.