Nuprl Lemma : rsc4-ilf

(

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:

Cmd

Id. {v

rsc4_vote'base(Cmd)(e)

v

Base(``rsc4 vote``;

Cmd

Id)(e)})

(

[a:

].

[clients:bag(Id)].

[Cmd:ValueAllType].

[es:EO'].

[e:E].

[i:Id].

[m:Message].
{<i, m>

rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|(e)

i

clients

(

b:Cmd. ((m = make-Msg([notify];

Cmd;<a, b>))

<a, b>

Base(``rsc4 decided``;

Cmd)(e)))})

(

[a:

].

[clients:bag(Id)].

[Cmd:ValueAllType].

[es:EO'].

[e:E].

[i:Id].

[m:Message].
{<i, m>

rsc4_Notify(Cmd;clients) a(e)

(no rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)| prior to e)

<i, m>

{rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|}(e)})

(

[b,a,flrs,coeff:

].

[Cmd:ValueAllType].

[cmdeq:EqDecider(Cmd)].

[es:EO'].

[e:E].

[i:Id].

[m:Message].
{<i, m>

rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b>(e)

(i = loc(e))

(

a1,b1:

b2:Cmd

b3:Id
((

a2:Cmd List
(((

b4:Id List
(<a2, b4>

Memory-class(rsc4_add_to_quorum(Cmd) <a, b>;rsc4_init()
<[], []>;rsc4_vote'base(Cmd))(e)

(

(rsc4_newvote(Cmd) <a, b> <<<a1, b1>, b2>, b3> <a2, b4>))))

(((m = make-Msg(``rsc4 decided``;

Cmd;<a1, snd(poss-maj(cmdeq;[b2 / a2];b2))>))

((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))

((m = make-Msg(``rsc4 retry``;

Cmd;<<a1, b1 + 1>, snd(poss-maj(cmdeq;[b2 / a2];b2))>))

(

((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))))))

(||a2|| = (coeff * flrs))))

<<<a1, b1>, b2>, b3>

Base(``rsc4 vote``;

Cmd

Id)(e)))})

(

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:

Cmd
{v

rsc4_RoundInfo(Cmd)(e)

v

Base(``rsc4 retry``;

Cmd)(e)

(

a,b:

b1:Cmd
((v = <<a, b>, b1>)

(

b2:Id. <<<a, b>, b1>, b2>

Base(``rsc4 vote``;

Cmd

Id)(e))))})

(

[Cmd:ValueAllType].

[es:EO'].

[e:E].

v:

Cmd
{v

rsc4_Proposal(Cmd)(e)

v

Base([propose];

Cmd)(e)

(

a,b:

b1:Cmd. ((v = <a, b1>)

(

b2:Id. <<<a, b>, b1>, b2>

Base(``rsc4 vote``;

Cmd

Id)(e))))})

(

[Cmd:ValueAllType].

[clients:bag(Id)].

[cmdeq:EqDecider(Cmd)].

[coeff,flrs:

].

[locs:bag(Id)].

[es:EO'].

[e:E].

[i:Id].

[m:Message].
{<i, m>

rsc4_Main(e)

loc(e)

locs

(

e':{e':E| e'

loc e }

a:

((

b:Cmd
((<a, b>

Base([propose];

Cmd)(e')

(

b1:

.

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

Base(``rsc4 vote``;

Cmd

Id)(e')))

(((((i

locs

(m = make-Msg(``rsc4 vote``;

Cmd

Id;<<<a, 0>, b>, loc(e)>)))

(e = e'))

((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)

<i, m>

{rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0>}(e)))

((no rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)| between e' and e)

<i, m>

{rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|}(e)))

((no rsc4_Notify(Cmd;clients) a between e' and e)

(

e1:{e1:E| e1

loc e }

b:

((

b1:Cmd
((((i

locs

(m = make-Msg(``rsc4 vote``;

Cmd

Id;<<<a, b>, b1>, loc(e)>)))

(e = e1))

((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e1 and e)

<i, m>

{rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b>}(e)))

(<<a, b>, b1>

Base(``rsc4 retry``;

Cmd)(e1)

(

b5:Id. <<..., ...>, ...>

...(...)))))

...))))))

...))})

Proof

Definitions occuring in Statement : rsc4_main: rsc4_Main, rsc4_update_replica: rsc4_update_replica(Cmd), rsc4_Proposal: rsc4_Proposal(Cmd), rsc4_Notify: rsc4_Notify(Cmd;clients), rsc4_decision: rsc4_decision(Cmd;clients), rsc4_update_round: rsc4_update_round(Cmd), rsc4_RoundInfo: rsc4_RoundInfo(Cmd), rsc4_Quorum: rsc4_Quorum(Cmd;cmdeq;coeff;flrs), rsc4_add_to_quorum: rsc4_add_to_quorum(Cmd), rsc4_newvote: rsc4_newvote(Cmd), rsc4_init: rsc4_init(), rsc4_decided'base: rsc4_decided'base(Cmd), rsc4_vote'base: rsc4_vote'base(Cmd), Memory-class: Memory-class(f;init;X), concat-lifting-loc-1: f@, make-Msg: make-Msg(hdr;typ;val), base-headers-msg-val: Base(hdr;typ), Message: Message, simple-loc-comb-1: F|Loc, X|, no-classrel-in-interval: (no X between start and e), no-prior-classrel: (no X prior to e), classrel: v

X(e), eo-forward: eo.e, event-ordering+: EO+(Info), es-le: e

loc e' , es-loc: loc(e), es-E: E, Id: Id, length: ||as||, assert:

b, sq_or: a

b, uall:

[x:A]. B[x], guard: {T}, pi1: fst(t), pi2: snd(t), all:

x:A. B[x], exists:

x:A. B[x], iff: P

Q, not:

A, squash:

T, or: P

Q, and: P

Q, less_than: a < b, set: {x:A| B[x]} , apply: f a, pair: <a, b>, product: x:A

B[x], cons: [car / cdr], nil: [], list: type List, multiply: n * m, add: n + m, natural_number: $n, int:

, token: "$token", equal: s = t, l_member: (x

l), poss-maj: poss-maj(eq;L;x), deq: EqDecider(T), bag-member: x

bs, bag: bag(T), vatype: ValueAllType
Definitions : hide: HIDDEN
Lemmas : rsc4-ilf-hide

(\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id \{v \mmember{} rsc4\_vote'base(Cmd)(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)\}) \mwedge{} (\mforall{}[a:\mBbbZ{}]. \mforall{}[clients:bag(Id)]. \mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message]. \{<i, m> \mmember{} rsc4\_decision(Cmd;clients) a@|Loc, rsc4\_decided'base(Cmd)|(e) \mLeftarrow{}{}\mRightarrow{} i \mdownarrow{}\mmember{} clients \mwedge{} (\mdownarrow{}\mexists{}b:Cmd ((m = make-Msg([notify];\mBbbZ{} \mtimes{} Cmd;<a, b>)) \mwedge{} <a, b> \mmember{} Base(``rsc4 decided``;\mBbbZ{} \mtimes{} Cmd)(e)))\}) \mwedge{} (\mforall{}[a:\mBbbZ{}]. \mforall{}[clients:bag(Id)]. \mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message]. \{<i, m> \mmember{} rsc4\_Notify(Cmd;clients) a(e) \mLeftarrow{}{}\mRightarrow{} (no rsc4\_decision(Cmd;clients) a@|Loc, rsc4\_decided'base(Cmd)| prior to e) \mwedge{} <i, m> \mmember{} \{rsc4\_decision(Cmd;clients) a@|Loc, rsc4\_decided'base(Cmd)|\}(e)\}) \mwedge{} (\mforall{}[b,a,flrs,coeff:\mBbbZ{}]. \mforall{}[Cmd:ValueAllType]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message]. \{<i, m> \mmember{} rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b>(e) \mLeftarrow{}{}\mRightarrow{} (i = loc(e)) \mwedge{} (\mdownarrow{}\mexists{}a1,b1:\mBbbZ{} \mexists{}b2:Cmd \mexists{}b3:Id ((\mexists{}a2:Cmd List (((\mexists{}b4:Id List (<a2, b4> \mmember{} Memory-class(rsc4\_add\_to\_quorum(Cmd) <a, b>rsc4\_init() <[], []>rsc4\_vote'base(Cmd))(e) \mwedge{} (\muparrow{}(rsc4\_newvote(Cmd) <a, b> <<<a1, b1>, b2>, b3> <a2, b4>)))) \mwedge{} (((m = make-Msg(``rsc4 decided``;\mBbbZ{} \mtimes{} Cmd;<a1, snd(poss-maj(cmdeq;[b2 / a2];b2))>)) \mwedge{} ((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))) \mvee{} ((m = make-Msg(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd;<<a1, b1 + 1> , snd(poss-maj(cmdeq;[b2 / a2];b2)) >)) \mwedge{} (\mneg{}((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))))) \mwedge{} (||a2|| = (coeff * flrs)))) \mwedge{} <<<a1, b1>, b2>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)))\}) \mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \{v \mmember{} rsc4\_RoundInfo(Cmd)(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e) \mdownarrow{}\mvee{} (\mexists{}a,b:\mBbbZ{} \mexists{}b1:Cmd ((v = <<a, b>, b1>) \mwedge{} (\mexists{}b2:Id. <<<a, b>, b1>, b2> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e))))\}) \mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} Cmd \{v \mmember{} rsc4\_Proposal(Cmd)(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e) \mdownarrow{}\mvee{} (\mexists{}a,b:\mBbbZ{} \mexists{}b1:Cmd ((v = <a, b1>) \mwedge{} (\mexists{}b2:Id. <<<a, b>, b1>, b2> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e))))\}) \mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[clients:bag(Id)]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[coeff,flrs:\mBbbZ{}]. \mforall{}[locs:bag(Id)]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message]. \{<i, m> \mmember{} rsc4\_Main(e) \mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} locs \mwedge{} (\mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \} \mexists{}a:\mBbbZ{} ((\mexists{}b:Cmd ((<a, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e') \mdownarrow{}\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, b>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e'))) \mwedge{} (((((i \mdownarrow{}\mmember{} locs \mwedge{} (m = make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<a, 0>, b>, loc(e)>))) \mwedge{} (e = e')) \mdownarrow{}\mvee{} ((no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e) \mwedge{} <i, m> \mmember{} \{rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0>\}(e))) \mvee{} ((no rsc4\_decision(Cmd;clients) a@|Loc, rsc4\_decided'base(Cmd)| between e' and e) \mwedge{} <i, m> \mmember{} \{rsc4\_decision(Cmd;clients) a@|Loc, rsc4\_decided'base(Cmd)|\}(e))) \mdownarrow{}\mvee{} ((no rsc4\_Notify(Cmd;clients) a between e' and e) \mwedge{} (\mdownarrow{}\mexists{}e1:\{e1:E| e1 \mleq{}loc e \} \mexists{}b:\mBbbZ{} ((\mexists{}b1:Cmd ((((i \mdownarrow{}\mmember{} locs \mwedge{} (m = make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<a, b>, b1> , loc(e) >))) \mwedge{} (e = e1)) \mdownarrow{}\mvee{} ((no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e1 and e) \mwedge{} <i, m> \mmember{} \{rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b>\}(e))) \mwedge{} (<<a, b>, b1> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e1) \mdownarrow{}\mvee{} (\mexists{}b5:Id. <<..., ...>, ...> \mmember{} ...(...))))) \mwedge{} ...)))))) \mwedge{} ...))\}) Date html generated: 2012_02_20-PM-04_56_23 Last ObjectModification: 2012_02_02-PM-02_16_13 Home Index