Library mcertikos.objects.dev.ObjInterruptProof
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Constant.
Require Import OracleInstances.
Require Import ObjSerialDevice.
Require Import ObjInterruptController.
Require Import ObjInterruptDriver.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import FutureTactic.
Require Import CommonTactic.
Lemma cons_intr_does_not_change_curr_intr_num:
∀ d d´,
cons_intr_aux d = Some d´ →
curr_intr_num d = curr_intr_num d´.
Proof.
intros. destruct d.
functional inversion H; simpl. reflexivity. reflexivity.
Qed.
Lemma cons_intr_does_not_change_intr_flag:
∀ d d´,
cons_intr_aux d = Some d´ →
intr_flag d = intr_flag d´.
Proof.
intros. destruct d.
functional inversion H; simpl. reflexivity. reflexivity.
Qed.
Lemma lapic_transparent:
∀ d n,
LapicEoi (s (lapic d)) = NoIntr →
LapicEsrClrPen (s (lapic d)) = false →
let lapic´ := lapic_trans_intr n (s (lapic d)) in
{|
s := {|
LapicEsr := LapicEsr lapic´;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt lapic´;
LapicEnable := LapicEnable lapic´;
LapicSpurious := LapicSpurious lapic´;
LapicLint0Mask := LapicLint0Mask lapic´;
LapicLint1Mask := LapicLint1Mask lapic´;
LapicPcIntMask := LapicPcIntMask lapic´;
LapicLdr := LapicLdr lapic´;
LapicErrorIrq := LapicErrorIrq lapic´;
LapicEsrClrPen := false;
LapicTpr := LapicTpr lapic´ |};
l1 := l1 (lapic d);
l2 := l2 (lapic d);
l3 := l3 (lapic d) |} = lapic d.
Proof.
intros d n Heoi Hesr lapic´. unfold lapic´.
unfold lapic_trans_intr. destruct lapic. destruct s. unfold_LApicState. simpl in ×.
destruct (zle_le 0 n 30). simpl.
rewrite Heoi, Hesr. reflexivity.
destruct (zle_le 32 n 55).
rewrite Heoi, Hesr. reflexivity.
destruct (zeq n 56).
rewrite Heoi, Hesr. reflexivity.
simpl.
rewrite Heoi, Hesr. reflexivity.
Qed.
Lemma ioapic_transparent:
∀ d,
CurrentIrq (s (ioapic d)) = None →
let ioapic´ := ioapic_trans_intr (IRQ 4) (s (ioapic d)) in
{|
s := {|
IoApicInit := IoApicInit ioapic´;
CurrentIrq := None;
IoApicBase := IoApicBase ioapic´;
IoApicId := IoApicId ioapic´;
IoApicMaxIntr := IoApicMaxIntr ioapic´;
IoApicIrqs := IoApicIrqs ioapic´;
IoApicEnables := IoApicEnables ioapic´ |};
l1 := l1 (ioapic d);
l2 := l2 (ioapic d);
l3 := l3 (ioapic d) |} = ioapic d.
Proof.
intros d Hirq ioapic´. unfold ioapic´.
destruct ioapic. destruct s. Opaque Z.to_nat. unfold_IoApicState. Transparent Z.to_nat. toNat.
Opaque nth_error.
simpl in ×.
destruct (nth_error IoApicIrqs 4).
destruct (nth_error IoApicEnables 4). destruct b. simpl. rewrite Hirq. reflexivity.
simpl. rewrite Hirq. reflexivity.
simpl. rewrite Hirq. reflexivity.
simpl. rewrite Hirq. reflexivity.
Qed.
Lemma Hnat4: Z.to_nat 4 = 4%nat. toNat; reflexivity. Qed.
Lemma serial_intr_transparent_not_routed:
∀ d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = error →
serial_intr_handler d = Some (d´, true) →
d {com1: serial_intr (com1 d)} = d´.
Proof.
Opaque Z.to_nat.
intros d d´ Hd Hcond. unfold serial_intr_handler. unfold serial_hw_intr_spec.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
- unfold hw_intr_trans. unfold ioapic_trans_intr.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
rewrite Hnat4. rewrite Hcond; simpl. unfold_RData. inversion 1. reflexivity.
- inversion 1.
Qed.
Lemma serial_intr_transparent_masked:
∀ d d´ v,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value v →
nth_error (IoApicEnables (s (ioapic d))) 4 = value false →
serial_intr_handler d = Some (d´, true) →
d {com1: serial_intr (com1 d)} = d´.
Proof.
intros d d´ v Hd Hidx Hmask. unfold serial_intr_handler. unfold serial_hw_intr_spec.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
- unfold hw_intr_trans. unfold ioapic_trans_intr.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
rewrite Hnat4. rewrite Hidx, Hmask; simpl. unfold_RData. inversion 1. reflexivity.
- inversion 1.
Qed.
Lemma serial_intr_transparent_iflag_disabled:
∀ d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = false →
serial_intr_handler d = Some (d´, true) →
d {com1: serial_intr (com1 d)} = d´.
Proof.
intros d d´ Hd Hidx Hmask Hif. unfold serial_intr_handler. unfold serial_hw_intr_spec.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
- unfold hw_intr_trans. unfold ioapic_trans_intr.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
rewrite Hnat4. rewrite Hidx, Hmask, Hif; simpl.
unfold lapic_trans_intr; simpl.
destruct lapic; simpl in ×. destruct s; simpl in ×.
unfold_RData. inversion 1. reflexivity.
- inversion 1.
Qed.
Lemma serial_intr_transparent_no_irq:
∀ d d´,
in_intr d = false →
SerialIrq (s (serial_intr (com1 d))) = false →
serial_intr_handler d = Some (d´, false) →
d = d´.
Proof.
intros d d´ Hd Hirq. unfold serial_intr_handler. unfold serial_hw_intr_spec.
rewrite Hirq. inversion 1. reflexivity.
Qed.
Lemma cons_intr_aux_independent_curr_intr_num:
∀ n d d´,
cons_intr_aux d = Some d´ →
cons_intr_aux d {curr_intr_num: n} = Some (d´ {curr_intr_num: n}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in *;
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9;
reflexivity.
Qed.
Lemma cons_intr_aux_independent_intr_flag:
∀ b d d´,
cons_intr_aux d = Some d´ →
cons_intr_aux d {intr_flag: b} = Some (d´ {intr_flag: b}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in *;
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9;
reflexivity.
Qed.
Lemma cons_intr_aux_independent_in_intr:
∀ d d´,
cons_intr_aux d = Some d´ →
cons_intr_aux d {in_intr: true} = Some (d´ {in_intr: true}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in ×.
rewrite H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
rewrite H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
Qed.
Lemma cons_intr_aux_independent_ioapic:
∀ d d´ n b,
cons_intr_aux d = Some d´ →
cons_intr_aux d {ioapic / s / IoApicEnables [(Z.to_nat n)]: b} = Some (d´ {ioapic / s / IoApicEnables [(Z.to_nat n)]: b}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in ×.
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
Qed.
Lemma update_in_intr_eq:
∀ d,
in_intr d = false →
Some d = Some (d { in_intr : true}) { in_intr : false}.
Proof.
intros. destruct d; simpl in ×. unfold_RData. rewrite H. reflexivity.
Qed.
Lemma in_intr_com1_update_commute:
∀ d,
(d { in_intr : true}) { com1 : serial_intr (com1 d)} =
(d { com1 : serial_intr (com1 d)}) { in_intr : true}.
Proof.
intros. destruct d; simpl in ×. unfold_RData. reflexivity.
Qed.
Lemma serial_intr_disable_aux_refinement_masked_not_routed:
∀ n d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = error →
serial_intr_disable_aux n true d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n. Opaque serial_intr.
- simpl. intros d d´ Hin Hcond Heq. inversion Heq. apply update_in_intr_eq. assumption.
- simpl. intros d d´ Hin Hcond Heq. destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
+ rewrite in_intr_com1_update_commute in Heq. apply IHn in Heq. simpl; trivial.
unfold update_com1 in Heq. subst.
unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
rewrite Hnat4. rewrite Hcond.
unfold_IoApicState. unfold update_com1, update_in_intr; simpl. rewrite Heq.
unfold update_in_intr. reflexivity.
Transparent serial_intr. simpl. assumption.
simpl. assumption.
+ Opaque serial_intr.
unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_disable_aux_refinement_masked:
∀ n d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value false →
serial_intr_disable_aux n true d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hin Hidx Henable Heq. inversion Heq. apply update_in_intr_eq. assumption.
- simpl. intros d d´ Hin Hidx Henable Heq. destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
+ rewrite in_intr_com1_update_commute in Heq. apply IHn in Heq; simpl; trivial.
unfold update_com1 in Heq. subst.
unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
rewrite Hnat4. rewrite Hidx. rewrite Henable.
unfold_IoApicState. unfold update_com1, update_in_intr; simpl. rewrite Heq.
unfold update_in_intr. reflexivity.
+ unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_disable_aux_refinement_iflag_disabled:
∀ n d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = false →
serial_intr_disable_aux n true d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hin Hidx Henable Hiflag Heq. inversion Heq. apply update_in_intr_eq; auto.
- simpl. intros d d´ Hin Hidx Henable Hiflag Heq.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hser.
+ rewrite in_intr_com1_update_commute in Heq. apply IHn in Heq; simpl; trivial.
unfold update_com1 in Heq. subst.
unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hser.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
rewrite Hnat4. rewrite Hidx. rewrite Henable. rewrite Hiflag.
unfold_IoApicState. unfold update_com1, update_in_intr; simpl. subst. rewrite Heq.
unfold update_in_intr. reflexivity.
+ unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hser.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_disable_aux_preserves_intr:
∀ n d d´,
serial_intr_disable_aux n false d = Some d´ →
curr_intr_num d = curr_intr_num d´ ∧
in_intr d = in_intr d´ ∧
intr_flag d = intr_flag d´.
Proof.
induction n.
- simpl. inversion 1. repeat (split; trivial).
- simpl. intros. subdestruct. apply IHn in H.
blast H.
functional inversion Hdestruct0.
unfold_SerialState. unfold_console. unfold_DeviceData. unfold_RData.
repeat (split; trivial).
unfold_SerialState. unfold_console. unfold_DeviceData. unfold_RData.
repeat (split; trivial).
inversion H.
repeat (split; trivial).
Qed.
Lemma serial_intr_disable_aux_independent_curr_intr_num:
∀ n x d d´,
serial_intr_disable_aux n false d = Some d´ →
serial_intr_disable_aux n false d {curr_intr_num: x} = Some (d´ {curr_intr_num: x}).
Proof.
induction n.
- simpl. inversion 1. reflexivity.
- simpl. intros. subdestruct.
apply cons_intr_aux_independent_curr_intr_num with (n:=x) in Hdestruct0.
generalize Hdestruct0. unfold_RData. intros Heq. rewrite Heq. clear Heq.
apply IHn. assumption. inv H. reflexivity.
Qed.
Lemma cons_intr_aux_preserves_all:
∀ d d´,
cons_intr_aux d = Some d´ →
curr_intr_num d = curr_intr_num d´ ∧
intr_flag d = intr_flag d´ ∧
in_intr d = in_intr d´ ∧
pg d = pg d´ ∧
init d = init d´ ∧
ikern d = ikern d´ ∧
ihost d = ihost d´ ∧
lapic d = lapic d´ ∧
ioapic d = ioapic d´.
Proof.
intros.
functional inversion H; simpl;
repeat (split; trivial).
Qed.
Lemma serial_intr_disable_aux_refinement_unmasked:
∀ n d d´,
ikern d = true →
ihost d = true →
init d = true →
LapicEoi (s (lapic d)) = NoIntr →
LapicEsrClrPen (s (lapic d)) = false →
CurrentIrq (s (ioapic d)) = None →
curr_intr_num d = 256 →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = true →
in_intr d = false →
serial_intr_disable_aux n false d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
inversion Heq. apply update_in_intr_eq; auto.
- Opaque serial_intr. Opaque cons_intr_aux.
simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
unfold update_com1 in Heq.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
subdestruct; simpl in ×.
+ unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hdestruct.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
rewrite Hnat4. rewrite Hidx. rewrite Henable. unfold_IoApicState. rewrite Hiflag.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
unfold lapic_eoi_spec; simpl. subst.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
generalize Hdestruct0; intro rval.
apply cons_intr_aux_independent_curr_intr_num with (n:=4) in Hdestruct0.
apply cons_intr_aux_independent_intr_flag with (b:=true) in Hdestruct0.
apply cons_intr_aux_independent_in_intr in Hdestruct0.
apply cons_intr_aux_independent_ioapic with (n:=4) (b:=false) in Hdestruct0.
revert Hdestruct0. unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData. intro Hrw.
change (Z.to_nat 4) with (4%nat) in Hrw.
rewrite Hrw; simpl. clear Hrw.
generalize (cons_intr_aux_preserves_all _ _ rval); simpl. intros Hr; blast Hr.
apply IHn; simpl; auto.
rewrite replace_replace.
rewrite nth_error_replace_gss.
reflexivity.
generalize (nth_error_range _ _ _ _ Henable); intro.
xomega.
destruct r; simpl in ×.
rewrite <- Hr0, <- Hr1, <- Hr2 in Heq. rewrite H1.
rewrite replace_replace.
rewrite nth_error_replace_id.
rewrite H2. unfold_RData. rewrite Heq. reflexivity.
assumption.
+ unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hdestruct.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Record invariant (abd: RData) :=
mkInvariant {
valid_ioapic_state:
init abd = true →
∀ n v, nth_error (IoApicIrqs (s (ioapic abd))) n = value v →
( v = Z.of_nat n + IRQ0
∧ ∃ b, nth_error (IoApicEnables (s (ioapic abd))) n = value b);
valid_intr_state: in_intr abd = false →
(LapicEoi (s (lapic abd)) = NoIntr ∧
LapicEsrClrPen (s (lapic abd)) = false ∧
CurrentIrq (s (ioapic abd)) = None ∧
curr_intr_num abd = 256)
}.
Lemma serial_intr_disable_spec_refinement:
∀ d d´,
invariant d →
serial_intr_disable_spec d = Some d´ →
serial_intr_disable_concrete_spec d = Some d´.
Proof.
intros d d´ Hinv H.
assert (Hrealirq: nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36
∨ nth_error (IoApicIrqs (s (ioapic d))) 4 = error).
{
assert (Hinit: init d = true).
{
functional inversion H; clear H; assumption.
}
inversion Hinv.
generalize (valid_ioapic_state0 Hinit). intros Hvalid.
functional inversion H; clear H;
(on_eq_left (nth_error (IoApicIrqs (s (ioapic d))) 4) act (fun Hx ⇒ rename Hx into Hirq)).
- generalize (Hvalid _ _ Hirq). toZ. intros (Hv & Hb). ring_simplify in Hv. rewrite Hv in Hirq. left. assumption.
- generalize (Hvalid _ _ Hirq). toZ. intros (Hv & Hb). ring_simplify in Hv. rewrite Hv in Hirq. left. assumption.
- generalize (Hvalid _ _ Hirq). toZ. intros (Hv & Hb). ring_simplify in Hv. rewrite Hv in Hirq. left. assumption.
- right. assumption.
}
functional inversion H; clear H.
-
Require Import Maps.
Require Import AuxStateDataType.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Constant.
Require Import OracleInstances.
Require Import ObjSerialDevice.
Require Import ObjInterruptController.
Require Import ObjInterruptDriver.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import FutureTactic.
Require Import CommonTactic.
Lemma cons_intr_does_not_change_curr_intr_num:
∀ d d´,
cons_intr_aux d = Some d´ →
curr_intr_num d = curr_intr_num d´.
Proof.
intros. destruct d.
functional inversion H; simpl. reflexivity. reflexivity.
Qed.
Lemma cons_intr_does_not_change_intr_flag:
∀ d d´,
cons_intr_aux d = Some d´ →
intr_flag d = intr_flag d´.
Proof.
intros. destruct d.
functional inversion H; simpl. reflexivity. reflexivity.
Qed.
Lemma lapic_transparent:
∀ d n,
LapicEoi (s (lapic d)) = NoIntr →
LapicEsrClrPen (s (lapic d)) = false →
let lapic´ := lapic_trans_intr n (s (lapic d)) in
{|
s := {|
LapicEsr := LapicEsr lapic´;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt lapic´;
LapicEnable := LapicEnable lapic´;
LapicSpurious := LapicSpurious lapic´;
LapicLint0Mask := LapicLint0Mask lapic´;
LapicLint1Mask := LapicLint1Mask lapic´;
LapicPcIntMask := LapicPcIntMask lapic´;
LapicLdr := LapicLdr lapic´;
LapicErrorIrq := LapicErrorIrq lapic´;
LapicEsrClrPen := false;
LapicTpr := LapicTpr lapic´ |};
l1 := l1 (lapic d);
l2 := l2 (lapic d);
l3 := l3 (lapic d) |} = lapic d.
Proof.
intros d n Heoi Hesr lapic´. unfold lapic´.
unfold lapic_trans_intr. destruct lapic. destruct s. unfold_LApicState. simpl in ×.
destruct (zle_le 0 n 30). simpl.
rewrite Heoi, Hesr. reflexivity.
destruct (zle_le 32 n 55).
rewrite Heoi, Hesr. reflexivity.
destruct (zeq n 56).
rewrite Heoi, Hesr. reflexivity.
simpl.
rewrite Heoi, Hesr. reflexivity.
Qed.
Lemma ioapic_transparent:
∀ d,
CurrentIrq (s (ioapic d)) = None →
let ioapic´ := ioapic_trans_intr (IRQ 4) (s (ioapic d)) in
{|
s := {|
IoApicInit := IoApicInit ioapic´;
CurrentIrq := None;
IoApicBase := IoApicBase ioapic´;
IoApicId := IoApicId ioapic´;
IoApicMaxIntr := IoApicMaxIntr ioapic´;
IoApicIrqs := IoApicIrqs ioapic´;
IoApicEnables := IoApicEnables ioapic´ |};
l1 := l1 (ioapic d);
l2 := l2 (ioapic d);
l3 := l3 (ioapic d) |} = ioapic d.
Proof.
intros d Hirq ioapic´. unfold ioapic´.
destruct ioapic. destruct s. Opaque Z.to_nat. unfold_IoApicState. Transparent Z.to_nat. toNat.
Opaque nth_error.
simpl in ×.
destruct (nth_error IoApicIrqs 4).
destruct (nth_error IoApicEnables 4). destruct b. simpl. rewrite Hirq. reflexivity.
simpl. rewrite Hirq. reflexivity.
simpl. rewrite Hirq. reflexivity.
simpl. rewrite Hirq. reflexivity.
Qed.
Lemma Hnat4: Z.to_nat 4 = 4%nat. toNat; reflexivity. Qed.
Lemma serial_intr_transparent_not_routed:
∀ d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = error →
serial_intr_handler d = Some (d´, true) →
d {com1: serial_intr (com1 d)} = d´.
Proof.
Opaque Z.to_nat.
intros d d´ Hd Hcond. unfold serial_intr_handler. unfold serial_hw_intr_spec.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
- unfold hw_intr_trans. unfold ioapic_trans_intr.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
rewrite Hnat4. rewrite Hcond; simpl. unfold_RData. inversion 1. reflexivity.
- inversion 1.
Qed.
Lemma serial_intr_transparent_masked:
∀ d d´ v,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value v →
nth_error (IoApicEnables (s (ioapic d))) 4 = value false →
serial_intr_handler d = Some (d´, true) →
d {com1: serial_intr (com1 d)} = d´.
Proof.
intros d d´ v Hd Hidx Hmask. unfold serial_intr_handler. unfold serial_hw_intr_spec.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
- unfold hw_intr_trans. unfold ioapic_trans_intr.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
rewrite Hnat4. rewrite Hidx, Hmask; simpl. unfold_RData. inversion 1. reflexivity.
- inversion 1.
Qed.
Lemma serial_intr_transparent_iflag_disabled:
∀ d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = false →
serial_intr_handler d = Some (d´, true) →
d {com1: serial_intr (com1 d)} = d´.
Proof.
intros d d´ Hd Hidx Hmask Hif. unfold serial_intr_handler. unfold serial_hw_intr_spec.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
- unfold hw_intr_trans. unfold ioapic_trans_intr.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
rewrite Hnat4. rewrite Hidx, Hmask, Hif; simpl.
unfold lapic_trans_intr; simpl.
destruct lapic; simpl in ×. destruct s; simpl in ×.
unfold_RData. inversion 1. reflexivity.
- inversion 1.
Qed.
Lemma serial_intr_transparent_no_irq:
∀ d d´,
in_intr d = false →
SerialIrq (s (serial_intr (com1 d))) = false →
serial_intr_handler d = Some (d´, false) →
d = d´.
Proof.
intros d d´ Hd Hirq. unfold serial_intr_handler. unfold serial_hw_intr_spec.
rewrite Hirq. inversion 1. reflexivity.
Qed.
Lemma cons_intr_aux_independent_curr_intr_num:
∀ n d d´,
cons_intr_aux d = Some d´ →
cons_intr_aux d {curr_intr_num: n} = Some (d´ {curr_intr_num: n}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in *;
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9;
reflexivity.
Qed.
Lemma cons_intr_aux_independent_intr_flag:
∀ b d d´,
cons_intr_aux d = Some d´ →
cons_intr_aux d {intr_flag: b} = Some (d´ {intr_flag: b}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in *;
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9;
reflexivity.
Qed.
Lemma cons_intr_aux_independent_in_intr:
∀ d d´,
cons_intr_aux d = Some d´ →
cons_intr_aux d {in_intr: true} = Some (d´ {in_intr: true}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in ×.
rewrite H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
rewrite H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
Qed.
Lemma cons_intr_aux_independent_ioapic:
∀ d d´ n b,
cons_intr_aux d = Some d´ →
cons_intr_aux d {ioapic / s / IoApicEnables [(Z.to_nat n)]: b} = Some (d´ {ioapic / s / IoApicEnables [(Z.to_nat n)]: b}).
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in ×.
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
rewrite H1, H2, H3, H4, H5, H6, H7, H8, H9.
reflexivity.
Qed.
Lemma update_in_intr_eq:
∀ d,
in_intr d = false →
Some d = Some (d { in_intr : true}) { in_intr : false}.
Proof.
intros. destruct d; simpl in ×. unfold_RData. rewrite H. reflexivity.
Qed.
Lemma in_intr_com1_update_commute:
∀ d,
(d { in_intr : true}) { com1 : serial_intr (com1 d)} =
(d { com1 : serial_intr (com1 d)}) { in_intr : true}.
Proof.
intros. destruct d; simpl in ×. unfold_RData. reflexivity.
Qed.
Lemma serial_intr_disable_aux_refinement_masked_not_routed:
∀ n d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = error →
serial_intr_disable_aux n true d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n. Opaque serial_intr.
- simpl. intros d d´ Hin Hcond Heq. inversion Heq. apply update_in_intr_eq. assumption.
- simpl. intros d d´ Hin Hcond Heq. destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
+ rewrite in_intr_com1_update_commute in Heq. apply IHn in Heq. simpl; trivial.
unfold update_com1 in Heq. subst.
unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
rewrite Hnat4. rewrite Hcond.
unfold_IoApicState. unfold update_com1, update_in_intr; simpl. rewrite Heq.
unfold update_in_intr. reflexivity.
Transparent serial_intr. simpl. assumption.
simpl. assumption.
+ Opaque serial_intr.
unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_disable_aux_refinement_masked:
∀ n d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value false →
serial_intr_disable_aux n true d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hin Hidx Henable Heq. inversion Heq. apply update_in_intr_eq. assumption.
- simpl. intros d d´ Hin Hidx Henable Heq. destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hirq.
+ rewrite in_intr_com1_update_commute in Heq. apply IHn in Heq; simpl; trivial.
unfold update_com1 in Heq. subst.
unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
rewrite Hnat4. rewrite Hidx. rewrite Henable.
unfold_IoApicState. unfold update_com1, update_in_intr; simpl. rewrite Heq.
unfold update_in_intr. reflexivity.
+ unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hirq.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_disable_aux_refinement_iflag_disabled:
∀ n d d´,
in_intr d = false →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = false →
serial_intr_disable_aux n true d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hin Hidx Henable Hiflag Heq. inversion Heq. apply update_in_intr_eq; auto.
- simpl. intros d d´ Hin Hidx Henable Hiflag Heq.
destruct (SerialIrq (s (serial_intr (com1 d)))) eqn: Hser.
+ rewrite in_intr_com1_update_commute in Heq. apply IHn in Heq; simpl; trivial.
unfold update_com1 in Heq. subst.
unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hser.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
rewrite Hnat4. rewrite Hidx. rewrite Henable. rewrite Hiflag.
unfold_IoApicState. unfold update_com1, update_in_intr; simpl. subst. rewrite Heq.
unfold update_in_intr. reflexivity.
+ unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hser.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_disable_aux_preserves_intr:
∀ n d d´,
serial_intr_disable_aux n false d = Some d´ →
curr_intr_num d = curr_intr_num d´ ∧
in_intr d = in_intr d´ ∧
intr_flag d = intr_flag d´.
Proof.
induction n.
- simpl. inversion 1. repeat (split; trivial).
- simpl. intros. subdestruct. apply IHn in H.
blast H.
functional inversion Hdestruct0.
unfold_SerialState. unfold_console. unfold_DeviceData. unfold_RData.
repeat (split; trivial).
unfold_SerialState. unfold_console. unfold_DeviceData. unfold_RData.
repeat (split; trivial).
inversion H.
repeat (split; trivial).
Qed.
Lemma serial_intr_disable_aux_independent_curr_intr_num:
∀ n x d d´,
serial_intr_disable_aux n false d = Some d´ →
serial_intr_disable_aux n false d {curr_intr_num: x} = Some (d´ {curr_intr_num: x}).
Proof.
induction n.
- simpl. inversion 1. reflexivity.
- simpl. intros. subdestruct.
apply cons_intr_aux_independent_curr_intr_num with (n:=x) in Hdestruct0.
generalize Hdestruct0. unfold_RData. intros Heq. rewrite Heq. clear Heq.
apply IHn. assumption. inv H. reflexivity.
Qed.
Lemma cons_intr_aux_preserves_all:
∀ d d´,
cons_intr_aux d = Some d´ →
curr_intr_num d = curr_intr_num d´ ∧
intr_flag d = intr_flag d´ ∧
in_intr d = in_intr d´ ∧
pg d = pg d´ ∧
init d = init d´ ∧
ikern d = ikern d´ ∧
ihost d = ihost d´ ∧
lapic d = lapic d´ ∧
ioapic d = ioapic d´.
Proof.
intros.
functional inversion H; simpl;
repeat (split; trivial).
Qed.
Lemma serial_intr_disable_aux_refinement_unmasked:
∀ n d d´,
ikern d = true →
ihost d = true →
init d = true →
LapicEoi (s (lapic d)) = NoIntr →
LapicEsrClrPen (s (lapic d)) = false →
CurrentIrq (s (ioapic d)) = None →
curr_intr_num d = 256 →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = true →
in_intr d = false →
serial_intr_disable_aux n false d {in_intr: true} = Some d´ →
serial_intr_disable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
inversion Heq. apply update_in_intr_eq; auto.
- Opaque serial_intr. Opaque cons_intr_aux.
simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
unfold update_com1 in Heq.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
subdestruct; simpl in ×.
+ unfold serial_intr_handler. unfold serial_hw_intr_spec; simpl. rewrite Hdestruct.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
rewrite Hnat4. rewrite Hidx. rewrite Henable. unfold_IoApicState. rewrite Hiflag.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
unfold lapic_eoi_spec; simpl. subst.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
generalize Hdestruct0; intro rval.
apply cons_intr_aux_independent_curr_intr_num with (n:=4) in Hdestruct0.
apply cons_intr_aux_independent_intr_flag with (b:=true) in Hdestruct0.
apply cons_intr_aux_independent_in_intr in Hdestruct0.
apply cons_intr_aux_independent_ioapic with (n:=4) (b:=false) in Hdestruct0.
revert Hdestruct0. unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData. intro Hrw.
change (Z.to_nat 4) with (4%nat) in Hrw.
rewrite Hrw; simpl. clear Hrw.
generalize (cons_intr_aux_preserves_all _ _ rval); simpl. intros Hr; blast Hr.
apply IHn; simpl; auto.
rewrite replace_replace.
rewrite nth_error_replace_gss.
reflexivity.
generalize (nth_error_range _ _ _ _ Henable); intro.
xomega.
destruct r; simpl in ×.
rewrite <- Hr0, <- Hr1, <- Hr2 in Heq. rewrite H1.
rewrite replace_replace.
rewrite nth_error_replace_id.
rewrite H2. unfold_RData. rewrite Heq. reflexivity.
assumption.
+ unfold serial_intr_handler; simpl. unfold serial_hw_intr_spec; simpl. rewrite Hdestruct.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Record invariant (abd: RData) :=
mkInvariant {
valid_ioapic_state:
init abd = true →
∀ n v, nth_error (IoApicIrqs (s (ioapic abd))) n = value v →
( v = Z.of_nat n + IRQ0
∧ ∃ b, nth_error (IoApicEnables (s (ioapic abd))) n = value b);
valid_intr_state: in_intr abd = false →
(LapicEoi (s (lapic abd)) = NoIntr ∧
LapicEsrClrPen (s (lapic abd)) = false ∧
CurrentIrq (s (ioapic abd)) = None ∧
curr_intr_num abd = 256)
}.
Lemma serial_intr_disable_spec_refinement:
∀ d d´,
invariant d →
serial_intr_disable_spec d = Some d´ →
serial_intr_disable_concrete_spec d = Some d´.
Proof.
intros d d´ Hinv H.
assert (Hrealirq: nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36
∨ nth_error (IoApicIrqs (s (ioapic d))) 4 = error).
{
assert (Hinit: init d = true).
{
functional inversion H; clear H; assumption.
}
inversion Hinv.
generalize (valid_ioapic_state0 Hinit). intros Hvalid.
functional inversion H; clear H;
(on_eq_left (nth_error (IoApicIrqs (s (ioapic d))) 4) act (fun Hx ⇒ rename Hx into Hirq)).
- generalize (Hvalid _ _ Hirq). toZ. intros (Hv & Hb). ring_simplify in Hv. rewrite Hv in Hirq. left. assumption.
- generalize (Hvalid _ _ Hirq). toZ. intros (Hv & Hb). ring_simplify in Hv. rewrite Hv in Hirq. left. assumption.
- generalize (Hvalid _ _ Hirq). toZ. intros (Hv & Hb). ring_simplify in Hv. rewrite Hv in Hirq. left. assumption.
- right. assumption.
}
functional inversion H; clear H.
-
not masked
destruct Hinv. generalize (valid_intr_state0 H1). intros Hintr. blast Hintr.
subst. unfold serial_intr_disable_concrete_spec. rewrite H1, H2, H3, H4, H5. unfold masked in ×.
rewrite serial_intr_disable_aux_refinement_unmasked with (d´:=d0); auto.
destruct Hrealirq; [assumption | rewrite H in H6; inversion H6].
-
subst. unfold serial_intr_disable_concrete_spec. rewrite H1, H2, H3, H4, H5. unfold masked in ×.
rewrite serial_intr_disable_aux_refinement_unmasked with (d´:=d0); auto.
destruct Hrealirq; [assumption | rewrite H in H6; inversion H6].
-
iflag cleared
subst. unfold serial_intr_disable_concrete_spec. rewrite H1, H2, H3, H4, H5. unfold masked in ×.
rewrite serial_intr_disable_aux_refinement_iflag_disabled with (d´:=d0) ; auto.
destruct Hrealirq; [assumption | rewrite H in H6; inversion H6].
-
rewrite serial_intr_disable_aux_refinement_iflag_disabled with (d´:=d0) ; auto.
destruct Hrealirq; [assumption | rewrite H in H6; inversion H6].
-
interrupt line maksed
subst. unfold serial_intr_disable_concrete_spec. rewrite H1, H2, H3, H4, H5. unfold masked in ×.
rewrite serial_intr_disable_aux_refinement_masked with (d´:=d0); auto; unfold value.
destruct Hrealirq; [assumption | rewrite H in H6; inversion H6].
inversion Hinv.
generalize (valid_ioapic_state0 H3 _ _ H6). intros (Hv & Hb). destruct Hb. rewrite H in H8; simpl in H8.
destruct x. inversion H8. assumption.
-
rewrite serial_intr_disable_aux_refinement_masked with (d´:=d0); auto; unfold value.
destruct Hrealirq; [assumption | rewrite H in H6; inversion H6].
inversion Hinv.
generalize (valid_ioapic_state0 H3 _ _ H6). intros (Hv & Hb). destruct Hb. rewrite H in H8; simpl in H8.
destruct x. inversion H8. assumption.
-
interrupt line is not routed
subst. unfold serial_intr_disable_concrete_spec. rewrite H1, H2, H3, H4, H5. unfold masked in ×.
rewrite serial_intr_disable_aux_refinement_masked_not_routed with (d´:=d0); auto.
Qed.
Lemma serial_intr_enable_aux_refinement:
∀ n d d´,
ikern d = true →
ihost d = true →
init d = true →
LapicEoi (s (lapic d)) = NoIntr →
LapicEsrClrPen (s (lapic d)) = false →
CurrentIrq (s (ioapic d)) = None →
curr_intr_num d = 256 →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = true →
in_intr d = false →
serial_intr_enable_aux n d {in_intr: true} = Some d´ →
serial_intr_enable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
inversion Heq. apply update_in_intr_eq; auto.
- Opaque serial_intr. Opaque cons_intr_aux.
simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
unfold update_com1 in Heq.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
subdestruct; simpl in ×.
+ unfold serial_intr_pending_handler. simpl in ×.
unfold ic_intr_spec; simpl.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
rewrite Hnat4. rewrite Hidx. rewrite Henable. unfold_IoApicState. rewrite Hiflag.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
unfold lapic_eoi_spec; simpl. subst.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
generalize Hdestruct0; intro rval.
apply cons_intr_aux_independent_curr_intr_num with (n:=4) in Hdestruct0.
apply cons_intr_aux_independent_intr_flag with (b:=true) in Hdestruct0.
apply cons_intr_aux_independent_in_intr in Hdestruct0.
apply cons_intr_aux_independent_ioapic with (n:=4) (b:=false) in Hdestruct0.
revert Hdestruct0. unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData. intro Hrw.
change (Z.to_nat 4) with (4%nat) in Hrw.
rewrite Hrw; simpl. clear Hrw.
generalize (cons_intr_aux_preserves_all _ _ rval); simpl. intros Hr; blast Hr.
apply IHn; simpl; auto.
rewrite replace_replace.
rewrite nth_error_replace_gss.
reflexivity.
generalize (nth_error_range _ _ _ _ Henable); intro.
xomega.
destruct r; simpl in ×.
rewrite <- Hr0, <- Hr1, <- Hr2 in Heq. rewrite H1.
rewrite replace_replace.
rewrite nth_error_replace_id.
rewrite H2. unfold_RData. rewrite Heq. reflexivity.
assumption.
+ unfold serial_intr_pending_handler; simpl. simpl in ×.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_enable_spec_refinement:
∀ d d´,
invariant d →
serial_intr_enable_spec d = Some d´ →
serial_intr_enable_concrete_spec d = Some d´.
Proof.
intros d d´ Hinv H.
functional inversion H; clear H.
destruct Hinv. generalize (valid_intr_state0 H1). intros Hintr. blast Hintr.
subst. unfold serial_intr_enable_concrete_spec. rewrite H1, H2, H3, H4, H5.
rewrite serial_intr_enable_aux_refinement with (d´:=d0); auto.
generalize H6; intro copy.
eapply valid_ioapic_state0 in H6; eauto.
destruct H6.
rewrite H in copy.
replace (Z.of_nat 4 + 32) with 36 in copy by xomega.
apply copy.
Qed.
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_INTR_DISABLE_REFINED_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_drv_serial}.
Context {re4: relate_impl_com1}.
Context {re5: relate_impl_console}.
Context {re6: relate_impl_ioapic}.
Context {re7: relate_impl_lapic}.
Context {re8: relate_impl_curr_intr_num}.
Context {re9: relate_impl_in_intr}.
Context {re10: relate_impl_init}.
Lemma serial_intr_disable_refined_exist:
∀ s habd habd´ labd f,
invariant labd
→ serial_intr_disable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_concrete_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros.
exploit serial_intr_disable_exist; eauto; intros (labd´ & HP & HM).
esplit.
split.
eapply serial_intr_disable_spec_refinement; eauto.
assumption.
Qed.
End SERIAL_INTR_DISABLE_REFINED_SIM.
Section SERIAL_INTR_ENABLE_REFINED_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_drv_serial}.
Context {re4: relate_impl_com1}.
Context {re5: relate_impl_console}.
Context {re6: relate_impl_ioapic}.
Context {re7: relate_impl_lapic}.
Context {re8: relate_impl_curr_intr_num}.
Context {re9: relate_impl_in_intr}.
Context {re10: relate_impl_init}.
Lemma serial_intr_enable_refined_exist:
∀ s habd habd´ labd f,
invariant labd
→ serial_intr_enable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_concrete_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros.
exploit serial_intr_enable_exist; eauto; intros (labd´ & HP & HM).
esplit.
split.
eapply serial_intr_enable_spec_refinement; eauto.
assumption.
Qed.
End SERIAL_INTR_ENABLE_REFINED_SIM.
End OBJ_SIM.
rewrite serial_intr_disable_aux_refinement_masked_not_routed with (d´:=d0); auto.
Qed.
Lemma serial_intr_enable_aux_refinement:
∀ n d d´,
ikern d = true →
ihost d = true →
init d = true →
LapicEoi (s (lapic d)) = NoIntr →
LapicEsrClrPen (s (lapic d)) = false →
CurrentIrq (s (ioapic d)) = None →
curr_intr_num d = 256 →
nth_error (IoApicIrqs (s (ioapic d))) 4 = value 36 →
nth_error (IoApicEnables (s (ioapic d))) 4 = value true →
intr_flag d = true →
in_intr d = false →
serial_intr_enable_aux n d {in_intr: true} = Some d´ →
serial_intr_enable_concrete_aux n d = Some d´ {in_intr: false}.
Proof.
induction n.
- simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
inversion Heq. apply update_in_intr_eq; auto.
- Opaque serial_intr. Opaque cons_intr_aux.
simpl. intros d d´ Hkern Hhost Hinit Heoi Hesr Hirq Hcur Hidx Henable Hiflag Hin Heq.
unfold update_com1 in Heq.
destruct d; simpl. destruct ioapic; simpl. destruct lapic; simpl.
destruct com1; simpl. destruct s, s0, s1; simpl in ×.
subdestruct; simpl in ×.
+ unfold serial_intr_pending_handler. simpl in ×.
unfold ic_intr_spec; simpl.
unfold hw_intr_trans. unfold ioapic_trans_intr; simpl.
rewrite Hnat4. rewrite Hidx. rewrite Henable. unfold_IoApicState. rewrite Hiflag.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
unfold lapic_eoi_spec; simpl. subst.
unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData.
generalize Hdestruct0; intro rval.
apply cons_intr_aux_independent_curr_intr_num with (n:=4) in Hdestruct0.
apply cons_intr_aux_independent_intr_flag with (b:=true) in Hdestruct0.
apply cons_intr_aux_independent_in_intr in Hdestruct0.
apply cons_intr_aux_independent_ioapic with (n:=4) (b:=false) in Hdestruct0.
revert Hdestruct0. unfold_IoApicState. unfold_LApicState. unfold_DeviceData. unfold_RData. intro Hrw.
change (Z.to_nat 4) with (4%nat) in Hrw.
rewrite Hrw; simpl. clear Hrw.
generalize (cons_intr_aux_preserves_all _ _ rval); simpl. intros Hr; blast Hr.
apply IHn; simpl; auto.
rewrite replace_replace.
rewrite nth_error_replace_gss.
reflexivity.
generalize (nth_error_range _ _ _ _ Henable); intro.
xomega.
destruct r; simpl in ×.
rewrite <- Hr0, <- Hr1, <- Hr2 in Heq. rewrite H1.
rewrite replace_replace.
rewrite nth_error_replace_id.
rewrite H2. unfold_RData. rewrite Heq. reflexivity.
assumption.
+ unfold serial_intr_pending_handler; simpl. simpl in ×.
inversion Heq. rewrite <- update_in_intr_eq; auto.
Qed.
Lemma serial_intr_enable_spec_refinement:
∀ d d´,
invariant d →
serial_intr_enable_spec d = Some d´ →
serial_intr_enable_concrete_spec d = Some d´.
Proof.
intros d d´ Hinv H.
functional inversion H; clear H.
destruct Hinv. generalize (valid_intr_state0 H1). intros Hintr. blast Hintr.
subst. unfold serial_intr_enable_concrete_spec. rewrite H1, H2, H3, H4, H5.
rewrite serial_intr_enable_aux_refinement with (d´:=d0); auto.
generalize H6; intro copy.
eapply valid_ioapic_state0 in H6; eauto.
destruct H6.
rewrite H in copy.
replace (Z.of_nat 4 + 32) with 36 in copy by xomega.
apply copy.
Qed.
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_INTR_DISABLE_REFINED_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_drv_serial}.
Context {re4: relate_impl_com1}.
Context {re5: relate_impl_console}.
Context {re6: relate_impl_ioapic}.
Context {re7: relate_impl_lapic}.
Context {re8: relate_impl_curr_intr_num}.
Context {re9: relate_impl_in_intr}.
Context {re10: relate_impl_init}.
Lemma serial_intr_disable_refined_exist:
∀ s habd habd´ labd f,
invariant labd
→ serial_intr_disable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_concrete_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros.
exploit serial_intr_disable_exist; eauto; intros (labd´ & HP & HM).
esplit.
split.
eapply serial_intr_disable_spec_refinement; eauto.
assumption.
Qed.
End SERIAL_INTR_DISABLE_REFINED_SIM.
Section SERIAL_INTR_ENABLE_REFINED_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_drv_serial}.
Context {re4: relate_impl_com1}.
Context {re5: relate_impl_console}.
Context {re6: relate_impl_ioapic}.
Context {re7: relate_impl_lapic}.
Context {re8: relate_impl_curr_intr_num}.
Context {re9: relate_impl_in_intr}.
Context {re10: relate_impl_init}.
Lemma serial_intr_enable_refined_exist:
∀ s habd habd´ labd f,
invariant labd
→ serial_intr_enable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_concrete_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros.
exploit serial_intr_enable_exist; eauto; intros (labd´ & HP & HM).
esplit.
split.
eapply serial_intr_enable_spec_refinement; eauto.
assumption.
Qed.
End SERIAL_INTR_ENABLE_REFINED_SIM.
End OBJ_SIM.