Library mcertikos.objects.dev.ObjInterruptManagement
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 ObjInterruptDriver.
Require Import ObjConsole.
Require Import ObjX86.
Section OBJ_InterruptManagement.
Definition Step := RData → option RData.
Notation "a ´[´ key ´:´ value ´]´" :=
(ZMap.set key value a) (at level 1, key, value at level 2).
Notation "a ´[´ key ´]´" := (ZMap.get key a) (at level 1, key at level 2).
Function intr_default_handler_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, in_intr abd) with
| (true, true, true, true) ⇒
Some (abd {lapic: (lapic abd) {s/LapicEoi: NoIntr}
{s/LapicEsrClrPen: false}}
{ioapic: (ioapic abd) {s/CurrentIrq: None}}
)
| _ ⇒ None
end.
Inductive IntrVector :=
| INT0
| INT1
| INT2
| INT3
| INT4
| INT5
| INT6
| INT7
| INT8
| INT9
| INT10
| INT11
| INT12
| INT32
| INT33
| INT34
| INT35
| INT36
| INT37
| INT38
| INT39
| INT40
| INT41
| INT42
| INT43
| INT44
| INT45
| INT46
| INT47
| INT48
| INT49
| INT50
| INT51
| INT52
| INT53
| INT54
| INT55
| INT56
| INTUndef.
Definition toIrq (trapno: Z) :=
if zeq trapno 0 then INT0 else
if zeq trapno 1 then INT1 else
if zeq trapno 2 then INT2 else
if zeq trapno 3 then INT3 else
if zeq trapno 4 then INT4 else
if zeq trapno 5 then INT5 else
if zeq trapno 6 then INT6 else
if zeq trapno 7 then INT7 else
if zeq trapno 8 then INT8 else
if zeq trapno 9 then INT9 else
if zeq trapno 10 then INT10 else
if zeq trapno 11 then INT11 else
if zeq trapno 12 then INT12 else
if zeq trapno 32 then INT32 else
if zeq trapno 33 then INT33 else
if zeq trapno 34 then INT34 else
if zeq trapno 35 then INT35 else
if zeq trapno 36 then INT36 else
if zeq trapno 37 then INT37 else
if zeq trapno 38 then INT38 else
if zeq trapno 39 then INT39 else
if zeq trapno 40 then INT40 else
if zeq trapno 41 then INT41 else
if zeq trapno 42 then INT42 else
if zeq trapno 43 then INT43 else
if zeq trapno 44 then INT44 else
if zeq trapno 45 then INT45 else
if zeq trapno 46 then INT46 else
if zeq trapno 47 then INT47 else
if zeq trapno 48 then INT48 else
if zeq trapno 49 then INT49 else
if zeq trapno 50 then INT50 else
if zeq trapno 51 then INT51 else
if zeq trapno 52 then INT52 else
if zeq trapno 53 then INT53 else
if zeq trapno 54 then INT54 else
if zeq trapno 55 then INT55 else
if zeq trapno 56 then INT56 else
INTUndef.
Definition toTrapno (irq: IntrVector) :=
match irq with
| INT0 ⇒ Some 0
| INT1 ⇒ Some 1
| INT2 ⇒ Some 2
| INT3 ⇒ Some 3
| INT4 ⇒ Some 4
| INT5 ⇒ Some 5
| INT6 ⇒ Some 6
| INT7 ⇒ Some 7
| INT8 ⇒ Some 8
| INT9 ⇒ Some 9
| INT10 ⇒ Some 10
| INT11 ⇒ Some 11
| INT12 ⇒ Some 12
| INT32 ⇒ Some 32
| INT33 ⇒ Some 33
| INT34 ⇒ Some 34
| INT35 ⇒ Some 35
| INT36 ⇒ Some 36
| INT37 ⇒ Some 37
| INT38 ⇒ Some 38
| INT39 ⇒ Some 39
| INT40 ⇒ Some 40
| INT41 ⇒ Some 41
| INT42 ⇒ Some 42
| INT43 ⇒ Some 43
| INT44 ⇒ Some 44
| INT45 ⇒ Some 45
| INT46 ⇒ Some 46
| INT47 ⇒ Some 47
| INT48 ⇒ Some 48
| INT49 ⇒ Some 49
| INT50 ⇒ Some 50
| INT51 ⇒ Some 51
| INT52 ⇒ Some 52
| INT53 ⇒ Some 53
| INT54 ⇒ Some 54
| INT55 ⇒ Some 55
| INT56 ⇒ Some 56
| INTUndef ⇒ None
end.
Require Import FutureTactic.
Lemma toIrq_inv_undef:
∀ trapno,
trapno < 0 ∨ trapno > 56 ∨ (12 < trapno < 32) →
toIrq trapno = INTUndef.
Proof.
intros.
destruct H as [Hl | [Hh | Hm]]; unfold toIrq;
repeat if_false; reflexivity.
Qed.
Lemma irq_trapno_inj:
∀ trapno irq, toIrq(trapno) = irq →
irq ≠ INTUndef →
toTrapno irq = Some trapno.
Proof.
intros n i. unfold toIrq.
repeat case_if; intros Hi Hn; rewrite <- Hi; try rewrite e; simpl; try reflexivity.
rewrite Hi in Hn. destruct Hn. reflexivity.
Qed.
Ltac solve_toIrq_inv :=
match goal with
| [ H: toIrq ?n = ?i |- ?n = _] ⇒
apply irq_trapno_inj in H;
[simpl in H; inversion H; reflexivity |
discriminate]
end.
Lemma toIrq_inv_0: ∀ n, toIrq n = INT0 → n = 0. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_1: ∀ n, toIrq n = INT1 → n = 1. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_2: ∀ n, toIrq n = INT2 → n = 2. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_3: ∀ n, toIrq n = INT3 → n = 3. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_4: ∀ n, toIrq n = INT4 → n = 4. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_5: ∀ n, toIrq n = INT5 → n = 5. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_6: ∀ n, toIrq n = INT6 → n = 6. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_7: ∀ n, toIrq n = INT7 → n = 7. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_8: ∀ n, toIrq n = INT8 → n = 8. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_9: ∀ n, toIrq n = INT9 → n = 9. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_10: ∀ n, toIrq n = INT10 → n = 10. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_11: ∀ n, toIrq n = INT11 → n = 11. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_12: ∀ n, toIrq n = INT12 → n = 12. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_32: ∀ n, toIrq n = INT32 → n = 32. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_33: ∀ n, toIrq n = INT33 → n = 33. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_34: ∀ n, toIrq n = INT34 → n = 34. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_35: ∀ n, toIrq n = INT35 → n = 35. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_36: ∀ n, toIrq n = INT36 → n = 36. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_37: ∀ n, toIrq n = INT37 → n = 37. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_38: ∀ n, toIrq n = INT38 → n = 38. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_39: ∀ n, toIrq n = INT39 → n = 39. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_40: ∀ n, toIrq n = INT40 → n = 40. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_41: ∀ n, toIrq n = INT41 → n = 41. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_42: ∀ n, toIrq n = INT42 → n = 42. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_43: ∀ n, toIrq n = INT43 → n = 43. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_44: ∀ n, toIrq n = INT44 → n = 44. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_45: ∀ n, toIrq n = INT45 → n = 45. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_46: ∀ n, toIrq n = INT46 → n = 46. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_47: ∀ n, toIrq n = INT47 → n = 47. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_48: ∀ n, toIrq n = INT48 → n = 48. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_49: ∀ n, toIrq n = INT49 → n = 49. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_50: ∀ n, toIrq n = INT50 → n = 50. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_51: ∀ n, toIrq n = INT51 → n = 51. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_52: ∀ n, toIrq n = INT52 → n = 52. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_53: ∀ n, toIrq n = INT53 → n = 53. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_54: ∀ n, toIrq n = INT54 → n = 54. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_55: ∀ n, toIrq n = INT55 → n = 55. intros; solve_toIrq_inv. Qed.
Lemma toIrq_inv_56: ∀ n, toIrq n = INT56 → n = 56. intros; solve_toIrq_inv. Qed.
Function get_curr_intr_num_spec (abd: RData): option Z :=
match (ikern abd, ihost abd) with
| (true, true) ⇒ Some (curr_intr_num abd)
| _ ⇒ None
end.
return: (abd', device_has_irq)
- None: error occurs.
- (abd', true): interrupt handled or be masked
- (abd', false): device transition does not request interrupt
Function serial_intr_handler (abd: RData): option (RData × bool) :=
match serial_hw_intr_spec abd with
| Some (d0, n) ⇒
if zeq n 36 then
match lapic_eoi_spec (d0 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒
match iret_spec (d2 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true}) with
| Some d3 ⇒ Some (d3, true)
| None ⇒ None
end
| None ⇒ None
end
| None ⇒ None
end
else
Some (abd {com1: serial_intr (com1 abd)}, true)
| _ ⇒ Some (abd, false)
end.
Function serial_intr_pending_handler (abd: RData): option (RData × bool) :=
if SerialIrq (s (com1 abd)) then
match ic_intr_spec 4 abd with
| Some (d0, n) ⇒
if zeq n 36 then
match lapic_eoi_spec (d0 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒
match iret_spec (d2 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true}) with
| Some d3 ⇒ Some (d3, true)
| None ⇒ None
end
| None ⇒ None
end
| None ⇒ None
end
else
None
| None ⇒ None
end
else
Some (abd, false).
Function serial_intr_handler_sw_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, in_intr abd) with
| (true, true, true, true) ⇒
match lapic_eoi_spec (abd {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒ Some (d2 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true})
| None ⇒ None
end
| None ⇒ None
end
| _ ⇒ None
end.
Definition serial_intr_handler_asm_spec (rs: regset) (abd: RData): option (RData × regset) :=
match (ikern abd, ihost abd, init abd, in_intr abd) with
| (true, true, true, true) ⇒
match lapic_eoi_spec ((save_context_spec rs abd) {ioapic / s / IoApicEnables [4%nat]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒
match restore_context_spec (d2 {ioapic / s / IoApicEnables [4%nat]: true}) with
| (rs´, d3) ⇒ Some (d3, rs´)
end
| None ⇒ None
end
| None ⇒ None
end
| _ ⇒ None
end.
Lemma lapic_eoi_spec_preserves_tf:
∀ d d´,
lapic_eoi_spec d = Some d´ →
tf d = tf d´.
Proof.
intros.
unfold lapic_eoi_spec.
functional inversion H; simpl in *; subst; simpl in ×.
reflexivity.
Qed.
Lemma cons_intr_aux_preserves_tf:
∀ d d´,
cons_intr_aux d = Some d´ →
tf d = tf d´.
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in *;
reflexivity.
Qed.
Require Import CommonTactic.
Lemma serial_intr_handler_asm_spec_inv:
∀ rs rs´ d d´,
serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
(ikern d = true ∧
ihost d = true ∧
init d = true ∧
in_intr d = true ∧
∃ d1 d2 d3 d4 d5,
save_context_spec rs d = d1 ∧
d1 {intr_flag: true} {ioapic / s / IoApicEnables [4%nat]: false} = d2 ∧
lapic_eoi_spec d2 = Some d3 ∧
cons_intr_aux d3 = Some d4 ∧
d4 {ioapic / s / IoApicEnables [4%nat]: true} = d5 ∧
restore_context_spec d5 = (rs´, d´)).
Proof.
intros rs rs´ d d´.
unfold serial_intr_handler_asm_spec.
intros H.
split; [subdestruct; auto|].
split; [subdestruct; auto|].
split; [subdestruct; auto|].
split; [subdestruct; auto|].
subdestruct.
repeat esplit.
eassumption.
eassumption.
inv H.
assumption.
Qed.
Definition serial_intr_handler_ext_spec (abd: RData): option (RData × bool) :=
match (ikern abd, ihost abd, init abd) with
| (true, true, true) ⇒
match serial_hw_intr_spec abd with
| Some (d0, n) ⇒
if zeq n 36 then
match serial_intr_handler_sw_spec d0 with
| Some d1 ⇒
match iret_spec d1 with
| Some d2 ⇒ Some (d2, true)
| None ⇒ None
end
| None ⇒ None
end
else
Some (abd {com1: serial_intr (com1 abd)}, true)
| _ ⇒ Some (abd, false)
end
| _ ⇒ None
end.
Lemma serial_intr_handler_ext_refinement:
∀ d d´ b,
serial_intr_handler_ext_spec d = Some (d´, b) →
serial_intr_handler d = Some (d´, b).
Proof.
intros d d´ b.
unfold serial_intr_handler_ext_spec.
unfold serial_intr_handler.
unfold serial_intr_handler_sw_spec.
intros Hspec.
subdestruct; eauto.
Qed.
Fixpoint serial_intr_disable_concrete_aux (n: nat) (abd: RData) {struct n} : option RData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
match serial_intr_handler abd with
| Some (d´, true) ⇒ serial_intr_disable_concrete_aux n´ d´
| Some (d´, false) ⇒ Some abd
| None ⇒ None
end
end.
Fixpoint serial_intr_enable_concrete_aux (n: nat) (abd: RData) {struct n}: option RData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
match serial_intr_pending_handler abd with
| Some (d´, true) ⇒ serial_intr_enable_concrete_aux n´ d´
| Some (d´, false) ⇒ Some abd
| None ⇒ None
end
end.
Fixpoint serial_intr_disable_aux (n: nat) (masked: bool) (abd: RData) {struct n} : option RData
:=
match n with
| O ⇒ Some abd
| S n´ ⇒
let d0 := abd {com1: serial_intr (com1 abd)} in
if SerialIrq (s (com1 d0)) then
if masked then
serial_intr_disable_aux n´ true d0
else
match cons_intr_aux d0 with
| Some d1 ⇒ serial_intr_disable_aux n´ false d1
| None ⇒ None
end
else
Some abd
end.
Function serial_intr_disable_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
let masked :=
match nth_error (IoApicIrqs (s (ioapic abd))) 4 with
| value v ⇒
match nth_error (IoApicEnables (s (ioapic abd))) 4 with
| value true ⇒
if intr_flag abd then false
else true
| _ ⇒ true
end
| error ⇒ true
end
in
match serial_intr_disable_aux INTR_DISABLE_REC_MAX masked (abd {in_intr: true}) with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_disable_concrete_aux_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_disable_concrete_aux INTR_DISABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_enable_concrete_aux_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_disable_concrete_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_disable_concrete_aux INTR_DISABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_enable_concrete_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true})
| None ⇒ None
end
| _ ⇒ None
end.
Fixpoint serial_intr_enable_aux (n: nat) (abd: RData) {struct n} : option RData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
if SerialIrq (s (com1 abd)) then
match cons_intr_aux abd with
| Some d1 ⇒ serial_intr_enable_aux n´ d1
| None ⇒ None
end
else
Some abd
end.
Function serial_intr_enable_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match nth_error (IoApicIrqs (s (ioapic abd))) 4 with
| value v ⇒
match nth_error (IoApicEnables (s (ioapic abd))) 4 with
| value true ⇒
match serial_intr_enable_aux INTR_ENABLE_REC_MAX (abd {in_intr: true}) with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true})
| None ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End OBJ_InterruptManagement.
Ltac toIrq_inv :=
match goal with
| [H: toIrq _ = INT0 |- _] ⇒ apply toIrq_inv_0 in H
| [H: toIrq _ = INT1 |- _] ⇒ apply toIrq_inv_1 in H
| [H: toIrq _ = INT2 |- _] ⇒ apply toIrq_inv_2 in H
| [H: toIrq _ = INT3 |- _] ⇒ apply toIrq_inv_3 in H
| [H: toIrq _ = INT4 |- _] ⇒ apply toIrq_inv_4 in H
| [H: toIrq _ = INT5 |- _] ⇒ apply toIrq_inv_5 in H
| [H: toIrq _ = INT6 |- _] ⇒ apply toIrq_inv_6 in H
| [H: toIrq _ = INT7 |- _] ⇒ apply toIrq_inv_7 in H
| [H: toIrq _ = INT8 |- _] ⇒ apply toIrq_inv_8 in H
| [H: toIrq _ = INT9 |- _] ⇒ apply toIrq_inv_9 in H
| [H: toIrq _ = INT10 |- _] ⇒ apply toIrq_inv_10 in H
| [H: toIrq _ = INT11 |- _] ⇒ apply toIrq_inv_11 in H
| [H: toIrq _ = INT12 |- _] ⇒ apply toIrq_inv_12 in H
| [H: toIrq _ = INT32 |- _] ⇒ apply toIrq_inv_32 in H
| [H: toIrq _ = INT33 |- _] ⇒ apply toIrq_inv_33 in H
| [H: toIrq _ = INT34 |- _] ⇒ apply toIrq_inv_34 in H
| [H: toIrq _ = INT35 |- _] ⇒ apply toIrq_inv_35 in H
| [H: toIrq _ = INT36 |- _] ⇒ apply toIrq_inv_36 in H
| [H: toIrq _ = INT37 |- _] ⇒ apply toIrq_inv_37 in H
| [H: toIrq _ = INT38 |- _] ⇒ apply toIrq_inv_38 in H
| [H: toIrq _ = INT39 |- _] ⇒ apply toIrq_inv_39 in H
| [H: toIrq _ = INT40 |- _] ⇒ apply toIrq_inv_40 in H
| [H: toIrq _ = INT41 |- _] ⇒ apply toIrq_inv_41 in H
| [H: toIrq _ = INT42 |- _] ⇒ apply toIrq_inv_42 in H
| [H: toIrq _ = INT43 |- _] ⇒ apply toIrq_inv_43 in H
| [H: toIrq _ = INT44 |- _] ⇒ apply toIrq_inv_44 in H
| [H: toIrq _ = INT45 |- _] ⇒ apply toIrq_inv_45 in H
| [H: toIrq _ = INT46 |- _] ⇒ apply toIrq_inv_46 in H
| [H: toIrq _ = INT47 |- _] ⇒ apply toIrq_inv_47 in H
| [H: toIrq _ = INT48 |- _] ⇒ apply toIrq_inv_48 in H
| [H: toIrq _ = INT49 |- _] ⇒ apply toIrq_inv_49 in H
| [H: toIrq _ = INT50 |- _] ⇒ apply toIrq_inv_50 in H
| [H: toIrq _ = INT51 |- _] ⇒ apply toIrq_inv_51 in H
| [H: toIrq _ = INT52 |- _] ⇒ apply toIrq_inv_52 in H
| [H: toIrq _ = INT53 |- _] ⇒ apply toIrq_inv_53 in H
| [H: toIrq _ = INT54 |- _] ⇒ apply toIrq_inv_54 in H
| [H: toIrq _ = INT55 |- _] ⇒ apply toIrq_inv_55 in H
| [H: toIrq _ = INT56 |- _] ⇒ apply toIrq_inv_56 in H
| _ ⇒ idtac "cannot find toIrq _ = _"
end.
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_ENABLE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ioapic}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_intr_flag}.
Context {re5: relate_impl_com1}.
Context {re6: relate_impl_console}.
Context {re7: relate_impl_drv_serial}.
Context {re8: relate_impl_in_intr}.
Lemma serial_intr_enable_aux_exist:
∀ s n habd habd´ labd f,
serial_intr_enable_aux n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_aux n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
exploit (cons_intr_aux_exist s habd); eauto.
intros (labd´ & HP & HM).
rewrite HP.
eapply IHn; eauto.
}
{
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_enable_exist:
∀ s habd habd´ labd f,
serial_intr_enable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_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.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_enable_aux.
subrewrite.
subdestruct;
exploit serial_intr_enable_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_ioapic_update;
try eassumption.
intros (labd´ & HP & HM).
rewrite HP.
inv HQ; refine_split´; trivial.
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt5: match_impl_console}.
Context {mt6: match_impl_ioapic}.
Context {mt8: match_impl_in_intr}.
Context {mt9: match_impl_init}.
Lemma serial_intr_enable_aux_match:
∀ s n d d´ m f,
serial_intr_enable_aux n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
intros until n.
induction n.
{
Transparent serial_intr_enable_aux.
unfold serial_intr_enable_aux.
simpl; intros.
inv H; trivial.
}
{
simpl; intros.
subdestruct.
{
exploit cons_intr_aux_match; eauto.
}
{
inv H; trivial.
}
}
Qed.
Lemma serial_intr_enable_match:
∀ s d d´ m f,
serial_intr_enable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
Opaque serial_intr_enable_aux.
unfold serial_intr_enable_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_ioapic_update;
eapply match_impl_in_intr_update; eauto;
exploit serial_intr_enable_aux_match; eauto;
try eapply match_impl_in_intr_update; eauto;
intro;
eapply match_impl_in_intr_update; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_intr_enable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_intr_enable_spec}.
Lemma serial_intr_enable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_intr_enable_spec)
(id ↦ gensem serial_intr_enable_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_intr_enable_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_intr_enable_match; eauto.
Qed.
End SERIAL_INTR_ENABLE_SIM.
Section SERIAL_INTR_DISABLE_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_init}.
Context {re10: relate_impl_in_intr}.
Lemma serial_intr_disable_aux_exist:
∀ s n masked habd habd´ labd f,
serial_intr_disable_aux n masked habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_aux n masked labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
eapply IHn; eauto.
eapply relate_impl_com1_update.
assumption.
}
{
exploit (cons_intr_aux_exist s (habd { com1 : serial_intr (com1 labd)})); eauto.
eapply relate_impl_com1_update.
eassumption.
intros (labd´ & HP & HM).
rewrite HP.
eapply IHn; eauto.
}
{
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_disable_exist:
∀ s habd habd´ labd f,
serial_intr_disable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_disable_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_disable_aux.
subrewrite.
subdestruct;
exploit serial_intr_disable_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_ioapic_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial;
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt4: match_impl_curr_intr_num}.
Context {mt5: match_impl_console}.
Context {mt6: match_impl_ioapic}.
Context {mt7: match_impl_lapic}.
Context {mt8: match_impl_in_intr}.
Context {mt9: match_impl_init}.
Lemma serial_intr_disable_aux_match:
∀ s n masked d d´ m f,
serial_intr_disable_aux n masked d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
intros until n.
induction n.
{
Transparent serial_intr_disable_aux.
unfold serial_intr_disable_aux.
simpl; intros.
inv H; trivial.
}
{
simpl; intros.
subdestruct.
{
eapply IHn; eauto.
eapply match_impl_com1_update; eauto.
}
{
exploit cons_intr_aux_match; eauto.
eapply match_impl_com1_update; eauto.
}
{
inv H; trivial.
}
}
Qed.
Lemma serial_intr_disable_match:
∀ s d d´ m f,
serial_intr_disable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
Opaque serial_intr_disable_aux.
unfold serial_intr_disable_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_ioapic_update;
eapply match_impl_in_intr_update; eauto;
exploit serial_intr_disable_aux_match; eauto;
try eapply match_impl_in_intr_update; eauto;
intro;
eapply match_impl_in_intr_update; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_intr_disable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_intr_disable_spec}.
Lemma serial_intr_disable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_intr_disable_spec)
(id ↦ gensem serial_intr_disable_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_intr_disable_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_intr_disable_match; eauto.
Qed.
End SERIAL_INTR_DISABLE_SIM.
Section SERIAL_INTR_DISABLE_CONCRETE_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_init}.
Context {re10: relate_impl_in_intr}.
Lemma serial_intr_handler_exist:
∀ s b habd habd´ labd f,
serial_intr_handler habd = Some (habd´, b)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_handler labd = Some (labd´, b)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_handler.
intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_drv_serial_eq; eauto; inversion 1.
exploit relate_impl_console_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
exploit serial_hw_intr_exist; eauto; inversion 1.
destruct H13.
rewrite H13.
rewrite Hdestruct1.
exploit lapic_eoi_exist; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_ioapic_update; eauto.
inversion 1.
destruct H17.
generalize (relate_impl_ioapic_eq _ _ _ _ H15); intro tmp; rewrite tmp in H17; clear tmp.
rewrite H17.
exploit cons_intr_aux_exist; eauto; inversion 1.
destruct H19.
destruct H20.
rewrite H20.
inv HQ; refine_split´; trivial.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
generalize (relate_impl_ioapic_eq _ _ _ _ H21); intro tmp; rewrite tmp; clear tmp.
apply relate_impl_ioapic_update; eauto.
}
{
exploit serial_hw_intr_exist; eauto; inversion 1.
destruct H13.
rewrite H13.
rewrite Hdestruct1.
inv HQ; refine_split´; trivial.
apply relate_impl_com1_update; eauto.
}
{
functional inversion Hdestruct; subst.
unfold serial_hw_intr_spec.
unfold d´ in ×.
rewrite H2 in H.
rewrite H.
inv HQ; refine_split´; trivial.
}
Qed.
Lemma serial_intr_disable_concrete_aux_exist:
∀ s n habd habd´ labd f,
serial_intr_disable_concrete_aux n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_concrete_aux n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
revert H.
subrewrite.
subdestruct.
{
exploit serial_intr_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
eapply IHn; eauto.
}
{
exploit serial_intr_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_disable_concrete_exist:
∀ s habd habd´ labd f,
serial_intr_disable_concrete_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.
unfold serial_intr_disable_concrete_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_disable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_disable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial;
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Lemma serial_intr_disable_handler_exist:
∀ s habd habd´ labd f,
serial_intr_disable_concrete_aux_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_concrete_aux_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_disable_concrete_aux_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_disable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_disable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial.
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
End SERIAL_INTR_DISABLE_CONCRETE_SIM.
Section SERIAL_INTR_ENABLE_CONCRETE_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_init}.
Context {re10: relate_impl_in_intr}.
Lemma serial_intr_pending_handler_exist:
∀ s b habd habd´ labd f,
serial_intr_pending_handler habd = Some (habd´, b)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_pending_handler labd = Some (labd´, b)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_pending_handler.
intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_drv_serial_eq; eauto; inversion 1.
exploit relate_impl_console_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
exploit ic_intr_exist; eauto; inversion 1.
destruct H13.
rewrite H13.
rewrite Hdestruct2.
exploit lapic_eoi_exist; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_ioapic_update; eauto.
inversion 1.
destruct H17.
generalize (relate_impl_ioapic_eq _ _ _ _ H15); intro tmp; rewrite tmp in H17; clear tmp.
rewrite H17.
exploit cons_intr_aux_exist; eauto; inversion 1.
destruct H19.
destruct H20.
rewrite H20.
inv HQ; refine_split´; trivial.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
generalize (relate_impl_ioapic_eq _ _ _ _ H21); intro tmp; rewrite tmp; clear tmp.
apply relate_impl_ioapic_update; eauto.
}
{
inv HQ; refine_split´; trivial.
}
Qed.
Lemma serial_intr_enable_concrete_aux_exist:
∀ s n habd habd´ labd f,
serial_intr_enable_concrete_aux n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_concrete_aux n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
revert H.
subrewrite.
subdestruct.
{
exploit serial_intr_pending_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
eapply IHn; eauto.
}
{
exploit serial_intr_pending_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_enable_concrete_exist:
∀ s habd habd´ labd f,
serial_intr_enable_concrete_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.
unfold serial_intr_enable_concrete_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_enable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_enable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial;
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Lemma serial_intr_enable_handler_exist:
∀ s habd habd´ labd f,
serial_intr_enable_concrete_aux_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_concrete_aux_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_enable_concrete_aux_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_enable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_enable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial.
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
End SERIAL_INTR_ENABLE_CONCRETE_SIM.
End OBJ_SIM.
match serial_hw_intr_spec abd with
| Some (d0, n) ⇒
if zeq n 36 then
match lapic_eoi_spec (d0 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒
match iret_spec (d2 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true}) with
| Some d3 ⇒ Some (d3, true)
| None ⇒ None
end
| None ⇒ None
end
| None ⇒ None
end
else
Some (abd {com1: serial_intr (com1 abd)}, true)
| _ ⇒ Some (abd, false)
end.
Function serial_intr_pending_handler (abd: RData): option (RData × bool) :=
if SerialIrq (s (com1 abd)) then
match ic_intr_spec 4 abd with
| Some (d0, n) ⇒
if zeq n 36 then
match lapic_eoi_spec (d0 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒
match iret_spec (d2 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true}) with
| Some d3 ⇒ Some (d3, true)
| None ⇒ None
end
| None ⇒ None
end
| None ⇒ None
end
else
None
| None ⇒ None
end
else
Some (abd, false).
Function serial_intr_handler_sw_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, in_intr abd) with
| (true, true, true, true) ⇒
match lapic_eoi_spec (abd {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒ Some (d2 {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true})
| None ⇒ None
end
| None ⇒ None
end
| _ ⇒ None
end.
Definition serial_intr_handler_asm_spec (rs: regset) (abd: RData): option (RData × regset) :=
match (ikern abd, ihost abd, init abd, in_intr abd) with
| (true, true, true, true) ⇒
match lapic_eoi_spec ((save_context_spec rs abd) {ioapic / s / IoApicEnables [4%nat]: false} {intr_flag: true}) with
| Some d1 ⇒
match cons_intr_aux d1 with
| Some d2 ⇒
match restore_context_spec (d2 {ioapic / s / IoApicEnables [4%nat]: true}) with
| (rs´, d3) ⇒ Some (d3, rs´)
end
| None ⇒ None
end
| None ⇒ None
end
| _ ⇒ None
end.
Lemma lapic_eoi_spec_preserves_tf:
∀ d d´,
lapic_eoi_spec d = Some d´ →
tf d = tf d´.
Proof.
intros.
unfold lapic_eoi_spec.
functional inversion H; simpl in *; subst; simpl in ×.
reflexivity.
Qed.
Lemma cons_intr_aux_preserves_tf:
∀ d d´,
cons_intr_aux d = Some d´ →
tf d = tf d´.
Proof.
intros.
unfold cons_intr_aux.
functional inversion H; simpl in *; subst; simpl in *;
reflexivity.
Qed.
Require Import CommonTactic.
Lemma serial_intr_handler_asm_spec_inv:
∀ rs rs´ d d´,
serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
(ikern d = true ∧
ihost d = true ∧
init d = true ∧
in_intr d = true ∧
∃ d1 d2 d3 d4 d5,
save_context_spec rs d = d1 ∧
d1 {intr_flag: true} {ioapic / s / IoApicEnables [4%nat]: false} = d2 ∧
lapic_eoi_spec d2 = Some d3 ∧
cons_intr_aux d3 = Some d4 ∧
d4 {ioapic / s / IoApicEnables [4%nat]: true} = d5 ∧
restore_context_spec d5 = (rs´, d´)).
Proof.
intros rs rs´ d d´.
unfold serial_intr_handler_asm_spec.
intros H.
split; [subdestruct; auto|].
split; [subdestruct; auto|].
split; [subdestruct; auto|].
split; [subdestruct; auto|].
subdestruct.
repeat esplit.
eassumption.
eassumption.
inv H.
assumption.
Qed.
Definition serial_intr_handler_ext_spec (abd: RData): option (RData × bool) :=
match (ikern abd, ihost abd, init abd) with
| (true, true, true) ⇒
match serial_hw_intr_spec abd with
| Some (d0, n) ⇒
if zeq n 36 then
match serial_intr_handler_sw_spec d0 with
| Some d1 ⇒
match iret_spec d1 with
| Some d2 ⇒ Some (d2, true)
| None ⇒ None
end
| None ⇒ None
end
else
Some (abd {com1: serial_intr (com1 abd)}, true)
| _ ⇒ Some (abd, false)
end
| _ ⇒ None
end.
Lemma serial_intr_handler_ext_refinement:
∀ d d´ b,
serial_intr_handler_ext_spec d = Some (d´, b) →
serial_intr_handler d = Some (d´, b).
Proof.
intros d d´ b.
unfold serial_intr_handler_ext_spec.
unfold serial_intr_handler.
unfold serial_intr_handler_sw_spec.
intros Hspec.
subdestruct; eauto.
Qed.
Fixpoint serial_intr_disable_concrete_aux (n: nat) (abd: RData) {struct n} : option RData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
match serial_intr_handler abd with
| Some (d´, true) ⇒ serial_intr_disable_concrete_aux n´ d´
| Some (d´, false) ⇒ Some abd
| None ⇒ None
end
end.
Fixpoint serial_intr_enable_concrete_aux (n: nat) (abd: RData) {struct n}: option RData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
match serial_intr_pending_handler abd with
| Some (d´, true) ⇒ serial_intr_enable_concrete_aux n´ d´
| Some (d´, false) ⇒ Some abd
| None ⇒ None
end
end.
Fixpoint serial_intr_disable_aux (n: nat) (masked: bool) (abd: RData) {struct n} : option RData
:=
match n with
| O ⇒ Some abd
| S n´ ⇒
let d0 := abd {com1: serial_intr (com1 abd)} in
if SerialIrq (s (com1 d0)) then
if masked then
serial_intr_disable_aux n´ true d0
else
match cons_intr_aux d0 with
| Some d1 ⇒ serial_intr_disable_aux n´ false d1
| None ⇒ None
end
else
Some abd
end.
Function serial_intr_disable_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
let masked :=
match nth_error (IoApicIrqs (s (ioapic abd))) 4 with
| value v ⇒
match nth_error (IoApicEnables (s (ioapic abd))) 4 with
| value true ⇒
if intr_flag abd then false
else true
| _ ⇒ true
end
| error ⇒ true
end
in
match serial_intr_disable_aux INTR_DISABLE_REC_MAX masked (abd {in_intr: true}) with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_disable_concrete_aux_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_disable_concrete_aux INTR_DISABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_enable_concrete_aux_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_disable_concrete_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_disable_concrete_aux INTR_DISABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: false})
| None ⇒ None
end
| _ ⇒ None
end.
Function serial_intr_enable_concrete_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX abd with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true})
| None ⇒ None
end
| _ ⇒ None
end.
Fixpoint serial_intr_enable_aux (n: nat) (abd: RData) {struct n} : option RData :=
match n with
| O ⇒ Some abd
| S n´ ⇒
if SerialIrq (s (com1 abd)) then
match cons_intr_aux abd with
| Some d1 ⇒ serial_intr_enable_aux n´ d1
| None ⇒ None
end
else
Some abd
end.
Function serial_intr_enable_spec (abd: RData): option RData :=
match (ikern abd, ihost abd, init abd, intr_flag abd, in_intr abd) with
| (true, true, true, true, false) ⇒
match nth_error (IoApicIrqs (s (ioapic abd))) 4 with
| value v ⇒
match nth_error (IoApicEnables (s (ioapic abd))) 4 with
| value true ⇒
match serial_intr_enable_aux INTR_ENABLE_REC_MAX (abd {in_intr: true}) with
| Some d ⇒ Some (d {in_intr: false} {ioapic / s / IoApicEnables [(Z.to_nat 4)]: true})
| None ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End OBJ_InterruptManagement.
Ltac toIrq_inv :=
match goal with
| [H: toIrq _ = INT0 |- _] ⇒ apply toIrq_inv_0 in H
| [H: toIrq _ = INT1 |- _] ⇒ apply toIrq_inv_1 in H
| [H: toIrq _ = INT2 |- _] ⇒ apply toIrq_inv_2 in H
| [H: toIrq _ = INT3 |- _] ⇒ apply toIrq_inv_3 in H
| [H: toIrq _ = INT4 |- _] ⇒ apply toIrq_inv_4 in H
| [H: toIrq _ = INT5 |- _] ⇒ apply toIrq_inv_5 in H
| [H: toIrq _ = INT6 |- _] ⇒ apply toIrq_inv_6 in H
| [H: toIrq _ = INT7 |- _] ⇒ apply toIrq_inv_7 in H
| [H: toIrq _ = INT8 |- _] ⇒ apply toIrq_inv_8 in H
| [H: toIrq _ = INT9 |- _] ⇒ apply toIrq_inv_9 in H
| [H: toIrq _ = INT10 |- _] ⇒ apply toIrq_inv_10 in H
| [H: toIrq _ = INT11 |- _] ⇒ apply toIrq_inv_11 in H
| [H: toIrq _ = INT12 |- _] ⇒ apply toIrq_inv_12 in H
| [H: toIrq _ = INT32 |- _] ⇒ apply toIrq_inv_32 in H
| [H: toIrq _ = INT33 |- _] ⇒ apply toIrq_inv_33 in H
| [H: toIrq _ = INT34 |- _] ⇒ apply toIrq_inv_34 in H
| [H: toIrq _ = INT35 |- _] ⇒ apply toIrq_inv_35 in H
| [H: toIrq _ = INT36 |- _] ⇒ apply toIrq_inv_36 in H
| [H: toIrq _ = INT37 |- _] ⇒ apply toIrq_inv_37 in H
| [H: toIrq _ = INT38 |- _] ⇒ apply toIrq_inv_38 in H
| [H: toIrq _ = INT39 |- _] ⇒ apply toIrq_inv_39 in H
| [H: toIrq _ = INT40 |- _] ⇒ apply toIrq_inv_40 in H
| [H: toIrq _ = INT41 |- _] ⇒ apply toIrq_inv_41 in H
| [H: toIrq _ = INT42 |- _] ⇒ apply toIrq_inv_42 in H
| [H: toIrq _ = INT43 |- _] ⇒ apply toIrq_inv_43 in H
| [H: toIrq _ = INT44 |- _] ⇒ apply toIrq_inv_44 in H
| [H: toIrq _ = INT45 |- _] ⇒ apply toIrq_inv_45 in H
| [H: toIrq _ = INT46 |- _] ⇒ apply toIrq_inv_46 in H
| [H: toIrq _ = INT47 |- _] ⇒ apply toIrq_inv_47 in H
| [H: toIrq _ = INT48 |- _] ⇒ apply toIrq_inv_48 in H
| [H: toIrq _ = INT49 |- _] ⇒ apply toIrq_inv_49 in H
| [H: toIrq _ = INT50 |- _] ⇒ apply toIrq_inv_50 in H
| [H: toIrq _ = INT51 |- _] ⇒ apply toIrq_inv_51 in H
| [H: toIrq _ = INT52 |- _] ⇒ apply toIrq_inv_52 in H
| [H: toIrq _ = INT53 |- _] ⇒ apply toIrq_inv_53 in H
| [H: toIrq _ = INT54 |- _] ⇒ apply toIrq_inv_54 in H
| [H: toIrq _ = INT55 |- _] ⇒ apply toIrq_inv_55 in H
| [H: toIrq _ = INT56 |- _] ⇒ apply toIrq_inv_56 in H
| _ ⇒ idtac "cannot find toIrq _ = _"
end.
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_ENABLE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ioapic}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_intr_flag}.
Context {re5: relate_impl_com1}.
Context {re6: relate_impl_console}.
Context {re7: relate_impl_drv_serial}.
Context {re8: relate_impl_in_intr}.
Lemma serial_intr_enable_aux_exist:
∀ s n habd habd´ labd f,
serial_intr_enable_aux n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_aux n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
exploit (cons_intr_aux_exist s habd); eauto.
intros (labd´ & HP & HM).
rewrite HP.
eapply IHn; eauto.
}
{
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_enable_exist:
∀ s habd habd´ labd f,
serial_intr_enable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_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.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_enable_aux.
subrewrite.
subdestruct;
exploit serial_intr_enable_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_ioapic_update;
try eassumption.
intros (labd´ & HP & HM).
rewrite HP.
inv HQ; refine_split´; trivial.
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt5: match_impl_console}.
Context {mt6: match_impl_ioapic}.
Context {mt8: match_impl_in_intr}.
Context {mt9: match_impl_init}.
Lemma serial_intr_enable_aux_match:
∀ s n d d´ m f,
serial_intr_enable_aux n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
intros until n.
induction n.
{
Transparent serial_intr_enable_aux.
unfold serial_intr_enable_aux.
simpl; intros.
inv H; trivial.
}
{
simpl; intros.
subdestruct.
{
exploit cons_intr_aux_match; eauto.
}
{
inv H; trivial.
}
}
Qed.
Lemma serial_intr_enable_match:
∀ s d d´ m f,
serial_intr_enable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
Opaque serial_intr_enable_aux.
unfold serial_intr_enable_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_ioapic_update;
eapply match_impl_in_intr_update; eauto;
exploit serial_intr_enable_aux_match; eauto;
try eapply match_impl_in_intr_update; eauto;
intro;
eapply match_impl_in_intr_update; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_intr_enable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_intr_enable_spec}.
Lemma serial_intr_enable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_intr_enable_spec)
(id ↦ gensem serial_intr_enable_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_intr_enable_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_intr_enable_match; eauto.
Qed.
End SERIAL_INTR_ENABLE_SIM.
Section SERIAL_INTR_DISABLE_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_init}.
Context {re10: relate_impl_in_intr}.
Lemma serial_intr_disable_aux_exist:
∀ s n masked habd habd´ labd f,
serial_intr_disable_aux n masked habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_aux n masked labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
exploit relate_impl_com1_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
eapply IHn; eauto.
eapply relate_impl_com1_update.
assumption.
}
{
exploit (cons_intr_aux_exist s (habd { com1 : serial_intr (com1 labd)})); eauto.
eapply relate_impl_com1_update.
eassumption.
intros (labd´ & HP & HM).
rewrite HP.
eapply IHn; eauto.
}
{
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_disable_exist:
∀ s habd habd´ labd f,
serial_intr_disable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_disable_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_disable_aux.
subrewrite.
subdestruct;
exploit serial_intr_disable_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_ioapic_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial;
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt4: match_impl_curr_intr_num}.
Context {mt5: match_impl_console}.
Context {mt6: match_impl_ioapic}.
Context {mt7: match_impl_lapic}.
Context {mt8: match_impl_in_intr}.
Context {mt9: match_impl_init}.
Lemma serial_intr_disable_aux_match:
∀ s n masked d d´ m f,
serial_intr_disable_aux n masked d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
intros until n.
induction n.
{
Transparent serial_intr_disable_aux.
unfold serial_intr_disable_aux.
simpl; intros.
inv H; trivial.
}
{
simpl; intros.
subdestruct.
{
eapply IHn; eauto.
eapply match_impl_com1_update; eauto.
}
{
exploit cons_intr_aux_match; eauto.
eapply match_impl_com1_update; eauto.
}
{
inv H; trivial.
}
}
Qed.
Lemma serial_intr_disable_match:
∀ s d d´ m f,
serial_intr_disable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
Opaque serial_intr_disable_aux.
unfold serial_intr_disable_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_ioapic_update;
eapply match_impl_in_intr_update; eauto;
exploit serial_intr_disable_aux_match; eauto;
try eapply match_impl_in_intr_update; eauto;
intro;
eapply match_impl_in_intr_update; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) serial_intr_disable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) serial_intr_disable_spec}.
Lemma serial_intr_disable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem serial_intr_disable_spec)
(id ↦ gensem serial_intr_disable_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit serial_intr_disable_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply serial_intr_disable_match; eauto.
Qed.
End SERIAL_INTR_DISABLE_SIM.
Section SERIAL_INTR_DISABLE_CONCRETE_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_init}.
Context {re10: relate_impl_in_intr}.
Lemma serial_intr_handler_exist:
∀ s b habd habd´ labd f,
serial_intr_handler habd = Some (habd´, b)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_handler labd = Some (labd´, b)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_handler.
intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_drv_serial_eq; eauto; inversion 1.
exploit relate_impl_console_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
exploit serial_hw_intr_exist; eauto; inversion 1.
destruct H13.
rewrite H13.
rewrite Hdestruct1.
exploit lapic_eoi_exist; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_ioapic_update; eauto.
inversion 1.
destruct H17.
generalize (relate_impl_ioapic_eq _ _ _ _ H15); intro tmp; rewrite tmp in H17; clear tmp.
rewrite H17.
exploit cons_intr_aux_exist; eauto; inversion 1.
destruct H19.
destruct H20.
rewrite H20.
inv HQ; refine_split´; trivial.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
generalize (relate_impl_ioapic_eq _ _ _ _ H21); intro tmp; rewrite tmp; clear tmp.
apply relate_impl_ioapic_update; eauto.
}
{
exploit serial_hw_intr_exist; eauto; inversion 1.
destruct H13.
rewrite H13.
rewrite Hdestruct1.
inv HQ; refine_split´; trivial.
apply relate_impl_com1_update; eauto.
}
{
functional inversion Hdestruct; subst.
unfold serial_hw_intr_spec.
unfold d´ in ×.
rewrite H2 in H.
rewrite H.
inv HQ; refine_split´; trivial.
}
Qed.
Lemma serial_intr_disable_concrete_aux_exist:
∀ s n habd habd´ labd f,
serial_intr_disable_concrete_aux n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_concrete_aux n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
revert H.
subrewrite.
subdestruct.
{
exploit serial_intr_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
eapply IHn; eauto.
}
{
exploit serial_intr_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_disable_concrete_exist:
∀ s habd habd´ labd f,
serial_intr_disable_concrete_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.
unfold serial_intr_disable_concrete_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_disable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_disable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial;
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Lemma serial_intr_disable_handler_exist:
∀ s habd habd´ labd f,
serial_intr_disable_concrete_aux_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_disable_concrete_aux_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_disable_concrete_aux_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_disable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_disable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial.
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
End SERIAL_INTR_DISABLE_CONCRETE_SIM.
Section SERIAL_INTR_ENABLE_CONCRETE_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_init}.
Context {re10: relate_impl_in_intr}.
Lemma serial_intr_pending_handler_exist:
∀ s b habd habd´ labd f,
serial_intr_pending_handler habd = Some (habd´, b)
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_pending_handler labd = Some (labd´, b)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_pending_handler.
intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_com1_eq; eauto; inversion 1.
exploit relate_impl_drv_serial_eq; eauto; inversion 1.
exploit relate_impl_console_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
revert H.
subrewrite.
subdestruct.
{
exploit ic_intr_exist; eauto; inversion 1.
destruct H13.
rewrite H13.
rewrite Hdestruct2.
exploit lapic_eoi_exist; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_ioapic_update; eauto.
inversion 1.
destruct H17.
generalize (relate_impl_ioapic_eq _ _ _ _ H15); intro tmp; rewrite tmp in H17; clear tmp.
rewrite H17.
exploit cons_intr_aux_exist; eauto; inversion 1.
destruct H19.
destruct H20.
rewrite H20.
inv HQ; refine_split´; trivial.
apply relate_impl_in_intr_update; eauto.
apply relate_impl_intr_flag_update; eauto.
apply relate_impl_curr_intr_num_update; eauto.
generalize (relate_impl_ioapic_eq _ _ _ _ H21); intro tmp; rewrite tmp; clear tmp.
apply relate_impl_ioapic_update; eauto.
}
{
inv HQ; refine_split´; trivial.
}
Qed.
Lemma serial_intr_enable_concrete_aux_exist:
∀ s n habd habd´ labd f,
serial_intr_enable_concrete_aux n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_concrete_aux n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
intros until n.
induction n.
{
simpl.
intros.
inv H; refine_split´; trivial.
}
{
simpl.
intros.
revert H.
subrewrite.
subdestruct.
{
exploit serial_intr_pending_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
eapply IHn; eauto.
}
{
exploit serial_intr_pending_handler_exist; eauto; inversion 1.
destruct H1.
rewrite H1.
inv HQ; refine_split´; trivial.
}
}
Qed.
Lemma serial_intr_enable_concrete_exist:
∀ s habd habd´ labd f,
serial_intr_enable_concrete_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.
unfold serial_intr_enable_concrete_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_enable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_enable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial;
generalize (relate_impl_ioapic_eq _ _ _ _ HM); intro tmp; rewrite tmp; clear tmp;
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
Lemma serial_intr_enable_handler_exist:
∀ s habd habd´ labd f,
serial_intr_enable_concrete_aux_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, serial_intr_enable_concrete_aux_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold serial_intr_enable_concrete_aux_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_intr_flag_eq; eauto; inversion 1.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
revert H.
Opaque serial_intr_enable_concrete_aux.
subrewrite.
subdestruct;
exploit serial_intr_enable_concrete_aux_exist; eauto;
try apply relate_impl_in_intr_update;
try apply relate_impl_intr_flag_update;
try eassumption;
intros (labd´ & HP & HM);
rewrite HP;
inv HQ; refine_split´; trivial.
try apply relate_impl_ioapic_update;
try apply relate_impl_intr_flag_update;
try apply relate_impl_in_intr_update;
assumption.
Qed.
End SERIAL_INTR_ENABLE_CONCRETE_SIM.
End OBJ_SIM.