Proof Status: THEOREM L_5 (H_QuorumsSafeAtTerms)

THEOREM L_5 proved L367

<1>. USE A0..A7 L368

<1>1. ClientRequestAction smt proved L370

<1>2. GetEntriesAction smt proved L372

<1>3. RollbackEntriesAction smt proved L374

<1>4. BecomeLeaderAction proved L376

<2>. SUFFICES ASSUME TypeOK, H_QuorumsSafeAtTerms, BecomeLeaderAction PROVE H_QuorumsSafeAtTerms' smt L377–L379

<2>1. PICK leader ∈ Server, Q ∈ Quorums(Server) : BecomeLeader(leader, Q) smt L380

<2>2. currentTerm' = [s_1 ∈ Server → IF s_1 ∈ Q THEN currentTerm[leader]+1 ELSE currentTerm[s_1]] smt L382

<2>3. state' = [s_1 ∈ Server → IF s_1 = leader THEN Primary ELSE IF s_1 ∈ Q THEN Secondary ELSE state[s_1]] smt L384

<2>4. leader ∈ Q smt L386

<2>5. ∀ v ∈ Q : currentTerm[v] < currentTerm[leader]+1 smt L388

<2>6. ∀ n ∈ Q : currentTerm'[n] = currentTerm[leader]+1 smt L390

<2>7. Q ⊆ Server smt L392

<2>8. ∀ Q1, Q2 ∈ Quorums(Server) : Q1 ∩ Q2 ≠ {} (quorum intersection) proved L395

<3>1. IsFiniteSet(Server) smt L396

<3>2. SUFFICES ASSUME NEW Q1, Q2 ∈ Quorums(Server) PROVE Q1 ∩ Q2 ≠ {} smt L397

<3>3. Q1 ⊆ Server ∧ Q2 ⊆ Server smt L398

<3>4. IsFiniteSet(Q1) ∧ IsFiniteSet(Q2) smt L399

<3>5. Cardinality(Q1)*2 > |Server| ∧ Cardinality(Q2)*2 > |Server| smt L400

<3>6. Cardinality(Server) ∈ Nat smt L401

<3>7. Cardinality(Q1) ∈ Nat ∧ Cardinality(Q2) ∈ Nat smt L402

<3>8. Cardinality(Q1) + Cardinality(Q2) > |Server| smt L403

<3>. QED by FS_MajoritiesIntersect smt L404

<2>9. ∀ s ∈ Server : state[s] = Primary ⇒ currentTerm[leader]+1 ≥ currentTerm[s] proved L406

<3>. SUFFICES ASSUME NEW s ∈ Server, state[s] = Primary PROVE currentTerm[leader]+1 ≥ currentTerm[s] smt L407

<3>1. PICK Qs ∈ Quorums(Server) : ∀ n ∈ Qs : currentTerm[n] ≥ currentTerm[s] smt L408

<3>2. Q ∩ Qs ≠ {} smt L410

<3>3. PICK w ∈ Q ∩ Qs smt L411

<3>4. currentTerm[w] ≥ currentTerm[s] smt L412

<3>5. currentTerm[w] < currentTerm[leader]+1 smt L413

<3>6. w ∈ Server smt L414

<3>. QED smt L415

<2>10. ∀ s ∈ Server : state'[s] = Primary ⇒ ∀ n ∈ Q : currentTerm'[n] ≥ currentTerm'[s] proved L417

<3>. SUFFICES ASSUME NEW s ∈ Server, state'[s] = Primary PROVE ∀ n ∈ Q : currentTerm'[n] ≥ currentTerm'[s] smt L419

<3>1. CASE s = leader → Q witnesses for leader smt L420

<3>2. CASE s ≠ leader proved L422

<4>1. s ∉ Q ∧ state[s] = Primary smt L423

<4>2. currentTerm'[s] = currentTerm[s] smt L424

<4>3. currentTerm[leader]+1 ≥ currentTerm[s] smt L425

<4>. QED smt L426

<3>. QED smt L427

<2>. QED by <2>10 DEF H_QuorumsSafeAtTerms smt L428

<1>5. CommitEntryAction smt proved L430

<1>6. UpdateTermsAction proved L432

<2>. SUFFICES ASSUME TypeOK, H_QuorumsSafeAtTerms, UpdateTerms(i,j), state'[s] = Primary PROVE ∃ Qw : ∀ n ∈ Qw : currentTerm'[n] ≥ currentTerm'[s] smt L433

<2>1. currentTerm' = [currentTerm EXCEPT ![j] = currentTerm[i]] smt L438

<2>2. state' = [state EXCEPT ![j] = Secondary] smt L440

<2>3. s ≠ j ∧ state[s] = Primary smt L442

<2>4. currentTerm'[s] = currentTerm[s] smt L444

<2>5. PICK Qs ∈ Quorums(Server) : ∀ n ∈ Qs : currentTerm[n] ≥ currentTerm[s] smt L446

<2>6. Qs ⊆ Server smt L448

<2>7. currentTerm[i] ≥ currentTerm[j] smt L450

<2>8. ASSUME NEW n ∈ Qs PROVE currentTerm'[n] ≥ currentTerm'[s] proved L452

<3>1. n ∈ Server smt L453

<3>2. CASE n = j → currentTerm'[n] = currentTerm[i] ≥ currentTerm[j] ≥ ... smt L454

<3>3. CASE n ≠ j → currentTerm'[n] = currentTerm[n] ≥ currentTerm[s] smt L456

<3>. QED smt L458

<2>. QED by <2>8 smt L459

<1>7. QED BY <1>1..<1>6 DEF Next smt L460

Proof Strategy

The invariant H_QuorumsSafeAtTerms states that every Primary server s has a witnessing quorum Qs such that every member of Qs has a term at least as large as currentTerm[s]. The proof proceeds action by action:

All 132 proof obligations were discharged by SMT (Z3 via TLAPM), with the quorum intersection sub-proof requiring explicit Cardinality arithmetic to guide the solver.

THEOREM L_5 — H_QuorumsSafeAtTerms

Proof Strategy