Proof Status: THEOREM L

▶ <1>7 <1>7. QED BY <1>1,<1>2,<1>3,<1>4,<1>5,<1>6 DEF Next 10/10 tlapm

#8 L298:12:298:14 trivial tlapm

#9 L298:15:298:17 trivial tlapm

#10 L298:18:298:20 trivial tlapm

#11 L298:21:298:23 trivial tlapm

#12 L298:24:298:26 trivial tlapm

#13 L298:27:298:29 trivial tlapm

#14 L298:30:298:32 trivial tlapm

#15 L298:33:298:35 trivial tlapm

#16 L300:94:300:96 proved smt

#17 L302:91:302:93 proved smt

▶ <1>1 <1>1. TypeOK /\ H_PrimaryTermGTELogTerm /\ ClientRequestAction => H_PrimaryTermGTELogTerm' BY DEF TypeOK,ClientRequestAction,ClientRequest,H_PrimaryTermGTELogTerm,Terms 1/1 smt

#18 L304:96:304:98 proved smt

▶ <1>2 <1>2. TypeOK /\ H_PrimaryTermGTELogTerm /\ GetEntriesAction => H_PrimaryTermGTELogTerm' BY DEF TypeOK,GetEntriesAction,GetEntries,H_PrimaryTermGTELogTerm,Empty

▶ <1>3 <1>3. TypeOK /\ H_PrimaryTermGTELogTerm /\ RollbackEntriesAction => H_PrimaryTermGTELogTerm' BY DEF TypeOK,RollbackEntriesAction,RollbackEntries,H_PrimaryTermGTELogTerm,CanRollback,LastTerm,Empty 1/1 smt

#22 L309:7:309:14 proved smt

▶ <1>4 <1>4. TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ H_PrimaryTermGTELogTerm /\ BecomeLeaderAction => H_PrimaryTermGTELogTerm' 185/185 smt

#23 L311:7:311:9 proved smt

#24 L313:7:313:9 proved smt

#25 L313:10:313:14 trivial tlapm

▶ <2>1 <2>1. PICK leader \in Server, Q \in Quorums(Server) : BecomeLeader(leader, Q) 8/8 smt

#26 L315:7:315:9 proved smt

#27 L315:10:315:14 trivial tlapm

#28 L317:7:317:9 proved smt

#29 L317:10:317:14 trivial tlapm

#30 L319:7:319:9 proved smt

#31 L319:10:319:14 trivial tlapm

#39 L323:106:323:113 proved smt

#40 L324:56:324:58 proved smt

▶ <2>2 <2>2. UNCHANGED <<log, immediatelyCommitted>> 5/5 tlapm

#68 L338:60:338:62 proved smt

#69 L338:63:338:67 trivial tlapm

#70 L338:69:338:73 trivial tlapm

#71 L339:40:339:42 proved smt

#72 L339:43:339:47 trivial tlapm

▶ <2>1 BY <2>1 DEF BecomeLeader 8/8 smt

#26 L315:7:315:9 proved smt

#27 L315:10:315:14 trivial tlapm

#28 L317:7:317:9 proved smt

#29 L317:10:317:14 trivial tlapm

#30 L319:7:319:9 proved smt

#31 L319:10:319:14 trivial tlapm

#39 L323:106:323:113 proved smt

#40 L324:56:324:58 proved smt

▶ <2>3 <2>3. \A v \in Q : currentTerm[v] < currentTerm[leader] + 1

▶ <2>1 BY <2>1 DEF BecomeLeader, CanVoteForOplog 8/8 smt

#26 L315:7:315:9 proved smt

#27 L315:10:315:14 trivial tlapm

#28 L317:7:317:9 proved smt

#29 L317:10:317:14 trivial tlapm

#30 L319:7:319:9 proved smt

#31 L319:10:319:14 trivial tlapm

#39 L323:106:323:113 proved smt

#40 L324:56:324:58 proved smt

