Proof Status: THEOREM L

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

#8 L1017:12:1017:14 trivial tlapm

#9 L1017:15:1017:17 trivial tlapm

#10 L1017:18:1017:20 trivial tlapm

#11 L1017:21:1017:23 trivial tlapm

#12 L1017:24:1017:26 trivial tlapm

#13 L1017:27:1017:29 trivial tlapm

#14 L1017:30:1017:32 trivial tlapm

▶ <1>1 (H_LeaderCompleteness,ClientRequestAction) TypeOK /\ H_LeaderCompleteness /\ ClientRequestAction => H_LeaderCompleteness' BY DEF TypeOK,ClientRequestAction,ClientRequest,H_LeaderComplet... 1/1 smt

#15 L1019:88:1019:90 proved smt cached

▶ <1>2 (H_LeaderCompleteness,GetEntriesAction) TypeOK /\ H_LeaderCompleteness /\ GetEntriesAction => H_LeaderCompleteness' BY DEF TypeOK,GetEntriesAction,GetEntries,H_LeaderCompleteness,InL... 1/1 smt

#16 L1021:85:1021:87 proved smt cached

▶ <1>3 (H_LeaderCompleteness,RollbackEntriesAction) TypeOK /\ H_LeaderCompleteness /\ RollbackEntriesAction => H_LeaderCompleteness' 12/12 smt

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

#21 L1026:38:1026:40 proved smt cached

▶ <2>1 state[i] = Secondary BY DEF RollbackEntries 1/1 smt

#22 L1027:32:1027:34 proved smt cached

▶ <2>2 UNCHANGED <<state, currentTerm, immediatelyCommitted>> BY DEF RollbackEntries 1/1 smt

#23 L1028:66:1028:68 proved smt cached

▶ <2>3 \A s \in Server : s # i => log'[s] = log[s] BY DEF RollbackEntries, TypeOK 1/1 smt

#24 L1029:55:1029:57 proved smt cached

▶ <2>4 \A s \in Server : state'[s] = Primary => s # i 4/4 tlapm

#25 L1031:7:1031:9 proved smt cached

#26 L1031:10:1031:14 trivial tlapm

#27 L1031:16:1031:20 trivial tlapm

#28 L1031:22:1031:24 trivial tlapm

▶ <2>. QED BY <2>2, <2>3, <2>4 DEF H_LeaderCompleteness, InLog 4/4 tlapm

#17 L1032:14:1032:16 proved smt cached

#18 L1032:17:1032:21 trivial tlapm

#19 L1032:23:1032:27 trivial tlapm

#20 L1032:29:1032:33 trivial tlapm

▶ <1>4 (H_LeaderCompleteness,BecomeLeaderAction) TypeOK /\ H_TermsMonotonic /\ H_UniformLogEntries /\ H_CommittedEntryIsOnQuorum /\ H_LaterLogsHaveEarlierCommitted /\ H_LeaderCompleteness /\ BecomeLe... 296/296 tlapm

▶ <2>. SUFFICES ASSUME TypeOK, H_TermsMonotonic, H_UniformLogEntries, H_CommittedEntryIsOnQuorum, 1/1 smt

#32 L1038:38:1038:40 proved smt cached

▶ <2>1 UNCHANGED <<log, immediatelyCommitted>> BY DEF BecomeLeader 1/1 smt

#33 L1039:51:1039:53 proved smt cached

▶ <2>2 state' = [s \in Server |-> IF s = leader THEN Primary ELSE IF s \in voteQ THEN Secondary ELSE state[s]] 1/1 smt

#34 L1041:7:1041:9 proved smt cached

▶ <2>3 currentTerm' = [s \in Server |-> IF s \in voteQ THEN currentTerm[leader] + 1 ELSE currentTerm[s]] 1/1 smt

#35 L1043:7:1043:9 proved smt cached

▶ <2>4 leader \in voteQ BY DEF BecomeLeader 1/1 smt

#36 L1044:28:1044:30 proved smt cached

▶ <2>5 \A v \in voteQ : CanVoteForOplog(v, leader, currentTerm[leader] + 1) BY DEF BecomeLeader 1/1 smt

#37 L1045:80:1045:82 proved smt cached

▶ <2>qi Quorum intersection \A Q1, Q2 \in Quorums(Server) : Q1 \cap Q2 # {} 24/24 tlapm

▶ <3>1 IsFiniteSet(Server) BY A0 2/2 smt

#43 L1048:33:1048:35 proved smt cached

#44 L1048:36:1048:38 trivial tlapm

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

#45 L1049:106:1049:113 proved smt cached

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

#46 L1050:56:1050:58 proved smt cached

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

#47 L1051:48:1051:50 proved smt cached

#48 L1051:51:1051:55 trivial tlapm

#49 L1051:57:1051:61 trivial tlapm

#50 L1051:63:1051:72 trivial tlapm

▶ <3>5 Cardinality(Q1) * 2 > Cardinality(Server) /\ Cardinality(Q2) * 2 > Cardinality(Server) BY DEF Quorums 1/1 smt

#51 L1052:100:1052:102 proved smt cached

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

#52 L1053:41:1053:43 proved smt cached

#53 L1053:44:1053:48 trivial tlapm

