Comment: EventML spec properties
exports: []
prefix: new_23_sig:s
name: new-23-sig.esh:s
Comment: ------ new_23_sig - headers ------
⋅
Definition: new_23_sig_headers
new_23_sig_headers(notify;propose) ==
[``new_23_sig vote``; ``new_23_sig retry``; ``new_23_sig decided``; notify; propose]
Lemma: new_23_sig_headers_wf
∀[notify,propose:Atom List]. (new_23_sig_headers(notify;propose) ∈ Name List)
Definition: new_23_sig_headers_no_rep
new_23_sig_headers_no_rep(notify;propose) == no_repeats(Name;new_23_sig_headers(notify;propose))
Lemma: new_23_sig_headers_no_rep_wf
∀[notify,propose:Atom List]. (new_23_sig_headers_no_rep(notify;propose) ∈ ℙ)
Definition: new_23_sig_headers_fun
new_23_sig_headers_fun(Cmd;notify;propose) ==
λhdr.if name_eq(hdr;``new_23_sig vote``) then ℤ × ℤ × Cmd × Id
if name_eq(hdr;``new_23_sig retry``) then ℤ × ℤ × Cmd
if name_eq(hdr;``new_23_sig decided``) then ℤ × Cmd
if name_eq(hdr;notify) then ℤ × Cmd
if name_eq(hdr;propose) then ℤ × Cmd
else Top
fi
Lemma: new_23_sig_headers_fun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. (new_23_sig_headers_fun(Cmd;notify;propose) ∈ Name ⟶ Type)
Definition: new_23_sig_headers_type
new_23_sig_headers_type{i:l}(Cmd;notify;propose) ==
{f:Name ⟶ ValueAllType|
new_23_sig_headers_no_rep(notify;propose)
∧ (∀hdr∈new_23_sig_headers(notify;propose).(f hdr) = (new_23_sig_headers_fun(Cmd;notify;propose) hdr))}
Lemma: new_23_sig_headers_type_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. (new_23_sig_headers_type{i:l}(Cmd;notify;propose) ∈ ℙ')
Comment: ------ new_23_sig - specification ------
⋅
Definition: new_23_sig_vote'base
new_23_sig_vote'base(Cmd;notify;propose;f) == Base(``new_23_sig vote``)
Lemma: new_23_sig_vote'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_vote'base(Cmd;notify;propose;f) ∈ EClass(ℤ × ℤ × Cmd × Id))
Definition: new_23_sig_vote'base-program
new_23_sig_vote'base-program(Cmd;notify;propose;f) == base-class-program(``new_23_sig vote``)
Lemma: new_23_sig_vote'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_vote'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_vote'base(Cmd;notify;propose;f)))
Definition: new_23_sig_vote'broadcast
new_23_sig_vote'broadcast(Cmd;notify;propose;f) ==
λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(``new_23_sig vote``;z));locs)
Lemma: new_23_sig_vote'broadcast_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_vote'broadcast(Cmd;notify;propose;f) ∈ bag(Id) ⟶ (ℤ × ℤ × Cmd × Id) ⟶ bag(Interface))
Definition: new_23_sig_retry'base
new_23_sig_retry'base(Cmd;notify;propose;f) == Base(``new_23_sig retry``)
Lemma: new_23_sig_retry'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_retry'base(Cmd;notify;propose;f) ∈ EClass(ℤ × ℤ × Cmd))
Definition: new_23_sig_retry'base-program
new_23_sig_retry'base-program(Cmd;notify;propose;f) == base-class-program(``new_23_sig retry``)
Lemma: new_23_sig_retry'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_retry'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_retry'base(Cmd;notify;propose;f)))
Definition: new_23_sig_retry'send
new_23_sig_retry'send(Cmd;notify;propose;f) == λl,z. mk-msg-interface(l;make-Msg(``new_23_sig retry``;z))
Lemma: new_23_sig_retry'send_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_retry'send(Cmd;notify;propose;f) ∈ Id ⟶ (ℤ × ℤ × Cmd) ⟶ Interface)
Definition: new_23_sig_decided'base
new_23_sig_decided'base(Cmd;notify;propose;f) == Base(``new_23_sig decided``)
Lemma: new_23_sig_decided'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_decided'base(Cmd;notify;propose;f) ∈ EClass(ℤ × Cmd))
Definition: new_23_sig_decided'base-program
new_23_sig_decided'base-program(Cmd;notify;propose;f) == base-class-program(``new_23_sig decided``)
Lemma: new_23_sig_decided'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_decided'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_decided'base(Cmd;notify;propose;f)))
Definition: new_23_sig_decided'broadcast
new_23_sig_decided'broadcast(Cmd;notify;propose;f) ==
λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(``new_23_sig decided``;z));locs)
Lemma: new_23_sig_decided'broadcast_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_decided'broadcast(Cmd;notify;propose;f) ∈ bag(Id) ⟶ (ℤ × Cmd) ⟶ bag(Interface))
Definition: new_23_sig_notify'broadcast
new_23_sig_notify'broadcast(Cmd;notify;propose;f) == λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(notify;z));locs)
Lemma: new_23_sig_notify'broadcast_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_notify'broadcast(Cmd;notify;propose;f) ∈ bag(Id) ⟶ (ℤ × Cmd) ⟶ bag(Interface))
Definition: new_23_sig_propose'base
new_23_sig_propose'base(Cmd;notify;propose;f) == Base(propose)
Lemma: new_23_sig_propose'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_propose'base(Cmd;notify;propose;f) ∈ EClass(ℤ × Cmd))
Definition: new_23_sig_propose'base-program
new_23_sig_propose'base-program(Cmd;notify;propose;f) == base-class-program(propose)
Lemma: new_23_sig_propose'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_propose'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_propose'base(Cmd;notify;propose;f)))
Definition: new_23_sig_roundout
new_23_sig_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λloc,za,z. let zb,sender = za
in let zc,c = zb
in let n,i = zc
in let cmds,locs = z
in if (||cmds|| =z coeff * flrs)
then let k,x = poss-maj(cmdeq;[c / cmds];c)
in if (k =z (coeff * flrs) + 1)
then new_23_sig_decided'broadcast(Cmd;notify;propose;f) reps <n, x>
else {new_23_sig_retry'send(Cmd;notify;propose;f) loc <<n, i + 1>, x>}
fi
else {}
fi
Lemma: new_23_sig_roundout_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ Id
⟶ (ℤ × ℤ × Cmd × Id)
⟶ (Cmd List × (Id List))
⟶ bag(Interface))
Definition: new_23_sig_newvote
new_23_sig_newvote(Cmd) ==
λni,zd,z. let ze,sender = zd
in let ni',c = ze
in let cmds,locs = z
in (product-deq(ℤ;ℤ;IntDeq;IntDeq) ni ni') ∧b (¬bsender ∈b locs)
Lemma: new_23_sig_newvote_wf
∀[Cmd:ValueAllType]. (new_23_sig_newvote(Cmd) ∈ (ℤ × ℤ) ⟶ (ℤ × ℤ × Cmd × Id) ⟶ (Cmd List × (Id List)) ⟶ 𝔹)
Definition: new_23_sig_addvote
new_23_sig_addvote(Cmd) ==
λzf,z. let zg,sender = zf in let ni,c = zg in let cmds,locs = z in <[c / cmds], [sender / locs]>
Lemma: new_23_sig_addvote_wf
∀[Cmd:ValueAllType]. (new_23_sig_addvote(Cmd) ∈ (ℤ × ℤ × Cmd × Id) ⟶ (Cmd List × (Id List)) ⟶ (Cmd List × (Id List)))
Definition: new_23_sig_add_to_quorum
new_23_sig_add_to_quorum(Cmd) ==
λni,loc,vt,state. if new_23_sig_newvote(Cmd) ni vt state then new_23_sig_addvote(Cmd) vt state else state fi
Lemma: new_23_sig_add_to_quorum_wf
∀[Cmd:ValueAllType]
(new_23_sig_add_to_quorum(Cmd) ∈ (ℤ × ℤ)
⟶ Id
⟶ (ℤ × ℤ × Cmd × Id)
⟶ (Cmd List × (Id List))
⟶ (Cmd List × (Id List)))
Definition: new_23_sig_when_quorum
new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λni,loc,vt,state. if new_23_sig_newvote(Cmd) ni vt state
then new_23_sig_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) loc vt state
else {}
fi
Lemma: new_23_sig_when_quorum_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × ℤ)
⟶ Id
⟶ (ℤ × ℤ × Cmd × Id)
⟶ (Cmd List × (Id List))
⟶ bag(Interface))
Definition: new_23_sig_QuorumState
new_23_sig_QuorumState(Cmd;notify;propose;f) ==
λni.memory-class1(initially λloc.<[], []>
applying new_23_sig_add_to_quorum(Cmd) ni
on new_23_sig_vote'base(Cmd;notify;propose;f))
Lemma: new_23_sig_QuorumState_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_QuorumState(Cmd;notify;propose;f) ∈ (ℤ × ℤ) ⟶ EClass(Cmd List × (Id List)))
Lemma: new_23_sig_QuorumState-functional
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[x:ℤ × ℤ].
new_23_sig_QuorumState(Cmd;notify;propose;f) x is functional
Definition: new_23_sig_QuorumStateFun
new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e) == new_23_sig_QuorumState(Cmd;notify;propose;f) x(e)
Lemma: new_23_sig_QuorumStateFun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[x:ℤ × ℤ].
(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e) ∈ Cmd List × (Id List))
Lemma: new_23_sig_QuorumState-classrel
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀es:EO+(Message(f)). ∀e:E. ∀x:ℤ × ℤ. ∀v:Cmd List × (Id List).
(v ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) x(e)
⇐⇒ v = new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e))
Definition: new_23_sig_QuorumState-program
new_23_sig_QuorumState-program(Cmd;notify;propose;f) ==
λni.memory-class1-program(λloc.<[], []>;new_23_sig_add_to_quorum(Cmd)
ni;new_23_sig_vote'base-program(Cmd;notify;propose;f))
Lemma: new_23_sig_QuorumState-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_QuorumState-program(Cmd;notify;propose;f) ∈ ∀x:ℤ × ℤ
LocalClass(new_23_sig_QuorumState(Cmd;notify;propose;f) x))
Definition: new_23_sig_Quorum
new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λni.((new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ni o
new_23_sig_vote'base(Cmd;notify;propose;f)) o new_23_sig_QuorumState(Cmd;notify;propose;f) ni)
Lemma: new_23_sig_Quorum_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × ℤ) ⟶ EClass(Interface))
Definition: new_23_sig_Quorum-program
new_23_sig_Quorum-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λni.eclass1-program(new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ni;
new_23_sig_vote'base-program(Cmd;notify;propose;f))
o new_23_sig_QuorumState-program(Cmd;notify;propose;f) ni
Lemma: new_23_sig_Quorum-program_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Quorum-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
∈ ∀x:ℤ × ℤ. LocalClass(new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) x))
Lemma: new_23_sig_quorum_invariant
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1:E. ∀ni:ℤ × ℤ. ∀z:Cmd List × (Id List).
(z ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
⇒ let cmds,locs = z
in no_repeats(Id;locs) ∧ (||locs|| = ||cmds||))
Lemma: new_23_sig_quorum_fseg
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀ni:ℤ × ℤ. ∀zh,z:Cmd List × (Id List).
((e1 <loc e2)
⇒ zh ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
⇒ z ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e2)
⇒ let cmds1,locs1 = zh
in let cmds2,locs2 = z
in fseg(Cmd;cmds1;cmds2) ∧ fseg(Id;locs1;locs2))
Definition: new_23_sig_Round
new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λz.let ni,c = z
in return-loc-bag-class(λloc.(new_23_sig_vote'broadcast(Cmd;notify;propose;f) reps
<<ni, c>, loc>)) || (new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
ni once)
Lemma: new_23_sig_Round_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × ℤ × Cmd) ⟶ EClass(Interface))
Definition: new_23_sig_Round-program
new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λz.let ni,c = z
in return-loc-bag-class-program(λloc.(new_23_sig_vote'broadcast(Cmd;notify;propose;f) reps
<<ni, c>, loc>))
|| once-class-program(new_23_sig_Quorum-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ni)
Lemma: new_23_sig_Round-program_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
∈ ∀x:ℤ × ℤ × Cmd. LocalClass(new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) x))
Definition: new_23_sig_vote2retry
new_23_sig_vote2retry(Cmd) == λloc,z. let z,sender = z in let ni,c = z in {<ni, c>}
Lemma: new_23_sig_vote2retry_wf
∀[Cmd:ValueAllType]. (new_23_sig_vote2retry(Cmd) ∈ Id ⟶ (ℤ × ℤ × Cmd × Id) ⟶ bag(ℤ × ℤ × Cmd))
Definition: new_23_sig_RoundInfo
new_23_sig_RoundInfo(Cmd;notify;propose;f) ==
new_23_sig_retry'base(Cmd;notify;propose;f)
|| (new_23_sig_vote2retry(Cmd) o new_23_sig_vote'base(Cmd;notify;propose;f))
Lemma: new_23_sig_RoundInfo_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_RoundInfo(Cmd;notify;propose;f) ∈ EClass(ℤ × ℤ × Cmd))
Definition: new_23_sig_RoundInfo-program
new_23_sig_RoundInfo-program(Cmd;notify;propose;f) ==
new_23_sig_retry'base-program(Cmd;notify;propose;f)
|| eclass0-program(new_23_sig_vote2retry(Cmd);new_23_sig_vote'base-program(Cmd;notify;propose;f))
Lemma: new_23_sig_RoundInfo-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_RoundInfo-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_RoundInfo(Cmd;notify;propose;f)))
Definition: new_23_sig_update_round
new_23_sig_update_round(Cmd) ==
λn,loc,z,round. let z,c = z in let m,i = z in if (n =z m) ∧b round <z i then i else round fi
Lemma: new_23_sig_update_round_wf
∀[Cmd:ValueAllType]. (new_23_sig_update_round(Cmd) ∈ ℤ ⟶ Id ⟶ (ℤ × ℤ × Cmd) ⟶ ℤ ⟶ ℤ)
Definition: new_23_sig_when_new_round
new_23_sig_when_new_round(Cmd) ==
λn,loc,z,round. let z,c = z in let m,i = z in if (n =z m) ∧b round <z i then {<<m, i>, c>} else {} fi
Lemma: new_23_sig_when_new_round_wf
∀[Cmd:ValueAllType]. (new_23_sig_when_new_round(Cmd) ∈ ℤ ⟶ Id ⟶ (ℤ × ℤ × Cmd) ⟶ ℤ ⟶ bag(ℤ × ℤ × Cmd))
Definition: new_23_sig_NewRoundsState
new_23_sig_NewRoundsState(Cmd;notify;propose;f) ==
λn.memory-class1(initially λloc.0
applying new_23_sig_update_round(Cmd) n
on new_23_sig_RoundInfo(Cmd;notify;propose;f))
Lemma: new_23_sig_NewRoundsState_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_NewRoundsState(Cmd;notify;propose;f) ∈ ℤ ⟶ EClass(ℤ))
Lemma: new_23_sig_NewRoundsState-functional
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[x:ℤ].
new_23_sig_NewRoundsState(Cmd;notify;propose;f) x is functional
Definition: new_23_sig_NewRoundsStateFun
new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e) == new_23_sig_NewRoundsState(Cmd;notify;propose;f) x(e)
Lemma: new_23_sig_NewRoundsStateFun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[x:ℤ].
(new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e) ∈ ℤ)
Lemma: new_23_sig_NewRoundsState-classrel
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀es:EO+(Message(f)). ∀e:E. ∀x,v:ℤ.
(v ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) x(e)
⇐⇒ v = new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e))
Definition: new_23_sig_NewRoundsState-program
new_23_sig_NewRoundsState-program(Cmd;notify;propose;f) ==
λn.memory-class1-program(λloc.0;new_23_sig_update_round(Cmd) n;new_23_sig_RoundInfo-program(Cmd;notify;propose;f))
Lemma: new_23_sig_NewRoundsState-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_NewRoundsState-program(Cmd;notify;propose;f)
∈ ∀x:ℤ. LocalClass(new_23_sig_NewRoundsState(Cmd;notify;propose;f) x))
Definition: new_23_sig_NewRounds
new_23_sig_NewRounds(Cmd;notify;propose;f) ==
λn.((new_23_sig_when_new_round(Cmd) n o new_23_sig_RoundInfo(Cmd;notify;propose;f)) o
new_23_sig_NewRoundsState(Cmd;notify;propose;f) n)
Lemma: new_23_sig_NewRounds_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_NewRounds(Cmd;notify;propose;f) ∈ ℤ ⟶ EClass(ℤ × ℤ × Cmd))
Definition: new_23_sig_NewRounds-program
new_23_sig_NewRounds-program(Cmd;notify;propose;f) ==
λn.eclass1-program(new_23_sig_when_new_round(Cmd) n;new_23_sig_RoundInfo-program(Cmd;notify;propose;f))
o new_23_sig_NewRoundsState-program(Cmd;notify;propose;f) n
Lemma: new_23_sig_NewRounds-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_NewRounds-program(Cmd;notify;propose;f) ∈ ∀x:ℤ. LocalClass(new_23_sig_NewRounds(Cmd;notify;propose;f) x))
Lemma: new_23_sig_rounds_pos
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1:E. ∀n,round:ℤ.
(round ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1) ⇒ (0 ≤ round))
Lemma: new_23_sig_rounds_inc
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ.
((e1 <loc e2)
⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
⇒ (round1 ≤ round2))
Lemma: new_23_sig_rounds_strict_inc
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ.
((∃z:ℤ × ℤ × Cmd
∃round:ℤ
∃e:E
(e1 ≤loc e
∧ (e <loc e2)
∧ z ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
∧ round ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e)
∧ let z,cmd = z
in let n',round' = z
in (n' = n) ∧ round < round'))
⇒ (e1 <loc e2)
⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
⇒ round1 < round2)
Lemma: new_23_sig_rounds_mem
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ. ∀z:ℤ × ℤ × Cmd.
((e1 <loc e2)
⇒ z ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e1)
⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
⇒ let z,cmd = z
in let n',round' = z
in (n = n') ⇒ (round' ≤ round2))
Definition: new_23_sig_decision
new_23_sig_decision(Cmd;clients;notify;propose;f) ==
λn,loc,z. let m,c = z in if (m =z n) then new_23_sig_notify'broadcast(Cmd;notify;propose;f) clients <m, c> else {} fi
Lemma: new_23_sig_decision_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[notify,propose:Atom List].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_decision(Cmd;clients;notify;propose;f) ∈ ℤ ⟶ Id ⟶ (ℤ × Cmd) ⟶ bag(Interface))
Definition: new_23_sig_Notify
new_23_sig_Notify(Cmd;clients;notify;propose;f) ==
λn.((new_23_sig_decision(Cmd;clients;notify;propose;f) n o new_23_sig_decided'base(Cmd;notify;propose;f)) once)
Lemma: new_23_sig_Notify_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[notify,propose:Atom List].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Notify(Cmd;clients;notify;propose;f) ∈ ℤ ⟶ EClass(Interface))
Definition: new_23_sig_Notify-program
new_23_sig_Notify-program(Cmd;clients;notify;propose;f) ==
λn.once-class-program(eclass0-program(new_23_sig_decision(Cmd;clients;notify;propose;f) n;
new_23_sig_decided'base-program(Cmd;notify;propose;f)))
Lemma: new_23_sig_Notify-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[notify,propose:Atom List].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Notify-program(Cmd;clients;notify;propose;f)
∈ ∀x:ℤ. LocalClass(new_23_sig_Notify(Cmd;clients;notify;propose;f) x))
Definition: new_23_sig_Rounds
new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λzi.let n,c = zi
in new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
<<n, 0>, c> || new_23_sig_NewRounds(Cmd;notify;propose;f) n
>z> new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) z
Lemma: new_23_sig_Rounds_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × Cmd) ⟶ EClass(Interface))
Definition: new_23_sig_Rounds-program
new_23_sig_Rounds-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λzi.let n,c = zi
in new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
<<n, 0>, c> || new_23_sig_NewRounds-program(Cmd;notify;propose;f) n
>>= λz.(new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) z)
Lemma: new_23_sig_Rounds-program_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Rounds-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
∈ ∀x:ℤ × Cmd. LocalClass(new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) x))
Definition: new_23_sig_Voter
new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λz.let n,c = z
in (new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <n, c> until new_23_sig_Notify(Cmd;clients;notify\000C;propose;f) n)
|| new_23_sig_Notify(Cmd;clients;notify;propose;f) n
Lemma: new_23_sig_Voter_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × Cmd) ⟶ EClass(Interface))
Definition: new_23_sig_Voter-program
new_23_sig_Voter-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) ==
λz.let n,c = z
in until-class-program(new_23_sig_Rounds-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <n, c>;new_23_sig_Noti\000Cfy-program(Cmd;clients;notify;propose;f) n)
|| new_23_sig_Notify-program(Cmd;clients;notify;propose;f) n
Lemma: new_23_sig_Voter-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Voter-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f)
∈ ∀x:ℤ × Cmd. LocalClass(new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) x))
Definition: new_23_sig_vote2prop
new_23_sig_vote2prop(Cmd) == λloc,z. let z,loc' = z in let z,c = z in let n,i = z in {<n, c>}
Lemma: new_23_sig_vote2prop_wf
∀[Cmd:ValueAllType]. (new_23_sig_vote2prop(Cmd) ∈ Id ⟶ (ℤ × ℤ × Cmd × Id) ⟶ bag(ℤ × Cmd))
Definition: new_23_sig_Proposal
new_23_sig_Proposal(Cmd;notify;propose;f) ==
new_23_sig_propose'base(Cmd;notify;propose;f)
|| (new_23_sig_vote2prop(Cmd) o new_23_sig_vote'base(Cmd;notify;propose;f))
Lemma: new_23_sig_Proposal_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Proposal(Cmd;notify;propose;f) ∈ EClass(ℤ × Cmd))
Definition: new_23_sig_Proposal-program
new_23_sig_Proposal-program(Cmd;notify;propose;f) ==
new_23_sig_propose'base-program(Cmd;notify;propose;f)
|| eclass0-program(new_23_sig_vote2prop(Cmd);new_23_sig_vote'base-program(Cmd;notify;propose;f))
Lemma: new_23_sig_Proposal-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Proposal-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_Proposal(Cmd;notify;propose;f)))
Definition: new_23_sig_update_replica
new_23_sig_update_replica(Cmd;slots) == λloc,zj,z. let n,c = zj in set-sig-add(slots) n z
Lemma: new_23_sig_update_replica_wf
∀[Cmd:ValueAllType]. ∀[slots:set-sig{i:l}(ℤ)].
(new_23_sig_update_replica(Cmd;slots) ∈ Id ⟶ (ℤ × Cmd) ⟶ set-sig-set(slots) ⟶ set-sig-set(slots))
Definition: new_23_sig_when_new_proposal
new_23_sig_when_new_proposal(Cmd;slots) ==
λloc,zk,z. let n,c = zk in if set-sig-member(slots) n z then {} else {<n, c>} fi
Lemma: new_23_sig_when_new_proposal_wf
∀[Cmd:ValueAllType]. ∀[slots:set-sig{i:l}(ℤ)].
(new_23_sig_when_new_proposal(Cmd;slots) ∈ Id ⟶ (ℤ × Cmd) ⟶ set-sig-set(slots) ⟶ bag(ℤ × Cmd))
Definition: new_23_sig_ReplicaState
new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) ==
memory-class1(initially λloc.set-sig-empty(slots)
applying new_23_sig_update_replica(Cmd;slots)
on new_23_sig_Proposal(Cmd;notify;propose;f))
Lemma: new_23_sig_ReplicaState_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) ∈ EClass(set-sig-set(slots)))
Lemma: new_23_sig_ReplicaState-functional
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) is functional
Definition: new_23_sig_ReplicaStateFun
new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e) == new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e)
Lemma: new_23_sig_ReplicaStateFun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E].
(new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e) ∈ set-sig-set(slots))
Lemma: new_23_sig_ReplicaState-classrel
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀es:EO+(Message(f)). ∀e:E. ∀v:set-sig-set(slots).
(v ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e)
⇐⇒ v = new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e))
Definition: new_23_sig_ReplicaState-program
new_23_sig_ReplicaState-program(Cmd;notify;propose;slots;f) ==
memory-class1-program(λloc.set-sig-empty(slots);new_23_sig_update_replica(Cmd;slots);...)
Lemma: new_23_sig_ReplicaState-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_ReplicaState-program(Cmd;notify;propose;slots;f)
∈ LocalClass(new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)))
Definition: new_23_sig_NewVoters
new_23_sig_NewVoters(Cmd;notify;propose;slots;f) ==
((new_23_sig_when_new_proposal(Cmd;slots) o new_23_sig_Proposal(Cmd;notify;propose;f)) o
new_23_sig_ReplicaState(Cmd;notify;propose;slots;f))
Lemma: new_23_sig_NewVoters_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_NewVoters(Cmd;notify;propose;slots;f) ∈ EClass(ℤ × Cmd))
Definition: new_23_sig_NewVoters-program
new_23_sig_NewVoters-program(Cmd;notify;propose;slots;f) ==
eclass1-program(new_23_sig_when_new_proposal(Cmd;slots);new_23_sig_Proposal-program(Cmd;notify;propose;f))
o new_23_sig_ReplicaState-program(Cmd;notify;propose;slots;f)
Lemma: new_23_sig_NewVoters-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_NewVoters-program(Cmd;notify;propose;slots;f)
∈ LocalClass(new_23_sig_NewVoters(Cmd;notify;propose;slots;f)))
Lemma: new_23_sig_increasing_max
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀slots1,slots2:set-sig-set(slots).
((e1 <loc e2)
⇒ slots1 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e1)
⇒ slots2 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e2)
⇒ (∀x:ℤ. ((↑(set-sig-member(slots) x slots1)) ⇒ (↑(set-sig-member(slots) x slots2)))))
Lemma: new_23_sig_replica_state_mem
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀slots1,slots2:set-sig-set(slots).
∀z:ℤ × Cmd.
((e1 <loc e2)
⇒ z ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
⇒ slots1 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e1)
⇒ slots2 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e2)
⇒ let n,cmd = z
in ↑(set-sig-member(slots) n slots2))
Definition: new_23_sig_Replica
new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
new_23_sig_NewVoters(Cmd;notify;propose;slots;f)
>z> new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) z
Lemma: new_23_sig_Replica_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ EClass(Interface))
Definition: new_23_sig_Replica-program
new_23_sig_Replica-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
new_23_sig_NewVoters-program(Cmd;notify;propose;slots;f)
>>= λz.(new_23_sig_Voter-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) z)
Lemma: new_23_sig_Replica-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_Replica-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)
∈ LocalClass(new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)))
Definition: new_23_sig_main
new_23_sig_main() == new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@reps
Lemma: new_23_sig_main_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_main() ∈ EClass(Interface))
Definition: new_23_sig_main-program
new_23_sig_main-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
(new_23_sig_Replica-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f))@reps
Lemma: new_23_sig_main-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_main-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ LocalClass(new_23_sig_main()))
Comment: ------ new_23_sig - extra ------
⋅
Definition: new_23_sig_headers_internal
new_23_sig_headers_internal() == [``new_23_sig vote``; ``new_23_sig retry``; ``new_23_sig decided``]
Lemma: new_23_sig_headers_internal_wf
new_23_sig_headers_internal() ∈ Name List
Definition: new_23_sig_headers_no_inputs
new_23_sig_headers_no_inputs(notify) == [``new_23_sig vote``; ``new_23_sig retry``; ``new_23_sig decided``; notify]
Lemma: new_23_sig_headers_no_inputs_wf
∀[notify:Atom List]. (new_23_sig_headers_no_inputs(notify) ∈ Name List)
Definition: new_23_sig_headers_no_inputs_types
new_23_sig_headers_no_inputs_types(Cmd;notify) ==
[<``new_23_sig vote``, ℤ × ℤ × Cmd × Id>; <``new_23_sig retry``, ℤ × ℤ × Cmd>; <``new_23_sig decided``, ℤ × Cmd>; <not\000Cify, ℤ × Cmd>]
Lemma: new_23_sig_headers_no_inputs_types_wf
∀[Cmd:ValueAllType]. ∀[notify:Atom List]. (new_23_sig_headers_no_inputs_types(Cmd;notify) ∈ (Name × Type) List)
Definition: new_23_sig_message-constraint
new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
msg-interface-constraint{i:l}(new_23_sig_main();new_23_sig_headers_internal();f)
Lemma: new_23_sig_message-constraint_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ ℙ')
Definition: new_23_sig_messages-delivered
new_23_sig_messages-delivered{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
msgs-interface-delivered{i:l}(new_23_sig_main();f)
Lemma: new_23_sig_messages-delivered_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
(new_23_sig_messages-delivered{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ ℙ')
Lemma: new_23_sig-ilf
(∀[z1:ℤ]. ∀[propose,notify:Atom List]. ∀[clients:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(f)].
{<d, i, m> ∈ new_23_sig_Notify(Cmd;clients;notify;propose;f) z1(e)
⇐⇒ (no (new_23_sig_decision(Cmd;clients;notify;propose;f)
z1 o new_23_sig_decided'base(Cmd;notify;propose;f)) prior to e)
∧ <d, i, m> ∈
{(new_23_sig_decision(Cmd;clients;notify;propose;f) z1 o new_23_sig_decided'base(Cmd;notify;propose;f))}(e)})
∧ (∀[z6,z1:ℤ]. ∀[reps:bag(Id)]. ∀[propose,notify:Atom List]. ∀[flrs,coeff:ℤ]. ∀[Cmd:{T:Type| valueall-type(T)} ].
∀[cmdeq:EqDecider(Cmd)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E].
∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(f)].
{<d, i, m> ∈ new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6>(e)
⇐⇒ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es;e)))
∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es;e))|| = (coeff * flrs))
∧ (d = 0)
∧ (↓(((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;e\000Cs;e)))];snd(fst(msgval(e)))))) = ((coeff * flrs) + 1))
∧ i ↓∈ reps
∧ (m
= make-Msg(``new_23_sig decided``;<fst(fst(fst(msgval(e))))
, snd(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;...;...;f;<z1
, z6
>;es\000C;e)))];snd(fst(msgval(e)))))
>)))
∨ ((¬((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es;e)))];snd(fst(ms\000Cgval(e))))))
= ((coeff * flrs) + 1)))
∧ (i = loc(e))
∧ (m
= make-Msg(``new_23_sig retry``;<<fst(fst(fst(msgval(e)))), (snd(fst(fst(msgval(e))))) + 1>
, snd(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;...;...;f;<z1
, z6
>;es\000C;e)))];snd(fst(msgval(e)))))
>))))})
∧ (∀[z1:ℤ]. ∀[propose,notify:Atom List]. ∀[clients:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id].
∀[m:Message(f)].
{<d, i, m> ∈
(new_23_sig_decision(Cmd;clients;notify;propose;f) z1 o new_23_sig_decided'base(Cmd;notify;propose;f))(e)
⇐⇒ (header(e) = ``new_23_sig decided``)
∧ has-es-info-type(es;e;f;ℤ × Cmd)
∧ ((fst(msgval(e))) = z1)
∧ i ↓∈ clients
∧ (d = 0)
∧ (m = make-Msg(notify;msgval(e)))})
∧ (∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id].
∀[m:Message(f)].
{<d, i, m> ∈ new_23_sig_main()(e)
⇐⇒ loc(e) ↓∈ reps
∧ (↓∃e':{e':E| e' ≤loc e }
∃z1:ℤ
∃z2:Cmd
(((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e')))
∨ ((header(e') = ``new_23_sig vote``)
∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e'))))))
∧ (z2 = (snd(fst(msgval(e')))))))
∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
∧ (((no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
∧ ((((i ↓∈ reps ∧ (d = 0) ∧ (m = make-Msg(``new_23_sig vote``;<<<z1, 0>, z2>, loc(e)>))) ∧ (e = e'))
∨ ((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' and e)
∧ <d, i, m> ∈ {new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0>}(e)))
∨ (∃e1:{e1:E| e1 ≤loc e }
∃z6:ℤ
∃z7:Cmd
(new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
∧ (((header(e1) = ``new_23_sig retry``)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e1)))
∨ ((header(e1) = ``new_23_sig vote``)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e1))))))
∧ (((i ↓∈ reps ∧ (d = 0) ∧ (m = make-Msg(``new_23_sig vote``;<<<z1, z6>, z7>, loc(e)>))) ∧ (e \000C= e1))
∨ ((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ... between ... and
...)
∧ ...))))))
∨ ...)))})
Lemma: new_23_sig-vote
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k,k1:ℤ]. ∀[v:Cmd]. ∀[i1:Id].
(<d, i, mk-msg(auth;``new_23_sig vote``;<<<k, k1>, v>, i1>)> ∈ new_23_sig_main()(e)
⇐⇒ loc(e) ↓∈ reps
∧ (↓∃e':{e':E| e' ≤loc e }
∃z2:Cmd
(((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<k, z2> = msgval(e')))
∨ ((header(e') = ``new_23_sig vote``)
∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
∧ (k = (fst(fst(fst(msgval(e'))))))
∧ (z2 = (snd(fst(msgval(e')))))))
∧ (¬↑(set-sig-member(slots) k new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) k between e' and e)
∧ i ↓∈ reps
∧ (d = 0)
∧ auth = ff
∧ (i1 = loc(e))
∧ (((k1 = 0) ∧ (v = z2) ∧ (e = e'))
∨ (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;k;es.e';e) < k1
∧ (((header(e) = ``new_23_sig retry``)
∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd)
∧ (<<k, k1>, v> = msgval(e)))
∨ ((header(e) = ``new_23_sig vote``)
∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
∧ (<<k, k1>, v> = (fst(msgval(e)))))))))))
Lemma: new_23_sig-retry
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k,k1:ℤ]. ∀[v:Cmd].
(<d, i, mk-msg(auth;``new_23_sig retry``;<<k, k1>, v>)> ∈ new_23_sig_main()(e)
⇐⇒ loc(e) ↓∈ reps
∧ (↓∃e':{e':E| e' ≤loc e }
∃z1:ℤ
∃z2:Cmd
(((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e')))
∨ ((header(e') = ``new_23_sig vote``)
∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e'))))))
∧ (z2 = (snd(fst(msgval(e')))))))
∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
∧ (((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' and e)
∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
∧ (↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.\000Ce';e)))
∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e))|| = (coeff * flrs))
∧ (d = 0)
∧ (¬((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e)))];snd(fst\000C(msgval(e))))))
= ((coeff * flrs) + 1)))
∧ (i = loc(e))
∧ auth = ff
∧ ((k = (fst(fst(fst(msgval(e)))))) ∧ (k1 = ((snd(fst(fst(msgval(e))))) + 1)))
∧ (v
= (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e)))];snd(fst(\000Cmsgval(e))))))))
∨ (∃e1:{e1:E| e1 ≤loc e }
∃z6:ℤ
∃z7:Cmd
(new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
∧ (((header(e1) = ``new_23_sig retry``)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e1)))
∨ ((header(e1) = ``new_23_sig vote``)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e1))))))
∧ (no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e1 and e)
∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1,\000C z6>;es.e1;e)))
∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e))|| = (coeff * flrs))
∧ (d = 0)
∧ (¬((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];\000Csnd(fst(msgval(e))))))
= ((coeff * flrs) + 1)))
∧ (i = loc(e))
∧ auth = ff
∧ ((k = (fst(fst(fst(msgval(e)))))) ∧ (k1 = ((snd(fst(fst(msgval(e))))) + 1)))
∧ (v
= (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];s\000Cnd(fst(msgval(e)))))))))))))
Lemma: new_23_sig-decided
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k:ℤ]. ∀[v:Cmd].
(<d, i, mk-msg(auth;``new_23_sig decided``;<k, v>)> ∈ new_23_sig_main()(e)
⇐⇒ loc(e) ↓∈ reps
∧ (↓∃e':{e':E| e' ≤loc e }
∃z1:ℤ
∃z2:Cmd
(((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e')))
∨ ((header(e') = ``new_23_sig vote``)
∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
∧ (z1 = (fst(fst(fst(msgval(e'))))))
∧ (z2 = (snd(fst(msgval(e')))))))
∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
∧ (((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' and e)
∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
∧ (↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.\000Ce';e)))
∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e))|| = (coeff * flrs))
∧ (d = 0)
∧ ((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>\000C;es.e';e)))];snd(fst(msgval(e)))))) = ((coeff * flrs) + 1))
∧ i ↓∈ reps
∧ auth = ff
∧ (k = (fst(fst(fst(msgval(e))))))
∧ (v
= (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e)))];snd(fst(\000Cmsgval(e))))))))
∨ (∃e1:{e1:E| e1 ≤loc e }
∃z6:ℤ
∃z7:Cmd
(new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
∧ (((header(e1) = ``new_23_sig retry``)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
∧ (<<z1, z6>, z7> = msgval(e1)))
∨ ((header(e1) = ``new_23_sig vote``)
∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
∧ (<<z1, z6>, z7> = (fst(msgval(e1))))))
∧ (no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e1 and e)
∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1,\000C z6>;es.e1;e)))
∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e))|| = (coeff * flrs))
∧ (d = 0)
∧ ((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];sn\000Cd(fst(msgval(e))))))
= ((coeff * flrs) + 1))
∧ i ↓∈ reps
∧ auth = ff
∧ (k = (fst(fst(fst(msgval(e))))))
∧ (v
= (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) /
(fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];s\000Cnd(fst(msgval(e)))))))))))))
Lemma: new_23_sig-notify
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k:ℤ]. ∀[v:Cmd].
(<d, i, mk-msg(auth;notify;<k, v>)> ∈ new_23_sig_main()(e)
⇐⇒ loc(e) ↓∈ reps
∧ (↓∃z2:Cmd
∃e':{e':E| e' ≤loc e }
((header(e) = ``new_23_sig decided``)
∧ has-es-info-type(es;e;f;ℤ × Cmd)
∧ i ↓∈ clients
∧ (d = 0)
∧ auth = ff
∧ (<k, v> = msgval(e))
∧ (((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<fst(msgval(e)), z2> = msgval(e')))
∨ ((header(e') = ``new_23_sig vote``)
∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
∧ ((fst(msgval(e))) = (fst(fst(fst(msgval(e'))))))
∧ (z2 = (snd(fst(msgval(e')))))))
∧ (¬↑(set-sig-member(slots) (fst(msgval(e))) new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
∧ (no (new_23_sig_decision(Cmd;clients;notify;propose;f)
(fst(msgval(e))) o new_23_sig_decided'base(Cmd;notify;propose;f)) between e' and e))))
Lemma: new_23_sig_replica_state_mem_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀n:ℤ. ∀c:Cmd.
((e1 <loc e2)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
⇒ (↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2))))
Lemma: new_23_sig_rounds_pos_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n:ℤ.
(0 ≤ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e))
Lemma: new_23_sig_rounds_mem_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round:ℤ. ∀cmd:Cmd.
((e1 <loc e2)
⇒ <<n, round>, cmd> ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e1)
⇒ (round ≤ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e2)))
Lemma: new_23_sig_quorum_invariant_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ.
(no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)))
∧ (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
= ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||))
Lemma: new_23_sig_quorum_inv_vote
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀p:Cmd List × (Id List).
(p ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e)
⇒ let cmds,locs = p
in no_repeats(Id;locs)
∧ (||locs|| = ||cmds||)
∧ (∀i:ℕ||locs||
(↓∃e':E. ((e' <loc e) ∧ <<ni, cmds[i]>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')))))
Lemma: new_23_sig_quorum_inv_vote_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||.
(↓∃e':E
((e' <loc e)
∧ <<ni, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]>
, snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]
> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')))
Lemma: new_23_sig_quorum_mem
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀ni:ℤ × ℤ. ∀s1,s2:Cmd List × (Id List). ∀v:ℤ × ℤ × Cmd × Id.
((e1 <loc e2)
⇒ v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
⇒ s1 ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
⇒ s2 ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e2)
⇒ let cmds1,locs1 = s1
in let cmds2,locs2 = s2
in let x,i = v
in let ni',c = x
in (ni = ni') ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2))))
Lemma: new_23_sig_quorum_inv_vote2
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀p:Cmd List × (Id List).
(p ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e)
⇒ let cmds,locs = p
in no_repeats(Id;locs)
∧ (||locs|| = ||cmds||)
∧ (∀i:ℕ||locs||
(↓∃e':E
((e' <loc e)
∧ <<ni, cmds[i]>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
(¬<<ni, c>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(
e'')))))))
Lemma: new_23_sig_quorum_inv_vote2_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ.
(no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)))
∧ (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
= ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||)
∧ (∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
(↓∃e':E
((e' <loc e)
∧ <<ni, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]>
, snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]
> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
(¬<<ni, c>, snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]> ∈
new_23_sig_vote'base(Cmd;notify;propose;f)(e'')))))))
Lemma: new_23_sig_replica_state_from_proposal
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀slots:set-sig{i:l}(ℤ). ∀s:set-sig-set(slots).
(s ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e)
⇒ (∀n:ℤ
((↑(set-sig-member(slots) n s))
⇒ (∃e':E
∃c:Cmd
((e' <loc e)
∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))))
Lemma: new_23_sig_replica_state_from_proposal_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀slots:set-sig{i:l}(ℤ). ∀n:ℤ.
((↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (∃e':E
∃c:Cmd
((e' <loc e)
∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))
Lemma: new_23_sig_voter_start_unique
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀n:ℤ. ∀e1,e2:E. ∀c1,c2:Cmd.
((¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1)))
⇒ <n, c1> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2)))
⇒ <n, c2> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e2)
⇒ (loc(e1) = loc(e2))
⇒ (e1 = e2))
Lemma: new_23_sig_votes_consistent
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
(eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)
⇒ (∀e1,e2:E. ∀n,r:ℤ. ∀sender,l1,l2:Id. ∀c1,c2:Cmd. ∀d1,d2:ℤ.
(<d1, l1, make-Msg(``new_23_sig vote``;<<<n, r>, c1>, sender>)> ∈ new_23_sig_main()(e1)
⇒ <d2, l2, make-Msg(``new_23_sig vote``;<<<n, r>, c2>, sender>)> ∈ new_23_sig_main()(e2)
⇒ (c1 = c2))))
Lemma: new_23_sig_assert_newvote
∀[Cmd:ValueAllType]
∀ni:ℤ × ℤ. ∀vote:ℤ × ℤ × Cmd × Id. ∀quorum:Cmd List × (Id List).
(↑(new_23_sig_newvote(Cmd) ni vote quorum) ⇐⇒ (ni = (fst(fst(vote)))) ∧ (¬(snd(vote) ∈ snd(quorum))))
Lemma: new_23_sig_decided_property
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℤ]. ∀[propose,notify:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
(eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)
⇒ (∀e:E. ∀c:Cmd. ∀n:ℤ.
(<n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
⇒ (↓∃x:Id
∃rnd:ℕ
∃L:Id List
(no_repeats(Id;L)
∧ (||L|| = ((coeff * flrs) + 1))
∧ (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c>, vtr>)) ∈ new_23_sig_ma\000Cin()(e')))))))
Lemma: new_23_sig_retry_property
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℕ]. ∀[propose,notify:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
(eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)
⇒ (∀e:E. ∀c:Cmd. ∀n,r:ℤ.
(<<n, r + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)
⇒ (↓∃x:Id
∃cs:Cmd List+
∃L:Id List
((no_repeats(Id;L) ∧ (||L|| = ((coeff * flrs) + 1)) ∧ (||cs|| = ||L||))
∧ (∀i:ℕ||L||. ((↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, r>, cs[i]>, L[i]>)) ∈ new_\000C23_sig_main()(e')) ∧ L[i] ↓∈ reps))
∧ (c = (snd(poss-maj(eq;cs;hd(cs))))))))))
Lemma: new_23_sig_proposal_classrel
∀[Cmd:ValueAllType]
∀propose:Atom List
∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀es:EO+(Message(f)). ∀e:E.
∀[nc:ℤ × Cmd]
uiff(nc ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e);nc ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e)
∨ nc ∈ (new_23_sig_vote2prop(Cmd) o new_23_sig_vote'base(Cmd;notify;propose;f))(e))
Lemma: new_23_sig_proposal_classrel2
∀[Cmd:ValueAllType]
∀propose:Atom List
∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀es:EO+(Message(f)). ∀e:E.
∀[nc:ℤ × Cmd]
uiff(nc ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e);((header(e) = propose) ∧ nc = body(e))
∨ (has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
∧ (header(e) = ``new_23_sig vote``)
∧ ((fst(nc)) = (fst(fst(fst(msgval(e))))))
∧ ((snd(nc)) = (snd(fst(msgval(e)))))))
Lemma: new_23_sig_proposal_if_vote
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[r:ℤ]. ∀[i:Id].
<n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
supposing <<<n, r>, c>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
Lemma: new_23_sig_proposal_has_header
∀[Cmd:ValueAllType]
∀propose:Atom List
∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀es:EO+(Message(f)). ∀e:E.
∀[nc:ℤ × Cmd]
(header(e) = propose) ∨ (header(e) = ``new_23_sig vote``)
supposing nc ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
Lemma: new_23_sig_round_info_classrel2
∀[Cmd:ValueAllType]
∀propose:Atom List
∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀es:EO+(Message(f)). ∀e:E.
∀[nrc:ℤ × ℤ × Cmd]
uiff(nrc ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e);((header(e) = ``new_23_sig retry``) ∧ nrc = body(e))
∨ (has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
∧ (header(e) = ``new_23_sig vote``)
∧ ((fst(fst(nrc))) = (fst(fst(fst(msgval(e))))))
∧ ((snd(fst(nrc))) = (snd(fst(fst(msgval(e))))))
∧ ((snd(nrc)) = (snd(fst(msgval(e)))))))
Lemma: new_23_sig_quorum_state_fun_eq
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀nr:ℤ × ℤ.
(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;nr;es;e)
= if first(e) then <[], []>
if pred(e) ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
then new_23_sig_add_to_quorum(Cmd) nr loc(e) new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e)
new_23_sig_QuorumStateFun(Cmd;notify;propose;f;nr;es;pred(e))
else new_23_sig_QuorumStateFun(Cmd;notify;propose;f;nr;es;pred(e))
fi )
Lemma: new_23_sig_RoundInfo-single-val
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))].
single-valued-classrel(es;new_23_sig_RoundInfo(Cmd;notify;propose;f);ℤ × ℤ × Cmd)
Lemma: new_23_sig_agreement
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))].
(eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ any v1,v2 from new_23_sig_decided'base(Cmd;notify;propose;f) satisfy
((fst(v1)) = (fst(v2))) ⇒ ((snd(v1)) = (snd(v2))))
Lemma: new_23_sig_validity
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))].
(eo-msg-interface-constraint(es;new_23_sig_main();new_23_sig_headers_internal();f)
⇒ for every p1 in new_23_sig_decided'base(Cmd;notify;propose;f) there is an
earlier event with info=m such that
(msg-header(m) = propose) ∧ (p1 = msg-body(m)))
Definition: new_23_sig_vote_with_ballot
new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) ==
e ∈b new_23_sig_vote'base(Cmd;notify;propose;f) ∧b (fst(fst(fst(msgval(e)))) =z n) ∧b (snd(fst(fst(msgval(e)))) =z r)
Lemma: new_23_sig_vote_with_ballot_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
(new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) ∈ 𝔹)
Lemma: new_23_sig_vote_with_ballot-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id) supposing ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
Lemma: new_23_sig_vote_with_ballot-assert-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
<<<n, r>, snd(fst(msgval(e)))>, snd(msgval(e))> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
supposing ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
Lemma: new_23_sig_vote_with_ballot-header
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
header(e) = ``new_23_sig vote`` supposing ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
Lemma: new_23_sig_vote_with_ballot-if-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[i:Id].
↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
supposing <<<n, r>, c>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
Lemma: new_23_sig_vote_with_ballot-forward
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[start:E]. ∀[Cmd,propose,notify,e,n,r:Top].
(new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es.start;e;n;r)
~ new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))
Definition: new_23_sig_vote_with_ballot_and_id
new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i) ==
e ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
∧b (fst(fst(fst(msgval(e)))) =z n)
∧b (snd(fst(fst(msgval(e)))) =z r)
∧b snd(msgval(e)) = i
Lemma: new_23_sig_vote_with_ballot_and_id_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
(new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i) ∈ 𝔹)
Lemma: new_23_sig_vote_with_ballot_and_id-implies
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)
Lemma: new_23_sig_vote_with_ballot_and_id-if-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[i:Id].
↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)
supposing <<<n, r>, c>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
Lemma: new_23_sig_vote_with_ballot_and_id-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)
Lemma: new_23_sig_vote_with_ballot_and_id-assert-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
<<<n, r>, snd(fst(msgval(e)))>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)
Lemma: new_23_sig_vote_with_ballot_and_id-snd
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
(snd(msgval(e))) = i supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)
Lemma: new_23_sig_vote_with_ballot_and_id-if-snd
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
(↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)) supposing
(((snd(msgval(e))) = i) and
(↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)))
Lemma: new_23_sig_vote_with_ballot_and_id-forward
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[start:E]. ∀[Cmd,propose,notify,e,n,r,i:Top].
(new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es.start;e;n;r;i)
~ new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i))
Definition: new_23_sig_vote_with_ballot_first
new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r) ==
new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
∧b (∀e'∈[es-init(es;e);e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b
Lemma: new_23_sig_vote_with_ballot_first_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
(new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r) ∈ 𝔹)
Lemma: new_23_sig_vote_with_ballot_first-assert
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
supposing ↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)
Lemma: new_23_sig_vote_with_ballot_first-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id) supposing ↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)
Definition: new_23_sig_commands_from_votes
new_23_sig_commands_from_votes(Cmd;notify;propose;f;es;e;e';n;r) ==
mapfilter(λe.(snd(fst(msgval(e))));λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;r);[e, e'])
Lemma: new_23_sig_commands_from_votes_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':{e':E| e ≤loc e' } ]. ∀[n,r:ℤ].
(new_23_sig_commands_from_votes(Cmd;notify;propose;f;es;e;e';n;r) ∈ Cmd List)
Lemma: new_23_sig_vote_with_ballot_first-not
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n,r:ℤ.
((∃e'∈[es-init(es;e);e). ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(...)))) supposing
((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and
(↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)))
Lemma: new_23_sig_vote_with_ballot_first-not2
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n,r:ℤ. ∀i:Id.
((∃e'∈[es-init(es;e);e). (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;i))
∧ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e';n;r)))) supposing
((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and
(↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)))
Lemma: new_23_sig_vote_with_ballot_first-forward
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
(start ≤loc e
⇒ (new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r)
~ new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
∧b (∀e'∈[start;e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b))
Lemma: new_23_sig_vote_with_ballot_first-assert-forward
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
(start ≤loc e
⇒ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r)
⇐⇒ (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))
∧ (↑(∀e'∈[start;e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b)))
Lemma: new_23_sig_vote_with_ballot_first-assert-forward2
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
(start ≤loc e
⇒ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r)
⇐⇒ (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))
∧ (∀e'∈[start;e).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))))
Definition: new_23_sig_vote_with_ballot_first_alt
new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;r;a) ==
new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;a;n;r)
∧b (¬b(∃x∈[e, e'].new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;r)
∧b es-blocl(es;x;a)
∧b (IdDeq (snd(msgval(x))) (snd(msgval(a)))))_b)
Lemma: new_23_sig_vote_with_ballot_first_alt_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e,e':E]. ∀[n,r:ℤ]. ∀[a:E].
(new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;r;a) ∈ 𝔹)
Definition: new_23_sig_decided_with_id
new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n) ==
e ∈b new_23_sig_decided'base(Cmd;notify;propose;f) ∧b (fst(msgval(e)) =z n)
Lemma: new_23_sig_decided_with_id_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ].
(new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n) ∈ 𝔹)
Lemma: new_23_sig_decided_with_id-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ].
has-es-info-type(es;e;f;ℤ × Cmd) supposing ↑new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n)
Lemma: new_23_sig_decided_with_id-assert-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ].
<n, snd(msgval(e))> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
supposing ↑new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n)
Lemma: new_23_sig_quorum_state_eq1
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n,r:ℤ.
(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es;e)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
[es-init(es;e);e)))
>)
Lemma: new_23_sig_quorum_state_eq1-forward
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
(start ≤loc e
⇒ (new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es.start;e)
= <rev(mapfilter(λe.(snd(fst(msgval(e))));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[start;e)))
, rev(mapfilter(λe.(snd(msgval(e)));
λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
[start;e)))
>))
Lemma: new_23_sig_voter_start
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd].
(<n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (↓∃e':E
∃c':Cmd
(e' ≤loc e
∧ <n, c'> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))
Lemma: filter-vote-with-ballot-lemma
∀Cmd:{T:Type| valueall-type(T)} . ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose).
∀es:EO+(Message(f)). ∀e:E. ∀n:ℤ. ∀e':E.
(filter(λa.new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;0;a);[e, e'])
~ filter(λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0);[e, e']))
Lemma: new_23_sig_progress-step1
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ b_all(Id;reps;i.mk-msg-interface(i;make-Msg(``new_23_sig vote``;<<<n, 0>, c>, loc(e)>)) ∈ new_23_sig_main()(e)))
Lemma: new_23_sig_progress-step2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ b_all(Id;reps;i.↓∃e':E
((e < e')
∧ (loc(e') = i)
∧ <<<n, 0>, c>, loc(e)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e'))))
Lemma: new_23_sig_progress-step3
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ b_all(Id;reps;i.↓∃e':E
∃c':Cmd. ((loc(e') = i) ∧ mk-msg-interface(loc(e);make-Msg(``new_23_sig vote``;<<<n, 0>, c'>, i>)\000C) ∈ new_23_sig_main()(e'))))
Lemma: new_23_sig_progress-step4
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ b_all(Id;[x∈reps|¬bbag-deq-member(IdDeq;x;faulty)];i.↓∃e':E
∃c':Cmd
((loc(e') = loc(e))
∧ <<<n, 0>, c'>, i> ∈
new_23_sig_vote'base(Cmd;notify;propose;f)(e'))))
Lemma: new_23_sig_progress-step5
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃bs:(Id × E × Cmd) List
((bag-map(λi.(fst(i));bs) = [x∈reps|¬bbag-deq-member(IdDeq;x;faulty)])
∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x)))))))
Lemma: new_23_sig_progress-step6
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃bs:(Id × E × Cmd) List
((bag-map(λi.(fst(i));bs) = [x∈reps|¬bbag-deq-member(IdDeq;x;faulty)])
∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs))))
Lemma: new_23_sig_progress-step7
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃bs:(Id × E × Cmd) List
((bag-map(λi.(fst(i));bs) = [x∈reps|¬bbag-deq-member(IdDeq;x;faulty)])
∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
∧ (∀x∈bs.e ≤loc fst(snd(x)) )
∧ (((coeff * flrs) + 1) ≤ ||bs||))))
Lemma: new_23_sig_progress-step8
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃bs:(Id × E × Cmd) List
((((coeff * flrs) + 1) ≤ ||bs||)
∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
∧ e ≤loc fst(snd(x))
∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
∧ (∀e'∈[e, fst(snd(last(bs)))].(↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e';n;0))
⇒ (e' ∈ map(λx.(fst(snd(x)));bs)))
∧ b_all(Id;[x∈reps|¬bbag-deq-member(IdDeq;x;faulty)];i.(i ∈ map(λi.(fst(i));bs))))))
Lemma: new_23_sig_progress-step8-v2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃bs:(Id × E × Cmd) List
((((coeff * flrs) + 1) ≤ ||bs||)
∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
∧ e ≤loc fst(snd(x))
∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
∧ (∀e'∈[e, fst(snd(last(bs)))].(↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e';n;0))
⇒ (e' ∈ map(λx.(fst(snd(x)));bs)))
∧ b_all(Id;[x∈reps|¬bbag-deq-member(IdDeq;x;faulty)];i.(i ∈ map(λi.(fst(i));bs)))
∧ (bs
= mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
λe.new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;0);
[e, fst(snd(last(bs)))])))))
Lemma: new_23_sig_progress-step8-v3
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃e':E
(b_all(Id;[x∈reps|
¬bbag-deq-member(IdDeq;x;faulty)];i.(i
∈ mapfilter(λe.(snd(msgval(e)));
λe....;
[e, e'])))
∧ (((coeff * flrs) + 1) ≤ ||mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
λe.new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;0);
[e, e'])||))))
Lemma: new_23_sig_progress-step9
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃bs:(Id × E × Cmd) List
((((coeff * flrs) + 1) = ||bs||)
∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
∧ e ≤loc fst(snd(x))
∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x)))
∧ (∀e'∈[e;fst(snd(x))).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;fst(x))))
∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
∧ (∀e'∈[e, fst(snd(last(bs)))].
∀i:Id
((↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;i))
⇒ (∀e''∈[e;e').¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e'';n;0;i))
⇒ (e' ∈ map(λx.(fst(snd(x)));bs))))
∧ no_repeats(Id;map(λx.(fst(x));bs)))))
Lemma: new_23_sig_progress-step9-v2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃e':E
(((coeff * flrs) + 1)
= ||mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0);
[e, e'])||)))
Lemma: new_23_sig_progress-step9-v3
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃e':E
((((coeff * flrs) + 1)
= ||mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0);
[e, e'])||)
∧ e ≤loc e'
∧ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0)))))
Lemma: new_23_sig_progress-step10
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃e':E
∃c':Cmd
((e <loc e')
∧ (<n, c'> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e')
∨ (∃r:ℕ+. <<n, r>, c'> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e'))))))
Lemma: new_23_sig_progress1
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
⇒ (↓∃e':E
∃c':Cmd
((e <loc e')
∧ (<n, c'> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e')
∨ (∃r:ℕ+. <<n, r>, c'> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e'))))))
Lemma: new_23_sig_progress2-step1
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)]. ∀[e':E]. ∀[c':Cmd].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ (e' ≤loc e
∧ <n, c'> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e))
⇒ <<n, r>, c> ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
⇒ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e) < r
⇒ b_all(Id;reps;i.mk-msg-interface(i;make-Msg(``new_23_sig vote``;<<<n, r>, c>, loc(e)>)) ∈ new_23_sig_main()(e)))
Lemma: new_23_sig_progress2-step2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)]. ∀[e':E]. ∀[c':Cmd].
(msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
⇒ bag-no-repeats(Id;reps)
⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
⇒ loc(e) ↓∈ reps
⇒ (¬loc(e) ↓∈ faulty)
⇒ (e' ≤loc e
∧ <n, c'> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e))
⇒ <<n, r>, c> ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
⇒ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e) < r
⇒ b_all(Id;reps;i.↓∃e1:E
((e < e1)
∧ (loc(e1) = i)
∧ <<<n, r>, c>, loc(e)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1))))
Home
Index