Module device_smclk

Require Import List.
Import ListNotations.
Require Import Relations.
Require Import Coq.Program.Equality.

Require Import util.
Require Import specification.
Require Import ctypes.
Require Import device.

Module dev_smclk : DEV_Sig.



  Record t_ := { src: clock_src_t;
                div: clock_div_t }.
  Definition t := t_.
  Definition init := Build_t_ clock_src_init clock_div_init.

  Inductive ops_query_ : Type :=
  | clk_set_smclk_src : clock_src_t -> ops_query_
  | clk_get_smclk_src : unit -> ops_query_
  | clk_set_smclk_div : clock_div_t -> ops_query_
  | clk_get_smclk_div : unit -> ops_query_.

  Definition ops_query := ops_query_.

  Definition ops_response (q : ops_query): Type :=
    match q with
    | clk_set_smclk_src _
    | clk_set_smclk_div _ => unit
    | clk_get_smclk_src _ => clock_src_t
    | clk_get_smclk_div _ => clock_div_t
    end.

  Inductive op_sem_: forall q: ops_query, t -> ops_response q -> t -> Prop :=
  | set_src: forall smclk s smclk',
      smclk' = Build_t_ s (smclk.(div)) ->
      op_sem_
        (clk_set_smclk_src s) smclk
        tt smclk'
  | get_src: forall smclk,
      op_sem_
        (clk_get_smclk_src tt) smclk
        smclk.(src) smclk
  | set_div: forall smclk d smclk',
      smclk' = Build_t_ (smclk.(src)) d ->
      op_sem_
        (clk_set_smclk_div d) smclk
        tt smclk'
  | get_div: forall smclk,
      op_sem_
        (clk_get_smclk_div tt) smclk
        smclk.(div) smclk.

  Definition op_sem := op_sem_.

  Definition equiv : relation t := fun x y => x = y.
  Lemma equiv_equiv: equivalence t equiv.

  Lemma op_sem_equiv: forall op_query op_resp dev1 dev2 dev3 dev4,
    op_sem op_query dev1 op_resp dev2 ->
    equiv dev1 dev3 ->
    op_sem op_query dev3 op_resp dev4 ->
    equiv dev2 dev4.

End dev_smclk.