THEOREM L_6 — H_UniformLogEntries

Status: ALL OBLIGATIONS PROVED  |  6 top-level action sub-goals  |  Lines 464–854  |  Prover: SMT (leaf steps), tlapm (trivial/QED)  |  Timing: cached

TypeOK /\ H_PrimaryHasOwnEntries /\ H_LogMatching /\ H_UniformLogEntries /\ Next => H_UniformLogEntries'

THEOREM L_6 proved L464
<1>. USE A0..A6 tlapm L465
<1>1. TypeOK /\ H_PrimaryHasOwnEntries /\ H_UniformLogEntries /\ ClientRequestAction => H_UniformLogEntries' proved L467
<2>. SUFFICES ASSUME TypeOK, H_PrimaryHasOwnEntries, H_UniformLogEntries, ClientRequest(p), ... PROVE ~(k < i) smt L468–475
<2>1. log' = [log EXCEPT ![p] = Append(log[p], currentTerm[p])] smt L476
<2>2. state[p] = Primary smt L477
<2>3. H_PrimaryHasOwnEntries: any server with currentTerm[p] in its log has it in log[p] too smt L478–479
<2>a. log'[p] = Append(log[p], currentTerm[p]) smt L481–482
<2>b. ∀ srv ≠ p: log'[srv] = log[srv] smt L483–484
<2>c. DOMAIN log'[p] = 1..(Len(log[p])+1) smt L485–486
<2>d. ∀ idx ∈ 1..Len(log[p]) : log'[p][idx] = log[p][idx] smt L487–488
<2>e. log'[p][Len(log[p])+1] = currentTerm[p] smt L489–490
<2>f. DOMAIN log[p] = 1..Len(log[p]) smt L491–492
<2>6. CASE s ≠ p /\ t ≠ p smt L493–494
<2>7. CASE s = p /\ t ≠ p proved L495
<3>a. log'[t][k] = log'[p][i] tlapm L497
<3>b. uniqueness in log'[p] tlapm L498
<3>1. CASE i ∈ DOMAIN log[p] (old entry) proved L499
<4>1. log'[p][i] = log[p][i] smt L501
<4>2. log'[t][k] = log[t][k] smt L502
<4>3. k ∈ DOMAIN log[t] smt L503
<4>4. log[t][k] = log[p][i] smt L504–505
<4>5. uniqueness lifts to pre-state log[p] proved L506
<5>. SUFFICES ASSUME j ∈ DOMAIN log[p], j < i PROVE log[p][j] ≠ log[p][i] tlapm L507
<5>1. j ∈ DOMAIN log'[p] smt L508
<5>2. log'[p][j] = log[p][j] smt L509
<5>3. log'[p][j] ≠ log'[p][i] smt L510
<5>. QED smt L511
<4>. QED by H_UniformLogEntries smt L512
<3>2. CASE i ∉ DOMAIN log[p] (new entry = currentTerm[p]) proved L513
<4>1. i = Len(log[p]) + 1 smt L516–517
<4>2. log'[p][i] = currentTerm[p] smt L518–519
<4>3. log'[t][k] = log[t][k] smt L520
<4>4. k ∈ DOMAIN log[t] smt L521
<4>5. log[t][k] = currentTerm[p] smt L522–523
<4>6. k ∈ DOMAIN log[p] /\ log[p][k] = currentTerm[p] (H_PrimaryHasOwnEntries) smt L524–525
<4>7–10. log'[p][k] = currentTerm[p] = log'[p][i] smt L526–531
<4>11. k < i => log'[p][k] ≠ log'[p][i] (uniqueness) smt L534–535
<4>. QED: contradiction k < i with equality smt L536
<3>. QED smt L537
<2>8. CASE s ≠ p /\ t = p proved L538
<3>a–d. Setup: log'[s] = log[s], i ∈ DOMAIN log[s], uniqueness in log[s] tlapm L540–543
<3>2. CASE k ∈ DOMAIN log[p] (k old) proved L544
<4>1. log'[p][k] = log[p][k] smt L546
<4>2. log[p][k] = log[s][i] smt L547
<4>. QED by H_UniformLogEntries smt L548
<3>3. CASE k ∉ DOMAIN log[p] (k new) proved L549
<4>1. k = Len(log[p]) + 1 smt L553–554
<4>2. log'[p][k] = currentTerm[p] smt L555
<4>3a–3. log[s][i] = currentTerm[p] smt L556–559
<4>5. i ∈ DOMAIN log[p] (by H_PrimaryHasOwnEntries) smt L561–562
<4>6. i ∈ 1..Len(log[p]), so i < k smt L563–564
<4>. QED: ~(k < i) smt L565
<3>. QED smt L566
<2>9. CASE s = p /\ t = p proved L567
<3>a–b. log'[p][k] = log'[p][i], uniqueness in log'[p] tlapm L569–570
<3>1. CASE i,k ∈ DOMAIN log[p] (both old) smt L571–582
<3>2. CASE i old, k new → k = Len+1 > i, so ~(k < i) smt L583–589
<3>3. CASE i new, k old → contradiction via uniqueness + equality smt L590–601
<3>4. CASE both new → i = k = Len+1, so ~(k < i) smt L602–608
<3>. QED (exhaustive case split) smt L609
<2>. QED by <2>6, <2>7, <2>8, <2>9 smt L610
<1>2. TypeOK /\ H_LogMatching /\ H_UniformLogEntries /\ GetEntriesAction => H_UniformLogEntries' proved L612
<2>. SUFFICES ASSUME ..., GetEntries(r, sender), ... PROVE ~(k < i) smt L613–620
<2>0. log' = [log EXCEPT ![r] = Append(log[r], newEntry)] smt L622–625
<2>1. Explicit form of log' smt L626–627
<2>a–f. Append properties for log'[r] smt L629–640
<2>g. Len(log[sender]) > Len(log[r]) smt L641–642
<2>h. ~Empty(log[r]) => log[sender][Len(log[r])] = log[r][Len(log[r])] smt L643–644
<2>i. newEntryIndex = Len(log[r]) + 1 (in both Empty and non-Empty cases) smt L648–649
<2>5. CASE s ≠ r /\ t ≠ r smt L650–651
<2>6. CASE s = r /\ t ≠ r proved L652
<3>a–d. Setup: log'[t] = log[t], k ∈ DOMAIN log[t] tlapm L654–657
<3>1. CASE i ∈ DOMAIN log[r] (old entry) proved L658
<4>1. log'[r][i] = log[r][i] smt L660
<4>2. log[t][k] = log[r][i] smt L661
<4>3. uniqueness in pre-state log[r] proved L662
<5>. SUFFICES j ∈ DOMAIN log[r], j < i PROVE log[r][j] ≠ log[r][i] tlapm L663
<5>1–3. j lifted to DOMAIN log'[r], uniqueness in post-state smt L664–666
<5>. QED smt L667
<4>. QED by H_UniformLogEntries smt L668
<3>2. CASE i ∉ DOMAIN log[r] (new entry from sender) proved L669
<4>1. i = Len(log[r]) + 1 smt L671–672
<4>2. log'[r][i] = log[sender][Len(log[r]) + 1] smt L673–674
<4>3. Len(log[r])+1 ∈ DOMAIN log[sender] smt L677–678
<4>4. uniqueness of log[sender][Len(log[r])+1] in sender's log (via H_LogMatching) proved L679
<5>. SUFFICES j2 ∈ DOMAIN log[sender], j2 < Len(log[r])+1 PROVE log[sender][j2] ≠ log[sender][Len(log[r])+1] tlapm L682–684
<5>1. j2 ∈ 1..Len(log[r]) smt L685–686
<5>2. j2 ∈ DOMAIN log[r] smt L687–688
<5>3–5. log'[r][j2] ≠ log'[r][i] via uniqueness in post-state smt L689–696
<5>8. CASE ~Empty(log[r]): log[sender][j2] = log[r][j2] by H_LogMatching proved L701
<6>1. log[sender][Len(log[r])] = log[r][Len(log[r])] smt L703–704
<6>2–4. SubSeq(log[r],1,Len) = SubSeq(log[sender],1,Len) by H_LogMatching smt L705–714
<6>5. log[sender][j2] = log[r][j2] smt L715–716
<6>. QED smt L717
<5>7. CASE Empty(log[r]): contradicts j2 ≥ 1 smt L698–700
<5>. QED smt L718
<4>5. log[t][k] = log[sender][Len(log[r])+1] smt L719–720
<4>. QED: apply H_UniformLogEntries on sender's log smt L722
<3>. QED smt L723
<2>7. CASE s ≠ r /\ t = r proved L724
<3>a–d. Setup: log'[s] = log[s], i ∈ DOMAIN log[s] tlapm L726–729
<3>1. CASE k ∈ DOMAIN log[r] (old): direct by H_UniformLogEntries smt L730–734
<3>2. CASE k ∉ DOMAIN log[r] (k = new entry) proved L735
<4>1. k = Len(log[r]) + 1 smt L737–738
<4>2. log'[r][k] = log[sender][Len(log[r])+1] smt L739–740
<4>3. log[s][i] = log[sender][Len(log[r])+1] smt L741–745
<4>4. Len(log[r])+1 ∈ DOMAIN log[sender] smt L747–748
<4>. QED: apply H_UniformLogEntries (s, i, sender, k) => ~(k < i) smt L749
<3>. QED smt L750
<2>8. CASE s = r /\ t = r proved L751
<3>a–b. log'[r][k] = log'[r][i], uniqueness in log'[r] tlapm L753–754
<3>1. CASE i,k ∈ DOMAIN log[r] (both old) smt L755–765
<3>2. CASE i old, k new → k = Len+1 > i smt L766–769
<3>3. CASE i new, k old → contradiction via uniqueness smt L770–774
<3>4. CASE both new → i = k = Len+1 smt L775–778
<3>. QED (exhaustive case split) smt L779
<2>. QED by <2>5, <2>6, <2>7, <2>8 smt L780
<1>3. TypeOK /\ H_UniformLogEntries /\ RollbackEntriesAction => H_UniformLogEntries' proved L782
<2>. SUFFICES ASSUME ..., RollbackEntries(r, j), ... PROVE ~(k < i) smt L783–790
<2>1. log' = [log EXCEPT ![r] = SubSeq(log[r], 1, Len(log[r])-1)] smt L791–792
<2>b. ∀ srv ≠ r : log'[srv] = log[srv] smt L793–794
<2>c. SubSeq preserves all entries: ∀ idx ∈ DOMAIN log'[r] : log'[r][idx] = log[r][idx] smt L796–797
<2>d. DOMAIN log'[r] downward-closed in DOMAIN log[r] smt L800–801
<2>3. CASE s ≠ r /\ t ≠ r smt L802–803
<2>5. CASE s = r /\ t ≠ r proved L804
<3>a–d. Setup tlapm L806–809
<3>1. i ∈ DOMAIN log[r] /\ log'[r][i] = log[r][i] (SubSeq preserves) smt L811
<3>2. log[t][k] = log[r][i] smt L812
<3>3. uniqueness in pre-state log[r] proved L813
<4>. SUFFICES jj ∈ DOMAIN log[r], jj < i tlapm L814
<4>0. i ∈ DOMAIN log'[r] smt L815
<4>1. jj ∈ DOMAIN log'[r] (downward-closed) smt L816–817
<4>2–3. log'[r][jj] = log[r][jj], uniqueness in post-state smt L818–819
<4>. QED smt L820
<3>. QED by H_UniformLogEntries smt L821
<2>6. CASE s ≠ r /\ t = r proved L822
<3>a–d. log'[s] = log[s], i ∈ DOMAIN log[s], uniqueness in log[s] tlapm L824–827
<3>1. k ∈ DOMAIN log[r] /\ log'[r][k] = log[r][k] smt L829
<3>2. log[r][k] = log[s][i] smt L830
<3>. QED by H_UniformLogEntries smt L831
<2>7. CASE s = r /\ t = r proved L832
<3>a–b. log'[r][k] = log'[r][i], uniqueness in log'[r] tlapm L833–834
<3>1. i ∈ DOMAIN log[r], log'[r][i] = log[r][i] smt L835
<3>2. k ∈ DOMAIN log[r], log'[r][k] = log[r][k] smt L836
<3>3. log[r][k] = log[r][i] smt L837
<3>4. uniqueness in pre-state log[r] proved L838
<4>1. i ∈ DOMAIN log'[r] smt L840
<4>2. jj ∈ DOMAIN log'[r] (downward-closed) smt L841–842
<4>3–4. log'[r][jj] = log[r][jj], uniqueness in post-state smt L843–844
<4>. QED smt L845
<3>. QED by H_UniformLogEntries smt L846
<2>. QED by <2>3, <2>5, <2>6, <2>7 smt L847
<1>4. TypeOK /\ H_UniformLogEntries /\ BecomeLeaderAction => H_UniformLogEntries' smt proved L849
<1>5. TypeOK /\ H_UniformLogEntries /\ CommitEntryAction => H_UniformLogEntries' smt proved L851
<1>6. TypeOK /\ H_UniformLogEntries /\ UpdateTermsAction => H_UniformLogEntries' smt proved L853
<1>7. QED by <1>1..<1>6 DEF Next smt proved L854

