Nuprl Definition : Paxos-spec8-body

Paxos-spec8-body{i:l}(es; Info; T; f; acceptors; leader; Input; Decide; 1a; 1b; 2a; 2b; failset) ==
  ((||acceptors|| = ((2 * f) + 1))
   no_repeats(Id;acceptors)
   (||filter(a.deq-member(IdDeq;a;failset);acceptors)||  f))
   (e1,e2:E(1b).  (((fst(1b(e1))) = (fst(1b(e2))))  ((fst(snd(1b(e1)))) = (fst(snd(1b(e2)))))  (e1 = e2)))
   (e1,e2:E(2b).  ((2b(e1) = 2b(e2))  (loc(e1) = loc(e2))  (e1 = e2)))
   (r:E(1a). p:E(2a).  ((r = p)))
   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 NoProposal = tr.let b,b',v = tr in 
                          if b z b' then {b} 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. eVote(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. eAcceptOrReject(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'. eProposal(p) mcast to each of acceptors a
                                     2a(p') such that
                                     p' = <loc(e), p>
                                    unless loc(e)  failset
      (Decide
       = (snd(fst(p)) where p from Proposal;Collect(f + 1 vt's from 2b with maximum fst(snd(vt))
                                                    such that snd(snd(vt))) such that (fst(fst(p)) = snd(p))))
      (NewBallot:EClass()
         (e,b,r. eNewBallot(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))))
          (e':E(NewBallot)
              (((e:E(NoProposal). (e' loc e   (NoProposal(e) = NewBallot(e'))))
               (e:E(2b). (e' loc e   ((snd(2b(e))) = <NewBallot(e'), ff>)  x<e.x  Decide)))
               (n:E(NewBallot). (e' loc n   (NewBallot(e') < NewBallot(n))))))
          (e:E(Input). ((n:E(Input). ((n <loc e)))  (n:E(NewBallot). e loc n )))
          (nb1,nb2:E(NewBallot).
              ((nb1 <loc nb2)
               ((NewBallot(nb1) < NewBallot(nb2))
                  ((e:E(NoProposal). ((nb1 loc e   e loc nb2 )  (NoProposal(e) = NewBallot(nb1))))
                    (e:E(2b)
                       ((nb1 loc e   e loc nb2 )  ((snd(2b(e))) = <NewBallot(nb1), ff>)  x<e.x  Decide))))))))


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,  es-interface-pair-prior: X;Y,  es-collect-filter: Collect(size v's from X with maximum num[v] such that P[v]),  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),  mapfilter-class: (f[v] where v from X such that P[v]),  es-E-interface: E(X),  es-filter-image: f[X],  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  alle-lt: e<e'.P[e],  es-le: e loc e' ,  es-locl: (e <loc e'),  es-loc: loc(e),  es-E: E,  id-deq: IdDeq,  Id: Id,  length: ||as||,  imax: imax(a;b),  eq_int: (i = j),  le_int: i z j,  lt_int: i <z j,  assert: b,  ifthenelse: if b then t else f fi ,  bfalse: ff,  bool: ,  nat: ,  let: let,  it: ,  spreadn: spread3,  pi1: fst(t),  pi2: snd(t),  le: A  B,  all: x:A. B[x],  exists: x:A. B[x],  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  unit: Unit,  less_than: a < b,  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,  multiply: n * m,  add: n + m,  minus: -n,  natural_number: $n,  int: ,  equal: s = t,  no_repeats: no_repeats(T;l),  filter: filter(P;l),  deq-member: deq-member(eq;x;L),  single-bag: {x},  empty-bag: {}
Definitions :  pi2: snd(t),  imax: imax(a;b),  lambda: x.A[x],  es-interface-accum: es-interface-accum(f;x;X),  let: let,  empty-bag: {},  single-bag: {x},  le_int: i z j,  ifthenelse: if b then t else f fi ,  spreadn: spread3,  es-filter-image: f[X],  pair: <a, b>,  lt_int: i <z j,  pi1: fst(t),  natural_number: $n,  add: n + m,  es-collect-opt-max: es-collect-opt-max,  es-E: E,  equal: s = t,  not: A,  es-E-interface: E(X),  all: x:A. B[x],  and: P  Q,  es-loc: loc(e),  Id: Id,  implies: P  Q,  eclass-val: X(e),  bool: ,  nat: ,  product: x:A  B[x],  id-deq: IdDeq,  deq-member: deq-member(eq;x;L),  filter: filter(P;l),  length: ||as||,  le: A  B,  no_repeats: no_repeats(T;l),  multiply: n * m,  int: ,  map-class: (f[v] where v from X),  spread: spread def,  es-prior-class-when: (X'?d) when Y,  minus: -n,  es-tagged-true-class: Tagged_tt(X),  accum-class: accum-class(a,x.f[a; x];x.base[x];X),  inl: inl x ,  inr: inr x ,  it: ,  es-class-reply-or-fail: es-class-reply-or-fail,  union: left + right,  unit: Unit,  es-class-mcast-fail: es-class-mcast-fail,  eclass: EClass(A[eo; e]),  mapfilter-class: (f[v] where v from X such that P[v]),  eq_int: (i = j),  es-interface-pair-prior: X;Y,  es-collect-filter: Collect(size v's from X with maximum num[v] such that P[v]),  exists: x:A. B[x],  apply: f a,  or: P  Q,  es-le: e loc e' ,  bfalse: ff,  alle-lt: e<e'.P[e],  assert: b,  in-eclass: e  X,  less_than: a < b,  es-locl: (e <loc e')
Paxos-spec8-body\{i:l\}(es;  Info;  T;  f;  acceptors;  leader;  Input;  Decide;  1a;  1b;  2a;  2b;  failset)  ==
    ((||acceptors||  =  ((2  *  f)  +  1))
    \mwedge{}  no\_repeats(Id;acceptors)
    \mwedge{}  (||filter(\mlambda{}a.deq-member(IdDeq;a;failset);acceptors)||  \mleq{}  f))
    \mwedge{}  (\mforall{}e1,e2:E(1b).
              (((fst(1b(e1)))  =  (fst(1b(e2))))  {}\mRightarrow{}  ((fst(snd(1b(e1))))  =  (fst(snd(1b(e2)))))  {}\mRightarrow{}  (e1  =  e2)))
    \mwedge{}  (\mforall{}e1,e2:E(2b).    ((2b(e1)  =  2b(e2))  {}\mRightarrow{}  (loc(e1)  =  loc(e2))  {}\mRightarrow{}  (e1  =  e2)))
    \mwedge{}  (\mforall{}r:E(1a).  \mforall{}p:E(2a).    (\mneg{}(r  =  p)))
    \mwedge{}  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  NoProposal  =  \mlambda{}tr.let  b,b',v  =  tr  in 
                                                    if  b  \mleq{}z  b'  then  \{b\}  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{}  (Decide
              =  (snd(fst(p))  where  p  from  Proposal;
                                                                      Collect(f  +  1  vt's  from  2b  with  maximum  fst(snd(vt))
                                                                                      such  that  snd(snd(vt)))  such  that  (fst(fst(p))  =\msubz{}  ...)))
          \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))))
                  \mwedge{}  (\mforall{}e':E(NewBallot)
                            (((\mexists{}e:E(NoProposal).  (e'  \mleq{}loc  e    \mwedge{}  (NoProposal(e)  =  NewBallot(e'))))
                            \mvee{}  (\mexists{}e:E(2b)
                                    (e'  \mleq{}loc  e    \mwedge{}  ((snd(2b(e)))  =  <NewBallot(e'),  ff>)  \mwedge{}  \mforall{}x<e.\mneg{}\muparrow{}x  \mmember{}\msubb{}  Decide)))
                            {}\mRightarrow{}  (\mexists{}n:E(NewBallot).  (e'  \mleq{}loc  n    \mwedge{}  (NewBallot(e')  <  NewBallot(n))))))
                  \mwedge{}  (\mforall{}e:E(Input).  ((\mforall{}n:E(Input).  (\mneg{}(n  <loc  e)))  {}\mRightarrow{}  (\mexists{}n:E(NewBallot).  e  \mleq{}loc  n  )))
                  \mwedge{}  (\mforall{}nb1,nb2:E(NewBallot).
                            ((nb1  <loc  nb2)
                            {}\mRightarrow{}  ((NewBallot(nb1)  <  NewBallot(nb2))
                                  \mwedge{}  ((\mexists{}e:E(NoProposal)
                                            ((nb1  \mleq{}loc  e    \mwedge{}  e  \mleq{}loc  nb2  )  \mwedge{}  (NoProposal(e)  =  NewBallot(nb1))))
                                      \mvee{}  (\mexists{}e:E(2b)
                                              ((nb1  \mleq{}loc  e    \mwedge{}  e  \mleq{}loc  nb2  )
                                              \mwedge{}  ((snd(2b(e)))  =  <NewBallot(nb1),  ff>)
                                              \mwedge{}  \mforall{}x<e.\mneg{}\muparrow{}x  \mmember{}\msubb{}  Decide))))))))


Date html generated: 2011_10_20-PM-04_45_59
Last ObjectModification: 2011_01_22-PM-10_53_49

Home Index