Library mcertikos.proc.VVMCSInitCode
Require Import TacticsForTesting.
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 VMXIntroGenSpec.
Require Import VVMCSInitCSource.
Require Import VVMCSInit.
Require Import AbstractDataType.
Require Import ObjVMCS.
Require Import Constant.
Module VVMCSInitCode.
Section WithPrimitives.
Context `{real_params_ops : RealParamsOps}.
Context `{multi_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 tptrsize: sizeof (Tpointer tuint noattr) = 4.
Proof. reflexivity. Qed.
Definition vmx_size := VMX_Size´ × 4.
Section VMXREADZ.
Let L: compatlayer (cdata RData) :=
VMX_LOC ↦ v_VMX_LOC
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXReadZBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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 VMXIntroGenSpec.
Require Import VVMCSInitCSource.
Require Import VVMCSInit.
Require Import AbstractDataType.
Require Import ObjVMCS.
Require Import Constant.
Module VVMCSInitCode.
Section WithPrimitives.
Context `{real_params_ops : RealParamsOps}.
Context `{multi_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 tptrsize: sizeof (Tpointer tuint noattr) = 4.
Proof. reflexivity. Qed.
Definition vmx_size := VMX_Size´ × 4.
Section VMXREADZ.
Let L: compatlayer (cdata RData) :=
VMX_LOC ↦ v_VMX_LOC
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXReadZBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
VMX_LOC
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma VMX_readz_body_correct:
∀ m d env le vmx_idx vmx_val,
env = PTree.empty _ →
PTree.get _vmx_idx le = Some (Vint vmx_idx) →
0 ≤ (Int.unsigned vmx_idx) < VMX_Size´ →
Mem.load Mint32 ((m, d) : mem) bvmx_loc (vmx_size × (CPU_ID d) + (Int.unsigned vmx_idx) × 4) = Some (Vint vmx_val) →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_vmx_readz_body E0 le´ (m, d) (Out_return (Some (Vint vmx_val, tint))).
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
assert (tarraysize: (sizeof (Tarray tuint VMX_Size´ noattr)) = 152).
{ simpl; auto. }
assert (CPU_ID_range1: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H3; auto. }
assert (CPU_ID_range2: 0 ≤ CPU_ID d ≤ Int.max_unsigned).
{ inv H3; omega. }
assert (get_cpu_id: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
rewrite Int.unsigned_repr; try omega.
destruct H4 as (H4a & H4b); rewrite H4a, H4b; auto. }
assert (array_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) ≤ Int.max_unsigned) by omega.
assert (index1_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) × CPU_ID d ≤ Int.max_unsigned)
by (rewrite tarraysize; omega).
Opaque Z.mul Z.add sizeof.
unfold f_vmx_readz_body.
esplit; repeat vcgen.
rewrite tarraysize.
rewrite tintsize.
simpl.
unfold vmx_size in H2.
replace (0 + 152 × CPU_ID d + 4 × Int.unsigned vmx_idx) with (VMX_Size´ × 4 × CPU_ID d + Int.unsigned vmx_idx × 4);
try ring.
rewrite Int.unsigned_repr; try omega.
vcgen.
Qed.
End VMXReadZBody.
Theorem VMX_readz_code_correct:
spec_le (vmx_readz ↦ vmx_readz_spec_low) (〚vmx_readz ↦ f_vmx_readz 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m´; simpl in ×.
assert (match CPU_ID l with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos (y´ + (y´ + y´~0~0~0)~0)~0~0~0
| Z.neg y´ ⇒ Z.neg (y´ + (y´ + y´~0~0~0)~0)~0~0~0
end = vmx_size × (CPU_ID l)).
{ unfold vmx_size; simpl; auto. }
rewrite H3 in H1.
fbigstep (VMX_readz_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_readz)
(Vint i::nil)
(create_undef_temps (fn_temps f_vmx_readz)))) muval.
Qed.
End VMXREADZ.
Section VMXWRITEZ.
Let L: compatlayer (cdata RData) :=
VMX_LOC ↦ v_VMX_LOC
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXWriteZBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
VMX_LOC
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma VMX_writez_body_correct:
∀ m m´ d env le vmx_idx vmx_val,
env = PTree.empty _ →
PTree.get _vmx_idx le = Some (Vint vmx_idx) →
PTree.get _vmx_val le = Some (Vint vmx_val) →
0 ≤ (Int.unsigned vmx_idx) < VMX_Size´ →
Mem.store Mint32 ((m, d): mem) bvmx_loc (vmx_size × (CPU_ID d) + (Int.unsigned vmx_idx) × 4)
(Vint vmx_val) = Some (m´, d) →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_vmx_writez_body E0 le´ (m´, d) Out_normal.
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
assert (tarraysize: (sizeof (Tarray tuint VMX_Size´ noattr)) = 152).
{ simpl; auto. }
assert (CPU_ID_range1: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H4; auto. }
assert (CPU_ID_range2: 0 ≤ CPU_ID d ≤ Int.max_unsigned).
{ inv H4; omega. }
assert (get_cpu_id: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
rewrite Int.unsigned_repr; try omega.
destruct H5 as (H5a & H5b); rewrite H5a, H5b; auto. }
assert (array_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) ≤ Int.max_unsigned) by omega.
assert (index1_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) × CPU_ID d ≤ Int.max_unsigned)
by (rewrite tarraysize; omega).
Opaque Z.mul Z.add sizeof.
unfold f_vmx_writez_body.
esplit; repeat vcgen.
rewrite tarraysize.
rewrite tintsize.
unfold vmx_size in H3.
replace (0 + 152 × CPU_ID d + 4 × Int.unsigned vmx_idx) with (VMX_Size´ × 4 × CPU_ID d + Int.unsigned vmx_idx × 4);
try ring.
simpl; rewrite Int.unsigned_repr; try omega.
vcgen.
Qed.
End VMXWriteZBody.
Theorem VMX_writez_code_correct:
spec_le (vmx_writez ↦ vmx_writez_spec_low) (〚vmx_writez ↦ f_vmx_writez 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m´.
destruct m.
destruct H1; destruct H2.
simpl in *; subst.
assert (match CPU_ID l with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos (y´ + (y´ + y´~0~0~0)~0)~0~0~0
| Z.neg y´ ⇒ Z.neg (y´ + (y´ + y´~0~0~0)~0)~0~0~0
end = vmx_size × (CPU_ID l)).
{ unfold vmx_size; simpl; auto. }
rewrite H3 in H1.
fbigstep (VMX_writez_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_writez)
(Vint i::Vint v::nil)
(create_undef_temps (fn_temps f_vmx_writez)))) muval.
Qed.
End VMXWRITEZ.
Section VMXENTERPRE.
Let L: compatlayer (cdata RData) :=
VMX_LOC ↦ v_VMX_LOC ⊕
get_CPU_ID ↦ gensem get_CPU_ID_spec ⊕
vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXEnterPreBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
VMX_LOC
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
vmcs_writez
Variable bvmcs_writez: block.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez
= Some (External (EF_external vmcs_writez
(signature_of_type (Tcons tint (Tcons tint Tnil))
tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma VMX_enter_pre_body_correct:
∀ m d d´ env le val,
env = PTree.empty _ →
Mem.load Mint32 ((m, d): mem) bvmx_loc (vmx_size × (CPU_ID d) + VMX_G_RIP) = Some (Vint val) →
vmcs_writez_spec C_VMCS_GUEST_RIP (Int.unsigned val) d = Some d´ →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_vmx_enter_pre_body E0 le´ (m, d´) Out_normal.
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
assert (tarraysize: (sizeof (Tarray tuint VMX_Size´ noattr)) = 152).
{ simpl; auto. }
assert (CPU_ID_range1: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H2; auto. }
assert (CPU_ID_range2: 0 ≤ CPU_ID d ≤ Int.max_unsigned).
{ inv H2; omega. }
assert (get_cpu_id: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
rewrite Int.unsigned_repr; try omega.
destruct H3 as (H3a & H3b); rewrite H3a, H3b; auto. }
assert (array_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) ≤ Int.max_unsigned) by omega.
assert (index1_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) × CPU_ID d ≤ Int.max_unsigned)
by (rewrite tarraysize; omega).
Opaque Z.mul Z.add sizeof.
functional inversion H1.
unfold f_vmx_enter_pre_body; subst.
esplit; repeat vcgen.
unfold vmx_size in H0.
rewrite tarraysize.
rewrite tintsize.
replace (0 + 152 × CPU_ID d + 4 × 14) with (VMX_Size´ × 4 × CPU_ID d + 56); try ring.
simpl; rewrite Int.unsigned_repr; try omega.
vcgen.
repeat vcgen.
Qed.
End VMXEnterPreBody.
Theorem VMX_enter_pre_code_correct:
spec_le (vmx_enter_pre ↦ vmx_enter_pre_spec_low) (〚vmx_enter_pre ↦ f_vmx_enter_pre 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
simpl in ×.
assert (match CPU_ID labd with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos (y´ + (y´ + y´~0~0~0)~0)~0~0~0
| Z.neg y´ ⇒ Z.neg (y´ + (y´ + y´~0~0~0)~0)~0~0~0
end = vmx_size × (CPU_ID labd)).
{ unfold vmx_size; simpl; auto. }
rewrite H3 in H0.
fbigstep (VMX_enter_pre_body_correct s (Genv.globalenv p) makeglobalenv
b0 H b2
Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_enter_pre)
(nil)
(create_undef_temps (fn_temps f_vmx_enter_pre)))) muval.
Qed.
End VMXENTERPRE.
Section VMXEXITPOST.
Let L: compatlayer (cdata RData) :=
VMX_LOC ↦ v_VMX_LOC ⊕
get_CPU_ID ↦ gensem get_CPU_ID_spec ⊕
vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXExitPostBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
VMX_LOC
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 : Genv.find_funct_ptr ge bget_CPU_ID
= Some (External
(EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
vmcs_readz
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz
= Some (External (EF_external vmcs_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma VMX_exit_post_body_correct:
∀ m m´ m´´ m´´´ m´´´´ d env le val0 val1 val2,
env = PTree.empty _ →
vmcs_readz_spec C_VMCS_GUEST_RIP d = Some (Int.unsigned val0) →
vmcs_readz_spec C_VMCS_EXIT_REASON d = Some (Int.unsigned val1) →
vmcs_readz_spec C_VMCS_EXIT_QUALIFICATION d = Some (Int.unsigned val2) →
Mem.store Mint32 ((m, d): mem) bvmx_loc (vmx_size × (CPU_ID d) + VMX_G_RIP) (Vint val0) = Some (m´, d) →
Mem.store Mint32 ((m´, d): mem) bvmx_loc (vmx_size × (CPU_ID d) + VMX_EXIT_REASON)
(Vint val1) = Some (m´´, d) →
Mem.store Mint32 ((m´´, d): mem) bvmx_loc (vmx_size × (CPU_ID d) + VMX_EXIT_QUALIFICATION)
(Vint val2) = Some (m´´´, d) →
Mem.store Mint32 ((m´´´, d): mem) bvmx_loc (vmx_size × (CPU_ID d) + VMX_LAUNCHED) Vone = Some (m´´´´, d) →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_vmx_exit_post_body E0 le´ (m´´´´, d) Out_normal.
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
assert (tarraysize: (sizeof (Tarray tuint VMX_Size´ noattr)) = 152).
{ simpl; auto. }
assert (CPU_ID_range1: 0 ≤ CPU_ID d < TOTAL_CPU).
{ inv H7; auto. }
assert (CPU_ID_range2: 0 ≤ CPU_ID d ≤ Int.max_unsigned).
{ inv H7; omega. }
assert (get_cpu_id: get_CPU_ID_spec d = Some (Int.unsigned (Int.repr (CPU_ID d)))).
{ unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
rewrite Int.unsigned_repr; try omega.
destruct H8 as (H8a & H8b); rewrite H8a, H8b; auto. }
assert (array_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) ≤ Int.max_unsigned) by omega.
assert (index1_range: 0 ≤ sizeof (Tarray tuint VMX_Size´ noattr) × CPU_ID d ≤ Int.max_unsigned)
by (rewrite tarraysize; omega).
Opaque Z.mul Z.add sizeof.
functional inversion H0;
functional inversion H1;
functional inversion H2.
unfold f_vmx_exit_post_body; subst.
esplit; repeat vcgen.
-
unfold vmx_size in H3.
rewrite tarraysize.
rewrite tintsize.
replace (0 + 152 × CPU_ID d + 4 × 14) with (VMX_Size´ × 4 × CPU_ID d + 56); try ring.
simpl; rewrite Int.unsigned_repr; try omega.
vcgen.
-
unfold vmx_size in H4.
rewrite tarraysize.
rewrite tintsize.
replace (0 + 152 × CPU_ID d + 4 × 27) with (VMX_Size´ × 4 × CPU_ID d + 108); try ring.
simpl; rewrite Int.unsigned_repr; try omega.
vcgen.
-
unfold vmx_size in H5.
rewrite tarraysize.
rewrite tintsize.
replace (0 + 152 × CPU_ID d + 4 × 28) with (VMX_Size´ × 4 × CPU_ID d + 112); try ring.
simpl; rewrite Int.unsigned_repr; try omega.
vcgen.
-
unfold vmx_size in H6.
rewrite tarraysize.
rewrite tintsize.
replace (0 + 152 × CPU_ID d + 4 × 31) with (VMX_Size´ × 4 × CPU_ID d + 124); try ring.
simpl; rewrite Int.unsigned_repr; try omega.
vcgen.
Qed.
End VMXExitPostBody.
Theorem VMX_exit_post_code_correct:
spec_le (vmx_exit_post ↦ vmx_exit_post_spec_low) (〚vmx_exit_post ↦ f_vmx_exit_post 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
simpl in ×.
assert (match CPU_ID labd with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos (y´ + (y´ + y´~0~0~0)~0)~0~0~0
| Z.neg y´ ⇒ Z.neg (y´ + (y´ + y´~0~0~0)~0)~0~0~0
end = vmx_size × (CPU_ID labd)).
{ unfold vmx_size; simpl; auto. }
rewrite H8 in H3, H4, H5, H6.
fbigstep (VMX_exit_post_body_correct s (Genv.globalenv p) makeglobalenv
b0 H
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 m0 m1 m2 m3 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_exit_post)
(nil)
(create_undef_temps (fn_temps f_vmx_exit_post)))) muval.
Qed.
End VMXEXITPOST.
End WithPrimitives.
End VVMCSInitCode.