Library mcertikos.objects.ObjProc
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import BigStepLogReplay.
Require Import GlobalOracleProp.
Section OBJ_PROC.
Context `{real_params: RealParams}.
Context `{multi_oracle_ops : MultiOracleProp}.
Primitive: initialize VMCB and other components
Function save_uctx_spec (adt: RData) (rs: UContext) : option RData :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
Some adt {uctxt: ZMap.set curid rs (uctxt adt)}
| _ ⇒ None
end.
Function restore_uctx_spec (adt : RData): option (RData × UContext) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (ikern adt, ipt adt, pg adt, ihost adt, init adt) with
| (true, false, true, true, true) ⇒
let uctx0 := ZMap.get curid (uctxt adt) in
Some (adt {ikern: false}, uctx0)
| _ ⇒ None
end.
Function uctx_get_spec (i ofs: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_proc then
if is_UCTXT_ptr ofs then
None
else
match (ZMap.get ofs (ZMap.get i (uctxt adt))) with
| Vint n ⇒ Some (Int.unsigned n)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function uctx_set_spec (i ofs n: Z) (adt : RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_proc then
if is_UCTXT_ptr ofs then
None
else
let uctx := ZMap.get i (uctxt adt) in
let uctx´:= ZMap.set ofs (Vint (Int.repr n)) uctx in
Some adt {uctxt: ZMap.set i uctx´ (uctxt adt)}
else None
| _ ⇒ None
end.
Function uctx_set_eip_spec (adt : RData) (i: Z) (b: block) (ofs: int): option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_proc then
let uctx := ZMap.get i (uctxt adt) in
let uctx´:= ZMap.set U_EIP (Vptr b ofs) uctx in
Some adt {uctxt: ZMap.set i uctx´ (uctxt adt)}
else None
| _ ⇒ None
end.
primitive: save user context
Function proc_exit_user_spec (adt : RData) (rs : UContext) : option RData :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (init adt, ikern adt, pg adt, ihost adt) with
| (true, false, true, true) ⇒
Some adt {ikern: true} {PT: 0} {ipt: true} {uctxt: ZMap.set curid rs (uctxt adt)}
| _ ⇒ None
end.
Function proc_start_user_spec (adt: RData) : option (RData × UContext) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (ikern adt, pg adt, ihost adt, ipt adt, init adt) with
| (true, true, true, true, true) ⇒
let uctx0 := ZMap.get curid (uctxt adt) in
Some (adt {ikern: false} {ipt: false} {PT: curid}, uctx0)
| _ ⇒ None
end.
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (init adt, ikern adt, pg adt, ihost adt) with
| (true, false, true, true) ⇒
Some adt {ikern: true} {PT: 0} {ipt: true} {uctxt: ZMap.set curid rs (uctxt adt)}
| _ ⇒ None
end.
Function proc_start_user_spec (adt: RData) : option (RData × UContext) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (ikern adt, pg adt, ihost adt, ipt adt, init adt) with
| (true, true, true, true, true) ⇒
let uctx0 := ZMap.get curid (uctxt adt) in
Some (adt {ikern: false} {ipt: false} {PT: curid}, uctx0)
| _ ⇒ None
end.
primitive: return the first unused page table (or kctxt) and initialize the kernel context
Definition biglow_proc_create_spec (adt: RData) (b b´ buc: block) (ofs_uc: int) q : option (RData × Z) :=
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let c := ZMap.get curid (AC adt) in
let i := curid × max_children + 1 + Z_of_nat (length (cchildren c)) in
match (pg adt, ikern adt, ihost adt, ipt adt,cused c, cused (ZMap.get i (AC adt)), zlt_lt 0 i num_proc,
zlt (Z_of_nat (length (cchildren c))) max_children,
zle_le 0 q (cquota c - cusage c)) with
| (true, true, true, true, true, false, left _, left _, left _) ⇒
let child := mkContainer q 0 curid nil true in
let parent := (mkContainer (cquota c) (cusage c + q)
(cparent c) (i :: cchildren c) (cused c)) in
match ZMap.get lock_range (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get lock_range (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let e := TSHARED (OTDSPAWN i) in
let l´ := (TEVENT cpu e) :: l1 in
match CalTCB_log_real l´ with
| Some _ ⇒
let ofs := Int.repr ((i + 1) × PgSize -4) in
let rs := ((ZMap.get i (kctxt adt))#SP <- (Vptr b ofs))#RA <- (Vptr b´ Int.zero) in
let uctx0 := ZMap.get i (uctxt adt) in
let uctx1 := ZMap.set U_SS CPU_GDT_UDATA
(ZMap.set U_CS CPU_GDT_UCODE
(ZMap.set U_DS CPU_GDT_UDATA
(ZMap.set U_ES CPU_GDT_UDATA uctx0))) in
let uctx2 := ZMap.set U_EIP (Vptr buc ofs_uc)
(ZMap.set U_EFLAGS FL_IF
(ZMap.set U_ESP (Vint STACK_TOP) uctx1)) in
Some (adt {multi_log: ZMap.set lock_range (MultiDef l´) (multi_log adt)}
{AC: ZMap.set i child (ZMap.set curid parent (AC adt))}
{kctxt: ZMap.set i rs (kctxt adt)}
{uctxt: ZMap.set i uctx2 (uctxt adt)}, i)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition big_proc_create_spec (adt: RData) (b b´ buc: block) (ofs_uc: int) q : option (RData × Z) :=
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let c := ZMap.get curid (AC adt) in
let i := curid × max_children + 1 + Z_of_nat (length (cchildren c)) in
match (pg adt, ikern adt, ihost adt, ipt adt,cused c, cused (ZMap.get i (AC adt)), zlt_lt 0 i num_proc,
zlt (Z_of_nat (length (cchildren c))) max_children,
zle_le 0 q (cquota c - cusage c)) with
| (true, true, true, true, true, false, left _, left _, left _) ⇒
let child := mkContainer q 0 curid nil true in
let parent := (mkContainer (cquota c) (cusage c + q)
(cparent c) (i :: cchildren c) (cused c)) in
match big_log adt with
| BigDef l ⇒
let ofs := Int.repr ((i + 1) × PgSize -4) in
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSPAWN curid i q ofs
buc ofs_uc ) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some _ ⇒
let rs := ((ZMap.get i (kctxt adt))#SP <- (Vptr b ofs))#RA <- (Vptr b´ Int.zero) in
let uctx0 := ZMap.get i (uctxt adt) in
let uctx1 := ZMap.set U_SS CPU_GDT_UDATA
(ZMap.set U_CS CPU_GDT_UCODE
(ZMap.set U_DS CPU_GDT_UDATA
(ZMap.set U_ES CPU_GDT_UDATA uctx0))) in
let uctx2 := ZMap.set U_EIP (Vptr buc ofs_uc)
(ZMap.set U_EFLAGS FL_IF
(ZMap.set U_ESP (Vint STACK_TOP) uctx1)) in
Some (adt {big_log: BigDef l´}
{AC: ZMap.set i child (ZMap.set curid parent (AC adt))}
{kctxt: ZMap.set i rs (kctxt adt)}
{uctxt: ZMap.set i uctx2 (uctxt adt)}, i)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End OBJ_PROC.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import LAsmModuleSemAux.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_ops : MultiOracleProp}.
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}.
Local Open Scope Z_scope.
Section PROC_EXIT_USER_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re6: relate_impl_PT}.
Context {re300: relate_impl_CPU_ID}.
Context {re301: relate_impl_init}.
Lemma proc_exit_user_exist:
∀ s habd habd´ labd rs0 f,
proc_exit_user_spec habd rs0 = Some habd´
→ relate_AbData s f habd labd
→ (∀ i,
0≤ i < UCTXT_SIZE → val_inject f (ZMap.get i rs0) (ZMap.get i rs0))
→ ∃ labd´, proc_exit_user_spec labd rs0 = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold proc_exit_user_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite. intros.
subdestruct. inv HQ; refine_split´; trivial.
apply relate_impl_uctxt_update; eauto.
apply relate_impl_ipt_update; eauto.
apply relate_impl_PT_update; eauto.
apply relate_impl_ikern_update; eauto.
eapply uctxt_inj_set; eauto.
eapply relate_impl_uctxt_eq; eauto.
Qed.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {mt4: match_impl_uctxt}.
Lemma proc_exit_user_match:
∀ s d d´ m rs0 f,
proc_exit_user_spec d rs0 = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold proc_exit_user_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_uctxt_update.
eapply match_impl_ipt_update.
eapply match_impl_PT_update.
eapply match_impl_ikern_update. assumption.
Qed.
Context {inv: ExitUserInvariants proc_exit_user_spec (data_ops:= data_ops)}.
Context {inv0: ExitUserInvariants proc_exit_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma proc_exit_user_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_exit_user_compatsem proc_exit_user_spec)
(id ↦ primcall_exit_user_compatsem proc_exit_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit proc_exit_user_exist; eauto 1.
- subst uctx4 uctx3 uctx2 uctx1.
intros. inv_proc.
rewrite ZMap.gi. constructor.
- intros (labd´ & HP & HM).
refine_split; eauto 1.
econstructor; eauto 1.
+ reflexivity.
+ eapply reg_val_inject_defined; eauto 1.
+ intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H2) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H2 match_inject).
+ exploit (extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply extcall_args_without_data in H; eauto.
+ eapply reg_symbol_inject; eassumption.
+ econstructor; eauto. econstructor; eauto.
eapply proc_exit_user_match; eauto.
val_inject_simpl.
Qed.
End PROC_EXIT_USER_SIM.
Section PROC_START_USER_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re300: relate_impl_CPU_ID}.
Lemma proc_start_user_exist:
∀ s habd habd´ labd rs0 f,
proc_start_user_spec habd = Some (habd´, rs0)
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´ r´0, proc_start_user_spec labd = Some (labd´, r´0)
∧ relate_AbData s f habd´ labd´
∧ (∀ i,
0≤ i < UCTXT_SIZE → val_inject f (ZMap.get i rs0) (ZMap.get i r´0))
∧ r´0 = ZMap.get (ZMap.get (CPU_ID labd) (cid labd)) (uctxt labd)
∧ 0 ≤ ZMap.get (CPU_ID labd) (cid labd) < num_proc.
Proof.
unfold proc_start_user_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto. intros.
revert H H1 . subrewrite. intros.
subdestruct. inv HQ; refine_split´; trivial.
- apply relate_impl_PT_update; eauto.
apply relate_impl_ipt_update; eauto.
apply relate_impl_ikern_update; eauto.
- intros. eapply relate_impl_uctxt_eq; eauto.
Qed.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Lemma proc_start_user_match:
∀ s d d´ m rs0 f,
proc_start_user_spec d = Some (d´, rs0)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold proc_start_user_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_PT_update.
eapply match_impl_ipt_update.
eapply match_impl_ikern_update. assumption.
Qed.
Context {inv: StartUserInvariants proc_start_user_spec (data_ops:= data_ops)}.
Context {inv0: StartUserInvariants proc_start_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma proc_start_user_sim :
∀ id,
(∀ d1, high_level_invariant (CompatDataOps:= data_ops) d1 →
0 ≤ ZMap.get (CPU_ID d1) (cid d1) < num_proc) →
sim (crel RData RData) (id ↦ primcall_start_user_compatsem proc_start_user_spec)
(id ↦ primcall_start_user_compatsem proc_start_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H0. inv H1. inv match_extcall_states.
exploit proc_start_user_exist; eauto 1.
eapply H; assumption.
intros (labd´ & r´0 & HP & HM & Hrinj´ & Hr & HOS´). subst r´0.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; omega).
- intros. eapply uctxt_INJECT; try assumption.
- intros. eapply uctxt_INJECT; try assumption.
- eapply proc_start_user_match; eauto.
Qed.
End PROC_START_USER_SIM.
Section PROC_EXIT_USER_SIM2.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re6: relate_impl_PT}.
Context {re300: relate_impl_CPU_ID}.
Context {re301: relate_impl_init}.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {mt4: match_impl_uctxt}.
Context {inv: ExitUserInvariants2 proc_exit_user_spec (data_ops:= data_ops)}.
Context {inv0: ExitUserInvariants2 proc_exit_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma proc_exit_user_sim2 :
∀ id,
sim (crel RData RData) (id ↦ primcall_exit_user_compatsem2 proc_exit_user_spec)
(id ↦ primcall_exit_user_compatsem2 proc_exit_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit proc_exit_user_exist; eauto 1.
- subst uctx4 uctx3 uctx2 uctx1.
intros. inv_proc.
rewrite ZMap.gi. constructor.
- intros (labd´ & HP & HM).
refine_split; eauto 1.
econstructor; eauto 1.
+ reflexivity.
+ eapply reg_val_inject_defined; eauto 1.
+ intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H2) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H2 match_inject).
+ exploit (extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply extcall_args_without_data in H; eauto.
+ eapply reg_symbol_inject; eassumption.
+ econstructor; eauto. econstructor; eauto.
eapply proc_exit_user_match; eauto.
val_inject_simpl.
Qed.
End PROC_EXIT_USER_SIM2.
Section PROC_START_USER_SIM2.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re300: relate_impl_CPU_ID}.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {inv: StartUserInvariants2 proc_start_user_spec (data_ops:= data_ops)}.
Context {inv0: StartUserInvariants2 proc_start_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma proc_start_user_sim2 :
∀ id,
(∀ d1, high_level_invariant (CompatDataOps:= data_ops) d1 →
0 ≤ ZMap.get (CPU_ID d1) (cid d1) < num_proc) →
sim (crel RData RData) (id ↦ primcall_start_user_compatsem2 proc_start_user_spec)
(id ↦ primcall_start_user_compatsem2 proc_start_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H0. inv H1. inv match_extcall_states.
exploit proc_start_user_exist; eauto 1.
eapply H; assumption.
intros (labd´ & r´0 & HP & HM & Hrinj´ & Hr & HOS´). subst r´0.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; omega).
- intros. eapply uctxt_INJECT; try assumption.
- intros. eapply uctxt_INJECT; try assumption.
- eapply proc_start_user_match; eauto.
Qed.
End PROC_START_USER_SIM2.
Section BIGLOW_PROC_CREATE.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_multi_log}.
Context {re4: relate_impl_kctxt}.
Context {re5: relate_impl_uctxt}.
Context {re6: relate_impl_AC}.
Context {re7: relate_impl_cid}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_init}.
Context {re10: relate_impl_multi_oracle}.
Lemma biglow_proc_create_exist:
∀ (s : stencil) habd habd´ (labd : RData) b b´ buc ofs´ q n f,
biglow_proc_create_spec habd b buc b´ ofs´ q = Some (habd´, n)
→ relate_AbData s f habd labd
→ find_symbol s STACK_LOC = Some b
→ find_symbol s START_USER_FUN_LOC = Some buc
→ (∃ id, find_symbol s id = Some b´)
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, biglow_proc_create_spec labd b buc b´ ofs´ q = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_proc_create_spec. intros until f; intros HP HR Hsys Hsys´ Hsys´´ Hincr.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_multi_log_eq; eauto.
exploit relate_impl_multi_oracle_eq; eauto.
exploit relate_impl_AC_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert HP. subrewrite. subdestruct; inv HQ.
simpl.
generalize (relate_impl_kctxt_eq _ _ _ _ HR); eauto. intros.
generalize (relate_impl_uctxt_eq _ _ _ _ HR); eauto. intros.
refine_split´; trivial.
apply relate_impl_uctxt_update.
apply relate_impl_kctxt_update.
apply relate_impl_AC_update.
apply relate_impl_multi_log_update.
trivial.
- kctxt_inj_simpl.
+ eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply H7; eauto. omega.
- eapply uctxt_inj_set; eauto.
intros. inv_proc.
econstructor; eauto.
destruct Hsys´´ as [fun_id Hsys´´].
eapply stencil_find_symbol_inject´; eauto.
rewrite Int.add_zero; trivial.
eapply H8; eauto. omega.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt2: match_impl_multi_log}.
Context {mt3: match_impl_uctxt}.
Context {mt4: match_impl_AC}.
Lemma biglow_proc_create_match:
∀ s d d´ m b buc b´ ofs q n f,
biglow_proc_create_spec d b buc b´ ofs q = Some (d´, n)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_proc_create_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_uctxt_update.
eapply match_impl_kctxt_update.
eapply match_impl_AC_update.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: PCreateInvariants (data_ops:= data_ops) biglow_proc_create_spec}.
Context {inv0: PCreateInvariants (data_ops:= data_ops0) biglow_proc_create_spec}.
Lemma biglow_proc_create_sim :
∀ id,
sim (crel RData RData) (id ↦ proc_create_compatsem biglow_proc_create_spec)
(id ↦ proc_create_compatsem biglow_proc_create_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
exploit biglow_proc_create_exist; eauto 1; intros (labd´ & HP & HM).
destruct H9 as [fun_id Hsys].
exploit stencil_find_symbol_inject´; eauto. intros HFB.
match_external_states_simpl.
eapply biglow_proc_create_match; eauto.
Qed.
End BIGLOW_PROC_CREATE.
Section BIG_PROC_CREATE.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_big_log}.
Context {re4: relate_impl_kctxt}.
Context {re5: relate_impl_uctxt}.
Context {re6: relate_impl_AC}.
Context {re7: relate_impl_cid}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_init}.
Context {re10: relate_impl_big_oracle}.
Lemma big_proc_create_exist:
∀ (s : stencil) habd habd´ (labd : RData) b b´ buc ofs´ q n f,
big_proc_create_spec habd b buc b´ ofs´ q = Some (habd´, n)
→ relate_AbData s f habd labd
→ find_symbol s STACK_LOC = Some b
→ find_symbol s START_USER_FUN_LOC = Some buc
→ (∃ id, find_symbol s id = Some b´)
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, big_proc_create_spec labd b buc b´ ofs´ q = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_proc_create_spec. intros until f; intros HP HR Hsys Hsys´ Hsys´´ Hincr.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
exploit relate_impl_big_oracle_eq; eauto.
exploit relate_impl_AC_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert HP. subrewrite. subdestruct; inv HQ.
rewrite <- H3.
rewrite Hdestruct9.
simpl.
generalize (relate_impl_kctxt_eq _ _ _ _ HR); eauto. intros.
generalize (relate_impl_uctxt_eq _ _ _ _ HR); eauto. intros.
refine_split´; trivial.
apply relate_impl_uctxt_update.
apply relate_impl_kctxt_update.
apply relate_impl_AC_update.
apply relate_impl_big_log_update.
trivial.
- kctxt_inj_simpl.
+ eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply H7; eauto. omega.
- eapply uctxt_inj_set; eauto.
intros. inv_proc.
econstructor; eauto.
destruct Hsys´´ as [fun_id Hsys´´].
eapply stencil_find_symbol_inject´; eauto.
rewrite Int.add_zero; trivial.
eapply H8; eauto. omega.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt2: match_impl_big_log}.
Context {mt3: match_impl_uctxt}.
Context {mt4: match_impl_AC}.
Lemma big_proc_create_match:
∀ s d d´ m b buc b´ ofs q n f,
big_proc_create_spec d b buc b´ ofs q = Some (d´, n)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_proc_create_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_uctxt_update.
eapply match_impl_kctxt_update.
eapply match_impl_AC_update.
eapply match_impl_big_log_update.
assumption.
Qed.
Context {inv: PCreateInvariants (data_ops:= data_ops) big_proc_create_spec}.
Context {inv0: PCreateInvariants (data_ops:= data_ops0) big_proc_create_spec}.
Lemma big_proc_create_sim :
∀ id,
sim (crel RData RData) (id ↦ proc_create_compatsem big_proc_create_spec)
(id ↦ proc_create_compatsem big_proc_create_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
exploit big_proc_create_exist; eauto 1; intros (labd´ & HP & HM).
destruct H9 as [fun_id Hsys].
exploit stencil_find_symbol_inject´; eauto. intros HFB.
match_external_states_simpl.
eapply big_proc_create_match; eauto.
Qed.
End BIG_PROC_CREATE.
Section UCTX_GET_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_uctxt}.
Context {re3: relate_impl_ipt}.
Lemma uctx_get_exist:
∀ s habd labd i1 i2 z f,
uctx_get_spec i1 i2 habd = Some z
→ relate_AbData s f habd labd
→ uctx_get_spec i1 i2 labd = Some z.
Proof.
unfold uctx_get_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
revert H; subrewrite. subdestruct.
apply is_UCTXT_ptr_range in Hdestruct4.
exploit relate_impl_uctxt_eq; eauto.
rewrite Hdestruct5. intros HV. inv HV.
assumption.
Qed.
Lemma uctx_get_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem uctx_get_spec)
(id ↦ gensem uctx_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite uctx_get_exist; eauto. reflexivity.
Qed.
End UCTX_GET_SIM.
Section UCTX_SET_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Lemma uctx_set_exist:
∀ s habd habd´ labd z1 z2 i f,
uctx_set_spec i z1 z2 habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, uctx_set_spec i z1 z2 labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold uctx_set_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ; refine_split´; trivial.
apply relate_impl_uctxt_update; eauto.
eapply uctxt_inj_set; eauto.
- eapply relate_impl_uctxt_eq; eauto.
- intros. inv_proc.
eapply relate_impl_uctxt_eq; eauto.
Qed.
Context {mt1: match_impl_uctxt}.
Lemma uctx_set_match:
∀ s d d´ m z1 z2 i f,
uctx_set_spec i z1 z2 d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold uctx_set_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_uctxt_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) uctx_set_spec}.
Context {inv0: PreservesInvariants (HD:= data0) uctx_set_spec}.
Lemma uctx_set_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem uctx_set_spec)
(id ↦ gensem uctx_set_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit uctx_set_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply uctx_set_match; eauto.
Qed.
End UCTX_SET_SIM.
End OBJ_SIM.