▶ <2>4 <2>4. state' = [s_1 \in Server |-> IF s_1 = leader THEN Primary ELSE IF s_1 \in Q THEN Secondary ELSE state[s_1]]

▶ <2>1 BY <2>1 DEF BecomeLeader 8/8 smt

#26 L315:7:315:9 proved smt

#27 L315:10:315:14 trivial tlapm

#28 L317:7:317:9 proved smt

#29 L317:10:317:14 trivial tlapm

#30 L319:7:319:9 proved smt

#31 L319:10:319:14 trivial tlapm

#39 L323:106:323:113 proved smt

#40 L324:56:324:58 proved smt

▶ <2>5 <2>5. currentTerm' = [s_1 \in Server |-> IF s_1 \in Q THEN currentTerm[leader] + 1 ELSE currentTerm[s_1]] 2/2 smt

#37 L322:33:322:35 proved smt

#38 L322:36:322:38 trivial tlapm

▶ <2>1 BY <2>1 DEF BecomeLeader 8/8 smt

#26 L315:7:315:9 proved smt

#27 L315:10:315:14 trivial tlapm

#28 L317:7:317:9 proved smt

#29 L317:10:317:14 trivial tlapm

#30 L319:7:319:9 proved smt

#31 L319:10:319:14 trivial tlapm

#39 L323:106:323:113 proved smt

#40 L324:56:324:58 proved smt

▶ <2>6 <2>6. \A Q1, Q2 \in Quorums(Server) : Q1 \cap Q2 # {} 50/50 tlapm

#41 L325:48:325:50 proved smt

#42 L325:51:325:55 trivial tlapm

#43 L325:57:325:61 trivial tlapm

#44 L325:63:325:72 trivial tlapm

▶ <3>1 <3>1. IsFiniteSet(Server) BY A0 5/5 tlapm

#45 L326:100:326:102 proved smt

#56 L334:7:334:9 proved smt

#57 L334:10:334:14 trivial tlapm

#58 L334:16:334:20 trivial tlapm

#59 L334:22:334:26 trivial tlapm

▶ <3>2 <3>2. SUFFICES ASSUME NEW Q1 \in Quorums(Server), NEW Q2 \in Quorums(Server) PROVE Q1 \cap Q2 # {} OBVIOUS 8/8 tlapm

#46 L327:41:327:43 proved smt

#47 L327:44:327:48 trivial tlapm

#48 L327:50:327:68 trivial tlapm

#73 L342:9:342:11 proved smt

#74 L342:12:342:16 trivial tlapm

#75 L342:18:342:22 trivial tlapm

#79 L346:41:346:43 proved smt

#80 L346:44:346:48 trivial tlapm

▶ <3>3 <3>3. Q1 \subseteq Server /\ Q2 \subseteq Server BY DEF Quorums 6/6 smt

#49 L328:64:328:66 proved smt

#50 L328:67:328:71 trivial tlapm

#51 L328:73:328:91 trivial tlapm

#76 L344:9:344:11 proved smt

#77 L345:28:345:30 proved smt

#78 L345:31:345:35 trivial tlapm

▶ <3>4 <3>4. IsFiniteSet(Q1) /\ IsFiniteSet(Q2) BY <3>1, <3>3, FS_Subset 10/10 tlapm

#52 L329:69:329:71 proved smt

#53 L329:72:329:76 trivial tlapm

#54 L329:78:329:82 trivial tlapm

#55 L329:84:329:88 trivial tlapm

#81 L347:54:347:56 proved smt

#82 L347:57:347:61 trivial tlapm

#83 L347:63:347:67 trivial tlapm

#84 L348:48:348:50 proved smt

#85 L348:51:348:55 trivial tlapm

#86 L348:57:348:61 trivial tlapm

▶ <3>5 <3>5. Cardinality(Q1) * 2 > Cardinality(Server) /\ Cardinality(Q2) * 2 > Cardinality(Server) BY DEF Quorums 8/8 tlapm

