Nuprl Definition : Paxos-partial-spec8

Paxos-partial-spec8{i:l}(Info; es; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset) ==
  let Collect = Collect(f + 1 vs's from 1b
                         with maximum num= fst(snd(vs))
                         return <num,n,outl(vs).2> for which
                         n=outl(snd(snd(vs))).1 is maximum
                         or <num,-1,prior Input> if all isr(snd(snd(vs))))) in
   let Proposal =

tr.let b,b',v = tr in
if b' <z b then {<b, v>} else {} fi [Collect] in
let MaxReserve = es-interface-accum(

mx,x.imax(mx;snd(x));0;1a) in
   let AcceptOrReject = (let lbv,m = lbvm
                         in let l,b,v = lbv in
                            <lbv, m

z b> where lbvm from (MaxReserve'?-1) when 2a) in
let Accept =

tr.{snd(tr)}[Tagged_tt(AcceptOrReject)] in
let MaxAccept = accum-class(bv1,bv2.if fst(bv1) <z fst(bv2) then bv2 else bv1 fi ; bv.bv; Accept) in
let Vote = ((inl bv where bv from MaxAccept)'?inr

) when 1a in

e,v,vs. e

Vote(v)

c

reply 1b(vs)@fst(fst(v)) such that
(snd(vs)) = <snd(fst(v)), snd(v)>

fst(vs)=loc(e)
unless loc(e)

failset

e,x,v. e

AcceptOrReject(x)

c

reply 2b(v)@fst(fst(x)) such that
(snd(v)) = <fst(snd(fst(x))), snd(x)>

fst(v)=loc(e)
unless loc(e)

failset

e,p,p'. e

Proposal(p) mcast to each of acceptors a
                                   2a(p') such that
                                   p' = <loc(e), p>
                                  unless loc(e)

failset

(

NewBallot:EClass(

)
(

e,b,r. e

NewBallot(b) mcast to each of acceptors a
                                      1a(r) such that
                                      r = <loc(e), b>
                                     unless loc(e)

failset

(

n:E(NewBallot). (loc(n) = (leader NewBallot(n))))))

Proof not projected

Definitions occuring in Statement : es-class-mcast-fail: es-class-mcast-fail, es-class-reply-or-fail: es-class-reply-or-fail, es-prior-class-when: (X'?d) when Y, es-collect-opt-max: es-collect-opt-max, accum-class: accum-class(a,x.f[a; x];x.base[x];X), es-interface-accum: es-interface-accum(f;x;X), es-tagged-true-class: Tagged_tt(X), map-class: (f[v] where v from X), es-E-interface: E(X), es-filter-image: f[X], eclass-val: X(e), eclass: EClass(A[eo; e]), es-loc: loc(e), Id: Id, imax: imax(a;b), le_int: i

z j, lt_int: i <z j, ifthenelse: if b then t else f fi , bool:

, nat:

, let: let, it:

, spreadn: spread3, pi1: fst(t), pi2: snd(t), all:

x:A. B[x], exists:

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

Q, unit: Unit, apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, product: x:A

B[x], inr: inr x , inl: inl x , union: left + right, add: n + m, minus: -n, natural_number: $n, equal: s = t, single-bag: {x}, empty-bag: {}
Definitions : nat:

, Id: Id, product: x:A

B[x], equal: s = t, es-class-mcast-fail: es-class-mcast-fail, and: P

Q, eclass: EClass(A[eo; e]), exists:

x:A. B[x], es-loc: loc(e), pair: <a, b>, pi1: fst(t), pi2: snd(t), bool:

, es-class-reply-or-fail: es-class-reply-or-fail, unit: Unit, union: left + right, it:

, inr: inr x , inl: inl x , map-class: (f[v] where v from X), es-prior-class-when: (X'?d) when Y, let: let, lt_int: i <z j, ifthenelse: if b then t else f fi , accum-class: accum-class(a,x.f[a; x];x.base[x];X), es-tagged-true-class: Tagged_tt(X), single-bag: {x}, lambda:

x.A[x], es-filter-image: f[X], natural_number: $n, minus: -n, le_int: i

z j, spreadn: spread3, spread: spread def, imax: imax(a;b), es-interface-accum: es-interface-accum(f;x;X), empty-bag: {}, add: n + m, es-collect-opt-max: es-collect-opt-max, all:

x:A. B[x], es-E-interface: E(X), apply: f a, eclass-val: X(e)

Paxos-partial-spec8\{i:l\}(Info; es; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset ) == let Collect = Collect(f + 1 vs's from 1b with maximum num= fst(snd(vs)) return <num,n,outl(vs).2> for which n=outl(snd(snd(vs))).1 is maximum or <num,-1,prior Input> if all isr(snd(snd(vs))))) in let Proposal = \mlambda{}tr.let b,b',v = tr in if b' <z b then \{<b, v>\} else \{\} fi [Collect] in let MaxReserve = es-interface-accum(\mlambda{}mx,x.imax(mx;snd(x));0;1a) in let AcceptOrReject = (let lbv,m = lbvm in let l,b,v = lbv in <lbv, m \mleq{}z b> where lbvm from (MaxReserve'?-1) when 2a) in let Accept = \mlambda{}tr.\{snd(tr)\}[Tagged\_tt(AcceptOrReject)] in let MaxAccept = accum-class(bv1,bv2.if fst(bv1) <z fst(bv2) then bv2 else bv1 fi ; bv.bv; Accept ) in let Vote = ((inl bv where bv from MaxAccept)'?inr \mcdot{} ) when 1a in \mforall{}e,v,vs. e\mmember{}Vote(v) \mLeftarrow{}c\mRightarrow{} \mexists{} reply 1b(vs)@fst(fst(v)) such that (snd(vs)) = <snd(fst(v)), snd(v)>\mwedge{}fst(vs)=loc(e) unless loc(e) \mmember{} failset \mwedge{} \mforall{}e,x,v. e\mmember{}AcceptOrReject(x) \mLeftarrow{}c\mRightarrow{} \mexists{} reply 2b(v)@fst(fst(x)) such that (snd(v)) = <fst(snd(fst(x))), snd(x)>\mwedge{}fst(v)=loc(e) unless loc(e) \mmember{} failset \mwedge{} \mforall{}e,p,p'. e\mmember{}Proposal(p) mcast to each of acceptors a 2a(p') such that p' = <loc(e), p> unless loc(e) \mmember{} failset \mwedge{} (\mexists{}NewBallot:EClass(\mBbbN{}) (\mforall{}e,b,r. e\mmember{}NewBallot(b) mcast to each of acceptors a 1a(r) such that r = <loc(e), b> unless loc(e) \mmember{} failset \mwedge{} (\mforall{}n:E(NewBallot). (loc(n) = (leader NewBallot(n)))))) Date html generated: 2011_10_20-PM-04_46_56 Last ObjectModification: 2011_01_22-PM-10_57_01 Home Index