Proof Status: THEOREM L

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

#8 L1301:12:1301:14 trivial tlapm

#9 L1301:15:1301:17 trivial tlapm

#10 L1301:18:1301:20 trivial tlapm

#11 L1301:21:1301:23 trivial tlapm

#12 L1301:24:1301:26 trivial tlapm

#13 L1301:27:1301:29 trivial tlapm

#14 L1301:30:1301:32 trivial tlapm

▶ <1>1 (H_LaterLogsHaveEarlierCommitted,ClientRequestAction) TypeOK /\ H_LeaderCompleteness /\ H_LaterLogsHaveEarlierCommitted /\ ClientRequestAction => H_LaterLogsHaveEarlierCommit... 102/102

▶ <2>. SUFFICES ASSUME TypeOK, H_LeaderCompleteness, H_LaterLogsHaveEarlierCommitted, ClientRequestAction, 1/1 smt

#18 L1309:10:1309:12 proved smt cached

▶ <2>1 PICK i \in Server : ClientRequest(i) BY DEF ClientRequestAction 1/1 smt

#19 L1310:48:1310:50 proved smt cached

▶ <2>2 immediatelyCommitted' = immediatelyCommitted /\ c \in immediatelyCommitted BY <2>1 DEF ClientRequest 2/2 smt

#20 L1311:86:1311:88 proved smt cached

#21 L1311:89:1311:93 trivial tlapm

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

#22 L1312:37:1312:39 proved smt cached

#23 L1312:40:1312:44 trivial tlapm

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

#24 L1313:33:1313:35 proved smt cached

▶ <2>5 CASE s # i 4/4 smt

#25 L1315:7:1315:9 proved smt cached

#26 L1315:10:1315:14 trivial tlapm

#27 L1315:16:1315:20 trivial tlapm

#28 L1315:22:1315:26 trivial tlapm

▶ <2>6 CASE s = i 88/88

▶ <3>1 log'[i] = Append(log[i], currentTerm[i]) BY <2>1, <2>4 DEF ClientRequest, TypeOK 3/3 smt

#33 L1317:54:1317:56 proved smt cached

#34 L1317:57:1317:61 trivial tlapm

#35 L1317:63:1317:67 trivial tlapm

▶ <3>2 state[i] = Primary BY <2>1 DEF ClientRequest 2/2 smt

#36 L1318:32:1318:34 proved smt cached

#37 L1318:35:1318:39 trivial tlapm

▶ <3>3 CASE idx \in DOMAIN log[i] 37/37

▶ <4>1 log[i][idx] > c[2] BY <2>6, <3>1, <3>3, <2>4 5/5 smt

#41 L1320:34:1320:36 proved smt cached

#42 L1320:37:1320:41 trivial tlapm

#43 L1320:43:1320:47 trivial tlapm

#44 L1320:49:1320:53 trivial tlapm

#45 L1320:55:1320:59 trivial tlapm

▶ <4>2 Len(log[i]) >= c[1] /\ log[i][c[1]] = c[2] 4/4 smt

#46 L1322:11:1322:13 proved smt cached

#47 L1322:14:1322:18 trivial tlapm

#48 L1322:20:1322:24 trivial tlapm

#49 L1322:26:1322:30 trivial tlapm

▶ <4>3 c[1] \in DOMAIN log[i] BY <2>3, <4>2, <2>4 4/4 smt

#50 L1323:38:1323:40 proved smt cached

#51 L1323:41:1323:45 trivial tlapm

#52 L1323:47:1323:51 trivial tlapm

#53 L1323:53:1323:57 trivial tlapm

