Library mcertikos.proc.VEPTIntroCode
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 ObjEPT.
Require Import XOmega.
Module EPTINTROCODE.
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_GET_PAGE_ENTRY.
Let L: compatlayer (cdata RData) := get_EPTE ↦ gensem getEPTE_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 EPTGetPageEntryBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
get_EPTE
Variable bget_EPTE: block.
Hypothesis hget_EPTE1 : Genv.find_symbol ge get_EPTE = Some bget_EPTE.
Hypothesis hget_EPTE2 : Genv.find_funct_ptr ge bget_EPTE
= Some (External (EF_external get_EPTE
(signature_of_type
(Tcons tint
(Tcons tint (Tcons tint (Tcons tint Tnil))))
tint cc_default))
(Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default).
Lemma ept_get_page_entry_body_correct:
∀ m d env le gpa hpa,
env = PTree.empty _ →
PTree.get _gpa le = Some (Vint gpa) →
high_level_invariant d →
ept_get_page_entry_spec (Int.unsigned gpa) d = Some (Int.unsigned hpa) →
∃ le´,
exec_stmt ge env le ((m, d): mem) ept_get_page_entry_body E0 le´ (m, d) (Out_return (Some (Vint hpa, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold ept_get_page_entry_body.
functional inversion H2; subst.
unfold pml4, pdpt, pdir, ptab in ×.
unfold EPT_PML4_INDEX´, EPT_PDPT_INDEX´, EPT_PDIR_INDEX´, EPT_PTAB_INDEX´ in ×.
assert(ptabmax: EPT_PTAB_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PTAB_INDEX; reflexivity).
assert(pdirmax: EPT_PDIR_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PDIR_INDEX; reflexivity).
assert(pdptmax: EPT_PDPT_INDEX Int.max_unsigned = 3)
by (rewrite muval; unfold EPT_PDPT_INDEX; reflexivity).
assert(ptabrange: 0 ≤ Int.unsigned gpa mod 512 ≤ EPT_PTAB_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x ptabmax; xomega).
assert(pdirrange: 0 ≤ (Int.unsigned gpa / 512) mod 512 ≤ EPT_PDIR_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x pdirmax; xomega).
assert(pdptrange: 0 ≤ (Int.unsigned gpa / 262144) mod 512 ≤ EPT_PDPT_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x pdptmax; xomega).
assert(pml4val´: (Int.unsigned gpa / (512 × 512 × 512)) = 0).
{ clearAllExceptOne _x; xomega. }
assert(pml4val: (Int.unsigned gpa / (512 × 512 × 512)) mod 512 = 0).
{ rewrite pml4val´; apply Zmod_0_l. }
rewrite pml4val in H8.
esplit.
repeat vcgen.
unfold getEPTE_spec.
simpl in ×.
rewrite H4, H5, H6, H8, H9, H10, H11.
repeat rewrite zle_le_true; try omega.
reflexivity.
Qed.
End EPTGetPageEntryBody.
Theorem ept_get_page_entry_code_correct:
spec_le (ept_get_page_entry ↦ ept_get_page_entry_spec_low) (〚ept_get_page_entry ↦ f_ept_get_page_entry 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (ept_get_page_entry_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ept_get_page_entry)
(Vint gpa::nil)
(create_undef_temps (fn_temps f_ept_get_page_entry)))) H0.
Qed.
End EPT_GET_PAGE_ENTRY.
Section EPT_SET_PAGE_ENTRY.
Let L: compatlayer (cdata RData) := set_EPTE ↦ gensem setEPTE_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 EPTSetPageEntryBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
set_EPTE
Variable bset_EPTE: block.
Hypothesis hset_EPTE1 : Genv.find_symbol ge set_EPTE = Some bset_EPTE.
Hypothesis hset_EPTE2 : Genv.find_funct_ptr ge bset_EPTE
= Some (External (EF_external set_EPTE
(signature_of_type
(Tcons tint
(Tcons tint
(Tcons tint (Tcons tint (Tcons tint Tnil)))))
Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))))
Tvoid cc_default).
Lemma ept_set_page_entry_body_correct:
∀ m d d´ env le gpa hpa,
env = PTree.empty _ →
PTree.get _gpa le = Some (Vint gpa) →
PTree.get _hpa le = Some (Vint hpa) →
high_level_invariant d →
ept_set_page_entry_spec (Int.unsigned gpa) (Int.unsigned hpa) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) ept_set_page_entry_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold ept_set_page_entry_body.
functional inversion H3; subst.
unfold pml4, pdpt, pdir, ptab in ×.
unfold EPT_PML4_INDEX´, EPT_PDPT_INDEX´, EPT_PDIR_INDEX´, EPT_PTAB_INDEX´ in ×.
assert(ptabmax: EPT_PTAB_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PTAB_INDEX; reflexivity).
assert(pdirmax: EPT_PDIR_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PDIR_INDEX; reflexivity).
assert(pdptmax: EPT_PDPT_INDEX Int.max_unsigned = 3)
by (rewrite muval; unfold EPT_PDPT_INDEX; reflexivity).
assert(ptabrange: 0 ≤ Int.unsigned gpa mod 512 ≤ EPT_PTAB_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x ptabmax; xomega).
assert(pdirrange: 0 ≤ (Int.unsigned gpa / 512) mod 512 ≤ EPT_PDIR_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x pdirmax; xomega).
assert(pdptrange: 0 ≤ (Int.unsigned gpa / 262144) mod 512 ≤ EPT_PDPT_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x pdptmax; xomega).
assert(pml4val´: (Int.unsigned gpa / (512 × 512 × 512)) = 0).
{ clearAllExceptOne _x; xomega. }
assert(pml4val: (Int.unsigned gpa / (512 × 512 × 512)) mod 512 = 0).
{ rewrite pml4val´; apply Zmod_0_l. }
assert ((Int.unsigned gpa / 134217728) mod 512 = 0) by (clearAllExceptOne _x; xomega).
esplit.
repeat vcgen.
unfold setEPTE_spec.
simpl in ×.
rewrite H in H10.
rewrite H5, H6, H7, H10, H11, H12.
repeat rewrite zle_le_true; repeat rewrite zle_lt_true; try omega.
rewrite <- H.
repeat vcgen.
Qed.
End EPTSetPageEntryBody.
Theorem ept_set_page_entry_code_correct:
spec_le (ept_set_page_entry ↦ ept_set_page_entry_spec_low) (〚ept_set_page_entry ↦ f_ept_set_page_entry 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (ept_set_page_entry_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ept_set_page_entry)
((Vint gpa)::((Vint hpa)::nil))
(create_undef_temps (fn_temps f_ept_set_page_entry)))) H0.
Qed.
End EPT_SET_PAGE_ENTRY.
Section EPT_ADD_MAPPING.
Let L: compatlayer (cdata RData) := set_EPTE ↦ gensem setEPTE_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 EPTAddMappingBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
set_EPTE
Variable bset_EPTE: block.
Hypothesis hset_EPTE1 : Genv.find_symbol ge set_EPTE = Some bset_EPTE.
Hypothesis hset_EPTE2 : Genv.find_funct_ptr ge bset_EPTE
= Some (External (EF_external set_EPTE
(signature_of_type
(Tcons tint
(Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))))
Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))))
Tvoid cc_default).
Lemma ept_add_mapping_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 →
ept_add_mapping_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) ept_add_mapping_body E0 le´ (m, d´) (Out_return (Some (Vint res, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold ept_add_mapping_body.
functional inversion H4; subst.
unfold pml4, pdpt, pdir, ptab in ×.
unfold EPT_PML4_INDEX, EPT_PDPT_INDEX, EPT_PDIR_INDEX, EPT_PTAB_INDEX in ×.
assert(ptabmax: EPT_PTAB_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PTAB_INDEX; reflexivity).
assert(pdirmax: EPT_PDIR_INDEX Int.max_unsigned = 511)
by (rewrite muval; unfold EPT_PDIR_INDEX; reflexivity).
assert(pdptmax: EPT_PDPT_INDEX Int.max_unsigned = 3)
by (rewrite muval; unfold EPT_PDPT_INDEX; reflexivity).
assert(ptabrange: 0 ≤ (Int.unsigned gpa / 4096) mod 512 ≤ EPT_PTAB_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x ptabmax; xomega).
assert(pdirrange: 0 ≤ (Int.unsigned gpa / (4096 × 512)) mod 512 ≤ EPT_PDIR_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x pdirmax; xomega).
assert(pdptrange: 0 ≤ (Int.unsigned gpa / (4096 × 512 × 512)) mod 512 ≤ EPT_PDPT_INDEX Int.max_unsigned)
by (clearAllExceptTwo _x pdptmax; xomega).
assert (ptmlmin: 0 ≤ EPT_PML4_INDEX Int.max_unsigned)
by (rewrite muval; unfold EPT_PML4_INDEX; simpl; clearAll; xomega).
assert(pml4val´: (Int.unsigned gpa / (4096 × 512 × 512 × 512)) = 0).
{ clearAllExceptOne _x; xomega. }
assert(pml4val: (Int.unsigned gpa / (4096 × 512 × 512 × 512)) mod 512 = 0).
{ rewrite pml4val´; apply Zmod_0_l. }
assert(addrmaskval: 4294963200 ≤ Int.max_unsigned) by omega.
assert(hparange: 0 ≤ Int.unsigned hpa ≤ Int.max_unsigned)
by (clearAllExceptTwo _x0 muval; omega).
assert (memtype_range: 0 ≤ 2 × (2 × (2 × Int.unsigned mem_type)) ≤ Int.max_unsigned)
by (clearAllExceptTwo _x1 muval; omega).
assert (hpa_zlor_range: 0 ≤ Z.lor (Z.land (Int.unsigned hpa) 4294963200) 71 ≤ Int.max_unsigned).
{ apply Z_lor_range; [apply Z_land_range | ]; omega. }
assert (0 ≤ Z.lor (Z.lor (Z.land (Int.unsigned hpa) 4294963200) 71)
(Int.unsigned (Int.repr (2 × (2 × (2 × Int.unsigned mem_type))))) ≤ Int.max_unsigned).
{ apply Z_lor_range.
- exact hpa_zlor_range.
- rewrite Int.unsigned_repr.
+ exact memtype_range.
+ exact memtype_range. }
assert (gpa_div_range: 0 ≤ Int.unsigned gpa / Int.unsigned (Int.repr (4 × 1024)) ≤ Int.max_unsigned).
{ clearAllExceptTwo _x muval; rewrite muval.
assert (Int.unsigned (Int.repr (4 × 1024)) = (4 × 1024)).
{ apply Int.unsigned_repr; rewrite muval; omega. }
rewrite H; simpl; xomega. }
assert (gpa_div_range´: 0 ≤ Int.unsigned gpa / Int.unsigned (Int.repr (2 × (1024 × 1024))) ≤ Int.max_unsigned).
{ clearAllExceptTwo _x muval; rewrite muval.
assert (Int.unsigned (Int.repr (2 × (1024 × 1024))) = (2 × (1024 × 1024))).
{ apply Int.unsigned_repr; rewrite muval; omega. }
rewrite H; simpl; xomega. }
assert (gpa_div_range´´: 0 ≤ Int.unsigned gpa / Int.unsigned (Int.repr (1024 × (1024 × 1024))) ≤ Int.max_unsigned).
{ clearAllExceptTwo _x muval; rewrite muval.
assert (Int.unsigned (Int.repr (1024 × (1024 × 1024))) = (1024 × (1024 × 1024))).
{ apply Int.unsigned_repr; rewrite muval; omega. }
rewrite H; simpl; xomega. }
assert(H13a: ZMap.get 0 (ZMap.get (CPU_ID d) (ept d)) = EPML4EValid epdpt) by (rewrite <- pml4val; exact H13).
esplit.
Opaque Z.mul.
d3 vcgenfull; [ repeat vcgenfull | ].
d3 vcgenfull.
d3 vcgenfull; [ d6 vcgenfull | d3 vcgenfull | d3 vcgenfull | repeat vcgenfull | ].
d3 vcgenfull.
vcgenfull.
- d3 vcgenfull.
+ d3 vcgenfull.
+ d3 vcgenfull.
+ d3 vcgenfull.
+ d6 vcgenfull.
+ d3 vcgenfull.
+ d12 vcgenfull.
+ d3 vcgenfull.
+ d3 vcgenfull.
+ d3 vcgenfull.
d3 vcgenfull.
d3 vcgenfull.
d3 vcgenfull.
d3 vcgenfull.
d3 vcgenfull.
unfold setEPTE_spec.
change (1024 × (1024 × 1024)) with (4096 × 512 × 512).
change (2 × (1024 × 1024)) with (4096 × 512).
rewrite H7, H8, H9, H13a, H14, H15.
repeat rewrite zle_le_true; try omega.
unfold ept´, pdpte´, epdt´, eptab´, va.
rewrite pml4val.
assert(shift_eq: 2 × (2 × (2 × Int.unsigned mem_type)) = Z.shiftl (Int.unsigned mem_type) 3).
{ rewrite Z.shiftl_mul_pow2; [ | omega].
clearAllExceptOne _x1.
simpl.
rewrite Zpower_pos_nat.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_1.
simpl.
rewrite Zpower_nat_succ_r.
rewrite Zpower_nat_succ_r.
rewrite Zpower_nat_succ_r.
rewrite Zpower_nat_0_r.
omega. }
rewrite shift_eq.
reflexivity.
auto.
change (Int.unsigned (Int.repr (4 × 1024))) with 4096.
apply ptabrange.
change (Int.unsigned (Int.repr (4 × 1024))) with 4096.
rewrite muval. omega.
change (Int.unsigned (Int.repr (2 × (1024 × 1024)))) with (4096 × 512).
omega.
change (Int.unsigned (Int.repr (2 × (1024 × 1024)))) with (4096 × 512).
rewrite muval. omega.
repeat vcgenfull.
change (1024 × (1024 × 1024)) with (4096 × 512 × 512).
omega.
change (1024 × (1024 × 1024)) with (4096 × 512 × 512).
rewrite muval. omega.
- unfold ept´, pdpte´, epdt´, eptab´, va.
rewrite pml4val.
vcgenfull.
rewrite H6.
rewrite Int.repr_unsigned.
d3 vcgenfull.
Qed.
End EPTAddMappingBody.
Theorem ept_add_mapping_code_correct:
spec_le (ept_add_mapping ↦ ept_add_mapping_spec_low) (〚ept_add_mapping ↦ f_ept_add_mapping 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (ept_add_mapping_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ept_add_mapping)
((Vint gpa)::(Vint hpa)::(Vint memtype)::nil)
(create_undef_temps (fn_temps f_ept_add_mapping)))) H0.
Qed.
End EPT_ADD_MAPPING.
End WithPrimitives.
End EPTINTROCODE.