Comment: EventML spec properties
exports: []
prefix: CLK:s
name: clock.esh:s
Comment: ------ CLK - headers ------
⋅
Definition: CLK_headers
CLK_headers() == [``CLK msg``]
Lemma: CLK_headers_wf
CLK_headers() ∈ Name List
Definition: CLK_headers_no_rep
CLK_headers_no_rep() == no_repeats(Name;CLK_headers())
Lemma: CLK_headers_no_rep_wf
CLK_headers_no_rep() ∈ ℙ
Definition: CLK_headers_fun
CLK_headers_fun(MsgType) == λhdr.if name_eq(hdr;``CLK msg``) then MsgType × ℤ else Top fi
Lemma: CLK_headers_fun_wf
∀[MsgType:ValueAllType]. (CLK_headers_fun(MsgType) ∈ Name ─→ Type)
Definition: CLK_headers_type
CLK_headers_type{i:l}(MsgType) ==
{f:Name ─→ ValueAllType| CLK_headers_no_rep() ∧ (∀hdr∈CLK_headers().(f hdr) = (CLK_headers_fun(MsgType) hdr))}
Lemma: CLK_headers_type_wf
∀[MsgType:ValueAllType]. (CLK_headers_type{i:l}(MsgType) ∈ ℙ')
Comment: ------ CLK - specification ------
⋅
Definition: CLK_msg'base
CLK_msg'base(MsgType;f) == Base(``CLK msg``)
Lemma: CLK_msg'base_wf
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. (CLK_msg'base(MsgType;f) ∈ EClass(MsgType × ℤ))
Definition: CLK_msg'base-program
CLK_msg'base-program(MsgType;f) == base-class-program(``CLK msg``)
Lemma: CLK_msg'base-program_wf
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_msg'base-program(MsgType;f) ∈ LocalClass(CLK_msg'base(MsgType;f)))
Definition: CLK_msg'send
CLK_msg'send(MsgType;f) == λl,z. mk-msg-interface(l;make-Msg(``CLK msg``;z))
Lemma: CLK_msg'send_wf
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_msg'send(MsgType;f) ∈ Id ─→ (MsgType × ℤ) ─→ Interface)
Definition: CLK_upd_clock
CLK_upd_clock(MsgType) == λslf,z,clock. let z,timestamp = z in imax(timestamp;clock) + 1
Lemma: CLK_upd_clock_wf
∀[MsgType:ValueAllType]. (CLK_upd_clock(MsgType) ∈ Id ─→ (MsgType × ℤ) ─→ ℤ ─→ ℤ)
Definition: CLK_Clock
CLK_Clock(MsgType;f) == state-class1(λslf.0;CLK_upd_clock(MsgType);CLK_msg'base(MsgType;f))
Lemma: CLK_Clock_wf
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. (CLK_Clock(MsgType;f) ∈ EClass(ℤ))
Lemma: CLK_Clock-functional
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. CLK_Clock(MsgType;f) is functional
Definition: CLK_ClockFun
CLK_ClockVal(MsgType;f)@e == CLK_Clock(MsgType;f)(e)
Lemma: CLK_ClockFun_wf
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E].
(CLK_ClockVal(MsgType;f)@e ∈ ℤ)
Lemma: CLK_Clock-classrel
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].
∀es:EO+(Message(f)). ∀e:E. ∀v:ℤ. (v ∈ CLK_Clock(MsgType;f)(e) ⇐⇒ v = CLK_ClockVal(MsgType;f)@e)
Definition: CLK_Clock-program
CLK_Clock-program(MsgType;f) == state-class1-program(λslf.0;CLK_upd_clock(MsgType);CLK_msg'base-program(MsgType;f))
Lemma: CLK_Clock-program_wf
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_Clock-program(MsgType;f) ∈ LocalClass(CLK_Clock(MsgType;f)))
Lemma: CLK_stric_inc
∀MsgType:ValueAllType. ∀f:CLK_headers_type{i:l}(MsgType). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀clock1,clock2:ℤ.
((∃a:MsgType × ℤ. ∃e:E. ((e1 <loc e) ∧ e ≤loc e2 ∧ a ∈ CLK_msg'base(MsgType;f)(e)))
⇒ (e1 <loc e2)
⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1)
⇒ clock2 ∈ CLK_Clock(MsgType;f)(e2)
⇒ clock1 < clock2)
Definition: CLK_mk_reply
CLK_mk_reply(MsgType;reply;f) ==
λslf,z,clock. let msg_val,z = z
in let new_msg,recipient = reply slf msg_val
in {CLK_msg'send(MsgType;f) recipient <new_msg, clock>}
Lemma: CLK_mk_reply_wf
∀[MsgType:ValueAllType]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_mk_reply(MsgType;reply;f) ∈ Id ─→ (MsgType × ℤ) ─→ ℤ ─→ bag(Interface))
Definition: CLK_Reply
CLK_Reply(MsgType;reply;f) == ((CLK_mk_reply(MsgType;reply;f) o CLK_msg'base(MsgType;f)) o CLK_Clock(MsgType;f))
Lemma: CLK_Reply_wf
∀[MsgType:ValueAllType]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_Reply(MsgType;reply;f) ∈ EClass(Interface))
Definition: CLK_Reply-program
CLK_Reply-program(MsgType;reply;f) ==
eclass1-program(CLK_mk_reply(MsgType;reply;f);CLK_msg'base-program(MsgType;f)) o CLK_Clock-program(MsgType;f)
Lemma: CLK_Reply-program_wf
∀[MsgType:ValueAllType]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_Reply-program(MsgType;reply;f) ∈ LocalClass(CLK_Reply(MsgType;reply;f)))
Definition: CLK_main
CLK_main(MsgType;locs;reply;f) == CLK_Reply(MsgType;reply;f)@locs
Lemma: CLK_main_wf
∀[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_main(MsgType;locs;reply;f) ∈ EClass(Interface))
Definition: CLK_main-program
CLK_main-program(MsgType;locs;reply;f) == (CLK_Reply-program(MsgType;reply;f))@locs
Lemma: CLK_main-program_wf
∀[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_main-program(MsgType;locs;reply;f) ∈ LocalClass(CLK_main(MsgType;locs;reply;f)))
Comment: ------ CLK - extra ------
⋅
Definition: CLK_headers_internal
CLK_headers_internal() == [``CLK msg``]
Lemma: CLK_headers_internal_wf
CLK_headers_internal() ∈ Name List
Definition: CLK_headers_no_inputs
CLK_headers_no_inputs() == [``CLK msg``]
Lemma: CLK_headers_no_inputs_wf
CLK_headers_no_inputs() ∈ Name List
Definition: CLK_headers_no_inputs_types
CLK_headers_no_inputs_types(MsgType) == [<``CLK msg``, MsgType × ℤ>]
Lemma: CLK_headers_no_inputs_types_wf
∀[MsgType:ValueAllType]. (CLK_headers_no_inputs_types(MsgType) ∈ (Name × Type) List)
Definition: CLK_message-constraint
CLK_message-constraint{i:l}(MsgType;locs;reply;f) ==
msg-interface-constraint{i:l}(CLK_main(MsgType;locs;reply;f);CLK_headers_internal();f)
Lemma: CLK_message-constraint_wf
∀[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_message-constraint{i:l}(MsgType;locs;reply;f) ∈ ℙ')
Definition: CLK_messages-delivered
CLK_messages-delivered{i:l}(MsgType;locs;reply;f) == msgs-interface-delivered{i:l}(CLK_main(MsgType;locs;reply;f);f)
Lemma: CLK_messages-delivered_wf
∀[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
(CLK_messages-delivered{i:l}(MsgType;locs;reply;f) ∈ ℙ')
Lemma: CLK-ilf
∀[MsgType:{T:Type| valueall-type(T)} ]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)].
∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(f)].
{<d, i, m> ∈ CLK_main(MsgType;locs;reply;f)(e)
⇐⇒ loc(e) ↓∈ locs
∧ ((header(e) = ``CLK msg``) ∧ has-es-info-type(es;e;f;MsgType × ℤ))
∧ (d = 0)
∧ (i = (snd((reply loc(e) (fst(msgval(e)))))))
∧ (m = make-Msg(``CLK msg``;<fst((reply loc(e) (fst(msgval(e))))), CLK_ClockVal(MsgType;f)@e>))}
Lemma: CLK-msg
∀[MsgType:{T:Type| valueall-type(T)} ]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)].
∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹]. ∀[v:MsgType]. ∀[k:ℤ].
(<d, i, mk-msg(auth;``CLK msg``;<v, k>)> ∈ CLK_main(MsgType;locs;reply;f)(e)
⇐⇒ loc(e) ↓∈ locs
∧ ((header(e) = ``CLK msg``) ∧ has-es-info-type(es;e;f;MsgType × ℤ))
∧ (d = 0)
∧ (i = (snd((reply loc(e) (fst(msgval(e)))))))
∧ auth = ff
∧ (v = (fst((reply loc(e) (fst(msgval(e)))))))
∧ (k = CLK_ClockVal(MsgType;f)@e))
Lemma: CLK_main-opt1
∀[MsgType,locs,reply,f:Top].
(CLK_main-program(MsgType;locs;reply;f)
~ λi.case i ∈b locs)
of inl() =>
fix((λmk-hdf,clock. (inl (λv.let x,y = v
in let x@0,y@0 = y
in case name_eq(x@0;``CLK msg``)
of inl(x5) =>
let z,timestamp = y@0
in let x1 ←─ eval a = timestamp in
eval b = clock in
if (b) < (a) then a + 1 else (b + 1)
in let v3 ←─ (CLK_mk_reply(MsgType;reply;f) i <z, timestamp> x1) @ []
in <mk-hdf x1, v3>
| inr(x5) =>
let x2 ←─ clock
in <mk-hdf x2, []>))))
0
| inr() =>
inr ⋅ )
Lemma: CLK_main-opt2
∀[MsgType,locs,reply,f:Top].
(CLK_main-program(MsgType;locs;reply;f)
~ λi.case i ∈b locs)
of inl() =>
fix((λmk-hdf,clock. (inl (λv.let x,y = v
in let x@0,y@0 = y
in case name_eq(x@0;``CLK msg``)
of inl(x5) =>
let z,timestamp = y@0
in let x1 ←─ eval a = timestamp in
eval b = clock in
if (b) < (a) then a + 1 else (b + 1)
in let v3 ←─ (CLK_mk_reply(MsgType;reply;f) i <z, timestamp> x1) @ []
in <mk-hdf x1, v3>
| inr(x5) =>
let x2 ←─ clock
in <mk-hdf x2, []>))))
0
| inr() =>
inr ⋅ )
Lemma: CLK_strict_inc2
∀MsgType:ValueAllType. ∀f:CLK_headers_type{i:l}(MsgType). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀clock1,clock2:ℤ.
((∃e:E. ((e1 <loc e) ∧ e ≤loc e2 ∧ (↑e ∈b CLK_msg'base(MsgType;f))))
⇒ (e1 <loc e2)
⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1)
⇒ clock2 ∈ CLK_Clock(MsgType;f)(e2)
⇒ clock1 < clock2)
Lemma: CLK_ClockFun-eq
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E].
CLK_ClockVal(MsgType;f)@e
= (imax(snd(CLK_msg'base(MsgType;f)@e);if first(e) then 0 else CLK_ClockVal(MsgType;f)@pred(e) fi ) + 1)
supposing ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))
Lemma: CLK_ClockFun-eq2
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E].
(CLK_ClockVal(MsgType;f)@e
= if e ∈b CLK_msg'base(MsgType;f)
then if first(e)
then imax(snd(CLK_msg'base(MsgType;f)@e);0) + 1
else imax(snd(CLK_msg'base(MsgType;f)@e);CLK_ClockVal(MsgType;f)@pred(e)) + 1
fi
if first(e) then 0
else CLK_ClockVal(MsgType;f)@pred(e)
fi )
Lemma: CLK-prop
∀MsgType:ValueAllType. ∀locs:bag(Id). ∀reply:Id ─→ MsgType ─→ (MsgType × Id). ∀f:CLK_headers_type{i:l}(MsgType).
∀es:EO+(Message(f)). ∀e1,e2:E. ∀clock1,clock2:ℤ.
(CLK_message-constraint{i:l}(MsgType;locs;reply;f)
⇒ (∀e:E. (↑e ∈b CLK_msg'base(MsgType;f)))
⇒ e1 ─→ e2
⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1)
⇒ clock2 ∈ CLK_Clock(MsgType;f)(e2)
⇒ clock1 < clock2)
Lemma: CLK-prop2
∀MsgType:ValueAllType. ∀locs:bag(Id). ∀reply:Id ─→ MsgType ─→ (MsgType × Id). ∀f:CLK_headers_type{i:l}(MsgType).
∀es:EO+(Message(f)). ∀e1,e2:E. ∀clock1,clock2:ℤ.
((∀e:E. (↑e ∈b CLK_msg'base(MsgType;f)))
⇒ e1 ─→ e2
⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1)
⇒ clock2 ∈ CLK_Clock(MsgType;f)(e2)
⇒ clock1 < clock2)
Home
Index