---

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