Nuprl Definition : Paxos-spec7-body

Paxos-spec7-body{i:l}(Info;
                      es;
                      T;
                      f;
                      acceptors;
                      Reserve;
                      VoteState;
                      Proposal;
                      AcceptOrReject;
                      leader;
                      Decide;
                      Vote;
                      Input;
                      Collect;
                      NoProposal;
                      NewBallot;
                      failset) ==
  ((||acceptors|| = ((2 * f) + 1))
   no_repeats(Id;acceptors)
   (||filter(a.deq-member(IdDeq;a;failset);acceptors)||  f))
   (e:E(Vote). (loc(e) = (leader (snd(fst(Vote(e)))))))
   (e:E(VoteState). (loc(e) = (leader Reservation(VoteState(e)))))
   e,r,vs. eReserve(r) c  VoteState(vs) such that
                               (r = Reservation(vs))
                               (loc(e) = Name(vs))
                               MaxVote(es;T;Tagged_tt(AcceptOrReject);e;Info(vs))
                              unless loc(e)  failset
   e,x,v. eAcceptOrReject(x) c  Vote(v) such that
                                     v = <<loc(e), fst(fst(x))>, snd(x)>
                                    unless loc(e)  failset
   (e1,e2:E(VoteState).
       ((Name(VoteState(e1)) = Name(VoteState(e2)))
        (Reservation(VoteState(e1)) = Reservation(VoteState(e2)))
        (e1 = e2)))
   (e1,e2:E(Vote).  ((Vote(e1) = Vote(e2))  (loc(e1) = loc(e2))  (e1 = e2)))
   (Collect
    = (let inpt,b,mx,vs = q
       in <b
          , mx
          , if (Ballot(vs) = -1)
          then inpt
          else Value(vs)
          fi >   where q from Input;Collect(f + 1 vs's from VoteState  with maximum Reservation(vs) such that tt
                                             return <Reservation(vs),n,vs> with n = maximum Ballot(vs))))
   (Proposal = tr.let b,b',v = tr in if b' <z b then {<b, v>} else {} fi [Collect])
   (NoProposal = tr.let b,b',v = tr in if b z b' then {b} else {} fi [Collect])
   e,p,pb. eProposal(p) c at each of acceptors
                                AcceptOrReject(pb) such that
                                p = (fst(pb))
                               unless loc(e)  failset
   (e:E(AcceptOrReject)
       ((snd(AcceptOrReject(e)))  e':E(Reserve). (e' loc e   (Reserve(e')  (fst(fst(AcceptOrReject(e))))))))
   (Decide
    = (snd(fst(p)) where p from Proposal;Collect(f + 1 vt's from Vote with maximum snd(fst(vt))
                                                 such that snd(vt)) such that (fst(fst(p)) = snd(p))))
   e,b,r. eNewBallot(b) c at each of acceptors
                                Reserve(r) such that
                                r = 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(Vote). (e' loc e   ((snd(fst(Vote(e)))) = NewBallot(e'))  snd(Vote(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(Vote)
                ((nb1 loc e   e loc nb2 )
                 ((snd(fst(Vote(e)))) = NewBallot(nb1))
                 snd(Vote(e)) = ff
                 x<e.x  Decide))))))
   (r:E(Reserve). ar:E(AcceptOrReject).  (((fst(fst(AcceptOrReject(ar)))) < Reserve(r))  ((r = ar))))


Proof not projected



