Nuprl Definition : Paxos-spec6-body

Paxos-spec6-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)))
   b,e such that e is first@ leader b s.t.  q.||filter(e'.(Reservation(VoteState(e')) = b);(VoteState)(q))||
                   = (f + 1)
      (e  (Input)')
      e'<e.(e'  VoteState)  (Reservation(VoteState(e'))  b)
      eCollect with value 
      let l = mapfilter(e'.VoteState(e');e'.(Reservation(VoteState(e')) = b);(VoteState)(e)) in
          let mx,vs = list-max(vs.Ballot(vs);l) 
          in <b, mx, if (mx = -1) then (Input)'(e) else Value(vs) fi > 
   (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))))))))
   b,d such that d is first@ leader b s.t.  q.||filter(e'.((snd(fst(Vote(e'))) = b)  snd(Vote(e')) =b tt);
                                                         (Vote)(q))||
                   = (f + 1)
      ((d  (Proposal)')  ((fst((Proposal)'(d))) = b))
      e'<d.(e'  Vote)  (((snd(fst(Vote(e'))))  b)  (((snd(fst(Vote(e')))) = b)  snd(Vote(e')) = tt))
      dDecide with value  snd((Proposal)'(d)) 
   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-class-def: es-class-def,  es-prior-val: (X)',  es-interface-predecessors: (X)(e),  es-tagged-true-class: Tagged_tt(X),  es-E-interface: E(X),  es-filter-image: f[X],  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  es-first-at: e is first@ i s.t.  e.P[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),  eq_bool: p =b q,  le_int: i z j,  band: p  q,  lt_int: i <z j,  assert: b,  ifthenelse: if b then t else f fi ,  bfalse: ff,  btrue: tt,  bool: ,  nat: ,  let: let,  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],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  multiply: n * m,  add: n + m,  minus: -n,  natural_number: $n,  int: ,  equal: s = t,  mapfilter: mapfilter(f;P;L),  no_repeats: no_repeats(T;l),  filter: filter(P;l),  deq-member: deq-member(eq;x;L),  single-bag: {x},  empty-bag: {},  list-max: list-max(x.f[x];L)
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: ,  es-class-def: es-class-def,  es-first-at: e is first@ i s.t.  e.P[e],  eq_int: (i = j),  es-interface-predecessors: (X)(e),  assert: b,  in-eclass: e  X,  es-prior-val: (X)',  alle-lt: e<e'.P[e],  let: let,  mapfilter: mapfilter(f;P;L),  spread: spread def,  list-max: list-max(x.f[x];L),  paxos-state-ballot: Ballot(s),  ifthenelse: if b then t else f fi ,  minus: -n,  paxos-state-value: Value(s),  eclass: EClass(A[eo; e]),  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,  es-le: e loc e' ,  band: p  q,  eq_bool: p =b q,  btrue: tt,  or: P  Q,  exists: x:A. B[x],  bfalse: ff,  not: A,  less_than: a < b,  es-locl: (e <loc e')
FDL editor aliases :  Paxos-spec6-body
Paxos-spec6-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{}  \mforall{}b,e  such  that  e  is  first@  leader  b  s.t.    q.||filter(\mlambda{}e'.(Reservation(VoteState(e'))  =\msubz{}  b);
                                                                                                                  \mleq{}(VoteState)(q))||
                                      =  (f  +  1)
          \mwedge{}  (\muparrow{}e  \mmember{}\msubb{}  (Input)')
          \mwedge{}  \mforall{}e'<e.(\muparrow{}e'  \mmember{}\msubb{}  VoteState)  {}\mRightarrow{}  (Reservation(VoteState(e'))  \mleq{}  b)
            e\mmember{}Collect  with  value    let  l  =  mapfilter(\mlambda{}e'.VoteState(e');
                                                                                            \mlambda{}e'.(Reservation(VoteState(e'))  =\msubz{}  b);
                                                                                            \mleq{}(VoteState)(e))  in
                                                                let  mx,vs  =  list-max(vs.Ballot(vs);l) 
                                                                in  <b,  mx,  if  (mx  =\msubz{}  -1)  then  (Input)'(e)  else  Value(vs)  fi  > 
    \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{}  \mforall{}b,d  such  that  d  is  first@  leader  b  s.t.    q.||filter(\mlambda{}e'.((snd(fst(Vote(e')))  =\msubz{}  b)
                                                                                                                          \mwedge{}\msubb{}  snd(Vote(e'))  =b  tt);\mleq{}(Vote)(q))||
                                      =  (f  +  1)
          \mwedge{}  ((\muparrow{}d  \mmember{}\msubb{}  (Proposal)')  \mwedge{}  ((fst((Proposal)'(d)))  =  b))
          \mwedge{}  \mforall{}e'<d.(\muparrow{}e'  \mmember{}\msubb{}  Vote)
              {}\mRightarrow{}  (((snd(fst(Vote(e'))))  \mleq{}  b)  \mwedge{}  (((snd(fst(Vote(e'))))  =  b)  {}\mRightarrow{}  snd(Vote(e'))  =  tt))
            d\mmember{}Decide  with  value    snd((Proposal)'(d)) 
    \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_33_26
Last ObjectModification: 2011_01_22-PM-10_23_49

Home Index