#54 L1053:50:1053:68 trivial tlapm

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

#55 L1054:64:1054:66 proved smt cached

#56 L1054:67:1054:71 trivial tlapm

#57 L1054:73:1054:91 trivial tlapm

▶ <3>8 Cardinality(Q1) + Cardinality(Q2) > Cardinality(Server) BY <3>5, <3>6, <3>7 4/4 tlapm

#58 L1055:69:1055:71 proved smt cached

#59 L1055:72:1055:76 trivial tlapm

#60 L1055:78:1055:82 trivial tlapm

#61 L1055:84:1055:88 trivial tlapm

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

#38 L1056:16:1056:18 proved smt cached

#39 L1056:19:1056:23 trivial tlapm

#40 L1056:25:1056:29 trivial tlapm

#41 L1056:31:1056:35 trivial tlapm

#42 L1056:37:1056:59 trivial tlapm

▶ <2>. SUFFICES: show for any primary s in post-state, all committed entries with smaller terms are in log'[s] SUFFICES ASSUME NEW s \in Server, state'[s] = Primary, 2/2 smt

#62 L1060:41:1060:43 proved smt cached

#63 L1060:44:1060:48 trivial tlapm

▶ <2>6 Case s # leader: s was already primary, use induction hypothesis CASE s # leader 20/20 tlapm

▶ <3>1 state[s] = Primary BY <2>6, <2>2, A7 4/4 tlapm

#67 L1063:32:1063:34 proved smt cached

#68 L1063:35:1063:39 trivial tlapm

#69 L1063:41:1063:45 trivial tlapm

#70 L1063:47:1063:49 trivial tlapm

▶ <3>2 s \notin voteQ BY <2>6, <2>2, <3>1, A7 5/5 tlapm

#71 L1064:28:1064:30 proved smt cached

#72 L1064:31:1064:35 trivial tlapm

#73 L1064:37:1064:41 trivial tlapm

#74 L1064:43:1064:47 trivial tlapm

#75 L1064:49:1064:51 trivial tlapm

▶ <3>3 currentTerm'[s] = currentTerm[s] BY <3>2, <2>3 3/3 tlapm

#76 L1065:46:1065:48 proved smt cached

#77 L1065:49:1065:53 trivial tlapm

#78 L1065:55:1065:59 trivial tlapm

▶ <3>4 c[2] < currentTerm[s] BY <3>3 2/2 smt

#79 L1066:35:1066:37 proved smt cached

#80 L1066:38:1066:42 trivial tlapm

▶ <3>5 InLog(<<c[1],c[2]>>, s) BY <3>1, <3>4 DEF H_LeaderCompleteness 3/3 tlapm

#81 L1067:37:1067:39 proved smt cached

#82 L1067:40:1067:44 trivial tlapm

#83 L1067:46:1067:50 trivial tlapm

▶ <3>. QED BY <3>5, <2>1 DEF InLog 3/3 tlapm

#64 L1068:16:1068:18 proved smt cached

#65 L1068:19:1068:23 trivial tlapm

#66 L1068:25:1068:29 trivial tlapm

▶ <2>7 Case s = leader: the new primary must have all committed entries CASE s = leader 241/241 tlapm

▶ <3>0 currentTerm'[leader] = currentTerm[leader]+1 since leader ∈ voteQ currentTerm'[leader] = currentTerm[leader] + 1 BY <2>3, <2>4 3/3 tlapm

#88 L1072:60:1072:62 proved smt cached

#89 L1072:63:1072:67 trivial tlapm

#90 L1072:69:1072:73 trivial tlapm

▶ <3>ct c[2] <= currentTerm[leader] c[2] \in Nat /\ currentTerm[leader] \in Nat BY DEF TypeOK, Terms, H_CommittedEntryIsOnQuorum, InLog 1/1 smt

#91 L1074:58:1074:60 proved smt cached

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

#92 L1075:43:1075:45 proved smt cached

▶ <3>1 c[2] < currentTerm[leader] + 1 BY <2>7, <3>0 3/3 tlapm

#93 L1076:44:1076:46 proved smt cached

#94 L1076:47:1076:51 trivial tlapm

#95 L1076:53:1076:57 trivial tlapm

▶ <3>2 From H_CommittedEntryIsOnQuorum, get quorum Qc where everyone has InLog(c, n) PICK Qc \in Quorums(Server) : \A n \in Qc : InLog(<<c[1],c[2]>>, n) 1/1 smt

#96 L1079:9:1079:11 proved smt cached

▶ <3>3 Qc and voteQ intersect Qc \cap voteQ # {} BY <2>qi 2/2 smt

#97 L1081:32:1081:34 proved smt cached

#98 L1081:35:1081:40 trivial tlapm

▶ <3>4 PICK w \in Qc \cap voteQ : TRUE BY <3>3 2/2 smt

#99 L1082:45:1082:47 proved smt cached

#100 L1082:48:1082:52 trivial tlapm

▶ <3>5 InLog(<<c[1],c[2]>>, w) BY <3>4, <3>2 3/3 tlapm

#101 L1083:37:1083:39 proved smt cached

#102 L1083:40:1083:44 trivial tlapm

#103 L1083:46:1083:50 trivial tlapm

