THEOREM L_7 — H_TermsMonotonic

Status: ALL 227 OBLIGATIONS PROVED  |  6 top-level action cases + 1 QED  |  Provers: SMT, trivial (tlapm)  |  TLAPM 1.5.0 • 8 threads
Proved: 2026-04-03 15:04–15:12 (approx. 8 min total across 6 runs) • Final run: tlapm --threads 8 --toolbox 858 994 AbstractRaft_IndProofs_test.tla

TypeOK /\ H_PrimaryTermGTELogTerm /\ H_TermsMonotonic /\ Next => H_TermsMonotonic'

THEOREM L_7 proved L858 227 obligations
<1>. USE A0, A1, A2, A3, A4, A5, A6 trivial L859
<1>1. TypeOK /\ H_PrimaryTermGTELogTerm /\ H_TermsMonotonic /\ ClientRequestAction => H_TermsMonotonic' proved L861
<2>. SUFFICES ASSUME TypeOK, H_PrimaryTermGTELogTerm, H_TermsMonotonic,
                 NEW p ∈ Server, ClientRequest(p), NEW sv, ii, jj, ii ≤ jj
                 PROVE log'[sv][ii] ≤ log'[sv][jj] smt L862–867
<2>1. log' = [log EXCEPT ![p] = Append(log[p], currentTerm[p])] smt L868
<2>a. log'[p] = Append(log[p], currentTerm[p]) smt L869
<2>b. ∀ idx ∈ 1..Len(log[p]): log'[p][idx] = log[p][idx] smt L870
<2>c. log'[p][Len(log[p])+1] = currentTerm[p] smt L871
<2>d. DOMAIN log[p] = 1..Len(log[p]) smt L872
<2>e. DOMAIN log'[p] = 1..(Len(log[p])+1) smt L873
<2>2. CASE sv ≠ p smt L874–875
<2>3. CASE sv = p proved L876
<3>1. CASE ii ∈ DOMAIN log[p] /\ jj ∈ DOMAIN log[p] smt L877–878 — by H_TermsMonotonic directly
<3>2. CASE ii ∈ DOMAIN log[p] /\ jj ∉ DOMAIN log[p] proved L879 — jj = Len+1; use H_PrimaryTermGTELogTerm
<4>1. jj = Len(log[p]) + 1 smt L882
<4>2. log'[p][jj] = currentTerm[p] smt L883
<4>3. log'[p][ii] = log[p][ii] smt L884
<4>4. state[p] = Primary smt L885
<4>5. log[p][ii] ≤ currentTerm[p] smt L886–887 — H_PrimaryTermGTELogTerm
<4>6. log'[sv][ii] ≤ log'[sv][jj] smt L888–889
<4>. QED smt L890
<3>3. CASE ii ∉ DOMAIN log[p] /\ jj ∉ DOMAIN log[p] proved L891 — both = Len+1, so ii = jj
<4>1. ii = Len(log[p]) + 1 smt L893
<4>2. jj = Len(log[p]) + 1 smt L894
<4>3. ii = jj smt L895
<4>4. log'[sv][ii] = log'[sv][jj] smt L896
<4>5. log'[p][ii] = currentTerm[p] smt L897
<4>6. currentTerm[p] ∈ Nat smt L898
<4>. QED smt L899
<3>4. CASE ii ∉ DOMAIN log[p] /\ jj ∈ DOMAIN log[p] proved L900 — contradiction: ii = Len+1 > jj violates ii ≤ jj
<4>1. ii = Len(log[p]) + 1 smt L902
<4>2. jj ∈ 1..Len(log[p]) smt L903
<4>. QED (contradiction) smt L904
<3>. QED (case split on domain membership) smt L905
<2>. QED BY <2>2, <2>3 smt L906
<1>2. TypeOK /\ H_TermsMonotonic /\ GetEntriesAction => H_TermsMonotonic' proved L908 — most complex case; chained monotonicity argument
<2>. SUFFICES ASSUME TypeOK, H_TermsMonotonic,
                 NEW r, sender, GetEntries(r, sender), NEW sv, ii, jj, ii ≤ jj
                 PROVE log'[sv][ii] ≤ log'[sv][jj] smt L909–914
