change local simulation relation to be more strongly typed and use vrel directly

theories/sim/body.v

@@ -154,7 +154,7 @@ Proof.
           - simplify_eq. right. split; [|done]. lia. }
         { pclearbot. left. eapply paco7_mon_bot; eauto. }
       + eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
-            Ks1 Kt1 fid el_tgt _ _ _ _ CALLTGT); eauto; [by etrans|].
+            Ks1 Kt1 fid vl_tgt _ _ _ _ CALLTGT); eauto; [by etrans|].
         intros r4 vs4 vt4 σs4 σt4 VREL4 STACK4.
         destruct (CONT _ _ _ σs4 σt4 VREL4 STACK4) as [idx4 CONT4].
         exists idx4. pclearbot. left.  eapply paco7_mon_bot; eauto.
@@ -170,7 +170,7 @@ Proof.
       + pclearbot. right. by apply CIH. }
   { (* Kt[et] has a call, and we step over the call *)
     eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
-            (Ks1 ++ Ks) (Kt1 ++ Kt) fid el_tgt); [by rewrite CALLTGT fill_app|..];
+            (Ks1 ++ Ks) (Kt1 ++ Kt) fid vl_tgt); [by rewrite CALLTGT fill_app|..];
             eauto; [rewrite fill_app; by apply fill_tstep_rtc|].
     intros r' vs' vt' σs' σt' VREL' STACK'.
     destruct (CONT _ _ _ σs' σt' VREL' STACK') as [idx' CONT2]. clear CONT.

theories/sim/instance.v

@@ -2,11 +2,11 @@ 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_expr fs ft r n%nat es%E σs et%E σt Φ)
+  (sim_local_body wsat vrel fs ft r n%nat es%E σs et%E σt Φ)
   (at level 70, format "'[hv' r  '/' ⊨{ n , fs , ft } '/  ' '[ ' ( es ,  '/' σs ) ']' '/' ≥  '/  ' '[ ' ( et ,  '/' σt ) ']'  '/' :  Φ ']'").
 
 Notation "⊨{ fs , ft } f1 ≥ᶠ f2" :=
