Library mcertikos.objects.dev.ObjInterruptDriver
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 ObjInterruptController.
Require Import ListLemma.
Require Import XOmega.
Section OBJ_InterruptDriver.
Notation T_IRQ0 := 32.
Section ioAPIC.
Function is_ioapic_init_spec (abd: RData): option Z :=
match (ikern abd, init abd, ihost abd) with
| (true, true, true) ⇒
if IoApicInit (s (ioapic abd)) then Some 1 else Some 0
| _ ⇒ None
end.
Function set_ioapic_init_spec (abd: RData): option (RData) :=
match (ikern abd, init abd, ihost abd) with
| (true, true, true) ⇒
Some (abd {ioapic / s / IoApicInit: true})
| _ ⇒ None
end.
Function disable_irq (s: IoApicState) (n: nat): IoApicState :=
(s {IoApicIrqs[n]: T_IRQ0 + Z.of_nat n} {IoApicEnables[n]: false}).
Lemma disable_irq_id:
∀ n s,
disable_irq (disable_irq s n) n = disable_irq s n.
Proof.
intros. unfold disable_irq.
Opaque Z.add Z.mul.
unfold_IoApicState; simpl.
repeat rewrite replace_replace. reflexivity.
Qed.
Lemma disable_irq_comm:
∀ s n m,
n ≠ m →
disable_irq (disable_irq s n) m = disable_irq (disable_irq s m) n.
Proof.
Opaque Z.add.
unfold disable_irq. unfold_IoApicState; simpl.
destruct s; simpl.
intros. f_equal; rewrite replace_comm; try reflexivity.
omega. omega.
Qed.
Fixpoint ioapic_init_aux (s: IoApicState) (n: nat): IoApicState :=
match n with
| O ⇒ disable_irq s 0
| S n´ ⇒ disable_irq (ioapic_init_aux s n´) n
end.
Lemma disable_irq_init_step:
∀ n d,
disable_irq (ioapic_init_aux d n) (S n) = ioapic_init_aux d (S n).
Proof.
intros. reflexivity.
Qed.
Lemma nth_error_range: ∀ T n l, ∀ v: T,
nth_error l n = Some v →
Z.of_nat n < Z.of_nat (length l) .
Proof.
intros.
generalize dependent n.
induction l.
intros.
simpl in ×.
destruct n.
simpl in ×.
inv H.
simpl in ×.
inv H.
intros.
assert(Z.of_nat n = 0 ∨ Z.of_nat n > 0) by xomega.
case_eq H0; intros.
assert (n = O) by xomega.
subst.
rewrite <- length_cons.
rewrite Nat2Z.inj_succ.
unfold Z.succ.
xomega.
Opaque Z.of_nat.
assert (Z.of_nat (pred n) < Z.of_nat (length l)).
{
eapply IHl; eauto.
destruct n.
change (Z.of_nat 0) with 0 in g.
omega.
simpl in ×.
assumption.
}
rewrite <- length_cons.
rewrite Nat2Z.inj_succ.
unfold Z.succ.
xomega.
Qed.
Lemma replace_preserves_length: ∀ T l n, ∀ v: T,
length l = length (replace v n l).
Proof.
intros.
generalize dependent n.
induction l.
simpl.
destruct n; reflexivity.
simpl in ×.
destruct n.
simpl.
reflexivity.
simpl in ×.
f_equal.
eapply IHl; eauto.
Qed.
Lemma ioapic_init_aux_preserves_ioapicirq_length:
∀ s n,
Z.of_nat (length (IoApicIrqs s)) = Z.of_nat (length (IoApicIrqs (ioapic_init_aux s n))).
Proof.
Opaque Z.add.
intros.
induction n.
{
simpl.
destruct (IoApicIrqs s).
simpl.
reflexivity.
simpl.
reflexivity.
}
{
simpl.
destruct (IoApicIrqs (ioapic_init_aux s n)).
simpl in ×.
assumption.
simpl in ×.
rewrite <- replace_preserves_length.
assumption.
}
Qed.
Lemma ioapic_init_aux_preserves_ioapicenables_length:
∀ s n,
Z.of_nat (length (IoApicEnables s)) = Z.of_nat (length (IoApicEnables (ioapic_init_aux s n))).
Proof.
Opaque Z.add.
intros.
induction n.
{
simpl.
destruct (IoApicEnables s).
simpl.
reflexivity.
simpl.
reflexivity.
}
{
simpl.
destruct (IoApicEnables (ioapic_init_aux s n)).
simpl in ×.
assumption.
simpl in ×.
rewrite <- replace_preserves_length.
assumption.
}
Qed.
Lemma replace_gss:
∀ T n l, ∀ v: T,
Z.of_nat n < Z.of_nat (length l) →
nth_error (replace v n l) n = value v.
Proof.
intros.
generalize dependent n.
induction l.
simpl.
intros.
xomega.
simpl in ×.
destruct n.
simpl.
reflexivity.
simpl in ×.
intros.
eapply IHl; eauto.
xomega.
Qed.
Lemma ntheq: ∀ T n1 n2 l, ∀ v: T, n1 ≠ n2 → nth_error (replace v n2 l) n1 = nth_error l n1.
Proof.
intros.
generalize dependent n1.
generalize dependent n2.
induction l.
simpl.
intros.
destruct n2; reflexivity.
intros.
simpl.
destruct n2.
destruct n1.
xomega.
simpl.
reflexivity.
destruct n1.
simpl.
reflexivity.
simpl.
eapply IHl; eauto.
Qed.
Function ioapic_init_spec (abd: RData): option RData :=
match (init abd, ikern abd, ihost abd) with
| (false, true, true) ⇒
let n := abd.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (abd.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (abd.(ioapic).(s).(IoApicEnables))) then
Some (abd {ioapic/s: ioapic_init_aux abd.(ioapic).(s) (Z.to_nat (n - 1))})
else
None
else
None
| _ ⇒ None
end.
Function ioapic_enable_spec (irq: Z) (lapicid: Z) (trigger: Z) (polarity: Z) (abd: RData): option RData :=
match (init abd, ikern abd, ihost abd) with
| (true, true, true) ⇒
if zle_le 0 irq (IoApicMaxIntr (s (ioapic abd))) then
if zle_le 0 lapicid 15 then
if zle_le 0 trigger 1 then
if zle_le 0 polarity 1 then
let idx := Z.to_nat irq in
Some (abd {ioapic: (ioapic abd)
{s: (s (ioapic abd))
{IoApicIrqs[idx]: irq + IRQ0}
{IoApicEnables[idx]: true}
}
})
else None
else None
else None
else None
| _ ⇒ None
end.
Function ioapic_mask_spec (irq: Z) (abd: RData) : option RData :=
match (init abd, ikern abd, ihost abd) with
| (true, true, true) ⇒
if zle_lt 0 irq (Zlength (abd.(ioapic).(s).(IoApicEnables))) then
Some (abd {ioapic / s / IoApicEnables [(Z.to_nat irq)]: false})
else
None
| _ ⇒ None
end.
Function ioapic_unmask_spec (irq: Z) (abd: RData) : option RData :=
match (init abd, ikern abd, ihost abd) with
| (true, true, true) ⇒
if zle_lt 0 irq (Zlength (abd.(ioapic).(s).(IoApicEnables))) then
Some (abd {ioapic / s / IoApicEnables [(Z.to_nat irq)]: true})
else
None
| _ ⇒ None
end.
End ioAPIC.
Section lAPIC.
Function lapic_init_spec (abd: RData): option RData :=
match (init abd, ikern abd, ihost abd) with
| (true, true, true) ⇒
Some (abd {lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic abd))) true
(T_IRQ0 + 7) true true true 0 50 false 0))
{l1: l1 (lapic abd)}
{l2: l2 (lapic abd)}
{l3: l3 (lapic abd)}
}
{ioapic / s / CurrentIrq: None}
)
| _ ⇒ None
end.
Function lapic_eoi_spec (abd: RData): option RData :=
match (init abd, ikern abd, ihost abd, in_intr abd) with
| (true, true, true, true) ⇒
Some (abd {lapic: (lapic abd)
{s: (s (lapic abd))
{LapicEoi: NoIntr}
{LapicEsrClrPen: false}
}
}
{ioapic: (ioapic abd)
{s: (s (ioapic abd))
{CurrentIrq: None}
}
}
)
| _ ⇒ None
end.
End lAPIC.
Section TRAP_HANDLER.
End TRAP_HANDLER.
End OBJ_InterruptDriver.
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 IOAPIC_INIT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ioapic}.
Context {re3: relate_impl_init}.
Lemma ioapic_init_exist:
∀ s habd habd´ labd f,
ioapic_init_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_init_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_init_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct. inv HQ; refine_split´; trivial.
apply relate_impl_ioapic_update; eauto.
Qed.
Context {mt1: match_impl_ioapic}.
Lemma ioapic_init_match:
∀ s d d´ m f,
ioapic_init_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ioapic_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_init_spec}.
Lemma ioapic_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_init_spec)
(id ↦ gensem ioapic_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_init_match; eauto.
Qed.
End IOAPIC_INIT_SIM.
Section IOAPIC_ENABLE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_ioapic}.
Lemma ioapic_enable_exist:
∀ s habd habd´ labd f (irq: Z) (lapicid: Z) (trigger: Z) (polarity: Z),
ioapic_enable_spec irq lapicid trigger polarity habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_enable_spec irq lapicid trigger polarity labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_enable_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct. inv HQ; refine_split´; trivial.
apply relate_impl_ioapic_update; eauto.
Qed.
Context {mt1: match_impl_ioapic}.
Lemma ioapic_enable_match:
∀ s d d´ m f irq lapicid trigger polarity,
ioapic_enable_spec irq lapicid trigger polarity d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_enable_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ioapic_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_enable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_enable_spec}.
Lemma ioapic_enable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_enable_spec)
(id ↦ gensem ioapic_enable_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_enable_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_enable_match; eauto.
Qed.
End IOAPIC_ENABLE_SIM.
Section IOAPIC_MASK_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_ioapic}.
Lemma ioapic_mask_exist:
∀ s habd habd´ labd f (irq: Z),
ioapic_mask_spec irq habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_mask_spec irq labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_mask_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct. inv HQ; refine_split´; trivial.
apply relate_impl_ioapic_update; eauto.
Qed.
Context {mt1: match_impl_ioapic}.
Lemma ioapic_mask_match:
∀ s d d´ m f irq,
ioapic_mask_spec irq d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_mask_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ioapic_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_mask_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_mask_spec}.
Lemma ioapic_mask_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_mask_spec)
(id ↦ gensem ioapic_mask_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_mask_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_mask_match; eauto.
Qed.
End IOAPIC_MASK_SIM.
Section IOAPIC_UNMASK_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_ioapic}.
Lemma ioapic_unmask_exist:
∀ s habd habd´ labd f (irq: Z),
ioapic_unmask_spec irq habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ioapic_unmask_spec irq labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ioapic_unmask_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct. inv HQ; refine_split´; trivial.
apply relate_impl_ioapic_update; eauto.
Qed.
Context {mt1: match_impl_ioapic}.
Lemma ioapic_unmask_match:
∀ s d d´ m f irq,
ioapic_unmask_spec irq d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ioapic_unmask_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ioapic_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ioapic_unmask_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ioapic_unmask_spec}.
Lemma ioapic_unmask_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ioapic_unmask_spec)
(id ↦ gensem ioapic_unmask_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ioapic_unmask_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ioapic_unmask_match; eauto.
Qed.
End IOAPIC_UNMASK_SIM.
Section LAPIC_INIT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re4: relate_impl_lapic}.
Context {re5: relate_impl_ioapic}.
Lemma lapic_init_exist:
∀ s habd habd´ labd f,
lapic_init_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, lapic_init_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lapic_init_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct;
inv HQ; refine_split´; trivial.
rewrite H5. apply relate_impl_ioapic_update; eauto.
apply relate_impl_lapic_update; eauto.
Qed.
Context {mt1: match_impl_lapic}.
Context {mt2: match_impl_ioapic}.
Lemma lapic_init_match:
∀ s d d´ m f,
lapic_init_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lapic_init_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) lapic_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lapic_init_spec}.
Lemma lapic_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lapic_init_spec)
(id ↦ gensem lapic_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lapic_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lapic_init_match; eauto.
Qed.
End LAPIC_INIT_SIM.
Section LAPIC_EOI_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ioapic}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_lapic}.
Context {re5: relate_impl_in_intr}.
Lemma lapic_eoi_exist:
∀ s habd habd´ labd f,
lapic_eoi_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, lapic_eoi_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lapic_eoi_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_ioapic_update; eauto.
apply relate_impl_lapic_update; eauto.
Qed.
Context {mt1: match_impl_lapic}.
Context {mt2: match_impl_ioapic}.
Lemma lapic_eoi_match:
∀ s d d´ m f,
lapic_eoi_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lapic_eoi_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) lapic_eoi_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lapic_eoi_spec}.
Lemma lapic_eoi_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lapic_eoi_spec)
(id ↦ gensem lapic_eoi_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lapic_eoi_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lapic_eoi_match; eauto.
Qed.
End LAPIC_EOI_SIM.
End OBJ_SIM.