Library mcertikos.dev.ObjInterruptController
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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.