▶ <4>4 Len(log'[i]) = Len(log[i]) + 1 BY <3>1, <2>4 3/3 smt

#54 L1324:46:1324:48 proved smt cached

#55 L1324:49:1324:53 trivial tlapm

#56 L1324:55:1324:59 trivial tlapm

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

#57 L1325:35:1325:37 proved smt cached

#58 L1325:38:1325:42 trivial tlapm

▶ <4>6 Len(log'[i]) >= c[1] BY <4>4, <4>2, <4>5, <2>3 5/5 smt

#59 L1326:36:1326:38 proved smt cached

#60 L1326:39:1326:43 trivial tlapm

#61 L1326:45:1326:49 trivial tlapm

#62 L1326:51:1326:55 trivial tlapm

#63 L1326:57:1326:61 trivial tlapm

▶ <4>7 log'[i][c[1]] = log[i][c[1]] BY <3>1, <4>3, <2>4 4/4 smt

#64 L1327:44:1327:46 proved smt cached

#65 L1327:47:1327:51 trivial tlapm

#66 L1327:53:1327:57 trivial tlapm

#67 L1327:59:1327:63 trivial tlapm

▶ <4>8 Len(log'[s]) >= c[1] BY <2>6, <4>6 3/3 smt

#68 L1328:36:1328:38 proved smt cached

#69 L1328:39:1328:43 trivial tlapm

#70 L1328:45:1328:49 trivial tlapm

▶ <4>9 log'[s][c[1]] = c[2] BY <2>6, <4>7, <4>2 4/4 smt

#71 L1329:36:1329:38 proved smt cached

#72 L1329:39:1329:43 trivial tlapm

#73 L1329:45:1329:49 trivial tlapm

#74 L1329:51:1329:55 trivial tlapm

▶ <4>. QED BY <4>8, <4>9 3/3 smt

#38 L1330:18:1330:20 proved smt cached

#39 L1330:21:1330:25 trivial tlapm

#40 L1330:27:1330:31 trivial tlapm

▶ <3>4 CASE idx = Len(log[i]) + 1 38/38

▶ <4>1 currentTerm[i] > c[2] BY <2>6, <3>1, <3>4, <2>4 5/5 smt

#78 L1332:37:1332:39 proved smt cached

#79 L1332:40:1332:44 trivial tlapm

#80 L1332:46:1332:50 trivial tlapm

#81 L1332:52:1332:56 trivial tlapm

#82 L1332:58:1332:62 trivial tlapm

▶ <4>2 InLog(<<c[1], c[2]>>, i) BY <3>2, <4>1, <2>2 DEF H_LeaderCompleteness 4/4 smt

#83 L1333:40:1333:42 proved smt cached

#84 L1333:43:1333:47 trivial tlapm

#85 L1333:49:1333:53 trivial tlapm

#86 L1333:55:1333:59 trivial tlapm

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

#87 L1334:61:1334:63 proved smt cached

#88 L1334:64:1334:68 trivial tlapm

▶ <4>4 Len(log[i]) >= c[1] BY <4>3, <2>4 3/3 smt

#89 L1335:35:1335:37 proved smt cached

#90 L1335:38:1335:42 trivial tlapm

#91 L1335:44:1335:48 trivial tlapm

▶ <4>5 Len(log'[i]) = Len(log[i]) + 1 BY <3>1, <2>4 3/3 smt

#92 L1336:46:1336:48 proved smt cached

#93 L1336:49:1336:53 trivial tlapm

#94 L1336:55:1336:59 trivial tlapm

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

#95 L1337:36:1337:38 proved smt cached

#96 L1337:39:1337:43 trivial tlapm

▶ <4>6 Len(log'[i]) >= c[1] BY <4>5, <4>4, <4>5a, <2>3 5/5 smt

#97 L1338:36:1338:38 proved smt cached

#98 L1338:39:1338:43 trivial tlapm

#99 L1338:45:1338:49 trivial tlapm

#100 L1338:51:1338:56 trivial tlapm

#101 L1338:58:1338:62 trivial tlapm

▶ <4>7 log'[i][c[1]] = log[i][c[1]] BY <3>1, <4>3, <2>4 4/4 smt

#102 L1339:44:1339:46 proved smt cached

#103 L1339:47:1339:51 trivial tlapm

#104 L1339:53:1339:57 trivial tlapm

#105 L1339:59:1339:63 trivial tlapm

▶ <4>8 Len(log'[s]) >= c[1] BY <2>6, <4>6 3/3 smt

#106 L1340:36:1340:38 proved smt cached

#107 L1340:39:1340:43 trivial tlapm

#108 L1340:45:1340:49 trivial tlapm

▶ <4>9 log'[s][c[1]] = c[2] BY <2>6, <4>7, <4>3 4/4 smt

#109 L1341:36:1341:38 proved smt cached

#110 L1341:39:1341:43 trivial tlapm

#111 L1341:45:1341:49 trivial tlapm

#112 L1341:51:1341:55 trivial tlapm

▶ <4>. QED BY <4>8, <4>9 3/3 smt

#75 L1342:18:1342:20 proved smt cached

#76 L1342:21:1342:25 trivial tlapm

#77 L1342:27:1342:31 trivial tlapm

▶ <3>5 idx \in DOMAIN log[i] \/ idx = Len(log[i]) + 1 4/4 smt

#113 L1344:9:1344:11 proved smt cached

#114 L1344:12:1344:16 trivial tlapm

#115 L1344:18:1344:22 trivial tlapm

#116 L1344:24:1344:28 trivial tlapm

▶ <3>. QED BY <3>3, <3>4, <3>5 4/4 smt

#29 L1345:16:1345:18 proved smt cached

#30 L1345:19:1345:23 trivial tlapm

#31 L1345:25:1345:29 trivial tlapm

#32 L1345:31:1345:35 trivial tlapm

▶ <2>. QED BY <2>5, <2>6 3/3 smt

#15 L1346:14:1346:16 proved smt cached

#16 L1346:17:1346:21 trivial tlapm

#17 L1346:23:1346:27 trivial tlapm

▶ <1>2 (H_LaterLogsHaveEarlierCommitted,GetEntriesAction) TypeOK /\ H_TermsMonotonic /\ H_UniformLogEntries /\ H_LogMatching /\ H_LaterLogsHaveEarlierCommitted /\ GetEntriesActio... 161/161

▶ <2>. SUFFICES ASSUME TypeOK, H_TermsMonotonic, H_UniformLogEntries, H_LogMatching, H_LaterLogsHaveEarlierCommitted, GetEntrie... 1/1 smt

#120 L1354:10:1354:12 proved smt cached

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

#121 L1355:62:1355:64 proved smt cached

▶ <2>2 immediatelyCommitted' = immediatelyCommitted /\ c \in immediatelyCommitted BY <2>1 DEF GetEntries 2/2 smt

#122 L1356:86:1356:88 proved smt cached

#123 L1356:89:1356:93 trivial tlapm

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

#124 L1357:37:1357:39 proved smt cached

#125 L1357:40:1357:44 trivial tlapm

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

#126 L1358:58:1358:60 proved smt cached

▶ <2>5 CASE s # i 4/4 smt

#127 L1360:7:1360:9 proved smt cached

#128 L1360:10:1360:14 trivial tlapm

#129 L1360:16:1360:20 trivial tlapm

#130 L1360:22:1360:26 trivial tlapm

▶ <2>6 CASE s = i 147/147

▶ <3>. DEFINE newEntryIndex == IF Empty(log[i]) THEN 1 ELSE Len(log[i]) + 1

▶ <3>0 log'[i] = Append(log[i], log[j][newEntryIndex]) BY <2>1, <2>4 DEF GetEntries, Empty, TypeOK 3/3 smt

#135 L1363:61:1363:63 proved smt cached

#136 L1363:64:1363:68 trivial tlapm

#137 L1363:70:1363:74 trivial tlapm

▶ <3>0a Len(log[j]) > Len(log[i]) BY <2>1 DEF GetEntries 2/2 smt

#138 L1364:40:1364:42 proved smt cached

#139 L1364:43:1364:47 trivial tlapm

▶ <3>1 CASE idx \in DOMAIN log[i] 37/37

▶ <4>1 log[i][idx] > c[2] BY <2>6, <3>0, <3>1, <2>4 5/5 smt

#143 L1366:34:1366:36 proved smt cached

#144 L1366:37:1366:41 trivial tlapm

#145 L1366:43:1366:47 trivial tlapm

#146 L1366:49:1366:53 trivial tlapm

#147 L1366:55:1366:59 trivial tlapm

▶ <4>2 Len(log[i]) >= c[1] /\ log[i][c[1]] = c[2] 4/4 smt

#148 L1368:11:1368:13 proved smt cached

#149 L1368:14:1368:18 trivial tlapm

#150 L1368:20:1368:24 trivial tlapm

#151 L1368:26:1368:30 trivial tlapm

▶ <4>3 c[1] \in DOMAIN log[i] BY <2>3, <4>2, <2>4 4/4 smt

#152 L1369:38:1369:40 proved smt cached

#153 L1369:41:1369:45 trivial tlapm

#154 L1369:47:1369:51 trivial tlapm

#155 L1369:53:1369:57 trivial tlapm

▶ <4>4 Len(log'[i]) = Len(log[i]) + 1 BY <3>0, <2>4 3/3 smt

#156 L1370:46:1370:48 proved smt cached

#157 L1370:49:1370:53 trivial tlapm

#158 L1370:55:1370:59 trivial tlapm

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

#159 L1371:35:1371:37 proved smt cached

#160 L1371:38:1371:42 trivial tlapm

▶ <4>6 Len(log'[i]) >= c[1] BY <4>4, <4>2, <4>5, <2>3 5/5 smt

#161 L1372:36:1372:38 proved smt cached

#162 L1372:39:1372:43 trivial tlapm

#163 L1372:45:1372:49 trivial tlapm

#164 L1372:51:1372:55 trivial tlapm

#165 L1372:57:1372:61 trivial tlapm

▶ <4>7 log'[i][c[1]] = log[i][c[1]] BY <3>0, <4>3, <2>4 4/4 smt

#166 L1373:44:1373:46 proved smt cached

#167 L1373:47:1373:51 trivial tlapm

#168 L1373:53:1373:57 trivial tlapm

#169 L1373:59:1373:63 trivial tlapm

▶ <4>8 Len(log'[s]) >= c[1] BY <2>6, <4>6 3/3 smt

#170 L1374:36:1374:38 proved smt cached

#171 L1374:39:1374:43 trivial tlapm

#172 L1374:45:1374:49 trivial tlapm

▶ <4>9 log'[s][c[1]] = c[2] BY <2>6, <4>7, <4>2 4/4 smt

#173 L1375:36:1375:38 proved smt cached

#174 L1375:39:1375:43 trivial tlapm

#175 L1375:45:1375:49 trivial tlapm

#176 L1375:51:1375:55 trivial tlapm

▶ <4>. QED BY <4>8, <4>9 3/3 smt

#140 L1376:18:1376:20 proved smt cached

#141 L1376:21:1376:25 trivial tlapm

#142 L1376:27:1376:31 trivial tlapm

▶ <3>2 CASE idx \notin DOMAIN log[i] 100/100

▶ <4>1 log[j][newEntryIndex] > c[2] BY <2>6, <3>0, <3>2, <2>4 5/5 smt

#180 L1378:44:1378:46 proved smt cached

#181 L1378:47:1378:51 trivial tlapm

#182 L1378:53:1378:57 trivial tlapm

#183 L1378:59:1378:63 trivial tlapm

#184 L1378:65:1378:69 trivial tlapm

▶ <4>2 newEntryIndex \in DOMAIN log[j] BY <3>0a, <2>4 DEF Empty 3/3 smt

#185 L1379:47:1379:49 proved smt cached

#186 L1379:50:1379:55 trivial tlapm

#187 L1379:57:1379:61 trivial tlapm

▶ <4>3 Len(log[j]) >= c[1] /\ log[j][c[1]] = c[2] 4/4 smt

#188 L1381:11:1381:13 proved smt cached

#189 L1381:14:1381:18 trivial tlapm

#190 L1381:20:1381:24 trivial tlapm

#191 L1381:26:1381:30 trivial tlapm

▶ <4>4 c[1] \in DOMAIN log[j] BY <2>3, <4>3, <2>4 4/4 smt

#192 L1382:38:1382:40 proved smt cached

#193 L1382:41:1382:45 trivial tlapm

#194 L1382:47:1382:51 trivial tlapm

#195 L1382:53:1382:57 trivial tlapm

▶ <4>5 newEntryIndex \in DOMAIN log[j] BY <4>2 2/2 smt

#196 L1383:47:1383:49 proved smt cached

#197 L1383:50:1383:54 trivial tlapm

▶ <4>6 By H_TermsMonotonic on j: c[1] < newEntryIndex. log[j] \in Seq(Terms) BY <2>4 2/2 smt

#198 L1385:37:1385:39 proved smt cached

#199 L1385:40:1385:44 trivial tlapm

▶ <4>7 c[1] < newEntryIndex 6/6 smt

#200 L1387:11:1387:13 proved smt cached

#201 L1387:14:1387:18 trivial tlapm

#202 L1387:20:1387:24 trivial tlapm

#203 L1387:26:1387:30 trivial tlapm

#204 L1387:32:1387:36 trivial tlapm

#205 L1387:38:1387:42 trivial tlapm

▶ <4>8 CASE ~Empty(log[i]) 67/67

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

#209 L1389:37:1389:39 proved smt cached

#210 L1389:40:1389:44 trivial tlapm

▶ <5>1 c[1] <= Len(log[i]) BY <4>7, <4>8, <5>0, <2>3 DEF Empty 5/5 smt

#211 L1390:37:1390:39 proved smt cached

#212 L1390:40:1390:44 trivial tlapm

#213 L1390:46:1390:50 trivial tlapm

#214 L1390:52:1390:56 trivial tlapm

#215 L1390:58:1390:62 trivial tlapm

▶ <5>2 c[1] \in DOMAIN log[i] BY <2>3, <5>1, <2>4 4/4 smt

#216 L1391:40:1391:42 proved smt cached

#217 L1391:43:1391:47 trivial tlapm

#218 L1391:49:1391:53 trivial tlapm

#219 L1391:55:1391:59 trivial tlapm

▶ <5>3 Log consistency check + H_LogMatching give prefix agreement. Len(log[i]) \in DOMAIN log[i] BY <4>8, <2>4 DEF Empty 3/3 smt

#220 L1393:47:1393:49 proved smt cached

#221 L1393:50:1393:54 trivial tlapm

#222 L1393:56:1393:60 trivial tlapm

▶ <5>4 Len(log[i]) >= 1 BY <4>8, <2>4 DEF Empty 3/3 smt

#223 L1394:34:1394:36 proved smt cached

#224 L1394:37:1394:41 trivial tlapm

#225 L1394:43:1394:47 trivial tlapm

▶ <5>4a Len(log[j]) \in Nat BY <2>4 2/2 smt

#226 L1395:38:1395:40 proved smt cached

#227 L1395:41:1395:45 trivial tlapm

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

#228 L1396:48:1396:50 proved smt cached

#229 L1396:51:1396:56 trivial tlapm

#230 L1396:58:1396:62 trivial tlapm

#231 L1396:64:1396:68 trivial tlapm

#232 L1396:70:1396:75 trivial tlapm

#233 L1396:77:1396:81 trivial tlapm

▶ <5>5 log[j][Len(log[i])] = log[i][Len(log[i])] BY <2>1, <4>8 DEF GetEntries, Empty 3/3 smt

#234 L1397:59:1397:61 proved smt cached

#235 L1397:62:1397:66 trivial tlapm

#236 L1397:68:1397:72 trivial tlapm

▶ <5>6 Len(log[i]) \in DOMAIN log[j] BY <5>4b 2/2 smt

#237 L1398:47:1398:49 proved smt cached

#238 L1398:50:1398:55 trivial tlapm

▶ <5>6a Instantiate H_LogMatching: matching index Len(log[i]) in log[i] and log[j]. log[i][Len(log[i])] = log[j][Len(log[i])] BY <5>5 2/2 smt

#239 L1400:60:1400:62 proved smt

#240 L1400:63:1400:67 trivial tlapm

▶ <5>6b \E k \in DOMAIN log[j] : k = Len(log[i]) /\ log[i][Len(log[i])] = log[j][k] 3/3 smt

#241 L1402:13:1402:15 proved smt

#242 L1402:16:1402:20 trivial tlapm

#243 L1402:22:1402:27 trivial tlapm

▶ <5>6c SubSeq(log[i], 1, Len(log[i])) = SubSeq(log[j], 1, Len(log[i])) 3/3 smt

#244 L1404:13:1404:15 proved smt

#245 L1404:16:1404:20 trivial tlapm

#246 L1404:22:1404:27 trivial tlapm

▶ <5>7 log[i][c[1]] = log[j][c[1]] BY <5>1, <5>6c, <5>2, <2>4, <2>3 6/6 smt

#247 L1405:45:1405:47 proved smt cached

#248 L1405:48:1405:52 trivial tlapm

#249 L1405:54:1405:59 trivial tlapm

#250 L1405:61:1405:65 trivial tlapm

#251 L1405:67:1405:71 trivial tlapm

#252 L1405:73:1405:77 trivial tlapm

▶ <5>8 log'[i][c[1]] = log[i][c[1]] BY <3>0, <5>2, <2>4 4/4 smt

#253 L1406:46:1406:48 proved smt cached

#254 L1406:49:1406:53 trivial tlapm

#255 L1406:55:1406:59 trivial tlapm

#256 L1406:61:1406:65 trivial tlapm

▶ <5>9 Len(log'[i]) = Len(log[i]) + 1 BY <3>0, <2>4 3/3 smt

#257 L1407:48:1407:50 proved smt cached

#258 L1407:51:1407:55 trivial tlapm

#259 L1407:57:1407:61 trivial tlapm

▶ <5>10 Len(log'[i]) >= c[1] BY <5>9, <5>1, <5>0, <2>3 5/5 smt

#260 L1408:39:1408:41 proved smt cached

#261 L1408:42:1408:46 trivial tlapm

#262 L1408:48:1408:52 trivial tlapm

#263 L1408:54:1408:58 trivial tlapm

#264 L1408:60:1408:64 trivial tlapm

▶ <5>11 Len(log'[s]) >= c[1] BY <2>6, <5>10 3/3 smt

#265 L1409:39:1409:41 proved smt cached

#266 L1409:42:1409:46 trivial tlapm

#267 L1409:48:1409:53 trivial tlapm

▶ <5>12 log'[s][c[1]] = c[2] BY <2>6, <5>8, <5>7, <4>3 5/5 smt

#268 L1410:39:1410:41 proved smt cached

#269 L1410:42:1410:46 trivial tlapm

#270 L1410:48:1410:52 trivial tlapm

#271 L1410:54:1410:58 trivial tlapm

#272 L1410:60:1410:64 trivial tlapm

▶ <5>. QED BY <5>11, <5>12 3/3 smt

#206 L1411:20:1411:22 proved smt cached

#207 L1411:23:1411:28 trivial tlapm

#208 L1411:30:1411:35 trivial tlapm

▶ <4>9 CASE Empty(log[i]) 4/4 smt

#273 L1413:11:1413:13 proved smt cached

#274 L1413:14:1413:18 trivial tlapm

#275 L1413:20:1413:24 trivial tlapm

#276 L1413:26:1413:30 trivial tlapm

▶ <4>. QED BY <4>8, <4>9 DEF Empty 3/3 smt

#177 L1414:18:1414:20 proved smt cached

#178 L1414:21:1414:25 trivial tlapm

#179 L1414:27:1414:31 trivial tlapm

▶ <3>3 idx \in DOMAIN log[i] \/ idx \notin DOMAIN log[i] OBVIOUS 1/1 smt

#277 L1415:63:1415:70 proved smt cached

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

#131 L1416:16:1416:18 proved smt cached

#132 L1416:19:1416:23 trivial tlapm

#133 L1416:25:1416:29 trivial tlapm

#134 L1416:31:1416:35 trivial tlapm

▶ <2>. QED BY <2>5, <2>6 3/3 smt

#117 L1417:14:1417:16 proved smt cached

#118 L1417:17:1417:21 trivial tlapm

#119 L1417:23:1417:27 trivial tlapm

▶ <1>3 (H_LaterLogsHaveEarlierCommitted,RollbackEntriesAction) TypeOK /\ H_TermsMonotonic /\ H_LaterLogsHaveEarlierCommitted /\ RollbackEntriesAction => H_LaterLogsHaveEarlierCommitte... 84/84

▶ <2>. SUFFICES ASSUME TypeOK, H_TermsMonotonic, H_LaterLogsHaveEarlierCommitted, RollbackEntriesAction, 1/1 smt

#281 L1425:10:1425:12 proved smt cached

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

#282 L1427:10:1427:12 proved smt cached

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

#283 L1428:56:1428:58 proved smt cached

#284 L1428:59:1428:63 trivial tlapm

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

#285 L1429:37:1429:39 proved smt cached

#286 L1429:40:1429:44 trivial tlapm

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

#287 L1430:33:1430:35 proved smt cached

▶ <2>5 CASE s # i 4/4 smt

#288 L1432:7:1432:9 proved smt cached

#289 L1432:10:1432:14 trivial tlapm

#290 L1432:16:1432:20 trivial tlapm

#291 L1432:22:1432:26 trivial tlapm

▶ <2>6 CASE s = i 70/70

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

#295 L1434:56:1434:58 proved smt cached

#296 L1434:59:1434:63 trivial tlapm

#297 L1434:65:1434:69 trivial tlapm

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

#298 L1435:40:1435:42 proved smt cached

#299 L1435:43:1435:47 trivial tlapm

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

#300 L1436:29:1436:31 proved smt cached

#301 L1436:32:1436:36 trivial tlapm

▶ <3>4 idx is in DOMAIN SubSeq = 1..Len(log[i])-1, so idx \in DOMAIN log[i] too. idx \in DOMAIN log[i] /\ log[i][idx] > c[2] 5/5 smt

#302 L1439:9:1439:11 proved smt cached

#303 L1439:12:1439:16 trivial tlapm

#304 L1439:18:1439:22 trivial tlapm

#305 L1439:24:1439:28 trivial tlapm

#306 L1439:30:1439:34 trivial tlapm

▶ <3>5 Len(log[i]) >= c[1] /\ log[i][c[1]] = c[2] 3/3 smt

#307 L1441:9:1441:11 proved smt cached

#308 L1441:12:1441:16 trivial tlapm

#309 L1441:18:1441:22 trivial tlapm

▶ <3>6 By H_TermsMonotonic, idx > c[1]. c[1] \in DOMAIN log[i] BY <2>3, <3>5, <2>4 4/4 smt

#310 L1443:36:1443:38 proved smt cached

#311 L1443:39:1443:43 trivial tlapm

#312 L1443:45:1443:49 trivial tlapm

#313 L1443:51:1443:55 trivial tlapm

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

#314 L1444:34:1444:36 proved smt cached

#315 L1444:37:1444:41 trivial tlapm

▶ <3>7 idx > c[1] 5/5 smt

#316 L1446:9:1446:11 proved smt cached

#317 L1446:12:1446:16 trivial tlapm

#318 L1446:18:1446:22 trivial tlapm

#319 L1446:24:1446:28 trivial tlapm

#320 L1446:30:1446:34 trivial tlapm

▶ <3>8 idx <= Len(log[i])-1, so c[1] < idx <= Len(log[i])-1. idx <= Len(log[i]) - 1 BY <2>6, <3>1, <3>3, <2>4 5/5 smt

#321 L1448:36:1448:38 proved smt cached

#322 L1448:39:1448:43 trivial tlapm

#323 L1448:45:1448:49 trivial tlapm

#324 L1448:51:1448:55 trivial tlapm

#325 L1448:57:1448:61 trivial tlapm

▶ <3>9 idx \in Nat BY <3>4, <3>6a 3/3 smt

#326 L1449:25:1449:27 proved smt cached

#327 L1449:28:1449:32 trivial tlapm

#328 L1449:34:1449:39 trivial tlapm

▶ <3>10 c[1] <= Len(log[i]) - 1 BY <3>7, <3>8, <3>9, <2>3, <3>6a 6/6 smt

#329 L1450:38:1450:40 proved smt cached

#330 L1450:41:1450:45 trivial tlapm

#331 L1450:47:1450:51 trivial tlapm

#332 L1450:53:1450:57 trivial tlapm

#333 L1450:59:1450:63 trivial tlapm

#334 L1450:65:1450:70 trivial tlapm

▶ <3>11 Len(log'[i]) = Len(log[i]) - 1 BY <3>1, <3>3, <2>4 4/4 smt

#335 L1451:45:1451:47 proved smt cached

#336 L1451:48:1451:52 trivial tlapm

#337 L1451:54:1451:58 trivial tlapm

#338 L1451:60:1451:64 trivial tlapm

▶ <3>12 Len(log'[i]) >= c[1] BY <3>11, <3>10, <3>6a, <2>3 5/5 smt

#339 L1452:35:1452:37 proved smt cached

#340 L1452:38:1452:43 trivial tlapm

#341 L1452:45:1452:50 trivial tlapm

#342 L1452:52:1452:57 trivial tlapm

#343 L1452:59:1452:63 trivial tlapm

▶ <3>13 c[1] \in DOMAIN log'[i] BY <2>3, <3>10, <3>11, <3>3, <3>6a 6/6 smt

#344 L1453:38:1453:40 proved smt cached

#345 L1453:41:1453:45 trivial tlapm

#346 L1453:47:1453:52 trivial tlapm

#347 L1453:54:1453:59 trivial tlapm

#348 L1453:61:1453:65 trivial tlapm

#349 L1453:67:1453:72 trivial tlapm

▶ <3>14 log'[i][c[1]] = log[i][c[1]] BY <3>1, <3>13, <3>3, <2>4 5/5 smt

#350 L1454:43:1454:45 proved smt cached

#351 L1454:46:1454:50 trivial tlapm

#352 L1454:52:1454:57 trivial tlapm

#353 L1454:59:1454:63 trivial tlapm

#354 L1454:65:1454:69 trivial tlapm

▶ <3>15 Len(log'[s]) >= c[1] BY <2>6, <3>12 3/3 smt

#355 L1455:35:1455:37 proved smt cached

#356 L1455:38:1455:42 trivial tlapm

#357 L1455:44:1455:49 trivial tlapm

▶ <3>16 log'[s][c[1]] = c[2] BY <2>6, <3>14, <3>5 4/4 smt

#358 L1456:35:1456:37 proved smt cached

#359 L1456:38:1456:42 trivial tlapm

#360 L1456:44:1456:49 trivial tlapm

#361 L1456:51:1456:55 trivial tlapm

▶ <3>. QED BY <3>15, <3>16 3/3 smt

#292 L1457:16:1457:18 proved smt cached

#293 L1457:19:1457:24 trivial tlapm

#294 L1457:26:1457:31 trivial tlapm

▶ <2>. QED BY <2>5, <2>6 3/3 smt

#278 L1458:14:1458:16 proved smt cached

#279 L1458:17:1458:21 trivial tlapm

#280 L1458:23:1458:27 trivial tlapm

▶ <1>4 (H_LaterLogsHaveEarlierCommitted,BecomeLeaderAction) TypeOK /\ H_LaterLogsHaveEarlierCommitted /\ BecomeLeaderAction => H_LaterLogsHaveEarlierCommitted' BY DEF TypeOK,Become... 1/1 smt

#362 L1460:109:1460:111 proved smt cached

▶ <1>5 (H_LaterLogsHaveEarlierCommitted,CommitEntryAction) TypeOK /\ H_LogEntryImpliesSafeAtTerm /\ H_LaterLogsHaveEarlierCommitted /\ CommitEntryAction => H_LaterLogsHaveEarlierC... 59/59

▶ <2>. SUFFICES ASSUME TypeOK, H_LogEntryImpliesSafeAtTerm, H_LaterLogsHaveEarlierCommitted, CommitEntryAction, 1/1 smt

#367 L1468:10:1468:12 proved smt cached

▶ <2>1 PICK leader \in Server, commitQuorum \in Quorums(Server) : CommitEntry(leader, commitQuorum) 1/1 smt

#368 L1470:10:1470:12 proved smt cached

▶ <2>2 UNCHANGED log BY <2>1 DEF CommitEntry 2/2 smt

#369 L1471:25:1471:27 proved smt cached

#370 L1471:28:1471:32 trivial tlapm

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

#371 L1473:7:1473:9 proved smt cached

#372 L1473:10:1473:14 trivial tlapm

#373 L1473:16:1473:20 trivial tlapm

▶ <2>4 CASE c = <<Len(log[leader]), currentTerm[leader]>> /\ c \notin immediatelyCommitted 48/48

▶ <3>1 Newly committed entry. Derive contradiction: no server can have entry > currentTerm[leader]. commitQuorum \subseteq Server BY DEF Quorums 1/1 smt

#378 L1476:43:1476:45 proved smt cached

▶ <3>2 \A q \in commitQuorum : currentTerm[q] = currentTerm[leader] 2/2 smt

#379 L1478:9:1478:11 proved smt cached

#380 L1478:12:1478:16 trivial tlapm

▶ <3>3 idx \in DOMAIN log[s] /\ log[s][idx] > currentTerm[leader] BY <2>2, <2>4 DEF TypeOK 3/3 smt

#381 L1479:72:1479:74 proved smt cached

#382 L1479:75:1479:79 trivial tlapm

#383 L1479:81:1479:85 trivial tlapm

▶ <3>4 \E Q2 \in Quorums(Server) : \A n \in Q2 : currentTerm[n] >= log[s][idx] 2/2 smt

#384 L1481:9:1481:11 proved smt cached

#385 L1481:12:1481:16 trivial tlapm

▶ <3>5 IsFiniteSet(Server) BY DEF TypeOK 1/1 smt

#386 L1482:33:1482:35 proved smt cached

▶ <3>6 Quorum intersection. PICK Q2 \in Quorums(Server) : \A n \in Q2 : currentTerm[n] >= log[s][idx] 2/2 smt

#387 L1485:9:1485:11 proved smt cached

#388 L1485:12:1485:16 trivial tlapm

▶ <3>7 Q2 \subseteq Server /\ commitQuorum \subseteq Server BY DEF Quorums 1/1 smt

#389 L1486:66:1486:68 proved smt cached

▶ <3>8 IsFiniteSet(Q2) /\ IsFiniteSet(commitQuorum) BY <3>5, <3>7, FS_Subset 4/4 smt

#390 L1487:58:1487:60 proved smt cached

#391 L1487:61:1487:65 trivial tlapm

#392 L1487:67:1487:71 trivial tlapm

#393 L1487:73:1487:82 trivial tlapm

▶ <3>9 Cardinality(Q2) \in Nat /\ Cardinality(commitQuorum) \in Nat /\ Cardinality(Server) \in Nat 4/4 smt

#394 L1489:9:1489:11 proved smt cached

#395 L1489:12:1489:16 trivial tlapm

#396 L1489:18:1489:22 trivial tlapm

#397 L1489:24:1489:42 trivial tlapm

▶ <3>10 Cardinality(Q2) * 2 > Cardinality(Server) /\ Cardinality(commitQuorum) * 2 > Cardinality(Server) 3/3 smt

#398 L1491:9:1491:11 proved smt cached

#399 L1491:12:1491:16 trivial tlapm

#400 L1491:18:1491:22 trivial tlapm

▶ <3>11 Cardinality(Q2) + Cardinality(commitQuorum) > Cardinality(Server) 3/3 smt

#401 L1493:9:1493:11 proved smt cached

#402 L1493:12:1493:16 trivial tlapm

#403 L1493:18:1493:23 trivial tlapm

▶ <3>12 Q2 \cap commitQuorum # {} 5/5 smt

#404 L1495:9:1495:11 proved smt cached

#405 L1495:12:1495:16 trivial tlapm

#406 L1495:18:1495:22 trivial tlapm

#407 L1495:24:1495:29 trivial tlapm

#408 L1495:31:1495:53 trivial tlapm

▶ <3>13 PICK n \in Server : n \in Q2 /\ n \in commitQuorum 3/3 smt

#409 L1497:9:1497:11 proved smt cached

#410 L1497:12:1497:17 trivial tlapm

#411 L1497:19:1497:23 trivial tlapm

▶ <3>14 currentTerm[n] >= log[s][idx] /\ currentTerm[n] = currentTerm[leader] 4/4 smt

#412 L1499:9:1499:11 proved smt cached

#413 L1499:12:1499:17 trivial tlapm

#414 L1499:19:1499:23 trivial tlapm

#415 L1499:25:1499:29 trivial tlapm

▶ <3>14a idx \in DOMAIN log[s] BY <2>2, <3>3 3/3 smt

#416 L1500:37:1500:39 proved smt cached

#417 L1500:40:1500:44 trivial tlapm

#418 L1500:46:1500:50 trivial tlapm

▶ <3>15 currentTerm[n] \in Nat /\ log[s][idx] \in Nat /\ currentTerm[leader] \in Nat 3/3 smt

#419 L1502:9:1502:11 proved smt cached

#420 L1502:12:1502:17 trivial tlapm

#421 L1502:19:1502:25 trivial tlapm

▶ <3>. QED BY <3>3, <3>14, <3>15 4/4 smt

#374 L1503:16:1503:18 proved smt cached

#375 L1503:19:1503:23 trivial tlapm

#376 L1503:25:1503:30 trivial tlapm

#377 L1503:32:1503:37 trivial tlapm

▶ <2>. QED BY <2>1, <2>3, <2>4 DEF CommitEntry 4/4 smt

#363 L1504:14:1504:16 proved smt cached

#364 L1504:17:1504:21 trivial tlapm

#365 L1504:23:1504:27 trivial tlapm

#366 L1504:29:1504:33 trivial tlapm

▶ <1>6 (H_LaterLogsHaveEarlierCommitted,UpdateTermsAction) TypeOK /\ H_LaterLogsHaveEarlierCommitted /\ UpdateTermsAction => H_LaterLogsHaveEarlierCommitted' BY DEF TypeOK,UpdateT... 1/1 smt

#422 L1506:108:1506:110 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 L1507:11:1507:13 proved smt cached

#2 L1507:14:1507:18 trivial tlapm

#3 L1507:19:1507:23 trivial tlapm

#4 L1507:24:1507:28 trivial tlapm

#5 L1507:29:1507:33 trivial tlapm

#6 L1507:34:1507:38 trivial tlapm

#7 L1507:39:1507:43 trivial tlapm

THEOREM L_10 (H_LaterLogsHaveEarlierCommitted)

Proof Notes

Proof Tree