fix function results; add lemma for var

theories/lang/steps_inversion.v

@@ -186,6 +186,24 @@ Proof. apply never_stuck_tstep_tc'. Qed.
 
 (** PURE STEP ----------------------------------------------------------------*)
 
+(** Var *)
+Lemma fill_var_decompose K e var:
+  fill K e = Var var →
+  K = [] ∧ e = Var var.
+Proof.
+  revert e.
+  induction K as [|Ki K IH]; [done|]. simpl; intros ? [? ?]%IH.
+  by destruct Ki.
+Qed.
+
+Lemma tstep_var_inv var e' σ σ' :
+  (Var var, σ) ~{fns}~> (e', σ') → False.
+Proof.
+  intros STEP. inv_tstep. symmetry in Eq.
+  destruct (fill_var_decompose _ _ _ Eq); subst.
+  simpl in HS. inv_head_step.
+Qed.
+
 (** BinOp *)
 Lemma fill_bin_op_decompose K e op e1 e2:
   fill K e = BinOp op e1 e2 →

theories/sim/instance.v

@@ -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 rrel 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 ) ']'  '/' :  Φ ']'").
 
 
@@ -14,7 +14,7 @@ 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 rrel fs ft end_call_sat f1 f2.
+           sim_local_fun wsat vrel 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,
@@ -67,7 +67,7 @@ Qed.
 assumption. *)
 Lemma sim_mod_funs_local fs ft :
   sim_mod_funs fs ft →
-  sim_local_funs wsat rrel fs ft end_call_sat.
+  sim_local_funs wsat vrel fs ft end_call_sat.
 Proof.
   intros Hmod. intros f fn_src Hlk.
   destruct (Hmod _ _ Hlk) as (fn_tgt & ? & ? & ?). exists fn_tgt.
@@ -84,3 +84,47 @@ Proof.
   intros Hne (ebs & HCs & EQ). exists ebs, HCs.
   rewrite lookup_insert_ne //.
 Qed.
+
+Lemma rrel_eq  r (e1 e2: result) :
+  rrel vrel r e1 e2 → e1 = e2.
+Proof.
+  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 rrel_mono (r1 r2 : resUR) (VAL: ✓ r2) :
+  r1 ≼ r2 → ∀ v1 v2, rrel vrel r1 v1 v2 → rrel vrel r2 v1 v2.
+Proof.
+  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 list_Forall_result_value (es: list result) (vs: list value) :
+  of_result <$> es = Val <$> vs → es = ValR <$> vs.
+Proof.
+  revert vs. induction es as [|e es IH]; intros vs.
+  { intros Eq. symmetry in Eq. apply fmap_nil_inv in Eq. by subst vs. }
+  destruct vs as [|v vs]; [by intros ?%fmap_nil_inv|].
+  rewrite 3!fmap_cons. intros Eq.
+  inversion Eq as [Eq1].
+  rewrite (IH vs) //. f_equal.
+  have Eq2 := to_of_result e. rewrite Eq1 /= in Eq2. by simplify_eq.
+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) →
+  Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> et) →
+  ∃ vs vt,  es = ValR <$> vs ∧ et = ValR <$> vt ∧
+  Forall2 (vrel r) vs vt.
+Proof.
+  intros RREL [vs Eqs]%list_Forall_to_value [vt Eqt]%list_Forall_to_value.
+  exists vs, vt.
+  apply list_Forall_result_value in Eqs.
+  apply list_Forall_result_value in Eqt. subst es et.
+  do 2 (split; [done|]).
+  by rewrite -> Forall2_fmap in RREL.
+Qed.
+

theories/sim/invariant.v

@@ -101,16 +101,6 @@ Definition wsat (r: resUR) (σs σt: state) : Prop :=
 (* Values passed among functions are public *)
 Definition vrel (r: resUR) (v1 v2: value) := Forall2 (arel 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 *)
 (* The call id [c] to be end must not have any privately protected locations. *)
 Definition end_call_sat (r: resUR) (c: call_id) : Prop :=
