Step * 4 2 of Lemma rsc4-decided-property


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. c : Cmd
13. n : 
14. <n, c rsc4_decided'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e')  locs
18. loc(e) = loc(e')
19. e1 : {e1:E| e1 loc e' } 
20. a : 
21. a2 : 
22. b2 :  List
23. <a2, b2 Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
24. (a2 < a)  (a  b2)
25. b : Cmd
26. True
27. <a, b Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, b>, b3 Base(``rsc4 vote``;    Cmd  Id)(e1))
28. e2 : {e1:E| e1 loc e' } 
29. b3 : 
30. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3between e2 and e')
31. b5 : 
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc Base(``rsc4 vote``;    Cmd  Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L Memory-class(rsc4_add_to_quorum(Cmd) <a, b3>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
41. a = n
42. b3 = b5
43. (lastloc  L)
44. b1 : Cmd
45. True
46. <<a, b3>, b1 Base(``rsc4 retry``;    Cmd)(e2)
 (b5:Id. <<<a, b3>, b1>, b5 Base(``rsc4 vote``;    Cmd  Id)(e2))
47. b4 : 
48. b4  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
49. b4 < b3
50. (no rsc4_Notify(Cmd;clients) a between e1 and e')
51. (z[c1 / cs].z = c)
52. ||cs|| = ||L||
53. no_repeats(Id;L)
 (vtr[lastloc / L].(e'@0:E
                         <loc(e'), make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, b3>, c>, vtr>) rsc4_Main(e'@0))
        vtr  locs)
BY
{ ((Assert <cs, L rsc4_QuorumState(Cmd) <a, b3>(e') THENA (RepUR ``rsc4_QuorumState`` 0 THEN Trivial))
   THEN (FLemma `rsc4_quorum_invariant` [-1] THENA MaAuto)
   THEN Reduce (-1)
   THEN Auto) }

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. c : Cmd
13. n : 
14. <n, c rsc4_decided'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e')  locs
18. loc(e) = loc(e')
19. e1 : {e1:E| e1 loc e' } 
20. a : 
21. a2 : 
22. b2 :  List
23. <a2, b2 Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
24. (a2 < a)  (a  b2)
25. b : Cmd
26. True
27. <a, b Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, b>, b3 Base(``rsc4 vote``;    Cmd  Id)(e1))
28. e2 : {e1:E| e1 loc e' } 
29. b3 : 
30. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3between e2 and e')
31. b5 : 
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc Base(``rsc4 vote``;    Cmd  Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L Memory-class(rsc4_add_to_quorum(Cmd) <a, b3>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
41. a = n
42. b3 = b5
43. (lastloc  L)
44. b1 : Cmd
45. True
46. <<a, b3>, b1 Base(``rsc4 retry``;    Cmd)(e2)
 (b5:Id. <<<a, b3>, b1>, b5 Base(``rsc4 vote``;    Cmd  Id)(e2))
47. b4 : 
48. b4  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
49. b4 < b3
50. (no rsc4_Notify(Cmd;clients) a between e1 and e')
51. (z[c1 / cs].z = c)
52. ||cs|| = ||L||
53. no_repeats(Id;L)
54. <cs, L rsc4_QuorumState(Cmd) <a, b3>(e')
55. no_repeats(Id;L)
56. ||L|| = ||cs||
57. i:||L||. (e:E. (e loc e'   <<<a, b3>, cs[i]>, L[i] rsc4_vote'base(Cmd)(e)))
 (vtr[lastloc / L].(e'@0:E
                         <loc(e'), make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, b3>, c>, vtr>) rsc4_Main(e'@0))
        vtr  locs)




1.  Cmd  :  Type
2.  Cmd  \mmember{}  ValueAllType
3.  valueall-type(Cmd)
4.  cmdeq  :  EqDecider(Cmd)
5.  locs  :  bag(Id)
6.  clients  :  bag(Id)
7.  coeff  :  \mBbbZ{}
8.  flrs  :  \mBbbZ{}
9.  es  :  EO'
10.  StandardAssumptions(rsc4\_Main)  es
11.  e  :  E
12.  c  :  Cmd
13.  n  :  \mBbbZ{}
14.  <n,  c>  \mmember{}  rsc4\_decided'base(Cmd)(e)
15.  e'  :  E
16.  (e'  <  e)
17.  loc(e')  \mdownarrow{}\mmember{}  locs
18.  loc(e)  =  loc(e')
19.  e1  :  \{e1:E|  e1  \mleq{}loc  e'  \} 
20.  a  :  \mBbbZ{}
21.  a2  :  \mBbbZ{}
22.  b2  :  \mBbbZ{}  List
23.  <a2,  b2>  \mmember{}  Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init()  ɘ,  []>rsc4\_Proposal(Cmd))(e1)
24.  (a2  <  a)  \mvee{}  (a  \mmember{}  b2)
25.  b  :  Cmd
26.  True
27.  <a,  b>  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  Cmd)(e1)
\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3:Id.  <<<a,  b1>,  b>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e1))
28.  e2  :  \{e1:E|  e1  \mleq{}loc  e'  \} 
29.  b3  :  \mBbbZ{}
30.  (no  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  b3>  between  e2  and  e')
31.  b5  :  \mBbbZ{}
32.  c1  :  Cmd
33.  lastloc  :  Id
34.  <<<n,  b5>,  c1>,  lastloc>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e')
35.  cs  :  Cmd  List
36.  ||cs||  =  (coeff  *  flrs)
37.  (fst(poss-maj(cmdeq;[c1  /  cs];c1)))  =  ((coeff  *  flrs)  +  1)
38.  c  =  (snd(poss-maj(cmdeq;[c1  /  cs];c1)))
39.  L  :  Id  List
40.  <cs,  L>  \mmember{}  Memory-class(rsc4\_add\_to\_quorum(Cmd)  <a,  b3>rsc4\_init() 
                                                                                                                      <[],  []>rsc4\_vote'base(Cmd))(e')
41.  a  =  n
42.  b3  =  b5
43.  \mneg{}(lastloc  \mmember{}  L)
44.  b1  :  Cmd
45.  True
46.  <<a,  b3>,  b1>  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e2)
\mvee{}  (\mexists{}b5:Id.  <<<a,  b3>,  b1>,  b5>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e2))
47.  b4  :  \mBbbZ{}
48.  b4  \mmember{}  Memory-class(rsc4\_update\_round(Cmd)  a;rsc4\_init()  0;rsc4\_RoundInfo(Cmd))(e2)
49.  b4  <  b3
50.  (no  rsc4\_Notify(Cmd;clients)  a  between  e1  and  e')
51.  (\mforall{}z\mmember{}[c1  /  cs].z  =  c)
52.  ||cs||  =  ||L||
53.  no\_repeats(Id;L)
\mvdash{}  (\mforall{}vtr\mmember{}[lastloc  /  L].(\mdownarrow{}\mexists{}e'@0:E
                                                  <loc(e'),  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  b3>,  c>,  vtr>)>  \mmember{}
                                                    rsc4\_Main(e'@0))
              \mwedge{}  vtr  \mdownarrow{}\mmember{}  locs)


By


((Assert  \mkleeneopen{}<cs,  L>  \mmember{}  rsc4\_QuorumState(Cmd)  <a,  b3>(e')\mkleeneclose{}\mcdot{}
    THENA  (RepUR  ``rsc4\_QuorumState``  0  THEN  Trivial)
    )
  THEN  (FLemma  `rsc4\_quorum\_invariant`  [-1]  THENA  MaAuto)
  THEN  Reduce  (-1)
  THEN  Auto)



Home Index