Library mcertikos.proc.EPTIntroGenLink
Require Import LinkTemplate.
Require Import VEPTIntro.
Require Import EPTIntroGen.
Require Import EPTIntroGenLinkSource.
Require Import PProc.
Require Import PProcCSource.
Require Import PProcCode.
Require Import EPTIntroGenAsm.
Section WITHCOMPCERTIKOS.
Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{multi_oracle_link: !MultiOracleLink}.
Notation EptSize := 8413184.
Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
(p <- make_program s (CTXT ⊕ (md ⊕ EPT_LOC ↦ v_ept) ⊕ ∅) (pproc ⊕ L64);
ret (Genv.init_mem p) = OK (Some m))
→ ∃ b, find_symbol s EPT_LOC = Some b ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID) Writable ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + 4) Writable ∧
∀ i : Z, 0 ≤ i ≤ EPT_PDPT_INDEX Int.max_unsigned →
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + 4096 + i × 8) Writable ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + 4096 + i × 8 + 4) Writable ∧
∀ j : Z, 0 ≤ j ≤ EPT_PDIR_INDEX Int.max_unsigned →
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + (i + 2) × 4096 + j × 8) Writable ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + (i + 2) × 4096 + j × 8 + 4) Writable ∧
∀ k : Z, 0 ≤ k ≤ EPT_PTAB_INDEX Int.max_unsigned →
Mem.valid_access m Mint64 b (EptSize × GlobalOracle.current_CPU_ID + (6 + i × 512 + j) × 4096 + k × 8) Writable.
Proof.
intros mkprog; inv_monad´ mkprog.
assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
pose proof mkgenv as mkgenv´.
eapply make_globalenv_stencil_matches in mkgenv´.
inv_make_globalenv mkgenv. subst.
rewrite (stencil_matches_symbols _ _ mkgenv´) in ×. inv mkgenv´.
eexists; split; try eassumption.
specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
Local Opaque Z.add Z.mul.
unfold Genv.perm_globvar; simpl; intros [Hperm _].
change (Z.max (align (align (align (align (align 0 4 + 4096) 4 + 4096) 4 +
16384) 4 + 8388608) (Z.max 4 (Z.max 4 (Z.max 4 (Z.max 4 1))))) 0 +
0) with 8413184 in Hperm.
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
generalize current_CPU_ID_range; intro.
omega.
- simpl. ∃ (2103296 × GlobalOracle.current_CPU_ID). omega.
}
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + 1). simpl. omega.
}
intros. change (EPT_PDPT_INDEX Int.max_unsigned) with 3 in H.
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H1.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + (1024 + i × 2)). simpl. omega.
}
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H1.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + (1024 + i × 2 + 1)). simpl. omega.
}
intros. change (EPT_PDIR_INDEX Int.max_unsigned) with 511 in H1.
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H2.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + ((i + 2) × 1024 + j × 2)). simpl. omega.
}
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H2.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + ((i + 2) × 1024 + j × 2 + 1)). simpl. omega.
}
intros. change (EPT_PTAB_INDEX Int.max_unsigned) with 511 in H2.
{ split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H3.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (1051648 × GlobalOracle.current_CPU_ID + ((6 + i × 512 + j) × 512 + k)). simpl. omega.
}
Qed.
Lemma init_correct:
init_correct_type VEPTIntro_module pproc eptintro.
Proof.
init_correct.
exploit make_program_find_symbol; eauto.
intros (b´ & find_symbol_EPT_LOC & access0 & access4 & access).
econstructor; try eassumption.
repeat rewrite ZMap.gi. econstructor.
Qed.
Lemma link_correct_aux:
link_correct_aux_type VEPTIntro_module pproc eptintro.
Proof.
link_correct_aux.
- link_cfunction getEPTE_spec_ref PPROCCODE.get_EPTE_code_correct.
- link_cfunction setEPTE_spec_ref PPROCCODE.set_EPTE_code_correct.
- link_cfunction setEPDPTE_spec_ref PPROCCODE.set_EPDPTE_code_correct.
- link_cfunction setEPDTE_spec_ref PPROCCODE.set_EPDTE_code_correct.
- link_cfunction setEPML4_spec_ref PPROCCODE.set_EPML4E_code_correct.
- link_asmfunction ept_invalidate_mappings_spec_ref ept_invalidate_mappings_code_correct.
- apply passthrough_correct.
Qed.
Theorem cl_backward_simulation:
cl_backward_simulation_type VEPTIntro_module pproc eptintro.
Proof.
cl_backward_simulation init_correct link_correct_aux.
Qed.
Theorem make_program_exists:
make_program_exist_type VEPTIntro_module pproc eptintro.
Proof.
make_program_exists link_correct_aux.
Qed.
End WITHCOMPCERTIKOS.
Require Import VEPTIntro.
Require Import EPTIntroGen.
Require Import EPTIntroGenLinkSource.
Require Import PProc.
Require Import PProcCSource.
Require Import PProcCode.
Require Import EPTIntroGenAsm.
Section WITHCOMPCERTIKOS.
Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{multi_oracle_link: !MultiOracleLink}.
Notation EptSize := 8413184.
Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
(p <- make_program s (CTXT ⊕ (md ⊕ EPT_LOC ↦ v_ept) ⊕ ∅) (pproc ⊕ L64);
ret (Genv.init_mem p) = OK (Some m))
→ ∃ b, find_symbol s EPT_LOC = Some b ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID) Writable ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + 4) Writable ∧
∀ i : Z, 0 ≤ i ≤ EPT_PDPT_INDEX Int.max_unsigned →
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + 4096 + i × 8) Writable ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + 4096 + i × 8 + 4) Writable ∧
∀ j : Z, 0 ≤ j ≤ EPT_PDIR_INDEX Int.max_unsigned →
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + (i + 2) × 4096 + j × 8) Writable ∧
Mem.valid_access m Mint32 b (EptSize × GlobalOracle.current_CPU_ID + (i + 2) × 4096 + j × 8 + 4) Writable ∧
∀ k : Z, 0 ≤ k ≤ EPT_PTAB_INDEX Int.max_unsigned →
Mem.valid_access m Mint64 b (EptSize × GlobalOracle.current_CPU_ID + (6 + i × 512 + j) × 4096 + k × 8) Writable.
Proof.
intros mkprog; inv_monad´ mkprog.
assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
pose proof mkgenv as mkgenv´.
eapply make_globalenv_stencil_matches in mkgenv´.
inv_make_globalenv mkgenv. subst.
rewrite (stencil_matches_symbols _ _ mkgenv´) in ×. inv mkgenv´.
eexists; split; try eassumption.
specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
Local Opaque Z.add Z.mul.
unfold Genv.perm_globvar; simpl; intros [Hperm _].
change (Z.max (align (align (align (align (align 0 4 + 4096) 4 + 4096) 4 +
16384) 4 + 8388608) (Z.max 4 (Z.max 4 (Z.max 4 (Z.max 4 1))))) 0 +
0) with 8413184 in Hperm.
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
generalize current_CPU_ID_range; intro.
omega.
- simpl. ∃ (2103296 × GlobalOracle.current_CPU_ID). omega.
}
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + 1). simpl. omega.
}
intros. change (EPT_PDPT_INDEX Int.max_unsigned) with 3 in H.
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H1.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + (1024 + i × 2)). simpl. omega.
}
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H1.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + (1024 + i × 2 + 1)). simpl. omega.
}
intros. change (EPT_PDIR_INDEX Int.max_unsigned) with 511 in H1.
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H2.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + ((i + 2) × 1024 + j × 2)). simpl. omega.
}
split. { split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H2.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (2103296 × GlobalOracle.current_CPU_ID + ((i + 2) × 1024 + j × 2 + 1)). simpl. omega.
}
intros. change (EPT_PTAB_INDEX Int.max_unsigned) with 511 in H2.
{ split.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H3.
generalize current_CPU_ID_range; intro.
rewrite Zmax_spec.
destruct (zlt 0 (8 × 8413184)); try omega.
- ∃ (1051648 × GlobalOracle.current_CPU_ID + ((6 + i × 512 + j) × 512 + k)). simpl. omega.
}
Qed.
Lemma init_correct:
init_correct_type VEPTIntro_module pproc eptintro.
Proof.
init_correct.
exploit make_program_find_symbol; eauto.
intros (b´ & find_symbol_EPT_LOC & access0 & access4 & access).
econstructor; try eassumption.
repeat rewrite ZMap.gi. econstructor.
Qed.
Lemma link_correct_aux:
link_correct_aux_type VEPTIntro_module pproc eptintro.
Proof.
link_correct_aux.
- link_cfunction getEPTE_spec_ref PPROCCODE.get_EPTE_code_correct.
- link_cfunction setEPTE_spec_ref PPROCCODE.set_EPTE_code_correct.
- link_cfunction setEPDPTE_spec_ref PPROCCODE.set_EPDPTE_code_correct.
- link_cfunction setEPDTE_spec_ref PPROCCODE.set_EPDTE_code_correct.
- link_cfunction setEPML4_spec_ref PPROCCODE.set_EPML4E_code_correct.
- link_asmfunction ept_invalidate_mappings_spec_ref ept_invalidate_mappings_code_correct.
- apply passthrough_correct.
Qed.
Theorem cl_backward_simulation:
cl_backward_simulation_type VEPTIntro_module pproc eptintro.
Proof.
cl_backward_simulation init_correct link_correct_aux.
Qed.
Theorem make_program_exists:
make_program_exist_type VEPTIntro_module pproc eptintro.
Proof.
make_program_exists link_correct_aux.
Qed.
End WITHCOMPCERTIKOS.