Module device_cc2500

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_cc2500 : DEV_Sig.

Device state, and initial state


  Variant cc2500_state :=
  | Unknown
  | Calibrated
  | Idle
  | Sleep
  | Rx.

  Axiom cc2500_state_to_int: cc2500_state -> int.

  Definition t := cc2500_state.
  Definition init := Unknown.

Device operations interface
  Inductive ops_query_ : Type :=
  | cc2500_calibrate : unit -> ops_query_
  | cc2500_idle : unit -> ops_query_
  | cc2500_sleep : unit -> ops_query_
  | cc2500_wakeup : unit -> ops_query_
  | cc2500_rx_enter : unit -> ops_query_
  | cc2500_send_packet : void_star -> uint8_t -> ops_query_
  | cc2500_rx_register_cb : cc2500_cb_t -> ops_query_
  | cc2500_rx_register_buffer : void_star -> uint8_t -> ops_query_
  | cc2500_set_channel : uint8_t -> ops_query_
  | cc2500_get_drv_mode : unit -> ops_query_
  | cc2500_get_cca : unit -> ops_query_
  | cc2500_get_rssi : unit -> ops_query_.
  Definition ops_query := ops_query_.

  Definition ops_response (q : ops_query): Type :=
    match q with
    | cc2500_calibrate _
    | cc2500_rx_register_cb _
    | cc2500_rx_register_buffer _ _
    | cc2500_set_channel _ => unit
    | cc2500_idle _
    | cc2500_sleep _
    | cc2500_wakeup _
    | cc2500_rx_enter _
    | cc2500_send_packet _ _
    | cc2500_get_drv_mode _ => int
    | cc2500_get_cca _
    | cc2500_get_rssi _ => uint8_t
    end.

  Inductive op_sem_: forall q: ops_query, t -> ops_response q -> t -> Prop :=
  | calibrate: forall s,
      op_sem_
        (cc2500_calibrate tt) s
        tt Calibrated
  | idle_success: forall s,
      op_sem_
        (cc2500_idle tt) s
        int_zero Idle
  | idle_failure: forall s errno,
      errno <> int_zero ->
      op_sem_
        (cc2500_idle tt) s
        errno s
  | sleep_success:
      op_sem_
        (cc2500_sleep tt) Idle
        int_zero Sleep
  | sleep_failure: forall s errno,
      errno <> int_zero ->
      op_sem_
        (cc2500_sleep tt) s
        errno s
  | wakeup_success:
      op_sem_
        (cc2500_wakeup tt) Sleep
        int_zero Idle
  | wakeup_failure: forall s errno,
      errno <> int_zero ->
      op_sem_
        (cc2500_wakeup tt) s
        errno s
  | rx_enter_success:
      op_sem_
        (cc2500_rx_enter tt) Idle
        int_zero Rx
  | rx_enter_failure: forall s errno,
      errno <> int_zero ->
      op_sem_
        (cc2500_rx_enter tt) s
        errno s
  | send_packet: forall pkt usize s errno,
      (errno = int_zero /\ s = Idle) \/ errno <> int_zero ->
      op_sem_
        (cc2500_send_packet pkt usize) s
        errno s
  | rx_register_cb : forall cb s,
      op_sem_
        (cc2500_rx_register_cb cb) s
        tt s
  | rx_register_buffer : forall buff size s,
      op_sem_
        (cc2500_rx_register_buffer buff size) s
        tt s
  | set_channel : forall n s,
      op_sem_
        (cc2500_set_channel n) s
        tt s
  | get_drv_mode : forall s,
      op_sem_
        (cc2500_get_drv_mode tt) s
        (cc2500_state_to_int s) s
  | get_cca : forall s n,
      op_sem_
        (cc2500_get_cca tt) s
        n s
  | get_rssi: forall s n,
      op_sem_
        (cc2500_get_rssi tt) s
        n s.
  Definition op_sem := op_sem_.

Equivalence relation on device states. In the paper, we simplify the presentation, and we abstract from that equivalence relation, using bare equality.
  Definition equiv : relation t := fun x y => x = y.
  Lemma equiv_equiv: equivalence t equiv.
  Proof.
  split.
  - intros x; eapply eq_refl.
  - intros ? ? ?; eapply eq_trans.
  - intros ? ?; eapply eq_sym.
  Qed.

  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.
  Proof.
    intros.
    dependent destruction H1;
    dependent destruction H;
    try (unfold equiv; auto);
    try contradiction.
  Qed.

End dev_cc2500.