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 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) ⇐⇒ 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 
                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) CLK_msg'base(MsgType;f)) 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)) 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 
                                     in let x@0,y@0 
                                        in case name_eq(x@0;``CLK msg``)
                                            of inl(x5) =>
                                            let z,timestamp y@0 
                                            in let x1 ←─ eval timestamp in
                                                         eval clock in
                                                           if (b) < (a)  then 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 
                                     in let x@0,y@0 
                                        in case name_eq(x@0;``CLK msg``)
                                            of inl(x5) =>
                                            let z,timestamp y@0 
                                            in let x1 ←─ eval timestamp in
                                                         eval clock in
                                                           if (b) < (a)  then 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 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