@@ -148,14 +138,6 @@ Proof.
   f_equal. by apply (arel_eq _ _ _ Eq1). by apply IH.
 Qed.
 
-Lemma rrel_eq r (e1 e2: result) :
-  rrel r e1 e2 → e1 = e2.
-Proof.
-  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 arel_mono (r1 r2 : resUR) (VAL: ✓ r2) :
   r1 ≼ r2 → ∀ s1 s2, arel r1 s1 s2 → arel r2 s1 s2.
 Proof.
@@ -184,14 +166,6 @@ 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 rrel_mono (r1 r2 : resUR) (VAL: ✓ r2) :
-  r1 ≼ r2 → ∀ v1 v2, rrel r1 v1 v2 → rrel r2 v1 v2.
-Proof.
-  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) :
   r1 ≼ r2 → ∀ l t, priv_loc r1 l t → priv_loc r2 l t.
 Proof.

theories/sim/local.v

@@ -9,9 +9,18 @@ Set Default Proof Using "Type".
 Section local.
 Context {A: ucmraT}.
 Variable (wsat: A → state → state → Prop).
-Variable (rrel: A → result → result → Prop).
+Variable (vrel: A → value → value → Prop).
 Variable (fs ft: fn_env).
 
+Definition rrel (r: A) 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.
+
 Notation PRED := (A → nat → result → state → result → state → Prop)%type.
 Notation SIM := (A → nat → expr → state → expr → state → PRED → Prop)%type.
 
@@ -122,10 +131,10 @@ Definition fun_post (esat: A → call_id → Prop) initial_call_id_stack
   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 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),
+  ∀ 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),
     ∃ idx, sim_local_body r idx
                           (InitCall es) σs (InitCall et) σt
                           (fun_post esat σt.(scs)).

theories/sim/local_adequacy.v

@@ -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  : rrel r' v_src v_tgt)
+         (VRET  : rrel vrel r' v_src v_tgt)
          (CIDS: σ_tgt'.(scs) = frame.(callids)),
-         ∃ idx', sim_local_body wsat rrel fns fnt
+         ∃ 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'
                                 (λ r _ vs σs vt σt,
                                   (∃ c, σt.(scs) = c :: cids ∧ end_call_sat r c) ∧
-                                  rrel r vs vt))
+                                  rrel vrel 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 rrel 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 c) ∧
-                              rrel r vs vt))
+                              rrel vrel 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 rrel 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)
@@ -134,7 +134,7 @@ Proof.
       simplify_eq.
 
       set Φ : resUR → nat → result → state → result → state → Prop :=
-        λ r2 _ vs2 σs2 vt2 σt2, rrel r2 vs2 vt2 ∧
+        λ r2 _ vs2 σs2 vt2 σt2, rrel vrel 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) ∧
@@ -206,12 +206,17 @@ Proof.
       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.
+      apply list_Forall_rrel_vrel in VREL as (vs & vt & ? & ? & VREL); [|done..].
+      subst vl_src vl_tgt.
+      rewrite -list_fmap_compose in Eqss.
+      rewrite -list_fmap_compose in x4.
       specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VREL Eqss x4) as [idx2 SIMf].
       esplits.
       * 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. }
+          econs. eapply (CallBS _ _ _ _ xls ebs); eauto.
+          rewrite -list_fmap_compose. 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').

theories/sim/program.v

@@ -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 rrel prog_src prog_tgt end_call_sat)
+      (FUNS: sim_local_funs wsat vrel prog_src prog_tgt end_call_sat)
   : behave_prog prog_tgt <1= behave_prog prog_src.
 Proof.
   destruct MAINT as (ebs & HCs & Eqs).
@@ -32,7 +32,7 @@ Proof.
     intros. simpl. exists 1%nat.
     apply sim_body_result.
     intros VALID.
