Library mcertikos.objects.dev.ObjSerialDevice
Require Import Coqlib.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import OracleInstances.
Section OBJ_SerialDevice.
Open Scope Z_scope.
Function byte_to_DLAB (x: Z) :=
match (x / COM_LCR_DLAB) with
| 1 ⇒ true
| _ ⇒ false
end.
Function byte_to_databits (x: Z) :=
(x mod 4 + 5).
Function byte_to_stopbits (x: Z) :=
(x / 4 mod 2 + 1).
Function byte_to_parity (x: Z): ParityType :=
match (x / 8 mod 8) with
| 1 ⇒ pOdd
| 3 ⇒ pEven
| 5 ⇒ pHigh
| 7 ⇒ pLow
| _ ⇒ pNone
end.
Function calc_baudrate_low8 (current: Z) (v: Z) :=
(current / 256 × 256 + v ).
Function calc_baudrate_high8 (current: Z) (v: Z) :=
(current mod 256 + v × 256).
Theorem update_baudrate_0_1_eq:
∀ v,
calc_baudrate_high8 (calc_baudrate_low8 v 1) 0 = 1.
Proof.
unfold calc_baudrate_low8, calc_baudrate_high8.
simpl. intros v. rewrite Zplus_mod. rewrite Z_mod_mult.
rewrite Zmod_1_l. reflexivity.
omega.
Qed.
Function remove_firstn {A} (l: list A) (n: nat): list A :=
match n, l with
| O, l ⇒ l
| S n´, nil ⇒ nil
| S n´, x :: l´ ⇒ remove_firstn l´ n´
end.
Notation SERIAL_HW_BUF_SIZE := 12%nat.
Function serial_trans_env (e: SerialEvent) (s: SerialState): SerialState :=
match s with
| mkSerialState base on irq rxint txbuf rxbuf
dlab baudrate databits
stopbits parity fifo modem ⇒
match e with
| SerialPlugin ⇒ s {SerialOn: true}
| SerialRecv str ⇒ let s´ := s {RxBuf:
skipn (length (rxbuf ++ str) - SERIAL_HW_BUF_SIZE)
(rxbuf ++ str)
} in if rxint then s´ {SerialIrq: true} else s´
| SerialSendComplete ⇒ s {TxBuf: nil}
| _ ⇒ s
end
end.
Function serial_trans_cpu (op: DeviceOp) (s: SerialState): SerialState :=
match s with
|mkSerialState base on irq rxint txbuf rxbuf
dlab baudrate databits
stopbits parity fifo modem ⇒
match op with
| OpInput n ⇒
if zeq n PortComRx then
match rxbuf with
| nil ⇒ s {SerialIrq: false}
| _ :: rxbuf´ ⇒ s {RxBuf: rxbuf´} {SerialIrq: false}
end
else if zeq n PortComIIR then
s {SerialIrq: false}
else s
| OpOutput n v ⇒
if zeq n PortComTx then
match dlab with
| true ⇒ s {Baudrate: calc_baudrate_low8 baudrate v}
| false ⇒ s {TxBuf: v :: txbuf}
end
else if zeq n PortComIER then
match dlab with
| true ⇒ s {Baudrate: calc_baudrate_high8 baudrate v}
| false ⇒ if zeq v 0 then s {RxIntEnable: false}
else if zeq v 1 then s {RxIntEnable: true}
else s
end
else if zeq n PortComFCR then
s {Fifo: v}
else if zeq n PortComLCR then
s {DLAB: byte_to_DLAB (v)}{Databits: byte_to_databits (v)}
{Stopbits: byte_to_stopbits (v)}{Parity: byte_to_parity (v)}
else if zeq n PortComMCR then
s {Modem: v}
else s
end
end.
Function serial_out_spec (port value: Z) (abd: RData): option RData :=
let p := port - (Base (s (com1 abd))) in
if zle_le 0 p 4
then
Some (abd {com1 / s: serial_trans_cpu (OpOutput p value) (s (com1 abd))})
else
None.
Function serial_valid_in_port (p: Z) :=
((p =? 0) || (p =? 2) || (p =? 5)).
Function serial_read_lsr (s: SerialState) : Z :=
match RxBuf s, TxBuf s with
| nil, nil ⇒ 0
| _, nil ⇒ 1
| nil, _ ⇒ 32
| _, _ ⇒ 33
end.
Function serial_in_spec (port pick: Z) (abd: RData): option (RData × Z) :=
let lrx := l1 (com1 abd) in
let ltx := l2 (com1 abd) in
let s := s (com1 abd) in
let p := port - (Base s) in
if zeq p 0 then
let s´ := serial_trans_env (SerialEnv lrx) s in
Some (abd {com1 / s: serial_trans_cpu (OpInput 0) s´}
{com1 / l1: lrx + 1}, (hd 0 (RxBuf s´)))
else if zeq p 2 then
Some (abd {com1 / s: serial_trans_cpu (OpInput 2) s},
if SerialIrq s then 1 else 0)
else if zeq p 5 then
match SerialOn s with
| false ⇒ Some (abd, 255)
| true ⇒
if zeq pick 1 then
let e := SerialEnv lrx in
match e with
| SerialRecv str ⇒ let s´ := serial_trans_env e s in
Some (abd {com1 / s: serial_trans_cpu (OpInput 5) s´}
{com1 / l1: lrx + 1},
match RxBuf s´ with
| nil ⇒ 0
| _ ⇒ 1
end)
| _ ⇒ Some (abd {com1 / s: serial_trans_cpu (OpInput 5) s}
{com1 / l1: lrx + 1},
match RxBuf s with
| nil ⇒ 0
| _ ⇒ 1
end)
end
else if zeq pick 32 then
let e := SerialEnv ltx in
match e with
| SerialSendComplete ⇒ let s´ := serial_trans_env e s in
Some (abd {com1 / s: serial_trans_cpu (OpInput 5) s´}
{com1 / l2: ltx + 1},
match TxBuf s´ with
| nil ⇒ 32
| _ ⇒ 0
end)
| _ ⇒ Some (abd {com1 / s: serial_trans_cpu (OpInput 5) s}
{com1 / l2: ltx + 1},
match TxBuf s with
| nil ⇒ 32
| _ ⇒ 0
end)
end
else if zeq pick 0 then Some (abd, 0)
else None
end
else None.
End OBJ_SerialDevice.
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 SERIAL_IN_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_com1}.
Lemma serial_in_exist:
∀ s habd habd´ labd port pic i f,
serial_in_spec port pic habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_in_spec port pic labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_in_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try apply relate_impl_com1_update; eauto).
Qed.
Context {mt1: match_impl_com1}.
Context {mt2: match_impl_console}.
Lemma serial_in_match:
∀ s d d´ m i f port pic,
serial_in_spec port pic d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold serial_in_spec; intros. subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_in_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_in_spec}.
Lemma serial_in_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_in_spec)
(id ↦ gensem serial_in_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_in_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_in_match; eauto.
Qed.
End SERIAL_IN_SIM.
Section SERIAL_OUT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_com1}.
Lemma serial_out_exist:
∀ s habd habd´ labd f port value,
serial_out_spec port value habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_out_spec port value labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_out_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_com1_update; eauto.
Qed.
Context {mt1: match_impl_com1}.
Lemma serial_out_match:
∀ s d d´ m f port value,
serial_out_spec port value d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold serial_out_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_com1_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_out_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_out_spec}.
Lemma serial_out_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_out_spec)
(id ↦ gensem serial_out_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_out_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_out_match; eauto.
Qed.
End SERIAL_OUT_SIM.
End OBJ_SIM.