strengthen call lemma to return values

theories/sim/instance.v

@@ -93,6 +93,10 @@ Proof.
   - intros [VREL ?]. subst. apply vrel_eq in VREL. by simplify_eq.
 Qed.
 
+Lemma vrel_rrel r (v1 v2 : value) :
+  vrel r v1 v2 → rrel vrel r #v1 #v2.
+Proof. done. Qed.
+
 Lemma rrel_mono (r1 r2 : resUR) (VAL: ✓ r2) :
   r1 ≼ r2 → ∀ v1 v2, rrel vrel r1 v1 v2 → rrel vrel r2 v1 v2.
 Proof.
@@ -113,6 +117,10 @@ Proof.
   have Eq2 := to_of_result e. rewrite Eq1 /= in Eq2. by simplify_eq.
 Qed.
 
+Lemma list_Forall_result_value_2 (vs: list value) :
+  of_result <$> (ValR <$> vs) = Val <$> vs.
+Proof. by rewrite -list_fmap_compose. Qed.
+
 Lemma list_Forall_rrel_vrel r (es et: list result) :
   Forall2 (rrel vrel r) es et →
   Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> es) →
@@ -128,3 +136,50 @@ Proof.
   by rewrite -> Forall2_fmap in RREL.
 Qed.
 
+Lemma rrel_to_value r (v1: value) e2:
+  rrel vrel r #v1 e2 → ∃ (v2: value), e2 = v2.
+Proof. destruct e2; [|done]. by eexists. Qed.
+
+Lemma list_Forall_rrel_to_value r vs et :
+  Forall2 (rrel vrel r) (ValR <$> vs) et →
+  ∃ vt, et = ValR <$> vt ∧ Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> et).
+Proof.
+  revert vs. induction et as [|e et IH]; intros vs.
+  { intros Eq%Forall2_nil_inv_r.
+    apply fmap_nil_inv in Eq. subst. simpl. by exists []. }
+  destruct vs as [|v vs]; [by intros Eq%Forall2_nil_inv_l|].
+  rewrite !fmap_cons. inversion 1 as [|???? RREL REST]; simplify_eq.
+  apply rrel_to_value in RREL as [vt ?].
+  apply IH in REST as [vts [? ?]]. subst e et. exists (vt :: vts).
+  rewrite fmap_cons. split; [done|]. constructor; [|done]. by eexists.
+Qed.
+
+Lemma list_Forall_rrel_vrel_2 r (es et: list result) :
+  Forall2 (rrel vrel r) es et →
+  Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> es) →
+  ∃ vs vt, es = ValR <$> vs ∧ et = ValR <$> vt ∧
+  Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> et) ∧
+  Forall2 (vrel r) vs vt.
+Proof.
+  intros RREL VRELs.
+  have VRELs' := VRELs. apply list_Forall_to_value in VRELs' as  [vs Eqs].
+  apply list_Forall_result_value in Eqs. subst es.
+  destruct (list_Forall_rrel_to_value _ _ _ RREL) as [vt [? VRELt]]. subst.
+  destruct (list_Forall_rrel_vrel _ _ _ RREL VRELs VRELt) as (vs' & vt' & Eq1 & Eq2 & ?).
+  by exists vs', vt'.
+Qed.
+
+Lemma list_Forall_rrel_vrel_3 r (vs: list value) (et: list result) :
+  Forall2 (rrel vrel r) (ValR <$> vs) et →
+  Forall (λ ei : expr, is_Some (to_value ei)) (Val <$> vs) →
+  ∃ vt, et = ValR <$> vt ∧
+  Forall (λ ei : expr, is_Some (to_value ei)) (Val <$> vt) ∧
+  Forall2 (vrel r) vs vt.
+Proof.
+  rewrite -list_Forall_result_value_2.
+  intros RREL VRELs.
+  destruct (list_Forall_rrel_vrel_2 _ _ _ RREL VRELs) as (vs1 & vt & Eqvs1 & ? & FA & ?).
+  subst. rewrite list_Forall_result_value_2 in FA.
+  exists vt. split; [done|].
+  apply Inj_instance_6 in Eqvs1; [by subst|]. intros ??. by inversion 1.
+Qed.