▶ <3>6 CanVoteForOplog(w, leader, currentTerm[leader] + 1) BY <3>4, <2>5 3/3 tlapm

#104 L1084:65:1084:67 proved smt cached

#105 L1084:68:1084:72 trivial tlapm

#106 L1084:74:1084:78 trivial tlapm

▶ <3>7 Expand InLog for w PICK xw \in DOMAIN log[w] : xw = c[1] /\ log[w][xw] = c[2] BY <3>5 DEF InLog 2/2 smt

#107 L1086:72:1086:74 proved smt cached

#108 L1086:75:1086:79 trivial tlapm

▶ <3>8 c[1] \in DOMAIN log[w] /\ log[w][c[1]] = c[2] BY <3>7 2/2 smt

#109 L1087:59:1087:61 proved smt cached

#110 L1087:62:1087:66 trivial tlapm

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

#111 L1088:26:1088:28 proved smt cached

#112 L1088:29:1088:33 trivial tlapm

#113 L1088:35:1088:37 trivial tlapm

▶ <3>10 CanVoteForOplog means: LastTerm(log[leader]) > LastTerm(log[w]) OR (equal and longer) LET logOk == \/ LastTerm(log[leader]) > LastTerm(log[w]) 2/2 smt

#114 L1094:9:1094:11 proved smt cached

#115 L1094:12:1094:16 trivial tlapm

▶ <3>11 By H_TermsMonotonic: c[2] = log[w][c[1]] <= LastTerm(log[w]) Len(log[w]) \in Nat /\ Len(log[w]) > 0 2/2 smt

#116 L1097:9:1097:11 proved smt cached

#117 L1097:12:1097:16 trivial tlapm

▶ <3>12 Len(log[w]) \in DOMAIN log[w] 2/2 smt

#118 L1099:9:1099:11 proved smt cached

#119 L1099:12:1099:17 trivial tlapm

▶ <3>13 c[2] <= LastTerm(log[w]) 10/10 tlapm

▶ <3>14 Case A: LastTerm(log[leader]) > LastTerm(log[w]) >= c[2] CASE LastTerm(log[leader]) > LastTerm(log[w]) 37/37 tlapm

▶ <4>1 LastTerm(log[leader]) > c[2] LastTerm(log[leader]) > c[2] 6/6 tlapm

▶ <4>2 log[leader] is non-empty ~Empty(log[leader]) 7/7 tlapm

▶ <4>2a Len(log[leader]) > 0 BY <4>2 DEF Empty 2/2 smt

#146 L1116:37:1116:39 proved smt cached

#147 L1116:40:1116:44 trivial tlapm

▶ <4>3 Len(log[leader]) \in DOMAIN log[leader] BY <4>2a DEF TypeOK 2/2 smt

#148 L1117:55:1117:57 proved smt cached

#149 L1117:58:1117:63 trivial tlapm

▶ <4>4 log[leader][Len(log[leader])] > c[2] 3/3 tlapm

#150 L1119:11:1119:13 proved smt cached

#151 L1119:14:1119:18 trivial tlapm

#152 L1119:20:1119:24 trivial tlapm

▶ <4>5 There exists an entry in log[leader] with term > c[2] \E idx \in DOMAIN log[leader] : log[leader][idx] > c[2] 3/3 tlapm

#153 L1122:11:1122:13 proved smt cached

#154 L1122:14:1122:18 trivial tlapm

#155 L1122:20:1122:24 trivial tlapm

▶ <4>6 By H_LaterLogsHaveEarlierCommitted: Len(log[leader]) >= c[1] /\ log[leader][c[1]] = c[2] Len(log[leader]) >= c[1] /\ log[leader][c[1]] = c[2] 2/2 smt

#156 L1125:11:1125:13 proved smt cached

#157 L1125:14:1125:18 trivial tlapm

▶ <4>7 c[1] \in DOMAIN log[leader] BY <4>6, <3>c1pos DEF TypeOK 3/3 tlapm

#158 L1126:43:1126:45 proved smt cached

#159 L1126:46:1126:50 trivial tlapm

#160 L1126:52:1126:60 trivial tlapm

▶ <4>8 log'[leader] = log[leader] BY <2>1 2/2 smt

#161 L1127:42:1127:44 proved smt cached

#162 L1127:45:1127:49 trivial tlapm

▶ <4>9 c[1] \in DOMAIN log'[leader] /\ log'[leader][c[1]] = c[2] BY <4>6, <4>7, <4>8 4/4 tlapm

#163 L1128:73:1128:75 proved smt cached

#164 L1128:76:1128:80 trivial tlapm

#165 L1128:82:1128:86 trivial tlapm

#166 L1128:88:1128:92 trivial tlapm

▶ <4>. QED BY <4>9, <2>7 DEF InLog 3/3 tlapm

#130 L1129:18:1129:20 proved smt cached

#131 L1129:21:1129:25 trivial tlapm

#132 L1129:27:1129:31 trivial tlapm

▶ <3>15 Case B: equal last terms and leader's log at least as long CASE LastTerm(log[leader]) = LastTerm(log[w]) /\ Len(log[leader]) >= Len(log[w]) 158/158 tlapm