<2>1. log' = [log EXCEPT ![r] = Append(log[r], log[sender][Len(log[r])+1])] smt L915–916
<2>a. log'[r] = Append(log[r], log[sender][...]) smt L917–918
<2>b. ∀ idx ∈ 1..Len(log[r]): log'[r][idx] = log[r][idx] smt L919
<2>c. DOMAIN log[r] = 1..Len(log[r]) trivial L920
<2>d. DOMAIN log'[r] = 1..(Len(log[r])+1) smt L921
<2>e. (IF Empty(log[r]) THEN 1 ELSE Len(log[r])+1) = Len(log[r])+1 smt L922–923
<2>f. log'[r][Len(log[r])+1] = log[sender][Len(log[r])+1] smt L924–925
<2>g. Len(log[sender]) > Len(log[r]) smt L926
<2>h. ¬Empty(log[r]) ⇒ log[sender][Len(log[r])] = log[r][Len(log[r])] smt L927–928
<2>2. CASE sv ≠ r smt L929–930
<2>3. CASE sv = r proved L931
<3>1. CASE ii ∈ DOMAIN log[r] /\ jj ∈ DOMAIN log[r] smt L932–933 — direct from H_TermsMonotonic
<3>2. CASE ii ∈ DOMAIN log[r] /\ jj ∉ DOMAIN log[r] proved L934 — new entry from sender; chain monotonicity
<4>1. jj = Len(log[r]) + 1 smt L939
<4>2. log'[r][jj] = log[sender][Len(log[r])+1] smt L940
<4>3. log'[r][ii] = log[r][ii] smt L941
<4>4. CASE Empty(log[r]) — contradiction (ii ∈ DOMAIN log[r]) smt L942–944
<4>5. CASE ¬Empty(log[r]) — chained inequality proved L945
<5>1. Len(log[r]) ∈ DOMAIN log[r] smt L946–947
<5>2. ii ∈ 1..Len(log[r]) smt L948
<5>3. log[r][ii] ≤ log[r][Len(log[r])] smt L949–950 — H_TermsMonotonic on r
<5>4. log[sender][Len(log[r])] = log[r][Len(log[r])] smt L951–952 — from GetEntries logOk
<5>5. Len(log[r]) ≥ 1 smt L953–954
<5>6. Len(log[r]) ∈ DOMAIN log[sender] smt L955–956
<5>7. Len(log[r])+1 ∈ DOMAIN log[sender] smt L957–958
<5>8. log[sender][Len(log[r])] ≤ log[sender][Len(log[r])+1] smt L959–960 — H_TermsMonotonic on sender
<5>9. log[r][Len(log[r])] ≤ log[sender][Len(log[r])+1] smt L961–962
<5>10. Nat type witnesses smt L963–964
<5>11. log[r][ii] ≤ log[sender][Len(log[r])+1] smt L965–966 — transitivity
<5>12. log'[sv][ii] ≤ log'[sv][jj] smt L967–968
<5>. QED smt L969
<4>. QED smt L970
<3>3. CASE ii ∉ DOMAIN log[r] /\ jj ∉ DOMAIN log[r] proved L971 — both = Len+1, trivially equal
<4>1. ii = Len(log[r]) + 1 smt L972
<4>2. jj = Len(log[r]) + 1 smt L973
<4>3. ii = jj smt L974
<4>4. log'[sv][ii] = log'[sv][jj] smt L975
<4>5. log'[r][ii] = log[sender][Len(log[r])+1] smt L976
<4>6. log[sender][Len(log[r])+1] ∈ Nat smt L977–978
<4>. QED smt L979
<3>4. CASE ii ∉ DOMAIN log[r] /\ jj ∈ DOMAIN log[r] proved L980 — contradiction: ii = Len+1 > jj violates ii ≤ jj
<4>1. ii = Len(log[r]) + 1 smt L981
<4>2. jj ∈ 1..Len(log[r]) smt L982
<4>. QED (contradiction) smt L983
<3>. QED smt L984
<2>. QED BY <2>2, <2>3 smt L985
<1>3. TypeOK /\ H_TermsMonotonic /\ RollbackEntriesAction => H_TermsMonotonic' smt proved L987 — BY DEF TypeOK, RollbackEntriesAction, RollbackEntries, H_TermsMonotonic
<1>4. TypeOK /\ H_TermsMonotonic /\ BecomeLeaderAction => H_TermsMonotonic' smt proved L989 — BY DEF TypeOK, BecomeLeaderAction, BecomeLeader, H_TermsMonotonic
<1>5. TypeOK /\ H_TermsMonotonic /\ CommitEntryAction => H_TermsMonotonic' smt proved L991 — BY DEF TypeOK, CommitEntryAction, CommitEntry, H_TermsMonotonic
<1>6. TypeOK /\ H_TermsMonotonic /\ UpdateTermsAction => H_TermsMonotonic' smt proved L993 — BY DEF TypeOK, UpdateTermsAction, UpdateTerms, H_TermsMonotonic
<1>7. QED smt proved L994 — BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6 DEF Next

Proof Strategy

H_TermsMonotonic asserts that for every server sv, the term sequence log[sv] is monotonically non-decreasing: ∀ i ≤ j ∈ DOMAIN log[sv]: log[sv][i] ≤ log[sv][j]. The proof proceeds by case analysis over each action in Next.

  1. RollbackEntries, BecomeLeader, CommitEntry, UpdateTerms (steps <1>3–<1>6): None of these actions modify log in a way that can decrease an entry, so the invariant is preserved trivially via definitional unfolding. SMT discharges these in a single step.
  2. ClientRequest (step <1>1): The only log change is appending currentTerm[p] to server p's log. The proof splits into four domain-membership cases for indices ii, jj:
  3. GetEntries (step <1>2): The hardest case. Server r appends one entry from sender at position Len(log[r])+1. The proof again uses four domain cases. The critical sub-case is ii old, jj new, requiring: log[r][ii] ≤ log[sender][Len(log[r])+1]. This is established by chaining two applications of H_TermsMonotonic: Transitivity (with explicit Nat witnesses for SMT) closes the goal.

Proof Metrics

Step Action Prover Status Timing
<1>1 ClientRequestAction smt proved cached
<1>2 GetEntriesAction smt proved ~8 min (multi-run)
<1>3 RollbackEntriesAction smt proved cached
<1>4 BecomeLeaderAction smt proved cached
<1>5 CommitEntryAction smt proved cached
<1>6 UpdateTermsAction smt proved cached
Total: 227 obligations smt + trivial ALL PROVED ~8 min total

Generated 2026-04-03 • TLAPM 1.5.0 • 8 threads • Final run: tlapm --threads 8 --toolbox 858 994 AbstractRaft_IndProofs_test.tla • All 227 obligations proved (6 runs, 15:04–15:12)