-  (sim_local_fun wsat vrel_expr fs ft end_call_sat f1 f2)
+  (sim_local_fun wsat vrel fs ft end_call_sat f1 f2)
   (at level 70, format "⊨{ fs , ft }  f1  ≥ᶠ  f2").
 
 Instance dom_proper `{Countable K} {A : cmraT} :

theories/sim/local.v

@@ -9,18 +9,9 @@ Set Default Proof Using "Type".
 Section local.
 Context {A: ucmraT}.
 Variable (wsat: A → state → state → Prop).
-Variable (vrel: A → expr → expr → Prop).
+Variable (vrel: A → value → value → Prop).
 Variable (fns fnt: fn_env).
 
-Definition rrel (vrel: A → expr → expr → Prop) (r: A) (es et: expr) : Prop :=
-  ∀ vt, to_result et = Some vt → ∃ vs, to_result es = Some vs ∧
-    match vs, vt with
-    | ValR vs, ValR vt => vrel r (Val vs) (Val vt)
-    | PlaceR ls ts Ts, PlaceR lt t_t Tt =>
-        vrel r #[ScPtr ls ts]%E #[ScPtr lt t_t]%E ∧ Ts = Tt
-    | _, _ => False
-    end.
-
 Notation PRED := (A → nat → result → state → result → state → Prop)%type.
 Notation SIM := (A → nat → expr → state → expr → state → PRED → Prop)%type.
 
@@ -42,24 +33,22 @@ 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 fns)))
     (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang fnt)))
-    fid el_tgt
-    el_src σ1_src
+    fid (vl_tgt: list value)
+    (vl_src: list value) σ1_src
     rc rv
     (* tgt is ready to make a call of [name] *)
-    (CALLTGT: et = fill Kt (Call #[ScFnPtr fid] el_tgt))
-    (VTGT: Forall (λ ei, is_Some (to_value ei)) el_tgt)
+    (CALLTGT: et = fill Kt (Call #[ScFnPtr fid] (Val <$> vl_tgt)))
     (* src is ready to make a call of [name] *)
-    (CALLSRC: (es, σs) ~{fns}~>* (fill Ks (Call #[ScFnPtr fid] el_src), σ1_src))
-    (VSRC: Forall (λ ei, is_Some (to_value ei)) el_src)
+    (CALLSRC: (es, σs) ~{fns}~>* (fill Ks (Call #[ScFnPtr fid] (Val <$> 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) el_src el_tgt)
+    (VREL: Forall2 (vrel 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
                 related w.r.t. (r ⋅ r' ⋅ r_f) *)
-             (VRET: vrel r' (Val v_src) (Val v_tgt))
+             (VRET: vrel r' v_src v_tgt)
              (STACK: σt.(scs) = σt'.(scs)),
         ∃ idx', sim_local_body (rc ⋅ r') idx'
                                (fill Ks (Val v_src)) σs'
@@ -129,7 +118,7 @@ Qed.
 Definition sim_local_fun
   (esat: A → state → state → Prop) (fn_src fn_tgt : function) : Prop :=
   ∀ r es et (vl_src vl_tgt: list value) σs σt
-    (VALEQ: Forall2 (vrel r) (Val <$> vl_src) (Val <$> vl_tgt))
+    (VALEQ: Forall2 (vrel r) vl_src vl_tgt)
     (EQS: match fn_src with
           | FunV xl e => subst_l xl (Val <$> vl_src) e = Some es
           end)
@@ -138,10 +127,11 @@ Definition sim_local_fun
           end),
     ∃ idx, sim_local_body r idx
                           (InitCall es) σs (InitCall et) σt
-                          (λ r' _ vs' σs' vt' σt',
+                          (λ r' _ rs' σs' rt' σt',
                             (∃ c, σt'.(scs) = c :: σt.(scs)) ∧
                             esat r' σs' σt' ∧
-                            vrel r' (of_result vs') (of_result vt')).
+                            (∃ vs' vt', rs' = ValR vs' ∧ rt' = ValR vt' ∧
+                               vrel r' vs' vt')).
 
 Definition sim_local_funs (esat: A → state → state → Prop) : Prop :=
   ∀ name fn_tgt, fnt !! name = Some fn_tgt → ∃ fn_src,

theories/sim/local_adequacy.v

@@ -46,9 +46,9 @@ 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_expr r' (Val v_src) (Val v_tgt))
+         (VRET  : vrel r' v_src v_tgt)
          (CIDS: σ_tgt'.(scs) = frame.(callids)),
-         ∃ idx', sim_local_body wsat vrel_expr fns fnt
+         ∃ idx', sim_local_body wsat vrel fns fnt
                                 (frame.(rc) ⋅ r') idx'
                                 (fill frame.(K_src) (Val v_src)) σ_src'
                                 (fill frame.(K_tgt) (Val v_tgt)) σ_tgt'
@@ -71,7 +71,7 @@ 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_expr fns fnt rc idx e_src σ_src e_tgt σ_tgt
+    (LOCAL: sim_local_body wsat vrel fns fnt rc idx e_src σ_src e_tgt σ_tgt
                            (λ r _ vs σs vt σt,
                               (∃ c, σt.(scs) = c :: cids) ∧
                               end_call_sat r σs σt ∧
@@ -82,7 +82,7 @@ Inductive sim_local_conf:
   : sim_local_conf idx Ke_src σ_src Ke_tgt σ_tgt.
 
 Lemma sim_local_conf_sim
-      (FUNS: sim_local_funs wsat vrel_expr fns fnt end_call_sat)
+      (FUNS: sim_local_funs wsat vrel 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)
@@ -148,7 +148,9 @@ Proof.
                     end), r'.(rlm)).
       have SIMEND : r' ⊨{idx',fns,fnt} (EndCall vs1, σs) ≥ (EndCall vt1, σt) : Φ.
       { apply sim_body_end_call; auto.
-        clear. intros. rewrite /Φ. naive_solver. }
+        clear. intros. rewrite /Φ. split; last naive_solver.
+        eexists _, _. done.
+      }
 
       have NONE : to_result (EndCall e_tgt0) = None. by done.
       destruct (fill_tstep_inv _ _ _ _ _ _ NONE H) as [et2 [? STEPT2]].
@@ -166,18 +168,20 @@ Proof.
       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.
+      destruct HΦ2 as [VR2 HP2].
+      destruct VR2 as (? & ? & [=<-] & [=<-] & VR2).
 
       exploit (CONTINUATION r2).
       { rewrite cmra_assoc; eauto. }
-      { apply HΦ2. }
+      { exact VR2. }
       { exploit tstep_end_call_inv; try exact STEPT2; eauto. i. des. subst. ss.
-        rewrite x2 in x7. inv x7. ss.
+        rewrite x2 in x7. simplify_eq. ss.
       }
       intros [idx3 SIMFR]. rename σ2_tgt into σt2.
       do 2 eexists. split.
       - left. apply fill_tstep_tc. eapply tc_rtc_l; [|apply STEPS].
         apply (fill_tstep_rtc _ [EndCallCtx]).
-        clear -x. destruct x as [|[]]. by apply tc_rtc. simplify_eq; constructor.
+        clear -x. destruct x as [|[]]. by apply tc_rtc. simplify_eq. constructor.
 
       - right. apply CIH. econs; eauto.
         + rewrite fill_app. eauto.
@@ -196,12 +200,14 @@ Proof.
       * right. apply CIH. econs; eauto.
     + (* call *)
       exploit fill_step_inv_2; eauto. i. des; ss.
-      exploit tstep_call_inv; try exact x2; eauto. i. des. subst.
+      exploit tstep_call_inv.
+      { eapply list_Forall_to_value. eauto. }
+      { exact x2. }
+      eauto. i. des. subst.
       destruct (FUNS _ _ x3) as ([xls ebs HCss] & Eqfs & Eql & SIMf).
-      destruct (subst_l_is_Some xls el_src ebs) as [ess Eqss].
-      { by rewrite (Forall2_length _ _ _ VREL) -(subst_l_is_Some_length _ _ _ _ x4). }
-      apply list_Forall_to_value in VSRC. destruct VSRC as [vl_src ->].
-      apply list_Forall_to_value in VTGT. destruct VTGT as [vl_tgt ->].
+      destruct (subst_l_is_Some xls (Val <$> vl_src) ebs) as [ess Eqss].
+      { rewrite fmap_length (Forall2_length _ _ _ VREL).
+        rewrite Eql (subst_l_is_Some_length _ _ _ _ x4) fmap_length //. }
       specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VREL Eqss x4) as [idx2 SIMf].
       esplits.
       * left. eapply tc_rtc_l.
@@ -210,11 +216,12 @@ Proof.
           econs; econs; eauto. apply list_Forall_to_value. eauto. }
       * right. apply CIH. econs.
         { econs 2; eauto. i. instantiate (1 := mk_frame _ _ _ _). ss.
-          destruct (CONT _ _ _ σ_src' σ_tgt' VRET).
+          destruct (CONT r' v_src v_tgt σ_src' σ_tgt' VRET).
           { rewrite CIDS. eauto. }
           pclearbot. esplits; eauto.
         }
-        { eapply sim_local_body_post_mono; [|apply SIMf]. simpl. naive_solver. }
+        { eapply sim_local_body_post_mono; [|apply SIMf]. simpl.
+          unfold vrel_expr. naive_solver. }
         { done. }
         { s. rewrite -fill_app. eauto. }
         { ss. rewrite -cmra_assoc; eauto. }

theories/sim/program.v

@@ -11,7 +11,7 @@ Lemma sim_prog_sim_classical
                     exists e' σ', (e, σ) ~{prog_src}~>* (e', σ') /\
                              ~ terminal e' /\
                              ~ reducible prog_src e' σ'}
-      (FUNS: sim_local_funs wsat vrel_expr prog_src prog_tgt end_call_sat)
+      (FUNS: sim_local_funs wsat vrel prog_src prog_tgt end_call_sat)
       (MAINT: ∃ ebt HCt, prog_tgt !! "main" = Some (@FunV [] ebt HCt))
   : behave_prog prog_tgt <1= behave_prog prog_src.
 Proof.

theories/sim/refl_step.v

@@ -955,7 +955,7 @@ Lemma sim_body_end_call fs ft r n vs vt σs σt Φ :
                  | Some (Cinl (Excl T)) => <[c2 := to_callStateR csPub]> r.(rcm)
                  | _ => r.(rcm)
                  end in
-      Wf σt → vrel_expr ((r.(rtm), r2'), r.(rlm)) vs vt →
+      Wf σt → vrel ((r.(rtm), r2'), r.(rlm)) vs vt →
       Φ ((r.(rtm), r2'), r.(rlm)) n (ValR vs) σs' (ValR vt) σt' : Prop) →
   r ⊨{n,fs,ft} (EndCall (Val vs), σs) ≥ (EndCall (Val vt), σt) : Φ.
 Proof.
@@ -1044,7 +1044,6 @@ Proof.
     - intros ???. rewrite /=. apply LINV. }
   (* result *)
   left. apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
-  have ?: vrel_expr ((r.(rtm), r2'), r.(rlm)) vs vt by do 2 eexists; eauto.
   intros VALID'.
   eapply POST; eauto. destruct SREL as (?&?&Eqs&?). by rewrite Eqs.
 Qed.
@@ -1064,7 +1063,7 @@ 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] el_tgt)) as [[] ?];
+    destruct (fill_result ft K' (Call #[ScFnPtr fid] (Val <$> vl_tgt))) as [[] ?];
       [rewrite Eq; by eexists|done]. }
   specialize (STEP _ _ STEPT) as (es1 & σs1 & r1 & n1 & STEP1 & WSAT1 & SIMV).
   have STEPK: (EndCall #vs, σs) ~{fs}~>* (es1, σs1).
@@ -1112,7 +1111,7 @@ 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] el_tgt)) as [[] ?];
+    destruct (fill_result ft K' (Call #[ScFnPtr fid] (Val <$> vl_tgt))) as [[] ?];
       [rewrite Eq; by eexists|done]. }
   specialize (STEP _ _ STEPT) as (es1 & σs1 & r1 & n1 & STEP1 & WSAT1 & SIMV).
   have STEPK: (EndCall #vs, σs) ~{fs}~>* (es1, σs1).
@@ -1149,24 +1148,23 @@ Qed.
 Lemma sim_body_step_over_call fs ft
   (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
   (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft)))
-  rc rv n fid els xlt et et' elt HCt σs σt Φ
-  (VS  : Forall (λ ei, is_Some (to_value ei)) els)
-  (VREL: Forall2 (vrel_expr rv) els elt)
+  rc rv n fid vls xlt et et' vlt HCt σs σt Φ
+  (VREL: Forall2 (vrel rv) vls vlt)
   (FT: ft !! fid = Some (@FunV xlt et HCt))
-  (VT : Forall (λ ei, is_Some (to_value ei)) elt)
-  (ST: subst_l xlt elt et = Some et') :
+  (ST: subst_l xlt (Val <$> vlt) et = Some et') :
   (∀ r' vs vt σs' σt' (VRET: vrel r' vs vt) (STACK: σt.(scs) = σt'.(scs)), ∃ n',
     rc ⋅ r' ⊨{n',fs,ft} (fill Ks (Val vs), σs') ≥ (fill Kt (Val vt), σt') : Φ) →
   rc ⋅ rv ⊨{n,fs,ft}
-    (fill Ks (Call #[ScFnPtr fid] els), σs) ≥ (fill Kt (Call #[ScFnPtr fid] elt), σt) : Φ.
+    (fill Ks (Call #[ScFnPtr fid] (Val <$> vls)), σs) ≥ (fill Kt (Call #[ScFnPtr fid] (Val <$> vlt)), σt) : Φ.
 Proof.
   intros CONT. pfold. intros NT r_f WSAT. split.
   { right. exists (fill Kt (EndCall (InitCall et'))), σt.
-     eapply (head_step_fill_tstep _ Kt). econstructor. by econstructor. }
+     eapply (head_step_fill_tstep _ Kt). econstructor. econstructor; try done.
+     apply list_Forall_to_value. eauto. }
   { intros vt. by rewrite fill_not_result. }
   eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
-            Ks _ fid elt els); eauto; [done|].
-  intros r' ? ? σs' σt' (vs&vt&?&?&VR) STACK. simplify_eq.
+            Ks _ fid vlt vls); eauto; [done|].
+  intros r' ? ? σs' σt' VR STACK. simplify_eq.
   destruct (CONT _ _ _ σs' σt' VR STACK) as [n' ?].
   exists n'. by left.
 Qed.