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.
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.