Proof Status: THEOREM L

▶ <1>. USE A0,A1,A2,A3,A4,A5,A6 7/7 tlapm

#8 L1512:12:1512:14 trivial tlapm fresh

#9 L1512:15:1512:17 trivial tlapm fresh

#10 L1512:18:1512:20 trivial tlapm fresh

#11 L1512:21:1512:23 trivial tlapm fresh

#12 L1512:24:1512:26 trivial tlapm fresh

#13 L1512:27:1512:29 trivial tlapm fresh

#14 L1512:30:1512:32 trivial tlapm fresh

▶ <1>1 (H_CommittedEntryIsOnQuorum,ClientRequestAction) TypeOK /\ H_CommittedEntryIsOnQuorum /\ ClientRequestAction => H_CommittedEntryIsOnQuorum' 1/1 smt

#15 L1514:100:1514:102 proved smt cached

▶ <1>2 (H_CommittedEntryIsOnQuorum,GetEntriesAction) TypeOK /\ H_CommittedEntryIsOnQuorum /\ GetEntriesAction => H_CommittedEntryIsOnQuorum' 1/1 smt

#16 L1516:97:1516:99 proved smt cached

▶ <1>3 (H_CommittedEntryIsOnQuorum,RollbackEntriesAction) TypeOK /\ H_LaterLogsHaveEarlierCommitted /\ H_CommittedEntryIsOnQuorum /\ RollbackEntriesAction => H_CommittedEntryIsOnQuorum' 17/17

▶ <2>. SUFFICES ASSUME TypeOK, H_LaterLogsHaveEarlierCommitted, H_CommittedEntryIsOnQuorum, RollbackEntriesAction, NEW c \in immediatelyCommitted' 1/1 smt

#20 L1525:10:1525:12 proved smt cached

▶ <2>1 PICK i \in Server, j \in Server : RollbackEntries(i, j) BY DEF RollbackEntriesAction 1/1 smt

#21 L1526:67:1526:69 proved smt cached

▶ <2>2 immediatelyCommitted' = immediatelyCommitted BY <2>1 DEF RollbackEntries 2/2 smt

#22 L1527:56:1527:58 proved smt cached

#23 L1527:59:1527:63 trivial tlapm fresh

▶ <2>3 c \in immediatelyCommitted BY <2>2 2/2 smt

#24 L1528:38:1528:40 proved smt cached

#25 L1528:41:1528:45 trivial tlapm fresh

▶ <2>4 log[i] \in Seq(Terms) /\ log[j] \in Seq(Terms) BY DEF TypeOK 1/1 smt

#26 L1529:58:1529:60 proved smt cached

▶ <2>5 log'[i] = SubSeq(log[i], 1, Len(log[i])-1) BY <2>1, <2>4 DEF RollbackEntries, TypeOK 3/3 smt

#27 L1530:54:1530:56 proved smt cached

#28 L1530:57:1530:61 trivial tlapm fresh

#29 L1530:63:1530:67 trivial tlapm fresh

▶ <2>6 Len(log[i]) > 0 BY <2>1 DEF RollbackEntries, CanRollback 2/2 smt

#30 L1531:27:1531:29 proved smt cached

#31 L1531:30:1531:34 trivial tlapm fresh

▶ <2>7 PICK Q \in Quorums(Server) : \A n \in Q : InLog(<<c[1],c[2]>>, n) BY <2>3 DEF H_CommittedEntryIsOnQuorum 2/2 smt

#32 L1534:7:1534:9 proved smt cached

#33 L1534:10:1534:14 trivial tlapm fresh

▶ <2>8 SUFFICES \A n \in Q : InLog(<<c[1],c[2]>>, n)' BY <2>7 2/2 smt

#34 L1537:7:1537:9 proved smt cached

#35 L1537:10:1537:14 trivial tlapm fresh

▶ <2>9 SUFFICES ASSUME NEW n \in Q, InLog(<<c[1],c[2]>>, n) PROVE InLog(<<c[1],c[2]>>, n)' BY <2>7 2/2 smt

#36 L1540:7:1540:9 proved smt cached

#37 L1540:10:1540:14 trivial tlapm fresh

▶ <2>10 CASE n # i BY <2>1, <2>9, <2>10 DEF RollbackEntries, InLog, TypeOK 4/4 smt

