Library mcertikos.mm.ALInitGenPassthrough
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Section Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section Exists.
Lemma setPG_exist:
∀ habd habd´ labd (s: stencil) f,
setPG0_spec habd = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, setPG_spec labd = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC 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 (s: stencil) f,
setCR30_spec habd (GLOBP id ofs) = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, setCR3_spec labd (GLOBP id ofs) = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold setCR30_spec, setCR3_spec; intros until f; exist_simpl.
Qed.
Lemma trapout_exist:
∀ habd habd´ labd (s: stencil) f,
trapout0_spec habd = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, trapout´_spec labd = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold trapout0_spec, trapout´_spec; intros until f; exist_simpl.
Qed.
Lemma hostout_exist:
∀ habd habd´ labd (s: stencil) f,
hostout_spec habd = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, hostout´_spec labd = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold hostout_spec, hostout´_spec; intros until f; exist_simpl.
Qed.
Import CalTicketLock.
Lemma relate_AT_Log_Pool_base:
∀ s habd labd,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log_pb O (multi_log habd)) (real_multi_log_pb O (multi_log labd)).
simpl. auto.
Qed.
Lemma relate_AT_Log_Pool_step:
∀ s habd labd x,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log_pb x (multi_log habd)) (real_multi_log_pb x (multi_log labd)) →
relate_AT_Log_Pool s (real_multi_log_pb (S x) (multi_log habd)) (real_multi_log_pb (S x) (multi_log labd)).
Proof.
simpl. intros. econstructor.
- intros.
remember (Z.of_nat x) as nx.
assert (Hr: r = nx ∨ r ≠ nx) by omega. destruct Hr.
+ rewrite H3.
repeat erewrite ZMap.gss; reflexivity.
+ repeat (erewrite ZMap.gso; [|eassumption]).
inv H0. exploit H4. eapply H1. eapply H2. auto.
- inv H0. assert (Hx: (Z.of_nat x) = 0 ∨ (Z.of_nat x) ≠ 0) by omega. destruct Hx.
+ rewrite H0. simpl. repeat erewrite ZMap.gss. econstructor. econstructor.
+ repeat (erewrite ZMap.gso; [| congruence]). eassumption.
Qed.
Lemma relate_AT_Log_Pool_induction:
∀ s habd labd range,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log_pb range (multi_log habd))
(real_multi_log_pb range (multi_log labd)).
Proof.
intros. induction range.
eapply relate_AT_Log_Pool_base; eauto.
eapply relate_AT_Log_Pool_step; eauto.
Qed.
Lemma real_relate_AT_Log_Pool:
∀ s habd labd,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log (multi_log habd)) (real_multi_log (multi_log labd)).
Proof.
intros.
unfold real_multi_log.
eapply relate_AT_Log_Pool_induction; eauto.
Qed.
Lemma container_init_exist:
∀ s habd habd´ labd mbi f,
container_init_spec mbi habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, container_init_spec mbi labd = Some labd´
∧ relate_AbData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold container_init_spec; intros until f; exist_simpl.
eapply real_relate_AT_Log_Pool; eauto.
Qed.
Lemma container_init_sim:
∀ id,
sim (crel RData RData)
(id ↦ gensem (container_init_spec))
(id ↦ gensem (container_init_spec)).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit container_init_exist; eauto 1; intros (labd´ & HP & HM & HAT & HATC´ & HN).
match_external_states_simpl.
congruence.
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.
Section ACQUIRE_SIM.
Lemma Shared2ID_imply:
∀ i p,
Shared2ID1 i = Some p →
Shared2ID0 i = Some p.
Proof.
intros. functional inversion H; trivial.
Qed.
Lemma Shared2ID1_id:
∀ i p,
Shared2ID1 i = Some p →
p ≠ AT_LOC.
Proof.
intros. functional inversion H; red; intros HF; inv HF.
Qed.
Lemma Shared2ID1_neq:
∀ i p,
Shared2ID1 i = Some p →
i ≠ 0.
Proof.
intros. functional inversion H; red; intros HF; inv HF.
Qed.
Lemma acquire_lock_exist:
∀ s i ofs bound habd habd´ labd f p l,
acquire_lock_spec1 bound i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_lock_spec0 bound i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ Shared2ID1 i = Some p.
Proof.
unfold acquire_lock_spec; intros.
inv H0. revert H; subrewrite. subdestruct.
- inv HQ.
erewrite Shared2ID_imply; eauto.
subrewrite´.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq. rewrite <- Heq.
rewrite Hdestruct4.
pose proof multi_oracle_re as multi_oracle_re´.
inv multi_oracle_re. exploit H1; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq´. rewrite <- Heq´.
rewrite Hdestruct5.
refine_split´; trivial.
econstructor; eauto. simpl.
inv multi_log_re´.
econstructor; eauto.
+ intros. exploit H3; eauto.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss.
intros Heq1. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_match:
∀ s bound i ofs d d´ m f p l,
acquire_lock_spec1 bound i ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_spec; intros. subdestruct.
- inv H. inv H0. econstructor; eauto.
Qed.
Require Import LAsmModuleSemAux.
Lemma acquire_lock_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec1))
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec0)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
simpl. eapply Hst.
econstructor; eauto ; try congruence.
-
eapply storebytes_match_correct; eauto.
eapply acquire_lock_match; eauto.
intros.
assert (HMatch: ∀ i, In i new_glbl → CheckID1 i = false).
{
intros. inv H1. trivial. inv H2. trivial. inv H1. trivial. inv H2.
}
exploit HMatch; eauto. intros.
destruct (peq i id0).
+ subst. eapply Shared2ID_valid1 in HS. congruence.
+ red; intros; subst. elim n.
eapply (genv_vars_inj s i id0); eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_storebytes_2; eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
simpl. trivial.
econstructor; eauto ; try congruence.
-
eapply acquire_lock_match; eauto.
-
subst rs´. val_inject_simpl.
}
Qed.
End ACQUIRE_SIM.
Section RELEASE_SIM.
Lemma release_lock_exist:
∀ s i ofs e habd habd´ labd f,
release_lock_spec1 i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ (∃ labd´, release_lock_spec0 i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´).
Proof.
unfold release_lock_spec; intros.
inv H0. revert H; subrewrite. subdestruct.
- inv HQ.
erewrite Shared2ID_imply; eauto.
subrewrite´.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq. rewrite <- Heq.
rewrite Hdestruct3.
rewrite Hdestruct4.
refine_split´; trivial.
econstructor; eauto.
simpl.
inv multi_log_re´.
econstructor; eauto.
+ intros. exploit H1; eauto.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss.
intros Heq1. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma release_lock_match:
∀ s i ofs e d d´ m f,
release_lock_spec1 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_spec; intros. subdestruct.
- inv H. inv H0. econstructor; eauto.
Qed.
Require Import LAsmModuleSemAux.
Lemma release_lock_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_release_lock_compatsem release_lock (release_lock_spec1))
(id ↦ primcall_release_lock_compatsem release_lock (release_lock_spec0)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- econstructor; eauto.
econstructor; eauto.
+ eapply release_lock_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End RELEASE_SIM.
Section PAGE_COPY_SIM.
Lemma page_copy´_exist:
∀ s habd habd´ labd index i from f,
page_copy´_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy´_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy´_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
intros Heq. rewrite <- Heq.
rewrite Hdestruct5.
exploit page_copy_aux_exists; eauto.
intros.
rewrite H2.
rewrite Hdestruct9.
refine_split´; try trivial.
econstructor; simpl; auto.
rewrite ikern_re; auto.
rewrite ihost_re; auto.
inv multi_log_re´.
econstructor; eauto.
+ intros. exploit H3; eauto.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss.
intros Heq1. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy´_match:
∀ s d d´ m index i from f,
page_copy´_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy´_spec; intros.
subdestruct.
inv H. inv H0.
econstructor; eauto.
Qed.
Lemma page_copy´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy´_spec)
(id ↦ gensem page_copy´_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy´_exist; eauto 1.
exploit page_copy´_match; eauto 1.
intros.
destruct H5 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Lemma page_copy_back´_exist:
∀ s habd habd´ labd index i to f,
page_copy_back´_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back´_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back´_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
intros Heq. rewrite <- Heq.
rewrite Hdestruct5.
rewrite Hdestruct6.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & H2 & H3).
rewrite H2.
refine_split´; eauto.
econstructor; simpl; auto.
rewrite ikern_re; auto.
rewrite ihost_re; auto.
Qed.
Lemma page_copy_back´_match:
∀ s d d´ m index i to f,
page_copy_back´_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back´_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_back´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back´_spec)
(id ↦ gensem page_copy_back´_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy_back´_exist; eauto 1.
exploit page_copy_back´_match; eauto 1.
intros.
destruct H5 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End PAGE_COPY_BACK_SIM.
Lemma passthrough_correct:
sim (crel HDATA LDATA) malinit_passthrough mcontainer.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´_sim.
- apply page_copy_back´_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 & HATC´ & 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 & HATC´ & HN).
match_external_states_simpl.
rewrite Int.add_zero; eauto. congruence.
- apply container_init_sim.
- apply container_get_parent_sim.
- apply container_get_nchildren_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 get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply release_lock_sim.
-
eapply acquire_lock_sim; eauto.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_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 & HATC´ & 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 & HATC´ & HN).
inv match_match. match_external_states_simpl. congruence.
- apply proc_create_postinit_sim.
- 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 (s: stencil) f,
setPG0_spec habd = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, setPG_spec labd = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC 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 (s: stencil) f,
setCR30_spec habd (GLOBP id ofs) = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, setCR3_spec labd (GLOBP id ofs) = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold setCR30_spec, setCR3_spec; intros until f; exist_simpl.
Qed.
Lemma trapout_exist:
∀ habd habd´ labd (s: stencil) f,
trapout0_spec habd = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, trapout´_spec labd = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold trapout0_spec, trapout´_spec; intros until f; exist_simpl.
Qed.
Lemma hostout_exist:
∀ habd habd´ labd (s: stencil) f,
hostout_spec habd = Some habd´
→ relate_RData s f habd labd
→ ∃ labd´, hostout´_spec labd = Some labd´ ∧ relate_RData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold hostout_spec, hostout´_spec; intros until f; exist_simpl.
Qed.
Import CalTicketLock.
Lemma relate_AT_Log_Pool_base:
∀ s habd labd,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log_pb O (multi_log habd)) (real_multi_log_pb O (multi_log labd)).
simpl. auto.
Qed.
Lemma relate_AT_Log_Pool_step:
∀ s habd labd x,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log_pb x (multi_log habd)) (real_multi_log_pb x (multi_log labd)) →
relate_AT_Log_Pool s (real_multi_log_pb (S x) (multi_log habd)) (real_multi_log_pb (S x) (multi_log labd)).
Proof.
simpl. intros. econstructor.
- intros.
remember (Z.of_nat x) as nx.
assert (Hr: r = nx ∨ r ≠ nx) by omega. destruct Hr.
+ rewrite H3.
repeat erewrite ZMap.gss; reflexivity.
+ repeat (erewrite ZMap.gso; [|eassumption]).
inv H0. exploit H4. eapply H1. eapply H2. auto.
- inv H0. assert (Hx: (Z.of_nat x) = 0 ∨ (Z.of_nat x) ≠ 0) by omega. destruct Hx.
+ rewrite H0. simpl. repeat erewrite ZMap.gss. econstructor. econstructor.
+ repeat (erewrite ZMap.gso; [| congruence]). eassumption.
Qed.
Lemma relate_AT_Log_Pool_induction:
∀ s habd labd range,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log_pb range (multi_log habd))
(real_multi_log_pb range (multi_log labd)).
Proof.
intros. induction range.
eapply relate_AT_Log_Pool_base; eauto.
eapply relate_AT_Log_Pool_step; eauto.
Qed.
Lemma real_relate_AT_Log_Pool:
∀ s habd labd,
relate_AT_Log_Pool s (multi_log habd) (multi_log labd) →
relate_AT_Log_Pool s (real_multi_log (multi_log habd)) (real_multi_log (multi_log labd)).
Proof.
intros.
unfold real_multi_log.
eapply relate_AT_Log_Pool_induction; eauto.
Qed.
Lemma container_init_exist:
∀ s habd habd´ labd mbi f,
container_init_spec mbi habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, container_init_spec mbi labd = Some labd´
∧ relate_AbData s f habd´ labd´
∧ AT habd´ = AT habd ∧ ATC habd´ = ATC habd
∧ nps habd´ = nps habd.
Proof.
unfold container_init_spec; intros until f; exist_simpl.
eapply real_relate_AT_Log_Pool; eauto.
Qed.
Lemma container_init_sim:
∀ id,
sim (crel RData RData)
(id ↦ gensem (container_init_spec))
(id ↦ gensem (container_init_spec)).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit container_init_exist; eauto 1; intros (labd´ & HP & HM & HAT & HATC´ & HN).
match_external_states_simpl.
congruence.
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.
Section ACQUIRE_SIM.
Lemma Shared2ID_imply:
∀ i p,
Shared2ID1 i = Some p →
Shared2ID0 i = Some p.
Proof.
intros. functional inversion H; trivial.
Qed.
Lemma Shared2ID1_id:
∀ i p,
Shared2ID1 i = Some p →
p ≠ AT_LOC.
Proof.
intros. functional inversion H; red; intros HF; inv HF.
Qed.
Lemma Shared2ID1_neq:
∀ i p,
Shared2ID1 i = Some p →
i ≠ 0.
Proof.
intros. functional inversion H; red; intros HF; inv HF.
Qed.
Lemma acquire_lock_exist:
∀ s i ofs bound habd habd´ labd f p l,
acquire_lock_spec1 bound i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_lock_spec0 bound i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ Shared2ID1 i = Some p.
Proof.
unfold acquire_lock_spec; intros.
inv H0. revert H; subrewrite. subdestruct.
- inv HQ.
erewrite Shared2ID_imply; eauto.
subrewrite´.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq. rewrite <- Heq.
rewrite Hdestruct4.
pose proof multi_oracle_re as multi_oracle_re´.
inv multi_oracle_re. exploit H1; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq´. rewrite <- Heq´.
rewrite Hdestruct5.
refine_split´; trivial.
econstructor; eauto. simpl.
inv multi_log_re´.
econstructor; eauto.
+ intros. exploit H3; eauto.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss.
intros Heq1. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_match:
∀ s bound i ofs d d´ m f p l,
acquire_lock_spec1 bound i ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_spec; intros. subdestruct.
- inv H. inv H0. econstructor; eauto.
Qed.
Require Import LAsmModuleSemAux.
Lemma acquire_lock_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec1))
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec0)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
simpl. eapply Hst.
econstructor; eauto ; try congruence.
-
eapply storebytes_match_correct; eauto.
eapply acquire_lock_match; eauto.
intros.
assert (HMatch: ∀ i, In i new_glbl → CheckID1 i = false).
{
intros. inv H1. trivial. inv H2. trivial. inv H1. trivial. inv H2.
}
exploit HMatch; eauto. intros.
destruct (peq i id0).
+ subst. eapply Shared2ID_valid1 in HS. congruence.
+ red; intros; subst. elim n.
eapply (genv_vars_inj s i id0); eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_storebytes_2; eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
simpl. trivial.
econstructor; eauto ; try congruence.
-
eapply acquire_lock_match; eauto.
-
subst rs´. val_inject_simpl.
}
Qed.
End ACQUIRE_SIM.
Section RELEASE_SIM.
Lemma release_lock_exist:
∀ s i ofs e habd habd´ labd f,
release_lock_spec1 i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ (∃ labd´, release_lock_spec0 i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´).
Proof.
unfold release_lock_spec; intros.
inv H0. revert H; subrewrite. subdestruct.
- inv HQ.
erewrite Shared2ID_imply; eauto.
subrewrite´.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
intros Heq. rewrite <- Heq.
rewrite Hdestruct3.
rewrite Hdestruct4.
refine_split´; trivial.
econstructor; eauto.
simpl.
inv multi_log_re´.
econstructor; eauto.
+ intros. exploit H1; eauto.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss.
intros Heq1. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma release_lock_match:
∀ s i ofs e d d´ m f,
release_lock_spec1 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_spec; intros. subdestruct.
- inv H. inv H0. econstructor; eauto.
Qed.
Require Import LAsmModuleSemAux.
Lemma release_lock_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_release_lock_compatsem release_lock (release_lock_spec1))
(id ↦ primcall_release_lock_compatsem release_lock (release_lock_spec0)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- econstructor; eauto.
econstructor; eauto.
+ eapply release_lock_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End RELEASE_SIM.
Section PAGE_COPY_SIM.
Lemma page_copy´_exist:
∀ s habd habd´ labd index i from f,
page_copy´_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy´_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy´_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
intros Heq. rewrite <- Heq.
rewrite Hdestruct5.
exploit page_copy_aux_exists; eauto.
intros.
rewrite H2.
rewrite Hdestruct9.
refine_split´; try trivial.
econstructor; simpl; auto.
rewrite ikern_re; auto.
rewrite ihost_re; auto.
inv multi_log_re´.
econstructor; eauto.
+ intros. exploit H3; eauto.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss.
intros Heq1. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq´: z ≠ 0).
{
eapply index2Z_neq; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy´_match:
∀ s d d´ m index i from f,
page_copy´_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy´_spec; intros.
subdestruct.
inv H. inv H0.
econstructor; eauto.
Qed.
Lemma page_copy´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy´_spec)
(id ↦ gensem page_copy´_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy´_exist; eauto 1.
exploit page_copy´_match; eauto 1.
intros.
destruct H5 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Lemma page_copy_back´_exist:
∀ s habd habd´ labd index i to f,
page_copy_back´_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back´_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back´_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. exploit H; eauto.
eapply Shared2ID1_neq; eauto.
reflexivity.
intros Heq. rewrite <- Heq.
rewrite Hdestruct5.
rewrite Hdestruct6.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & H2 & H3).
rewrite H2.
refine_split´; eauto.
econstructor; simpl; auto.
rewrite ikern_re; auto.
rewrite ihost_re; auto.
Qed.
Lemma page_copy_back´_match:
∀ s d d´ m index i to f,
page_copy_back´_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back´_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_back´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back´_spec)
(id ↦ gensem page_copy_back´_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy_back´_exist; eauto 1.
exploit page_copy_back´_match; eauto 1.
intros.
destruct H5 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End PAGE_COPY_BACK_SIM.
Lemma passthrough_correct:
sim (crel HDATA LDATA) malinit_passthrough mcontainer.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´_sim.
- apply page_copy_back´_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 & HATC´ & 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 & HATC´ & HN).
match_external_states_simpl.
rewrite Int.add_zero; eauto. congruence.
- apply container_init_sim.
- apply container_get_parent_sim.
- apply container_get_nchildren_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 get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply release_lock_sim.
-
eapply acquire_lock_sim; eauto.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_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 & HATC´ & 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 & HATC´ & HN).
inv match_match. match_external_states_simpl. congruence.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End WITHMEM.
End Refinement.