---

Step * of Lemma rsc4-retry-property

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff,flrs:]. [es:EO'].
  ((StandardAssumptions(rsc4_Main) es)
   (e:E. c:Cmd. n,r:.
        (<<n, r + 1>, c>  rsc4_retry'base(Cmd)(e)
         (x:Id
              cs:Cmd List
               L:Id List
                ((no_repeats(Id;L)  (||L|| = ((coeff * flrs) + 1))  (||cs|| = ||L||))
                 (i:||L||
                     ((e':E. <x, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r>, cs[i]>, L[i]>)>  rsc4_Main(e'))
                      L[i]  locs))
                 (c = (snd(poss-maj(cmdeq;cs;hd(cs))))))))))
BY
{ (Unfold `vatype` 0
   THEN (Auto THEN AllHyps h.DVaType h )
   THEN (UseMessageConstraint (-1) THENA MaAuto)
   THEN (RWO "rsc4-retry" (-1) THENA MaAuto)
   THEN SquashExRepD
   THEN D (-1)
   THEN SquashExRepD
   THEN RenameTypedVars 
     [Cmd List, `cs'; Cmd, `cmd';Id List, `L'; Id,`loc']
   THEN AllHyps h.(FoldAbstracting [1;2] `rsc4_QuorumState` h
                   THEN FLemma `rsc4_quorum_invariant` [h]
                   THEN Auto
                   THEN Reduce (-1)
                   THEN MaAuto) 
   THEN AllHyps h.(RepUR ``rsc4_newvote`` h THEN (RW assert_pushdownC h THENA Auto)) 
   THEN SplitAndHyps
   THEN (InstLemma `mul_bounds_1a` [coeff;flrs] THENA Auto)
   THEN (D 0 THEN InstConcl [loc(e');[cmd / cs];[loc / L]])
   THEN Reduce 0
   THEN SplitAndConcl
   THEN Try (Complete (Auto))
   THEN MaAuto
   THEN skip{(SqExRepD THEN RWW "rsc4-vote" (-1) THEN Auto THEN (Reduce 0 THEN MaAuto))}) }

1
1. Cmd : Type
2. Cmd  ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : 
8. flrs : 
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c2 : Cmd
13. n : 
14. r : 
15. <<n, r + 1>, c2>  rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' } 
21. a : 
22. a2 : 
23. b2 :  List
24. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a)  (a  b2)
26. c1 : Cmd
27. True
28. <a, c1>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, c1>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
29. b1 : 
30. (r + 1) = (b1 + 1)
31. cmd : Cmd
32. loc : Id
33. <<<n, b1>, cmd>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
37. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
38. L : Id List
39. <cs, L>  rsc4_QuorumState(Cmd) <a, 0>(e')
40. a = n
41. 0 = b1
42. (loc  L)
43. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
44. no_repeats(Id;L)
45. ||L|| = ||cs||
46. i:||L||. (e:E. (e loc e'   <<<a, 0>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
47. 0  (coeff * flrs)
48. i : ||L|| + 1
 e'@0:E
    <loc(e'), make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r>, [cmd / cs][i]>, [loc / L][i]>)>  rsc4_Main(e'@0)

2
1. Cmd : Type
2. Cmd  ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : 
8. flrs : 
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c2 : Cmd
13. n : 
14. r : 
15. <<n, r + 1>, c2>  rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' } 
21. a : 
22. a2 : 
23. b2 :  List
24. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a)  (a  b2)
26. c1 : Cmd
27. True
28. <a, c1>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, c1>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
29. b1 : 
30. (r + 1) = (b1 + 1)
31. cmd : Cmd
32. loc : Id
33. <<<n, b1>, cmd>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
37. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
38. L : Id List
39. <cs, L>  rsc4_QuorumState(Cmd) <a, 0>(e')
40. a = n
41. 0 = b1
42. (loc  L)
43. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
44. no_repeats(Id;L)
45. ||L|| = ||cs||
46. i:||L||. (e:E. (e loc e'   <<<a, 0>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
47. 0  (coeff * flrs)
48. i : ||L|| + 1
49. e'@0:E
      <loc(e'), make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r>, [cmd / cs][i]>, [loc / L][i]>)>  rsc4_Main(e'@0)
 [loc / L][i]  locs

3
1. Cmd : Type
2. Cmd  ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : 
8. flrs : 
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c2 : Cmd
13. n : 
14. r : 
15. <<n, r + 1>, c2>  rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' } 
21. a : 
22. a2 : 
23. b2 :  List
24. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a)  (a  b2)
26. c1 : Cmd
27. True
28. <a, c1>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, c1>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
29. b1 : 
30. (r + 1) = (b1 + 1)
31. cmd : Cmd
32. loc : Id
33. <<<n, b1>, cmd>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
37. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
38. L : Id List
39. <cs, L>  rsc4_QuorumState(Cmd) <a, 0>(e')
40. a = n
41. 0 = b1
42. (loc  L)
43. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
44. no_repeats(Id;L)
45. ||L|| = ||cs||
46. i:||L||. (e:E. (e loc e'   <<<a, 0>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
47. 0  (coeff * flrs)
48. L1 : Id List
49. no_repeats(Id;L1)
50. ||L1|| = ((coeff * flrs) + 1)
51. (||cs|| + 1) = ||L1||
52. i : ||L1||
53. e'@0 : E
 i < ||[cmd / cs]||

4
1. Cmd : Type
2. Cmd  ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : 
8. flrs : 
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c3 : Cmd
13. n : 
14. r : 
15. <<n, r + 1>, c3>  rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' } 
21. a : 
22. a2 : 
23. b2 :  List
24. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a)  (a  b2)
26. c2 : Cmd
27. True
28. <a, c2>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, c2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
29. e2 : {e1:E| e1 loc e' } 
30. b3 : 
31. b6 : 
32. b6  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
33. b6 < b3
34. c1 : Cmd
35. True
36. <<a, b3>, c1>  Base(``rsc4 retry``;    Cmd)(e2)
 (b5@0:Id. <<<a, b3>, c1>, b5@0>  Base(``rsc4 vote``;    Cmd  Id)(e2))
37. b1 : 
38. (r + 1) = (b1 + 1)
39. cmd : Cmd
40. loc : Id
41. <<<n, b1>, cmd>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e')
42. cs : Cmd List
43. ||cs|| = (coeff * flrs)
44. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
45. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
46. L : Id List
47. <cs, L>  rsc4_QuorumState(Cmd) <a, b3>(e')
48. a = n
49. b3 = b1
50. (loc  L)
51. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
52. (no rsc4_Notify(Cmd;clients) a between e1 and e')
53. no_repeats(Id;L)
54. ||L|| = ||cs||
55. i:||L||. (e:E. (e loc e'   <<<a, b3>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
56. 0  (coeff * flrs)
57. i : ||L|| + 1
 e'@0:E
    <loc(e'), make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r>, [cmd / cs][i]>, [loc / L][i]>)>  rsc4_Main(e'@0)

5
1. Cmd : Type
2. Cmd  ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : 
8. flrs : 
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c3 : Cmd
13. n : 
14. r : 
15. <<n, r + 1>, c3>  rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' } 
21. a : 
22. a2 : 
23. b2 :  List
24. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a)  (a  b2)
26. c2 : Cmd
27. True
28. <a, c2>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, c2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
29. e2 : {e1:E| e1 loc e' } 
30. b3 : 
31. b6 : 
32. b6  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
33. b6 < b3
34. c1 : Cmd
35. True
36. <<a, b3>, c1>  Base(``rsc4 retry``;    Cmd)(e2)
 (b5@0:Id. <<<a, b3>, c1>, b5@0>  Base(``rsc4 vote``;    Cmd  Id)(e2))
37. b1 : 
38. (r + 1) = (b1 + 1)
39. cmd : Cmd
40. loc : Id
41. <<<n, b1>, cmd>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e')
42. cs : Cmd List
43. ||cs|| = (coeff * flrs)
44. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
45. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
46. L : Id List
47. <cs, L>  rsc4_QuorumState(Cmd) <a, b3>(e')
48. a = n
49. b3 = b1
50. (loc  L)
51. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
52. (no rsc4_Notify(Cmd;clients) a between e1 and e')
53. no_repeats(Id;L)
54. ||L|| = ||cs||
55. i:||L||. (e:E. (e loc e'   <<<a, b3>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
56. 0  (coeff * flrs)
57. i : ||L|| + 1
58. e'@0:E
      <loc(e'), make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r>, [cmd / cs][i]>, [loc / L][i]>)>  rsc4_Main(e'@0)
 [loc / L][i]  locs

6
1. Cmd : Type
2. Cmd  ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : 
8. flrs : 
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c3 : Cmd
13. n : 
14. r : 
15. <<n, r + 1>, c3>  rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e')  locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' } 
21. a : 
22. a2 : 
23. b2 :  List
24. <a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a)  (a  b2)
26. c2 : Cmd
27. True
28. <a, c2>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, c2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
29. e2 : {e1:E| e1 loc e' } 
30. b3 : 
31. b6 : 
32. b6  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
33. b6 < b3
34. c1 : Cmd
35. True
36. <<a, b3>, c1>  Base(``rsc4 retry``;    Cmd)(e2)
 (b5@0:Id. <<<a, b3>, c1>, b5@0>  Base(``rsc4 vote``;    Cmd  Id)(e2))
37. b1 : 
38. (r + 1) = (b1 + 1)
39. cmd : Cmd
40. loc : Id
41. <<<n, b1>, cmd>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e')
42. cs : Cmd List
43. ||cs|| = (coeff * flrs)
44. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
45. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
46. L : Id List
47. <cs, L>  rsc4_QuorumState(Cmd) <a, b3>(e')
48. a = n
49. b3 = b1
50. (loc  L)
51. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
52. (no rsc4_Notify(Cmd;clients) a between e1 and e')
53. no_repeats(Id;L)
54. ||L|| = ||cs||
55. i:||L||. (e:E. (e loc e'   <<<a, b3>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
56. 0  (coeff * flrs)
57. L1 : Id List
58. no_repeats(Id;L1)
59. ||L1|| = ((coeff * flrs) + 1)
60. (||cs|| + 1) = ||L1||
61. i : ||L1||
62. e'@0 : E
 i < ||[cmd / cs]||

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[locs,clients:bag(Id)].  \mforall{}[coeff,flrs:\mBbbN{}].  \mforall{}[es:EO'].
    ((StandardAssumptions(rsc4\_Main)  es)
    {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}c:Cmd.  \mforall{}n,r:\mBbbZ{}.
                (<<n,  r  +  1>,  c>  \mmember{}  rsc4\_retry'base(Cmd)(e)
                {}\mRightarrow{}  (\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
                                                  <x,  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  r>,  cs[i]>,  L[i]>)>  \mmember{}
                                                    rsc4\_Main(e'))
                                          \mwedge{}  L[i]  \mdownarrow{}\mmember{}  locs))
                                \mwedge{}  (c  =  (snd(poss-maj(cmdeq;cs;hd(cs))))))))))


By

---

(Unfold  `vatype`  0
  THEN  (Auto  THEN  AllHyps  h.DVaType  h  )
  THEN  (UseMessageConstraint  (-1)  THENA  MaAuto)
  THEN  (RWO  "rsc4-retry"  (-1)  THENA  MaAuto)
  THEN  SquashExRepD
  THEN  D  (-1)
  THEN  SquashExRepD
  THEN  RenameTypedVars 
      [\mkleeneopen{}Cmd  List\mkleeneclose{},  `cs';  \mkleeneopen{}Cmd\mkleeneclose{},  `cmd';\mkleeneopen{}Id  List\mkleeneclose{},  `L';  \mkleeneopen{}Id\mkleeneclose{},`loc']\mcdot{}
  THEN  AllHyps  h.(FoldAbstracting  [1;2]  `rsc4\_QuorumState`  h
                                  THEN  FLemma  `rsc4\_quorum\_invariant`  [h]
                                  THEN  Auto
                                  THEN  Reduce  (-1)
                                  THEN  MaAuto) 
  THEN  AllHyps  h.(RepUR  ``rsc4\_newvote``  h  THEN  (RW  assert\_pushdownC  h  THENA  Auto)) 
  THEN  SplitAndHyps
  THEN  (InstLemma  `mul\_bounds\_1a`  [\mkleeneopen{}coeff\mkleeneclose{};\mkleeneopen{}flrs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  0  THEN  InstConcl  [loc(e');\mkleeneopen{}[cmd  /  cs]\mkleeneclose{};\mkleeneopen{}[loc  /  L]\mkleeneclose{}]\mcdot{})
  THEN  Reduce  0
  THEN  SplitAndConcl
  THEN  Try  (Complete  (Auto))
  THEN  MaAuto
  THEN  skip\{(SqExRepD  THEN  RWW  "rsc4-vote"  (-1)  THEN  Auto  THEN  (Reduce  0  THEN  MaAuto))\}\mcdot{})



Home Index