Library mcertikos.objects.dev.ObjInterruptController
Require Import Coqlib.
Require Import Maps.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Constant.
Require Import OracleInstances.
Require Import ObjSerialDevice.
Section OBJ_InterruptController.
Section ioAPIC.
Function ioapic_trans_cpu (op: DeviceOp) (s: IoApicState) : IoApicState :=
match s with
| mkIoApicState init current base id maxIntr irqs enables
⇒
match op with
| OpOutput addr v ⇒
if zeq addr IOAPIC_ID
then s {IoApicId: v}
else
if zle_le 16 addr (maxIntr × 2 + 17)
then
match addr_to_idx addr with
| Low32 i ⇒
let idx := Z.to_nat i in
s {IoApicIrqs [idx]: (low32_to_irq v)}
{IoApicEnables [idx]: (low32_to_enable v)}
| High32 i ⇒ s
end
else
s
| _ ⇒ s
end
end.
Function ioapic_trans_intr (w: IntrOp) (s: IoApicState) : IoApicState :=
match s with
| mkIoApicState init current base id maxIntr irqs enables
⇒
match w with
| IRQ x ⇒
let n:= (Z.to_nat x) in
match nth_error irqs n with
| value v ⇒
match nth_error enables n with
| value true ⇒ s {CurrentIrq: Some (v, 0)}
| _ ⇒ s {CurrentIrq: None}
end
| error ⇒ s {CurrentIrq: None}
end
| EOI ⇒
s {CurrentIrq: None}
end
end.
Function ioapic_valid_write_range (offset: Z) (maxIntr: Z) : bool :=
((zeq offset 0) || (zle_le 16 offset (maxIntr × 2 + 17))).
Function ioapic_write_spec (addr: Z) (v: Z) (abd: RData): option RData :=
if zeq addr 0 then
if zle_le (2^24) v (2^27) then
Some (abd {ioapic / s: (ioapic_trans_cpu (OpOutput addr v) (s (ioapic abd)))})
else
None
else if zle_le 16 addr ((IoApicMaxIntr (s (ioapic abd))) × 2 + 17) then
Some (abd {ioapic / s: (ioapic_trans_cpu (OpOutput addr v) (s (ioapic abd)))})
else
None.
Function ioapic_valid_read_range (offset: Z) (maxIntr: Z) : bool :=
((zeq offset 1) || (offset =? 2) || (zle_le 16 offset (maxIntr × 2 + 17))).
Function ioapic_read_0 (s: IoApicState) : Z :=
(s.(IoApicId) × 16777216).
Function ioapic_read_1 (s: IoApicState) : Z :=
(s.(IoApicMaxIntr) × 65536).
Function ioapic_read_tbl (s: IoApicState) (idx: Z): Z :=
let i := Z.to_nat (idx / 2) in
if zeq (idx mod 2) 0
then
let irqs:= s.(IoApicIrqs) in
let enables := s.(IoApicEnables) in
let vec := nth i irqs 0 in
let msk := if nth i enables false then 0 else 1 in
vec + msk × 65536
else
0.
Function ioapic_read_spec (addr: Z) (abd: RData): option (RData × Z) :=
if zeq addr IOAPIC_ID then
Some (abd, ioapic_read_0 abd.(ioapic).(s))
else if zeq addr IOAPIC_VER then
Some (abd, ioapic_read_1 abd.(ioapic).(s))
else if zle_le 16 addr (IoApicMaxIntr (s (ioapic abd)) × 2 + 17) then
Some (abd, ioapic_read_tbl abd.(ioapic).(s) (addr - 16))
else
None.
Function ioapic_intr (irq: Z) (abd: RData): RData :=
abd {ioapic / s: (ioapic_trans_intr (IRQ irq) (s (ioapic abd)))}.
Function ioapic_eoi (abd: RData): RData :=
abd {ioapic / s: (ioapic_trans_intr EOI (s (ioapic abd)))}.
End ioAPIC.
Section lAPIC.
Inductive LAPIC_REGS : Set :=
| LAPIC_SVR
| LAPIC_LVT_PMC
| LAPIC_LVT_LINT0
| LAPIC_LVT_LINT1
| LAPIC_DFR
| LAPIC_LDR
| LAPIC_ERROR
| LAPIC_ESR
| LAPIC_EOI
| LAPIC_TPR.
Function lapic_idx_to_reg (idx: Z) : option LAPIC_REGS :=
match idx with
| LAPIC_IDX_SVR ⇒ Some (LAPIC_SVR)
| LAPIC_IDX_LVT_PMC ⇒ Some (LAPIC_LVT_PMC)
| LAPIC_IDX_LVT_LINT0 ⇒ Some (LAPIC_LVT_LINT0)
| LAPIC_IDX_LVT_LINT1 ⇒ Some (LAPIC_LVT_LINT1)
| LAPIC_IDX_DFR ⇒ Some (LAPIC_DFR)
| LAPIC_IDX_LDR ⇒ Some (LAPIC_LDR)
| LAPIC_IDX_ERROR ⇒ Some (LAPIC_ERROR)
| LAPIC_IDX_ESR ⇒ Some (LAPIC_ESR)
| LAPIC_IDX_EOI ⇒ Some (LAPIC_EOI)
| LAPIC_IDX_TPR ⇒ Some (LAPIC_TPR)
| _ ⇒ None
end.
Function lapic_trans_cpu (op: DeviceOp) (s: LApicState) : LApicState :=
match s with
| mkLApicState esr eoi maxLvt enable spurious lint0m lint1m pcm ldr errIrq esrClr tpr
⇒
match op with
| OpOutput addr v ⇒
match lapic_idx_to_reg addr with
| Some r ⇒
match r with
| LAPIC_SVR ⇒ s {LapicEnable: (lapic_reg_to_enable v)}
{LapicSpurious: (lapic_reg_to_spurious v)}
{LapicEsrClrPen: false}
| LAPIC_LVT_PMC ⇒ s {LapicPcIntMask: (lapic_reg_to_lvt_mask v)}
{LapicEsrClrPen: false}
| LAPIC_LVT_LINT0 ⇒ s {LapicLint0Mask: (lapic_reg_to_lvt_mask v)}
{LapicEsrClrPen: false}
| LAPIC_LVT_LINT1 ⇒ s {LapicLint1Mask: (lapic_reg_to_lvt_mask v)}
{LapicEsrClrPen: false}
| LAPIC_DFR ⇒ s {LapicEsrClrPen: false}
| LAPIC_LDR ⇒ s {LapicLdr: v}
{LapicEsrClrPen: false}
| LAPIC_ERROR ⇒ s {LapicErrorIrq: v}
{LapicEsrClrPen: false}
| LAPIC_ESR ⇒ if esrClr
then if zeq v 0 then s {LapicEsr: 0} else s
else s {LapicEsrClrPen: true}
| LAPIC_EOI ⇒ if zeq v 0 then s {LapicEoi: NoIntr}
{LapicEsrClrPen: false}
else s
| LAPIC_TPR ⇒ s {LapicTpr: v}
{LapicEsrClrPen: false}
end
| None ⇒ s
end
| OpInput addr ⇒
s {LapicEsrClrPen: false}
end
end.
Function lapic_trans_intr (n: Z) (s: LApicState) : LApicState :=
match s with
| mkLApicState esr eoi maxLvt enable spurious lint0m lint1m pcm ldr errIrq esrClr tpr
⇒
if zle_le TRAPNO_EXCEPTIONS_BEGIN n TRAPNO_EXCEPTIONS_END
then s {LapicEoi: IntrException n}
else if zle_le TRAPNO_IOAPIC_BEGIN n TRAPNO_IOAPIC_END
then s {LapicEoi: IntrIoApic n}
else if zeq n TRAPNO_SYSCALL then s {LapicEoi: IntrSyscall n}
else s
end.
Function lapic_valid_write_range (idx: Z) : bool :=
((zeq idx 8) || (zeq idx 32) || (zeq idx 44) || (zeq idx 52) || (zeq idx 56)
|| (zeq idx 60) || (zeq idx 52) || (zeq idx 160)
|| (zle_le 188 idx 224) || (zeq idx 248)).
Function lapic_write_spec (addr: Z) (v: Z) (abd: RData): option RData :=
if lapic_valid_write_range addr
then
if zeq addr LAPIC_IDX_EOI then
Some (abd {lapic / s: lapic_trans_cpu (OpOutput addr v) (s (lapic abd))}
{ioapic / s / CurrentIrq: None})
else
Some (abd {lapic / s: lapic_trans_cpu (OpOutput addr v) (s (lapic abd))})
else
None.
Function lapic_read_ver (s: LApicState): Z :=
s.(LapicMaxLvt) × 2^16.
Function lapic_read_spec (addr: Z) (abd: RData): option (RData × Z) :=
if zeq addr 12 then
Some (abd {lapic / s: (lapic_trans_cpu (OpInput addr) (s (lapic abd)))},
lapic_read_ver (s (lapic abd)))
else
None.
Function lapic_intr (irq: Z) (abd: RData): RData :=
abd {lapic / s: lapic_trans_intr irq (s (lapic abd))}.
End lAPIC.
Section CPU.
Function cli_spec (abd: RData): option RData :=
Some (abd {intr_flag: false}).
Function sti_spec (abd: RData): option RData :=
Some (abd {intr_flag: true}).
Function local_irq_save_spec (abd: RData): option RData :=
match (init abd, ikern abd, ihost abd) with
| (true, true, true) ⇒
Some abd {saved_intr_flags: (saved_intr_flags abd) ++ (intr_flag abd::nil)} {intr_flag: false}
| _ ⇒ None
end.
Function local_irq_restore_spec (abd: RData): option RData :=
match (init abd, ikern abd, ihost abd) with
| (true, true, true) ⇒
match saved_intr_flags abd with
| nil ⇒ None
| _ ⇒ Some abd {saved_intr_flags: removelast (saved_intr_flags abd)} {intr_flag: last (saved_intr_flags abd) false}
end
| _ ⇒ None
end.
Function cpu_intr (irq: Z) (abd: RData): RData :=
if intr_flag abd then
abd {curr_intr_num: irq}
{intr_flag: false}
{in_intr: true}
else
abd.
Function iret_spec (abd: RData): option RData :=
Some (abd {curr_intr_num: 256}
{intr_flag: true}
{in_intr: false}
).
End CPU.
Section TRAP_HANDLER.
Function hw_intr_trans (irq: Z) (abd: RData): RData × (option Z) :=
let s_ioapic´ := ioapic_trans_intr (IRQ irq) (s (ioapic abd)) in
match CurrentIrq s_ioapic´ with
| Some (n, lapicid) ⇒
let s_lapic´ := lapic_trans_intr n (s (lapic abd)) in
match LapicEoi s_lapic´ with
| IntrIoApic m ⇒
if intr_flag abd then
(abd {curr_intr_num: irq}
{intr_flag: false}
{in_intr: true}
{ioapic / s: s_ioapic´}
{lapic / s: s_lapic´}, Some m)
else
(abd, None)
| _ ⇒ (abd, None)
end
| None ⇒ (abd, None)
end.
Function ic_intr_spec (irq: Z) (abd: RData): option (RData × Z) :=
match hw_intr_trans irq abd with
| (abd´, Some n) ⇒
if zle_le 32 n 47 then Some (abd´, n)
else Some (abd, 0)
| (abd´, None) ⇒ Some (abd´, 0)
end.
Function device_hw_intr {T: Type} (device_intr: DeviceData T → DeviceData T)
(get_device: RData → DeviceData T)
(is_irq_pending: T → bool)
(update_device: RData → DeviceData T → RData)
irq (abd: RData): option (RData × Z) :=
let d´ := device_intr (get_device abd) in
if is_irq_pending d´.(s) then
match hw_intr_trans irq abd with
| (abd´, Some n) ⇒ Some (update_device abd´ d´, n)
| (abd´, None) ⇒ Some (update_device abd´ d´, 0)
end
else
Some (update_device abd d´, 0).
Function serial_intr (d: SerialData): SerialData :=
d {s: serial_trans_env (SerialEnv d.(l1)) d.(s)}
{l2: d.(l1) + 1}.
Function serial_irq_check_spec (abd: RData): Z :=
if SerialIrq (serial_intr abd.(com1)).(s) then 1 else 0.
Function serial_irq_current_spec (abd: RData): Z :=
if SerialIrq abd.(com1).(s) then 1 else 0.
Function serial_get_device (abd: RData): SerialData :=
com1 abd.
Function serial_is_irq_pending (s: SerialState): bool :=
SerialIrq s.
Function serial_update_device (abd: RData) (d: SerialData): RData :=
abd {com1: d}.
Definition SERIAL_IRQ := 4.
serial hardware interrupt handler
Function serial_hw_intr_spec´ (abd: RData): option (RData × Z) :=
device_hw_intr serial_intr serial_get_device serial_is_irq_pending
serial_update_device SERIAL_IRQ abd.
device_hw_intr serial_intr serial_get_device serial_is_irq_pending
serial_update_device SERIAL_IRQ abd.
unfold of serial_hw_intr
Require Import Integers.
Function serial_hw_intr_spec (abd: RData): option (RData × Z) :=
let d´ := serial_intr abd.(com1) in
if SerialIrq d´.(s) then
match hw_intr_trans 4 abd with
| (abd´, Some n) ⇒
if zle_le 32 n 47 then
Some (abd´ {com1: d´}, n)
else Some (abd {com1: d´}, 0)
| (abd´, None) ⇒ Some (abd´ {com1: d´}, 0)
end
else
None.
Function serial_hw_intr_spec (abd: RData): option (RData × Z) :=
let d´ := serial_intr abd.(com1) in
if SerialIrq d´.(s) then
match hw_intr_trans 4 abd with
| (abd´, Some n) ⇒
if zle_le 32 n 47 then
Some (abd´ {com1: d´}, n)
else Some (abd {com1: d´}, 0)
| (abd´, None) ⇒ Some (abd´ {com1: d´}, 0)
end
else
None.
keyboard
Require Import ObjKeyboard.
Function keyboard_intr (d: KeyboardData): KeyboardData :=
d {s: keyboard_trans_env (KeyboardEnv d.(l1)) d.(s)}
{l2: d.(l1) + 1}.
Function keyboard_hw_intr_spec (abd: RData): option (RData × Z) :=
let d´ := keyboard_intr abd.(kbd) in
if KbdIrq d´.(s) then
match hw_intr_trans 1 abd with
| (abd´, Some n) ⇒
if zle_le 32 n 47 then
Some (abd´ {kbd: d´}, n)
else Some (abd {kbd: d´}, 0)
| (abd´, None) ⇒ Some (abd´ {kbd: d´}, 0)
end
else
None.
End TRAP_HANDLER.
End OBJ_InterruptController.
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_HW_INTR_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_com1}.
Context {re3: relate_impl_ioapic}.
Context {re4: relate_impl_lapic}.
Context {re5: relate_impl_intr_flag}.
Context {re6: relate_impl_curr_intr_num}.
Context {re7: relate_impl_in_intr}.
Lemma serial_hw_intr_exist:
∀ s habd habd´ labd i f,
serial_hw_intr_spec habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_hw_intr_spec labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_hw_intr_spec; intros.
revert H. subrewrite.
unfold hw_intr_trans in ×.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subst.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_in_intr_update; eauto;
try apply relate_impl_intr_flag_update; eauto;
try apply relate_impl_curr_intr_num_update; eauto
).
Qed.
Context {mt1: match_impl_com1}.
Context {mt2: match_impl_ioapic}.
Context {mt3: match_impl_lapic}.
Context {mt4: match_impl_intr_flag}.
Context {mt5: match_impl_curr_intr_num}.
Context {mt6: match_impl_in_intr}.
Lemma serial_hw_intr_match:
∀ s d d´ m i f,
serial_hw_intr_spec d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold serial_hw_intr_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_in_intr_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_hw_intr_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_hw_intr_spec}.
Lemma serial_hw_intr_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_hw_intr_spec)
(id ↦ gensem serial_hw_intr_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_hw_intr_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_hw_intr_match; eauto.
Qed.
End SERIAL_HW_INTR_SIM.
Section IC_INTR_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_ioapic}.
Context {re4: relate_impl_lapic}.
Context {re5: relate_impl_intr_flag}.
Context {re6: relate_impl_curr_intr_num}.
Context {re7: relate_impl_in_intr}.
Lemma ic_intr_exist:
∀ s habd habd´ labd irq i f,
ic_intr_spec irq habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ic_intr_spec irq labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ic_intr_spec; intros.
revert H. subrewrite.
unfold hw_intr_trans in ×.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subst.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H1; try rewrite H2;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_in_intr_update; eauto;
try apply relate_impl_intr_flag_update; eauto;
try apply relate_impl_curr_intr_num_update; eauto
).
Qed.
Context {mt2: match_impl_ioapic}.
Context {mt3: match_impl_lapic}.
Context {mt4: match_impl_intr_flag}.
Context {mt5: match_impl_curr_intr_num}.
Context {mt6: match_impl_in_intr}.
Lemma ic_intr_match:
∀ s d d´ m irq i f,
ic_intr_spec irq d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ic_intr_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_in_intr_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ic_intr_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ic_intr_spec}.
Lemma ic_intr_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ic_intr_spec)
(id ↦ gensem ic_intr_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ic_intr_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ic_intr_match; eauto.
Qed.
End IC_INTR_SIM.
Section SERIAL_IRQ_CURRENT_SIM.
Context {re1: relate_impl_com1}.
Lemma serial_irq_current_exist:
∀ s habd labd z f,
serial_irq_current_spec habd = z
→ relate_AbData s f habd labd
→ serial_irq_current_spec labd = z.
Proof.
unfold serial_irq_current_spec; intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H; subrewrite.
Qed.
Lemma serial_irq_current_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_irq_current_spec)
(id ↦ gensem serial_irq_current_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite serial_irq_current_exist; eauto. reflexivity.
Qed.
End SERIAL_IRQ_CURRENT_SIM.
Section SERIAL_IRQ_CHECK_SIM.
Context {re1: relate_impl_com1}.
Lemma serial_irq_check_exist:
∀ s habd labd z f,
serial_irq_check_spec habd = z
→ relate_AbData s f habd labd
→ serial_irq_check_spec labd = z.
Proof.
unfold serial_irq_check_spec; intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H; subrewrite.
Qed.
Lemma serial_irq_check_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_irq_check_spec)
(id ↦ gensem serial_irq_check_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite serial_irq_check_exist; eauto. reflexivity.
Qed.
End SERIAL_IRQ_CHECK_SIM.
Section CLI_SIM.
Context {re1: relate_impl_iflags}.
Context {re5: relate_impl_intr_flag}.
Lemma cli_exist:
∀ s habd habd´ labd f,
cli_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, cli_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold cli_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt4: match_impl_intr_flag}.
Lemma cli_match:
∀ s d d´ m f,
cli_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold cli_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) cli_spec}.
Context {inv0: PreservesInvariants (HD:= data0) cli_spec}.
Lemma cli_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem cli_spec)
(id ↦ gensem cli_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
apply relate_impl_intr_flag_update; eauto.
eapply cli_match; eauto.
unfold cli_spec; reflexivity.
Qed.
End CLI_SIM.
Section STI_SIM.
Context {re1: relate_impl_iflags}.
Context {re5: relate_impl_intr_flag}.
Lemma sti_exist:
∀ s habd habd´ labd f,
sti_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, sti_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold sti_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt4: match_impl_intr_flag}.
Lemma sti_match:
∀ s d d´ m f,
sti_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold sti_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) sti_spec}.
Context {inv0: PreservesInvariants (HD:= data0) sti_spec}.
Lemma sti_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem sti_spec)
(id ↦ gensem sti_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
apply relate_impl_intr_flag_update; eauto.
eapply sti_match; eauto.
unfold sti_spec; reflexivity.
Qed.
End STI_SIM.
Section LOCAL_IRQ_SAVE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_saved_intr_flags}.
Lemma local_irq_save_exist:
∀ s habd habd´ labd f,
local_irq_save_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, local_irq_save_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold local_irq_save_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_saved_intr_flags_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst.
rewrite <- ikern_eq, <- ihost_eq.
reflexivity.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_saved_intr_flags_update; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_saved_intr_flags}.
Lemma local_irq_save_match:
∀ s d d´ m f,
local_irq_save_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold local_irq_save_spec; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update;
try eapply match_impl_saved_intr_flags_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) local_irq_save_spec}.
Context {inv0: PreservesInvariants (HD:= data0) local_irq_save_spec}.
Lemma local_irq_save_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem local_irq_save_spec)
(id ↦ gensem local_irq_save_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit local_irq_save_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply local_irq_save_match; eauto.
Qed.
End LOCAL_IRQ_SAVE_SIM.
Section LOCAL_IRQ_RESTORE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_saved_intr_flags}.
Lemma local_irq_restore_exist:
∀ s habd habd´ labd f,
local_irq_restore_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, local_irq_restore_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold local_irq_restore_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_saved_intr_flags_eq; eauto; inversion 1.
Opaque removelast last.
subdestruct;
inv HQ; refine_split´; trivial; subst.
rewrite <- ikern_eq, <- ihost_eq.
reflexivity.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_saved_intr_flags_update; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_saved_intr_flags}.
Lemma local_irq_restore_match:
∀ s d d´ m f,
local_irq_restore_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold local_irq_restore_spec; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update;
try eapply match_impl_saved_intr_flags_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) local_irq_restore_spec}.
Context {inv0: PreservesInvariants (HD:= data0) local_irq_restore_spec}.
Lemma local_irq_restore_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem local_irq_restore_spec)
(id ↦ gensem local_irq_restore_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit local_irq_restore_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply local_irq_restore_match; eauto.
Qed.
End LOCAL_IRQ_RESTORE_SIM.
Section IRET_SIM.
Context {re1: relate_impl_intr_flag}.
Context {re2: relate_impl_curr_intr_num}.
Context {re3: relate_impl_in_intr}.
Lemma iret_exist:
∀ s habd habd´ labd f,
iret_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, iret_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold iret_spec; intros.
revert H. subrewrite.
exploit relate_impl_curr_intr_num_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_curr_intr_num}.
Context {mt3: match_impl_in_intr}.
Lemma iret_match:
∀ s d d´ m f,
iret_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold iret_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial.
eapply match_impl_in_intr_update.
eapply match_impl_intr_flag_update.
eapply match_impl_curr_intr_num_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) iret_spec}.
Context {inv0: PreservesInvariants (HD:= data0) iret_spec}.
Lemma iret_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem iret_spec)
(id ↦ gensem iret_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
eapply iret_match; eauto.
unfold iret_spec; reflexivity.
Qed.
End IRET_SIM.
Section IOAPIC_READ_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_ioapic}.
Lemma ioapic_read_exist:
∀ s habd habd´ labd addr i f,
ioapic_read_spec addr habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_read_spec addr labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_read_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt2: match_impl_ioapic}.
Lemma ioapic_read_match:
∀ s d d´ m addr i f,
ioapic_read_spec addr d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_read_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_read_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_read_spec}.
Lemma ioapic_read_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_read_spec)
(id ↦ gensem ioapic_read_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_read_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_read_match; eauto.
Qed.
End IOAPIC_READ_SIM.
Section IOAPIC_WRITE_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_ioapic}.
Lemma ioapic_write_exist:
∀ s habd habd´ labd addr i f,
ioapic_write_spec addr i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_write_spec addr i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_write_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt2: match_impl_ioapic}.
Lemma ioapic_write_match:
∀ s d d´ m addr i f,
ioapic_write_spec addr i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_write_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_write_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_write_spec}.
Lemma ioapic_write_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_write_spec)
(id ↦ gensem ioapic_write_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_write_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_write_match; eauto.
Qed.
End IOAPIC_WRITE_SIM.
Section LAPIC_READ_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_lapic}.
Lemma lapic_read_exist:
∀ s habd habd´ labd addr i f,
lapic_read_spec addr habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, lapic_read_spec addr labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lapic_read_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt2: match_impl_lapic}.
Lemma lapic_read_match:
∀ s d d´ m addr i f,
lapic_read_spec addr d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lapic_read_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_lapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) lapic_read_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lapic_read_spec}.
Lemma lapic_read_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lapic_read_spec)
(id ↦ gensem lapic_read_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lapic_read_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lapic_read_match; eauto.
Qed.
End LAPIC_READ_SIM.
Section LAPIC_WRITE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_lapic}.
Context {re3: relate_impl_ioapic}.
Lemma lapic_write_exist:
∀ s habd habd´ labd addr i f,
lapic_write_spec addr i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, lapic_write_spec addr i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lapic_write_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt1: match_impl_lapic}.
Context {mt2: match_impl_ioapic}.
Lemma lapic_write_match:
∀ s d d´ m addr i f,
lapic_write_spec addr i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lapic_write_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_lapic_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
); eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) lapic_write_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lapic_write_spec}.
Lemma lapic_write_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lapic_write_spec)
(id ↦ gensem lapic_write_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lapic_write_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lapic_write_match; eauto.
Qed.
End LAPIC_WRITE_SIM.
End OBJ_SIM.
Function keyboard_intr (d: KeyboardData): KeyboardData :=
d {s: keyboard_trans_env (KeyboardEnv d.(l1)) d.(s)}
{l2: d.(l1) + 1}.
Function keyboard_hw_intr_spec (abd: RData): option (RData × Z) :=
let d´ := keyboard_intr abd.(kbd) in
if KbdIrq d´.(s) then
match hw_intr_trans 1 abd with
| (abd´, Some n) ⇒
if zle_le 32 n 47 then
Some (abd´ {kbd: d´}, n)
else Some (abd {kbd: d´}, 0)
| (abd´, None) ⇒ Some (abd´ {kbd: d´}, 0)
end
else
None.
End TRAP_HANDLER.
End OBJ_InterruptController.
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_HW_INTR_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_com1}.
Context {re3: relate_impl_ioapic}.
Context {re4: relate_impl_lapic}.
Context {re5: relate_impl_intr_flag}.
Context {re6: relate_impl_curr_intr_num}.
Context {re7: relate_impl_in_intr}.
Lemma serial_hw_intr_exist:
∀ s habd habd´ labd i f,
serial_hw_intr_spec habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_hw_intr_spec labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_hw_intr_spec; intros.
revert H. subrewrite.
unfold hw_intr_trans in ×.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subst.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_in_intr_update; eauto;
try apply relate_impl_intr_flag_update; eauto;
try apply relate_impl_curr_intr_num_update; eauto
).
Qed.
Context {mt1: match_impl_com1}.
Context {mt2: match_impl_ioapic}.
Context {mt3: match_impl_lapic}.
Context {mt4: match_impl_intr_flag}.
Context {mt5: match_impl_curr_intr_num}.
Context {mt6: match_impl_in_intr}.
Lemma serial_hw_intr_match:
∀ s d d´ m i f,
serial_hw_intr_spec d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold serial_hw_intr_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_in_intr_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_hw_intr_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_hw_intr_spec}.
Lemma serial_hw_intr_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_hw_intr_spec)
(id ↦ gensem serial_hw_intr_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_hw_intr_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_hw_intr_match; eauto.
Qed.
End SERIAL_HW_INTR_SIM.
Section IC_INTR_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_ioapic}.
Context {re4: relate_impl_lapic}.
Context {re5: relate_impl_intr_flag}.
Context {re6: relate_impl_curr_intr_num}.
Context {re7: relate_impl_in_intr}.
Lemma ic_intr_exist:
∀ s habd habd´ labd irq i f,
ic_intr_spec irq habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ic_intr_spec irq labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ic_intr_spec; intros.
revert H. subrewrite.
unfold hw_intr_trans in ×.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subst.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H1; try rewrite H2;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_in_intr_update; eauto;
try apply relate_impl_intr_flag_update; eauto;
try apply relate_impl_curr_intr_num_update; eauto
).
Qed.
Context {mt2: match_impl_ioapic}.
Context {mt3: match_impl_lapic}.
Context {mt4: match_impl_intr_flag}.
Context {mt5: match_impl_curr_intr_num}.
Context {mt6: match_impl_in_intr}.
Lemma ic_intr_match:
∀ s d d´ m irq i f,
ic_intr_spec irq d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ic_intr_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_in_intr_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ic_intr_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ic_intr_spec}.
Lemma ic_intr_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ic_intr_spec)
(id ↦ gensem ic_intr_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ic_intr_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ic_intr_match; eauto.
Qed.
End IC_INTR_SIM.
Section SERIAL_IRQ_CURRENT_SIM.
Context {re1: relate_impl_com1}.
Lemma serial_irq_current_exist:
∀ s habd labd z f,
serial_irq_current_spec habd = z
→ relate_AbData s f habd labd
→ serial_irq_current_spec labd = z.
Proof.
unfold serial_irq_current_spec; intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H; subrewrite.
Qed.
Lemma serial_irq_current_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_irq_current_spec)
(id ↦ gensem serial_irq_current_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite serial_irq_current_exist; eauto. reflexivity.
Qed.
End SERIAL_IRQ_CURRENT_SIM.
Section SERIAL_IRQ_CHECK_SIM.
Context {re1: relate_impl_com1}.
Lemma serial_irq_check_exist:
∀ s habd labd z f,
serial_irq_check_spec habd = z
→ relate_AbData s f habd labd
→ serial_irq_check_spec labd = z.
Proof.
unfold serial_irq_check_spec; intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H; subrewrite.
Qed.
Lemma serial_irq_check_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_irq_check_spec)
(id ↦ gensem serial_irq_check_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite serial_irq_check_exist; eauto. reflexivity.
Qed.
End SERIAL_IRQ_CHECK_SIM.
Section CLI_SIM.
Context {re1: relate_impl_iflags}.
Context {re5: relate_impl_intr_flag}.
Lemma cli_exist:
∀ s habd habd´ labd f,
cli_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, cli_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold cli_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt4: match_impl_intr_flag}.
Lemma cli_match:
∀ s d d´ m f,
cli_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold cli_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) cli_spec}.
Context {inv0: PreservesInvariants (HD:= data0) cli_spec}.
Lemma cli_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem cli_spec)
(id ↦ gensem cli_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
apply relate_impl_intr_flag_update; eauto.
eapply cli_match; eauto.
unfold cli_spec; reflexivity.
Qed.
End CLI_SIM.
Section STI_SIM.
Context {re1: relate_impl_iflags}.
Context {re5: relate_impl_intr_flag}.
Lemma sti_exist:
∀ s habd habd´ labd f,
sti_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, sti_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold sti_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt4: match_impl_intr_flag}.
Lemma sti_match:
∀ s d d´ m f,
sti_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold sti_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) sti_spec}.
Context {inv0: PreservesInvariants (HD:= data0) sti_spec}.
Lemma sti_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem sti_spec)
(id ↦ gensem sti_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
apply relate_impl_intr_flag_update; eauto.
eapply sti_match; eauto.
unfold sti_spec; reflexivity.
Qed.
End STI_SIM.
Section LOCAL_IRQ_SAVE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_saved_intr_flags}.
Lemma local_irq_save_exist:
∀ s habd habd´ labd f,
local_irq_save_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, local_irq_save_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold local_irq_save_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_saved_intr_flags_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst.
rewrite <- ikern_eq, <- ihost_eq.
reflexivity.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_saved_intr_flags_update; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_saved_intr_flags}.
Lemma local_irq_save_match:
∀ s d d´ m f,
local_irq_save_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold local_irq_save_spec; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update;
try eapply match_impl_saved_intr_flags_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) local_irq_save_spec}.
Context {inv0: PreservesInvariants (HD:= data0) local_irq_save_spec}.
Lemma local_irq_save_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem local_irq_save_spec)
(id ↦ gensem local_irq_save_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit local_irq_save_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply local_irq_save_match; eauto.
Qed.
End LOCAL_IRQ_SAVE_SIM.
Section LOCAL_IRQ_RESTORE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_saved_intr_flags}.
Lemma local_irq_restore_exist:
∀ s habd habd´ labd f,
local_irq_restore_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, local_irq_restore_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold local_irq_restore_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_saved_intr_flags_eq; eauto; inversion 1.
Opaque removelast last.
subdestruct;
inv HQ; refine_split´; trivial; subst.
rewrite <- ikern_eq, <- ihost_eq.
reflexivity.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_saved_intr_flags_update; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_saved_intr_flags}.
Lemma local_irq_restore_match:
∀ s d d´ m f,
local_irq_restore_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold local_irq_restore_spec; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_intr_flag_update;
try eapply match_impl_saved_intr_flags_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) local_irq_restore_spec}.
Context {inv0: PreservesInvariants (HD:= data0) local_irq_restore_spec}.
Lemma local_irq_restore_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem local_irq_restore_spec)
(id ↦ gensem local_irq_restore_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit local_irq_restore_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply local_irq_restore_match; eauto.
Qed.
End LOCAL_IRQ_RESTORE_SIM.
Section IRET_SIM.
Context {re1: relate_impl_intr_flag}.
Context {re2: relate_impl_curr_intr_num}.
Context {re3: relate_impl_in_intr}.
Lemma iret_exist:
∀ s habd habd´ labd f,
iret_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, iret_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold iret_spec; intros.
revert H. subrewrite.
exploit relate_impl_curr_intr_num_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_curr_intr_num}.
Context {mt3: match_impl_in_intr}.
Lemma iret_match:
∀ s d d´ m f,
iret_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold iret_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial.
eapply match_impl_in_intr_update.
eapply match_impl_intr_flag_update.
eapply match_impl_curr_intr_num_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) iret_spec}.
Context {inv0: PreservesInvariants (HD:= data0) iret_spec}.
Lemma iret_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem iret_spec)
(id ↦ gensem iret_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
eapply iret_match; eauto.
unfold iret_spec; reflexivity.
Qed.
End IRET_SIM.
Section IOAPIC_READ_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_ioapic}.
Lemma ioapic_read_exist:
∀ s habd habd´ labd addr i f,
ioapic_read_spec addr habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_read_spec addr labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_read_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt2: match_impl_ioapic}.
Lemma ioapic_read_match:
∀ s d d´ m addr i f,
ioapic_read_spec addr d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_read_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_read_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_read_spec}.
Lemma ioapic_read_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_read_spec)
(id ↦ gensem ioapic_read_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_read_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_read_match; eauto.
Qed.
End IOAPIC_READ_SIM.
Section IOAPIC_WRITE_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_ioapic}.
Lemma ioapic_write_exist:
∀ s habd habd´ labd addr i f,
ioapic_write_spec addr i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_write_spec addr i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_write_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt2: match_impl_ioapic}.
Lemma ioapic_write_match:
∀ s d d´ m addr i f,
ioapic_write_spec addr i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_write_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_write_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_write_spec}.
Lemma ioapic_write_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_write_spec)
(id ↦ gensem ioapic_write_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_write_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_write_match; eauto.
Qed.
End IOAPIC_WRITE_SIM.
Section LAPIC_READ_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_lapic}.
Lemma lapic_read_exist:
∀ s habd habd´ labd addr i f,
lapic_read_spec addr habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, lapic_read_spec addr labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lapic_read_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt2: match_impl_lapic}.
Lemma lapic_read_match:
∀ s d d´ m addr i f,
lapic_read_spec addr d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lapic_read_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_lapic_update;
try eapply match_impl_lapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
);
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) lapic_read_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lapic_read_spec}.
Lemma lapic_read_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lapic_read_spec)
(id ↦ gensem lapic_read_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lapic_read_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lapic_read_match; eauto.
Qed.
End LAPIC_READ_SIM.
Section LAPIC_WRITE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_lapic}.
Context {re3: relate_impl_ioapic}.
Lemma lapic_write_exist:
∀ s habd habd´ labd addr i f,
lapic_write_spec addr i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, lapic_write_spec addr i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lapic_write_spec; intros.
revert H. subrewrite.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
subdestruct;
inv HQ; refine_split´; trivial; subst;
repeat (
try rewrite H4; try rewrite H2;
try apply relate_impl_com1_update; eauto;
try apply relate_impl_lapic_update; eauto;
try apply relate_impl_ioapic_update; eauto;
try apply relate_impl_intr_flag_update; eauto
).
Qed.
Context {mt1: match_impl_lapic}.
Context {mt2: match_impl_ioapic}.
Lemma lapic_write_match:
∀ s d d´ m addr i f,
lapic_write_spec addr i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lapic_write_spec; unfold hw_intr_trans; intros.
subdestruct; inv H; trivial;
repeat(
try eapply match_impl_com1_update;
try eapply match_impl_lapic_update;
try eapply match_impl_ioapic_update;
try eapply match_impl_intr_flag_update;
try eapply match_impl_curr_intr_num_update
); eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) lapic_write_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lapic_write_spec}.
Lemma lapic_write_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lapic_write_spec)
(id ↦ gensem lapic_write_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lapic_write_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lapic_write_match; eauto.
Qed.
End LAPIC_WRITE_SIM.
End OBJ_SIM.