▶ <4>1 Sub-case B1: LastTerm(log[w]) > c[2] - same as Case A CASE LastTerm(log[w]) > c[2] 32/32 tlapm

▶ <5>1 LastTerm(log[leader]) > c[2] BY <3>15, <4>1 3/3 tlapm

#176 L1134:46:1134:48 proved smt cached

#177 L1134:49:1134:54 trivial tlapm

#178 L1134:56:1134:60 trivial tlapm

▶ <5>2 ~Empty(log[leader]) 5/5 tlapm

▶ <5>2a Len(log[leader]) > 0 BY <5>2 DEF Empty 2/2 smt

#184 L1138:39:1138:41 proved smt cached

#185 L1138:42:1138:46 trivial tlapm

▶ <5>3 Len(log[leader]) \in DOMAIN log[leader] BY <5>2a DEF TypeOK 2/2 smt

#186 L1139:57:1139:59 proved smt cached

#187 L1139:60:1139:65 trivial tlapm

▶ <5>4 log[leader][Len(log[leader])] > c[2] BY <5>1, <5>2 DEF LastTerm, Empty 3/3 tlapm

#188 L1140:54:1140:56 proved smt cached

#189 L1140:57:1140:61 trivial tlapm

#190 L1140:63:1140:67 trivial tlapm

▶ <5>5 \E idx \in DOMAIN log[leader] : log[leader][idx] > c[2] 3/3 tlapm

#191 L1142:13:1142:15 proved smt cached

#192 L1142:16:1142:20 trivial tlapm

#193 L1142:22:1142:26 trivial tlapm

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

#194 L1144:13:1144:15 proved smt cached

#195 L1144:16:1144:20 trivial tlapm

▶ <5>7 c[1] \in DOMAIN log[leader] BY <5>6, <3>c1pos DEF TypeOK 3/3 tlapm

#196 L1145:45:1145:47 proved smt cached

#197 L1145:48:1145:52 trivial tlapm

#198 L1145:54:1145:62 trivial tlapm

▶ <5>8 log'[leader] = log[leader] BY <2>1 2/2 smt

#199 L1146:44:1146:46 proved smt cached

#200 L1146:47:1146:51 trivial tlapm

▶ <5>9 c[1] \in DOMAIN log'[leader] /\ log'[leader][c[1]] = c[2] BY <5>6, <5>7, <5>8 4/4 tlapm

#201 L1147:75:1147:77 proved smt cached

#202 L1147:78:1147:82 trivial tlapm

#203 L1147:84:1147:88 trivial tlapm

#204 L1147:90:1147:94 trivial tlapm

▶ <5>. QED BY <5>9, <2>7 DEF InLog 3/3 tlapm

#173 L1148:20:1148:22 proved smt cached

#174 L1148:23:1148:27 trivial tlapm

#175 L1148:29:1148:33 trivial tlapm

▶ <4>2 Sub-case B2: LastTerm(log[w]) = c[2] CASE LastTerm(log[w]) = c[2] 117/117 tlapm

▶ <5>1 Establish lengths and domains first Len(log[leader]) >= Len(log[w]) BY <3>15 2/2 smt

#208 L1152:49:1152:51 proved smt cached

#209 L1152:52:1152:57 trivial tlapm

▶ <5>2 c[1] <= Len(log[w]) BY <3>8 DEF TypeOK 2/2 smt

#210 L1153:37:1153:39 proved smt cached

#211 L1153:40:1153:44 trivial tlapm

▶ <5>2a c[1] \in Nat /\ Len(log[w]) \in Nat /\ Len(log[leader]) \in Nat BY <3>8, <3>9 DEF TypeOK, Terms 3/3 tlapm

#212 L1154:82:1154:84 proved smt cached

#213 L1154:85:1154:89 trivial tlapm

#214 L1154:91:1154:95 trivial tlapm

▶ <5>3 c[1] <= Len(log[leader]) BY <5>1, <5>2, <5>2a 4/4 tlapm

#215 L1155:42:1155:44 proved smt cached

#216 L1155:45:1155:49 trivial tlapm

#217 L1155:51:1155:55 trivial tlapm

#218 L1155:57:1155:62 trivial tlapm

▶ <5>0b Len(log[leader]) > 0 BY <5>3, <3>c1pos 3/3 tlapm

#219 L1156:39:1156:41 proved smt cached

#220 L1156:42:1156:46 trivial tlapm

#221 L1156:48:1156:56 trivial tlapm

▶ <5>0a ~Empty(log[leader]) BY <5>0b DEF Empty 2/2 smt

#222 L1157:38:1157:40 proved smt cached

#223 L1157:41:1157:46 trivial tlapm

▶ <5>0c Len(log[leader]) \in DOMAIN log[leader] BY <5>0b DEF TypeOK 2/2 smt

#224 L1158:58:1158:60 proved smt cached

#225 L1158:61:1158:66 trivial tlapm

▶ <5>0 LastTerm(log[leader]) = c[2] LastTerm(log[leader]) = c[2] BY <3>15, <4>2 3/3 tlapm

#226 L1160:46:1160:48 proved smt cached

#227 L1160:49:1160:54 trivial tlapm

#228 L1160:56:1160:60 trivial tlapm

