Library mcertikos.virt.intel.VEPTIntroCodeEPTInit
*********************************************************************** * * * 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 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 EPTOpGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VEPTIntroCSource.
Require Import ObjProc.
Require Import ObjEPT.
Require Import CalRealIntelModule.
Require Import XOmega.
Require Import ObjSyncIPC.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Module EPTINTROCODEEPTINIT.
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 EPT_Init.
Let L: compatlayer (cdata RData) := set_EPDPTE ↦ gensem setEPDPTE_spec
⊕ set_EPDTE ↦ gensem setEPDTE_spec
⊕ set_EPML4E ↦ gensem setEPML4_spec
⊕ proc_init ↦ gensem proc_init_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 EPTInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
proc_init
Variable bproc_init: block.
Hypothesis hproc_init1 : Genv.find_symbol ge proc_init = Some bproc_init.
Hypothesis hproc_init2 : Genv.find_funct_ptr ge bproc_init = Some (External (EF_external proc_init (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
set_EPML4E
Variable bset_EPML4E: block.
Hypothesis hset_EPML4E1 : Genv.find_symbol ge set_EPML4E = Some bset_EPML4E.
Hypothesis hset_EPML4E2 : Genv.find_funct_ptr ge bset_EPML4E = Some (External (EF_external set_EPML4E (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
set_EPDPTE
Variable bset_EPDPTE: block.
Hypothesis hset_EPDPTE1 : Genv.find_symbol ge set_EPDPTE = Some bset_EPDPTE.
Hypothesis hset_EPDPTE2 : Genv.find_funct_ptr ge bset_EPDPTE = Some (External (EF_external set_EPDPTE (signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default)) (Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
set_EPDTE
Variable bset_EPDTE: block.
Hypothesis hset_EPDTE1 : Genv.find_symbol ge set_EPDTE = Some bset_EPDTE.
Hypothesis hset_EPDTE2 : Genv.find_funct_ptr ge bset_EPDTE = Some (External (EF_external set_EPDTE (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).
Definition ept_init_epdte_mk_rdata (i j: Z) (adt: RData) := adt {ept: Calculate_EPDTE i (Z.to_nat j) (ept adt)}.
Section ept_init_epdte_loop_proof.
Variable minit: memb.
Variable adt: RData.
Variable i: Z.
Hypothesis pg : pg adt = true.
Hypothesis ihost: ihost adt = true.
Hypothesis ikern: ikern adt = true.
Hypothesis irange: 0 ≤ i < 4.
Hypothesis eptvalid: ∃ epdpt epdt, ZMap.get 0 (ept adt) = EPML4EValid epdpt ∧ ZMap.get i epdpt = EPDPTEValid epdt.
Definition ept_init_epdte_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get _j le = Some (Vint Int.zero) ∧
PTree.get _i le = Some (Vint (Int.repr i)) ∧
m = (minit, adt).
Definition ept_init_epdte_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, ept_init_epdte_mk_rdata i 511 adt) ∧ PTree.get _i le = Some (Vint (Int.repr i)).
Lemma ept_init_epdte_loop_correct_aux : LoopProofSimpleWhile.t ept_init_inner_while_condition ept_init_inner_while_body ge (PTree.empty _) (ept_init_epdte_loop_body_P) (ept_init_epdte_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ j,
PTree.get _i le = Some (Vint (Int.repr i)) ∧
PTree.get _j le = Some (Vint j) ∧
0 ≤ Int.unsigned j ≤ 512 ∧
(Int.unsigned j = 0 ∧ m = (minit, adt) ∨ 0 < Int.unsigned j ∧ m = (minit, ept_init_epdte_mk_rdata i (Int.unsigned j - 1) adt) ∧ (∃ epdpt epdt, ZMap.get 0 (ept (ept_init_epdte_mk_rdata i (Int.unsigned j - 1) adt)) = EPML4EValid epdpt ∧ ZMap.get i epdpt = EPDPTEValid epdt)) ∧
w = 512 - Int.unsigned j
)
.
apply Zwf_well_founded.
intros.
unfold ept_init_epdte_loop_body_P in H.
destruct H as [tjle tmpH].
destruct tmpH as [tile msubst].
subst.
esplit. esplit.
repeat vcgen.
intros.
unfold ept_init_inner_while_condition.
unfold ept_init_inner_while_body.
destruct H as [j tmpH].
destruct tmpH as [tile tmpH].
destruct tmpH as [tjle tmpH].
destruct tmpH as [jrange tmpH].
destruct tmpH as [jcase nval].
subst.
destruct jrange as [jlow jhigh].
apply Zle_lt_or_eq in jhigh.
destruct m.
Caseeq jhigh.
intro jhigh.
assert(jbound: 0 ≤ Int.unsigned j ≤ EPT_PDIR_INDEX Int.max_unsigned).
{
unfold EPT_PDIR_INDEX.
rewrite muval.
xomega.
}
assert(ibound: 0 ≤ i ≤ EPT_PDPT_INDEX Int.max_unsigned).
{
unfold EPT_PDPT_INDEX.
xomega.
}
assert(zerobound: 0 ≤ 0 ≤ EPT_PML4_INDEX Int.max_unsigned).
{
unfold EPT_PML4_INDEX.
xomega.
}
Caseeq jcase.
intro tmpH; destruct tmpH as [jval msubst].
injection msubst; intros; subst.
destruct eptvalid as [epdpt eptvalid´].
destruct eptvalid´ as [epdt eptvalid´].
destruct eptvalid´ as [epdptvalid epdtvalid].
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold setEPDTE_spec.
rewrite pg, ihost, ikern, epdptvalid, epdtvalid.
repeat rewrite zle_le_true; auto.
∃ (512 - Int.unsigned j - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
unfold ept_init_epdte_mk_rdata.
rewrite jval; simpl.
unfold Calculate_EPDTE_at_j.
rewrite epdptvalid, epdtvalid.
split.
reflexivity.
rewrite ZMap.gss.
esplit. esplit.
split.
reflexivity.
rewrite ZMap.gss.
reflexivity.
intro tmpH.
destruct tmpH as [jgt0 tmpH].
destruct tmpH as [mval tmpH].
destruct tmpH as [epdpt tmpH].
destruct tmpH as [epdt tmpH].
destruct tmpH as [epdptvalid epdtvalid].
injection mval; intros; subst.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold setEPDTE_spec.
simpl in ×.
rewrite pg, ihost, ikern, epdptvalid, epdtvalid.
repeat rewrite zle_le_true; auto.
∃ (512 - Int.unsigned j - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
unfold ept_init_epdte_mk_rdata.
replace (Int.unsigned j + 1 - 1) with (Int.unsigned j - 1 + 1) by omega.
change (Int.unsigned j - 1 + 1) with (Z.succ (Int.unsigned j - 1)).
rewrite Z2Nat.inj_succ with (n:=(Int.unsigned j - 1)).
Opaque Z.to_nat Z.of_nat.
simpl.
rewrite Nat2Z.inj_succ.
rewrite Z2Nat.id.
unfold Z.succ.
replace (Int.unsigned j - 1 + 1) with (Int.unsigned j) by omega.
unfold Calculate_EPDTE_at_j.
simpl in ×.
rewrite epdptvalid, epdtvalid.
split.
reflexivity.
rewrite ZMap.gss.
esplit. esplit.
split.
reflexivity.
rewrite ZMap.gss.
reflexivity.
omega.
omega.
intro jval.
subst.
esplit. esplit.
repeat vcgen.
unfold ept_init_epdte_loop_body_Q.
Caseeq jcase.
intro tmpH; destruct tmpH.
rewrite jval in H0.
discriminate H0.
intro tmpH; destruct tmpH.
rewrite jval in H1.
destruct H1.
injection H1; intros; subst.
split; eauto.
Qed.
End ept_init_epdte_loop_proof.
Lemma ept_init_epdte_loop_correct: ∀ m d d´ le i,
pg d = true →
ihost d = true →
ikern d = true →
0 ≤ i < 4 →
(∃ epdpt epdt, ZMap.get 0 (ept d) = EPML4EValid epdpt ∧ ZMap.get i epdpt = EPDPTEValid epdt) →
PTree.get _j le = Some (Vint Int.zero) →
PTree.get _i le = Some (Vint (Int.repr i)) →
d´ = ept_init_epdte_mk_rdata i 511 d →
∃ le´,
(exec_stmt ge (PTree.empty _) le ((m, d): mem) (Swhile ept_init_inner_while_condition ept_init_inner_while_body) E0 le´ (m, d´) Out_normal ∧ PTree.get _i le´ = Some (Vint (Int.repr i))).
Proof.
intros.
generalize (ept_init_epdte_loop_correct_aux m d i H H0 H1 H2 H3).
unfold ept_init_epdte_loop_body_P.
unfold ept_init_epdte_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp tmppre].
destruct tmppre as [m´´val tpile´].
∃ le´.
subst.
repeat vcgen.
repeat vcgen.
Qed.
Definition ept_init_epdpte_mk_rdata (i: Z) (adt: RData) := adt {ept: Calculate_EPDPTE (Z.to_nat i) (ept adt)}.
Section ept_init_epdpte_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis pg : pg adt = true.
Hypothesis ihost: ihost adt = true.
Hypothesis ikern: ikern adt = true.
Hypothesis eptvalid: (∃ epdpt, ZMap.get 0 (ept adt) = EPML4EValid epdpt).
Definition ept_init_epdpte_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get _i le = Some (Vint Int.zero) ∧
m = (minit, adt).
Definition ept_init_epdpte_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, ept_init_epdpte_mk_rdata 3 adt).
Lemma ept_init_epdpte_loop_correct_aux : LoopProofSimpleWhile.t ept_init_outter_while_condition ept_init_outter_while_body ge (PTree.empty _) (ept_init_epdpte_loop_body_P) (ept_init_epdpte_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get _i le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ 4 ∧
(∃ epdpt, ZMap.get 0 (ept (snd m)) = EPML4EValid epdpt) ∧
(Int.unsigned i = 0 ∧ m = (minit, adt) ∨ 0 < Int.unsigned i ∧ m = (minit, ept_init_epdpte_mk_rdata (Int.unsigned i - 1) adt)) ∧
w = 4 - Int.unsigned i
)
.
apply Zwf_well_founded.
intros.
unfold ept_init_epdpte_loop_body_P in H.
destruct H as [tile msubst].
subst.
esplit. esplit.
repeat vcgen.
intros.
unfold ept_init_outter_while_condition.
unfold ept_init_outter_while_body.
destruct H as [i tmpH].
destruct tmpH as [tile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [epdptvalid tmpH].
destruct tmpH as [icase nval].
subst.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct m.
simpl in epdptvalid.
destruct epdptvalid as [epdpt epdptvalid].
Caseeq ihigh.
intro ihigh.
assert(ibound: 0 ≤ Int.unsigned i ≤ EPT_PDPT_INDEX Int.max_unsigned).
{
unfold EPT_PDPT_INDEX.
xomega.
}
assert(zerobound: 0 ≤ 0 ≤ EPT_PML4_INDEX Int.max_unsigned).
{
unfold EPT_PML4_INDEX.
xomega.
}
Caseeq icase.
intro tmpH; destruct tmpH as [ival msubst].
injection msubst; intros; subst.
set (initd := adt {ept
: ZMap.set 0
(EPML4EValid
(ZMap.set (Int.unsigned i) (EPDPTEValid (ZMap.init EPDTEUndef))
epdpt)) (ept adt)}).
exploit (ept_init_epdte_loop_correct minit initd (ept_init_epdte_mk_rdata 0 511 initd) (PTree.set _j (Vint (Int.repr 0)) (set_opttemp None Vundef le)) 0); unfold initd; repeat vcgen.
esplit. esplit.
simpl.
rewrite ZMap.gss.
split.
reflexivity.
rewrite ival.
rewrite ZMap.gss.
reflexivity.
rewrite <- ival.
rewrite Int.repr_unsigned.
assumption.
destruct H as [le´ stmt].
destruct stmt as [stmt tmp].
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold setEPDPTE_spec.
rewrite ihost, ikern, pg, epdptvalid.
repeat rewrite zle_le_true; auto.
∃ (4 - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
Opaque Z.of_nat Z.to_nat.
simpl.
set (ni := Z.to_nat 511).
induction ni.
simpl.
unfold Calculate_EPDTE_at_j.
rewrite ival.
repeat rewrite ZMap.gss.
esplit; reflexivity.
simpl.
unfold Calculate_EPDTE_at_j.
destruct IHni.
rewrite H0.
destruct (ZMap.get 0 x).
repeat rewrite ZMap.gss.
esplit; reflexivity.
esplit; eauto.
right.
split.
omega.
unfold ept_init_epdpte_mk_rdata.
Transparent Z.to_nat.
rewrite ival; simpl.
unfold Calculate_EPDPTE_at_i.
rewrite epdptvalid.
unfold ept_init_epdte_mk_rdata.
reflexivity.
intro tmpH.
destruct tmpH as [igt0 mval].
injection mval; intros; subst.
set (initd := (ept_init_epdpte_mk_rdata (Int.unsigned i - 1) adt) {ept
: ZMap.set 0
(EPML4EValid
(ZMap.set (Int.unsigned i)
(EPDPTEValid (ZMap.init EPDTEUndef)) epdpt))
(Calculate_EPDPTE (Z.to_nat (Int.unsigned i - 1)) (ept adt))}).
exploit (ept_init_epdte_loop_correct minit initd (ept_init_epdte_mk_rdata (Int.unsigned i) 511 initd) (PTree.set _j (Vint (Int.repr 0)) (set_opttemp None Vundef le)) (Int.unsigned i)); unfold initd; repeat vcgen.
esplit. esplit.
simpl.
rewrite ZMap.gss.
split.
reflexivity.
rewrite ZMap.gss.
reflexivity.
destruct H as [le´ stmt].
destruct stmt as [stmt tmp].
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold setEPDPTE_spec.
simpl in ×.
rewrite ihost, ikern, pg, epdptvalid.
repeat rewrite zle_le_true; auto.
∃ (4 - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
Opaque Z.of_nat Z.to_nat.
simpl.
set (ni := Z.to_nat 511).
induction ni.
simpl.
unfold Calculate_EPDTE_at_j.
repeat rewrite ZMap.gss.
esplit; reflexivity.
simpl.
unfold Calculate_EPDTE_at_j.
destruct IHni.
rewrite H0.
destruct (ZMap.get (Int.unsigned i) x).
repeat rewrite ZMap.gss.
esplit; reflexivity.
esplit; eauto.
right.
split.
omega.
unfold ept_init_epdpte_mk_rdata.
f_equal.
replace (Int.unsigned i + 1 - 1) with (Int.unsigned i - 1 + 1) by omega.
change (Int.unsigned i - 1 + 1) with (Z.succ (Int.unsigned i - 1)).
rewrite Z2Nat.inj_succ with (n:=(Int.unsigned i - 1)).
Opaque Z.to_nat Z.of_nat.
simpl.
rewrite Nat2Z.inj_succ.
rewrite Z2Nat.id.
unfold Z.succ.
replace (Int.unsigned i - 1 + 1) with (Int.unsigned i) by omega.
unfold Calculate_EPDPTE_at_i.
simpl in epdptvalid.
rewrite epdptvalid.
unfold ept_init_epdte_mk_rdata.
symmetry.
reflexivity.
omega.
omega.
intro ival.
subst.
esplit. esplit.
repeat vcgen.
unfold ept_init_epdpte_loop_body_Q.
Caseeq icase.
intro tmpH; destruct tmpH.
rewrite ival in H0.
discriminate H0.
intro tmpH; destruct tmpH.
rewrite ival in H1.
injection H1; intros; subst.
split; eauto.
Qed.
End ept_init_epdpte_loop_proof.
Lemma ept_init_epdpte_loop_correct: ∀ m d d´ le,
pg d = true →
ihost d = true →
ikern d = true →
(∃ epdpt, ZMap.get 0 (ept d) = EPML4EValid epdpt) →
PTree.get _i le = Some (Vint Int.zero) →
d´ = ept_init_epdpte_mk_rdata 3 d →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) (Swhile ept_init_outter_while_condition ept_init_outter_while_body) E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize (ept_init_epdpte_loop_correct_aux m d H H0 H1 H2).
unfold ept_init_epdpte_loop_body_P.
unfold ept_init_epdpte_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp m´´val].
∃ le´.
subst.
repeat vcgen.
repeat vcgen.
Qed.
Lemma ept_init_body_correct: ∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get _mbi_adr le = Some (Vint mbi_adr) →
ept_init_spec (Int.unsigned mbi_adr) d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) ept_init_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold ept_init_body.
functional inversion H1; subst.
assert(zerobound: 0 ≤ 0 ≤ EPT_PML4_INDEX Int.max_unsigned).
{
unfold EPT_PML4_INDEX.
xomega.
}
set (initd := ((((((((((((((d { ioapic
: DeviceStateDataType.update_s (ioapic d)
(ObjInterruptDriver.ioapic_init_aux (DeviceStateDataType.s (ioapic d))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d)) + 1 - 1)))} {
lapic
: DeviceStateDataType.update_l3
(DeviceStateDataType.update_l2
(DeviceStateDataType.update_l1
(DeviceStateDataType.mkLApicData
{|
DeviceStateDataType.LapicEsr := 0;
DeviceStateDataType.LapicEoi := DeviceStateDataType.NoIntr;
DeviceStateDataType.LapicMaxLvt := DeviceStateDataType.LapicMaxLvt
(DeviceStateDataType.s
(lapic d));
DeviceStateDataType.LapicEnable := true;
DeviceStateDataType.LapicSpurious := 32 + 7;
DeviceStateDataType.LapicLint0Mask := true;
DeviceStateDataType.LapicLint1Mask := true;
DeviceStateDataType.LapicPcIntMask := true;
DeviceStateDataType.LapicLdr := 0;
DeviceStateDataType.LapicErrorIrq := 50;
DeviceStateDataType.LapicEsrClrPen := false;
DeviceStateDataType.LapicTpr := 0 |})
(DeviceStateDataType.l1 (lapic d)))
(DeviceStateDataType.l2 (lapic d)))
(DeviceStateDataType.l3 (lapic d))} { ioapic / s /
CurrentIrq : None} {vmxinfo : real_vmxinfo}) {pg : true}) {LAT
: real_LAT (LAT d)}) {nps : real_nps} {AC : AC_init}) {init : true}) {PT
: 0}) {ptpool : CalRealPT.real_pt (ptpool d)}) {idpde
: CalRealIDPDE.real_idpde (idpde d)}) {pb
: CalRealPTB.real_ptb (pb d)}) {smspool
: CalRealSMSPool.real_smspool (smspool d)}) {abtcb
: ZMap.set 0 (AbTCBValid RUN (-1))
(CalRealProcModule.real_abtcb (abtcb d))}) {abq
: CalRealProcModule.real_abq (abq d)}) {cid : 0}) {syncchpool
: CalRealProcModule.real_syncchpool (syncchpool d)}) {ept
: ZMap.set 0 (EPML4EValid (ZMap.init EPDPTEUndef)) (ept d)}).
exploit (ept_init_epdpte_loop_correct m initd (ept_init_epdpte_mk_rdata 3 initd) (PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef (set_opttemp None Vundef le)))); unfold initd; simpl; try reflexivity; try assumption; repeat ptreesolve.
esplit.
simpl.
rewrite ZMap.gss.
reflexivity.
intro stmt.
destruct stmt as [le´ stmt].
esplit.
change E0 with (E0 ** E0).
econstructor.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
vcgen.
unfold proc_init_spec.
rewrite H3, H4, H5, H6, H7, H8, H9, H10.
reflexivity.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
unfold setEPML4_spec.
simpl.
rewrite H4, H5.
reflexivity.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
eapply stmt.
Qed.
End EPTInitBody.
Theorem ept_init_code_correct:
spec_le (ept_init ↦ ept_init_spec_low) (〚ept_init ↦ f_ept_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (ept_init_body_correct s (Genv.globalenv p) makeglobalenv b3 Hb3fs Hb3fp b2 Hb2fs Hb2fp b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ept_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_ept_init)))) H0.
Qed.
End EPT_Init.
End WithPrimitives.
End EPTINTROCODEEPTINIT.