Proof Strategy

H_UniformLogEntries states that within any server's log, term values uniquely determine their position: if two entries in two (possibly identical) servers' logs have the same term value, the one with the lower index cannot appear after the other (formally: the index bearing the matching value is never strictly less than the first occurrence's index). The invariant is proved by induction over every Next action.

  1. ClientRequestAction (most complex): The appended entry carries currentTerm[p]. Four sub-cases split on whether each of the two witness indices s, t is the primary p or not. When i is the newly appended index, uniqueness follows either trivially (the new index is the largest) or from H_PrimaryHasOwnEntries, which guarantees that any server already carrying currentTerm[p] in its log must have it at a position that already existed in log[p], keeping the new tail entry truly unique.
  2. GetEntriesAction: The receiver r appends one entry from the sender. When the new entry is at Len(log[r])+1, uniqueness within the sender's log is established first (using H_LogMatching to equate the shared prefix), then H_UniformLogEntries is applied to the sender's log to conclude ~(k < i).
  3. RollbackEntriesAction: The log shrinks (SubSeq). Since every entry in the new shorter log was already in the old log at the same index, and the old log satisfied H_UniformLogEntries, the shortened log trivially inherits the property. The key lemma used is that DOMAIN log'[r] is downward-closed inside DOMAIN log[r], so any j < i with i in the new domain is also in the new domain.
  4. BecomeLeaderAction, CommitEntryAction, UpdateTermsAction: None of these modify log, so H_UniformLogEntries is preserved by definition. Each dispatches directly to SMT with the relevant action definition unfolded.

Proof lines: 464–854  |  Log: output/L6_full_test4.log  |  All obligations: proved (SMT / tlapm trivial)  |  Timing: cached (previously verified)