Library mcertikos.mm.PTBitGenLink
*********************************************************************** * * * 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 MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import VCGen.
Require Import RealParams.
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 I64Layer.
Require Import LinkTactic.
Require Import CompCertiKOSproof.
Require Import LayerCalculusLemma.
Require Import MPTInit.
Require Import MPTBit.
Require Import MPTInitCode.
Require Import PTBitGen.
Require Import PTBitGenSpec.
Require Import MPTInitCSource.
Require Import PTBitGenLinkSource.
Section WITHCOMPCERTIKOS.
Context `{compcertikos_prf: CompCertiKOS}.
Context `{real_params_prf : RealParams}.
Notation HDATA := AbstractDataType.RData.
Notation LDATA := AbstractDataType.RData.
Notation HDATAOps := (cdata (cdata_ops := mptinit_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mptinit_data_ops) LDATA).
Lemma set_bit_correct:
∀ COMPILABLE: LayerCompilable ((PTP_LOC ↦ ptp_loc_type ⊕ mptinit) ⊕ L64),
∀ MOK: ModuleOK (set_bit ↦ f_set_bit),
∀ M2: LAsm.module,
CompCertiKOS.transf_module (set_bit ↦ f_set_bit) = OK M2 →
cl_sim _ _
(crel HDATA LDATA)
(set_bit ↦ gensem set_pt_bit_spec)
(〚 M2 〛((PTP_LOC ↦ ptp_loc_type ⊕ mptinit) ⊕ L64)).
Proof.
intros.
eapply link_compiler; eauto.
- eapply setbit_spec_ref.
- link_nextblock.
- link_kernel_mode.
- eapply MPTINITCODE.set_bit_correct.
- apply left_upper_bound.
Qed.
Lemma is_used_correct:
∀ COMPILABLE: LayerCompilable ((PTP_LOC ↦ ptp_loc_type ⊕ mptinit) ⊕ L64),
∀ MOK: ModuleOK (is_used ↦ f_is_used),
∀ M2: LAsm.module,
CompCertiKOS.transf_module (is_used ↦ f_is_used) = OK M2 →
cl_sim _ _
(crel HDATA LDATA)
(is_used ↦ gensem is_pt_used_spec)
(〚 M2 〛((PTP_LOC ↦ ptp_loc_type ⊕ mptinit) ⊕ L64)).
Proof.
intros.
eapply link_compiler; eauto.
- eapply isused_spec_ref.
- link_nextblock.
- link_kernel_mode.
- eapply MPTINITCODE.is_used_correct.
- apply left_upper_bound.
Qed.
XXX: added
Record MPTBit_impl_inverted (M: module) : Prop:=
{
MPTBIT_set_bit: module;
MPTBIT_is_used: module;
MPTBIT_set_bit_transf: CompCertiKOS.transf_module (set_bit ↦ f_set_bit) = ret MPTBIT_set_bit;
MPTBIT_is_used_transf: CompCertiKOS.transf_module (is_used ↦ f_is_used) = ret MPTBIT_is_used;
MPTBIT_M: M = (((MPTBIT_set_bit ⊕ MPTBIT_is_used)
⊕ PTP_LOC ↦ ptp_loc_type)
⊕ ∅);
MPTBIT_Mok: LayerOK (〚M 〛 (mptinit ⊕ L64) ⊕ mptinit ⊕ L64);
MPTBIT_Lok: LayerOK
(〚MPTBIT_set_bit ⊕ MPTBIT_is_used〛
((mptinit ⊕ L64) ⊕ PTP_LOC ↦ ptp_loc_type)
⊕ (mptinit ⊕ L64) ⊕ PTP_LOC ↦ ptp_loc_type)
}.
{
MPTBIT_set_bit: module;
MPTBIT_is_used: module;
MPTBIT_set_bit_transf: CompCertiKOS.transf_module (set_bit ↦ f_set_bit) = ret MPTBIT_set_bit;
MPTBIT_is_used_transf: CompCertiKOS.transf_module (is_used ↦ f_is_used) = ret MPTBIT_is_used;
MPTBIT_M: M = (((MPTBIT_set_bit ⊕ MPTBIT_is_used)
⊕ PTP_LOC ↦ ptp_loc_type)
⊕ ∅);
MPTBIT_Mok: LayerOK (〚M 〛 (mptinit ⊕ L64) ⊕ mptinit ⊕ L64);
MPTBIT_Lok: LayerOK
(〚MPTBIT_set_bit ⊕ MPTBIT_is_used〛
((mptinit ⊕ L64) ⊕ PTP_LOC ↦ ptp_loc_type)
⊕ (mptinit ⊕ L64) ⊕ PTP_LOC ↦ ptp_loc_type)
}.
XXX: added
Lemma module_impl_imply:
∀ M, MPTBit_impl = OK M → MPTBit_impl_inverted M.
Proof.
unfold MPTBit_impl. intros M HM.
inv_monad´ HM.
inv_monad´ HM0.
econstructor.
eassumption.
eassumption.
inv HM1. reflexivity.
apply x1.
apply x3.
Qed.
Lemma link_correct_aux:
∀ M, MPTBit_impl = OK M →
mptinit ⊕ L64
⊢ (path_inj (crel HDATA LDATA), M)
: mptbit ⊕ L64.
Proof.
∀ M, MPTBit_impl = OK M → MPTBit_impl_inverted M.
Proof.
unfold MPTBit_impl. intros M HM.
inv_monad´ HM.
inv_monad´ HM0.
econstructor.
eassumption.
eassumption.
inv HM1. reflexivity.
apply x1.
apply x3.
Qed.
Lemma link_correct_aux:
∀ M, MPTBit_impl = OK M →
mptinit ⊕ L64
⊢ (path_inj (crel HDATA LDATA), M)
: mptbit ⊕ L64.
Proof.
XXX: added
intros M HM.
eapply module_impl_imply in HM; destruct HM; subst.
unfold mptbit.
eapply conseq_le_assoc_comm.
hcomp_tac.
{
apply transfer_variable.
eapply module_impl_imply in HM; destruct HM; subst.
unfold mptbit.
eapply conseq_le_assoc_comm.
hcomp_tac.
{
apply transfer_variable.
XXX: added
apply MPTBIT_Lok.
eapply (LayerOK_impl_subst MPTBIT_Mok0).
apply module_le_left.
reflexivity.
unfold mptbit_fresh.
layer_link_split_tac.
- apply set_bit_correct; code_correct_tac.
- apply is_used_correct; code_correct_tac.
}
{
eapply layer_link_new_glbl_both.
apply oplus_sim_monotonic.
apply passthrough_correct.
apply L64_auto_sim.
}
Qed.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import CommonTactic.
Lemma init_correct:
∀ M, MPTBit_impl = OK M →
ModuleOK M →
cl_init_sim HDATAOps LDATAOps (crel HDATA LDATA) (mptbit ⊕ L64) M (mptinit⊕ L64).
Proof.
Opaque oplus.
intros.
pose proof (fun i ⇒ module_ok_variable M i (H0 i)) as MOK; clear H0. apply cl_init_sim_intro.
- intros.
eapply (LayerOK_impl_subst MPTBIT_Mok0).
apply module_le_left.
reflexivity.
unfold mptbit_fresh.
layer_link_split_tac.
- apply set_bit_correct; code_correct_tac.
- apply is_used_correct; code_correct_tac.
}
{
eapply layer_link_new_glbl_both.
apply oplus_sim_monotonic.
apply passthrough_correct.
apply L64_auto_sim.
}
Qed.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import CommonTactic.
Lemma init_correct:
∀ M, MPTBit_impl = OK M →
ModuleOK M →
cl_init_sim HDATAOps LDATAOps (crel HDATA LDATA) (mptbit ⊕ L64) M (mptinit⊕ L64).
Proof.
Opaque oplus.
intros.
pose proof (fun i ⇒ module_ok_variable M i (H0 i)) as MOK; clear H0. apply cl_init_sim_intro.
- intros.
XXX: added
eapply module_impl_imply in H; destruct H; subst.
inv_monad´ H0.
generalize (make_program_make_globalenv _ _ _ _ H1).
intros HP. pose proof HP as HP´.
eapply make_globalenv_stencil_matches in HP´.
unfold MVar in HP.
inv_make_globalenv HP.
rewrite (stencil_matches_symbols _ _ HP´) in ×.
inv HP´.
constructor.
+ constructor; simpl; trivial. apply FlatMem.flatmem_empty_inj.
+ econstructor; eauto.
× econstructor; eauto.
specialize (Genv.init_mem_characterization _ _ Hbvi H2); eauto.
unfold Genv.perm_globvar; simpl; intros [Hperm _].
assert(HVALID: ∀ ofs, 0≤ ofs < num_proc →
Mem.valid_access m2 Mint32 b (ofs × 4) Writable).
{
intros; split; simpl.
change (Z.max 256 0) with 256 in Hperm.
unfold Mem.range_perm in ×.
intros. apply Hperm. omega.
apply Zdivide_mult_r. apply Zdivide_refl.
}
assert(HEX: ∀ ofs, 0≤ ofs < num_proc →
(∃ v, Mem.load Mint32 m2 b (ofs × 4) = Some v)).
{
intros; apply (Mem.valid_access_load).
apply Mem.valid_access_implies with Writable.
apply HVALID; trivial.
constructor.
}
intros.
specialize (HVALID _ H).
destruct (HEX _ H) as [v1 HEX1].
refine_split´; eauto.
rewrite ZMap.gi. constructor.
- unfold mptbit. simpl; intros.
destruct H0 as [HF|HF]; inv HF; reflexivity.
- unfold mptbit. simpl; intros.
destruct H0 as [HF|HF]; inv HF; reflexivity.
- intros.
inv_monad´ H0.
generalize (make_program_make_globalenv _ _ _ _ H1).
intros HP. pose proof HP as HP´.
eapply make_globalenv_stencil_matches in HP´.
unfold MVar in HP.
inv_make_globalenv HP.
rewrite (stencil_matches_symbols _ _ HP´) in ×.
inv HP´.
constructor.
+ constructor; simpl; trivial. apply FlatMem.flatmem_empty_inj.
+ econstructor; eauto.
× econstructor; eauto.
specialize (Genv.init_mem_characterization _ _ Hbvi H2); eauto.
unfold Genv.perm_globvar; simpl; intros [Hperm _].
assert(HVALID: ∀ ofs, 0≤ ofs < num_proc →
Mem.valid_access m2 Mint32 b (ofs × 4) Writable).
{
intros; split; simpl.
change (Z.max 256 0) with 256 in Hperm.
unfold Mem.range_perm in ×.
intros. apply Hperm. omega.
apply Zdivide_mult_r. apply Zdivide_refl.
}
assert(HEX: ∀ ofs, 0≤ ofs < num_proc →
(∃ v, Mem.load Mint32 m2 b (ofs × 4) = Some v)).
{
intros; apply (Mem.valid_access_load).
apply Mem.valid_access_implies with Writable.
apply HVALID; trivial.
constructor.
}
intros.
specialize (HVALID _ H).
destruct (HEX _ H) as [v1 HEX1].
refine_split´; eauto.
rewrite ZMap.gi. constructor.
- unfold mptbit. simpl; intros.
destruct H0 as [HF|HF]; inv HF; reflexivity.
- unfold mptbit. simpl; intros.
destruct H0 as [HF|HF]; inv HF; reflexivity.
- intros.
XXX: added
eapply module_impl_imply in H; destruct H; subst.
transf_none i. specialize (MOK i).
destruct H0 as [HF|HF]; inv HF; econstructor.
get_module_variable_relfexivity.
- intros.
transf_none i. specialize (MOK i).
destruct H0 as [HF|HF]; inv HF; econstructor.
get_module_variable_relfexivity.
- intros.
XXX: added
eapply module_impl_imply in H; destruct H; subst.
transf_none i. specialize (MOK i).
destruct (peq i PTP_LOC); subst.
+ eapply (get_module_varible_OK_Some_left ptp_loc_type) in H0; subst.
reflexivity.
destruct (get_module_variable_isOK _ _ _ MOK) as [HT1 _].
get_module_variable_relfexivity.
+ assert (get_module_variable
i (((MPTBIT_set_bit ⊕ MPTBIT_is_used) ⊕ PTP_LOC ↦ ptp_loc_type) ⊕ ∅) = OK None).
{
get_module_variable_relfexivity.
}
unfold module, module_ops in ×.
congruence.
- decision.
Qed.
Theorem cl_backward_simulation:
∀ (s: stencil) (CTXT M: module) pl ph
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
MPTBit_impl = OK M →
make_program s CTXT (mptbit ⊕ L64) = OK ph →
make_program s (CTXT ⊕ M) (mptinit ⊕ L64) = OK pl →
backward_simulation
(LAsm.semantics (lcfg_ops := LC (mptbit ⊕ L64)) ph)
(LAsm.semantics (lcfg_ops := LC (mptinit ⊕ L64)) pl).
Proof.
intros.
eapply (soundness (crel HDATA LDATA)); try eassumption; try decision.
eapply link_correct_aux; eauto.
eapply init_correct; eauto.
eapply make_program_oplus_right; eassumption.
transf_none i. specialize (MOK i).
destruct (peq i PTP_LOC); subst.
+ eapply (get_module_varible_OK_Some_left ptp_loc_type) in H0; subst.
reflexivity.
destruct (get_module_variable_isOK _ _ _ MOK) as [HT1 _].
get_module_variable_relfexivity.
+ assert (get_module_variable
i (((MPTBIT_set_bit ⊕ MPTBIT_is_used) ⊕ PTP_LOC ↦ ptp_loc_type) ⊕ ∅) = OK None).
{
get_module_variable_relfexivity.
}
unfold module, module_ops in ×.
congruence.
- decision.
Qed.
Theorem cl_backward_simulation:
∀ (s: stencil) (CTXT M: module) pl ph
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
MPTBit_impl = OK M →
make_program s CTXT (mptbit ⊕ L64) = OK ph →
make_program s (CTXT ⊕ M) (mptinit ⊕ L64) = OK pl →
backward_simulation
(LAsm.semantics (lcfg_ops := LC (mptbit ⊕ L64)) ph)
(LAsm.semantics (lcfg_ops := LC (mptinit ⊕ L64)) pl).
Proof.
intros.
eapply (soundness (crel HDATA LDATA)); try eassumption; try decision.
eapply link_correct_aux; eauto.
eapply init_correct; eauto.
eapply make_program_oplus_right; eassumption.
XXX: added
eapply module_impl_imply in H.
destruct H. assumption.
Qed.
Require Import LAsmModuleSemMakeProgram.
Theorem make_program_exists:
∀ (s: stencil) (CTXT M: module) pl,
MPTBit_impl = OK M →
make_program s (CTXT ⊕ M) (mptinit ⊕ L64) = OK pl →
∃ ph, make_program s CTXT (mptbit ⊕ L64) = OK ph.
Proof.
intros.
exploit link_correct_aux; eauto.
eapply make_program_vertical´ in H0.
destruct H0 as [p´ Hmake].
intros Hle.
eapply make_program_sim_monotonic_exists.
2: eapply Hle.
reflexivity.
eassumption.
destruct H. assumption.
Qed.
Require Import LAsmModuleSemMakeProgram.
Theorem make_program_exists:
∀ (s: stencil) (CTXT M: module) pl,
MPTBit_impl = OK M →
make_program s (CTXT ⊕ M) (mptinit ⊕ L64) = OK pl →
∃ ph, make_program s CTXT (mptbit ⊕ L64) = OK ph.
Proof.
intros.
exploit link_correct_aux; eauto.
eapply make_program_vertical´ in H0.
destruct H0 as [p´ Hmake].
intros Hle.
eapply make_program_sim_monotonic_exists.
2: eapply Hle.
reflexivity.
eassumption.
XXX: added