#38 L1543:7:1543:9 proved smt cached

#39 L1543:10:1543:14 trivial tlapm fresh

#40 L1543:16:1543:20 trivial tlapm fresh

#41 L1543:22:1543:27 trivial tlapm fresh

▶ <2>11 CASE n = i 42/42

▶ <3>1 c[1] \in DOMAIN log[i] /\ log[i][c[1]] = c[2] BY <2>9, <2>11 DEF InLog 3/3 smt

#48 L1546:59:1546:61 proved smt cached

#49 L1546:62:1546:66 trivial tlapm fresh

#50 L1546:68:1546:73 trivial tlapm fresh

▶ <3>2 c[1] >= 1 /\ c[1] \in Nat BY <2>3 DEF TypeOK, LogIndices 2/2 smt

#51 L1547:39:1547:41 proved smt cached

#52 L1547:42:1547:46 trivial tlapm fresh

▶ <3>3 Len(log[i]) \in Nat BY <2>4 2/2 smt

#53 L1548:33:1548:35 proved smt cached

#54 L1548:36:1548:40 trivial tlapm fresh

▶ <3>4 LastTerm(log[i]) < LastTerm(log[j]) BY <2>1 DEF RollbackEntries, CanRollback 2/2 smt

#55 L1550:49:1550:51 proved smt cached

#56 L1550:52:1550:56 trivial tlapm fresh

▶ <3>5 LastTerm(log[j]) > c[2] \/ c[1] < Len(log[i]) BY <3>1, <3>4, <2>6, <2>4, <3>3, <3>2 DEF LastTerm 7/7 smt

#57 L1555:9:1555:11 proved smt 3.0 (60%)

#58 L1555:12:1555:16 trivial tlapm fresh

#59 L1555:18:1555:22 trivial tlapm fresh

#60 L1555:24:1555:28 trivial tlapm fresh

#61 L1555:30:1555:34 trivial tlapm fresh

#62 L1555:36:1555:40 trivial tlapm fresh

#63 L1555:42:1555:46 trivial tlapm fresh

▶ <3>6 CASE c[1] < Len(log[i]) 81/81

▶ <3>7 CASE c[1] = Len(log[i]) 106/106

▶ <4>1 c[2] = LastTerm(log[i]) BY <3>7, <3>1, <2>6 DEF LastTerm 4/4 smt

#83 L1563:39:1563:41 proved smt cached

#84 L1563:42:1563:46 trivial tlapm fresh

#85 L1563:48:1563:52 trivial tlapm fresh

#86 L1563:54:1563:58 trivial tlapm fresh

▶ <4>2 LastTerm(log[j]) > c[2] BY <3>4, <4>1 3/3 smt

#87 L1565:39:1565:41 proved smt cached

#88 L1565:42:1565:46 trivial tlapm fresh

#89 L1565:48:1565:52 trivial tlapm fresh

▶ <4>3 c[2] \in Nat BY <2>3 DEF TypeOK, LogIndices, Terms 2/2 smt

#90 L1567:28:1567:30 proved smt 0.9 (19%)

#91 L1567:31:1567:35 trivial tlapm fresh

▶ <4>3a Len(log[j]) > 0 BY <4>2, <4>3, <2>4 DEF LastTerm 4/4 smt

#92 L1569:11:1569:13 proved smt 0.7 (15%)

#93 L1569:14:1569:18 trivial tlapm fresh

#94 L1569:20:1569:24 trivial tlapm fresh

#95 L1569:26:1569:30 trivial tlapm fresh

▶ <4>4 Len(log[j]) \in DOMAIN log[j] BY <4>3a, <2>4 3/3 smt

#96 L1570:45:1570:47 proved smt cached

#97 L1570:48:1570:53 trivial tlapm fresh

#98 L1570:55:1570:59 trivial tlapm fresh

▶ <4>5 log[j][Len(log[j])] > c[2] BY <4>2, <4>3a, <2>4 DEF LastTerm 4/4 smt

#99 L1572:11:1572:13 proved smt cached

#100 L1572:14:1572:18 trivial tlapm fresh

#101 L1572:20:1572:25 trivial tlapm fresh

#102 L1572:27:1572:31 trivial tlapm fresh

