Library mcertikos.proc.VVMXIntroCode
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 IntelPrimSemantics.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import VMXInitGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VVMXIntroCSource.
Require Import VVMXIntro.
Require Import ObjVMCS.
Require Import ObjVMX.
Require Import ObjEPT.
Require Import XOmega.
Module VVMXINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
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.
Section VMXSetMmap.
Let L: compatlayer (cdata RData) :=
ept_add_mapping ↦ gensem ept_add_mapping_spec
⊕ ept_invalidate_mappings ↦ gensem ept_invalidate_mappings_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 VMXSetMmapBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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 IntelPrimSemantics.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import VMXInitGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VVMXIntroCSource.
Require Import VVMXIntro.
Require Import ObjVMCS.
Require Import ObjVMX.
Require Import ObjEPT.
Require Import XOmega.
Module VVMXINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
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.
Section VMXSetMmap.
Let L: compatlayer (cdata RData) :=
ept_add_mapping ↦ gensem ept_add_mapping_spec
⊕ ept_invalidate_mappings ↦ gensem ept_invalidate_mappings_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 VMXSetMmapBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
ept_add_mapping
Variable bept_add_mapping: block.
Hypothesis hept_add_mapping1 : Genv.find_symbol ge ept_add_mapping = Some bept_add_mapping.
Hypothesis hept_add_mapping2 : Genv.find_funct_ptr ge bept_add_mapping
= Some (External (EF_external ept_add_mapping
(signature_of_type (Tcons tint (Tcons tint
(Tcons tint Tnil)))
tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
ept_invalidate_mappings
Variable bept_invalidate_mappings: block.
Hypothesis hept_invalidate_mappings1 : Genv.find_symbol ge ept_invalidate_mappings = Some bept_invalidate_mappings.
Hypothesis hept_invalidate_mappings2 : Genv.find_funct_ptr ge bept_invalidate_mappings
= Some (External
(EF_external ept_invalidate_mappings
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma vmx_set_mmap_body_correct:
∀ m d d´ env le gpa hpa mem_type res,
env = PTree.empty _ →
PTree.get _gpa le = Some (Vint gpa) →
PTree.get _hpa le = Some (Vint hpa) →
PTree.get _mem_type le = Some (Vint mem_type) →
high_level_invariant d →
vmx_set_mmap_spec (Int.unsigned gpa) (Int.unsigned hpa) (Int.unsigned mem_type) d = Some (d´, Int.unsigned res) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_mmap_body E0 le´ (m, d´) (Out_return (Some (Vint res, tint))).
Proof.
generalize max_unsigned_val; intro muval.
generalize max_unsigned64_val; intro mu64val.
intros.
unfold vmx_set_mmap_body.
functional inversion H4; subst.
{ esplit.
repeat vcgenfull. }
{ esplit.
repeat vcgenfull. }
Qed.
End VMXSetMmapBody.
Theorem vmx_set_mmap_code_correct:
spec_le (vmx_set_mmap ↦ vmx_set_mmap_spec_low) (〚vmx_set_mmap ↦ f_vmx_set_mmap 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_set_mmap_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_vmx_set_mmap)
(Vint gpa::Vint hpa::Vint mem_type::nil)
(create_undef_temps (fn_temps f_vmx_set_mmap)))) H0.
Qed.
End VMXSetMmap.
Section VMXGetExitQualification.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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 VMXGetExitQualificationBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_qualification_body_correct:
∀ m d env le val,
env = PTree.empty _ →
high_level_invariant d →
vmx_get_exit_qualification_spec d = Some (Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_qualification_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_exit_qualification_body.
functional inversion H1; subst.
esplit.
repeat vcgenfull.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega.
rewrite H2.
reflexivity.
Qed.
End VMXGetExitQualificationBody.
Theorem vmx_get_exit_qualification_code_correct:
spec_le (vmx_get_exit_qualification ↦ vmx_get_exit_qualification_spec_low) (〚vmx_get_exit_qualification ↦ f_vmx_get_exit_qualification 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_exit_qualification_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_exit_qualification)
nil
(create_undef_temps
(fn_temps f_vmx_get_exit_qualification)))) H0.
Qed.
End VMXGetExitQualification.
Section VMXGetExitIOPort.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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 VMXGetExitIOPortBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_io_port_body_correct:
∀ m d env le val,
env = PTree.empty _ →
high_level_invariant d →
vmx_get_exit_io_port_spec d = Some (Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_io_port_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_exit_io_port_body.
functional inversion H1; subst.
esplit.
repeat vcgenfull.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
+ reflexivity.
+ repeat discharge_unsigned_range.
- simpl.
unfold sem_div.
unfold sem_binarith.
simpl.
discharge_cmp.
+ rewrite H2.
rewrite Int.repr_unsigned.
reflexivity.
+ repeat discharge_unsigned_range.
Qed.
End VMXGetExitIOPortBody.
Theorem vmx_get_exit_io_port_code_correct:
spec_le (vmx_get_exit_io_port ↦ vmx_get_exit_io_port_spec_low) (〚vmx_get_exit_io_port ↦ f_vmx_get_exit_io_port 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_exit_io_port_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_exit_io_port)
nil
(create_undef_temps
(fn_temps f_vmx_get_exit_io_port)))) H0.
Qed.
End VMXGetExitIOPort.
Section VMXGetExitIOStr.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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 VMXGetExitIOStrBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_io_str_body_correct:
∀ m d env le val,
env = PTree.empty _ →
high_level_invariant d →
vmx_get_exit_io_str_spec d = Some (Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_io_str_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_exit_io_str_body.
functional inversion H1; subst.
generalize (Int.unsigned_range v); intro vrange;
repeat autounfold in vrange; unfold two_power_nat, shift_nat in vrange; simpl in vrange.
esplit.
repeat vcgenfull.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega; try auto.
rewrite Int.unsigned_repr; try omega; try auto.
omega.
- rewrite H2.
rewrite Int.repr_unsigned.
reflexivity.
- rewrite Z.shiftr_div_pow2.
+ change (2 ^ 4) with 16.
xomega.
+ omega.
- rewrite Z.shiftr_div_pow2.
+ change (2 ^ 4) with 16.
xomega.
+ omega.
- omega.
- omega.
Qed.
End VMXGetExitIOStrBody.
Theorem vmx_get_exit_io_str_code_correct:
spec_le (vmx_get_exit_io_str ↦ vmx_get_exit_io_str_spec_low) (〚vmx_get_exit_io_str ↦ f_vmx_get_exit_io_str 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_exit_io_str_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_exit_io_str)
nil
(create_undef_temps
(fn_temps f_vmx_get_exit_io_str)))) H0.
Qed.
End VMXGetExitIOStr.
Section VMXGetExitIORep.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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 VMXGetExitIORepBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_exit_io_rep_body_correct:
∀ m d env le val,
env = PTree.empty _ →
high_level_invariant d →
vmx_get_exit_io_rep_spec d = Some (Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_exit_io_rep_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_exit_io_rep_body.
functional inversion H1; subst.
generalize (Int.unsigned_range v); intro vrange; repeat autounfold in vrange;
unfold two_power_nat, shift_nat in vrange; simpl in vrange.
esplit.
repeat vcgenfull.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try auto; try omega.
rewrite Int.unsigned_repr; try auto; try omega.
- rewrite H2.
rewrite Int.repr_unsigned; try omega.
reflexivity.
- rewrite Z.shiftr_div_pow2; try omega.
change (2 ^ 5) with 32.
xomega.
- rewrite Z.shiftr_div_pow2; try omega.
change (2 ^ 5) with 32.
xomega.
- omega.
- omega.
Qed.
End VMXGetExitIORepBody.
Theorem vmx_get_exit_io_rep_code_correct:
spec_le (vmx_get_exit_io_rep ↦ vmx_get_exit_io_rep_spec_low) (〚vmx_get_exit_io_rep ↦ f_vmx_get_exit_io_rep 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_exit_io_rep_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_exit_io_rep)
nil
(create_undef_temps
(fn_temps f_vmx_get_exit_io_rep)))) H0.
Qed.
End VMXGetExitIORep.
Section VMXGetIOWrite.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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 VMXGetIOWriteBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_io_write_body_correct:
∀ m d env le val,
env = PTree.empty _ →
high_level_invariant d →
vmx_get_io_write_spec d = Some (Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_io_write_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_io_write_body.
functional inversion H1; subst.
{
generalize (Int.unsigned_range v); intro vrange; repeat autounfold in vrange;
unfold two_power_nat, shift_nat in vrange; simpl in vrange.
esplit.
repeat vcgen.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega.
rewrite Int.unsigned_repr; try auto; try omega.
- repeat vcgenfull.
+ rewrite Z.shiftr_div_pow2; try omega.
change (2 ^ 3) with 8.
xomega.
+ rewrite Z.shiftr_div_pow2; try omega.
change (2 ^ 3) with 8.
xomega.
- omega.
- omega.
- rewrite H2.
rewrite Int.repr_unsigned.
repeat vcgen.
- ptreesolve.
}
{
generalize (Int.unsigned_range v); intro vrange; repeat autounfold in vrange;
unfold two_power_nat, shift_nat in vrange; simpl in vrange.
unfold qdir in ×.
assert(0 ≤ Z.shiftr (Int.unsigned v) 3 ≤ Int.max_unsigned).
{ rewrite Z.shiftr_div_pow2.
change (2 ^ 3) with 8.
xomega.
omega. }
esplit.
repeat vcgen.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega.
rewrite Int.unsigned_repr; try auto; try omega.
- discharge_cmp.
- omega.
- omega.
- rewrite H2.
rewrite Int.repr_unsigned.
repeat vcgen.
- ptreesolve.
}
Qed.
End VMXGetIOWriteBody.
Theorem vmx_get_io_write_code_correct:
spec_le (vmx_get_io_write ↦ vmx_get_io_write_spec_low) (〚vmx_get_io_write ↦ f_vmx_get_io_write 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_io_write_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_io_write)
nil
(create_undef_temps (fn_temps f_vmx_get_io_write)))) H0.
Qed.
End VMXGetIOWrite.
Section VMXGetIOWidth.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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 VMXGetIOWidthBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_io_width_body_correct:
∀ m d env le val,
env = PTree.empty _ →
high_level_invariant d →
vmx_get_io_width_spec d = Some (Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_io_width_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_io_width_body.
functional inversion H1; subst.
{
generalize (Int.unsigned_range v); intro vrange; repeat autounfold in vrange;
unfold two_power_nat, shift_nat in vrange; simpl in vrange.
esplit.
repeat vcgen.
unfold vmx_readz_spec.
- rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega.
rewrite Int.unsigned_repr; try auto; try omega.
- discharge_cmp.
- discharge_unsigned_range.
- omega.
- omega.
- repeat vcgen.
- rewrite H2.
rewrite Int.repr_unsigned.
ptreesolve.
- omega.
- omega.
}
{
generalize (Int.unsigned_range v); intro vrange; repeat autounfold in vrange;
unfold two_power_nat, shift_nat in vrange; simpl in vrange.
esplit.
repeat vcgen.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega.
rewrite Int.unsigned_repr; try auto; try omega.
- discharge_cmp.
- discharge_unsigned_range.
- omega.
- repeat vcgen.
- repeat vcgen.
- rewrite H2.
rewrite Int.repr_unsigned.
ptreesolve.
- omega.
- omega.
}
{
generalize (Int.unsigned_range v); intro vrange; repeat autounfold in vrange;
unfold two_power_nat, shift_nat in vrange; simpl in vrange.
unfold qsize in ×.
esplit.
repeat vcgen.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, H6, H7, zle_lt_true; try omega.
rewrite Int.unsigned_repr; try auto; try omega.
- discharge_cmp.
- discharge_unsigned_range.
- omega.
- omega.
- repeat vcgen.
- rewrite H2.
rewrite Int.repr_unsigned.
ptreesolve.
- omega.
- omega.
}
Qed.
End VMXGetIOWidthBody.
Theorem vmx_get_io_width_code_correct:
spec_le (vmx_get_io_width ↦ vmx_get_io_width_spec_low) (〚vmx_get_io_width ↦ f_vmx_get_io_width 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_io_width_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_io_width)
nil
(create_undef_temps
(fn_temps f_vmx_get_io_width)))) H0.
Qed.
End VMXGetIOWidth.
Section VMXGetNextEIP.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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.
Local Open Scope Z_scope.
Section VMXGetNextEIPBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_next_eip_body_correct:
∀ m d env le val,
env = PTree.empty _ →
high_level_invariant d →
vmx_get_next_eip_spec d = Some (Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_next_eip_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_next_eip_body.
functional inversion H1; subst.
generalize (Int.unsigned_range v1); intro v1range; repeat autounfold in v1range;
unfold two_power_nat, shift_nat in v1range; simpl in v1range.
generalize (Int.unsigned_range v2); intro v2range; repeat autounfold in v2range;
unfold two_power_nat, shift_nat in v2range; simpl in v2range.
esplit.
repeat vcgen.
- unfold vmx_readz_spec.
rewrite H3, H4, H5, zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
rewrite H8.
reflexivity.
- unfold vmcs_readz_spec.
rewrite H3, H4, H5.
rewrite zle_lt_true; try omega.
rewrite H7.
simpl.
rewrite H9.
reflexivity.
- simpl.
unfold sem_add; simpl.
unfold sem_binarith; simpl.
repeat vcgen.
rewrite H2.
rewrite Int.repr_unsigned; reflexivity.
Qed.
End VMXGetNextEIPBody.
Theorem vmx_get_next_eip_code_correct:
spec_le (vmx_get_next_eip ↦ vmx_get_next_eip_spec_low) (〚vmx_get_next_eip ↦ f_vmx_get_next_eip 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_next_eip_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_next_eip)
nil
(create_undef_temps
(fn_temps f_vmx_get_next_eip)))) H0.
Qed.
End VMXGetNextEIP.
Section VMXGetReg.
Let L: compatlayer (cdata RData) := vmx_readz ↦ gensem vmx_readz_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.
Local Open Scope Z_scope.
Section VMXGetRegBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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).
vmx_readz
Variable bvmx_readz: block.
Hypothesis hvmx_readz1 : Genv.find_symbol ge vmx_readz = Some bvmx_readz.
Hypothesis hvmx_readz2 : Genv.find_funct_ptr ge bvmx_readz
= Some (External (EF_external vmx_readz
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemma vmx_get_reg_body_correct:
∀ m d env le reg result,
env = PTree.empty _ →
PTree.get _reg le = Some (Vint reg) →
high_level_invariant d →
vmx_get_reg_spec (Int.unsigned reg) d = Some (Int.unsigned result) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_get_reg_body E0 le´ (m, d) (Out_return (Some (Vint result, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_get_reg_body.
functional inversion H2; subst.
{ functional inversion H8; subst;
esplit;
repeat vcgen;
unfold vmx_readz_spec;
rewrite H4, H5, H6, zle_lt_true, zle_lt_true, H9, H3;
try reflexivity; try omega. }
{ functional inversion H8; subst;
esplit;
repeat vcgen;
unfold vmcs_readz_spec;
rewrite H4, H5, H6, zle_lt_true, H9; simpl; try rewrite H10, H3;
try reflexivity; try omega. }
Qed.
End VMXGetRegBody.
Theorem vmx_get_reg_code_correct:
spec_le (vmx_get_reg ↦ vmx_get_reg_spec_low) (〚vmx_get_reg ↦ f_vmx_get_reg 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_get_reg_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_get_reg)
(Vint reg::nil)
(create_undef_temps (fn_temps f_vmx_get_reg)))) H0.
Qed.
End VMXGetReg.
Section VMXSetReg.
Let L: compatlayer (cdata RData) := vmx_writez ↦ gensem vmx_writez_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.
Local Open Scope Z_scope.
Section VMXSetRegBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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).
vmx_writez
Variable bvmx_writez: block.
Hypothesis hvmx_writez1 : Genv.find_symbol ge vmx_writez = Some bvmx_writez.
Hypothesis hvmx_writez2 : Genv.find_funct_ptr ge bvmx_writez
= Some (External (EF_external vmx_writez
(signature_of_type (Tcons tint (Tcons tint Tnil))
tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma vmx_set_reg_body_correct:
∀ m d d´ env le reg val,
env = PTree.empty _ →
PTree.get _reg le = Some (Vint reg) →
PTree.get _val le = Some (Vint val) →
high_level_invariant d →
vmx_set_reg_spec (Int.unsigned reg) (Int.unsigned val) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_reg_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_set_reg_body.
functional inversion H3; subst.
{ functional inversion H9; subst;
esplit;
repeat vcgen;
unfold vmx_writez_spec;
rewrite H5, H6, H7, zle_lt_true, zle_lt_true;
try rewrite Int.repr_unsigned;
try reflexivity; try omega. }
{ functional inversion H9; subst;
esplit;
repeat vcgen;
unfold vmcs_writez_spec;
rewrite H5, H6, H7, zle_lt_true, H10; simpl;
try rewrite Int.repr_unsigned;
try reflexivity; try omega. }
Qed.
End VMXSetRegBody.
Theorem vmx_set_reg_code_correct:
spec_le (vmx_set_reg ↦ vmx_set_reg_spec_low) (〚vmx_set_reg ↦ f_vmx_set_reg 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_set_reg_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp b0 Hb0fs Hb0fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_set_reg)
(Vint reg::Vint v::nil)
(create_undef_temps (fn_temps f_vmx_set_reg)))) H0.
Qed.
End VMXSetReg.
Section VMXInit.
Let L: compatlayer (cdata RData) := vmx_writez ↦ gensem vmx_writez_spec
⊕ vmcs_set_defaults ↦ vmcs_set_defaults_compatsem vmcs_set_defaults_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 VMXInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_writez
Variable bvmx_writez: block.
Hypothesis hvmx_writez1 : Genv.find_symbol ge vmx_writez = Some bvmx_writez.
Hypothesis hvmx_writez2 : Genv.find_funct_ptr ge bvmx_writez = Some (External (EF_external vmx_writez (signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default)) (Tcons tint (Tcons tint Tnil)) tvoid cc_default).
vmcs_set_defaults
Variable bvmcs_set_defaults: block.
Hypothesis hvmcs_set_defaults1 : Genv.find_symbol ge vmcs_set_defaults = Some bvmcs_set_defaults.
Hypothesis hvmcs_set_defaults2 : Genv.find_funct_ptr ge bvmcs_set_defaults
= Some (External (EF_external vmcs_set_defaults
(signature_of_type Tnil tvoid cc_default))
Tnil tvoid cc_default).
Lemma vmx_init_body_correct:
∀ m d d´ env le pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b,
env = PTree.empty _ →
high_level_invariant d →
Genv.find_symbol ge EPT_LOC = Some pml4ept_b →
Genv.find_symbol ge STACK_LOC = Some stack_b →
True →
Genv.find_symbol ge idt_LOC = Some idt_b →
Genv.find_symbol ge msr_bitmap_LOC = Some msr_bitmap_b →
Genv.find_symbol ge io_bitmap_LOC = Some io_bitmap_b →
Genv.find_symbol ge vmx_return_from_guest = Some host_rip_b →
vmx_init_spec pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_init_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold vmx_init_body.
assert (vmx_double_update: ∀ d vmx1 vmx2, d {vmx: vmx1} {vmx: vmx2} = d {vmx : vmx2}).
{ unfold update_vmx; simpl; auto. }
functional inversion H8; subst.
esplit.
Opaque Calculate_EPDPTE_at_i Calculate_VMX_at_i.
repeat vcgen.
- unfold vmcs_set_defaults_spec.
rewrite H10, H11, H12, H13, H14, H15, H16, H17.
reflexivity.
- erewrite <- stencil_matches_symbols; eauto.
- erewrite <- stencil_matches_symbols; eauto.
- erewrite <- stencil_matches_symbols; eauto.
- erewrite <- stencil_matches_symbols; eauto.
- erewrite <- stencil_matches_symbols; eauto.
- erewrite <- stencil_matches_symbols; eauto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite zle_lt_true; auto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite vmx_double_update.
rewrite ZMap.set2.
rewrite zle_lt_true; auto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite vmx_double_update.
rewrite ZMap.set2.
rewrite zle_lt_true; auto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite vmx_double_update.
rewrite ZMap.set2.
rewrite zle_lt_true; auto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite vmx_double_update.
rewrite ZMap.set2.
rewrite zle_lt_true; auto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite vmx_double_update.
rewrite ZMap.set2.
rewrite zle_lt_true; auto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite vmx_double_update.
rewrite ZMap.set2.
rewrite zle_lt_true; auto.
- unfold vmx_writez_spec; simpl.
rewrite H11, H12, H14.
rewrite vmx_double_update.
rewrite ZMap.set2.
rewrite zle_lt_true; auto.
unfold ret; simpl.
f_equal.
Transparent Calculate_EPDPTE_at_i Calculate_VMX_at_i.
f_equal.
unfold Calculate_VMX_at_i.
simpl.
repeat f_equal.
rewrite ZMap.gss.
repeat f_equal.
rewrite ZMap.gss.
repeat f_equal.
rewrite ZMap.gss.
repeat f_equal.
rewrite ZMap.gss.
repeat f_equal.
rewrite ZMap.gss.
repeat f_equal.
rewrite ZMap.gss.
repeat f_equal.
rewrite ZMap.gss.
reflexivity.
Qed.
End VMXInitBody.
Theorem vmx_init_code_correct:
spec_le (vmx_init ↦ vmx_init_spec_low) (〚vmx_init ↦ f_vmx_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (vmx_init_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_vmx_init)
nil
(create_undef_temps (fn_temps f_vmx_init)))) H7.
Qed.
End VMXInit.
End WithPrimitives.
End VVMXINTROCODE.