Definitions occuring in Statement :  MaxVote: MaxVote(es;T;Vote;e;s),  paxos-state-reservation: Reservation(s),  paxos-state-info: Info(s),  paxos-state-name: Name(s),  paxos-state-value: Value(s),  paxos-state-ballot: Ballot(s),  es-class-causal-mrel-fail: es-class-causal-mrel-fail,  es-class-causal-rel-fail: es-class-causal-rel-fail,  es-interface-pair-prior: X;Y,  es-collect-filter-max: Collect(size v's from X  with maximum num[v] such that P[v]  return <num[v],n,v> with n = maximum f[v]),  es-collect-filter: Collect(size v's from X with maximum num[v] such that P[v]),  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||,  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,  btrue: tt,  bool: ,  nat: ,  spreadn: spread4,  spreadn: spread3,  pi1: fst(t),  pi2: snd(t),  le: A  B,  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  less_than: a < b,  apply: f a,  lambda: x.A[x],  pair: <a, b>,  product: x:A  B[x],  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 :  implies: P  Q,  eclass-val: X(e),  bool: ,  nat: ,  Id: Id,  product: x:A  B[x],  equal: s = t,  es-E-interface: E(X),  all: x:A. B[x],  and: P  Q,  es-E: E,  paxos-state-reservation: Reservation(s),  paxos-state-name: Name(s),  pi2: snd(t),  pi1: fst(t),  es-loc: loc(e),  pair: <a, b>,  es-class-causal-rel-fail: es-class-causal-rel-fail,  paxos-state-info: Info(s),  es-tagged-true-class: Tagged_tt(X),  MaxVote: MaxVote(es;T;Vote;e;s),  apply: f a,  id-deq: IdDeq,  deq-member: deq-member(eq;x;L),  lambda: x.A[x],  filter: filter(P;l),  length: ||as||,  le: A  B,  no_repeats: no_repeats(T;l),  natural_number: $n,  multiply: n * m,  add: n + m,  int: ,  eclass: EClass(A[eo; e]),  map-class: (f[v] where v from X),  spreadn: spread4,  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  paxos-state-ballot: Ballot(s),  minus: -n,  paxos-state-value: Value(s),  es-interface-pair-prior: X;Y,  es-collect-filter-max: Collect(size v's from X  with maximum num[v] such that P[v]  return <num[v],n,v> with n = maximum f[v]),  btrue: tt,  es-filter-image: f[X],  spreadn: spread3,  lt_int: i <z j,  single-bag: {x},  empty-bag: {},  le_int: i z j,  es-class-causal-mrel-fail: es-class-causal-mrel-fail,  iff: P  Q,  assert: b,  es-le: e loc e' ,  mapfilter-class: (f[v] where v from X such that P[v]),  es-collect-filter: Collect(size v's from X with maximum num[v] such that P[v]),  or: P  Q,  exists: x:A. B[x],  bfalse: ff,  alle-lt: e<e'.P[e],  not: A,  in-eclass: e  X,  less_than: a < b,  es-locl: (e <loc e')
Paxos-spec7-body\{i:l\}(Info;
                                            es;
                                            T;
                                            f;
                                            acceptors;
                                            Reserve;
                                            VoteState;
                                            Proposal;
                                            AcceptOrReject;
                                            leader;
                                            Decide;
                                            Vote;
                                            Input;
                                            Collect;
                                            NoProposal;
                                            NewBallot;
                                            failset)  ==
    ((||acceptors||  =  ((2  *  f)  +  1))
    \mwedge{}  no\_repeats(Id;acceptors)
    \mwedge{}  (||filter(\mlambda{}a.deq-member(IdDeq;a;failset);acceptors)||  \mleq{}  f))
    \mwedge{}  (\mforall{}e:E(Vote).  (loc(e)  =  (leader  (snd(fst(Vote(e)))))))
    \mwedge{}  (\mforall{}e:E(VoteState).  (loc(e)  =  (leader  Reservation(VoteState(e)))))
    \mwedge{}  \mforall{}e,r,vs.  e\mmember{}Reserve(r)  \mLeftarrow{}c\mRightarrow{}  \mexists{}  VoteState(vs)  such  that
                                                              (r  =  Reservation(vs))
                                                            \mwedge{}  (loc(e)  =  Name(vs))
                                                            \mwedge{}  MaxVote(es;T;Tagged\_tt(AcceptOrReject);e;Info(vs))
                                                            unless  loc(e)  \mmember{}  failset
    \mwedge{}  \mforall{}e,x,v.  e\mmember{}AcceptOrReject(x)  \mLeftarrow{}c\mRightarrow{}  \mexists{}  Vote(v)  such  that
                                                                          v  =  <<loc(e),  fst(fst(x))>,  snd(x)>
                                                                        unless  loc(e)  \mmember{}  failset
    \mwedge{}  (\mforall{}e1,e2:E(VoteState).
              ((Name(VoteState(e1))  =  Name(VoteState(e2)))
              {}\mRightarrow{}  (Reservation(VoteState(e1))  =  Reservation(VoteState(e2)))
              {}\mRightarrow{}  (e1  =  e2)))
    \mwedge{}  (\mforall{}e1,e2:E(Vote).    ((Vote(e1)  =  Vote(e2))  {}\mRightarrow{}  (loc(e1)  =  loc(e2))  {}\mRightarrow{}  (e1  =  e2)))
    \mwedge{}  (Collect
        =  (let  inpt,b,mx,vs  =  q
              in  <b
                    ,  mx
                    ,  if  (Ballot(vs)  =\msubz{}  -1)
                    then  inpt
                    else  Value(vs)
                    fi  >      where  q  from  Input;
                                                            Collect(f  +  1  vs's  from  VoteState    with  maximum  Reservation(vs)
                                                                            such  that  tt
                                                                              return  <Reservation(vs),n,vs>  with  n  =  maximum  Ballot(vs))))
    \mwedge{}  (Proposal  =  \mlambda{}tr.let  b,b',v  =  tr  in  if  b'  <z  b  then  \{<b,  v>\}  else  \{\}  fi  [Collect])
    \mwedge{}  (NoProposal  =  \mlambda{}tr.let  b,b',v  =  tr  in  if  b  \mleq{}z  b'  then  \{b\}  else  \{\}  fi  [Collect])
    \mwedge{}  \mforall{}e,p,pb.  e\mmember{}Proposal(p)  \mLeftarrow{}c\mRightarrow{}  at  each  of  acceptors
                                                              \mexists{}  AcceptOrReject(pb)  such  that
                                                                p  =  (fst(pb))
                                                              unless  loc(e)  \mmember{}  failset
    \mwedge{}  (\mforall{}e:E(AcceptOrReject)
              (\muparrow{}(snd(AcceptOrReject(e)))
              \mLeftarrow{}{}\mRightarrow{}  \mforall{}e':E(Reserve).  (e'  \mleq{}loc  e    {}\mRightarrow{}  (Reserve(e')  \mleq{}  (fst(fst(AcceptOrReject(e))))))))
    \mwedge{}  (Decide
        =  (snd(fst(p))  where  p  from  Proposal;
                                                                Collect(f  +  1  vt's  from  Vote  with  maximum  snd(fst(vt))
                                                                                such  that  snd(vt))  such  that  (fst(fst(p))  =\msubz{}  snd(p))))
    \mwedge{}  \mforall{}e,b,r.  e\mmember{}NewBallot(b)  \mLeftarrow{}c\mRightarrow{}  at  each  of  acceptors
                                                              \mexists{}  Reserve(r)  such  that
                                                                r  =  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(Vote)
                      (e'  \mleq{}loc  e 
                      \mwedge{}  ((snd(fst(Vote(e))))  =  NewBallot(e'))
                      \mwedge{}  snd(Vote(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(Vote)
                                ((nb1  \mleq{}loc  e    \mwedge{}  e  \mleq{}loc  nb2  )
                                \mwedge{}  ((snd(fst(Vote(e))))  =  NewBallot(nb1))
                                \mwedge{}  snd(Vote(e))  =  ff
                                \mwedge{}  \mforall{}x<e.\mneg{}\muparrow{}x  \mmember{}\msubb{}  Decide))))))
    \mwedge{}  (\mforall{}r:E(Reserve).  \mforall{}ar:E(AcceptOrReject).
              (((fst(fst(AcceptOrReject(ar))))  <  Reserve(r))  {}\mRightarrow{}  (\mneg{}(r  =  ar))))


Date html generated: 2011_10_20-PM-04_43_40
Last ObjectModification: 2011_01_22-PM-10_26_29

Home Index