▶ <4>6 Len(log[j]) >= c[1] /\ log[j][c[1]] = c[2] BY <4>4, <4>5, <2>3 DEF H_LaterLogsHaveEarlierCommitted 4/4 smt

#103 L1574:11:1574:13 proved smt cached

#104 L1574:14:1574:18 trivial tlapm fresh

#105 L1574:20:1574:24 trivial tlapm fresh

#106 L1574:26:1574:30 trivial tlapm fresh

▶ <4>7 Len(log[j]) >= Len(log[i]) BY <4>6, <3>7 3/3 smt

#107 L1580:42:1580:44 proved smt cached

#108 L1580:45:1580:49 trivial tlapm fresh

#109 L1580:51:1580:55 trivial tlapm fresh

▶ <4>8 LogTerm(j, Len(log[i])) = c[2] BY <3>7, <4>6, <2>6, <2>4 DEF LogTerm, GetTerm 5/5 smt

#110 L1582:11:1582:13 proved smt cached

#111 L1582:14:1582:18 trivial tlapm fresh

#112 L1582:20:1582:24 trivial tlapm fresh

#113 L1582:26:1582:30 trivial tlapm fresh

#114 L1582:32:1582:36 trivial tlapm fresh

▶ <4>9 LastTerm(log[i]) = c[2] BY <4>1 2/2 smt

#115 L1583:39:1583:41 proved smt cached

#116 L1583:42:1583:46 trivial tlapm fresh

▶ <4>10 FALSE BY <2>1, <4>7, <4>8, <4>9, <2>6 DEF RollbackEntries, CanRollback 6/6 smt

#117 L1584:22:1584:24 proved smt cached

#118 L1584:25:1584:29 trivial tlapm fresh

#119 L1584:31:1584:35 trivial tlapm fresh

#120 L1584:37:1584:41 trivial tlapm fresh

#121 L1584:43:1584:47 trivial tlapm fresh

#122 L1584:49:1584:53 trivial tlapm fresh

▶ <4>. QED BY <4>10 2/2 smt

#81 L1585:18:1585:20 proved smt cached

#82 L1585:21:1585:26 trivial tlapm fresh

▶ <3>. QED BY <3>6, <3>7, <3>1, <3>3, <2>4 6/6 smt

#42 L1586:16:1586:18 proved smt cached

#43 L1586:19:1586:23 trivial tlapm fresh

#44 L1586:25:1586:29 trivial tlapm fresh

#45 L1586:31:1586:35 trivial tlapm fresh

#46 L1586:37:1586:41 trivial tlapm fresh

#47 L1586:43:1586:47 trivial tlapm fresh

▶ <2>. QED BY <2>10, <2>11 3/3 smt

#17 L1587:14:1587:16 proved smt cached

#18 L1587:17:1587:22 trivial tlapm fresh

#19 L1587:24:1587:29 trivial tlapm fresh

▶ <1>4 (H_CommittedEntryIsOnQuorum,BecomeLeaderAction) TypeOK /\ H_CommittedEntryIsOnQuorum /\ BecomeLeaderAction => H_CommittedEntryIsOnQuorum' 1/1 smt

#123 L1589:99:1589:101 proved smt cached

▶ <1>5 (H_CommittedEntryIsOnQuorum,CommitEntryAction) TypeOK /\ H_CommittedEntryIsOnQuorum /\ CommitEntryAction => H_CommittedEntryIsOnQuorum' 1/1 smt

#124 L1591:98:1591:100 proved smt cached

▶ <1>6 (H_CommittedEntryIsOnQuorum,UpdateTermsAction) TypeOK /\ H_CommittedEntryIsOnQuorum /\ UpdateTermsAction => H_CommittedEntryIsOnQuorum' 1/1 smt

#125 L1593:98:1593:100 proved smt cached

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

#1 L1594:11:1594:13 proved smt cached

#2 L1594:14:1594:18 trivial tlapm fresh

#3 L1594:19:1594:23 trivial tlapm fresh

#4 L1594:24:1594:28 trivial tlapm fresh

#5 L1594:29:1594:33 trivial tlapm fresh

#6 L1594:34:1594:38 trivial tlapm fresh

#7 L1594:39:1594:43 trivial tlapm fresh

THEOREM L_11 (H_CommittedEntryIsOnQuorum)

Proof Notes

Proof Tree