Commit 28168cc9 by Hai Dang

### functions take and return results; breaking simple.v and refl.v

parent 92a15853
 ... ... @@ -59,6 +59,13 @@ Proof. by intros ?? Hv; apply (inj Some); rewrite -2!to_of_result Hv /=. Qed. Lemma is_closed_to_result X e v : to_result e = Some v → is_closed X e. Proof. intros <-%of_to_result. apply is_closed_of_result. Qed. Lemma list_Forall_to_of_result vl : Forall (λ ei, is_Some (to_result ei)) (of_result <\$> vl). Proof. apply Forall_forall. move => e /elem_of_list_fmap [? [-> ?]]. rewrite to_of_result. by eexists. Qed. (* Lemma subst_is_closed X x es e : is_closed X es → is_closed (x::X) e → is_closed X (subst x es e). Proof. ... ...
 ... ... @@ -427,6 +427,30 @@ Proof. + by rewrite /= HS in Eqv. Qed. Lemma tstep_call_inv_result (fid: fn_id) el e' σ σ' (TERM: Forall (λ ei, is_Some (to_result ei)) el) (STEP: (Call #[fid] el, σ) ~{fns}~> (e', σ')) : ∃ xl e HC es, fns !! fid = Some (@FunV xl e HC) ∧ subst_l xl el e = Some es ∧ e' = (EndCall (InitCall es)) ∧ σ' = σ ∧ Forall (λ ei, is_Some (to_value ei)) el. Proof. inv_tstep. symmetry in Eq. destruct (fill_call_decompose _ _ _ _ Eq) as [[]|[[K' [? Eq']]|[K' [v1 [vl [e2 [el2 [? Eq']]]]]]]]; subst. - simpl in *. inv_head_step. naive_solver. - exfalso. simpl in *. apply result_head_stuck in HS. destruct (fill_val (Λ:=bor_ectx_lang fns) K' e1') as [? Eqv]. + rewrite /= Eq'. by eexists. + by rewrite /= HS in Eqv. - exfalso. simpl in *. destruct Eq' as [Eq1 Eq2]. apply result_head_stuck in HS. destruct (fill_val (Λ:=bor_ectx_lang fns) K' e1') as [? Eqv]. + rewrite /= Eq1. apply (Forall_forall (λ ei, is_Some (to_result ei)) el); [exact TERM|]. rewrite Eq2. set_solver. + by rewrite /= HS in Eqv. Qed. (** MEM STEP -----------------------------------------------------------------*) (** Alloc *) ... ...
 ... ... @@ -2,7 +2,7 @@ From stbor.lang Require Import steps_inversion. From stbor.sim Require Export local invariant. Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" := (sim_local_body wsat vrel fs ft r n%nat es%E σs et%E σt Φ) (sim_local_body wsat rrel fs ft r n%nat es%E σs et%E σt Φ) (at level 70, format "'[hv' r '/' ⊨{ n , fs , ft } '/ ' '[ ' ( es , '/' σs ) ']' '/' ≥ '/ ' '[ ' ( et , '/' σt ) ']' '/' : Φ ']'"). ... ... @@ -13,7 +13,8 @@ fn table, allow giving a lower bound. But this is good enough for now. This could be done in general, but we just do it for the instance. *) Definition sim_mod_fun f1 f2 := ∀ fs ft, sim_local_funs_lookup fs ft → sim_local_fun wsat vrel fs ft end_call_sat f1 f2. ∀ fs ft, sim_local_funs_lookup fs ft → sim_local_fun wsat rrel fs ft end_call_sat f1 f2. Definition sim_mod_funs (fns fnt: fn_env) := ∀ name fn_src, fns !! name = Some fn_src → ∃ fn_tgt, ... ... @@ -66,7 +67,7 @@ Qed. assumption. *) Lemma sim_mod_funs_local fs ft : sim_mod_funs fs ft → sim_local_funs wsat vrel fs ft end_call_sat. sim_local_funs wsat rrel fs ft end_call_sat. Proof. intros Hmod. intros f fn_src Hlk. destruct (Hmod _ _ Hlk) as (fn_tgt & ? & ? & ?). exists fn_tgt. ... ...
 ... ... @@ -100,8 +100,15 @@ Definition wsat (r: resUR) (σs σt: state) : Prop := (** Value relation for function arguments/return values *) (* Values passed among functions are public *) Definition vrel (r: resUR) (v1 v2: value) := Forall2 (arel r) v1 v2. Definition vrel_res (r: resUR) (e1 e2: result) := ∃ v1 v2, e1 = ValR v1 ∧ e2 = ValR v2 ∧ vrel r v1 v2. Definition rrel (r: resUR) rs rt: Prop := match rs, rt with | ValR vs, ValR vt => vrel r vs vt | PlaceR ls ts Ts, PlaceR lt t_t Tt => (* Places are related like pointers, and the types must be equal. *) vrel r [ScPtr ls ts] [ScPtr lt t_t] ∧ Ts = Tt | _, _ => False end. (** Condition for resource before EndCall *) ... ... @@ -141,16 +148,14 @@ Proof. f_equal. by apply (arel_eq _ _ _ Eq1). by apply IH. Qed. Lemma vrel_res_eq r (e1 e2: result) : vrel_res r e1 e2 → e1 = e2. Lemma rrel_eq r (e1 e2: result) : rrel r e1 e2 → e1 = e2. Proof. intros (v1 & v2 & Eq1 & Eq2 & VREL). subst. f_equal. by eapply vrel_eq. destruct e1, e2; simpl; [|done..|]. - intros ?. f_equal. by eapply vrel_eq. - intros [VREL ?]. subst. apply vrel_eq in VREL. by simplify_eq. Qed. Lemma vrel_res_vrel r (v1 v2: value) : vrel_res r #v1 #v2 → vrel r v1 v2. Proof. intros (? & ? & Eq1 & Eq2 & ?). by simplify_eq. Qed. Lemma arel_mono (r1 r2 : resUR) (VAL: ✓ r2) : r1 ≼ r2 → ∀ s1 s2, arel r1 s1 s2 → arel r2 s1 s2. Proof. ... ... @@ -179,10 +184,12 @@ Lemma vrel_mono (r1 r2 : resUR) (VAL: ✓ r2) : r1 ≼ r2 → ∀ v1 v2, vrel r1 v1 v2 → vrel r2 v1 v2. Proof. intros Le v1 v2 VREL. by apply (Forall2_impl _ _ _ _ VREL), arel_mono. Qed. Lemma vrel_res_mono (r1 r2 : resUR) (VAL: ✓ r2) : r1 ≼ r2 → ∀ v1 v2, vrel_res r1 v1 v2 → vrel_res r2 v1 v2. Lemma rrel_mono (r1 r2 : resUR) (VAL: ✓ r2) : r1 ≼ r2 → ∀ v1 v2, rrel r1 v1 v2 → rrel r2 v1 v2. Proof. move => Le v1 v2 [? [? [? [? /(vrel_mono _ _ VAL Le) ?]]]]. do 2 eexists. eauto. intros Le v1 v2. destruct v1, v2; simpl; [|done..|]. - by apply vrel_mono. - intros [VREL ?]. split; [|done]. move : VREL. by apply vrel_mono. Qed. Lemma priv_loc_mono (r1 r2 : resUR) (VAL: ✓ r2) : ... ...
 ... ... @@ -9,7 +9,7 @@ Set Default Proof Using "Type". Section local. Context {A: ucmraT}. Variable (wsat: A → state → state → Prop). Variable (vrel: A → value → value → Prop). Variable (rrel: A → result → result → Prop). Variable (fs ft: fn_env). Notation PRED := (A → nat → result → state → result → state → Prop)%type. ... ... @@ -33,27 +33,27 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM) | sim_local_body_step_over_call (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) fid (vl_tgt: list value) (vl_src: list value) σ1_src fid (vl_tgt: list result) (vl_src: list result) σ1_src rc rv (* tgt is ready to make a call of [name] *) (CALLTGT: et = fill Kt (Call #[ScFnPtr fid] (Val <\$> vl_tgt))) (CALLTGT: et = fill Kt (Call #[ScFnPtr fid] (of_result <\$> vl_tgt))) (* src is ready to make a call of [name] *) (CALLSRC: (es, σs) ~{fs}~>* (fill Ks (Call #[ScFnPtr fid] (Val <\$> vl_src)), σ1_src)) (CALLSRC: (es, σs) ~{fs}~>* (fill Ks (Call #[ScFnPtr fid] (of_result <\$> vl_src)), σ1_src)) (* and we can pick a resource [rv] for the arguments *) (WSAT: wsat (r_f ⋅ (rc ⋅ rv)) σ1_src σt) (* [rv] justifies the arguments *) (VREL: Forall2 (vrel rv) vl_src vl_tgt) (VREL: Forall2 (rrel rv) vl_src vl_tgt) (* and after the call our context can continue *) (CONT: ∀ r' v_src v_tgt σs' σt' (* For any new resource r' that supports the returned values are (CONT: ∀ r' r_src r_tgt σs' σt' (* For any new resource r' that supports the returned results are related w.r.t. (r ⋅ r' ⋅ r_f) *) (VRET: vrel r' v_src v_tgt) (VRET: rrel r' r_src r_tgt) (WSAT: wsat (r_f ⋅ (rc ⋅ r')) σs' σt') (STACK: σt.(scs) = σt'.(scs)), ∃ idx', sim_local_body (rc ⋅ r') idx' (fill Ks (Val v_src)) σs' (fill Kt (Val v_tgt)) σt' Φ). (fill Ks (of_result r_src)) σs' (fill Kt (of_result r_tgt)) σt' Φ). Record sim_local_body_base (r_f: A) (sim_local_body : SIM) (r: A) (idx: nat) es σs et σt Φ : Prop := { ... ... @@ -112,20 +112,20 @@ Qed. (** Simulating functions: - We start after the substitution. - We assume the arguments are values related by [r] - The returned result must also be values and related by [vrel]. - We assume the arguments are results related by [r] - The returned result must also be related by [rrel]. This is called "local" because it considers one function at a time. However, it does assume full knowledge about the GLOBAL function table! *) Definition fun_post (esat: A → call_id → Prop) initial_call_id_stack (r: A) (n: nat) rs (σs: state) rt σt := (∃ c, σt.(scs) = c :: initial_call_id_stack ∧ esat r c) ∧ (∃ vs vt, rs = ValR vs ∧ rt = ValR vt ∧ vrel r vs vt). rrel r rs rt. Definition sim_local_fun (esat: A → call_id → Prop) (fn_src fn_tgt : function) : Prop := ∀ r es et (vl_src vl_tgt: list value) σs σt (VALEQ: Forall2 (vrel r) vl_src vl_tgt) (EQS: subst_l fn_src.(fun_args) (Val <\$> vl_src) fn_src.(fun_body) = Some es) (EQT: subst_l fn_tgt.(fun_args) (Val <\$> vl_tgt) fn_tgt.(fun_body) = Some et), ∀ r es et (vl_src vl_tgt: list result) σs σt (VALEQ: Forall2 (rrel r) vl_src vl_tgt) (EQS: subst_l fn_src.(fun_args) (of_result <\$> vl_src) fn_src.(fun_body) = Some es) (EQT: subst_l fn_tgt.(fun_args) (of_result <\$> vl_tgt) fn_tgt.(fun_body) = Some et), ∃ idx, sim_local_body r idx (InitCall es) σs (InitCall et) σt (fun_post esat σt.(scs)). ... ...
 ... ... @@ -46,15 +46,15 @@ Inductive sim_local_frames: our local resource r and have world satisfaction *) (WSAT' : wsat (r_f ⋅ (frame.(rc) ⋅ r')) σ_src' σ_tgt') (* and the returned values are related w.r.t. (r ⋅ r' ⋅ r_f) *) (VRET : vrel r' v_src v_tgt) (VRET : rrel r' v_src v_tgt) (CIDS: σ_tgt'.(scs) = frame.(callids)), ∃ idx', sim_local_body wsat vrel fns fnt ∃ idx', sim_local_body wsat rrel fns fnt (frame.(rc) ⋅ r') idx' (fill frame.(K_src) (Val v_src)) σ_src' (fill frame.(K_tgt) (Val v_tgt)) σ_tgt' (fill frame.(K_src) (of_result v_src)) σ_src' (fill frame.(K_tgt) (of_result v_tgt)) σ_tgt' (λ r _ vs σs vt σt, (∃ c, σt.(scs) = c :: cids ∧ end_call_sat r c) ∧ vrel_res r vs vt)) rrel r vs vt)) : sim_local_frames (r_f ⋅ frame.(rc)) frame.(callids) ... ... @@ -70,17 +70,17 @@ Inductive sim_local_conf: rc idx e_src σ_src e_tgt σ_tgt Ke_src Ke_tgt (FRAMES: sim_local_frames r_f cids K_src K_tgt frames) (LOCAL: sim_local_body wsat vrel fns fnt rc idx e_src σ_src e_tgt σ_tgt (LOCAL: sim_local_body wsat rrel fns fnt rc idx e_src σ_src e_tgt σ_tgt (λ r _ vs σs vt σt, (∃ c, σt.(scs) = c :: cids ∧ end_call_sat r c) ∧ vrel_res r vs vt)) rrel r vs vt)) (KE_SRC: Ke_src = fill K_src e_src) (KE_TGT: Ke_tgt = fill K_tgt e_tgt) (WSAT: wsat (r_f ⋅ rc) σ_src σ_tgt) : sim_local_conf idx Ke_src σ_src Ke_tgt σ_tgt. Lemma sim_local_conf_sim (FUNS: sim_local_funs wsat vrel fns fnt end_call_sat) (FUNS: sim_local_funs wsat rrel fns fnt end_call_sat) (idx:nat) (e_src:expr) (σ_src:state) (e_tgt:expr) (σ_tgt:state) (SIM: sim_local_conf idx e_src σ_src e_tgt σ_tgt) : sim fns fnt idx (e_src, σ_src) (e_tgt, σ_tgt) ... ... @@ -94,12 +94,12 @@ Proof. destruct sim_local_body_stuck as [vt Eqvt]. rewrite -(of_to_result _ _ Eqvt). destruct (sim_local_body_terminal _ Eqvt) as (vs' & σs' & r' & SS' & WSAT' & (c & CALLIDS & ESAT') & VREL). as (vs' & σs' & r' & SS' & WSAT' & (c & CALLIDS & ESAT') & RREL). have STEPK: (fill (Λ:=bor_ectxi_lang fns) K_src0 e_src0, σ_src) ~{fns}~>* (fill (Λ:=bor_ectxi_lang fns) K_src0 vs', σs'). { by apply fill_tstep_rtc. } have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NEVER_STUCK. clear -STEPK NT3 FRAMES WSAT' VREL. clear -STEPK NT3 FRAMES WSAT' RREL. inversion FRAMES. { left. rewrite to_of_result. by eexists. } right. subst K_src0 K_tgt0. move : NT3. simpl. intros NT3. ... ... @@ -109,14 +109,14 @@ Proof. apply tstep_reducible_fill_inv in RED; [|done]. apply tstep_reducible_fill. destruct RED as [e2 [σ2 Eq2]]. destruct VREL as (v1 & v2 & ? & ? & ?). subst vs' vt. move : Eq2. eapply end_call_tstep_src_tgt; eauto. by destruct (end_call_tstep_src_tgt _ fnt _ _ _ _ _ _ _ _ RREL WSAT' Eq2) as (?&?&?&?&?). - guardH sim_local_body_stuck. s. i. apply fill_result in H. unfold terminal in H. des. subst. inv FRAMES. ss. exploit sim_local_body_terminal; eauto. i. des. esplits; eauto; ss. + rewrite to_of_result. esplits; eauto. + ii. clarify. erewrite to_of_result. f_equal. eapply vrel_res_eq; eauto. + rewrite to_of_result; by eexists. + ii. clarify. erewrite to_of_result. f_equal. eapply rrel_eq; eauto. - guardH sim_local_body_stuck. i. destruct eσ2_tgt as [e2_tgt σ2_tgt]. ... ... @@ -130,20 +130,19 @@ Proof. (* Simulatin EndCall *) rename σ_tgt into σt. rename σs' into σs. destruct x3 as (vs1 & vt1 & Eqvs1 & Eqv1 & VR). (* destruct x3 as (vs1 & vt1 & Eqvs1 & Eqv1 & VR). *) simplify_eq. set Φ : resUR → nat → result → state → result → state → Prop := λ r2 _ vs2 σs2 vt2 σt2, vrel_res r2 vs2 vt2 ∧ λ r2 _ vs2 σs2 vt2 σt2, rrel r2 vs2 vt2 ∧ ∃ c1 c2 cids1 cids2, σs.(scs) = c1 :: cids1 ∧ σt.(scs) = c2 :: cids2 ∧ σs2 = mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc) ∧ σt2 = mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc) ∧ r2 = r'. have SIMEND : r' ⊨{idx,fns,fnt} (EndCall vs1, σs) ≥ (EndCall vt1, σt) : Φ. have SIMEND : r' ⊨{idx,fns,fnt} (EndCall vs', σs) ≥ (EndCall v, σt) : Φ. { apply sim_body_end_call; auto; [naive_solver|]. clear -VR. intros. rewrite /Φ. simpl. split; last naive_solver. by eexists _, _. } intros. rewrite /Φ. simpl. split; last naive_solver. done. } have NONE : to_result (EndCall e_tgt0) = None. by done. destruct (fill_tstep_inv _ _ _ _ _ _ NONE H) as [et2 [? STEPT2]]. ... ... @@ -152,20 +151,23 @@ Proof. have STEPK: (fill (Λ:= bor_ectxi_lang fns) (EndCallCtx :: K_src frame0 ++ K_f_src) e_src0, σ_src) ~{fns}~>* (fill (Λ:= bor_ectxi_lang fns) (EndCallCtx :: K_src frame0 ++ K_f_src) vs1, σs). (EndCallCtx :: K_src frame0 ++ K_f_src) vs', σs). { by apply fill_tstep_rtc. } have NT3 := never_stuck_tstep_rtc _ _ _ _ _ STEPK NEVER_STUCK. rewrite /= in NT3. have NT4 := never_stuck_fill_inv _ _ _ _ NT3. rewrite -(of_to_result _ _ x0) in STEPT2. destruct (sim_body_end_call_elim' _ _ _ _ _ _ _ _ _ SIMEND _ _ _ x1 NT4 STEPT2) as (r2 & idx2 & σs2 & STEPS & ? & HΦ2 & WSAT2). subst et2. as (r2 & idx2 & σs2 & vs & vt & STEPS & ? & HΦ2 & WSAT2). subst et2. exploit (CONTINUATION r2). { rewrite cmra_assoc; eauto. } { apply vrel_res_vrel. apply HΦ2. } { exploit tstep_end_call_inv; try exact STEPT2; eauto. i. des. subst. ss. rewrite HFRAME0 in x5. simplify_eq. ss. { apply HΦ2. } { exploit tstep_end_call_inv; try exact STEPT2; eauto. - rewrite to_of_result. by eexists. - i. des. subst. ss. rewrite HFRAME0 in x6. simplify_eq. ss. } intros [idx3 SIMFR]. rename σ2_tgt into σt2. do 2 eexists. split. ... ... @@ -189,18 +191,19 @@ Proof. * right. apply CIH. econs; eauto. + (* call *) exploit fill_step_inv_2; eauto. i. des; ss. exploit tstep_call_inv. { eapply list_Forall_to_value. eauto. } exploit tstep_call_inv_result. { instantiate (1:= (of_result <\$> vl_tgt)). by apply list_Forall_to_of_result. } { exact x2. } eauto. i. des. subst. have NT: never_stuck fns (Call #[ScFnPtr fid] (Val <\$> vl_src)) σ1_src. have NT: never_stuck fns (Call #[ScFnPtr fid] (of_result <\$> vl_src)) σ1_src. { apply (never_stuck_fill_inv _ Ks). eapply never_stuck_tstep_rtc; eauto. by apply (never_stuck_fill_inv _ K_src0). } edestruct NT as [[]|[e2 [σ2 RED]]]; [constructor 1|done|]. apply tstep_call_inv in RED; last first. { apply list_Forall_to_value. eauto. } destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ?). subst e2 σ2. apply tstep_call_inv_result in RED; last first. { by apply list_Forall_to_of_result. } destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ? & ?). subst e2 σ2. destruct (FUNS _ _ Eqfs) as ([xlt2 ebt2 HCt2] & Eqft2 & Eql2 & SIMf). rewrite Eqft2 in x3. simplify_eq. specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VREL Eqss x4) as [idx2 SIMf]. ... ... @@ -208,8 +211,7 @@ Proof. * left. eapply tc_rtc_l. { apply fill_tstep_rtc. eauto. } { econs. rewrite -fill_app. eapply (head_step_fill_tstep). econs. eapply (CallBS _ _ _ _ xls ebs); eauto. apply list_Forall_to_value. eauto. } econs. eapply (CallBS _ _ _ _ xls ebs); eauto. } * right. apply CIH. econs. { econs 2; eauto. i. instantiate (1 := mk_frame _ _ _ _). ss. destruct (CONT r' v_src v_tgt σ_src' σ_tgt' VRET WSAT'). ... ... @@ -217,7 +219,7 @@ Proof. pclearbot. esplits; eauto. } { eapply sim_local_body_post_mono; [|apply SIMf]. simpl. unfold vrel_res. naive_solver. } naive_solver. } { done. } { s. rewrite -fill_app. eauto. } { ss. rewrite -cmra_assoc; eauto. } ... ...
 ... ... @@ -10,7 +10,7 @@ Theorem sim_prog_sim_classical prog_tgt `{NSD: stuck_decidable_1 prog_src} (MAINT: has_main prog_src) (FUNS: sim_local_funs wsat vrel prog_src prog_tgt end_call_sat) (FUNS: sim_local_funs wsat rrel prog_src prog_tgt end_call_sat) : behave_prog prog_tgt <1= behave_prog prog_src. Proof. destruct MAINT as (ebs & HCs & Eqs). ... ... @@ -30,11 +30,10 @@ Proof. - eapply (sim_body_step_over_call _ _ init_res ε _ _ [] []); [done|..]. { intros fid fn_src. specialize (FUNS fid fn_src). naive_solver. } intros. simpl. exists 1%nat. apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)). apply sim_body_result. intros VALID. have ?: vrel_res (init_res ⋅ r') (#vs) (#vt). { do 2 eexists. do 2 (split; [done|]). eapply vrel_mono; [done|apply cmra_included_r|done]. } have ?: rrel (init_res ⋅ r') vs vt. { eapply rrel_mono; [done|apply cmra_included_r|exact VRET]. } split; [|done]. exists O. split; [by rewrite -STACKT|]. apply cmap_lookup_op_l_equiv_pub; [apply VALID|]. ... ...
 ... ... @@ -46,14 +46,6 @@ Context (css cst: call_id_stack). Definition sem_steps := 10%nat. Definition rrel (r: resUR) rs rt: Prop := match rs, rt with | ValR vs, ValR vt => vrel r vs vt | PlaceR ls ts Ts, PlaceR lt t_t Tt => (* Places are related like pointers, and the types must be equal. *) vrel r [ScPtr ls ts] [ScPtr lt t_t] ∧ Ts = Tt | _, _ => False end. Definition sem_post (r: resUR) (n: nat) rs css' rt cst': Prop := n = sem_steps ∧ css' = css ∧ cst' = cst ∧ rrel r rs rt. ... ... @@ -130,7 +122,7 @@ Proof. split. - eexists. split. subst cst css. rewrite <-Hstacks. congruence. admit. (* end_call_sat *) - admit. (* need to show they are values?!? *) - done. } rewrite (subst_l_map _ _ _ _ Hsubst1). rewrite (subst_l_map _ _ _ _ Hsubst2). ... ...
 ... ... @@ -1137,45 +1137,53 @@ Proof. Qed. (** EndCall *) Lemma end_call_tstep_src_tgt fs ft r σs σt (vs vt: value) es' σs' : wsat r σs σt → (EndCall vs, σs) ~{fs}~> (es', σs') → reducible ft (EndCall vt) σt. Lemma end_call_tstep_src_tgt fs ft r_f r σs σt (rs rt: result) es' σs' : rrel r rs rt → wsat (r_f ⋅ r) σs σt → (EndCall rs, σs) ~{fs}~> (es', σs') → ∃ vs vt : value, rs = ValR vs ∧ rt = ValR vt ∧ reducible ft (EndCall rt) σt. Proof. intros WSAT STEPS. edestruct (tstep_end_call_inv _ vs _ _ _ (ltac:(by eexists)) STEPS) as (vs' & Eqvs & ? & c & cids & Eqc & Eqs). intros RREL WSAT STEPS. edestruct (tstep_end_call_inv _ rs _ _ _ (ltac:(rewrite to_of_result; by eexists)) STEPS) as (vs & Eqvs & ? & c & cids & Eqc & Eqs). subst. simpl in Eqvs. symmetry in Eqvs. simplify_eq. destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (? & ? & Eqcs' & ?). rewrite to_of_result in Eqvs. simplify_eq. destruct rt as [vt|]; [|done]. exists vs, vt. do 2 (split; [done|]). exists (#vt)%E, (mkState σt.(shp) σt.(sst) cids σt.(snp) σt.(snc)). eapply (head_step_fill_tstep _ []). econstructor. by econstructor. econstructor. by rewrite -Eqcs'. Qed. Lemma sim_body_end_call fs ft r n vs vt σs σt Φ : Lemma sim_body_end_call fs ft r n rs rt σs σt Φ : (* return values are related *) vrel r vs vt → rrel r rs rt → (* The top of the call stack has no privately protected locations left *) (∃ c cids, σt.(scs) = c :: cids ∧ end_call_sat r c) → (∀ c1 c2 cids1 cids2, σs.(scs) = c1 :: cids1 → σt.(scs) = c2 :: cids2 → (∀ c1 c2 cids1 cids2 vs vt, σs.(scs) = c1 :: cids1 → σt.(scs) = c2 :: cids2 → rs = ValR vs → rt = ValR vt → let σs' := mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc) in let σt' := mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc) in Wf σt → Φ r n (ValR vs) σs' (ValR vt) σt' : Prop) → r ⊨{n,fs,ft} (EndCall (Val vs), σs) ≥ (EndCall (Val vt), σt) : Φ. Φ r n rs σs' rt σt' : Prop) → r ⊨{n,fs,ft} (EndCall (of_result rs), σs) ≥ (EndCall (of_result rt), σt) : Φ. Proof. intros VREL ESAT POST. pfold. intros NT r_f WSAT. split; [|done|]. { right. destruct (NT (EndCall #vs) σs) as [[]|[es' [σs' STEPS]]]; [done..|]. move : WSAT STEPS. apply end_call_tstep_src_tgt. } destruct (NT (EndCall rs) σs) as [[]|[es' [σs' STEPS]]]; [done..|]. eapply (end_call_tstep_src_tgt fs ft r_f r) in STEPS as (?&?&?&?&?); eauto. } constructor 1. intros et' σt' STEPT. destruct (tstep_end_call_inv _ #vt _ _ _ (ltac:(by eexists)) STEPT) destruct (tstep_end_call_inv ft (of_result rt) et' σt σt' (ltac:(rewrite to_of_result; by eexists)) STEPT) as (vt' & Eqvt & ? & c & cids & Eqc & Eqs). subst. simpl in Eqvt. symmetry in Eqvt. simplify_eq. subst. rewrite to_of_result in Eqvt. simplify_eq. rewrite /end_call_sat Eqc in ESAT. destruct ESAT as [c' [cs [Eqcs ESAT]]]. symmetry in Eqcs. simplify_eq. set σs' := (mkState σs.(shp) σs.(sst) cids σs.(snp) σs.(snc)). destruct rs as [vs|]; [|done]. have STEPS: (EndCall #vs, σs) ~{fs}~> ((#vs)%E, σs'). { destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (? & ? & Eqcs' & ?). eapply (head_step_fill_tstep _ []). ... ... @@ -1206,17 +1214,17 @@ Proof. intros l InD SHR. by specialize (Eqhp _ InD SHR). - intros ??. rewrite /=. by apply LINV. } (* result *) left. apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)). left. apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt')). intros VALID'. eapply POST; eauto. destruct SREL as (?&?&Eqs&?). by rewrite Eqs. Qed. Lemma sim_body_end_call_elim' fs ft r n vs vt σs σt Φ : r ⊨{n,fs,ft} (EndCall (Val vs), σs) ≥ (EndCall (Val vt), σt) : Φ → Lemma sim_body_end_call_elim' fs ft r n (rs rt: result) σs σt Φ : r ⊨{n,fs,ft} (EndCall rs, σs) ≥ (EndCall rt, σt) : Φ → ∀ r_f et' σt' (WSAT: wsat (r_f ⋅ r) σs σt) (NT: never_stuck fs (EndCall (Val vs)) σs) (STEPT: (EndCall (Val vt), σt) ~{ft}~> (et', σt')), ∃ r' n' σs', (EndCall (Val vs), σs) ~{fs}~>+ (Val vs, σs') ∧ et' = Val vt ∧ (NT: never_stuck fs (EndCall rs) σs) (STEPT: (EndCall rt, σt) ~{ft}~> (et', σt')), ∃ r' n' σs' vs vt, (EndCall rs, σs) ~{fs}~>+ (Val vs, σs') ∧ et' = Val vt ∧ Φ r' n' (ValR vs) σs' (ValR vt) σt' ∧ wsat (r_f ⋅ r') σs' σt'. Proof. ... ... @@ -1226,50 +1234,57 @@ Proof. inversion STEPSS; last first. { exfalso. clear -CALLTGT. symmetry in CALLTGT. apply fill_end_call_decompose in CALLTGT as [[]|[K' [? Eq]]]; [done|]. destruct (fill_result ft K' (Call #[ScFnPtr fid] (Val <\$> vl_tgt))) as [[] ?]; [rewrite Eq; by eexists|done]. } destruct (fill_result ft K' (Call #[ScFnPtr fid] (of_result <\$> vl_tgt))) as [[] ?]; [rewrite Eq to_of_result; by eexists|done]. } specialize (STEP _ _ STEPT) as (es1 & σs1 & r1 & n1 & STEP1 & WSAT1 & SIMV). have STEPK: (EndCall #vs, σs) ~{fs}~>* (es1, σs1). have STEPK: (EndCall rs, σs) ~{fs}~>* (es1, σs1). { destruct STEP1 as [|[]]. by apply tc_rtc. by simplify_eq. } have NT1 := never_stuck_tstep_rtc _ _ _ _ _ STEPK NT. pclearbot. punfold SIMV. specialize (SIMV NT1 _ WSAT1) as [ST1 TE1 STEPS1]. apply tstep_end_call_inv in STEPT as (? & Eq1 &? & ? & ? & ? & ?); [|by eexists]. simpl in Eq1. symmetry in Eq1. simplify_eq. specialize (TE1 vt eq_refl) as (vs2 & σs2 & r2 & STEP2 & WSAT2 & POST). apply tstep_end_call_inv in STEPT as (vt & Eq1 &? & ? & ? & ? & ?); [|by rewrite to_of_result; eexists]. rewrite to_of_result /= in Eq1. simplify_eq. specialize (TE1 vt eq_refl) as (rs2 & σs2 & r2 & STEP2 & WSAT2 & POST). exists r2, n1, σs2. assert (vs2 = vs ∧ (EndCall #vs, σs) ~{fs}~>+ ((#vs)%E, σs2)) as []. assert (rs2 = rs ∧ ∃ vs, (EndCall rs, σs) ~{fs}~>+ ((#vs)%E, σs2) ∧ rs = ValR vs) as [? [vs [??]]]. { clear -STEP1 STEP2. destruct STEP1 as [STEP1|[Eq11 Eq12]]; [|simplify_eq]. - have STEP1' := STEP1.