Library mcertikos.objects.dev.ObjSerialDriver
Require Import Coqlib.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import Values.
Require Import Constant.
Require Import OracleInstances.
Require Import Integers.
Open Scope Z_scope.
Section OBJ_SerialDriver.
Function get_serial_exists_spec (abd: RData): option Z :=
match (ikern abd, init abd, ihost abd) with
| (true, true, true) ⇒ Some (serial_exists (drv_serial abd))
| _ ⇒ None
end.
Function set_serial_exists_spec (v: Z) (abd: RData): option (RData) :=
match (ikern abd, ihost abd) with
| (true, true) ⇒
if (zle_le 0 v Int.max_unsigned) then
if (zlt_le 0 v Int.max_unsigned) then
Some (abd {drv_serial: (drv_serial abd){serial_exists: 1}})
else
Some (abd {drv_serial: (drv_serial abd){serial_exists: 0}})
else
None
| _ ⇒ None
end.
Function serial_init_spec (abd: RData) : option RData :=
match (ikern abd, init abd, ihost abd) with
| (true, true, true) ⇒
match com1 abd with
| mkDevData
(mkSerialState PortCom1Base true false _ nil nil _ _ _ _ _ _ _) lrx _ _ ⇒
match SerialEnv lrx with
| SerialRecv str ⇒
Some (abd {com1 / s: ( mkSerialState
PortCom1Base true false false nil (tl str)
false 1 8 1 pNone 199 11)}
{com1 / l1: lrx + 1}
{drv_serial: (mkSerialDriver 1)}
)
| _ ⇒
Some (abd {com1 / s: ( mkSerialState
PortCom1Base true false false nil nil
false 1 8 1 pNone 199 11)}
{com1 / l1: lrx + 1}
{drv_serial: (mkSerialDriver 1)}
)
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function when_send_complete (i: nat) (t: Z) :=
match SerialEnv (t + (Z.of_nat i)) with
| SerialSendComplete ⇒ Some i
| _ ⇒ None
end.
Function aux_check_tx_rdy_inner (i: nat) (t: Z) {struct i}: option nat :=
match i with
| O ⇒ when_send_complete 0%nat t
| S i ⇒ match aux_check_tx_rdy_inner i t with
| None ⇒ when_send_complete (S i) t
| Some i ⇒ Some i
end
end.
Lemma aux_check_tx_rdy_inner_p1_same:
∀ i t,
aux_check_tx_rdy_inner i t = Some i →
aux_check_tx_rdy_inner (S i) t = Some i.
Proof.
intros.
simpl.
rewrite H.
reflexivity.
Qed.
Lemma aux_check_tx_rdy_inner_same:
∀ i t,
aux_check_tx_rdy_inner i t = Some i →
(∀ n, aux_check_tx_rdy_inner (i + n) t = Some i).
Proof.
intros.
induction n.
- replace (i + 0)%nat with i by omega.
assumption.
- replace ((i + S n)%nat) with ((S (i + n))%nat) by omega.
simpl.
rewrite IHn.
reflexivity.
Qed.
Lemma aux_check_tx_rdy_inner_same_gt:
∀ i r t,
(i < r)%nat →
aux_check_tx_rdy_inner i t = Some i →
aux_check_tx_rdy_inner r t = Some i.
Proof.
intros.
set (n:=(r-i)%nat).
assert (r = i + n)%nat.
{
unfold n.
omega.
}
rewrite H1.
rewrite aux_check_tx_rdy_inner_same with (i:=i) (n:=n) (t:=t).
reflexivity.
assumption.
Qed.
Function putc_scan_log (t: Z)(bound: nat): option Z :=
match bound with
| O ⇒ None
| S bound´ ⇒
match SerialEnv t with
| SerialSendComplete ⇒ Some t
| _ ⇒ putc_scan_log (t + 1) bound´
end
end.
Definition next_sendcomplete (t: Z) :=
match putc_scan_log t 12800%nat with
| None ⇒ t + 12800
| Some i ⇒ i + 1
end.
Require Import FutureTactic.
Lemma putc_scan_log_eq_t:
∀ bound t n,
0 ≤ n < (Z.of_nat bound) →
SerialEnv (t + n) = SerialSendComplete →
(∀ x, 0 ≤ x < n → SerialEnv (t + x) = NullEvent) →
putc_scan_log t bound = Some (t + n).
Proof.
intros bound.
induction bound.
- intros. generalize H. toZ. intros. omega.
- intros.
assert (Hzb: 0 ≤ n < (Z.of_nat bound) + 1).
{
rewrite Nat2Z.inj_succ in H. omega.
}
remember (Z.of_nat bound) as zbound.
assert (Hcase: n = 0 ∨ 0 < n < zbound + 1) by omega.
destruct Hcase.
+ subst. rewrite Z.add_0_r in H0.
unfold putc_scan_log.
rewrite H0. f_equal. omega.
+ generalize (IHbound (t + 1) (n - 1)); intros IHb´.
assert (Hb: 0 ≤ n - 1 < zbound) by omega.
assert (Hevent: SerialEnv (t + 1 + (n - 1)) = SerialSendComplete).
{
calc. simpl. assumption.
}
assert (Horacle: ∀ x : Z, 0 ≤ x < n - 1 → SerialEnv (t + 1 + x) = NullEvent).
{
intros. generalize (H1 (1 + x)). calc. intros. rewrite H4. reflexivity.
omega.
}
generalize (IHb´ Hb Hevent Horacle).
assert (Htn: t + 1 + (n - 1) = t + n) by omega.
rewrite Htn. intros IHn.
unfold putc_scan_log. fold putc_scan_log.
rewrite IHn.
destruct (SerialEnv t) eqn: Ht; try reflexivity.
generalize (H1 0). rewrite Z.add_0_r. intros Hfact.
rewrite Hfact in Ht. inversion Ht. omega.
Qed.
Lemma next_sendcomplete_eq_t:
∀ t t´,
0 ≤ t´ < 12800 →
SerialEnv (t + t´) = SerialSendComplete →
(∀ n, 0 ≤ n < t´ → SerialEnv (t + n) = NullEvent) →
next_sendcomplete t = t + t´ + 1.
Proof.
intros t t´ Ht Horacle Hevent.
unfold next_sendcomplete.
assert (Hconst: Z.of_nat 12800%nat = 12800%Z). vm_compute. reflexivity.
assert (Hrange: 0 ≤ t´ < (Z.of_nat 12800%nat)). rewrite Hconst. assumption.
generalize (putc_scan_log_eq_t (12800%nat) t t´ Hrange Horacle Hevent).
intros Hputc. rewrite Hputc. reflexivity.
Qed.
Notation CHAR_CR := 13.
Notation CHAR_LF := 10.
Function serial_putc_spec (c: Z) (abd: RData): option RData :=
match (ikern abd, init abd, ihost abd) with
| (true, true, true) ⇒
if zeq 1 (serial_exists (drv_serial abd))
then
match (com1 abd) with
| mkDevData
(mkSerialState _ true _ _ txbuf nil false _ _ _ _ _ _) _ ltx _ ⇒
match txbuf with
| nil ⇒
if Z.eq_dec c CHAR_LF
then Some (abd {com1: (com1 abd)
{s/TxBuf: CHAR_LF :: CHAR_CR :: nil}
{l2: ltx + 1}})
else Some (abd {com1: (com1 abd)
{s/TxBuf: c :: nil}
{l2: ltx + 1}})
| _ ⇒
if Z.eq_dec c CHAR_LF
then Some (abd {com1: (com1 abd)
{s/TxBuf: CHAR_LF :: CHAR_CR :: nil}
{l2: (next_sendcomplete ltx)}})
else Some (abd {com1: (com1 abd)
{s/TxBuf: c :: nil}
{l2: (next_sendcomplete ltx)}})
end
| _ ⇒ None
end
else
Some abd
| _ ⇒ None
end.
Function serial_getc_spec (abd: RData) : option (RData × Z) :=
match (ikern abd, init abd, ihost abd) with
| (true, true, true) ⇒
if zeq 1 (serial_exists (drv_serial abd))
then
match com1 abd with
| mkDevData
(mkSerialState _ true _ true _ rxbuf false _ _ _ _ _ _) lrx _ _
⇒
match rxbuf with
| nil ⇒
match (SerialEnv lrx, SerialEnv (lrx + 1)) with
| (SerialRecv str, NullEvent) ⇒
Some (abd {com1 / s / RxBuf: tl str}
{com1 / s / SerialIrq: false}
{com1 / l1: lrx + 2}
{console: handle_cons_buf_write (console abd) (hd 0 str)}, 1)
| (NullEvent, _) ⇒
Some (abd {com1 / l1: lrx + 1}, 0)
| _ ⇒ None
end
| c :: t ⇒
match (SerialEnv lrx, SerialEnv (lrx + 1)) with
| (SerialRecv str, NullEvent) ⇒
let rxbuf´ := skipn (length (rxbuf ++ str) - 12) (rxbuf ++ str) in
let c´ := hd 0 rxbuf´ in
let tl´ := tl rxbuf´ in
if zle_le 0 c´ 255 then
Some (abd {com1 / s / RxBuf: tl´}
{com1 / s / SerialIrq: false}
{com1 / l1: lrx + 2}
{console: handle_cons_buf_write (console abd) c´}, 1)
else
None
| (NullEvent, SerialRecv str) ⇒
let rxbuf´ := skipn (length (rxbuf ++ str) - 12) (rxbuf ++ str) in
let c´ := hd 0 rxbuf´ in
let tl´ := tl rxbuf´ in
if zle_le 0 c´ 255 then
Some (abd {com1 / s / SerialIrq: false}
{com1 / s / RxBuf: tl´}
{com1 / l1: lrx + 2}
{console: handle_cons_buf_write (console abd) c´}, 1)
else
None
| (NullEvent, NullEvent) ⇒
if zle_le 0 c 255 then
Some (abd {com1 / s / SerialIrq: false}
{com1 / s / RxBuf: t}
{com1 / l1: lrx + 2}
{console: handle_cons_buf_write (console abd) c}, 1)
else
None
| _ ⇒ None
end
end
| _⇒ None
end
else Some (abd, 0)
| _ ⇒ None
end.
End OBJ_SerialDriver.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import LAsmModuleSemAux.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Local Open Scope Z_scope.
Section GET_SERIAL_EXISTS_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_drv_serial}.
Context {re3: relate_impl_init}.
Lemma get_serial_exists_exist:
∀ s habd labd z f,
get_serial_exists_spec habd = Some z
→ relate_AbData s f habd labd
→ get_serial_exists_spec labd = Some z.
Proof.
unfold get_serial_exists_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_drv_serial_eq; eauto.
revert H; subrewrite. subdestruct.
intros HV Hinit. rewrite <- Hinit. inv HV.
assumption.
Qed.
Lemma get_serial_exists_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_serial_exists_spec)
(id ↦ gensem get_serial_exists_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_serial_exists_exist; eauto. reflexivity.
Qed.
End GET_SERIAL_EXISTS_SIM.
Section SET_SERIAL_EXISTS_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_drv_serial}.
Lemma set_serial_exists_exist:
∀ s habd habd´ labd i f,
set_serial_exists_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_serial_exists_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_serial_exists_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite.
subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_drv_serial_update; eauto.
inv HQ; refine_split´; trivial.
apply relate_impl_drv_serial_update; eauto.
Qed.
Context {mt1: match_impl_drv_serial}.
Lemma set_serial_exists_match:
∀ s d d´ m i f,
set_serial_exists_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_serial_exists_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_drv_serial_update. assumption.
eapply match_impl_drv_serial_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_serial_exists_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_serial_exists_spec}.
Lemma set_serial_exists_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_serial_exists_spec)
(id ↦ gensem set_serial_exists_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_serial_exists_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply set_serial_exists_match; eauto.
Qed.
End SET_SERIAL_EXISTS_SIM.
Section SERIAL_INIT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_drv_serial}.
Context {re3: relate_impl_com1}.
Context {re4: relate_impl_init}.
Lemma serial_init_exist:
∀ s habd habd´ labd f,
serial_init_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_init_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. inversion 1.
exploit relate_impl_com1_eq; eauto.
revert H. subrewrite.
intro tmp; rewrite <- tmp.
subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_drv_serial_update; eauto.
apply relate_impl_com1_update; eauto.
apply relate_impl_com1_update; eauto.
inv HQ; refine_split´; trivial.
apply relate_impl_drv_serial_update; eauto.
apply relate_impl_com1_update; eauto.
apply relate_impl_com1_update; eauto.
inv HQ; refine_split´; trivial.
apply relate_impl_drv_serial_update; eauto.
apply relate_impl_com1_update; eauto.
apply relate_impl_com1_update; eauto.
inv HQ; refine_split´; trivial.
apply relate_impl_drv_serial_update; eauto.
apply relate_impl_com1_update; eauto.
apply relate_impl_com1_update; eauto.
Qed.
Context {mt1: match_impl_drv_serial}.
Context {mt2: match_impl_com1}.
Lemma serial_init_match:
∀ s d d´ m f,
serial_init_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold serial_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_drv_serial_update.
eapply match_impl_com1_update.
eapply match_impl_com1_update.
assumption.
eapply match_impl_drv_serial_update.
eapply match_impl_com1_update.
eapply match_impl_com1_update.
assumption.
eapply match_impl_drv_serial_update.
eapply match_impl_com1_update.
eapply match_impl_com1_update.
assumption.
eapply match_impl_drv_serial_update.
eapply match_impl_com1_update.
eapply match_impl_com1_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_init_spec}.
Lemma serial_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_init_spec)
(id ↦ gensem serial_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_init_match; eauto.
Qed.
End SERIAL_INIT_SIM.
Section SERIAL_PUTC_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_drv_serial}.
Context {re3: relate_impl_com1}.
Context {re4: relate_impl_init}.
Lemma serial_putc_exist:
∀ s habd habd´ labd i f,
serial_putc_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_putc_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_putc_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_drv_serial_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct;
inv HQ; refine_split´; trivial;
repeat apply relate_impl_com1_update; eauto.
Qed.
Context {mt1: match_impl_com1}.
Lemma serial_putc_match:
∀ s d d´ m i f,
serial_putc_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold serial_putc_spec; intros. subdestruct; inv H; trivial;
repeat (eapply match_impl_com1_update; assumption).
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_putc_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_putc_spec}.
Lemma serial_putc_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_putc_spec)
(id ↦ gensem serial_putc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_putc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_putc_match; eauto.
Qed.
End SERIAL_PUTC_SIM.
Section SERIAL_GETC_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_drv_serial}.
Context {re3: relate_impl_com1}.
Context {re4: relate_impl_console}.
Context {re5: relate_impl_init}.
Lemma serial_getc_exist:
∀ s habd habd´ labd i f,
serial_getc_spec habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_getc_spec labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_getc_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_drv_serial_eq; eauto; inversion 1.
exploit relate_impl_console_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct;
inv HQ; refine_split´; trivial;
repeat (
try apply relate_impl_console_update; eauto;
try apply relate_impl_com1_update; eauto).
Qed.
Context {mt1: match_impl_com1}.
Context {mt2: match_impl_console}.
Lemma serial_getc_match:
∀ s d d´ m i f,
serial_getc_spec d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold serial_getc_spec; intros. subdestruct; inv H; trivial;
repeat(
try eapply match_impl_console_update;
try eapply match_impl_com1_update);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_getc_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_getc_spec}.
Lemma serial_getc_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_getc_spec)
(id ↦ gensem serial_getc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_getc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_getc_match; eauto.
Qed.
End SERIAL_GETC_SIM.
End OBJ_SIM.