Library mcertikos.devdrivers.DSerialCode_ioapic_unmask
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import FutureTactic.
Require Import List.
Require Import AbstractDataType.
Require Import IoApicGenSpec.
Require Import ObjInterruptDriver.
Require Import DSerial.
Require Import DeviceStateDataType.
Require Import INVLemmaDriver.
Require Import DSerialCSource.
Require Import XOmega.
Module DSERIALCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section IOAPICUNMASK.
Let L: compatlayer (cdata RData) :=
ioapic_read ↦ gensem ioapic_read_spec
⊕ ioapic_write ↦ gensem ioapic_write_spec
⊕ local_irq_save ↦ gensem local_irq_save_spec
⊕ local_irq_restore ↦ gensem local_irq_restore_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section IoApicUnmaskBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bioapic_read: block).
Hypothesis hioapic_read1 : Genv.find_symbol ge ioapic_read = Some bioapic_read.
Hypothesis hioapic_read2 : Genv.find_funct_ptr ge bioapic_read =
Some (External (EF_external ioapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (bioapic_write: block).
Hypothesis hioapic_write1 : Genv.find_symbol ge ioapic_write = Some bioapic_write.
Hypothesis hioapic_write2 : Genv.find_funct_ptr ge bioapic_write =
Some (External (EF_external ioapic_write
(signature_of_type (Tcons tuint (Tcons tuint Tnil))
tvoid
cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Variable (blocal_irq_save: block).
Hypothesis hlocal_irq_save1 : Genv.find_symbol ge local_irq_save = Some blocal_irq_save.
Hypothesis hlocal_irq_save2 : Genv.find_funct_ptr ge blocal_irq_save =
Some (External (EF_external local_irq_save
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (blocal_irq_restore: block).
Hypothesis hlocal_irq_restore1 : Genv.find_symbol ge local_irq_restore = Some blocal_irq_restore.
Hypothesis hlocal_irq_restore2 : Genv.find_funct_ptr ge blocal_irq_restore =
Some (External (EF_external local_irq_restore
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Ltac unfold_data :=
unfold update_ioapic; unfold update_s; simpl; unfold_IoApicState; unfold_RData.
Ltac unfold_read_spec :=
unfold ioapic_read_spec;
unfold ioapic_valid_read_range; simpl;
unfold ioapic_read_1; simpl;
unfold ioapic_read_0; simpl.
Ltac unfold_write_spec :=
unfold ioapic_write_spec;
unfold ioapic_valid_write_range; simpl;
unfold low32_to_irq; simpl;
unfold low32_to_enable; simpl.
Lemma ioapic_unmask_body_correct:
∀ m d d´ env le i,
env = PTree.empty _ →
high_level_invariant d →
PTree.get _irq le = Some (Vint i) →
ioapic_unmask_spec (Int.unsigned i) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) ioapic_unmask_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le i Henv Hinv Hlei Hspec.
functional inversion Hspec. subst. clear Hspec.
inversion Hinv. clear Hinv.
generalize (valid_ioapic_state_range (Z.to_nat (Int.unsigned i))). intros Hni.
destruct (nth (Z.to_nat (Int.unsigned i)) (IoApicEnables (s (ioapic d))) false) eqn: x.
{
destruct d; destruct ioapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold ioapic_unmask_body.
Opaque Z.add Z.mul.
repeat vcgen.
{
replace (Int.unsigned i - 0) with (Int.unsigned i) by omega.
remember (16 + 2 × Int.unsigned i) as n.
unfold_read_spec.
Transparent Z.add Z.mul.
if_false. if_false.
rewrite Heqn. if_true. rewrite <- Heqn.
unfold_data. unfold ioapic_read_tbl. rewrite Heqn. calc. simpl.
rewrite x. calc. rewrite Int.unsigned_repr. reflexivity.
- omega.
- omega.
}
{
Opaque Z.add Z.mul.
unfold_write_spec.
if_false.
Transparent Z.add Z.mul.
calc. if_true.
if_false.
if_true.
unfold addr_to_idx. calc. if_true.
Opaque Z.add Z.mul.
unfold_data.
- reflexivity.
- calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
- intros H. apply H. calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
}
{
apply Z_land_range_lo. rewrite Int.unsigned_repr; omega.
}
{
unfold local_irq_restore_spec. simpl. unfold_data.
unfold ret; simpl.
case_eq (saved_intr_flags ++ intr_flag :: nil); intros.
eapply app_eq_nil in H.
destruct H as [? contra].
inv contra.
f_equal. f_equal. f_equal. f_equal.
{
Transparent Z.add Z.mul.
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
rewrite Int.unsigned_repr.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
unfold Int.modulus, two_power_nat; simpl.
replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=16%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
rewrite Z.lor_0_l. calc. replace (2 ^ 16) with 65536.
rewrite Zmod_small with (x:= irqn) by omega.
rewrite Zmod_small by omega.
rewrite Heqirqn. rewrite replace_nth_eq. reflexivity.
calc. reflexivity. omega. calc. reflexivity.
calc. replace (2 ^ 16) with 65536. omega.
calc. reflexivity.
calc. replace (2 ^ 16) with 65536. calc. reflexivity.
calc. reflexivity.
vm_compute. reflexivity.
omega. simpl. omega.
omega. omega. omega.
}
{
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
simpl. replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=16%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
rewrite Z.lor_0_l. calc. replace (2 ^ 16) with 65536.
rewrite Zmod_small with (x:=irqn) by omega.
rewrite Zdiv_small by omega. simpl.
reflexivity.
calc. reflexivity.
omega.
calc. reflexivity.
calc. replace (2 ^ 16) with 65536. omega.
calc. reflexivity. calc. replace (2 ^ 16) with 65536. calc. reflexivity.
calc. reflexivity.
vm_compute. reflexivity.
omega. simpl. omega.
omega. omega. omega.
}
rewrite <- H.
rewrite last_concat.
reflexivity.
intro contra; inv contra.
rewrite <- H.
rewrite removelast_app.
simpl.
rewrite app_nil_r.
reflexivity.
intro contra; inv contra.
}
}
{
destruct d; destruct ioapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold ioapic_unmask_body.
Opaque Z.add Z.mul.
repeat vcgen.
{
replace (Int.unsigned i - 0) with (Int.unsigned i) by omega.
remember (16 + 2 × Int.unsigned i) as n.
unfold_read_spec.
Transparent Z.add Z.mul.
if_false. if_false.
rewrite Heqn. if_true. rewrite <- Heqn.
unfold_data. unfold ioapic_read_tbl. rewrite Heqn. calc. simpl.
rewrite x. calc. rewrite Int.unsigned_repr. reflexivity.
- omega.
- omega.
}
{
Opaque Z.add Z.mul.
unfold_write_spec.
if_false.
Transparent Z.add Z.mul.
calc. if_true.
if_false.
if_true.
unfold addr_to_idx. calc. if_true.
Opaque Z.add Z.mul.
unfold_data.
- reflexivity.
- calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
- intros H. apply H. calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
}
{
apply Z_land_range_lo. rewrite Int.unsigned_repr; omega.
}
{
unfold local_irq_restore_spec. simpl. unfold_data.
unfold ret; simpl.
case_eq (saved_intr_flags ++ intr_flag :: nil); intros.
eapply app_eq_nil in H.
destruct H as [? contra].
inv contra.
f_equal. f_equal. f_equal. f_equal.
{
Transparent Z.add Z.mul.
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
rewrite Int.unsigned_repr.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
unfold Int.modulus, two_power_nat; simpl.
replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=17%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
calc. change (2 ^ 16) with 65536. calc.
rewrite Z.lor_0_l.
rewrite Zmod_small by omega.
rewrite Heqirqn. rewrite replace_nth_eq. reflexivity. omega.
calc. reflexivity. calc. change (2 ^ 17) with 131072. omega.
calc. vm_compute. reflexivity.
vm_compute. reflexivity.
omega. simpl. omega.
omega. omega. omega.
}
{
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
simpl. replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=17%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
rewrite Z.lor_0_l. calc. change (2 ^ 16) with 65536.
rewrite Z_add_mod_same.
rewrite Zmod_small with (x:=irqn) by omega.
rewrite Zdiv_small with (x:=irqn) by omega.
simpl.
reflexivity.
omega. omega.
calc. reflexivity.
calc. change (2 ^ 17) with 131072. omega.
calc. change (2 ^ 17) with 131072. calc. reflexivity.
vm_compute.
reflexivity.
omega.
simpl. omega.
omega.
omega.
omega.
}
rewrite <- H.
rewrite last_concat.
reflexivity.
intro contra; inv contra.
rewrite <- H.
rewrite removelast_app.
simpl.
rewrite app_nil_r.
reflexivity.
intro contra; inv contra.
}
}
Qed.
End IoApicUnmaskBody.
Theorem ioapic_unmask_code_correct:
spec_le
(ioapic_unmask ↦ ioapic_unmask_spec_low)
(〚ioapic_unmask ↦ f_ioapic_unmask 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(ioapic_unmask_body_correct
s
(Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ioapic_unmask)
(Vint i :: nil)
(create_undef_temps (fn_temps f_ioapic_unmask))
)
) H0.
Qed.
End IOAPICUNMASK.
End WithPrimitives.
End DSERIALCODE.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import FutureTactic.
Require Import List.
Require Import AbstractDataType.
Require Import IoApicGenSpec.
Require Import ObjInterruptDriver.
Require Import DSerial.
Require Import DeviceStateDataType.
Require Import INVLemmaDriver.
Require Import DSerialCSource.
Require Import XOmega.
Module DSERIALCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section IOAPICUNMASK.
Let L: compatlayer (cdata RData) :=
ioapic_read ↦ gensem ioapic_read_spec
⊕ ioapic_write ↦ gensem ioapic_write_spec
⊕ local_irq_save ↦ gensem local_irq_save_spec
⊕ local_irq_restore ↦ gensem local_irq_restore_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section IoApicUnmaskBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bioapic_read: block).
Hypothesis hioapic_read1 : Genv.find_symbol ge ioapic_read = Some bioapic_read.
Hypothesis hioapic_read2 : Genv.find_funct_ptr ge bioapic_read =
Some (External (EF_external ioapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (bioapic_write: block).
Hypothesis hioapic_write1 : Genv.find_symbol ge ioapic_write = Some bioapic_write.
Hypothesis hioapic_write2 : Genv.find_funct_ptr ge bioapic_write =
Some (External (EF_external ioapic_write
(signature_of_type (Tcons tuint (Tcons tuint Tnil))
tvoid
cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Variable (blocal_irq_save: block).
Hypothesis hlocal_irq_save1 : Genv.find_symbol ge local_irq_save = Some blocal_irq_save.
Hypothesis hlocal_irq_save2 : Genv.find_funct_ptr ge blocal_irq_save =
Some (External (EF_external local_irq_save
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (blocal_irq_restore: block).
Hypothesis hlocal_irq_restore1 : Genv.find_symbol ge local_irq_restore = Some blocal_irq_restore.
Hypothesis hlocal_irq_restore2 : Genv.find_funct_ptr ge blocal_irq_restore =
Some (External (EF_external local_irq_restore
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Ltac unfold_data :=
unfold update_ioapic; unfold update_s; simpl; unfold_IoApicState; unfold_RData.
Ltac unfold_read_spec :=
unfold ioapic_read_spec;
unfold ioapic_valid_read_range; simpl;
unfold ioapic_read_1; simpl;
unfold ioapic_read_0; simpl.
Ltac unfold_write_spec :=
unfold ioapic_write_spec;
unfold ioapic_valid_write_range; simpl;
unfold low32_to_irq; simpl;
unfold low32_to_enable; simpl.
Lemma ioapic_unmask_body_correct:
∀ m d d´ env le i,
env = PTree.empty _ →
high_level_invariant d →
PTree.get _irq le = Some (Vint i) →
ioapic_unmask_spec (Int.unsigned i) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) ioapic_unmask_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le i Henv Hinv Hlei Hspec.
functional inversion Hspec. subst. clear Hspec.
inversion Hinv. clear Hinv.
generalize (valid_ioapic_state_range (Z.to_nat (Int.unsigned i))). intros Hni.
destruct (nth (Z.to_nat (Int.unsigned i)) (IoApicEnables (s (ioapic d))) false) eqn: x.
{
destruct d; destruct ioapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold ioapic_unmask_body.
Opaque Z.add Z.mul.
repeat vcgen.
{
replace (Int.unsigned i - 0) with (Int.unsigned i) by omega.
remember (16 + 2 × Int.unsigned i) as n.
unfold_read_spec.
Transparent Z.add Z.mul.
if_false. if_false.
rewrite Heqn. if_true. rewrite <- Heqn.
unfold_data. unfold ioapic_read_tbl. rewrite Heqn. calc. simpl.
rewrite x. calc. rewrite Int.unsigned_repr. reflexivity.
- omega.
- omega.
}
{
Opaque Z.add Z.mul.
unfold_write_spec.
if_false.
Transparent Z.add Z.mul.
calc. if_true.
if_false.
if_true.
unfold addr_to_idx. calc. if_true.
Opaque Z.add Z.mul.
unfold_data.
- reflexivity.
- calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
- intros H. apply H. calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
}
{
apply Z_land_range_lo. rewrite Int.unsigned_repr; omega.
}
{
unfold local_irq_restore_spec. simpl. unfold_data.
unfold ret; simpl.
case_eq (saved_intr_flags ++ intr_flag :: nil); intros.
eapply app_eq_nil in H.
destruct H as [? contra].
inv contra.
f_equal. f_equal. f_equal. f_equal.
{
Transparent Z.add Z.mul.
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
rewrite Int.unsigned_repr.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
unfold Int.modulus, two_power_nat; simpl.
replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=16%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
rewrite Z.lor_0_l. calc. replace (2 ^ 16) with 65536.
rewrite Zmod_small with (x:= irqn) by omega.
rewrite Zmod_small by omega.
rewrite Heqirqn. rewrite replace_nth_eq. reflexivity.
calc. reflexivity. omega. calc. reflexivity.
calc. replace (2 ^ 16) with 65536. omega.
calc. reflexivity.
calc. replace (2 ^ 16) with 65536. calc. reflexivity.
calc. reflexivity.
vm_compute. reflexivity.
omega. simpl. omega.
omega. omega. omega.
}
{
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
simpl. replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=16%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
rewrite Z.lor_0_l. calc. replace (2 ^ 16) with 65536.
rewrite Zmod_small with (x:=irqn) by omega.
rewrite Zdiv_small by omega. simpl.
reflexivity.
calc. reflexivity.
omega.
calc. reflexivity.
calc. replace (2 ^ 16) with 65536. omega.
calc. reflexivity. calc. replace (2 ^ 16) with 65536. calc. reflexivity.
calc. reflexivity.
vm_compute. reflexivity.
omega. simpl. omega.
omega. omega. omega.
}
rewrite <- H.
rewrite last_concat.
reflexivity.
intro contra; inv contra.
rewrite <- H.
rewrite removelast_app.
simpl.
rewrite app_nil_r.
reflexivity.
intro contra; inv contra.
}
}
{
destruct d; destruct ioapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold ioapic_unmask_body.
Opaque Z.add Z.mul.
repeat vcgen.
{
replace (Int.unsigned i - 0) with (Int.unsigned i) by omega.
remember (16 + 2 × Int.unsigned i) as n.
unfold_read_spec.
Transparent Z.add Z.mul.
if_false. if_false.
rewrite Heqn. if_true. rewrite <- Heqn.
unfold_data. unfold ioapic_read_tbl. rewrite Heqn. calc. simpl.
rewrite x. calc. rewrite Int.unsigned_repr. reflexivity.
- omega.
- omega.
}
{
Opaque Z.add Z.mul.
unfold_write_spec.
if_false.
Transparent Z.add Z.mul.
calc. if_true.
if_false.
if_true.
unfold addr_to_idx. calc. if_true.
Opaque Z.add Z.mul.
unfold_data.
- reflexivity.
- calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
- intros H. apply H. calc. replace (16 + 2 × Int.unsigned i) with ((8 + Int.unsigned i) × 2) by omega.
rewrite Z_mod_mult. reflexivity.
}
{
apply Z_land_range_lo. rewrite Int.unsigned_repr; omega.
}
{
unfold local_irq_restore_spec. simpl. unfold_data.
unfold ret; simpl.
case_eq (saved_intr_flags ++ intr_flag :: nil); intros.
eapply app_eq_nil in H.
destruct H as [? contra].
inv contra.
f_equal. f_equal. f_equal. f_equal.
{
Transparent Z.add Z.mul.
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
rewrite Int.unsigned_repr.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
unfold Int.modulus, two_power_nat; simpl.
replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=17%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
calc. change (2 ^ 16) with 65536. calc.
rewrite Z.lor_0_l.
rewrite Zmod_small by omega.
rewrite Heqirqn. rewrite replace_nth_eq. reflexivity. omega.
calc. reflexivity. calc. change (2 ^ 17) with 131072. omega.
calc. vm_compute. reflexivity.
vm_compute. reflexivity.
omega. simpl. omega.
omega. omega. omega.
}
{
rewrite Z.mul_comm. rewrite Z.div_mul.
remember (Z.to_nat (Int.unsigned i)) as ni.
remember (nth ni IoApicIrqs 0) as irqn.
unfold Int.not.
unfold Int.xor.
rewrite Int.unsigned_mone.
repeat rewrite Int.unsigned_repr.
simpl. replace 4294901759 with (Z.lor 4294836224 65535).
rewrite Z.land_lor_distr_r.
rewrite land_eq_0 with (n:=17%nat) at 1.
rewrite land_eq_smaller with (n:=16%nat) at 1.
rewrite Z.lor_0_l. calc. change (2 ^ 16) with 65536.
rewrite Z_add_mod_same.
rewrite Zmod_small with (x:=irqn) by omega.
rewrite Zdiv_small with (x:=irqn) by omega.
simpl.
reflexivity.
omega. omega.
calc. reflexivity.
calc. change (2 ^ 17) with 131072. omega.
calc. change (2 ^ 17) with 131072. calc. reflexivity.
vm_compute.
reflexivity.
omega.
simpl. omega.
omega.
omega.
omega.
}
rewrite <- H.
rewrite last_concat.
reflexivity.
intro contra; inv contra.
rewrite <- H.
rewrite removelast_app.
simpl.
rewrite app_nil_r.
reflexivity.
intro contra; inv contra.
}
}
Qed.
End IoApicUnmaskBody.
Theorem ioapic_unmask_code_correct:
spec_le
(ioapic_unmask ↦ ioapic_unmask_spec_low)
(〚ioapic_unmask ↦ f_ioapic_unmask 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(ioapic_unmask_body_correct
s
(Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ioapic_unmask)
(Vint i :: nil)
(create_undef_temps (fn_temps f_ioapic_unmask))
)
) H0.
Qed.
End IOAPICUNMASK.
End WithPrimitives.
End DSERIALCODE.