#32 L330:16:330:18 proved smt

#33 L330:19:330:23 trivial tlapm

#34 L330:25:330:29 trivial tlapm

#35 L330:31:330:35 trivial tlapm

#36 L330:37:330:59 trivial tlapm

#87 L349:26:349:28 proved smt

#88 L349:29:349:33 trivial tlapm

#89 L349:35:349:37 trivial tlapm

▶ <3>6 <3>6. Cardinality(Server) \in Nat BY <3>1, FS_CardinalityType 2/2 smt

#90 L350:37:350:39 proved smt

#91 L350:40:350:44 trivial tlapm

▶ <3>7 <3>7. Cardinality(Q1) \in Nat /\ Cardinality(Q2) \in Nat BY <3>4, FS_CardinalityType 1/1 smt

#92 L351:39:351:41 proved smt

▶ <3>8 <3>8. Cardinality(Q1) + Cardinality(Q2) > Cardinality(Server) BY <3>5, <3>6, <3>7 1/1 smt

#93 L352:42:352:44 proved smt 0.1s (0%)

▶ <3>1 <3>. QED BY <3>1, <3>3, <3>8, FS_MajoritiesIntersect 5/5 tlapm

#45 L326:100:326:102 proved smt

#56 L334:7:334:9 proved smt

#57 L334:10:334:14 trivial tlapm

#58 L334:16:334:20 trivial tlapm

#59 L334:22:334:26 trivial tlapm

▶ <2>7 <2>7. \A s \in Server : s # leader /\ state'[s] = Primary => 10/10 tlapm

#1 L359:11:359:13 proved smt

#2 L359:14:359:18 trivial tlapm

#3 L359:19:359:23 trivial tlapm

#4 L359:24:359:28 trivial tlapm

#5 L359:29:359:33 trivial tlapm

#6 L359:34:359:38 trivial tlapm

#7 L359:39:359:43 trivial tlapm

#66 L337:26:337:28 proved smt

#67 L337:29:337:33 trivial tlapm

#95 L358:92:358:94 proved smt

▶ <2>2 BY <2>2, <2>4, <2>5 DEF H_PrimaryTermGTELogTerm 5/5 tlapm

#68 L338:60:338:62 proved smt

#69 L338:63:338:67 trivial tlapm

#70 L338:69:338:73 trivial tlapm

#71 L339:40:339:42 proved smt

#72 L339:43:339:47 trivial tlapm

▶ <2>8 <2>8. \A idx \in DOMAIN log'[leader] : currentTerm'[leader] >= log'[leader][idx] 60/60

▶ <3>1 <3>1. leader \in Q BY <2>1 DEF BecomeLeader 5/5 tlapm

#45 L326:100:326:102 proved smt

#56 L334:7:334:9 proved smt

#57 L334:10:334:14 trivial tlapm

#58 L334:16:334:20 trivial tlapm

#59 L334:22:334:26 trivial tlapm

▶ <3>2 <3>2. currentTerm'[leader] = currentTerm[leader] + 1 BY <3>1, <2>5 8/8 tlapm

#46 L327:41:327:43 proved smt

#47 L327:44:327:48 trivial tlapm

#48 L327:50:327:68 trivial tlapm

#73 L342:9:342:11 proved smt

#74 L342:12:342:16 trivial tlapm

#75 L342:18:342:22 trivial tlapm

#79 L346:41:346:43 proved smt

#80 L346:44:346:48 trivial tlapm

▶ <3>3 <3>3. log'[leader] = log[leader] BY <2>2 6/6 smt

#49 L328:64:328:66 proved smt

#50 L328:67:328:71 trivial tlapm

#51 L328:73:328:91 trivial tlapm

#76 L344:9:344:11 proved smt

#77 L345:28:345:30 proved smt

#78 L345:31:345:35 trivial tlapm

▶ <3>2 BY <3>2, <3>3 8/8 tlapm

