THEOREM L_8 — H_LogEntryImpliesSafeAtTerm

Status: ALL 20 OBLIGATIONS PROVED  |  7 proof steps (6 action cases + QED)  |  Provers: SMT + TLAPM (trivial)

TypeOK /\ H_QuorumsSafeAtTerms /\ H_LogEntryImpliesSafeAtTerm /\ Next => H_LogEntryImpliesSafeAtTerm'

THEOREM L_8 proved L998
<1>. USE A0,A1,A2,A3,A4,A5,A6 tlapm trivial ×7 L999
<1>1. TypeOK /\ H_QuorumsSafeAtTerms /\ H_LogEntryImpliesSafeAtTerm /\ ClientRequestAction => H_LogEntryImpliesSafeAtTerm' smt proved cached L1001
BY DEF TypeOK, H_QuorumsSafeAtTerms, ClientRequestAction, ClientRequest, H_LogEntryImpliesSafeAtTerm
<1>2. TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ GetEntriesAction => H_LogEntryImpliesSafeAtTerm' smt proved cached L1003
BY DEF TypeOK, GetEntriesAction, GetEntries, H_LogEntryImpliesSafeAtTerm
<1>3. TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ RollbackEntriesAction => H_LogEntryImpliesSafeAtTerm' smt proved cached L1005
BY DEF TypeOK, RollbackEntriesAction, RollbackEntries, H_LogEntryImpliesSafeAtTerm
<1>4. TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ BecomeLeaderAction => H_LogEntryImpliesSafeAtTerm' smt proved cached (0.2s) L1007
BY DEF TypeOK, BecomeLeaderAction, BecomeLeader, H_LogEntryImpliesSafeAtTerm, CanVoteForOplog, Terms
<1>5. TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ CommitEntryAction => H_LogEntryImpliesSafeAtTerm' smt proved cached L1009
BY DEF TypeOK, CommitEntryAction, CommitEntry, H_LogEntryImpliesSafeAtTerm
<1>6. TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ UpdateTermsAction => H_LogEntryImpliesSafeAtTerm' smt proved cached (0.1s) L1011
BY DEF TypeOK, UpdateTermsAction, UpdateTerms, UpdateTermsExpr, H_LogEntryImpliesSafeAtTerm, Terms
<1>7. QED smt proved L1012
BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6 DEF Next

Obligation Breakdown

Step Action Prover Status Timing Notes
<1>. USE A0–A6 axiom assumptions tlapm trivial (×7) cached IDs 8–14
<1>1 ClientRequestAction smt proved cached ID 15; needs H_QuorumsSafeAtTerms
<1>2 GetEntriesAction smt proved cached ID 16; log copy preserves invariant
<1>3 RollbackEntriesAction smt proved cached ID 17; log truncation preserves invariant
<1>4 BecomeLeaderAction smt proved 0.2s (3%) ID 18; needs CanVoteForOplog, Terms defs
<1>5 CommitEntryAction smt proved cached ID 19; commit does not change log
<1>6 UpdateTermsAction smt proved 0.1s (1%) ID 20; needs UpdateTermsExpr, Terms defs
<1>7. QED Exhaustive action case split smt proved cached IDs 1–7

Proof Strategy

H_LogEntryImpliesSafeAtTerm asserts that every log entry at index i with term t implies that a quorum of servers was safe at term t at the time of appending. The inductive step proves this is preserved by all six Next-state actions.

The proof is a straightforward flat case split over each action in Next:

  1. ClientRequest: A new entry is appended by a primary. Requires H_QuorumsSafeAtTerms to establish that the leader's current quorum was safe at the entry's term — this is the only action that needs an extra inductive hypothesis beyond TypeOK.
  2. GetEntries: Log entries are copied from another server. The invariant is preserved because the copied entries already satisfy it (from H_LogEntryImpliesSafeAtTerm on the source).
  3. RollbackEntries: Log entries are removed. Since the set of log entries only shrinks, the invariant trivially holds for the remaining entries.
  4. BecomeLeader: No log entries are added or removed; only state and currentTerm change. The CanVoteForOplog and Terms definitions are unfolded to confirm the log is unchanged.
  5. CommitEntry: Only the immediatelyCommitted set changes; the log itself is unchanged.
  6. UpdateTerms: Only currentTerm and state change; the log and safety witnesses are unchanged. Requires unfolding UpdateTermsExpr and Terms.

All six cases are discharged automatically by SMT after unfolding the relevant definitions. The only non-trivial step is BecomeLeaderAction (0.2s) and UpdateTermsAction (0.1s); all others were satisfied from the fingerprint cache.

Total TLAPM-reported obligations: 20 (7 QED sub-obligations from the case-split, 7 trivial axiom-use obligations, and 6 BY obligations for each action case). All proved.