Library mcertikos.proc.VEPTIntroCodeEPTInit
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 VEPTIntro.
Require Import VEPTIntroCSource.
Require Import ObjProc.
Require Import ObjEPT.
Require Import CalRealIntelModule.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Module EPTINTROCODEEPTINIT.
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 EPT_Init.
Let L: compatlayer (cdata RData) :=
set_EPDPTE ↦ gensem setEPDPTE_spec
⊕ set_EPDTE ↦ gensem setEPDTE_spec
⊕ set_EPML4E ↦ gensem setEPML4_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).
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 VEPTIntro.
Require Import VEPTIntroCSource.
Require Import ObjProc.
Require Import ObjEPT.
Require Import CalRealIntelModule.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Module EPTINTROCODEEPTINIT.
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 EPT_Init.
Let L: compatlayer (cdata RData) :=
set_EPDPTE ↦ gensem setEPDPTE_spec
⊕ set_EPDTE ↦ gensem setEPDTE_spec
⊕ set_EPML4E ↦ gensem setEPML4_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).
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 (cpuid : Z) (i j: Z) (adt: RData)
:= adt {ept: ZMap.set cpuid (Calculate_EPDTE i (Z.to_nat j) (ZMap.get cpuid (ept adt))) (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 CPU_ID_range: 0 ≤ (CPU_ID adt) < TOTAL_CPU.
Hypothesis eptvalid: ∃ epdpt epdt, ZMap.get 0 (ZMap.get (CPU_ID adt) (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 (CPU_ID adt) 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 (CPU_ID adt) i (Int.unsigned j - 1) adt) ∧
(∃ epdpt epdt, ZMap.get 0 (ZMap.get (CPU_ID adt) (ept
(ept_init_epdte_mk_rdata
(CPU_ID adt) 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 ikern, pg, ihost, 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.
rewrite ZMap.gss.
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 ZMap.set2.
rewrite ZMap.gss in epdptvalid.
rewrite epdptvalid, epdtvalid.
split.
simpl in ×.
assert (ept_double_update: ∀ eptp eptp´, (adt {ept: eptp}) {ept: eptp´}
= adt {ept:eptp´}).
{ intros.
unfold update_ept; simpl; auto. }
rewrite ept_double_update.
rewrite ZMap.gss.
reflexivity.
esplit. esplit.
split.
rewrite ZMap.gss.
rewrite ZMap.gss.
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 →
0 ≤ CPU_ID d < TOTAL_CPU →
(∃ epdpt epdt, ZMap.get 0 (ZMap.get (CPU_ID d) (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 (CPU_ID d) 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 H4).
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 (cpuid : Z) (i: Z) (adt: RData)
:= adt {ept: ZMap.set cpuid (Calculate_EPDPTE (Z.to_nat i)
(ZMap.get cpuid (ept adt))) (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 CPU_ID_range : 0 ≤ CPU_ID adt < TOTAL_CPU.
Hypothesis eptvalid: (∃ epdpt, ZMap.get 0 (ZMap.get (CPU_ID adt) (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 (CPU_ID adt) 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 (ZMap.get (CPU_ID (snd m)) (ept (snd m))) = EPML4EValid epdpt) ∧
(Int.unsigned i = 0 ∧ m = (minit, adt) ∨ 0 < Int.unsigned i ∧
m = (minit, ept_init_epdpte_mk_rdata (CPU_ID (snd m)) (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 (CPU_ID adt)
(ZMap.set 0
(EPML4EValid
(ZMap.set (Int.unsigned i) (EPDPTEValid (ZMap.init EPDTEUndef))
epdpt)) (ZMap.get (CPU_ID adt) (ept adt)))
(ept adt)}).
exploit (ept_init_epdte_loop_correct minit initd
(ept_init_epdte_mk_rdata (CPU_ID adt) 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.
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 ZMap.gss.
rewrite ZMap.gss.
rewrite ZMap.gss in H0.
rewrite ZMap.gss in H0.
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.
assert (ept_double_update: ∀ eptp eptp´, (adt {ept: eptp}) {ept: eptp´} = adt {ept:eptp´}).
{ intros.
unfold update_ept; simpl; auto. }
rewrite ept_double_update.
Opaque Calculate_EPDTE.
simpl.
rewrite ZMap.gss.
simpl.
f_equal.
rewrite ZMap.set2.
reflexivity.
×
intro tmpH.
destruct tmpH as [igt0 mval].
injection mval; intros.
assert (CPU_ID r = CPU_ID adt).
{ simpl in H.
clearAllExceptOne H.
rewrite H.
simpl; auto. }
rewrite H1 in H.
subst.
set (initd := (ept_init_epdpte_mk_rdata (CPU_ID adt) (Int.unsigned i - 1) adt)
{ept : ZMap.set
(CPU_ID adt)
(ZMap.set 0
(EPML4EValid
(ZMap.set (Int.unsigned i)
(EPDPTEValid
(ZMap.init EPDTEUndef)) epdpt))
(Calculate_EPDPTE (Z.to_nat (Int.unsigned i - 1))
(ZMap.get (CPU_ID adt) (ept adt)))) (ept adt)}).
exploit (ept_init_epdte_loop_correct
minit initd
(ept_init_epdte_mk_rdata (CPU_ID adt) (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.
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.
simpl.
unfold ret; simpl.
f_equal.
simpl.
f_equal.
rewrite ZMap.gss.
rewrite ZMap.set2.
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.
rewrite ZMap.gss.
repeat rewrite ZMap.gss.
Transparent Calculate_EPDTE.
simpl.
unfold Calculate_EPDTE_at_j.
esplit.
rewrite ZMap.gss.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
simpl.
unfold Calculate_EPDTE_at_j.
destruct IHni.
rewrite ZMap.gss in H0.
rewrite ZMap.gss in H0.
repeat rewrite ZMap.gss.
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 ZMap.gss in epdptvalid.
rewrite epdptvalid.
unfold ept_init_epdte_mk_rdata.
symmetry.
assert (ept_double_update: ∀ eptp eptp´, (adt {ept: eptp}) {ept: eptp´}
= adt {ept:eptp´}).
{ intros.
unfold update_ept; simpl; auto. }
rewrite ept_double_update.
rewrite ept_double_update.
Opaque Calculate_EPDTE.
simpl.
rewrite ZMap.set2.
rewrite ZMap.gss.
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.
idtac.
simpl in H1.
assert (CPU_ID r = CPU_ID adt).
{ simpl in H1.
clearAllExceptOne H1.
injection H1.
intros.
rewrite H.
simpl; auto. }
rewrite H2 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 →
0 ≤ CPU_ID d < TOTAL_CPU →
(∃ epdpt, ZMap.get 0 (ZMap.get (CPU_ID d) (ept d))
= EPML4EValid epdpt) →
PTree.get _i le = Some (Vint Int.zero) →
d´ = ept_init_epdpte_mk_rdata (CPU_ID d) 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 H3).
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,
env = PTree.empty _ →
ept_init_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_ept_init_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold f_ept_init_body.
functional inversion H0; subst.
assert(zerobound: 0 ≤ 0 ≤ EPT_PML4_INDEX Int.max_unsigned).
{
unfold EPT_PML4_INDEX.
xomega.
}
set (initd := d {ept : ZMap.set (CPU_ID d)
(ZMap.set 0 (EPML4EValid (ZMap.init EPDPTEUndef))
(ZMap.get (CPU_ID d) (ept d)))
(ept d)}).
assert (cpuid_eq: CPU_ID d = CPU_ID initd).
{ unfold initd.
simpl.
auto. }
exploit (ept_init_epdpte_loop_correct
m initd
(ept_init_epdpte_mk_rdata (CPU_ID initd) 3 initd)
(PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef (set_opttemp None Vundef le))));
try reflexivity; try assumption; repeat ptreesolve.
- rewrite <- cpuid_eq; inv H1; auto.
- esplit; simpl.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
- intro stmt.
destruct stmt as [le´ stmt].
esplit.
change E0 with (E0 ** E0).
unfold exec_stmt.
econstructor.
+ repeat vcgen.
+ repeat vcgen.
simpl in stmt.
simpl.
fold initd.
unfold ept_init_epdpte_mk_rdata in stmt.
simpl in stmt.
unfold initd in stmt.
unfold initd.
assert (ept_double_update: ∀ eptp eptp´, (d {ept: eptp})
{ept: eptp´} = d {ept:eptp´}).
{ intros.
unfold update_ept; simpl; auto. }
rewrite ept_double_update in stmt.
unfold exec_stmt in stmt.
rewrite ZMap.gss in stmt.
rewrite ZMap.set2 in stmt.
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
b2 Hb2fs Hb2fp b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ept_init)
(nil)
(create_undef_temps (fn_temps f_ept_init)))) H0.
Qed.
End EPT_Init.
End WithPrimitives.
End EPTINTROCODEEPTINIT.