Library mcertikos.multithread.highrefins.AsmPHThread2T
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import Constant.
Require Import PrimSemantics.
Require Import LRegSet.
Require Import AuxStateDataType.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobalOracle.
Require Import AlgebraicMem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import SingleOracle.
Require Import AbstractDataType.
Require Export ObjMultiprocessor.
Require Import AuxFunctions.
Require Import liblayers.compat.CompatLayers.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import CompatExternalCalls.
Require Import MakeProgram.
Require Import LAsmModuleSem.
Require Import I64Layer.
Require Import Soundness.
Require Import LinkTactic.
Require Import MakeProgramImpl.
Require Import StencilImpl.
Require Import LAsmModuleSemAux.
Require Import SingleConfiguration.
Require Import LAsm.
Require Import TAsm.
Require Import HAsm.
Require Export PHThread.
Require Import VCGen.
Require Import FutureTactic.
Section LIBRARY.
Context {D}`{data_prf : CompatData D}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{Hstencil: Stencil (stencil := stencil)}.
Context `{L: compatlayer (cdata D)}.
Local Instance : ExternalCallsOps (mwd (cdata D)) := CompatExternalCalls.compatlayer_extcall_ops L.
Lemma exec_external_prop:
∀ (ge: genv) WB ef args t vl (m m´: mwd (cdata D)),
external_call´ WB ef ge args m t vl m´ →
∀ (BUILTIN_ENABLED : match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
snd m´ = snd m.
Proof.
intros; simpl in ×.
destruct m; destruct m´; subst; simpl.
inversion H; subst.
destruct ef; try contradiction;
try (inversion H0; subst; auto; fail).
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H7; subst; try tauto.
inversion H2; lift_unfold.
destruct H4; subst; tauto.
+ destruct decode_longs in *; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H8; subst; auto.
inversion H2; lift_unfold.
destruct H5; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H8; lift_unfold.
destruct H2; destruct H3; destruct H8; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H9; lift_unfold.
destruct H2; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H14; lift_unfold.
destruct H2; subst; tauto.
Qed.
End LIBRARY.
Section Refinement.
Context `{s_link_config : SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil (stencil := stencil)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{LH: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined (LH ⊕ L64)}.
Local Instance ec_ops : ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops (LH ⊕ L64).
Local Instance lcfg_ops : LayerConfigurationOps := compatlayer_configuration_ops (LH ⊕ L64).
Lemma ef_case_extern_call:
∀ ef,
(match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then True else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then False else True
| _ ⇒ True
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end).
Proof.
intros. destruct ef; auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
destruct (has_event name); auto.
Qed.
Lemma ef_case_prim_call:
∀ ef,
(match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end).
Proof.
intros. destruct ef; auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
Qed.
Section WITH_ORACLE.
Section ABSTRACT_REL_T.
Class AbstractRelT:=
{
match_dproc_RData: dproc → Log → RData → Prop;
match_curid: current_thread = current_curid;
match_init:
match_dproc_RData
(thread_init_dproc current_thread)
init_log
(thread_init_rdata current_thread);
get_env_log_exist:
∀ e l l´ curid,
proc_id (uRData l) = curid →
lastEvType l ≠ Some LogYieldTy →
l´ = e::l →
lastEvType l´ = Some LogYieldTy →
match last_op l´ with
| Some e ⇒ match e with
| LEvent curid´ _ ⇒ curid = curid´
end
| _ ⇒ False
end →
∃ l´´, get_env_log limit curid l´ = Some l´´ ∧ lastEvType l´´ = Some LogYieldTy;
yield_nextstate_match:
∀ curid ae (m m´ : mem) (a a´: RData) (l l´ l´´ l´´´: Log) e nb WB ef (ge : genv) args m t res,
lastEvType l ≠ Some LogYieldTy →
proc_id (uRData l) = curid →
match_dproc_RData ae l a →
l´ = LEvent curid (LogYield (Mem.nextblock m)) :: l →
get_env_log limit curid l´ = Some l´´ →
last_op l´´ = Some e →
getLogEventNB e = Some nb →
l´´´ = LEvent current_curid LogYieldBack::l´´ →
match ef with
| EF_external id _ ⇒
if peq id thread_yield then True else False
| _ ⇒ False
end →
external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (phthread ⊕ L64))
WB ef ge args (m, a) t res (m´, a´) →
(mem_lift_nextblock m (Pos.to_nat nb - Pos.to_nat (Mem.nextblock m)) = m´) ∧
match_dproc_RData ae l´´´ a´ ∧
state_check thread_yield nil l ae ∧
proc_id (uRData l´´´) = curid;
sleep_nextstate_match:
∀ curid ae (m m´ : mem) (a a´: RData) (l l´ l´´ l´´´: Log) e nb WB ef (ge : genv) args m t res i,
lastEvType l ≠ Some LogYieldTy →
proc_id (uRData l) = curid →
match_dproc_RData ae l a →
l´ = LEvent curid (LogSleep (Int.unsigned i) (Mem.nextblock m)
(sync_chpool_check thread_sleep (Lint i::nil) (uRData l) ae))::l →
get_env_log limit curid l´ = Some l´´ →
last_op l´´ = Some e →
getLogEventNB e = Some nb →
l´´´ = LEvent current_curid LogYieldBack::l´´ →
match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True else False
| _ ⇒ False
end →
external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (phthread ⊕ L64))
WB ef ge args (m, a) t res (m´, a´) →
args = Vint i :: nil →
(mem_lift_nextblock m (Pos.to_nat nb - Pos.to_nat (Mem.nextblock m)) = m´) ∧
match_dproc_RData ae l´´´ a´ ∧
state_check thread_sleep (Lint i::nil) l ae ∧
proc_id (uRData l´´´) = curid;
acc_exec_load_match:
∀ (ge: genv) a a´ rs rd rs´ TY (m m´: mem) l d addr,
exec_loadex ge TY (m, a) addr rs rd = Next rs´ (m´, a´) →
match_dproc_RData d l a →
∃ d´,
(acc_exec_load (cl_oplus (cdata PData) LH L64))
fundef unit ge TY (m, (uRData l, d)) addr rs rd = Next rs´ (m´, (uRData l, d´)) ∧
match_dproc_RData d´ l a´;
acc_exec_store_match:
∀ (ge: genv) a a´ rs rd rs´ TY ST (m m´: mem) l d addr,
exec_storeex ge TY (m, a) addr rs rd ST = Next rs´ (m´, a´) →
match_dproc_RData d l a →
∃ d´ : dproc,
(acc_exec_store (cl_oplus (cdata PData) LH L64))
fundef unit ge TY (m, (uRData l, d)) addr rs rd ST =
Next rs´ (m´, (uRData l, d´)) ∧ match_dproc_RData d´ l a´;
external_call_match_no_event:
∀ (ge: genv) WB ef (args: list val) t res (m m´ : mem) (a a´: RData) ae l,
external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (phthread ⊕ L64))
WB ef ge args (m, a) t res (m´, a´) →
match_dproc_RData ae l a →
proc_id (uRData l) = current_curid →
lastEvType l ≠ Some LogYieldTy →
match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then False else True
| _ ⇒ True
end →
∃ ae´,
external_call´ (mem := mwd (cdata PData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (LH ⊕ L64))
WB ef ge args (m, (uRData l, ae)) t res (m´, (uRData l, ae´)) ∧
match_dproc_RData ae´ l a´ ∧
proc_id (uRData l) = current_curid;
external_call_match_has_event:
∀ (ge: genv) WB ef (args: list val) t res (m m´ : mem) (a a´: RData) ae l,
external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (phthread ⊕ L64))
WB ef ge args (m, a) t res (m´, a´) →
match_dproc_RData ae l a →
proc_id (uRData l) = current_curid →
lastEvType l ≠ Some LogYieldTy →
match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then True else False
| _ ⇒ False
end →
∃ (largs : list lval) ae´ (l´ : Log),
external_call´ (mem := mwd (cdata PData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (LH ⊕ L64))
WB ef ge args (m, (uRData l, ae)) t res (m´, (uRData l´, ae´)) ∧
match_dproc_RData ae´ l´ a´ ∧
val2Lval_list args largs ∧
proc_id (uRData l´) = current_curid ∧
match ef with
| EF_external id _ ⇒
∃ choice,
choice_check id largs (uRData l) ae = choice ∧
l´ = LEvent (proc_id (uRData l)) (LogPrim id largs choice (snap_func ae)) :: l
| _ ⇒ l´ = l
end;
primitive_call_match:
∀ (ge: genv) ef t rs rs´ (m m´ : mem) l a a´ ae,
primitive_call (LayerConfigurationOps := compatlayer_configuration_ops (phthread ⊕ L64))
(mem := mwd (cdata RData)) ef ge rs (m, a) t rs´ (m´, a´) →
match_dproc_RData ae l a →
proc_id (uRData l) = current_curid →
match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end →
∃ l´ ae´,
primitive_call (LayerConfigurationOps := lcfg_ops)
(mem := mwd (cdata PData)) ef ge rs (m, (uRData l, ae)) t rs´ (m´, (uRData l´, ae´)) ∧
match_dproc_RData ae´ l´ a´ ∧
proc_id (uRData l´) = current_curid ∧
match ef with
| EF_external id _ ⇒
if has_event id
then l´ = LEvent (proc_id (uRData l)) (LogPrim id nil 0 (snap_func ae)) :: l
else l´ = l
| _ ⇒ l´ = l
end
}.
End ABSTRACT_REL_T.
Context `{abs_rel: AbstractRelT}.
Inductive match_tstate: (state (mem:= mwd (cdata RData))) →
(tstate (mem := mem)) → Prop :=
| MATCH_TSTATE:
∀ (rs: regset) (m: mem) a ae (l : Log)
(Hdata: match_dproc_RData ae l a)
(Hcurid: proc_id (uRData l) = current_curid)
(Hlast: lastEvType l ≠ Some LogYieldTy),
match_tstate (State rs (m, a)) (TState current_curid rs m ae l).
Lemma asm_exec_instr_match:
∀ ge f (i : Asm.instruction) rs rs´ (m m´: mem) l d a a´
(Hexec: exec_instr (lcfg_ops:= compatlayer_configuration_ops (phthread ⊕ L64)) ge f i rs (m, a) = Next rs´ (m´, a´))
(Hmatch: match_dproc_RData d l a),
∃ d´,
exec_instr (lcfg_ops := compatlayer_configuration_ops (LH ⊕ L64)) ge f i rs (m, (uRData l, d)) = Next rs´ (m´, (uRData l, d´))
∧ match_dproc_RData d´ l a´.
Proof.
intros.
intros; simpl in ×.
destruct i; try (simpl in *; inversion Hexec; subst; ∃ d; eauto; fail);
simpl in *; try (eauto using acc_exec_load_match; fail); try (eauto using acc_exec_store_match; fail).
- destruct (Val.divu (rs EAX) (rs # EDX <- Vundef r1)); [ | inversion Hexec].
destruct (Val.modu (rs EAX) (rs # EDX <- Vundef r1)); inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- destruct (Val.divs (rs EAX) (rs # EDX <- Vundef r1)); [ | inversion Hexec].
destruct (Val.mods (rs EAX) (rs # EDX <- Vundef r1)); inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- destruct (eval_testcond c rs).
+ destruct b; inversion Hexec; subst.
× ∃ d; split; [simpl; auto | assumption ].
× ∃ d; split; [simpl; auto | assumption ].
+ inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- destruct (eval_testcond c rs); try (inversion Hexec; fail).
destruct b; subst.
+ unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
+ inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- destruct (eval_testcond c1); try (inversion Hexec; fail).
destruct b; simpl.
+ destruct (eval_testcond c2 rs); try (inversion Hexec; fail).
destruct b.
× unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
× inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
+ destruct (eval_testcond c2 rs); inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- destruct (rs r); try (inversion Hexec; fail).
destruct (list_nth_z tbl (Int.unsigned i)); try (inversion Hexec; fail).
unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- simpl in Hexec.
lift_unfold; simpl in ×.
destruct (Mem.alloc m 0 sz); simpl in ×.
destruct (Mem.store Mint32 m0 b (Int.unsigned (Int.add Int.zero ofs_link)) (rs ESP));
[simpl in × | inversion Hexec].
destruct (Mem.store Mint32 m1 b (Int.unsigned (Int.add Int.zero ofs_ra)) (rs RA));
[simpl in × | inversion Hexec].
inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
- unfold Mem.loadv in *; simpl in ×.
destruct (Val.add (rs ESP) (Vint ofs_ra)); try (inversion Hexec; fail).
lift_unfold; simpl in ×.
destruct (Mem.load Mint32 m b (Int.unsigned i)); try (inversion Hexec; fail).
destruct (Val.add (rs ESP) (Vint ofs_link)); try (inversion Hexec; fail).
destruct (Mem.load Mint32 m b0 (Int.unsigned i0)); try (inversion Hexec; fail).
destruct (rs ESP); try (inversion Hexec; fail).
destruct (Mem.free m b1 0 sz); try (inversion Hexec; fail).
simpl in *; inversion Hexec; subst.
∃ d; split; [simpl; auto | assumption ].
Fail idtac.
Qed.
Lemma exec_instr_match:
∀ ge f i rs rs´ (m m´: mem) l d a a´
(Hexec: exec_instr (lcfg_ops:= compatlayer_configuration_ops (phthread ⊕ L64)) ge f i rs (m, a) = Next rs´ (m´, a´))
(Hmatch: match_dproc_RData d l a),
∃ d´,
exec_instr ge f i rs (m, (uRData l, d)) = Next rs´ (m´, (uRData l, d´))
∧ match_dproc_RData d´ l a´.
Proof.
intros.
unfold exec_instr in Hexec; simpl.
subdestruct; try (inv Hexec; esplit; eauto; fail);
simpl in *; try (eauto using acc_exec_load_match; fail); try (eauto using acc_exec_store_match; fail).
eapply asm_exec_instr_match; eauto.
Qed.
Lemma no_nil_exists_last_op:
∀ {A : Type} (l : list A), l ≠ nil → ∃ e, last_op l = Some e.
Proof.
intros.
destruct l; subst; [ elim H; reflexivity | ].
simpl; ∃ a; auto.
Qed.
Lemma exec_external_has_event:
∀ (ge : genv) (t : trace) (rs : regset) (m : mwd (cdata RData)) (m´ : mwd (cdata RData)) (st : tstate)
(H0 : match_tstate (State rs m) st) (b : block) (ef : external_function) (args : list val)
(res : list val)
(H5 : rs PC = Vptr b Int.zero)
(H6 : Genv.find_funct_ptr ge b = Some (External ef))
(H8 : extcall_arguments rs m (ef_sig ef) args)
(H9 : external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (phthread ⊕ L64))
(fun _ : block ⇒ True) ef ge args m t res m´)
(STACK : ∀ (b0 : block) (o : int), rs ESP = Vptr b0 o → Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m))
(SP_NOT_VUNDEF : rs ESP ≠ Vundef)
(RA_NOT_VUNDEF : rs RA ≠ Vundef)
(EF_YIELD : match ef with
| EF_external id _ ⇒
if peq id thread_yield
then False
else if peq id thread_sleep then False else if has_event id then True else False
| EF_builtin _ _ ⇒ False
| EF_vload _ ⇒ False
| EF_vstore _ ⇒ False
| EF_vload_global _ _ _ ⇒ False
| EF_vstore_global _ _ _ ⇒ False
| EF_malloc ⇒ False
| EF_free ⇒ False
| EF_memcpy _ _ ⇒ False
| EF_annot _ _ ⇒ False
| EF_annot_val _ _ ⇒ False
| EF_inline_asm _ ⇒ False
end),
∃ st´ : tstate,
tstep ge st t st´ ∧
match_tstate
(State
((set_regs (loc_external_result (ef_sig ef)) res
(undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs))) # PC <- (rs RA)) # RA <- Vundef m´) st´.
Proof.
intros.
inv H0.
destruct m´; simpl.
rename m into m´.
rename m0 into m.
rename l0 into a´.
exploit external_call_match_has_event; eauto.
intros external_call_prop.
destruct external_call_prop
as (largs & ( ae´ & (l´ & ext_call_prop))).
destruct ext_call_prop as (ext_call_p1 & (ext_call_p2 & (ext_call_p3 & (ext_call_p4 & ext_call_p5)))).
esplit; split.
{ eapply texec_step_external; eauto.
- clearAllExceptOne H8.
unfold extcall_arguments in ×.
induction H8; econstructor; eauto.
inversion H; econstructor; eauto.
- instantiate (1:= l´).
destruct ef; try auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
destruct (has_event name); eauto; try contradiction.
∃ largs.
destruct ext_call_p5 as (choice & ext_call_p5 & ext_call_p6).
∃ choice.
split; auto; split; auto.
rewrite <- Hcurid.
assumption. }
{ econstructor; eauto.
destruct ef; try (subst; auto).
destruct ext_call_p5 as (choice & ext_call_p5 & ext_call_p6).
destruct (has_event name); subst; auto.
- unfold lastEvType; simpl; intro contra; inv contra.
- subdestruct; inv EF_NORM_HAS_EVENT. }
Qed.
Lemma exec_external_yield:
∀ (ge : genv) (t : trace) (rs : regset) (m : mwd (cdata RData)) (m´ : mwd (cdata RData)) (st : tstate)
(H0 : match_tstate (State rs m) st) (b : block) (ef : external_function) (args : list val)
(res : list val)
(H5 : rs PC = Vptr b Int.zero)
(H6 : Genv.find_funct_ptr ge b = Some (External ef))
(H8 : extcall_arguments rs m (ef_sig ef) args)
(H9 : external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (phthread ⊕ L64))
(fun _ : block ⇒ True) ef ge args m t res m´)
(STACK : ∀ (b0 : block) (o : int), rs ESP = Vptr b0 o → Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m))
(SP_NOT_VUNDEF : rs ESP ≠ Vundef)
(RA_NOT_VUNDEF : rs RA ≠ Vundef)
(EF_YIELD : match ef with
| EF_external id _ ⇒ if peq id thread_yield then True else False
| EF_builtin _ _ ⇒ False
| EF_vload _ ⇒ False
| EF_vstore _ ⇒ False
| EF_vload_global _ _ _ ⇒ False
| EF_vstore_global _ _ _ ⇒ False
| EF_malloc ⇒ False
| EF_free ⇒ False
| EF_memcpy _ _ ⇒ False
| EF_annot _ _ ⇒ False
| EF_annot_val _ _ ⇒ False
| EF_inline_asm _ ⇒ False
end),
∃ st´ : tstate,
tstep ge st t st´ ∧
match_tstate
(State
((set_regs (loc_external_result (ef_sig ef)) res
(undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs))) # PC <- (rs RA)) # RA <- Vundef m´) st´.
Proof.
intros.
inv H0.
destruct m´; simpl.
rename m into m´.
rename m0 into m.
rename l0 into a´.
destruct ef; try contradiction.
destruct (peq name thread_yield); try contradiction.
subst.
inversion H9; subst.
inversion H; subst.
destruct H0.
set (l´ := LEvent current_curid (LogYield (Mem.nextblock m))::l).
edestruct get_env_log_exist with (l := l) (l´ := l´) as (l´´, (get_env_val, l_not_nil)); auto.
{ unfold l´; reflexivity. }
destruct (no_nil_exists_last_op l´´) as (e, l_op); auto.
{ destruct l´´; unfold lastEvType in l_not_nil; simpl in l_not_nil; try inv l_not_nil.
intro contra; inv contra. }
assert (Hnextblock: ∃ nb, getLogEventNB (e) = Some nb).
{ unfold getLogEventNB; destruct e; simpl.
destruct l0; simpl.
- ∃ n; auto.
- ∃ n; auto.
- destruct l´´; simpl in l_op; try (inv l_op; fail).
unfold lastEvType in l_not_nil.
simpl in l_not_nil.
unfold getLogEventType in l_not_nil.
destruct l0.
unfold getLogEventUnitType in l_not_nil.
destruct l0; inv l_op.
inv l_not_nil.
- destruct l´´; simpl in l_op; try (inv l_op; fail).
unfold lastEvType in l_not_nil.
simpl in l_not_nil.
unfold getLogEventType in l_not_nil.
destruct l0.
unfold getLogEventUnitType in l_not_nil.
destruct l0; inv l_op.
inv l_not_nil. }
destruct Hnextblock as (nb, Hnextblock).
set (l´´´ := LEvent current_curid LogYieldBack::l´´).
exploit yield_nextstate_match; eauto; simpl; try (rewrite peq_true; auto); [rewrite Hcurid in get_env_val; auto | ].
intros Hnextblock_prop.
destruct Hnextblock_prop as (Hnextblock_prop1 & Hnextblock_prop2 & Hnextblock_prop3 & Hnextblock_prop4).
set (rs´ := ((set_regs (loc_external_result sg) (encode_long (sig_res sg) v)
((((((((((((((((rs # ST0 <- Vundef) # EAX <- Vundef)
# ECX <- Vundef) # EDX <- Vundef) # XMM0 <- Vundef)
# XMM1 <- Vundef) # XMM2 <- Vundef) # XMM3 <- Vundef)
# XMM4 <- Vundef) # XMM5 <- Vundef) # XMM6 <- Vundef)
# XMM7 <- Vundef) # ZF <- Vundef) # CF <- Vundef) # PF <- Vundef)
# SF <- Vundef) # OF <- Vundef) # PC <- (rs RA)) # RA <- Vundef ).
set (rs´´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs))
# EAX <- Vundef #PC <- (rs RA) #RA <- Vundef).
∃ (TState current_curid rs´´ m´ ae l´´´).
assert (x = CompatGenSem.gensem big2_thread_yield_spec).
{ clearAllExceptOne H0.
eapply get_layer_primitive_oplus_either in H0.
destruct H0.
- unfold phthread.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]);
inversion H.
simpl in *; eauto.
- unfold L64 in H.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]);
inversion H. }
subst.
inv H1.
simpl.
destruct H2 as (sigma, (Hstencil_matches, (H2a, (H2b, (Hsub1, Hsub2))))).
assert (rs´_eq_rs´´ : rs´ = rs´´).
{ unfold rs´; unfold rs´´. subst.
unfold rs´ in ×. unfold rs´´ in ×.
inversion H2b.
simpl.
repeat f_equal.
clear H H0 H2 Hnextblock Hnextblock_prop2 Hnextblock_prop3 H8 H9 get_env_val.
inv H2b.
simpl in ×.
unfold big2_thread_yield_spec in H2a; simpl in H2a.
clear l_op l_not_nil e H6 rs´ rs´´ l´´´ l´.
simpl in ×.
inversion H2a.
clear H2a; inversion H3.
auto. }
simpl in rs´´.
fold rs´.
rewrite Hsub2.
split.
{ eapply texec_step_external_yield; eauto.
rewrite Hcurid in get_env_val.
subst; unfold l´ in get_env_val; auto. }
{ simpl.
fold rs´.
rewrite rs´_eq_rs´´.
unfold l´´´.
econstructor; eauto.
unfold lastEvType.
simpl.
intro contra; inv contra. }
Fail idtac.
Qed.
Lemma exec_external_sleep:
∀ (ge : genv) (t : trace) (rs : regset) (m : mwd (cdata RData)) (m´ : mwd (cdata RData)) (st : tstate)
(H0 : match_tstate (State rs m) st) (b : block) (ef : external_function) (args : list val)
(res : list val)
(H5 : rs PC = Vptr b Int.zero)
(H6 : Genv.find_funct_ptr ge b = Some (External ef))
(H8 : extcall_arguments rs m (ef_sig ef) args)
(H9 : external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (phthread ⊕ L64))
(fun _ : block ⇒ True) ef ge args m t res m´)
(STACK : ∀ (b0 : block) (o : int), rs ESP = Vptr b0 o → Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m))
(SP_NOT_VUNDEF : rs ESP ≠ Vundef)
(RA_NOT_VUNDEF : rs RA ≠ Vundef)
(EF_YIELD : match ef with
| EF_external id _ ⇒ if peq id thread_sleep then True else False
| EF_builtin _ _ ⇒ False
| EF_vload _ ⇒ False
| EF_vstore _ ⇒ False
| EF_vload_global _ _ _ ⇒ False
| EF_vstore_global _ _ _ ⇒ False
| EF_malloc ⇒ False
| EF_free ⇒ False
| EF_memcpy _ _ ⇒ False
| EF_annot _ _ ⇒ False
| EF_annot_val _ _ ⇒ False
| EF_inline_asm _ ⇒ False
end),
∃ st´ : tstate,
tstep ge st t st´ ∧
match_tstate
(State
((set_regs (loc_external_result (ef_sig ef)) res
(undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs))) # PC <- (rs RA)) # RA <- Vundef m´) st´.
Proof.
intros.
inv H0.
destruct m´; simpl.
rename m into m´.
rename m0 into m.
rename l0 into a´.
destruct ef; try contradiction.
destruct (peq name thread_sleep); try contradiction.
subst.
inversion H9; subst.
inversion H; subst.
destruct H0.
assert (x = CompatGenSem.gensem big2_thread_sleep_spec).
{ clearAllExceptOne H0.
eapply get_layer_primitive_oplus_either in H0.
destruct H0.
- unfold phthread in H.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]);
inversion H.
simpl in *; eauto.
- unfold L64 in H.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]);
inversion H. }
subst.
inv H1.
simpl.
destruct H2 as (sigma, (Hstencil_matches, (H2a, (H2b, (Hsub1, Hsub2))))).
subst.
assert (thread_sleep_arguments:
∃ i, extcall_arguments rs m (mksignature (Tint:: nil) None cc_default) (Vint i:: nil) ∧
args = (Vint i)::nil).
{ simpl.
subst.
inv H2b; simpl in ×.
simpl in H8.
subst.
unfold CompatGenSem.sextcall_generic_info in H8.
simpl in H8.
unfold sextcall_sig in H8.
simpl in H8.
unfold csig_sig in H8.
simpl in H8.
unfold Ctypes.signature_of_type in H8.
simpl in H8.
destruct args; try (inv H8; fail).
destruct args; try (clearAllExceptOne H8; inv H8; inv H4; fail).
inv H2a; inv H9; inv H7.
∃ i.
clearAllExceptOne H8.
simpl in H8.
unfold extcall_arguments in ×.
inversion H8; subst.
econstructor; eauto.
inversion H2; subst.
simpl in H5.
econstructor; eauto.
econstructor; eauto.
econstructor. }
destruct thread_sleep_arguments as (i & thread_sleep_arguments & args_eq).
set (l´ := LEvent current_curid
(LogSleep (Int.unsigned i) (Mem.nextblock m)
(sync_chpool_check thread_sleep (Lint i::nil) (uRData l) ae))::l).
edestruct get_env_log_exist with (l := l) (l´ := l´) as (l´´, (get_env_val, l_not_nil)); auto.
{ unfold l´; reflexivity. }
destruct (no_nil_exists_last_op l´´) as (e, l_op); auto.
{ destruct l´´; unfold lastEvType in l_not_nil; simpl in l_not_nil; try inv l_not_nil.
intro contra; inv contra. }
assert (Hnextblock: ∃ nb, getLogEventNB (e) = Some nb).
{ unfold getLogEventNB; destruct e; simpl.
destruct l0; simpl.
- ∃ n; auto.
- ∃ n; auto.
- destruct l´´; simpl in l_op; try (inv l_op; fail).
unfold lastEvType in l_not_nil.
simpl in l_not_nil.
unfold getLogEventType in l_not_nil.
destruct l0.
unfold getLogEventUnitType in l_not_nil.
destruct l0; inv l_op.
inv l_not_nil.
- destruct l´´; simpl in l_op; try (inv l_op; fail).
unfold lastEvType in l_not_nil.
simpl in l_not_nil.
unfold getLogEventType in l_not_nil.
destruct l0.
unfold getLogEventUnitType in l_not_nil.
destruct l0; inv l_op.
inv l_not_nil. }
destruct Hnextblock as (nb, Hnextblock).
set (l´´´ := LEvent current_curid LogYieldBack::l´´).
exploit sleep_nextstate_match; eauto; simpl; try (rewrite peq_true; auto);
[ unfold l´ in get_env_val; rewrite Hcurid in get_env_val; eauto | ].
intros Hnextblock_prop.
destruct Hnextblock_prop as (Hnextblock_prop1 & Hnextblock_prop2 & Hnextblock_prop3 & Hnextblock_prop4).
set (rs´ := ((set_regs (loc_external_result (sextcall_sig sigma))
(encode_long
(Ctypes.opttyp_of_type (csig_res (sextcall_csig sigma)))
v)
((((((((((((((((rs # ST0 <- Vundef) # EAX <- Vundef)
# ECX <- Vundef) # EDX <- Vundef) # XMM0 <- Vundef)
# XMM1 <- Vundef) # XMM2 <- Vundef) # XMM3 <- Vundef)
# XMM4 <- Vundef) # XMM5 <- Vundef) # XMM6 <- Vundef)
# XMM7 <- Vundef) # ZF <- Vundef) # CF <- Vundef) # PF <- Vundef)
# SF <- Vundef) # OF <- Vundef) # PC <- (rs RA)) # RA <- Vundef).
set (rs´´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs))
# EAX <- Vundef #PC <- (rs RA) #RA <- Vundef).
∃ (TState current_curid rs´´ m´ ae l´´´).
assert (rs´_eq_rs´´ : rs´ = rs´´).
{ unfold rs´; unfold rs´´. subst.
unfold rs´ in ×. unfold rs´´ in ×.
inversion H2b.
simpl.
repeat f_equal.
clear H H0 H2 Hnextblock Hnextblock_prop2 Hnextblock_prop3 H8 H9 get_env_val.
inv H2b.
simpl in ×.
unfold big2_thread_sleep_spec in H2a; simpl in H2a.
clear l_op l_not_nil e H6 rs´ rs´´ l´´´ l´.
simpl in ×.
clear Hnextblock_prop4 thread_sleep_arguments Hstencil_matches.
inversion H2a.
clear H2a.
inversion H3; substx.
inversion H13; substx.
reflexivity.
}
simpl in rs´´.
fold rs´.
split.
{ eapply texec_step_external_sleep; eauto.
rewrite Hcurid in get_env_val.
subst; unfold l´ in get_env_val; auto. }
{ simpl.
fold rs´.
rewrite rs´_eq_rs´´.
unfold l´´´.
econstructor; eauto.
unfold lastEvType.
simpl.
intro contra; inv contra. }
Fail idtac.
Qed.
Theorem LAsm_refine_TAsm :
∀ ge t rs m rs´ m´ st,
LAsm.step (lcfg_ops := compatlayer_configuration_ops (phthread ⊕ L64)) ge (State rs m) t (State rs´ m´) →
match_tstate (State rs m) st →
∃ st´,
TAsm.tstep ge st t st´
∧ match_tstate (State rs´ m´) st´.
Proof.
intros. inv H.
-
inv H0. destruct m´ as (m´, a´).
exploit exec_instr_match; eauto.
intros (d´ & Hexec & Hmatch); subst.
esplit. split.
+ eapply texec_step_internal; eauto.
+ econstructor; eauto.
-
inv H0.
pose proof H9 as Hext.
eapply exec_external_prop in H9; eauto.
destruct m´ as (m´, a´). simpl in H9. subst.
esplit.
split.
+ instantiate (1:= TState current_curid
(nextinstr_nf
(set_regs res vl
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs))) m´ ae l).
eapply texec_step_builtin; eauto.
instantiate (1:= uRData l).
inversion Hext; subst.
econstructor; try reflexivity.
subdestruct; try contradiction.
×
simpl in ×.
inversion H; subst; simpl in *;
subdestruct; subst;
unfold PregEq.t in *; rewrite Hdestruct.
{ inv H; eapply CompCertBuiltins.builtin_sem_i64_neg; eauto. }
{ inv H1.
inv H. eapply CompCertBuiltins.builtin_sem_i64_neg; reflexivity. }
{ inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_add; eauto. }
{ inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_add; eauto. }
{ inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_sub; eauto. }
{ inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_sub; eauto. }
{ inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_mul; eauto. }
×
simpl in H.
subdestruct; subst; setoid_rewrite Hdestruct0; inv H.
econstructor.
inv H7; econstructor; eauto.
×
simpl in ×.
subdestruct;
unfold PregEq.t in *; rewrite Hdestruct0;
try (inv H; fail);
try (subst; inv H; econstructor; eauto;
(inversion H10 || inversion H9); subst; econstructor; eauto;
simpl; lift_unfold;
destruct H0; split; eauto; fail).
×
simpl in ×.
inv H; subdestruct; unfold PregEq.t in *; rewrite <- H0; econstructor; eauto; inv H9; econstructor; eauto.
×
simpl in ×.
subdestruct; simpl in *;
unfold PregEq.t in *; rewrite Hdestruct1;
inv H; econstructor; eauto;
(inv H10 || inv H2); econstructor; eauto;
lift_unfold; destruct H0; split; auto.
×
simpl in H; subdestruct; subst; setoid_rewrite Hdestruct0.
{ inv H; econstructor; eauto. }
{ inv H.
destruct m´0.
simpl in H2, H10; lift_unfold.
destruct H2, H10.
econstructor; lift_unfold.
- instantiate (1:= (m, (uRData l, ae))).
split; eauto.
- split; eauto. }
×
inv H; subst.
subdestruct; setoid_rewrite Hdestruct.
rewrite <- H0.
econstructor; eauto.
simpl in *; lift_unfold.
destruct H3; split; auto.
×
simpl in H; subdestruct; setoid_rewrite Hdestruct0.
inv H; subst.
{ inv H. }
{ inv H; subst.
econstructor; eauto.
simpl in ×.
lift_unfold.
destruct H17; split; auto. }
×
simpl in H; inv H; econstructor; eauto.
×
simpl in H; subdestruct; unfold PregEq.t in *; rewrite Hdestruct1;
inversion H; subst; econstructor; eauto.
+ econstructor; eauto.
-
inv H0.
pose proof H10 as Hext.
eapply exec_external_prop in H10; eauto.
destruct m´ as (m´, a´). simpl in H10. subst.
esplit.
split.
+ instantiate (1:= TState current_curid (nextinstr rs) m´ ae l).
eapply texec_step_annot; eauto.
instantiate (1:= vargs).
× clearAllExceptOne H9.
unfold annot_arguments in ×.
induction H9; try econstructor; try assumption.
inversion H; subst; econstructor; eauto.
× instantiate (1:= uRData l).
instantiate (1:= v).
inversion Hext; subst.
econstructor; try reflexivity.
subdestruct; try contradiction.
{
simpl in H.
inversion H; subst.
- eapply CompCertBuiltins.builtin_sem_i64_neg; eauto.
- eapply CompCertBuiltins.builtin_sem_i64_add; eauto.
- eapply CompCertBuiltins.builtin_sem_i64_sub; eauto.
- eapply CompCertBuiltins.builtin_sem_i64_mul; eauto. }
{
simpl in H.
subdestruct; subst; inv H.
inversion H7; subst.
+ inversion H7; subst.
econstructor; econstructor; eauto.
+ inversion H7; subst.
econstructor; econstructor; eauto. }
{
simpl in ×.
subdestruct; subst; try (inv H; fail);
try (inv H; econstructor; (inv H11 || inv H10); econstructor; eauto; simpl in *; lift_unfold;
destruct H0; split; eauto; fail). }
{
simpl in ×.
inv H; subdestruct; econstructor; eauto; inv H10; econstructor; eauto. }
{
simpl in ×.
subdestruct; simpl in *; inv H; econstructor; eauto;
(inv H11 || inv H2); econstructor; eauto; lift_unfold; destruct H0; split; eauto. }
{
simpl in H; subdestruct; subst.
- inv H; econstructor; eauto.
- inv H.
destruct m´0.
simpl in H2, H11; lift_unfold.
destruct H2, H11.
econstructor; lift_unfold.
instantiate (1:= (m, (uRData l, ae))).
× split; eauto.
× split; eauto. }
{
inv H; subst; subdestruct.
econstructor; eauto.
simpl in *; lift_unfold.
destruct H3; split; auto. }
{
simpl in H; subdestruct; inv H; subst.
econstructor; eauto.
simpl in ×.
lift_unfold.
destruct H18; split; auto. }
{
simpl in H; inv H; econstructor; eauto. }
{
simpl in H; subdestruct; inv H; econstructor; eauto. }
+ econstructor; eauto.
-
exploit ef_case_extern_call; eauto.
instantiate (1:= ef); intros ef_case.
destruct ef_case as [EF_NORM_HAS_EVENT | [EF_NORM_NO_EVENT | [EF_YIELD | EF_SLEEP]]].
×
eapply exec_external_has_event; eauto.
×
intros.
inv H0.
destruct m´; simpl.
rename m into m´.
rename m0 into m.
rename l0 into a´.
exploit external_call_match_no_event; eauto.
intros external_call_prop.
destruct external_call_prop
as (ae´ & ext_call_prop).
destruct ext_call_prop as (ext_call_p1 & (ext_call_p2 & ext_call_p3)).
esplit; split.
{ eapply texec_step_external; eauto.
- clearAllExceptOne H8.
unfold extcall_arguments in ×.
induction H8; econstructor; eauto.
inversion H; econstructor; eauto.
- instantiate (1:= l).
destruct ef; try auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
destruct (has_event name); eauto; try contradiction. }
{ econstructor; eauto. }
×
eapply exec_external_yield; eauto.
×
eapply exec_external_sleep; eauto.
-
exploit ef_case_prim_call; eauto.
instantiate (1:= ef); intros ef_case.
destruct ef_case as [EF_NORM | [EF_YIELD | EF_SLEEP]].
×
destruct m as (m, a).
destruct m´ as (m´, a´).
inv H0; subst.
exploit primitive_call_match; eauto.
intros primitive_call_prop.
destruct primitive_call_prop as (l´ & (ae´ & (prim_call_p1 & (prim_call_p2 & (prim_call_p3 & prim_call_p4))))).
esplit; split.
{ eapply texec_step_prim_call; eauto.
instantiate (1 := l´).
destruct ef; try auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
destruct (has_event name); eauto.
rewrite <- Hcurid; eauto. }
{ econstructor; eauto.
destruct ef; try (subst; auto).
destruct (has_event name); subst; auto.
unfold lastEvType; simpl; intro contra; inv contra. }
×
destruct m as (m, a).
destruct m´ as (m´, a´).
inv H0; subst.
inv H8.
destruct H as (sg & (sigma & H)).
destruct H as (EF_val & (Ha & Hb)).
destruct ef; try contradiction.
destruct (peq name thread_yield); try contradiction; subst.
inv EF_val.
assert (sigma = CompatGenSem.gensem big2_thread_yield_spec).
{ clearAllExceptOne Ha.
eapply get_layer_primitive_oplus_either in Ha.
destruct Ha.
- unfold phthread.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]); inversion H.
simpl in *; eauto.
- unfold L64 in H.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]); inversion H. }
subst; inversion Hb.
×
destruct m as (m, a).
destruct m´ as (m´, a´).
inv H0; subst.
inv H8.
destruct H as (sg & (sigma & H)).
destruct H as (EF_val & (Ha & Hb)).
destruct ef; try contradiction.
destruct (peq name thread_sleep); try contradiction; subst.
inv EF_val.
assert (sigma = CompatGenSem.gensem big2_thread_sleep_spec).
{ clearAllExceptOne Ha.
eapply get_layer_primitive_oplus_either in Ha.
destruct Ha.
- unfold phthread in H.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]);
inversion H.
simpl in *; eauto.
- unfold L64 in H.
repeat (eapply get_layer_primitive_oplus_either in H; destruct H; [inversion H | idtac]); inversion H. }
subst; inversion Hb.
Fail idtac.
Qed.
Context `{extcallsx: !ExternalCallsXDefined (LH ⊕ L64)}.
Context `{primcall_props: !PrimcallProperties TAsm.sprimitive_call}.
Theorem cl_backward_simulation:
∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
(Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (LH ⊕ L64) = OK ph),
backward_simulation
(HAsm.semantics (phthread ⊕ L64) ph)
(TAsm.tsemantics ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_step with (match_states:= match_tstate);
simpl; intros; trivial.
+
inv H. setoid_rewrite InitMem.init_mem_with_data in H0.
destruct (Genv.init_mem ph) eqn:Hinit; contra_inv. inv H0.
esplit; split.
× econstructor; eauto.
{ instantiate (1 := rs0).
unfold initial_thread_state.
subst ge.
rewrite H2.
reflexivity. }
×
rewrite match_curid.
eapply MATCH_TSTATE.
{
rewrite <- match_curid.
eapply match_init; eauto.
}
{
rewrite <- match_curid.
apply init_log_proc_id.
}
{
destruct init_log_structure as [Hil | (l & _ & Hil & _)];
setoid_rewrite Hil;
discriminate.
}
+ destruct s1, s1´, s2. exploit LAsm_refine_TAsm; eauto.
- eapply lasm_semantics_receptive.
decision.
- apply tasm_semantics_determinate.
Qed.
End WITH_ORACLE.
End Refinement.