Proof of Nuprl Lemma : rsc4-validity-property

Step * 3 2 1 1 of Lemma rsc4-validity-property

1. Cmd : {T:Type| valueall-type(T)}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs :

7. es : EO'
8. StandardAssumptions(rsc4_Main) es
9. e : E
10.

e1:E
((e1 < e)

((

v:

Cmd. (v

rsc4_decided'base(Cmd)(e1)

(

e':E. ((e' < e1)

v

rsc4_propose'base(Cmd)(e')))))

(

v:

Cmd

Id
(v

rsc4_vote'base(Cmd)(e1)

(

e':E. ((e' < e1)

<fst(fst(fst(v))), snd(fst(v))>

rsc4_propose'base(Cmd)(e')))))

(

v:

Cmd
(v

rsc4_retry'base(Cmd)(e1)

(

e':E. ((e' < e1)

<fst(fst(v)), snd(v)>

rsc4_propose'base(Cmd)(e')))))

(

e2:E
(e2 c

e1

(

cs:Cmd List.

L:Id List.

n,rnd:

.

c:Cmd.
(<cs, L>

rsc4_QuorumState(Cmd) <n, rnd>(e1)

(c

cs)

(

e':E. ((e' < e1)

<n, c>

rsc4_propose'base(Cmd)(e')))))))))
11. n1 :

12. n :

13. c3 : Cmd
14. <<n1, n>, c3>

rsc4_retry'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. c2 : Cmd
26. True
27. <a, c2>

Base([propose];

Cmd)(e1)

(

b1:

.

b3:Id. <<<a, b1>, c2>, b3>

Base(``rsc4 vote``;

Cmd

Id)(e1))
28. e2 : {e1:E| e1

loc e' }
29. b3 :

30. b6 :

31. b6

Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
32. b6 < b3
33. c1 : Cmd
34. True
35. <<a, b3>, c1>

Base(``rsc4 retry``;

Cmd)(e2)

(

b5@0:Id. <<<a, b3>, c1>, b5@0>

Base(``rsc4 vote``;

Cmd

Id)(e2))
36. b1 :

37. n = (b1 + 1)
38. cmd : Cmd
39. loc : Id
40. <<<n1, b1>, cmd>, loc>

Base(``rsc4 vote``;

Cmd

Id)(e')
41. cs : Cmd List
42. ||cs|| = (coeff * flrs)
43.

((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
44. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
45. L : Id List
46. <cs, L>

rsc4_QuorumState(Cmd) <a, b3>(e')
47. a = n1
48. b3 = b1
49.

(loc

L)
50. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
51. (no rsc4_Notify(Cmd;clients) a between e1 and e')
52. c3 = cmd
53.

v:

Cmd. (v

rsc4_decided'base(Cmd)(e')

(

e'@0:E. ((e'@0 < e')

v

rsc4_propose'base(Cmd)(e'@0))))
54.

v:

Cmd

Id
(v

rsc4_vote'base(Cmd)(e')

(

e'@0:E. ((e'@0 < e')

<fst(fst(fst(v))), snd(fst(v))>

rsc4_propose'base(Cmd)(e'@0))))
55.

v:

Cmd
(v

rsc4_retry'base(Cmd)(e')

(

e'@0:E. ((e'@0 < e')

<fst(fst(v)), snd(v)>

rsc4_propose'base(Cmd)(e'@0))))
56.

e2:E
(e2 c

e'

(

cs:Cmd List.

L:Id List.

n,rnd:

.

c:Cmd.
(<cs, L>

rsc4_QuorumState(Cmd) <n, rnd>(e')

(c

cs)

(

e'@0:E. ((e'@0 < e')

<n, c>

rsc4_propose'base(Cmd)(e'@0))))))

e':E. ((e' < e)

<n1, c3>

rsc4_propose'base(Cmd)(e'))
BY
{ (RepUR ``rsc4_vote'base`` -3
THEN OnMaybeHyp 40 (\h. ((FHyp (-3) [h] THENA Auto) THEN Reduce (-1) THEN RepeatFor 3 (ParallelLast) THEN MaAuto))
)

}