▶ <5>0d log[leader][Len(log[leader])] = c[2] BY <5>0, <5>0a DEF LastTerm, Empty 3/3 tlapm

#229 L1161:55:1161:57 proved smt cached

#230 L1161:58:1161:62 trivial tlapm

#231 L1161:64:1161:69 trivial tlapm

▶ <5>4 c[1] \in DOMAIN log[leader] BY <5>3, <3>c1pos DEF TypeOK 3/3 tlapm

#232 L1162:45:1162:47 proved smt cached

#233 L1162:48:1162:52 trivial tlapm

#234 L1162:54:1162:62 trivial tlapm

▶ <5>5 By H_TermsMonotonic on log[leader]: log[leader][c[1]] <= c[2] log[leader][c[1]] <= c[2] 6/6 tlapm

#235 L1165:13:1165:15 proved smt cached

#236 L1165:16:1165:20 trivial tlapm

#237 L1165:22:1165:27 trivial tlapm

#238 L1165:29:1165:34 trivial tlapm

#239 L1165:36:1165:40 trivial tlapm

#240 L1165:42:1165:47 trivial tlapm

▶ <5>8 Find first occurrence of c[2] in log[w] using SmallestNatural \E mw \in Nat : (mw \in DOMAIN log[w] /\ log[w][mw] = c[2]) /\ (\A k \in 0..(mw-1) : ~(k \in DOMAIN log[w] /\ log[w][k] = c[2])) 10/10 tlapm

▶ <5>9 PICK mw \in Nat : (mw \in DOMAIN log[w] /\ log[w][mw] = c[2]) /\ (\A k \in 0..(mw-1) : ~(k \in DOMAIN log[w] /\ log[w][k] = c[2])) BY <5>8 2/2 smt

#251 L1176:148:1176:150 proved smt cached

#252 L1176:151:1176:155 trivial tlapm

▶ <5>10 mw \in DOMAIN log[w] /\ log[w][mw] = c[2] BY <5>9 2/2 smt

#253 L1177:60:1177:62 proved smt cached

#254 L1177:63:1177:67 trivial tlapm

▶ <5>11 All earlier indices in log[w] don't have c[2] \A j \in DOMAIN log[w] : j < mw => log[w][j] # c[2] 2/2 smt

#255 L1180:13:1180:15 proved smt cached

#256 L1180:16:1180:20 trivial tlapm

▶ <5>12 By H_UniformLogEntries(w, leader, mw): no c[2] before mw in log[leader] ~\E k \in DOMAIN log[leader] : log[leader][k] = c[2] /\ k < mw 4/4 tlapm

#257 L1183:13:1183:15 proved smt cached

#258 L1183:16:1183:21 trivial tlapm

#259 L1183:23:1183:28 trivial tlapm

#260 L1183:30:1183:34 trivial tlapm

▶ <5>15 Find first occurrence of c[2] in log[leader] using SmallestNatural \E ml \in Nat : (ml \in DOMAIN log[leader] /\ log[leader][ml] = c[2]) /\ (\A k \in 0..(ml-1) : ~(k \in DOMAIN log[leader] /\ log[leader][k] = c[2])) 11/11 tlapm

▶ <5>16 PICK ml \in Nat : (ml \in DOMAIN log[leader] /\ log[leader][ml] = c[2]) /\ (\A k \in 0..(ml-1) : ~(k \in DOMAIN log[leader] /\ log[leader][k] = c[2]))... 2/2 smt

#272 L1193:169:1193:171 proved smt cached

#273 L1193:172:1193:177 trivial tlapm

▶ <5>17 ml \in DOMAIN log[leader] /\ log[leader][ml] = c[2] BY <5>16 2/2 smt

#274 L1194:70:1194:72 proved smt cached

#275 L1194:73:1194:78 trivial tlapm

▶ <5>18 All earlier indices in log[leader] don't have c[2] \A j \in DOMAIN log[leader] : j < ml => log[leader][j] # c[2] 2/2 smt

#276 L1197:13:1197:15 proved smt cached

#277 L1197:16:1197:21 trivial tlapm

▶ <5>19 By H_UniformLogEntries(leader, w, ml): no c[2] before ml in log[w] ~\E k \in DOMAIN log[w] : log[w][k] = c[2] /\ k < ml 4/4 tlapm

#278 L1200:13:1200:15 proved smt cached

#279 L1200:16:1200:21 trivial tlapm

#280 L1200:23:1200:28 trivial tlapm

#281 L1200:30:1200:34 trivial tlapm

▶ <5>20 ml >= mw (from <5>12, since log[leader][ml] = c[2] and ml ∈ DOMAIN log[leader]) ml >= mw BY <5>12, <5>17 3/3 tlapm

#282 L1202:27:1202:29 proved smt cached

#283 L1202:30:1202:35 trivial tlapm

#284 L1202:37:1202:42 trivial tlapm

▶ <5>21 mw >= ml (from <5>19, since log[w][mw] = c[2] and mw ∈ DOMAIN log[w]) mw >= ml BY <5>19, <5>10 3/3 tlapm

#285 L1204:27:1204:29 proved smt cached

#286 L1204:30:1204:35 trivial tlapm

