Step
*
2
of Lemma
new_23_sig_retry_property
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℕ
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. r : ℤ@i
17. <<n, r + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
18. (f propose) = (ℤ × Cmd) ∈ Type
19. (f notify) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
21. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
22. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
23. f ∈ Name ⟶ Type
24. e' : E
25. delay : ℤ
26. (e' < e)
27. loc(e') ↓∈ reps
28. e1 : {e1:E| e1 ≤loc e' }
29. z1 : ℤ
30. z2 : Cmd
31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
32. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. e2 : {e1:E| e1 ≤loc e' }
35. z6 : ℤ
36. z7 : Cmd
37. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
38. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
39. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
40. header(e') = ``new_23_sig vote`` ∈ Name
41. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
42. <z1, z6> = (fst(fst(msgval(e')))) ∈ (ℤ × ℤ)
43. ¬(snd(msgval(e')) ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
44. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
45. delay = 0 ∈ ℤ
46. ¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))]\000C;snd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)
47. loc(e) = loc(e') ∈ Id
48. msg-authentic(info(e)) = ff
49. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
50. (r + 1) = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ
51. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd
52. 0 ≤ (coeff * flrs)
⊢ ↓∃x:Id
∃cs:Cmd List+
∃L:Id List
((no_repeats(Id;L) ∧ (||L|| = ((coeff * flrs) + 1) ∈ ℤ) ∧ (||cs|| = ||L|| ∈ ℤ))
∧ (∀i:ℕ||L||. ((↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, r>, cs[i]>, L[i]>)) ∈ new_23_sig_mai\000Cn()(e')) ∧ L[i] ↓∈ reps))
∧ (c = (snd(poss-maj(eq;cs;hd(cs)))) ∈ Cmd))
BY
{ ((InstLemma `new_23_sig_quorum_invariant_fun` [⌜Cmd⌝;⌜notify⌝;⌜propose⌝;⌜f⌝;⌜es.e2⌝;⌜e'⌝;⌜<z1, z6>⌝]⋅ THENA Auto)
THEN (InstLemma `new_23_sig_quorum_inv_vote_fun` [⌜Cmd⌝;⌜notify⌝;⌜propose⌝;⌜f⌝;⌜es.e2⌝;⌜e'⌝;⌜<z1, z6>⌝]⋅ THENA Auto)
THEN RepD
THEN D 0
THEN InstConcl [⌜loc(e')⌝;⌜[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2\000C;e')))]⌝;⌜[snd(msgval(e')) /
(snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.\000Ce2;e')))]⌝]⋅
THEN RepeatFor 2 ((Reduce 0 THEN Auto))
THEN (RW ListC 0 THENA Auto)
THEN AutoSplit) }
1
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℕ
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. r : ℤ@i
17. <<n, r + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
18. (f propose) = (ℤ × Cmd) ∈ Type
19. (f notify) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
21. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
22. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
23. f ∈ Name ⟶ Type
24. e' : E
25. delay : ℤ
26. (e' < e)
27. loc(e') ↓∈ reps
28. e1 : {e1:E| e1 ≤loc e' }
29. z1 : ℤ
30. z2 : Cmd
31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
32. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. e2 : {e1:E| e1 ≤loc e' }
35. z6 : ℤ
36. z7 : Cmd
37. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
38. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
39. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
40. header(e') = ``new_23_sig vote`` ∈ Name
41. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
42. <z1, z6> = (fst(fst(msgval(e')))) ∈ (ℤ × ℤ)
43. ¬(snd(msgval(e')) ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
44. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
45. delay = 0 ∈ ℤ
46. ¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))]\000C;snd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)
47. loc(e) = loc(e') ∈ Id
48. msg-authentic(info(e)) = ff
49. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
50. (r + 1) = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ
51. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd
52. 0 ≤ (coeff * flrs)
53. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
54. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;not\000Cify;propose;f;<z1, z6>;es.e2;e'))|| ∈ ℤ
55. ∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))||
(↓∃e'@0:E
((e'@0 <loc e')
∧ <<<z1, z6>, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]>, snd(new_23_sig_Quorum\000CStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]> ∈
new_23_sig_vote'base(Cmd;notify;propose;f)(e'@0)))
56. no_repeats(Id;[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))])
57. (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = ((coeff * flrs) + 1) ∈ ℤ
58. (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = (||snd(new_23_sig_QuorumStateFun(\000CCmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) ∈ ℤ
59. i : ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1@i
60. msgval(e') ∈ ℤ × ℤ × Cmd × Id
61. i ≤ 0
⊢ ↓∃e'@0:E. mk-msg-interface(loc(e');make-Msg(``new_23_sig vote``;<<<n, r>, snd(fst(msgval(e')))>, snd(msgval(e'))>)) ∈ \000Cnew_23_sig_main()(e'@0)
2
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℕ
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. r : ℤ@i
17. <<n, r + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
18. (f propose) = (ℤ × Cmd) ∈ Type
19. (f notify) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
21. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
22. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
23. f ∈ Name ⟶ Type
24. e' : E
25. delay : ℤ
26. (e' < e)
27. loc(e') ↓∈ reps
28. e1 : {e1:E| e1 ≤loc e' }
29. z1 : ℤ
30. z2 : Cmd
31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
32. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. e2 : {e1:E| e1 ≤loc e' }
35. z6 : ℤ
36. z7 : Cmd
37. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
38. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
39. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
40. header(e') = ``new_23_sig vote`` ∈ Name
41. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
42. <z1, z6> = (fst(fst(msgval(e')))) ∈ (ℤ × ℤ)
43. ¬(snd(msgval(e')) ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
44. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
45. delay = 0 ∈ ℤ
46. ¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))]\000C;snd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)
47. loc(e) = loc(e') ∈ Id
48. msg-authentic(info(e)) = ff
49. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
50. (r + 1) = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ
51. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd
52. 0 ≤ (coeff * flrs)
53. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
54. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;not\000Cify;propose;f;<z1, z6>;es.e2;e'))|| ∈ ℤ
55. ∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))||
(↓∃e'@0:E
((e'@0 <loc e')
∧ <<<z1, z6>, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]>, snd(new_23_sig_Quorum\000CStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]> ∈
new_23_sig_vote'base(Cmd;notify;propose;f)(e'@0)))
56. no_repeats(Id;[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))])
57. (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = ((coeff * flrs) + 1) ∈ ℤ
58. (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = (||snd(new_23_sig_QuorumStateFun(\000CCmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) ∈ ℤ
59. i : ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1@i
60. ¬(i ≤ 0)
61. msgval(e') ∈ ℤ × ℤ × Cmd × Id
⊢ ↓∃e'@0:E
mk-msg-interface(loc(e');make-Msg(``new_23_sig vote``;<<<n, r>
, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>\000C;es.e2;e'))[i - 1]
>
, snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;\000Ces.e2;e'))[i - 1]
>)) ∈ new_23_sig_main()(e'@0)
3
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℕ
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. r : ℤ@i
17. <<n, r + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
18. (f propose) = (ℤ × Cmd) ∈ Type
19. (f notify) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
21. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
22. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
23. f ∈ Name ⟶ Type
24. e' : E
25. delay : ℤ
26. (e' < e)
27. loc(e') ↓∈ reps
28. e1 : {e1:E| e1 ≤loc e' }
29. z1 : ℤ
30. z2 : Cmd
31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
32. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. e2 : {e1:E| e1 ≤loc e' }
35. z6 : ℤ
36. z7 : Cmd
37. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
38. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
39. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
40. header(e') = ``new_23_sig vote`` ∈ Name
41. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
42. <z1, z6> = (fst(fst(msgval(e')))) ∈ (ℤ × ℤ)
43. ¬(snd(msgval(e')) ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
44. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
45. delay = 0 ∈ ℤ
46. ¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))]\000C;snd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)
47. loc(e) = loc(e') ∈ Id
48. msg-authentic(info(e)) = ff
49. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
50. (r + 1) = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ
51. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd
52. 0 ≤ (coeff * flrs)
53. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
54. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;not\000Cify;propose;f;<z1, z6>;es.e2;e'))|| ∈ ℤ
55. ∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))||
(↓∃e'@0:E
((e'@0 <loc e')
∧ <<<z1, z6>, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]>, snd(new_23_sig_Quorum\000CStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]> ∈
new_23_sig_vote'base(Cmd;notify;propose;f)(e'@0)))
56. no_repeats(Id;[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))])
57. (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = ((coeff * flrs) + 1) ∈ ℤ
58. (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = (||snd(new_23_sig_QuorumStateFun(\000CCmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) ∈ ℤ
59. i : ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1@i
60. ↓∃e'@0:E
mk-msg-interface(loc(e');make-Msg(``new_23_sig vote``;<<<n, r>
, [snd(fst(msgval(e'))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1
, z6
>;es\000C.e2;e')))][i]
>
, [snd(msgval(e')) /
(snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1
, z6
>;es.\000Ce2;e')))][i]
>)) ∈ new_23_sig_main()(e'@0)
61. msgval(e') ∈ ℤ × ℤ × Cmd × Id
62. i ≤ 0
⊢ snd(msgval(e')) ↓∈ reps
4
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℕ
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : ℤ@i
16. r : ℤ@i
17. <<n, r + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)@i
18. (f propose) = (ℤ × Cmd) ∈ Type
19. (f notify) = (ℤ × Cmd) ∈ Type
20. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
21. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
22. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
23. f ∈ Name ⟶ Type
24. e' : E
25. delay : ℤ
26. (e' < e)
27. loc(e') ↓∈ reps
28. e1 : {e1:E| e1 ≤loc e' }
29. z1 : ℤ
30. z2 : Cmd
31. ((header(e1) = propose ∈ Name) ∧ has-es-info-type(es;e1;f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e1) ∈ (ℤ × Cmd)))
∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e1))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e1)))) ∈ Cmd))
32. ¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. e2 : {e1:E| e1 ≤loc e' }
35. z6 : ℤ
36. z7 : Cmd
37. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
38. ((header(e2) = ``new_23_sig retry`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))
39. (no new_23_sig_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
40. header(e') = ``new_23_sig vote`` ∈ Name
41. has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
42. <z1, z6> = (fst(fst(msgval(e')))) ∈ (ℤ × ℤ)
43. ¬(snd(msgval(e')) ∈ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
44. ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = (coeff * flrs) ∈ ℤ
45. delay = 0 ∈ ℤ
46. ¬((fst(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))]\000C;snd(fst(msgval(e')))))) = ((coeff * flrs) + 1) ∈ ℤ)
47. loc(e) = loc(e') ∈ Id
48. msg-authentic(info(e)) = ff
49. n = (fst(fst(fst(msgval(e'))))) ∈ ℤ
50. (r + 1) = ((snd(fst(fst(msgval(e'))))) + 1) ∈ ℤ
51. c = (snd(poss-maj(eq;[snd(fst(msgval(e'))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))\000C)];snd(fst(msgval(e')))))) ∈ Cmd
52. 0 ≤ (coeff * flrs)
53. no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))
54. ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| = ||fst(new_23_sig_QuorumStateFun(Cmd;not\000Cify;propose;f;<z1, z6>;es.e2;e'))|| ∈ ℤ
55. ∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))||
(↓∃e'@0:E
((e'@0 <loc e')
∧ <<<z1, z6>, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]>, snd(new_23_sig_Quorum\000CStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i]> ∈
new_23_sig_vote'base(Cmd;notify;propose;f)(e'@0)))
56. no_repeats(Id;[snd(msgval(e')) / (snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e')))])
57. (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = ((coeff * flrs) + 1) ∈ ℤ
58. (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) = (||snd(new_23_sig_QuorumStateFun(\000CCmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1) ∈ ℤ
59. i : ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))|| + 1@i
60. ¬(i ≤ 0)
61. ↓∃e'@0:E
mk-msg-interface(loc(e');make-Msg(``new_23_sig vote``;<<<n, r>
, [snd(fst(msgval(e'))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1
, z6
>;es\000C.e2;e')))][i]
>
, [snd(msgval(e')) /
(snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1
, z6
>;es.\000Ce2;e')))][i]
>)) ∈ new_23_sig_main()(e'@0)
62. msgval(e') ∈ ℤ × ℤ × Cmd × Id
⊢ snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e2;e'))[i - 1] ↓∈ reps
Latex:
Latex:
1. Cmd : \{T:Type| valueall-type(T)\}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : \mBbbN{}
6. flrs : \mBbbN{}
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig\{i:l\}(\mBbbZ{})
10. f : new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. eo-msg-interface-constraint(es;new\_23\_sig\_main();new\_23\_sig\_headers\_internal();f)@i
13. e : E@i
14. c : Cmd@i
15. n : \mBbbZ{}@i
16. r : \mBbbZ{}@i
17. <<n, r + 1>, c> \mmember{} new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e)@i
18. (f propose) = (\mBbbZ{} \mtimes{} Cmd)
19. (f notify) = (\mBbbZ{} \mtimes{} Cmd)
20. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd)
21. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
22. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
23. f \mmember{} Name {}\mrightarrow{} Type
24. e' : E
25. delay : \mBbbZ{}
26. (e' < e)
27. loc(e') \mdownarrow{}\mmember{} reps
28. e1 : \{e1:E| e1 \mleq{}loc e' \}
29. z1 : \mBbbZ{}
30. z2 : Cmd
31. ((header(e1) = propose) \mwedge{} has-es-info-type(es;e1;f;\mBbbZ{} \mtimes{} Cmd) \mwedge{} (<z1, z2> = msgval(e1)))
\mvee{} ((header(e1) = ``new\_23\_sig vote``)
\mwedge{} has-es-info-type(es;e1;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mwedge{} (z1 = (fst(fst(fst(msgval(e1))))))
\mwedge{} (z2 = (snd(fst(msgval(e1))))))
32. \mneg{}\muparrow{}(set-sig-member(slots) z1 new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1))
33. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) z1 between e1 and e')
34. e2 : \{e1:E| e1 \mleq{}loc e' \}
35. z6 : \mBbbZ{}
36. z7 : Cmd
37. new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e1;e2) < z6
38. ((header(e2) = ``new\_23\_sig retry``)
\mwedge{} has-es-info-type(es;e2;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
\mwedge{} (<<z1, z6>, z7> = msgval(e2)))
\mvee{} ((header(e2) = ``new\_23\_sig vote``)
\mwedge{} has-es-info-type(es;e2;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mwedge{} (<<z1, z6>, z7> = (fst(msgval(e2)))))
39. (no new\_23\_sig\_Quorum(Cmd;eq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e2 and e')
40. header(e') = ``new\_23\_sig vote``
41. has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
42. <z1, z6> = (fst(fst(msgval(e'))))
43. \mneg{}(snd(msgval(e')) \mmember{} snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))
44. ||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))|| = (coeff * flrs)
45. delay = 0
46. \mneg{}((fst(poss-maj(eq;[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))];sn\000Cd(fst(msgval(e'))))))
= ((coeff * flrs) + 1))
47. loc(e) = loc(e')
48. msg-authentic(info(e)) = ff
49. n = (fst(fst(fst(msgval(e')))))
50. (r + 1) = ((snd(fst(fst(msgval(e'))))) + 1)
51. c
= (snd(poss-maj(eq;[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))];snd(fs\000Ct(msgval(e'))))))
52. 0 \mleq{} (coeff * flrs)
\mvdash{} \mdownarrow{}\mexists{}x:Id
\mexists{}cs:Cmd List\msupplus{}
\mexists{}L:Id List
((no\_repeats(Id;L) \mwedge{} (||L|| = ((coeff * flrs) + 1)) \mwedge{} (||cs|| = ||L||))
\mwedge{} (\mforall{}i:\mBbbN{}||L||
((\mdownarrow{}\mexists{}e':E. mk-msg-interface(x;make-Msg(``new\_23\_sig vote``;<<<n, r>, cs[i]>, L[i]>)) \mmember{} new\000C\_23\_sig\_main()(e')) \mwedge{} L[i] \mdownarrow{}\mmember{} reps))
\mwedge{} (c = (snd(poss-maj(eq;cs;hd(cs))))))
By
Latex:
((InstLemma `new\_23\_sig\_quorum\_invariant\_fun` [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es.e2\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}<z1, z6>\mkleeneclose{}]
\mcdot{}
THENA Auto
)
THEN (InstLemma `new\_23\_sig\_quorum\_inv\_vote\_fun` [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es.e2\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}<z1
, z6
>\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN RepD
THEN D 0
THEN InstConcl [\mkleeneopen{}loc(e')\mkleeneclose{};\mkleeneopen{}[snd(fst(msgval(e'))) /
(fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e'))\000C)]\mkleeneclose{};
\mkleeneopen{}[snd(msgval(e')) / (snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>es.e2;e')))]\mkleeneclose{}]\mcdot{}
THEN RepeatFor 2 ((Reduce 0 THEN Auto))
THEN (RW ListC 0 THENA Auto)
THEN AutoSplit)
Home
Index