1. Cmd : \{T:Type| valueall-type(T)\} 2. cmdeq : EqDecider(Cmd) 3. locs : bag(Id) 4. clients : bag(Id) 5. coeff : \{2...\} 6. flrs : \mBbbN{} 7. es : EO' 8. StandardAssumptions(rsc4\_Main) es 9. e : E 10. \mforall{}e1:E ((e1 < e) {}\mRightarrow{} ((\mforall{}v:\mBbbZ{} \mtimes{} Cmd (v \mmember{} rsc4\_decided'base(Cmd)(e1) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} v \mmember{} rsc4\_propose'base(Cmd)(e'))))) \mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id (v \mmember{} rsc4\_vote'base(Cmd)(e1) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E ((e' < e1) \mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} rsc4\_propose'base(Cmd)(e'))))) \mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd (v \mmember{} rsc4\_retry'base(Cmd)(e1) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} <fst(fst(v)), snd(v)> \mmember{} rsc4\_propose'base(Cmd)(e'))))) \mwedge{} (\mforall{}e2:E (e2 c\mleq{} e1 {}\mRightarrow{} (\mforall{}cs:Cmd List. \mforall{}L:Id List. \mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd. (<cs, L> \mmember{} rsc4\_QuorumState(Cmd) <n, rnd>(e1) {}\mRightarrow{} (c \mmember{} cs) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} <n, c> \mmember{} rsc4\_propose'base(Cmd)(e'))))))))) 11. n1 : \mBbbZ{} 12. n : \mBbbZ{} 13. c3 : Cmd 14. <<n1, n>, c3> \mmember{} rsc4\_retry'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. c2 : Cmd 26. True 27. <a, c2> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e1) \mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, c2>, 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. b6 : \mBbbZ{} 31. b6 \mmember{} Memory-class(rsc4\_update\_round(Cmd) a;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e2) 32. b6 < b3 33. c1 : Cmd 34. True 35. <<a, b3>, c1> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e2) \mvee{} (\mexists{}b5@0:Id. <<<a, b3>, c1>, b5@0> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e2)) 36. b1 : \mBbbZ{} 37. n = (b1 + 1) 38. cmd : Cmd 39. loc : Id 40. <<<n1, b1>, cmd>, loc> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e') 41. cs : Cmd List 42. ||cs|| = (coeff * flrs) 43. \mneg{}((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1)) 44. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd))) 45. L : Id List 46. <cs, L> \mmember{} rsc4\_QuorumState(Cmd) <a, b3>(e') 47. a = n1 48. b3 = b1 49. \mneg{}(loc \mmember{} L) 50. (no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e') 51. (no rsc4\_Notify(Cmd;clients) a between e1 and e') 52. c3 = cmd 53. \mforall{}v:\mBbbZ{} \mtimes{} Cmd (v \mmember{} rsc4\_decided'base(Cmd)(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} v \mmember{} rsc4\_propose'base(Cmd)(e'@0)))) 54. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id (v \mmember{} rsc4\_vote'base(Cmd)(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} rsc4\_propose'base(Cmd)(e'@0)))) 55. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd (v \mmember{} rsc4\_retry'base(Cmd)(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} <fst(fst(v)), snd(v)> \mmember{} rsc4\_propose'base(Cmd)(e'@0)))) 56. \mforall{}e2:E (e2 c\mleq{} e' {}\mRightarrow{} (\mforall{}cs:Cmd List. \mforall{}L:Id List. \mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd. (<cs, L> \mmember{} rsc4\_QuorumState(Cmd) <n, rnd>(e') {}\mRightarrow{} (c \mmember{} cs) {}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} <n, c> \mmember{} rsc4\_propose'base(Cmd)(e'@0)))))) \mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <n1, c3> \mmember{} rsc4\_propose'base(Cmd)(e')) By (RepUR ``rsc4\_vote'base`` -3 THEN OnMaybeHyp 40 (\mbackslash{}h. ((FHyp (-3) [h] THENA Auto) THEN Reduce (-1) THEN RepeatFor 3 (ParallelLast) THEN MaAuto)) )\mcdot{} Home Index