#287 L1204:37:1204:42 trivial tlapm

▶ <5>22 ml = mw ml = mw BY <5>20, <5>21 3/3 tlapm

#288 L1206:26:1206:28 proved smt cached

#289 L1206:29:1206:34 trivial tlapm

#290 L1206:36:1206:41 trivial tlapm

▶ <5>23 c[1] >= mw (from <5>9: Pw(c[1]) and all k < mw don't have Pw) c[1] >= mw BY <5>9, <3>8, <3>c1pos 4/4 tlapm

#291 L1208:29:1208:31 proved smt cached

#292 L1208:32:1208:36 trivial tlapm

#293 L1208:38:1208:42 trivial tlapm

#294 L1208:44:1208:52 trivial tlapm

▶ <5>24 mw = ml ∈ DOMAIN log[leader] mw \in DOMAIN log[leader] BY <5>22, <5>17 3/3 tlapm

#295 L1210:44:1210:46 proved smt cached

#296 L1210:47:1210:52 trivial tlapm

#297 L1210:54:1210:59 trivial tlapm

▶ <5>25 By H_TermsMonotonic: log[leader][mw] <= log[leader][c[1]] log[leader][mw] <= log[leader][c[1]] 5/5 tlapm

#298 L1213:13:1213:15 proved smt cached

#299 L1213:16:1213:21 trivial tlapm

#300 L1213:23:1213:27 trivial tlapm

#301 L1213:29:1213:34 trivial tlapm

#302 L1213:36:1213:41 trivial tlapm

▶ <5>26 log[leader][mw] = c[2] log[leader][mw] = c[2] BY <5>22, <5>17 3/3 tlapm

#303 L1215:41:1215:43 proved smt cached

#304 L1215:44:1215:49 trivial tlapm

#305 L1215:51:1215:56 trivial tlapm

▶ <5>27 Therefore log[leader][c[1]] >= c[2] log[leader][c[1]] >= c[2] BY <5>25, <5>26 3/3 tlapm

#306 L1217:44:1217:46 proved smt cached

#307 L1217:47:1217:52 trivial tlapm

#308 L1217:54:1217:59 trivial tlapm

▶ <5>28 Combined with <= c[2]: log[leader][c[1]] = c[2] log[leader][c[1]] = c[2] 7/7 tlapm

▶ <5>29 log'[leader] = log[leader] BY <2>1 2/2 smt

#316 L1222:45:1222:47 proved smt cached

#317 L1222:48:1222:52 trivial tlapm

▶ <5>30 c[1] \in DOMAIN log'[leader] /\ log'[leader][c[1]] = c[2] BY <5>4, <5>28, <5>29 4/4 tlapm

#318 L1223:76:1223:78 proved smt cached

#319 L1223:79:1223:83 trivial tlapm

#320 L1223:85:1223:90 trivial tlapm

#321 L1223:92:1223:97 trivial tlapm

▶ <5>. QED BY <5>30, <2>7 DEF InLog 3/3 tlapm

#205 L1224:20:1224:22 proved smt cached

#206 L1224:23:1224:28 trivial tlapm

#207 L1224:30:1224:34 trivial tlapm

▶ <4>3 Sub-case B3: LastTerm(log[w]) < c[2] - impossible since c[2] <= LastTerm(log[w]) CASE LastTerm(log[w]) < c[2] 3/3 tlapm

#322 L1227:11:1227:13 proved smt cached

#323 L1227:14:1227:18 trivial tlapm

#324 L1227:20:1227:25 trivial tlapm

▶ <4>. QED BY <4>1, <4>2, <4>3, <3>13, <3>9 DEF TypeOK, Terms, LastTerm, Empty 6/6 tlapm

#167 L1228:18:1228:20 proved smt cached

#168 L1228:21:1228:25 trivial tlapm

#169 L1228:27:1228:31 trivial tlapm

#170 L1228:33:1228:37 trivial tlapm

#171 L1228:39:1228:44 trivial tlapm

#172 L1228:46:1228:50 trivial tlapm

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

#84 L1229:16:1229:18 proved smt cached

#85 L1229:19:1229:24 trivial tlapm

#86 L1229:26:1229:31 trivial tlapm

#87 L1229:33:1229:38 trivial tlapm

▶ <2>. QED BY <2>6, <2>7 3/3 tlapm

#29 L1230:14:1230:16 proved smt cached

#30 L1230:17:1230:21 trivial tlapm

#31 L1230:23:1230:27 trivial tlapm

▶ <1>5 (H_LeaderCompleteness,CommitEntryAction) TypeOK /\ H_TermsMonotonic /\ H_QuorumsSafeAtTerms /\ H_LeaderCompleteness /\ CommitEntryAction => H_LeaderCompleteness' 60/60 tlapm

▶ <2>. SUFFICES ASSUME TypeOK, H_TermsMonotonic, H_QuorumsSafeAtTerms, H_LeaderCompleteness, 1/1 smt

#329 L1235:38:1235:40 proved smt cached

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

#330 L1236:49:1236:51 proved smt cached

▶ <2>2 immediatelyCommitted' = immediatelyCommitted \cup {<<Len(log[p]), currentTerm[p]>>} BY DEF CommitEntry 1/1 smt

#331 L1237:95:1237:97 proved smt cached

▶ <2>qi Quorum intersection lemma \A Q1, Q2 \in Quorums(Server) : Q1 \cap Q2 # {} 24/24 tlapm

▶ <3>1 IsFiniteSet(Server) BY A0 2/2 smt

#337 L1240:33:1240:35 proved smt cached

#338 L1240:36:1240:38 trivial tlapm

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

#339 L1241:106:1241:113 proved smt cached

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

#340 L1242:56:1242:58 proved smt cached

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

#341 L1243:48:1243:50 proved smt cached

#342 L1243:51:1243:55 trivial tlapm

#343 L1243:57:1243:61 trivial tlapm

#344 L1243:63:1243:72 trivial tlapm

▶ <3>5 Cardinality(Q1) * 2 > Cardinality(Server) /\ Cardinality(Q2) * 2 > Cardinality(Server) BY DEF Quorums 1/1 smt

#345 L1244:100:1244:102 proved smt cached

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

#346 L1245:41:1245:43 proved smt cached

#347 L1245:44:1245:48 trivial tlapm

#348 L1245:50:1245:68 trivial tlapm

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

#349 L1246:64:1246:66 proved smt cached

#350 L1246:67:1246:71 trivial tlapm

#351 L1246:73:1246:91 trivial tlapm

▶ <3>8 Cardinality(Q1) + Cardinality(Q2) > Cardinality(Server) BY <3>5, <3>6, <3>7 4/4 tlapm

#352 L1247:69:1247:71 proved smt cached

#353 L1247:72:1247:76 trivial tlapm

#354 L1247:78:1247:82 trivial tlapm

#355 L1247:84:1247:88 trivial tlapm

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

#332 L1248:16:1248:18 proved smt cached

#333 L1248:19:1248:23 trivial tlapm

#334 L1248:25:1248:29 trivial tlapm

#335 L1248:31:1248:35 trivial tlapm

#336 L1248:37:1248:59 trivial tlapm

▶ <2>3 The commit quorum all have term = currentTerm[p] ImmediatelyCommitted(<<Len(log[p]), currentTerm[p]>>, commitQ) BY DEF CommitEntry 1/1 smt

#356 L1250:74:1250:76 proved smt cached

▶ <2>4 \A n \in commitQ : currentTerm[n] = currentTerm[p] BY <2>3 DEF ImmediatelyCommitted 2/2 smt

#357 L1251:62:1251:64 proved smt cached

#358 L1251:65:1251:69 trivial tlapm

▶ <2>5 For any primary s with currentTerm[s] > currentTerm[p], contradiction via quorum intersection \A s \in Server : state[s] = Primary /\ currentTerm[s] > currentTerm[p] => FALSE 16/16 tlapm

▶ <3>. SUFFICES ASSUME NEW s \in Server, state[s] = Primary, currentTerm[s] > currentTerm[p] PROVE FALSE OBVIOUS 1/1 smt

#362 L1254:110:1254:117 proved smt cached

▶ <3>1 PICK Qs \in Quorums(Server) : \A n \in Qs : currentTerm[n] >= currentTerm[s] 1/1 smt

#363 L1256:9:1256:11 proved smt cached

▶ <3>2 commitQ \cap Qs # {} BY <2>qi 2/2 smt

#364 L1257:34:1257:36 proved smt cached

#365 L1257:37:1257:42 trivial tlapm

▶ <3>3 PICK w \in commitQ \cap Qs : TRUE BY <3>2 2/2 smt

#366 L1258:47:1258:49 proved smt cached

#367 L1258:50:1258:54 trivial tlapm

▶ <3>4 currentTerm[w] = currentTerm[p] /\ currentTerm[w] >= currentTerm[s] BY <2>4, <3>1, <3>3 4/4 tlapm

#368 L1259:81:1259:83 proved smt cached

#369 L1259:84:1259:88 trivial tlapm

#370 L1259:90:1259:94 trivial tlapm

#371 L1259:96:1259:100 trivial tlapm

▶ <3>5 w \in Server BY <3>3, A4 DEF Quorums 3/3 tlapm

#372 L1260:26:1260:28 proved smt cached

#373 L1260:29:1260:33 trivial tlapm

#374 L1260:35:1260:37 trivial tlapm

▶ <3>. QED BY <3>4, <3>5 DEF TypeOK, Terms 3/3 tlapm

#359 L1261:16:1261:18 proved smt cached

#360 L1261:19:1261:23 trivial tlapm

#361 L1261:25:1261:29 trivial tlapm

▶ <2>. Main proof: for all primaries s, all committed entries in post-state with smaller terms are in log SUFFICES ASSUME NEW s \in Server, state'[s] = Primary, 1/1 smt

#375 L1265:41:1265:43 proved smt cached

▶ <2>6 state[s] = Primary /\ currentTerm'[s] = currentTerm[s] /\ log'[s] = log[s] BY <2>1 2/2 smt

#376 L1266:86:1266:88 proved smt cached

#377 L1266:89:1266:93 trivial tlapm

▶ <2>7 CASE c \in immediatelyCommitted 3/3 tlapm

#378 L1268:7:1268:9 proved smt cached

#379 L1268:10:1268:14 trivial tlapm

#380 L1268:16:1268:20 trivial tlapm

▶ <2>8 CASE c = <<Len(log[p]), currentTerm[p]>> 4/4 tlapm

#381 L1271:7:1271:9 proved smt cached

#382 L1271:10:1271:14 trivial tlapm

#383 L1271:16:1271:20 trivial tlapm

#384 L1271:22:1271:26 trivial tlapm

▶ <2>. QED BY <2>2, <2>7, <2>8 4/4 tlapm

#325 L1272:14:1272:16 proved smt cached

#326 L1272:17:1272:21 trivial tlapm

#327 L1272:23:1272:27 trivial tlapm

#328 L1272:29:1272:33 trivial tlapm

▶ <1>6 (H_LeaderCompleteness,UpdateTermsAction) TypeOK /\ H_LeaderCompleteness /\ UpdateTermsAction => H_LeaderCompleteness' 34/34 tlapm

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

#388 L1277:38:1277:40 proved smt cached

▶ <2>1 UNCHANGED <<log, immediatelyCommitted>> BY DEF UpdateTerms 1/1 smt

#389 L1278:51:1278:53 proved smt cached

▶ <2>2 state' = [state EXCEPT ![j] = Secondary] BY DEF UpdateTerms, UpdateTermsExpr 1/1 smt

#390 L1279:52:1279:54 proved smt cached

▶ <2>3 currentTerm' = [currentTerm EXCEPT ![j] = currentTerm[i]] BY DEF UpdateTerms, UpdateTermsExpr 1/1 smt

#391 L1280:69:1280:71 proved smt cached

▶ <2>4 \A s \in Server : state'[s] = Primary => s # j 8/8 smt

▶ <3>. SUFFICES ASSUME NEW s \in Server, state'[s] = Primary PROVE s # j OBVIOUS 1/1 smt

#395 L1282:78:1282:85 proved smt cached

▶ <3>1 j \in Server OBVIOUS 1/1 smt

#396 L1283:26:1283:33 proved smt 1.2s (12%)

▶ <3>2 state'[j] = Secondary BY <3>1, <2>2 DEF TypeOK 3/3 tlapm

#397 L1284:35:1284:37 proved smt 1.1s (11%)

#398 L1284:38:1284:42 trivial tlapm

#399 L1284:44:1284:48 trivial tlapm

▶ <3>. QED BY <3>2, A7 3/3 tlapm

#392 L1285:16:1285:18 proved smt cached

#393 L1285:19:1285:23 trivial tlapm

#394 L1285:25:1285:27 trivial tlapm

▶ <2>5 \A s \in Server : s # j => currentTerm'[s] = currentTerm[s] /\ log'[s] = log[s] BY <2>3, <2>1 3/3 tlapm

#400 L1286:91:1286:93 proved smt cached

#401 L1286:94:1286:98 trivial tlapm

#402 L1286:100:1286:104 trivial tlapm

▶ <2>. SUFFICES ASSUME NEW s \in Server, state'[s] = Primary, 1/1 smt

#403 L1289:41:1289:43 proved smt cached

▶ <2>6 s # j BY <2>4 2/2 smt

#404 L1290:17:1290:19 proved smt cached

#405 L1290:20:1290:24 trivial tlapm

▶ <2>7 log'[s] = log[s] /\ currentTerm'[s] = currentTerm[s] BY <2>6, <2>5 3/3 tlapm

#406 L1291:64:1291:66 proved smt cached

#407 L1291:67:1291:71 trivial tlapm

#408 L1291:73:1291:77 trivial tlapm

▶ <2>8 state[s] = Primary BY <2>6, <2>2, A7 4/4 tlapm

#409 L1292:30:1292:32 proved smt cached

#410 L1292:33:1292:37 trivial tlapm

#411 L1292:39:1292:43 trivial tlapm

#412 L1292:45:1292:47 trivial tlapm

▶ <2>9 c \in immediatelyCommitted BY <2>1 2/2 smt

#413 L1293:38:1293:40 proved smt cached

#414 L1293:41:1293:45 trivial tlapm

▶ <2>10 InLog(<<c[1],c[2]>>, s) BY <2>7, <2>8, <2>9 DEF H_LeaderCompleteness 4/4 tlapm

#415 L1294:36:1294:38 proved smt cached

#416 L1294:39:1294:43 trivial tlapm

#417 L1294:45:1294:49 trivial tlapm

#418 L1294:51:1294:55 trivial tlapm

▶ <2>. QED BY <2>10, <2>7 DEF InLog 3/3 tlapm

#385 L1295:14:1295:16 proved smt cached

#386 L1295:17:1295:22 trivial tlapm

#387 L1295:24:1295:28 trivial tlapm

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

#1 L1296:11:1296:13 proved smt cached

#2 L1296:14:1296:18 trivial tlapm

#3 L1296:19:1296:23 trivial tlapm

#4 L1296:24:1296:28 trivial tlapm

#5 L1296:29:1296:33 trivial tlapm

#6 L1296:34:1296:38 trivial tlapm

#7 L1296:39:1296:43 trivial tlapm

THEOREM L_9 (H_LeaderCompleteness)

Proof Notes

Proof Tree