Library mcertikos.devdrivers.DHandlerOpCode
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 AbstractDataType.
Require Import HandlerGenSpec.
Require Import ObjInterruptController.
Require Import ObjConsole.
Require Import FutureTactic.
Require Import INVLemmaDriver.
Require Import INVLemmaInterrupt.
Require Import ObjInterruptManagement.
Require Import CommonTactic.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import DHandlerOp.
Require Import FutureTactic.
Require Import DHandlerOpCSource.
Require Import ObjInterruptController.
Module DHANDLEROPCODE.
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.
Lemma intr_flag_eq:
∀ d, intr_flag d = true → d = d {intr_flag: true}.
Proof.
intros.
destruct d.
simpl in ×.
rewrite H.
reflexivity.
Qed.
Section SERIAL_INTR_ENABLE.
Let L: compatlayer (cdata RData) :=
serial_intr_enable_handler ↦ gensem serial_intr_enable_concrete_aux_spec
⊕ ioapic_unmask ↦ gensem ioapic_unmask_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 Serial_Intr_Enable_Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bserial_intr_enable_handler: block).
Hypothesis hserial_intr_enable_handler1 : Genv.find_symbol ge serial_intr_enable_handler = Some bserial_intr_enable_handler.
Hypothesis hserial_intr_enable_handler2 : Genv.find_funct_ptr ge bserial_intr_enable_handler = Some (External (EF_external serial_intr_enable_handler (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
Variable (bioapic_unmask: block).
Hypothesis hioapic_unmask1 : Genv.find_symbol ge ioapic_unmask = Some bioapic_unmask.
Hypothesis hioapic_unmask2 : Genv.find_funct_ptr ge bioapic_unmask = Some (External (EF_external ioapic_unmask (signature_of_type (Tcons tuint Tnil) tvoid cc_default)) (Tcons tuint Tnil) tvoid cc_default).
Lemma serial_intr_pending_handler_preserves_all:
∀ d d´ b,
serial_intr_pending_handler d = Some (d´, b) →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
functional inversion H; subst.
functional inversion H7; functional inversion H6; functional inversion H5; functional inversion H3; functional inversion H24; simpl in *; subst.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
Qed.
Lemma serial_intr_enable_concrete_aux_preserves_all:
∀ n d d´,
serial_intr_enable_concrete_aux n d = Some d´ →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
induction n.
simpl.
intros.
inv H; eauto.
simpl.
intros.
subdestruct.
inv Hdestruct0.
eapply IHn in H; eauto.
generalize (serial_intr_pending_handler_preserves_all _ _ _ Hdestruct); intro.
destruct H0 as (? & ? & ? & ? & ?).
rewrite H0, H1, H2, H3, H4 in H.
assumption.
inv Hdestruct0.
inv H.
eauto.
Qed.
Lemma serial_intr_enable_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_intr_enable_concrete_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_enable_concrete_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold serial_intr_enable_concrete_body.
functional inversion H1; subst.
esplit.
repeat vcgen.
unfold ioapic_unmask_spec; simpl.
eapply serial_intr_enable_concrete_aux_preserves_all in H7.
destruct H7 as (? & ? & ? & ? & ?).
rewrite H, H7, H8, H4, H5, H6.
inv H0.
destruct (zle_lt 0 4 (Zlength (IoApicEnables (s (ioapic d0))))); try omega.
reflexivity.
Qed.
End Serial_Intr_Enable_Body.
Theorem serial_intr_enable_code_correct:
spec_le
(serial_intr_enable ↦ serial_intr_enable_spec_low)
(〚serial_intr_enable ↦ f_serial_intr_enable_concrete 〛L).
Proof.
fbigstep_pre L.
fbigstep
(serial_intr_enable_body_correct s
(Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_intr_enable_concrete) nil
(create_undef_temps (fn_temps f_serial_intr_enable_concrete))
)
) H0.
Qed.
End SERIAL_INTR_ENABLE.
Section SERIAL_INTR_DISABLE.
Let L: compatlayer (cdata RData) :=
serial_intr_disable_handler ↦ gensem serial_intr_disable_concrete_aux_spec
⊕ ioapic_mask ↦ gensem ioapic_mask_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 Serial_Intr_Disable_Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bserial_intr_disable_handler: block).
Hypothesis hserial_intr_disable_handler1 : Genv.find_symbol ge serial_intr_disable_handler = Some bserial_intr_disable_handler.
Hypothesis hserial_intr_disable_handler2 : Genv.find_funct_ptr ge bserial_intr_disable_handler = Some (External (EF_external serial_intr_disable_handler (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
Variable (bioapic_mask: block).
Hypothesis hioapic_mask1 : Genv.find_symbol ge ioapic_mask = Some bioapic_mask.
Hypothesis hioapic_mask2 : Genv.find_funct_ptr ge bioapic_mask = Some (External (EF_external ioapic_mask (signature_of_type (Tcons tuint Tnil) tvoid cc_default)) (Tcons tuint Tnil) tvoid cc_default).
Lemma serial_intr_handler_preserves_all:
∀ d d´ b,
serial_intr_handler d = Some (d´, b) →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
functional inversion H; subst.
functional inversion H6; functional inversion H5; functional inversion H4; functional inversion H2; functional inversion H24; simpl in *; subst.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
eauto.
Qed.
Lemma serial_intr_diable_concrete_aux_preserves_all:
∀ n d d´,
serial_intr_disable_concrete_aux n d = Some d´ →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
induction n.
simpl.
intros.
inv H; eauto.
simpl.
intros.
subdestruct.
inv Hdestruct0.
eapply IHn in H; eauto.
generalize (serial_intr_handler_preserves_all _ _ _ Hdestruct); intro.
destruct H0 as (? & ? & ? & ? & ?).
rewrite H0, H1, H2, H3, H4 in H.
assumption.
inv Hdestruct0.
inv H.
eauto.
Qed.
Lemma serial_intr_disable_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_intr_disable_concrete_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_disable_concrete_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold serial_intr_disable_concrete_body.
functional inversion H1; subst.
esplit.
repeat vcgen.
unfold ioapic_mask_spec; simpl.
eapply serial_intr_diable_concrete_aux_preserves_all in H7.
destruct H7 as (? & ? & ? & ? & ?).
rewrite H, H7, H8, H4, H5, H6.
inv H0.
destruct (zle_lt 0 4 (Zlength (IoApicEnables (s (ioapic d0))))); try omega.
reflexivity.
Qed.
End Serial_Intr_Disable_Body.
Theorem serial_intr_disable_code_correct:
spec_le
(serial_intr_disable ↦ serial_intr_disable_spec_low)
(〚serial_intr_disable ↦ f_serial_intr_disable_concrete 〛L).
Proof.
fbigstep_pre L.
fbigstep
(serial_intr_disable_body_correct s
(Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_intr_disable_concrete) nil
(create_undef_temps (fn_temps f_serial_intr_disable_concrete))
)
) H0.
Qed.
End SERIAL_INTR_DISABLE.
End WithPrimitives.
End DHANDLEROPCODE.
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 AbstractDataType.
Require Import HandlerGenSpec.
Require Import ObjInterruptController.
Require Import ObjConsole.
Require Import FutureTactic.
Require Import INVLemmaDriver.
Require Import INVLemmaInterrupt.
Require Import ObjInterruptManagement.
Require Import CommonTactic.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import DHandlerOp.
Require Import FutureTactic.
Require Import DHandlerOpCSource.
Require Import ObjInterruptController.
Module DHANDLEROPCODE.
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.
Lemma intr_flag_eq:
∀ d, intr_flag d = true → d = d {intr_flag: true}.
Proof.
intros.
destruct d.
simpl in ×.
rewrite H.
reflexivity.
Qed.
Section SERIAL_INTR_ENABLE.
Let L: compatlayer (cdata RData) :=
serial_intr_enable_handler ↦ gensem serial_intr_enable_concrete_aux_spec
⊕ ioapic_unmask ↦ gensem ioapic_unmask_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 Serial_Intr_Enable_Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bserial_intr_enable_handler: block).
Hypothesis hserial_intr_enable_handler1 : Genv.find_symbol ge serial_intr_enable_handler = Some bserial_intr_enable_handler.
Hypothesis hserial_intr_enable_handler2 : Genv.find_funct_ptr ge bserial_intr_enable_handler = Some (External (EF_external serial_intr_enable_handler (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
Variable (bioapic_unmask: block).
Hypothesis hioapic_unmask1 : Genv.find_symbol ge ioapic_unmask = Some bioapic_unmask.
Hypothesis hioapic_unmask2 : Genv.find_funct_ptr ge bioapic_unmask = Some (External (EF_external ioapic_unmask (signature_of_type (Tcons tuint Tnil) tvoid cc_default)) (Tcons tuint Tnil) tvoid cc_default).
Lemma serial_intr_pending_handler_preserves_all:
∀ d d´ b,
serial_intr_pending_handler d = Some (d´, b) →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
functional inversion H; subst.
functional inversion H7; functional inversion H6; functional inversion H5; functional inversion H3; functional inversion H24; simpl in *; subst.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
Qed.
Lemma serial_intr_enable_concrete_aux_preserves_all:
∀ n d d´,
serial_intr_enable_concrete_aux n d = Some d´ →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
induction n.
simpl.
intros.
inv H; eauto.
simpl.
intros.
subdestruct.
inv Hdestruct0.
eapply IHn in H; eauto.
generalize (serial_intr_pending_handler_preserves_all _ _ _ Hdestruct); intro.
destruct H0 as (? & ? & ? & ? & ?).
rewrite H0, H1, H2, H3, H4 in H.
assumption.
inv Hdestruct0.
inv H.
eauto.
Qed.
Lemma serial_intr_enable_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_intr_enable_concrete_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_enable_concrete_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold serial_intr_enable_concrete_body.
functional inversion H1; subst.
esplit.
repeat vcgen.
unfold ioapic_unmask_spec; simpl.
eapply serial_intr_enable_concrete_aux_preserves_all in H7.
destruct H7 as (? & ? & ? & ? & ?).
rewrite H, H7, H8, H4, H5, H6.
inv H0.
destruct (zle_lt 0 4 (Zlength (IoApicEnables (s (ioapic d0))))); try omega.
reflexivity.
Qed.
End Serial_Intr_Enable_Body.
Theorem serial_intr_enable_code_correct:
spec_le
(serial_intr_enable ↦ serial_intr_enable_spec_low)
(〚serial_intr_enable ↦ f_serial_intr_enable_concrete 〛L).
Proof.
fbigstep_pre L.
fbigstep
(serial_intr_enable_body_correct s
(Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_intr_enable_concrete) nil
(create_undef_temps (fn_temps f_serial_intr_enable_concrete))
)
) H0.
Qed.
End SERIAL_INTR_ENABLE.
Section SERIAL_INTR_DISABLE.
Let L: compatlayer (cdata RData) :=
serial_intr_disable_handler ↦ gensem serial_intr_disable_concrete_aux_spec
⊕ ioapic_mask ↦ gensem ioapic_mask_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 Serial_Intr_Disable_Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bserial_intr_disable_handler: block).
Hypothesis hserial_intr_disable_handler1 : Genv.find_symbol ge serial_intr_disable_handler = Some bserial_intr_disable_handler.
Hypothesis hserial_intr_disable_handler2 : Genv.find_funct_ptr ge bserial_intr_disable_handler = Some (External (EF_external serial_intr_disable_handler (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
Variable (bioapic_mask: block).
Hypothesis hioapic_mask1 : Genv.find_symbol ge ioapic_mask = Some bioapic_mask.
Hypothesis hioapic_mask2 : Genv.find_funct_ptr ge bioapic_mask = Some (External (EF_external ioapic_mask (signature_of_type (Tcons tuint Tnil) tvoid cc_default)) (Tcons tuint Tnil) tvoid cc_default).
Lemma serial_intr_handler_preserves_all:
∀ d d´ b,
serial_intr_handler d = Some (d´, b) →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
functional inversion H; subst.
functional inversion H6; functional inversion H5; functional inversion H4; functional inversion H2; functional inversion H24; simpl in *; subst.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
rewrite replace_replace.
rewrite replace_preserves_Zlength.
unfold s_ioapic´.
unfold ioapic_trans_intr.
destruct (s (ioapic d)).
destruct (nth_error IoApicIrqs (Z.to_nat 4)).
destruct (nth_error IoApicEnables (Z.to_nat 4)).
destruct b.
intros;
simpl in ×.
eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
simpl; eauto.
eauto.
Qed.
Lemma serial_intr_diable_concrete_aux_preserves_all:
∀ n d d´,
serial_intr_disable_concrete_aux n d = Some d´ →
init d´ = init d ∧
ikern d´ = ikern d ∧
ihost d´ = ihost d ∧
intr_flag d´ = intr_flag d ∧
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
induction n.
simpl.
intros.
inv H; eauto.
simpl.
intros.
subdestruct.
inv Hdestruct0.
eapply IHn in H; eauto.
generalize (serial_intr_handler_preserves_all _ _ _ Hdestruct); intro.
destruct H0 as (? & ? & ? & ? & ?).
rewrite H0, H1, H2, H3, H4 in H.
assumption.
inv Hdestruct0.
inv H.
eauto.
Qed.
Lemma serial_intr_disable_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
serial_intr_disable_concrete_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_disable_concrete_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold serial_intr_disable_concrete_body.
functional inversion H1; subst.
esplit.
repeat vcgen.
unfold ioapic_mask_spec; simpl.
eapply serial_intr_diable_concrete_aux_preserves_all in H7.
destruct H7 as (? & ? & ? & ? & ?).
rewrite H, H7, H8, H4, H5, H6.
inv H0.
destruct (zle_lt 0 4 (Zlength (IoApicEnables (s (ioapic d0))))); try omega.
reflexivity.
Qed.
End Serial_Intr_Disable_Body.
Theorem serial_intr_disable_code_correct:
spec_le
(serial_intr_disable ↦ serial_intr_disable_spec_low)
(〚serial_intr_disable ↦ f_serial_intr_disable_concrete 〛L).
Proof.
fbigstep_pre L.
fbigstep
(serial_intr_disable_body_correct s
(Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_intr_disable_concrete) nil
(create_undef_temps (fn_temps f_serial_intr_disable_concrete))
)
) H0.
Qed.
End SERIAL_INTR_DISABLE.
End WithPrimitives.
End DHANDLEROPCODE.