Library mcertikos.mm.ALInitGenPassthrough
*********************************************************************** * * * 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. * * * ***********************************************************************
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Section Refinement.
Context `{real_params: RealParams}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Section Exists.
Lemma setPG_exist:
∀ habd habd´ labd f,
setPG0_spec habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, setPG_spec labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold setPG0_spec, setPG_spec; intros until f; exist_simpl.
Qed.
Lemma setCR3_exist:
∀ habd habd´ labd id ofs f,
setCR30_spec habd (GLOBP id ofs) = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, setCR3_spec labd (GLOBP id ofs) = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold setCR30_spec, setCR3_spec; intros until f; exist_simpl.
Qed.
Lemma trapout_exist:
∀ habd habd´ labd f,
trapout0_spec habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, trapout´_spec labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold trapout0_spec, trapout´_spec; intros until f; exist_simpl.
Qed.
Lemma hostout_exist:
∀ habd habd´ labd f,
hostout_spec habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, hostout´_spec labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold hostout_spec, hostout´_spec; intros until f; exist_simpl.
Qed.
End Exists.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) malinit_passthrough mcontainer.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply flatmem_copy´_sim.
- apply vmxinfo_get_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit setPG_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
match_external_states_simpl. congruence.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
inv_val_inject.
eapply inject_forward_equal´ in H8; eauto 1. inv H8.
exploit setCR3_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
match_external_states_simpl.
rewrite Int.add_zero; eauto. congruence.
- apply container_init_sim.
- apply container_get_parent_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply container_split_sim.
- apply container_alloc_sim.
- apply cli_sim.
- apply sti_sim.
- apply cons_buf_read_sim.
- apply serial_putc_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply trapin_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
inv H4. inv match_extcall_states.
exploit trapout_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
inv match_match. match_external_states_simpl. congruence.
- apply hostin_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
inv H4. inv match_extcall_states.
exploit hostout_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
inv match_match. match_external_states_simpl. congruence.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End WITHMEM.
End Refinement.
Lemma setPG_exist:
∀ habd habd´ labd f,
setPG0_spec habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, setPG_spec labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold setPG0_spec, setPG_spec; intros until f; exist_simpl.
Qed.
Lemma setCR3_exist:
∀ habd habd´ labd id ofs f,
setCR30_spec habd (GLOBP id ofs) = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, setCR3_spec labd (GLOBP id ofs) = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold setCR30_spec, setCR3_spec; intros until f; exist_simpl.
Qed.
Lemma trapout_exist:
∀ habd habd´ labd f,
trapout0_spec habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, trapout´_spec labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold trapout0_spec, trapout´_spec; intros until f; exist_simpl.
Qed.
Lemma hostout_exist:
∀ habd habd´ labd f,
hostout_spec habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, hostout´_spec labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ AT habd´ = AT habd ∧ nps habd´ = nps habd.
Proof.
unfold hostout_spec, hostout´_spec; intros until f; exist_simpl.
Qed.
End Exists.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) malinit_passthrough mcontainer.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply flatmem_copy´_sim.
- apply vmxinfo_get_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit setPG_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
match_external_states_simpl. congruence.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
inv_val_inject.
eapply inject_forward_equal´ in H8; eauto 1. inv H8.
exploit setCR3_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
match_external_states_simpl.
rewrite Int.add_zero; eauto. congruence.
- apply container_init_sim.
- apply container_get_parent_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply container_split_sim.
- apply container_alloc_sim.
- apply cli_sim.
- apply sti_sim.
- apply cons_buf_read_sim.
- apply serial_putc_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply trapin_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
inv H4. inv match_extcall_states.
exploit trapout_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
inv match_match. match_external_states_simpl. congruence.
- apply hostin_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
inv H4. inv match_extcall_states.
exploit hostout_exist; eauto 1; intros [labd´ [HP [HM[HAT HN]]]].
inv match_match. match_external_states_simpl. congruence.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End WITHMEM.
End Refinement.