Definition: mData
mData == T:Type × T
Lemma: mData_wf
mData ∈ 𝕌'
Lemma: mData-examples
(<ℤ, 33> ∈ mData) ∧ (<𝔹, tt> ∈ mData) ∧ (<ℤ ⟶ ℤ, λx.(x + 1)> ∈ mData) ∧ (<ℤ × 𝔹, 33, ff> ∈ mData)
Definition: mdata-type
mdata-type(mdata) == fst(mdata)
Lemma: mdata-type_wf
∀[mdata:mData]. (mdata-type(mdata) ∈ Type)
Definition: mdata-val
mdata-val(mdata) == snd(mdata)
Lemma: mdata-val_wf
∀[mdata:mData]. (mdata-val(mdata) ∈ mdata-type(mdata))
Definition: header-type-spec
header-type-spec{i:l}(L;g) == {f:Name ⟶ ValueAllType| no_repeats(Name;L) ∧ (∀hdr∈L.(f hdr) = (g hdr) ∈ Type)}
Lemma: header-type-spec_wf
∀[L:Name List]. ∀[g:Name ⟶ Type]. (header-type-spec{i:l}(L;g) ∈ 𝕌')
Lemma: subtype_rel_header-type-spec
∀[L:Name List]. ∀[g:Name ⟶ Type]. (header-type-spec{i:l}(L;g) ⊆r header-type-spec{i':l}(L; g))
Definition: basicMessage
A basic message is a header and a value whose type depends on the header.⋅
basicMessage(f) == h:Name × (f h)
Lemma: basicMessage_wf
∀[f:Name ⟶ Type]. (basicMessage(f) ∈ Type)
Definition: make-basicMsg
make-basicMsg(hdr;val) == <hdr, val>
Lemma: make-basicMsg_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[val:f hdr]. (make-basicMsg(hdr;val) ∈ basicMessage(f))
Definition: Message
A message is a basic message together with a boolean that indicates
whether the basic message was authenticated or not.⋅
Message(f) == 𝔹 × basicMessage(f)
Lemma: Message_wf
∀[f:Name ⟶ Type]. (Message(f) ∈ Type)
Lemma: basicMessage-valueall-type
∀[f:Name ⟶ ValueAllType]. valueall-type(basicMessage(f))
Lemma: Message-valueall-type
∀[f:Name ⟶ ValueAllType]. valueall-type(Message(f))
Definition: msg-authentic
msg-authentic(m) == fst(m)
Lemma: msg-authentic_wf
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. (msg-authentic(m) ∈ 𝔹)
Definition: msg-msg
msg-msg(m) == snd(m)
Lemma: msg-msg_wf
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. (msg-msg(m) ∈ basicMessage(f))
Definition: msg-header
msg-header(m) == fst(msg-msg(m))
Lemma: msg-header_wf
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. (msg-header(m) ∈ Name)
Definition: msg-mdata
msg-mdata(f;msg) == let hdr,val = msg-msg(msg) in <f hdr, val>
Lemma: msg-mdata_wf
∀[f:Name ⟶ Type]. ∀[msg:Message(f)]. (msg-mdata(f;msg) ∈ mData)
Definition: msg-type
msg-type(msg;f) == f msg-header(msg)
Lemma: msg-type_wf
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. (msg-type(m;f) ∈ Type)
Lemma: msg-type_wf2
∀[f:Name ⟶ ValueAllType]. ∀[m:Message(f)]. (msg-type(m;f) ∈ {T:Type| valueall-type(T)} )
Definition: msg-has-type
msg-has-type(m;f;T) == msg-type(m;f) ⊆r T
Lemma: msg-has-type_wf
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. ∀[T:Type]. (msg-has-type(m;f;T) ∈ ℙ)
Definition: msg-body
msg-body(msg) == snd(msg-msg(msg))
Lemma: msg-body_wf2
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. ∀[T:Type]. msg-body(m) ∈ T supposing msg-type(m;f) ⊆r T
Lemma: msg-body_wf
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. (msg-body(m) ∈ msg-type(m;f))
Lemma: Message-extensionality
∀[f:Name ⟶ Type]. ∀[m1,m2:Message(f)].
uiff(m1 = m2 ∈ Message(f);msg-authentic(m1) = msg-authentic(m2)
∧ (msg-header(m1) = msg-header(m2) ∈ Name)
∧ (msg-body(m1) = msg-body(m2) ∈ (f msg-header(m1))))
Lemma: eclass_wf2
∀[f:Name ⟶ Type]. ∀[T:𝕌']. (EClass(T) ∈ 𝕌{i''})
Lemma: eclass_wf3
∀[f:Name ⟶ Type]. ∀[T:Type]. (EClass(T) ∈ 𝕌')
Definition: es-authentic
es-authentic(es;e) == msg-authentic(info(e))
Lemma: es-authentic_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. (es-authentic(es;e) ∈ 𝔹)
Definition: es-header
header(e) == msg-header(info(e))
Lemma: es-header_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. (header(e) ∈ Name)
Definition: es-info-type
es-info-type(es;e;f) == msg-type(info(e);f)
Lemma: es-info-type_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. (es-info-type(es;e;f) ∈ Type)
Definition: has-es-info-type
has-es-info-type(es;e;f;T) == es-info-type(es;e;f) ⊆r T
Lemma: has-es-info-type_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type]. (has-es-info-type(es;e;f;T) ∈ Type)
Lemma: eo-forward-has-es-info-type
∀[f,es,e',e,T:Top]. (has-es-info-type(es.e';e;f;T) ~ has-es-info-type(es;e;f;T))
Lemma: has-es-info-type-is-msg-has-type
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type]. (has-es-info-type(es;e;f;T) ~ msg-has-type(info(e);f;T))
Lemma: has-es-info-type-subtype
∀[T,U:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].
(has-es-info-type(es;e;f;T)) supposing (has-es-info-type(es;e;f;U) and (U ⊆r T))
Lemma: sq_stable__has-es-info-type
∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. SqStable(has-es-info-type(es;e;f;T))
Lemma: eo-forward-info-type
∀[f,es,e,e':Top]. (es-info-type(es.e;e';f) ~ es-info-type(es;e';f))
Lemma: eo-forward-header
∀[es,e,e':Top]. (header(e') ~ header(e'))
Definition: es-info-body
msgval(e) == msg-body(info(e))
Lemma: es-info-body_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. (msgval(e) ∈ es-info-type(es;e;f))
Lemma: es-info-body-equal
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e,e':E]. ∀[T:Type].
(msgval(e) = msgval(e') ∈ T) supposing ((e = e' ∈ E) and ((f header(e)) ⊆r T))
Lemma: es-info-type-implies
∀[f:Name ⟶ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. (has-es-info-type(es;e;f;T) ⇒ (msgval(e) ∈ T))
Lemma: eo-forward-info-body
∀[es,e,e':Top]. (msgval(e') ~ msgval(e'))
Definition: equal-info-body
v = body(e) == has-es-info-type(es;e;f;T) ∧ (v = msgval(e) ∈ T)
Lemma: equal-info-body_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type]. ∀[v:T]. (v = body(e) ∈ ℙ)
Lemma: sq_stable__equal-info-body
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type]. ∀[v:T]. SqStable(v = body(e))
Lemma: eo-forward-equal-info-body
∀[f,es,T,e,e',v:Top]. (v = body(e) ~ v = body(e))
Lemma: trivial-equal-info-body
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type].
uiff(msgval(e) = body(e);True) supposing has-es-info-type(es;e;f;T)
Definition: es-info-auth
es-info-auth(es;e) == msg-authentic(info(e))
Lemma: es-info-auth_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. (es-info-auth(es;e) ∈ 𝔹)
Definition: encodes-msg-type
hdr encodes T == (f hdr) ⊆r T
Lemma: encodes-msg-type_wf
∀[hdr:Name]. ∀[f:Name ⟶ Type]. ∀[T:Type]. (hdr encodes T ∈ Type)
Lemma: encodes-msg-type-trivial
∀[f:Name ⟶ Type]. ∀[hdr:Name]. hdr encodes f hdr
Lemma: msg-has-type-encodes
∀[f,m,T:Top]. (msg-has-type(m;f;T) ~ msg-header(m) encodes T)
Lemma: sq_stable__encodes-msg-type
∀[f:Name ⟶ Type]. ∀[h:Name]. ∀[T:Type]. SqStable(h encodes T)
Definition: get-mdata
get-mdata(f;msg;hdr) == if name_eq(msg-header(msg);hdr) then {msg-mdata(f;msg)} else {} fi
Lemma: get-mdata_wf
∀[f:Name ⟶ Type]. ∀[msg:Message(f)]. ∀[hdr:Name]. (get-mdata(f;msg;hdr) ∈ bag(mData))
Definition: mdata-class
mdata-class(f;hdr) == λes,e. get-mdata(f;info(e);hdr)
Lemma: mdata-class_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. (mdata-class(f;hdr) ∈ EClass(mData))
Definition: cond-msg-body
cond-msg-body(hdr;msg) == if name_eq(msg-header(msg);hdr) then {msg-body(msg)} else {} fi
Lemma: cond-msg-body_wf
∀[f:Name ⟶ Type]. ∀[T:Type]. ∀[hdr:Name]. ∀[m:Message(f)]. cond-msg-body(hdr;m) ∈ bag(T) supposing hdr encodes T
Lemma: map-cond-msg-body
∀[g,hdr,m:Top]. (map(g;cond-msg-body(hdr;m)) ~ if name_eq(msg-header(m);hdr) then {g msg-body(m)} else {} fi )
Lemma: cond-msg-body-cbva
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[msg:Message(f)]. ∀[G:Top].
let x ⟵ cond-msg-body(hdr;msg) in G[x] ~ G[cond-msg-body(hdr;msg)] supposing valueall-type(f hdr)
Lemma: cond-msg-body-single-valued
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[m:Message(f)]. ∀[T:Type].
single-valued-bag(cond-msg-body(hdr;m);T) supposing hdr encodes T
Lemma: cond-msg-body-sv-bag-only
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type].
(sv-bag-only(cond-msg-body(hdr;info(e))) ∈ T) supposing ((header(e) = hdr ∈ Name) and hdr encodes T)
Definition: base-headers-msg-val
Base(hdr) == λes,e. cond-msg-body(hdr;info(e))
Lemma: base-headers-msg-val_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type]. Base(hdr) ∈ EClass(T) supposing hdr encodes T
Lemma: base-headers-msg-val-es-sv
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. es-sv-class(es;Base(hdr))
Lemma: base-headers-msg-val-single-val
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[T:Type].
single-valued-classrel(es;Base(hdr);T) supposing hdr encodes T
Definition: test-msg-header-and-loc
test-msg-header-and-loc(msg;hdr;loc) == name_eq(msg-header(msg);hdr) ∧b loc = fst(msg-body(msg))
Lemma: test-msg-header-and-loc_wf
∀[f:Name ⟶ Type]. ∀[msg:Message(f)]. ∀[hdr:Name]. ∀[loc:Id].
test-msg-header-and-loc(msg;hdr;loc) ∈ 𝔹 supposing hdr encodes Id × Top
Lemma: assert-test-msg-header-and-loc
∀[f:Name ⟶ Type]
∀msg:Message(f). ∀hdr:Name. ∀loc:Id.
uiff(↑test-msg-header-and-loc(msg;hdr;loc);(msg-header(msg) = hdr ∈ Name) ∧ (loc = (fst(msg-body(msg))) ∈ Id))
supposing hdr encodes Id × Top
Definition: base-process-inputs
The base-process-inputs (upto to event e) are the list of m:Info
for which a message ⌜<hdr, loc, m>⌝ has been received ⌜≤loc(e)⌝.
(For this to be well-formed, the header hdr must encode the type
⌜Id × Info⌝). ⋅
base-process-inputs(loc;hdr;es;e) ==
map(λmsg.(snd(msg-body(msg)));filter(λmsg.test-msg-header-and-loc(msg;hdr;loc);map(λe.info(e);≤loc(e))))
Lemma: base-process-inputs_wf
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
∀[es:EO+(Message(f))]. ∀[e:E]. (base-process-inputs(loc;hdr;es;e) ∈ Info List) supposing hdr encodes Id × Info
Lemma: base-process-inputs-non-null
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
∀[es:EO+(Message(f))]. ∀[e:E].
0 < ||base-process-inputs(loc;hdr;es;e)|| supposing ↑test-msg-header-and-loc(info(e);hdr;loc)
supposing hdr encodes Id × Info
Definition: base-process-class
The base-process-class does (at any location) what class X does
at location loc in the event ordering with only the events
in the base-process-inputs(loc;hdr;es;e)⋅
base-process-class(X;loc;hdr) ==
λes,e. if test-msg-header-and-loc(info(e);hdr;loc)
then let Infos = base-process-inputs(loc;hdr;es;e) in
X list-eo(Infos;loc) (||Infos|| - 1)
else {}
fi
Lemma: base-process-class_wf
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
base-process-class(X;loc;hdr) ∈ EClass(T) supposing hdr encodes Id × Info
Comment: parallel composition of base-process-class
The `base-process-class` ⌜base-process-class(X;i;hdr)⌝ runs the program
for X at location i on just those messages m for which it receives a message
⌜<hdr, i, m>⌝.
The parallel composition ⌜(||i∈locs.base-process-class(X;i;hdr))⌝
will then simulate the class X at all the locations in locs
on reciept of ⌜<hdr, i, m>⌝ messages.
So we define ⌜local-simulation-class(X;locs;hdr)⌝ = ⌜(||i∈locs.base-process-class(X;i;hdr))⌝.
Given any event e, the inputs to the simulation of class X upto and including e
will be the list
⌜local-simulation-inputs(es;e;hdr;locs) ==
mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e)))⌝
and this defines a `global ordering` of events
from which we can construct an event ordering
local-simulation-eo(es;e;hdr;locs) == global-eo(local-simulation-inputs(es;e;hdr;locs))
.
If ⌜↑has-header-and-in-locs(info(e);hdr;locs)⌝ then event e corresponds to an event
⌜local-simulation-event(es;e;hdr;locs)⌝ in the ⌜local-simulation-eo(es;e;hdr;locs)⌝,
and the output of the ⌜local-simulation-class(X;locs;hdr)⌝ at event e will be the
output of the class X at that corresponding event in ⌜local-simulation-eo(es;e;hdr;locs)⌝
Thus the `classrel` for ⌜local-simulation-class(X;locs;hdr)⌝ should be
⌜v ∈ local-simulation-class(X;locs;hdr)(e)
⇐⇒ has-header-and-in-locs(info(e);hdr;locs) ∧ v ∈ X(local-simulation-eo(es;e;hdr;locs))⌝.
⋅
Definition: local-simulation-class
A local simulation of class X for a given (bag of) locs is the parallel
composition of the base-process-class for X at each of the locs.
The classrel lemma is: Error :local-simulation-classrel⋅
local-simulation-class(X;locs;hdr) == (||i∈locs.base-process-class(X;i;hdr))
Lemma: local-simulation-class_wf
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[locs:bag(Id)]. ∀[hdr:Name].
local-simulation-class(X;locs;hdr) ∈ EClass(T) supposing hdr encodes Id × Info
Definition: has-header-and-in-locs
has-header-and-in-locs(msg;hdr;locs) == name_eq(msg-header(msg);hdr) ∧b bag-deq-member(IdDeq;fst(msg-body(msg));locs)
Lemma: has-header-and-in-locs_wf
∀[f:Name ⟶ Type]. ∀[msg:Message(f)]. ∀[hdr:Name]. ∀[locs:bag(Id)].
has-header-and-in-locs(msg;hdr;locs) ∈ 𝔹 supposing hdr encodes Id × Top
Lemma: assert-has-header-and-in-locs
∀[f:Name ⟶ Type]
∀msg:Message(f). ∀hdr:Name. ∀locs:bag(Id).
↑has-header-and-in-locs(msg;hdr;locs) ⇐⇒ (msg-header(msg) = hdr ∈ Name) ∧ fst(msg-body(msg)) ↓∈ locs
supposing hdr encodes Id × Top
Definition: local-simulation-inputs
local-simulation-inputs(es;e;hdr;locs) ==
mapfilter(λm.msg-body(m);λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e)))
Lemma: local-simulation-inputs_wf
∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs} × Info) List) supposing hdr encodes Id × Info
Lemma: member-local-simulation-inputs
∀f:Name ⟶ Type
∀[Info:Type]
∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
∀e:E. ∀v:Id × Info.
((v ∈ local-simulation-inputs(es;e;hdr;locs))
⇐⇒ ∃e':E
(e' ≤loc e
∧ (msg-header(info(e')) = hdr ∈ Name)
∧ fst(v) ↓∈ locs
∧ (v = msg-body(info(e')) ∈ (Id × Info))))
supposing hdr encodes Id × Info
Lemma: iseg-local-simulation-inputs
∀f:Name ⟶ Type
∀[Info:Type]
∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
∀e1,e2:E. (e1 ≤loc e2 ⇒ local-simulation-inputs(es;e1;hdr;locs) ≤ local-simulation-inputs(es;e2;hdr;locs))
supposing hdr encodes Id × Info
Definition: local-simulation-eo
local-simulation-eo(es;e;hdr;locs) == global-eo(local-simulation-inputs(es;e;hdr;locs))
Lemma: local-simulation-eo_wf
∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[e:E]. (local-simulation-eo(es;e;hdr;locs) ∈ EO+(Info)) supposing hdr encodes Id × Info
Lemma: local-simulation-eo-loc
∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[e:E]. ∀[e1:E]. loc(e1) ↓∈ locs supposing hdr encodes Id × Info
Lemma: local-simulation-E-subtype
∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[e1,e2:E]. (e1 ≤loc e2 ⇒ (E ⊆r E)) supposing hdr encodes Id × Info
Lemma: local-simulation-embedding
∀f:Name ⟶ Type
∀[Info:Type]
∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
∀e1,e2:E.
(e1 ≤loc e2 ⇒ (λx.x embeds local-simulation-eo(es;e1;hdr;locs) into local-simulation-eo(es;e2;hdr;locs)))
supposing hdr encodes Id × Info
Definition: local-simulation-event
local-simulation-event(es;e;hdr;locs) == ||filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);before(e)))||
Lemma: local-simulation-event_wf
∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[e:E]. local-simulation-event(es;e;hdr;locs) ∈ E supposing ↑has-header-and-in-locs(info(e);hdr;locs)
supposing hdr encodes Id × Info
Lemma: local-simulation-event-loc
∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[e:E]
loc(local-simulation-event(es;e;hdr;locs)) = (fst(msg-body(info(e)))) ∈ Id
supposing ↑has-header-and-in-locs(info(e);hdr;locs)
supposing hdr encodes Id × Info
Lemma: local-simulation-event-info
∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[e:E]
info(local-simulation-event(es;e;hdr;locs)) = (snd(msg-body(info(e)))) ∈ Info
supposing ↑has-header-and-in-locs(info(e);hdr;locs)
supposing hdr encodes Id × Info
Definition: typed-base-class
Base(hdr;T) == Base(hdr)
Lemma: typed-base-class_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type]. Base(hdr;T) ∈ EClass(T) supposing hdr encodes T
Definition: cond-verify-msg-body
cond-verify-msg-body(hdr;msg) == if msg-authentic(msg) then cond-msg-body(hdr;msg) else {} fi
Lemma: cond-verify-msg-body_wf
∀[f:Name ⟶ Type]. ∀[T:Type]. ∀[hdr:Name]. ∀[msg:Message(f)].
cond-verify-msg-body(hdr;msg) ∈ bag(T) supposing hdr encodes T
Definition: verify-class
Verify(hdr) == λes,e. cond-verify-msg-body(hdr;info(e))
Lemma: verify-class_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type]. Verify(hdr) ∈ EClass(T) supposing hdr encodes T
Definition: base-headers-msg-val-loc
Base(hdr;locs) == Base(hdr)@locs
Lemma: base-headers-msg-val-loc_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[locs:bag(Id)]. ∀[T:Type]. Base(hdr;locs) ∈ EClass(T) supposing hdr encodes T
Lemma: eo-forward-base-classrel
∀[f:Name ⟶ Type]. ∀[eo:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type]. ∀[v:T].
uiff(v ∈ Base(hdr)(e');v ∈ Base(hdr)(e')) supposing hdr encodes T
Lemma: eo-forward-base-classfun
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
(Base(hdr)(e') = Base(hdr)(e') ∈ T) supposing ((header(e') = hdr ∈ Name) and hdr encodes T)
Lemma: eo-forward-base-classfun-sq
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
(Base(hdr)(e') ~ Base(hdr)(e')) supposing ((header(e') = hdr ∈ Name) and hdr encodes T)
Lemma: eo-forward-base-classfun-res
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
(Base(hdr)@e' = Base(hdr)@e' ∈ T) supposing ((header(e') = hdr ∈ Name) and hdr encodes T)
Lemma: eo-forward-base-classfun-res-sq
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
(Base(hdr)@e' ~ Base(hdr)@e') supposing ((header(e') = hdr ∈ Name) and hdr encodes T)
Lemma: eo-forward-member-eclass
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[e',hdr:Top]. (e' ∈b Base(hdr) ~ e' ∈b Base(hdr))
Definition: class-caused-by
X <-- Z == ∀e':E. ∀v:T. (v ∈ X(e') ⇒ (↓∃e:E. ((e < e') ∧ <loc(e'), info(e')> ∈ Z(e))))
Lemma: class-caused-by_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[Z:EClass(Id × Message(f))]. ∀[T:Type]. ∀[X:EClass(T)]. (X <-- Z ∈ ℙ')
Definition: class-caused-by-some
X <-- p.Z[p] ==
∀e':E. ∀v:T. (v ∈ X(e') ⇒ (↓∃e,start:E. ∃p:A. (start ≤loc e ∧ (e < e') ∧ <loc(e'), info(e')> ∈ Z[p](e))))
Lemma: class-caused-by-some_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[A:Type]. ∀[Z:A ⟶ EClass(Id × Message(f))]. ∀[T:Type]. ∀[X:EClass(T)].
(X <-- p.Z[p] ∈ ℙ')
Definition: base-class-caused-by
hdr.X <-- p.Z[p] ==
∀e':E. ∀v:f hdr.
(v ∈ X(e') ⇒ (↓∃e,start:E. ∃p:A. (start ≤loc e ∧ (e < e') ∧ <loc(e'), make-Msg(hdr;v)> ∈ Z[p](e))))
Definition: info-delivered
info-delivered{i:l}(Info;X) ==
∀es:EO+(Info). ∀e:E. ∀locnfo:Id × Info.
(locnfo ∈ X(e) ⇒ (∃e':E. ((e < e') ∧ (loc(e') = (fst(locnfo)) ∈ Id) ∧ (info(e') = (snd(locnfo)) ∈ Info))))
Lemma: info-delivered_wf
∀[Info:Type]. ∀[X:EClass(Id × Info)]. (info-delivered{i:l}(Info;X) ∈ ℙ')
Definition: messages-delivered
messages-delivered{i:l}(es;X;f) ==
∀e:E. ∀locmsg:Id × Message(f).
(locmsg ∈ X(e) ⇒ (∃e':E. ((e < e') ∧ (loc(e') = (fst(locmsg)) ∈ Id) ∧ (info(e') = (snd(locmsg)) ∈ Message(f)))))
Lemma: messages-delivered_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. (messages-delivered{i:l}(es;X;f) ∈ ℙ')
Definition: messages-delivered-with-omissions
messages-delivered-with-omissions{i:l}(es;X;faults;f) ==
∃faulty:bag(Id)
((#(faulty) ≤ faults)
∧ (∀e:E. ∀locmsg:Id × Message(f).
(locmsg ∈ X(e)
⇒ (¬loc(e) ↓∈ faulty)
⇒ (∃e':E. ((e < e') ∧ (loc(e') = (fst(locmsg)) ∈ Id) ∧ (info(e') = (snd(locmsg)) ∈ Message(f)))))))
Lemma: messages-delivered-with-omissions_wf
∀[f:Name ⟶ Type]. ∀[faults:ℤ]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))].
(messages-delivered-with-omissions{i:l}(es;X;faults;f) ∈ ℙ')
Definition: messages-delivered-with-omissions-sub
messages-delivered-with-omissions-sub{i:l}(es;X;failures;ids;f) ==
∃faulty:bag(Id)
((#(faulty) ≤ failures)
∧ (∀e:E. ∀locmsg:Id × Message(f).
(locmsg ∈ X(e)
⇒ (¬loc(e) ↓∈ faulty)
⇒ loc(e) ↓∈ ids
⇒ (∃e':E. ((e < e') ∧ (loc(e') = (fst(locmsg)) ∈ Id) ∧ (info(e') = (snd(locmsg)) ∈ Message(f)))))))
Lemma: messages-delivered-with-omissions-sub_wf
∀[failures:ℤ]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[ids:bag(Id)].
(messages-delivered-with-omissions-sub{i:l}(es;X;failures;ids;f) ∈ ℙ')
Definition: message-constraint
message-constraint{i:l}(es;X;hdrs;f) == ∀e:E. ((header(e) ∈ hdrs) ⇒ (↓∃e':E. ((e' < e) ∧ <loc(e), info(e)> ∈ X(e'))))
Lemma: message-constraint_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(message-constraint{i:l}(es;X;hdrs;f) ∈ ℙ')
Definition: delivered-with-headers
delivered-with-headers(hdrs;es;e) == mapfilter(λe.<loc(e), info(e)>;λe.header(e) ∈b hdrs;≤loc(e))
Lemma: delivered-with-headers_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdrs:Name List].
(delivered-with-headers(hdrs;es;e) ∈ {im:Id × Message(f)| (msg-header(snd(im)) ∈ hdrs)} List)
Lemma: delivered-with-headers-no_repeats
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdrs:Name List]. no_repeats(E;filter(λe.header(e) ∈b hdrs;≤loc(e)))
Definition: strong-message-constraint
strong-message-constraint{i:l}(es;X;hdrs;f) ==
∀e:E
(↓∃bg:bag(E)
((∀e':E. (e' ↓∈ bg ⇒ (e' < e)))
∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))
Lemma: strong-message-constraint_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(strong-message-constraint{i:l}(es;X;hdrs;f) ∈ ℙ')
Lemma: strong-message-constraint-implies-message-constraint
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(strong-message-constraint{i:l}(es;X;hdrs;f) ⇒ message-constraint{i:l}(es;X;hdrs;f))
Definition: strong-message-constraint-no-rep
strong-message-constraint-no-rep{i:l}(es;X;hdrs;f) ==
∀e:E
(↓∃bg:bag(E)
(bag-no-repeats(E;bg)
∧ (∀e1,e2:E. (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2))))
∧ (∀e':E. (e' ↓∈ bg ⇒ (e' < e)))
∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))
Lemma: strong-message-constraint-no-rep_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(strong-message-constraint-no-rep{i:l}(es;X;hdrs;f) ∈ ℙ')
Lemma: strong-message-constraint-no-rep-implies
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(strong-message-constraint-no-rep{i:l}(es;X;hdrs;f) ⇒ strong-message-constraint{i:l}(es;X;hdrs;f))
Definition: strong-message-constraint-no-rep-large
strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) ==
∀e:E
(↓∃bg:bag(E)
(bag-no-repeats(E;bg)
∧ (∀e1,e2:E. (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2))))
∧ (∀e':E. (e' ↓∈ bg ⇒ (e' < e)))
∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
∧ (∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' ))))))
Lemma: strong-message-constraint-no-rep-large_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) ∈ ℙ')
Lemma: strong-message-constraint-no-rep-large-implies
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) ⇒ message-constraint{i:l}(es;X;hdrs;f))
Lemma: mapfilter-bor-eq
∀T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
((mapfilter(f;P;L) @ mapfilter(f;Q;L))
= (mapfilter(f;λx.(P[x] ∨bQ[x]);L) @ mapfilter(f;λx.(P[x] ∧b Q[x]);L))
∈ bag(U))
Lemma: mapfilter-bor
∀T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
sub-bag(U;mapfilter(f;λx.(P[x] ∨bQ[x]);L);mapfilter(f;P;L) @ mapfilter(f;Q;L))
Lemma: mapfilter-subbag
∀T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
((∀t:T. ((↑(P t)) ⇒ (↑(Q t)))) ⇒ sub-bag(U;mapfilter(f;P;L);mapfilter(f;Q;L)))
Lemma: strong-message-constraint-no-rep-large-1hdr
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(no_repeats(Name;hdrs)
⇒ strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f)
⇒ (∀hdr:Name. ((hdr ∈ hdrs) ⇒ strong-message-constraint-no-rep-large{i:l}(es;X;[hdr];f))))
Definition: strong-message-constraint-bag
strong-message-constraint-bag{i:l}(es; X; hdrs; f) ==
∀be:bag(E)
(bag-no-repeats(E;be)
⇒ (∀e1,e2:E. (e1 ↓∈ be ⇒ e2 ↓∈ be ⇒ (¬(e1 <loc e2))))
⇒ (↓∃bg:bag(E)
(bag-no-repeats(E;bg)
∧ (∀e1,e2:E. (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2))))
∧ (∀e':E. (e' ↓∈ bg ⇒ (∃e:E. (e ↓∈ be ∧ (e' < e)))))
∧ sub-bag(Id × Message(f);⋃e∈be.delivered-with-headers(hdrs;es;e);class-output(X;es;bg)))))
Lemma: strong-message-constraint-bag_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(strong-message-constraint-bag{i:l}(es; X; hdrs; f) ∈ ℙ')
Definition: std-ma
StandardMessageAutomaton(X;hdrs) == message-constraint{i:l}(es;X;hdrs;f) ∧ messages-delivered{i:l}(es;X;f)
Lemma: std-ma_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
(StandardMessageAutomaton(X;hdrs) ∈ ℙ')
Definition: std-ma-with-omissions
StandardMessageAutomaton(X;hdrs) (with send omissions at fail locations) ==
message-constraint{i:l}(es;X;hdrs;f) ∧ messages-delivered-with-omissions{i:l}(es;X;fail;f)
Lemma: std-ma-with-omissions_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List]. ∀[faults:ℤ].
(StandardMessageAutomaton(X;hdrs) (with send omissions at faults locations) ∈ ℙ')
Definition: causal-class-rel-in-out
if class_out outputs (m) then class_in observed x == ∀e:E. (m ∈ class_out(e) ⇒ (↓∃e':E. (e' c≤ e ∧ x ∈ class_in(e'))))
Lemma: causal-class-rel-in-out_wf
∀[f:Name ⟶ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[m:Id × Message(f)]. ∀[class_out:EClass(Id × Message(f))]. ∀[x:T].
∀[class_in:EClass(T)].
(if class_out outputs (m) then class_in observed x ∈ ℙ')
Definition: mk-msg
mk-msg(auth;hdr;val) == <auth, make-basicMsg(hdr;val)>
Lemma: mk-msg_wf
∀[f:Name ⟶ Type]. ∀[auth:𝔹]. ∀[hdr:Name]. ∀[val:f hdr]. (mk-msg(auth;hdr;val) ∈ Message(f))
Lemma: hdrmkmsg_lemma
∀val,hdr,auth:Top. (msg-header(mk-msg(auth;hdr;val)) ~ hdr)
Lemma: mk-msg-equal
∀[f:Name ⟶ Type]. ∀[auth1,auth2:𝔹]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
(mk-msg(auth1;hdr1;val1) = mk-msg(auth2;hdr2;val2) ∈ Message(f)
⇐⇒ {auth1 = auth2 ∧ (hdr1 = hdr2 ∈ Name) ∧ (val1 = val2 ∈ (f hdr1))})
Definition: make-Msg
make-Msg(hdr;val) == <ff, make-basicMsg(hdr;val)>
Lemma: make-Msg_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[val:f hdr]. (make-Msg(hdr;val) ∈ Message(f))
Lemma: make-Msg-equal
∀[f:Name ⟶ Type]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
(make-Msg(hdr1;val1) = make-Msg(hdr2;val2) ∈ Message(f) ⇐⇒ {(hdr1 = hdr2 ∈ Name) ∧ (val1 = val2 ∈ (f hdr1))})
Lemma: makeMsgfst_lemma
∀c,a:Top. (fst(snd(make-Msg(a;c))) ~ a)
Lemma: hdrmakeMsg_lemma
∀val,hdr:Top. (msg-header(make-Msg(hdr;val)) ~ hdr)
Lemma: make-Msg-as-mk-msg
∀[hdr,val:Top]. (make-Msg(hdr;val) ~ mk-msg(ff;hdr;val))
Definition: make-Authentic-Msg
make-Authentic-Msg(hdr;val) == <tt, make-basicMsg(hdr;val)>
Lemma: make-Authentic-Msg_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[val:f hdr]. (make-Authentic-Msg(hdr;val) ∈ Message(f))
Lemma: bodymakeMsg_lemma
∀val,hdr:Top. (msg-body(make-Msg(hdr;val)) ~ val)
Lemma: Message-inhabited
∀[f:Name ⟶ Type]. ↓Message(f) supposing ↓∃h:Name. (↓f h)
Lemma: Message-eta
∀[f:Name ⟶ Type]. ∀[m:Message(f)].
(m
= if msg-authentic(m) then make-Authentic-Msg(msg-header(m);msg-body(m)) else make-Msg(msg-header(m);msg-body(m)) fi
∈ Message(f))
Lemma: Message-eta2
∀[f:Name ⟶ Type]. ∀[m:Message(f)]. (m = mk-msg(msg-authentic(m);msg-header(m);msg-body(m)) ∈ Message(f))
Lemma: base-class-caused-by_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[A:Type]. ∀[Z:A ⟶ EClass(Id × Message(f))]. ∀[hdr:Name]. ∀[X:EClass(f hdr)].
(hdr.X <-- p.Z[p] ∈ ℙ')
Lemma: es-info-make-Msg
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
(make-Msg(hdr;v) = info(e) ∈ Message(f)) supposing
(msg-authentic(info(e)) = ff and
(msg-body(info(e)) = v ∈ (f hdr)) and
(header(e) = hdr ∈ Name))
Lemma: es-info-mk-msg
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[auth:𝔹]. ∀[hdr:Name]. ∀[v:f hdr].
(mk-msg(auth;hdr;v) = info(e) ∈ Message(f)) supposing
(msg-authentic(info(e)) = auth and
(msg-body(info(e)) = v ∈ (f hdr)) and
(header(e) = hdr ∈ Name))
Lemma: es-info-make-Msg-iff
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
uiff(make-Msg(hdr;v) = info(e) ∈ Message(f);msg-authentic(info(e)) = ff
∧ (header(e) = hdr ∈ Name)
∧ (msg-body(info(e)) = v ∈ (f hdr)))
Lemma: es-info-make-Msg-iff2
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
uiff(make-Msg(hdr;v) = info(e) ∈ Message(f);es-authentic(es;e) = ff
∧ (header(e) = hdr ∈ Name)
∧ (msgval(e) = v ∈ (f hdr)))
Definition: message-constraint-swap-hdr
message-constraint-swap-hdr{i:l}(f; es; X; hdr_in; hdrs_out) ==
∀e:E
((header(e) = hdr_in ∈ Name)
⇒ (↓∃e':E
∃hdr:Name
(((hdr ∈ hdrs_out) ∧ ((f hdr) = (f hdr_in) ∈ Type)) ∧ (e' < e) ∧ <loc(e), make-Msg(hdr;msgval(e))> ∈ X(e'))))
Lemma: message-constraint-swap-hdr_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdr_in:Name]. ∀[hdrs_out:Name List].
(message-constraint-swap-hdr{i:l}(f; es; X; hdr_in; hdrs_out) ∈ ℙ')
Definition: msg-interface
A msg interface consists of a delay, a destination location, and a message.
Interface == ℤ × Id × Message(f)
Lemma: msg-interface_wf
∀[f:Name ⟶ Type]. (Interface ∈ Type)
Definition: msg-interface-destination
mi.dst == fst(snd(mi))
Lemma: msg-interface-destination_wf
∀[f:Name ⟶ Type]. ∀[mi:Interface]. (mi.dst ∈ Id)
Definition: msg-interface-message
mi.msg == snd(snd(mi))
Lemma: msg-interface-message_wf
∀[f:Name ⟶ Type]. ∀[mi:Interface]. (mi.msg ∈ Message(f))
Definition: msg-interface-delay
mi.delay == fst(mi)
Lemma: msg-interface-delay_wf
∀[f:Name ⟶ Type]. ∀[mi:Interface]. (mi.delay ∈ ℤ)
Lemma: msg-interface-extensionality
∀[f:Name ⟶ Type]. ∀[x,y:Interface].
uiff(x = y ∈ Interface;(x.delay = y.delay ∈ ℤ) ∧ (x.dst = y.dst ∈ Id) ∧ (x.msg = y.msg ∈ Message(f)))
Definition: constrained-msg-interface
Interface(to locs, with hdrs) == {mi:Interface| (mi.dst ∈ locs) ∧ (msg-header(mi.msg) ∈ hdrs)}
Lemma: constrained-msg-interface_wf
∀[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. (Interface(to locs, with hdrs) ∈ Type)
Lemma: constrained-msg-interface-valueall-type
∀[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List].
valueall-type(Interface(to locs, with hdrs)) supposing (∀h∈hdrs.valueall-type(f h))
Definition: make-msg-interface
make-msg-interface(i;l;m) == <i, l, m>
Lemma: make-msg-interface_wf
∀[f:Name ⟶ Type]. ∀[i:ℤ]. ∀[l:Id]. ∀[m:Message(f)]. (make-msg-interface(i;l;m) ∈ Interface)
Lemma: make-msg-interface-equal
∀[f:Name ⟶ Type]. ∀[i1,i2:ℤ]. ∀[l1,l2:Id]. ∀[m1,m2:Message(f)].
(make-msg-interface(i1;l1;m1) = make-msg-interface(i2;l2;m2) ∈ Interface
⇐⇒ (i1 = i2 ∈ ℤ) ∧ (l1 = l2 ∈ Id) ∧ (m1 = m2 ∈ Message(f)))
Definition: mk-msg-interface
mk-msg-interface(l;m) == make-msg-interface(0;l;m)
Lemma: mk-msg-interface_wf
∀[f:Name ⟶ Type]. ∀[l:Id]. ∀[m:Message(f)]. (mk-msg-interface(l;m) ∈ Interface)
Definition: eo-msg-interface-constraint
eo-msg-interface-constraint(es;X;hdrs;f) ==
∀e:E. ((header(e) ∈ hdrs) ⇒ (↓∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))
Lemma: eo-msg-interface-constraint_wf
∀[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdrs:Name List]. ∀[es:EO+(Message(f))].
(eo-msg-interface-constraint(es;X;hdrs;f) ∈ ℙ)
Lemma: global-order-pairwise-compat-msg-interface-constraint
∀f:Name ⟶ Type. ∀hdrs:Name List. ∀X:EClass(Interface).
(LocalClass(X)
⇒ (∀LL:(Id × Message(f)) List List
((∀L1,L2∈LL. L1 || L2)
⇒ (∀L∈LL.eo-msg-interface-constraint(global-eo(L);X;hdrs;f))
⇒ (∃G:(Id × Message(f)) List
(eo-msg-interface-constraint(global-eo(G);X;hdrs;f)
∧ (∀L∈LL.∃g:E ⟶ E. es-local-embedding(Message(f);global-eo(L);global-eo(G);g)))))))
Lemma: global-order-pairwise-compat-msg-and-classrel
∀f:Name ⟶ Type. ∀hdrs:Name List. ∀X:EClass(Interface).
(LocalClass(X)
⇒ (∀LL:(Id × Message(f)) List List
((∀L1,L2∈LL. L1 || L2)
⇒ (∀L∈LL.eo-msg-interface-constraint(global-eo(L);X;hdrs;f))
⇒ (∃G:(Id × Message(f)) List
(eo-msg-interface-constraint(global-eo(G);X;hdrs;f)
∧ (∀L∈LL.∃g:E ⟶ E. ∀[e:E]. ∀[v:Interface]. (v ∈ X(e) ⇐⇒ v ∈ X(g e))))))))
Definition: msg-interface-constraint
msg-interface-constraint{i:l}(X;hdrs;f) ==
∀es:EO+(Message(f)). ∀e:E.
((header(e) ∈ hdrs) ⇒ (↓∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))
Lemma: msg-interface-constraint_wf
∀[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdrs:Name List]. (msg-interface-constraint{i:l}(X;hdrs;f) ∈ ℙ')
Definition: msg-interface-constraint-byzantine
msg-interface-constraint-byzantine{i:l}(X;hdrs;faulty;f) ==
∀es:EO+(Message(f)). ∀e:E.
((header(e) ∈ hdrs)
⇒ (↓∃e':E. ((∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))) ∨ (loc(e') ∈ faulty))))
Lemma: msg-interface-constraint-byzantine_wf
∀[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdrs:Name List]. ∀[faulty:Id List].
(msg-interface-constraint-byzantine{i:l}(X;hdrs;faulty;f) ∈ ℙ')
Definition: msgs-interface-delivered
msgs-interface-delivered{i:l}(X;f) ==
∀es:EO+(Message(f)). ∀e:E. ∀msg:Interface.
(msg ∈ X(e) ⇒ (↓∃e':E. ∃delay:ℤ. ((e < e') ∧ (msg = make-msg-interface(delay;loc(e');info(e')) ∈ Interface))))
Lemma: msgs-interface-delivered_wf
∀[f:Name ⟶ Type]. ∀X:EClass(Interface). (msgs-interface-delivered{i:l}(X;f) ∈ ℙ')
Definition: eo-msgs-interface-delivered
eo-msgs-interface-delivered(es;X;f) ==
∀e:E. ∀msg:Interface.
(msg ∈ X(e) ⇒ (↓∃e':E. ∃delay:ℤ. ((e < e') ∧ (msg = make-msg-interface(delay;loc(e');info(e')) ∈ Interface))))
Lemma: eo-msgs-interface-delivered_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀X:EClass(Interface). (eo-msgs-interface-delivered(es;X;f) ∈ ℙ)
Definition: msgs-interface-delivered-with-omissions
msgs-interface-delivered-with-omissions(f;es;X;faulty;failures;ids) ==
(#(faulty) ≤ failures)
∧ (∀e:E. ∀dmsg:Interface.
(dmsg ∈ X(e)
⇒ (¬loc(e) ↓∈ faulty)
⇒ loc(e) ↓∈ ids
⇒ (↓∃e':E. ∃delay:ℤ. ((e < e') ∧ (dmsg = make-msg-interface(delay;loc(e');info(e')) ∈ Interface)))))
Lemma: msgs-interface-delivered-with-omissions_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Interface)]. ∀[faulty:bag(Id)]. ∀[failures:ℤ]. ∀[ids:bag(Id)].
(msgs-interface-delivered-with-omissions(f;es;X;faulty;failures;ids) ∈ ℙ)
Definition: msgs-interface-with-omissions-sub
msgs-interface-with-omissions-sub{i:l}(X;failures;ids;f) ==
∀es:EO+(Message(f))
∃faulty:bag(Id)
((#(faulty) ≤ failures)
∧ (∀e:E. ∀dmsg:Interface.
(dmsg ∈ X(e)
⇒ (¬loc(e) ↓∈ faulty)
⇒ loc(e) ↓∈ ids
⇒ (↓∃e':E. ∃delay:ℤ. ((e < e') ∧ (dmsg = make-msg-interface(delay;loc(e');info(e')) ∈ Interface))))))
Lemma: msgs-interface-with-omissions-sub_wf
∀[f:Name ⟶ Type]
∀X:EClass(Interface). ∀failures:ℤ. ∀ids:bag(Id). (msgs-interface-with-omissions-sub{i:l}(X;failures;ids;f) ∈ ℙ')
Definition: msg-interface-hdf
This is the type of a local program for a main class in EventML.
msg-interface-hdf(f) == hdataflow(Message(f);ℤ × Id × Message(f))
Lemma: msg-interface-hdf_wf
∀[f:Name ⟶ Type]. (msg-interface-hdf(f) ∈ Type)
Definition: single-valued-on-header
single-valued-on-header{i:l}(Info;X;hdr) == ∀es:EO+(Info). ∀e:E. (↑#([x∈X(e)|name_eq(msg-header(x.msg);hdr)]) ≤z 1)
Lemma: single-valued-on-header_wf
∀[Info:Type]. ∀[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdr:Name]. (single-valued-on-header{i:l}(Info;X;hdr) ∈ ℙ')
Definition: sequential-composition-inputs
sequential-composition-inputs(es;e;X;hdr) ==
mapfilter(λxs.only([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst = loc(e)]).msg;
λxs.(#([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst = loc(e)]) =z 1);
map(λe.X(e);≤loc(e)))
Lemma: sequential-composition-inputs_wf
∀[Info:Type]. ∀[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[hdr:Name].
sequential-composition-inputs(es;e;X;hdr) ∈ Message(f) List supposing single-valued-on-header{i:l}(Info;X;hdr)
Definition: sequential-composition-class
sequential-composition-class(X;Y;hdr) ==
λes,e. let xs = X(e) in
let not_hdr = [x∈xs|¬bname_eq(msg-header(x.msg);hdr)] in
let has_hdr = [x∈xs|name_eq(msg-header(x.msg);hdr)] in
not_hdr
+ if (#(has_hdr) =z 1)
then let Infos = sequential-composition-inputs(es;e;X;hdr) in
Y list-eo(Infos;loc(e)) (||Infos|| - 1)
else {}
fi
Definition: local-simulation-input-validity
local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i) ==
∀e:E
((loc(e) = i ∈ Id)
⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))
Lemma: local-simulation-input-validity_wf
∀[f,g:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[hdrs:Name List]. ∀[i:Id]. (local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i) ∈ ℙ)
supposing hdr encodes Id × Message(g)
Definition: local-simulation-input-consistency
local-simulation-input-consistency(g;X;hdr;locs;es;i;j) ==
∀e1,e2:E.
((loc(e1) = i ∈ Id)
⇒ (loc(e2) = j ∈ Id)
⇒ local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))
Lemma: local-simulation-input-consistency_wf
∀[f,g:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
∀[i,j:Id]. (local-simulation-input-consistency(g;X;hdr;locs;es;i;j) ∈ ℙ) supposing hdr encodes Id × Message(g)
Definition: hdf-single-valued-except
A halting-dataflow from ⌜Message(f)⌝ to ⌜Interface⌝ is single valued
except on a list of headers if after processing any list L of messages
it is either halted or else, after filtering out the part of the output
with the given headers, what remains is a single-valued bag.⋅
hdf-single-valued-except(f;hdrs;X) ==
hdf-invariant(Message(f);b.single-valued-bag([x∈b|¬bmsg-header(snd(snd(x))) ∈b hdrs];Interface);X)
Lemma: hdf-single-valued-except_wf
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:msg-interface-hdf(f)]. (hdf-single-valued-except(f;hdrs;X) ∈ ℙ)
Lemma: hdf-ap-single-valued-except
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:{X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} ].
∀m:Message(f). (fst(X(m)) ∈ {X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} )
Lemma: hdf-ap-single-valued-except2
∀[f:Name ⟶ Type]. ∀[hdrs:Name List].
∀X:{X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} . ∀m:Message(f).
single-valued-bag([x∈snd(X(m))|¬bmsg-header(snd(snd(x))) ∈b hdrs];Interface)
Definition: hdf-only-headers
hdf-only-headers(f;hdrs;X) == hdf-invariant(Message(f);b.∀mi:Interface. (mi ↓∈ b ⇒ (msg-header(mi.msg) ∈ hdrs));X)
Lemma: hdf-only-headers_wf
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:msg-interface-hdf(f)]. (hdf-only-headers(f;hdrs;X) ∈ ℙ)
Lemma: hdf-ap-only-headers
∀[f:Name ⟶ Type]. ∀[hdrs:Name List].
∀X:{X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} . ∀m:Message(f).
(fst(X(m)) ∈ {X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} )
Lemma: hdf-ap-only-headers2
∀[f:Name ⟶ Type]
∀hdrs:Name List. ∀X:{X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} . ∀m:Message(f). ∀mi:Interface.
(mi ↓∈ snd(X(m)) ⇒ (msg-header(mi.msg) ∈ hdrs))
Definition: single-valued-class-except
single-valued-class-except{i:l}(f;hdrs;X) ==
∀es:EO+(Message(f)). ∀e:E. single-valued-bag([v∈X(e)|¬bmsg-header(snd(snd(v))) ∈b hdrs];Interface)
Lemma: single-valued-class-except_wf
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)]. (single-valued-class-except{i:l}(f;hdrs;X) ∈ ℙ')
Definition: class-only-headers
X is a class of type ⌜Interface⌝ such that the only headers in its output
are members of the given list, hdrs.⋅
class-only-headers{i:l}(f;hdrs;X) ==
∀es:EO+(Message(f)). ∀e:E. ∀mi:Interface. (mi ↓∈ X(e) ⇒ (msg-header(mi.msg) ∈ hdrs))
Lemma: class-only-headers_wf
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)]. (class-only-headers{i:l}(f;hdrs;X) ∈ ℙ')
Lemma: local-class-single-valued-class-except
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)].
(single-valued-class-except{i:l}(f;hdrs;X) ⇒ (∀P:LocalClass(X). ∀a:Id. hdf-single-valued-except(f;hdrs;P a)))
Lemma: local-class-only-headers
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)].
(class-only-headers{i:l}(f;hdrs;X) ⇒ (∀P:LocalClass(X). ∀a:Id. hdf-only-headers(f;hdrs;P a)))
Definition: msg-body-cmp
msg-body-cmp(mcmp) == λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2))
Lemma: msg-body-cmp_wf
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
∀a:{x:Message(f)| (msg-header(x) ∈ hdrs)}
(msg-body-cmp(mcmp) ∈ comparison({b:{m:Message(f)| (msg-header(m) ∈ hdrs)} |
(list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) a b) = 0 ∈ ℤ} ))
Definition: message-cmp
message-cmp(hdrs;mcmp) ==
comparison-seq(compare-fun(bool-cmp();λm.msg-authentic(m));
comparison-seq(list-index-cmp(NameDeq;hdrs;λm.msg-header(m)); msg-body-cmp(mcmp)))
Lemma: message-cmp_wf
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
(message-cmp(hdrs;mcmp) ∈ comparison({m:Message(f)| (msg-header(m) ∈ hdrs)} ))
Lemma: message-cmp-zero
∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)]. ∀[x,y:{m:Message(f)|
(msg-header(m) ∈ hdrs)} ].
uiff((message-cmp(hdrs;mcmp) x y) = 0 ∈ ℤ;msg-authentic(x) = msg-authentic(y)
∧ (msg-header(x) = msg-header(y) ∈ Name)
∧ ((mcmp msg-header(x) msg-body(x) msg-body(y)) = 0 ∈ ℤ))
Definition: interface-cmp
Compare members of Interface(to locs, with hdrs)
"lexicographically" first on the delay,
then on the index in locs of the dst,
then on the index in hdrs of the message header,
finally compare the message bodies using the
comparison given by the message header.⋅
interface-cmp(mcmp;locs;hdrs) ==
comparison-seq(int-minus-comparison(λmi.mi.delay); comparison-seq(list-index-cmp(IdDeq;locs;λmi.mi.dst);
compare-fun(message-cmp(hdrs;mcmp);λmi.mi.msg)))
Lemma: interface-cmp_wf
∀[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
(interface-cmp(mcmp;locs;hdrs) ∈ comparison(Interface(to locs, with hdrs)))
Lemma: interface-cmp-zero
∀[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
∀[x,y:Interface(to locs, with hdrs)].
(((interface-cmp(mcmp;locs;hdrs) x y) = 0 ∈ ℤ)
⇒ {(x.delay = y.delay ∈ ℤ)
∧ (x.dst = y.dst ∈ Id)
∧ msg-authentic(x.msg) = msg-authentic(y.msg)
∧ (msg-header(x.msg) = msg-header(y.msg) ∈ Name)
∧ ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0 ∈ ℤ)})
Definition: order-messages
order-messages(mcmp;locs;hdrs) == λb.bag-to-list(interface-cmp(mcmp;locs;hdrs);b)
Lemma: order-messages_wf
∀[allhdrs:Name List]. ∀[f:hdr:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
order-messages(mcmp;locs;allhdrs) ∈ {b:bag(Interface(to locs, with allhdrs))|
single-valued-bag([mi∈b|¬bmsg-header(mi.msg) ∈b hdrs];Interface)} ⟶ (Interface(\000Cto locs, with allhdrs) List)
supposing (∀h∈allhdrs.valueall-type(f h)) ∧ (∀h∈hdrs.∀x,y:f h. (((mcmp h x y) = 0 ∈ ℤ) ⇒ (x = y ∈ (f h))))
Definition: event-caused-by
e2 caused by e1 in S == ∃delay:ℤ. make-msg-interface(delay;loc(e2);info(e2)) ∈ S(e1)
Lemma: event-caused-by_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[S:EClass(Interface)]. ∀[e1,e2:E]. (e2 caused by e1 in S ∈ ℙ)
Definition: es-happened-before
e1 ⟶ e2 ==
fix((λes-happened-before,e2. ∃e:E
((e < e2)
∧ ((¬(loc(e) = loc(e2) ∈ Id)) ⇒ e2 caused by e in S)
∧ ((e = e1 ∈ E) ∨ (es-happened-before e)))))
e2
Lemma: es-happened-before_wf
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[S:EClass(Interface)]. ∀[e1,e2:E]. (e1 ⟶ e2 ∈ ℙ)
Home
Index