theories/sim/local.v

@@ -54,15 +54,15 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
     (* [rv] justifies the arguments *)
     (VREL: Forall2 (rrel rv) vl_src vl_tgt)
     (* and after the call our context can continue *)
-    (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: rrel r' r_src r_tgt)
+    (CONT: ∀ r' v_src v_tgt σs' σt'
+             (* For any new resource r' that supports the returned values are
+                related w.r.t. r' *)
+             (VRET: vrel r' v_src v_tgt)
              (WSAT: wsat (r_f ⋅ (rc ⋅ r')) σs' σt')
              (STACK: σt.(scs) = σt'.(scs)),
         ∃ idx', sim_local_body (rc ⋅ r') idx'
-                               (fill Ks (of_result r_src)) σs'
-                               (fill Kt (of_result r_tgt)) σt' Φ).
+                               (fill Ks (Val v_src)) σs'
+                               (fill Kt (Val v_tgt)) σt' Φ).
 
 Record sim_local_body_base (r_f: A) (sim_local_body : SIM)
   (r: A) (idx: nat) es σs et σt Φ : Prop := {

theories/sim/local_adequacy.v

@@ -46,12 +46,12 @@ 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  : rrel vrel r' v_src v_tgt)
+         (VRET  : vrel r' v_src v_tgt)
          (CIDS: σ_tgt'.(scs) = frame.(callids)),
          ∃ idx', sim_local_body wsat vrel fns fnt
                                 (frame.(rc) ⋅ r') idx'
-                                (fill frame.(K_src) (of_result v_src)) σ_src'
-                                (fill frame.(K_tgt) (of_result v_tgt)) σ_tgt'
+                                (fill frame.(K_src) (Val v_src)) σ_src'
+                                (fill frame.(K_tgt) (Val v_tgt)) σ_tgt'
                                 (λ r _ vs σs vt σt,
                                   (∃ c, σt.(scs) = c :: cids ∧ end_call_sat r c) ∧
                                   rrel vrel r vs vt))

theories/sim/program.v

@@ -30,7 +30,7 @@ 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.
+    apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
     intros VALID.
     have ?: rrel vrel (init_res ⋅ r') vs vt.
     { eapply rrel_mono; [done|apply cmra_included_r|exact VRET]. }

theories/sim/refl_pure_step.v

@@ -9,21 +9,27 @@ Set Default Proof Using "Type".
 
 (** Call - step over *)
 Lemma sim_body_step_over_call fs ft
-  rc rv n fid vls vlt σs σt Φ
-  (VREL: Forall2 (vrel rv) vls vlt)
+  rc rv n fid rls rlt σs σt Φ
+  (RREL: Forall2 (rrel vrel rv) rls rlt)
   (FUNS: sim_local_funs_lookup fs ft) :
-  (∀ r' vs vt σs' σt' (VRET: rrel vrel r' vs vt)
+  (∀ r' vls vlt vs vt σs' σt' (VRET: vrel r' vs vt)
     (STACKS: σs.(scs) = σs'.(scs))
-    (STACKT: σt.(scs) = σt'.(scs)), ∃ n',
-    rc ⋅ r' ⊨{n',fs,ft} (of_result vs, σs') ≥ (of_result vt, σt') : Φ) →
+    (STACKT: σt.(scs) = σt'.(scs))
+    (Eqvls: rls = ValR <$> vls)
+    (Eqvlt: rlt = ValR <$> vlt), ∃ n',
+    rc ⋅ r' ⊨{n',fs,ft} (Val vs, σs') ≥ (Val vt, σt') : Φ) →
   rc ⋅ rv ⊨{n,fs,ft}
-    (Call #[ScFnPtr fid] (Val <$> vls), σs) ≥ (Call #[ScFnPtr fid] (Val <$> vlt), σt) : Φ.
+    (Call #[ScFnPtr fid] (of_result <$> rls), σs) ≥ (Call #[ScFnPtr fid] (of_result <$> rlt), σt) : Φ.
 Proof.
   intros CONT. pfold. intros NT r_f WSAT.
   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 by apply list_Forall_to_of_result.
+  destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ? & VALs).
+  have VALs' := VALs. apply list_Forall_to_value in VALs' as [vls Eqvls].
+  subst. rewrite Eqvls. rewrite Eqvls in VALs, Eqss.
+  apply list_Forall_result_value in Eqvls. subst rls.
+  destruct (list_Forall_rrel_vrel_3 _ _ _ RREL VALs) as (vlt & ? & VALt & VREL).
+  subst rlt.
   destruct (FUNS _ _ Eqfs) as ([xlt ebt HCt] & Eqft & Eql).
   simpl in Eql.
   destruct (subst_l_is_Some xlt (Val <$> vlt) ebt) as [est Eqst].
@@ -31,15 +37,14 @@ Proof.
             (subst_l_is_Some_length _ _ _ _ Eqss) fmap_length //. }
   split; [|done|].
   { right. exists (EndCall (InitCall est)), σt.
-     eapply (head_step_fill_tstep _ []). econstructor. econstructor; try done.
-     apply list_Forall_to_value. eauto. }
+     eapply (head_step_fill_tstep _ []).
+     econstructor. econstructor; try done; rewrite list_Forall_result_value_2 //. }
   eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
             [] [] fid (ValR <$> vlt) (ValR <$> vls)); eauto.
   { by rewrite of_result_list_expr. }
-  { by rewrite of_result_list_expr. }
-  { eapply Forall2_fmap, Forall2_impl; eauto. }
   intros r' ? ? σs' σt' VR WSAT' STACK.
-  destruct (CONT _ _ _ σs' σt' VR) as [n' ?]; [|done|exists n'; by left].
+  destruct (CONT r' vls vlt v_src v_tgt σs' σt') as [n' ?];
+    [by apply vrel_rrel| |done..|exists n'; by left].
   destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (?&?&?Eqcss&?).
   destruct WSAT' as (?&?&?&?&?&SREL'&?). destruct SREL' as (?&?&?Eqcss'&?).
   by rewrite Eqcss' Eqcss.

theories/sim/simple.v

@@ -127,14 +127,16 @@ Qed.
 
 (* [Val <$> _] in the goal makes this not work with [apply], but
 we'd need tactic support for anything better. *)
-Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
+Lemma sim_simple_call n' rls rlt rv fs ft r r' n fid css cst Φ :
   sim_local_funs_lookup fs ft →
-  Forall2 (vrel rv) vls vlt →
+  Forall2 (rrel vrel rv) rls rlt →
   r ≡ r' ⋅ rv →
-  (∀ rret vs vt, rrel vrel rret vs vt →
-    r' ⋅ rret ⊨ˢ{n',fs,ft} (of_result vs, css) ≥ (of_result vt, cst) : Φ) →
+  (∀ rret vs vt vls vlt,
+    rls = ValR <$> vls → rlt = ValR <$> vlt →
+    vrel rret vs vt →
+    r' ⋅ rret ⊨ˢ{n',fs,ft} (Val vs, css) ≥ (Val vt, cst) : Φ) →
   r ⊨ˢ{n,fs,ft}
-    (Call #[ScFnPtr fid] (Val <$> vls), css) ≥ (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.
+    (Call #[ScFnPtr fid] (of_result <$> rls), css) ≥ (Call #[ScFnPtr fid] (of_result <$> rlt), cst) : Φ.
 Proof.
   intros Hfns Hrel Hres HH σs σt <-<-.
   eapply sim_body_res_proper; last apply: sim_body_step_over_call.