Library mcertikos.virt.intel.VEPTInitCode
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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 VEPTInitCSource.
Require Import VMCSIntroGenSpec.
Module VEPTINITCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
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 VMCSGETREVID.
Let L: compatlayer (cdata RData) := VMCS_LOC ↦ v_vmcs.
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 VMCSGetRevidBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
Lemma vmcs_get_revid_body_correct:
∀ m d env le v,
env = PTree.empty _ →
Mem.loadv Mint32 (m, d) (Vptr bvmcs_loc Int.zero) = Some (Vint v) →
exec_stmt ge env le ((m, d): mem) vmcs_get_revid_body E0 le (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
intros m d env le z Henv Hmem. subst.
unfold vmcs_get_revid_body.
repeat vcgen.
Qed.
End VMCSGetRevidBody.
Theorem vmcs_get_revid_code_correct:
spec_le
(vmcs_get_revid ↦ vmcs_get_revid_spec_low)
(〚vmcs_get_revid ↦ f_vmcs_get_revid 〛L).
Proof.
fbigstep_pre L.
fbigstep
(vmcs_get_revid_body_correct
(Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_get_revid) nil
(create_undef_temps (fn_temps f_vmcs_get_revid))
)
) m´.
Qed.
End VMCSGETREVID.
Section VMCSSETREVID.
Let L: compatlayer (cdata RData) := VMCS_LOC ↦ v_vmcs.
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 VMCSSetRevidBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
Lemma vmcs_set_revid_body_correct:
∀ m m´ d env le revid,
env = PTree.empty _ →
PTree.get tid le = Some (Vint revid)->
Mem.store Mint32 (m, d) bvmcs_loc 0 (Vint revid) = Some (m´, d) →
exec_stmt ge env le ((m, d): mem) vmcs_set_revid_body E0 le (m´, d)
Out_normal.
Proof.
intros. subst.
unfold vmcs_set_revid_body.
repeat vcgen.
Qed.
End VMCSSetRevidBody.
Theorem vmcs_set_revid_code_correct:
spec_le
(vmcs_set_revid ↦ vmcs_set_revid_spec_low)
(〚vmcs_set_revid ↦ f_vmcs_set_revid 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m. destruct m´.
fbigstep
(vmcs_set_revid_body_correct
(Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_set_revid) (Vint v::nil)
(create_undef_temps (fn_temps f_vmcs_set_revid))
)
) H0.
Qed.
End VMCSSETREVID.
Section VMCSGETABRTID.
Let L: compatlayer (cdata RData) := VMCS_LOC ↦ v_vmcs.
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 VMCSGetAbrtIdBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
Lemma vmcs_get_abrtid_body_correct:
∀ m d env le v,
env = PTree.empty _ →
Mem.loadv Mint32 (m, d) (Vptr bvmcs_loc (Int.repr 4)) = Some (Vint v) →
exec_stmt ge env le ((m, d): mem) vmcs_get_abrtid_body E0 le (m, d)
(Out_return (Some (Vint v, tint))).
Proof.
intros m d env le z Henv Hmem. subst.
unfold vmcs_get_abrtid_body.
repeat vcgen.
Qed.
End VMCSGetAbrtIdBody.
Theorem vmcs_get_abrtid_code_correct:
spec_le
(vmcs_get_abrtid ↦ vmcs_get_abrtid_spec_low)
(〚vmcs_get_abrtid ↦ f_vmcs_get_abrtid 〛L).
Proof.
fbigstep_pre L.
fbigstep
(vmcs_get_abrtid_body_correct
(Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_get_abrtid) nil
(create_undef_temps (fn_temps f_vmcs_get_abrtid))
)
) m´.
Qed.
End VMCSGETABRTID.
Section VMCSSETABRTID.
Let L: compatlayer (cdata RData) := VMCS_LOC ↦ v_vmcs.
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 VMCSSetAbrtidBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bvmcs_loc: block).
Hypothesis hvmcs_loc : Genv.find_symbol ge VMCS_LOC = Some bvmcs_loc.
Lemma vmcs_set_abrtid_body_correct:
∀ m m´ d env le abrtid,
env = PTree.empty _ →
PTree.get tcode le = Some (Vint abrtid)->
Mem.store Mint32 (m, d) bvmcs_loc 4 (Vint abrtid) = Some (m´, d) →
exec_stmt ge env le ((m, d): mem) vmcs_set_abrtid_body E0 le (m´, d)
Out_normal.
Proof.
intros. subst.
unfold vmcs_set_abrtid_body.
repeat vcgen.
Qed.
End VMCSSetAbrtidBody.
Theorem vmcs_set_abrtid_code_correct:
spec_le
(vmcs_set_abrtid ↦ vmcs_set_abrtid_spec_low)
(〚vmcs_set_abrtid ↦ f_vmcs_set_abrtid 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m. destruct m´.
fbigstep
(vmcs_set_abrtid_body_correct
(Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmcs_set_abrtid) (Vint v::nil)
(create_undef_temps (fn_temps f_vmcs_set_abrtid))
)
) H0.
Qed.
End VMCSSETABRTID.
End WithPrimitives.
End VEPTINITCODE.