-    have ?: rrel (init_res ⋅ r') vs vt.
+    have ?: rrel vrel (init_res ⋅ r') vs vt.
     { eapply rrel_mono; [done|apply cmra_included_r|exact VRET]. }
     split; [|done].
     exists O. split; [by rewrite -STACKT|].

theories/sim/refl.v

@@ -47,12 +47,12 @@ Context (css cst: call_id_stack).
 Definition sem_steps := 10%nat.
 
 Definition sem_post (r: resUR) (n: nat) rs css' rt cst': Prop :=
-  n = sem_steps ∧ css' = css ∧ cst' = cst ∧ rrel r rs rt.
+  n = sem_steps ∧ css' = css ∧ cst' = cst ∧ rrel vrel r rs rt.
 
 (** We define a "semantic well-formedness", in some context. *)
 Definition sem_wf (r: resUR) es et :=
   ∀ xs : list (string * (result * result)),
-    Forall (λ '(_, (rs, rt)), rrel r rs rt) xs →
+    Forall (λ '(_, (rs, rt)), rrel vrel r rs rt) xs →
     r ⊨ˢ{sem_steps,fs,ft}
       (subst_map (prod_map id fst <$> xs) es, css)
     ≥

theories/sim/refl_step.v

@@ -1138,7 +1138,7 @@ Qed.
 
 (** EndCall *)
 Lemma end_call_tstep_src_tgt fs ft r_f r σs σt (rs rt: result) es' σs' :
-  rrel r rs rt →
+  rrel vrel 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.
@@ -1158,7 +1158,7 @@ Qed.
 
 Lemma sim_body_end_call fs ft r n rs rt σs σt Φ :
   (* return values are related *)
-  rrel r rs rt →
+  rrel vrel 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 vs vt,
@@ -1281,7 +1281,7 @@ Lemma sim_body_step_over_call fs ft
   rc rv n fid vls vlt σs σt Φ
   (VREL: Forall2 (vrel rv) vls vlt)
   (FUNS: sim_local_funs_lookup fs ft) :
-  (∀ r' vs vt σs' σt' (VRET: rrel r' vs vt)
+  (∀ r' vs vt σs' σt' (VRET: rrel 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') : Φ) →
@@ -1314,6 +1314,15 @@ Proof.
   by rewrite Eqcss' Eqcss.
 Qed.
 
+
+Lemma sim_body_var fs ft r n σs σt var Φ :
+  r ⊨{n,fs,ft} (Var var, σs) ≥ (Var var, σt) : Φ.
+Proof.
+  pfold. intros NT r_f WSAT.
+  destruct (NT (Var var) σs) as [[]|[? [? RED%tstep_var_inv]]];
+    [constructor|done..].
+Qed.
+
 (** Let *)
 Lemma sim_body_let fs ft r n x es1 es2 et1 et2 σs σt Φ :
   terminal es1 → terminal et1 →

theories/sim/simple.v

@@ -13,7 +13,7 @@ From stbor.sim Require Import refl_step.
 Definition fun_post_simple
   initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst :=
   (∃ c, cst = c::initial_call_id_stack ∧ end_call_sat r c) ∧
-  rrel r vs vt.
+  rrel vrel r vs vt.
 
 Definition sim_simple fs ft r n es css et cst
   (Φ : resUR → nat → result → call_id_stack → result → call_id_stack → Prop) : Prop :=
@@ -71,8 +71,8 @@ Proof.
   destruct vls as [|vs []]; [done| |done].
   destruct vlt as [|vt []]; [done| |done].
   inversion FREL as [|???? RREL]. intros _ _. simplify_eq.
-  (* eapply sim_simplify; last by eapply HH. done. *)
-Admitted.
+  eapply sim_simplify; last by eapply HH. done.
+Qed.
 
 Lemma sim_simple_bind fs ft
   (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
@@ -119,7 +119,7 @@ Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
   sim_local_funs_lookup fs ft →
   Forall2 (vrel rv) vls vlt →
   r ≡ r' ⋅ rv →
-  (∀ rret vs vt, rrel rret vs vt →
+  (∀ rret vs vt, rrel vrel rret vs vt →
     r' ⋅ rret ⊨ˢ{n',fs,ft} (of_result vs, css) ≥ (of_result vt, cst) : Φ) →
   r ⊨ˢ{n,fs,ft}
     (Call #[ScFnPtr fid] (Val <$> vls), css) ≥ (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.