#46 L327:41:327:43 proved smt

#47 L327:44:327:48 trivial tlapm

#48 L327:50:327:68 trivial tlapm

#73 L342:9:342:11 proved smt

#74 L342:12:342:16 trivial tlapm

#75 L342:18:342:22 trivial tlapm

#79 L346:41:346:43 proved smt

#80 L346:44:346:48 trivial tlapm

▶ <3>4 <3>4. PICK Qe \in Quorums(Server) : \A n \in Qe : currentTerm[n] >= log[leader][idx] 10/10 tlapm

#52 L329:69:329:71 proved smt

#53 L329:72:329:76 trivial tlapm

#54 L329:78:329:82 trivial tlapm

#55 L329:84:329:88 trivial tlapm

#81 L347:54:347:56 proved smt

#82 L347:57:347:61 trivial tlapm

#83 L347:63:347:67 trivial tlapm

#84 L348:48:348:50 proved smt

#85 L348:51:348:55 trivial tlapm

#86 L348:57:348:61 trivial tlapm

▶ <3>5 <3>5. Q \cap Qe # {} BY <2>6 8/8 tlapm

#32 L330:16:330:18 proved smt

#33 L330:19:330:23 trivial tlapm

#34 L330:25:330:29 trivial tlapm

#35 L330:31:330:35 trivial tlapm

#36 L330:37:330:59 trivial tlapm

#87 L349:26:349:28 proved smt

#88 L349:29:349:33 trivial tlapm

#89 L349:35:349:37 trivial tlapm

▶ <3>6 <3>6. PICK w \in Q \cap Qe : TRUE BY <3>5 2/2 smt

#90 L350:37:350:39 proved smt

#91 L350:40:350:44 trivial tlapm

▶ <3>7 <3>7. currentTerm[w] < currentTerm[leader] + 1 BY <3>6, <2>3 1/1 smt

#92 L351:39:351:41 proved smt

▶ <3>8 <3>8. currentTerm[w] >= log[leader][idx] BY <3>6, <3>4 1/1 smt

#93 L352:42:352:44 proved smt 0.1s (0%)

▶ <3>9 <3>9. w \in Server BY <3>6, A4 DEF Quorums 6/6 tlapm

#60 L353:16:353:18 proved smt 1.6s (11%)

#61 L353:19:353:23 trivial tlapm

#62 L353:25:353:29 trivial tlapm

#63 L353:31:353:36 trivial tlapm

#64 L353:38:353:43 trivial tlapm

#65 L353:45:353:50 trivial tlapm

▶ <3>10 <3>10. currentTerm[w] \in Int BY <3>9 DEF TypeOK, Terms 3/3 tlapm

#19 L354:14:354:16 proved smt

#20 L354:17:354:21 trivial tlapm

#21 L354:23:354:27 trivial tlapm

▶ <3>11 <3>11. log[leader][idx] \in Int BY DEF TypeOK, Terms

▶ <3>12 <3>12. currentTerm[leader] \in Int BY DEF TypeOK, Terms 1/1 smt

#94 L356:92:356:94 proved smt

▶ <3>7 <3>. QED BY <3>7, <3>8, <3>10, <3>11, <3>12 1/1 smt

#92 L351:39:351:41 proved smt

▶ <2>7 <2>. QED BY <2>7, <2>8 DEF H_PrimaryTermGTELogTerm 10/10 tlapm

#1 L359:11:359:13 proved smt

#2 L359:14:359:18 trivial tlapm

#3 L359:19:359:23 trivial tlapm

#4 L359:24:359:28 trivial tlapm

#5 L359:29:359:33 trivial tlapm

#6 L359:34:359:38 trivial tlapm

#7 L359:39:359:43 trivial tlapm

#66 L337:26:337:28 proved smt

#67 L337:29:337:33 trivial tlapm

#95 L358:92:358:94 proved smt

THEOREM L_4 (H_PrimaryTermGTELogTerm)

Proof Tree