Library mcertikos.objects.ObjCPU
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Section CPU.
primitve: trap into the kernel mode from user mode
Function trapin_spec (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (false, true) ⇒ Some adt {ikern: true}
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (false, true) ⇒ Some adt {ikern: true}
| _ ⇒ None
end.
primitve: return to the user mode from kernel mode
Function trapout´_spec (adt: RData): option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒ Some adt {ikern: false}
| _ ⇒ None
end.
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒ Some adt {ikern: false}
| _ ⇒ None
end.
primitve: return to the user mode from kernel mode
Function trapout0_spec (adt: RData): option RData :=
match (ikern adt, init adt, pg adt, ihost adt) with
| (true, true, true, true) ⇒ Some adt {ikern: false}
| _ ⇒ None
end.
Function trapout_spec (adt: RData): option RData :=
match (ikern adt, init adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true, false) ⇒
Some adt {ikern: false}
| _ ⇒ None
end.
match (ikern adt, init adt, pg adt, ihost adt) with
| (true, true, true, true) ⇒ Some adt {ikern: false}
| _ ⇒ None
end.
Function trapout_spec (adt: RData): option RData :=
match (ikern adt, init adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true, false) ⇒
Some adt {ikern: false}
| _ ⇒ None
end.
primitve: return to the host/kernel mode from guest/kernel mode
Function hostin_spec (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, false) ⇒ Some adt {ihost: true}
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, false) ⇒ Some adt {ihost: true}
| _ ⇒ None
end.
primitve: return to the guest/kernel mode from host/kernel mode
Function hostout´_spec (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt {ihost: false}
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt {ihost: false}
| _ ⇒ None
end.
primitve: return to the guest/kernel mode from host/kernel mode
Function hostout_spec (adt: RData): option RData :=
match (ikern adt, init adt, pg adt, ihost adt) with
| (true, true, true, true) ⇒ Some adt {ihost: false}
| _ ⇒ None
end.
Definition trap_info_get_spec (adt: RData): int := fst (ti adt).
Definition trap_info_ret_spec (adt: RData): val := snd (ti adt).
Function trapinfo_set (adt: RData) (addr: int) (ra: val) : RData := adt {ti: (addr, ra)}.
match (ikern adt, init adt, pg adt, ihost adt) with
| (true, true, true, true) ⇒ Some adt {ihost: false}
| _ ⇒ None
end.
Definition trap_info_get_spec (adt: RData): int := fst (ti adt).
Definition trap_info_ret_spec (adt: RData): val := snd (ti adt).
Function trapinfo_set (adt: RData) (addr: int) (ra: val) : RData := adt {ti: (addr, ra)}.
primitve: set the pointer to the page table
Function setCR3_spec (adt: RData) (cr3: globalpointer): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt {CR3: cr3}
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt {CR3: cr3}
| _ ⇒ None
end.
primitve: set the pointer to the page table
Function setCR30_spec (adt: RData) (cr3: globalpointer): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if CR3_valid_dec cr3 then Some adt {CR3: cr3}
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒
if CR3_valid_dec cr3 then Some adt {CR3: cr3}
else None
| _ ⇒ None
end.
primitve: enable the paging mechanism
Function setPG_spec (adt: RData): option RData :=
match (pg adt, ikern adt, ihost adt) with
| (false, true, true) ⇒ Some adt {pg: true}
| _ ⇒ None
end.
Function setPG0_spec (adt: RData) : option RData :=
match (pg adt, ikern adt, init adt, ihost adt) with
| (false, true, true, true) ⇒
if CR3_valid_dec (CR3 adt) then Some adt {pg: true}
else None
| _ ⇒ None
end.
Function setPG1_spec (adt: RData) : option RData :=
match (pg adt, ikern adt, init adt, ihost adt, ipt adt) with
| (false, true, true, true, true) ⇒
if zle_lt 0 (PT adt) num_proc then
if PMap_valid_dec (ZMap.get (PT adt) (ptpool adt)) then
if PMap_kern_dec (ZMap.get (PT adt) (ptpool adt)) then
Some adt {pg: true}
else None
else None
else None
| _ ⇒ None
end.
Function vmxinfo_get_spec (i: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
Some (ZMap.get i (vmxinfo adt))
| _ ⇒ None
end.
Function proc_create_postinit_spec (elf_id: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
Some adt
| _ ⇒ None
end.
End CPU.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section CPU_SIM.
Context {re1: relate_impl_iflags}.
Context {re2´: relate_impl_vmxinfo}.
Section vmxinfo_get_SIM.
Lemma vmxinfo_get_exist:
∀ s i habd labd v f,
vmxinfo_get_spec i habd = Some v
→ relate_AbData s f habd labd
→ vmxinfo_get_spec i labd = Some v.
Proof.
unfold vmxinfo_get_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_vmxinfo_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma vmxinfo_get_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmxinfo_get_spec)
(id ↦ gensem vmxinfo_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite vmxinfo_get_exist; eauto 1. trivial.
Qed.
End vmxinfo_get_SIM.
Context {mt1: match_impl_iflags}.
Section SETPG_SIM.
Lemma setPG_exist:
∀ s habd habd´ labd f,
setPG_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPG_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPG_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_pg_update. assumption.
Qed.
Lemma setPG_match:
∀ s d d´ m f,
setPG_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPG_spec; intros. subdestruct.
inv H. eapply match_impl_pg_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPG_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPG_spec}.
Lemma setPG_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPG_spec)
(id ↦ gensem setPG_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPG_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPG_match; eauto.
Qed.
End SETPG_SIM.
Section SETPG0_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_CR3}.
Lemma setPG0_exist:
∀ s habd habd´ labd f,
setPG0_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPG0_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPG0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_CR3_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_pg_update. assumption.
Qed.
Lemma setPG0_match:
∀ s d d´ m f,
setPG0_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPG0_spec; intros. subdestruct.
inv H. eapply match_impl_pg_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPG0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPG0_spec}.
Lemma setPG0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPG0_spec)
(id ↦ gensem setPG0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPG0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPG0_match; eauto.
Qed.
End SETPG0_SIM.
Section SETPG1_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_PT}.
Context {re4: relate_impl_ipt}.
Context {re5: relate_impl_ptpool}.
Lemma setPG1_exist:
∀ s habd habd´ labd f,
setPG1_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPG1_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPG1_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_PT_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_pg_update. assumption.
Qed.
Lemma setPG1_match:
∀ s d d´ m f,
setPG1_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPG1_spec; intros. subdestruct.
inv H. eapply match_impl_pg_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPG1_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPG1_spec}.
Lemma setPG1_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPG1_spec)
(id ↦ gensem setPG1_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPG1_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPG1_match; eauto.
Qed.
End SETPG1_SIM.
Section SETCR3_SIM.
Context {re2: relate_impl_CR3}.
Context {mt2: match_impl_CR3}.
Lemma setCR3_exist:
∀ s habd habd´ labd id ofs f,
setCR3_spec habd (GLOBP id ofs) = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setCR3_spec labd (GLOBP id ofs) = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold setCR3_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_CR3_update. assumption.
Qed.
Lemma setCR3_match:
∀ s d d´ m id ofs f,
setCR3_spec d (GLOBP id ofs) = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setCR3_spec; intros. subdestruct.
inv H. eapply match_impl_CR3_update. assumption.
Qed.
Context {inv: SetCR3Invariants (data_ops:= data_ops) setCR3_spec}.
Context {inv0: SetCR3Invariants (data_ops:= data_ops0) setCR3_spec}.
Lemma setCR3_sim :
∀ id,
sim (crel RData RData) (id ↦ setCR3_compatsem setCR3_spec)
(id ↦ setCR3_compatsem setCR3_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv_val_inject.
eapply inject_forward_equal´ in H2; eauto 1. inv H2.
exploit setCR3_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
rewrite Int.add_zero. eauto.
eapply setCR3_match; eauto.
Qed.
End SETCR3_SIM.
Section SETCR30_SIM.
Context {re2: relate_impl_CR3}.
Context {mt2: match_impl_CR3}.
Lemma setCR30_exist:
∀ s habd habd´ labd id ofs f,
setCR30_spec habd (GLOBP id ofs) = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setCR30_spec labd (GLOBP id ofs) = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold setCR30_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CR3_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_CR3_update. assumption.
Qed.
Lemma setCR30_match:
∀ s d d´ m id ofs f,
setCR30_spec d (GLOBP id ofs) = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setCR30_spec; intros. subdestruct.
inv H. eapply match_impl_CR3_update. assumption.
Qed.
Context {inv: SetCR3Invariants (data_ops:= data_ops) setCR30_spec}.
Context {inv0: SetCR3Invariants (data_ops:= data_ops0) setCR30_spec}.
Lemma setCR30_sim :
∀ id,
sim (crel RData RData) (id ↦ setCR3_compatsem setCR30_spec)
(id ↦ setCR3_compatsem setCR30_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv_val_inject.
eapply inject_forward_equal´ in H2; eauto 1. inv H2.
exploit setCR30_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
rewrite Int.add_zero. eauto.
eapply setCR30_match; eauto.
Qed.
End SETCR30_SIM.
Section TRAPIN_SIM.
Lemma trapin_exist:
∀ s habd habd´ labd f,
trapin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapin_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapin_match:
∀ s d d´ m f,
trapin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapin_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapin_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) trapin_spec}.
Lemma trapin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapin_spec)
(id ↦ primcall_general_compatsem trapin_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapin_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapin_match; eauto.
Qed.
End TRAPIN_SIM.
Section TRAPOUT´_SIM.
Lemma trapout´_exist:
∀ s habd habd´ labd f,
trapout´_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapout´_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapout´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapout´_match:
∀ s d d´ m f,
trapout´_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapout´_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapout´_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) trapout´_spec}.
Lemma trapout´_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapout´_spec)
(id ↦ primcall_general_compatsem trapout´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapout´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapout´_match; eauto.
Qed.
End TRAPOUT´_SIM.
Section TRAPOUT0_SIM.
Context {re2: relate_impl_init}.
Lemma trapout0_exist:
∀ s habd habd´ labd f,
trapout0_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapout0_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapout0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapout0_match:
∀ s d d´ m f,
trapout0_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapout0_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapout0_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) trapout0_spec}.
Lemma trapout0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapout0_spec)
(id ↦ primcall_general_compatsem trapout0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapout0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapout0_match; eauto.
Qed.
End TRAPOUT0_SIM.
Section TRAPOUT_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_ipt}.
Lemma trapout_exist:
∀ s habd habd´ labd f,
trapout_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapout_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapout_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_ipt_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapout_match:
∀ s d d´ m f,
trapout_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapout_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapout_spec}.
Context `{inv1: PrimInvariants RData (data_ops:= data_ops0) trapout_spec}.
Lemma trapout_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapout_spec)
(id ↦ primcall_general_compatsem trapout_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapout_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapout_match; eauto.
Qed.
End TRAPOUT_SIM.
Section HOSTIN_SIM.
Lemma hostin_exist:
∀ s habd habd´ labd f,
hostin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, hostin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold hostin_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ihost_update. assumption.
Qed.
Lemma hostin_match:
∀ s d d´ m f,
hostin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold hostin_spec; intros. subdestruct.
inv H. eapply match_impl_ihost_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) hostin_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) hostin_spec}.
Lemma hostin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem hostin_spec)
(id ↦ primcall_general_compatsem hostin_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit hostin_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply hostin_match; eauto.
Qed.
End HOSTIN_SIM.
Section HOSTOUT´_SIM.
Lemma hostout´_exist:
∀ s habd habd´ labd f,
hostout´_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, hostout´_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold hostout´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ihost_update. assumption.
Qed.
Lemma hostout´_match:
∀ s d d´ m f,
hostout´_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold hostout´_spec; intros. subdestruct.
inv H. eapply match_impl_ihost_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) hostout´_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) hostout´_spec}.
Lemma hostout´_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem hostout´_spec)
(id ↦ primcall_general_compatsem hostout´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit hostout´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply hostout´_match; eauto.
Qed.
End HOSTOUT´_SIM.
Section HOSTOUT_SIM.
Context {re2: relate_impl_init}.
Lemma hostout_exist:
∀ s habd habd´ labd f,
hostout_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, hostout_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold hostout_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ihost_update. assumption.
Qed.
Lemma hostout_match:
∀ s d d´ m f,
hostout_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold hostout_spec; intros. subdestruct.
inv H. eapply match_impl_ihost_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) hostout_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) hostout_spec}.
Lemma hostout_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem hostout_spec)
(id ↦ primcall_general_compatsem hostout_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit hostout_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply hostout_match; eauto.
Qed.
End HOSTOUT_SIM.
Section PROC_CREATE_POSTINIT_SIM.
Context {re2: relate_impl_init}.
Lemma proc_create_postinit_exist:
∀ s habd habd´ labd f elf_id,
proc_create_postinit_spec elf_id habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, proc_create_postinit_spec elf_id labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold proc_create_postinit_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
Qed.
Lemma proc_create_postinit_match:
∀ s d d´ m f elf_id,
proc_create_postinit_spec elf_id d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold proc_create_postinit_spec; intros. subdestruct.
inv H. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) proc_create_postinit_spec}.
Context {inv0: PreservesInvariants (HD:= data0) proc_create_postinit_spec}.
Lemma proc_create_postinit_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem proc_create_postinit_spec)
(id ↦ gensem proc_create_postinit_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit proc_create_postinit_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply proc_create_postinit_match; eauto.
Qed.
End PROC_CREATE_POSTINIT_SIM.
End CPU_SIM.
Section TRAP_INFO_SIM.
Context {re1: relate_impl_trapinfo}.
Lemma trap_info_get_exist:
∀ habd labd s z f,
trap_info_get_spec habd = z
→ relate_AbData s f habd labd
→ trap_info_get_spec labd = z.
Proof.
unfold trap_info_get_spec; unfold trap_info_get_spec.
intros. exploit relate_impl_trapinfo_eq; eauto.
inversion 1. congruence.
Qed.
Lemma trap_info_ret_exist:
∀ habd labd s f,
relate_AbData s f habd labd
→ val_inject f (trap_info_ret_spec habd) (trap_info_ret_spec labd).
Proof.
intros. exploit relate_impl_trapinfo_eq; eauto.
inversion 1. assumption.
Qed.
Lemma trap_info_get_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_get_compatsem trap_info_get_spec)
(id ↦ primcall_trap_info_get_compatsem trap_info_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
match_external_states_simpl.
erewrite (trap_info_get_exist d1´ d2); eauto.
Qed.
Context {low1: low_level_invariant_impl}.
Lemma trap_info_ret_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec)
(id ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl.
eapply trap_info_ret_exist; eauto.
Qed.
End TRAP_INFO_SIM.
End OBJ_SIM.
match (pg adt, ikern adt, ihost adt) with
| (false, true, true) ⇒ Some adt {pg: true}
| _ ⇒ None
end.
Function setPG0_spec (adt: RData) : option RData :=
match (pg adt, ikern adt, init adt, ihost adt) with
| (false, true, true, true) ⇒
if CR3_valid_dec (CR3 adt) then Some adt {pg: true}
else None
| _ ⇒ None
end.
Function setPG1_spec (adt: RData) : option RData :=
match (pg adt, ikern adt, init adt, ihost adt, ipt adt) with
| (false, true, true, true, true) ⇒
if zle_lt 0 (PT adt) num_proc then
if PMap_valid_dec (ZMap.get (PT adt) (ptpool adt)) then
if PMap_kern_dec (ZMap.get (PT adt) (ptpool adt)) then
Some adt {pg: true}
else None
else None
else None
| _ ⇒ None
end.
Function vmxinfo_get_spec (i: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
Some (ZMap.get i (vmxinfo adt))
| _ ⇒ None
end.
Function proc_create_postinit_spec (elf_id: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
Some adt
| _ ⇒ None
end.
End CPU.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section CPU_SIM.
Context {re1: relate_impl_iflags}.
Context {re2´: relate_impl_vmxinfo}.
Section vmxinfo_get_SIM.
Lemma vmxinfo_get_exist:
∀ s i habd labd v f,
vmxinfo_get_spec i habd = Some v
→ relate_AbData s f habd labd
→ vmxinfo_get_spec i labd = Some v.
Proof.
unfold vmxinfo_get_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_vmxinfo_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma vmxinfo_get_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmxinfo_get_spec)
(id ↦ gensem vmxinfo_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite vmxinfo_get_exist; eauto 1. trivial.
Qed.
End vmxinfo_get_SIM.
Context {mt1: match_impl_iflags}.
Section SETPG_SIM.
Lemma setPG_exist:
∀ s habd habd´ labd f,
setPG_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPG_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPG_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_pg_update. assumption.
Qed.
Lemma setPG_match:
∀ s d d´ m f,
setPG_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPG_spec; intros. subdestruct.
inv H. eapply match_impl_pg_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPG_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPG_spec}.
Lemma setPG_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPG_spec)
(id ↦ gensem setPG_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPG_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPG_match; eauto.
Qed.
End SETPG_SIM.
Section SETPG0_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_CR3}.
Lemma setPG0_exist:
∀ s habd habd´ labd f,
setPG0_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPG0_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPG0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_CR3_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_pg_update. assumption.
Qed.
Lemma setPG0_match:
∀ s d d´ m f,
setPG0_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPG0_spec; intros. subdestruct.
inv H. eapply match_impl_pg_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPG0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPG0_spec}.
Lemma setPG0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPG0_spec)
(id ↦ gensem setPG0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPG0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPG0_match; eauto.
Qed.
End SETPG0_SIM.
Section SETPG1_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_PT}.
Context {re4: relate_impl_ipt}.
Context {re5: relate_impl_ptpool}.
Lemma setPG1_exist:
∀ s habd habd´ labd f,
setPG1_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPG1_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPG1_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_PT_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_pg_update. assumption.
Qed.
Lemma setPG1_match:
∀ s d d´ m f,
setPG1_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPG1_spec; intros. subdestruct.
inv H. eapply match_impl_pg_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPG1_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPG1_spec}.
Lemma setPG1_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPG1_spec)
(id ↦ gensem setPG1_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPG1_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPG1_match; eauto.
Qed.
End SETPG1_SIM.
Section SETCR3_SIM.
Context {re2: relate_impl_CR3}.
Context {mt2: match_impl_CR3}.
Lemma setCR3_exist:
∀ s habd habd´ labd id ofs f,
setCR3_spec habd (GLOBP id ofs) = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setCR3_spec labd (GLOBP id ofs) = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold setCR3_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_CR3_update. assumption.
Qed.
Lemma setCR3_match:
∀ s d d´ m id ofs f,
setCR3_spec d (GLOBP id ofs) = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setCR3_spec; intros. subdestruct.
inv H. eapply match_impl_CR3_update. assumption.
Qed.
Context {inv: SetCR3Invariants (data_ops:= data_ops) setCR3_spec}.
Context {inv0: SetCR3Invariants (data_ops:= data_ops0) setCR3_spec}.
Lemma setCR3_sim :
∀ id,
sim (crel RData RData) (id ↦ setCR3_compatsem setCR3_spec)
(id ↦ setCR3_compatsem setCR3_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv_val_inject.
eapply inject_forward_equal´ in H2; eauto 1. inv H2.
exploit setCR3_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
rewrite Int.add_zero. eauto.
eapply setCR3_match; eauto.
Qed.
End SETCR3_SIM.
Section SETCR30_SIM.
Context {re2: relate_impl_CR3}.
Context {mt2: match_impl_CR3}.
Lemma setCR30_exist:
∀ s habd habd´ labd id ofs f,
setCR30_spec habd (GLOBP id ofs) = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setCR30_spec labd (GLOBP id ofs) = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold setCR30_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CR3_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_CR3_update. assumption.
Qed.
Lemma setCR30_match:
∀ s d d´ m id ofs f,
setCR30_spec d (GLOBP id ofs) = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setCR30_spec; intros. subdestruct.
inv H. eapply match_impl_CR3_update. assumption.
Qed.
Context {inv: SetCR3Invariants (data_ops:= data_ops) setCR30_spec}.
Context {inv0: SetCR3Invariants (data_ops:= data_ops0) setCR30_spec}.
Lemma setCR30_sim :
∀ id,
sim (crel RData RData) (id ↦ setCR3_compatsem setCR30_spec)
(id ↦ setCR3_compatsem setCR30_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv_val_inject.
eapply inject_forward_equal´ in H2; eauto 1. inv H2.
exploit setCR30_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
rewrite Int.add_zero. eauto.
eapply setCR30_match; eauto.
Qed.
End SETCR30_SIM.
Section TRAPIN_SIM.
Lemma trapin_exist:
∀ s habd habd´ labd f,
trapin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapin_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapin_match:
∀ s d d´ m f,
trapin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapin_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapin_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) trapin_spec}.
Lemma trapin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapin_spec)
(id ↦ primcall_general_compatsem trapin_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapin_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapin_match; eauto.
Qed.
End TRAPIN_SIM.
Section TRAPOUT´_SIM.
Lemma trapout´_exist:
∀ s habd habd´ labd f,
trapout´_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapout´_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapout´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapout´_match:
∀ s d d´ m f,
trapout´_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapout´_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapout´_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) trapout´_spec}.
Lemma trapout´_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapout´_spec)
(id ↦ primcall_general_compatsem trapout´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapout´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapout´_match; eauto.
Qed.
End TRAPOUT´_SIM.
Section TRAPOUT0_SIM.
Context {re2: relate_impl_init}.
Lemma trapout0_exist:
∀ s habd habd´ labd f,
trapout0_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapout0_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapout0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapout0_match:
∀ s d d´ m f,
trapout0_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapout0_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapout0_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) trapout0_spec}.
Lemma trapout0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapout0_spec)
(id ↦ primcall_general_compatsem trapout0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapout0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapout0_match; eauto.
Qed.
End TRAPOUT0_SIM.
Section TRAPOUT_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_ipt}.
Lemma trapout_exist:
∀ s habd habd´ labd f,
trapout_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, trapout_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold trapout_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_ipt_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ikern_update. assumption.
Qed.
Lemma trapout_match:
∀ s d d´ m f,
trapout_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold trapout_spec; intros. subdestruct.
inv H. eapply match_impl_ikern_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) trapout_spec}.
Context `{inv1: PrimInvariants RData (data_ops:= data_ops0) trapout_spec}.
Lemma trapout_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem trapout_spec)
(id ↦ primcall_general_compatsem trapout_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit trapout_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply trapout_match; eauto.
Qed.
End TRAPOUT_SIM.
Section HOSTIN_SIM.
Lemma hostin_exist:
∀ s habd habd´ labd f,
hostin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, hostin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold hostin_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ihost_update. assumption.
Qed.
Lemma hostin_match:
∀ s d d´ m f,
hostin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold hostin_spec; intros. subdestruct.
inv H. eapply match_impl_ihost_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) hostin_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) hostin_spec}.
Lemma hostin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem hostin_spec)
(id ↦ primcall_general_compatsem hostin_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit hostin_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply hostin_match; eauto.
Qed.
End HOSTIN_SIM.
Section HOSTOUT´_SIM.
Lemma hostout´_exist:
∀ s habd habd´ labd f,
hostout´_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, hostout´_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold hostout´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ihost_update. assumption.
Qed.
Lemma hostout´_match:
∀ s d d´ m f,
hostout´_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold hostout´_spec; intros. subdestruct.
inv H. eapply match_impl_ihost_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) hostout´_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) hostout´_spec}.
Lemma hostout´_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem hostout´_spec)
(id ↦ primcall_general_compatsem hostout´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit hostout´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply hostout´_match; eauto.
Qed.
End HOSTOUT´_SIM.
Section HOSTOUT_SIM.
Context {re2: relate_impl_init}.
Lemma hostout_exist:
∀ s habd habd´ labd f,
hostout_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, hostout_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold hostout_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ihost_update. assumption.
Qed.
Lemma hostout_match:
∀ s d d´ m f,
hostout_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold hostout_spec; intros. subdestruct.
inv H. eapply match_impl_ihost_update. assumption.
Qed.
Context `{inv: PrimInvariants RData (data_ops:= data_ops) hostout_spec}.
Context `{inv0: PrimInvariants RData (data_ops:= data_ops0) hostout_spec}.
Lemma hostout_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem hostout_spec)
(id ↦ primcall_general_compatsem hostout_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv H4. inv match_extcall_states.
exploit hostout_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply hostout_match; eauto.
Qed.
End HOSTOUT_SIM.
Section PROC_CREATE_POSTINIT_SIM.
Context {re2: relate_impl_init}.
Lemma proc_create_postinit_exist:
∀ s habd habd´ labd f elf_id,
proc_create_postinit_spec elf_id habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, proc_create_postinit_spec elf_id labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold proc_create_postinit_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
Qed.
Lemma proc_create_postinit_match:
∀ s d d´ m f elf_id,
proc_create_postinit_spec elf_id d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold proc_create_postinit_spec; intros. subdestruct.
inv H. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) proc_create_postinit_spec}.
Context {inv0: PreservesInvariants (HD:= data0) proc_create_postinit_spec}.
Lemma proc_create_postinit_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem proc_create_postinit_spec)
(id ↦ gensem proc_create_postinit_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit proc_create_postinit_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply proc_create_postinit_match; eauto.
Qed.
End PROC_CREATE_POSTINIT_SIM.
End CPU_SIM.
Section TRAP_INFO_SIM.
Context {re1: relate_impl_trapinfo}.
Lemma trap_info_get_exist:
∀ habd labd s z f,
trap_info_get_spec habd = z
→ relate_AbData s f habd labd
→ trap_info_get_spec labd = z.
Proof.
unfold trap_info_get_spec; unfold trap_info_get_spec.
intros. exploit relate_impl_trapinfo_eq; eauto.
inversion 1. congruence.
Qed.
Lemma trap_info_ret_exist:
∀ habd labd s f,
relate_AbData s f habd labd
→ val_inject f (trap_info_ret_spec habd) (trap_info_ret_spec labd).
Proof.
intros. exploit relate_impl_trapinfo_eq; eauto.
inversion 1. assumption.
Qed.
Lemma trap_info_get_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_get_compatsem trap_info_get_spec)
(id ↦ primcall_trap_info_get_compatsem trap_info_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
match_external_states_simpl.
erewrite (trap_info_get_exist d1´ d2); eauto.
Qed.
Context {low1: low_level_invariant_impl}.
Lemma trap_info_ret_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec)
(id ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl.
eapply trap_info_ret_exist; eauto.
Qed.
End TRAP_INFO_SIM.
End OBJ_SIM.