vrel_expr -> vrel_res

theories/sim/invariant.v

@@ -100,8 +100,8 @@ 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_expr (r: resUR) (e1 e2: expr) :=
-  ∃ v1 v2, e1 = Val v1 ∧ e2 = Val v2 ∧ vrel r v1 v2.
+Definition vrel_res (r: resUR) (e1 e2: result) :=
+  ∃ v1 v2, e1 = ValR v1 ∧ e2 = ValR v2 ∧ vrel r v1 v2.
 
 
 (** Condition for resource before EndCall *)
@@ -146,27 +146,14 @@ Proof.
   f_equal. by apply (arel_eq _ _ _ Eq1). by apply IH.
 Qed.
 
-Lemma vrel_expr_to_result r (e1 e2: result) :
-  vrel_expr r e1 e2 → to_result e1 = Some e2.
+Lemma vrel_res_eq r (e1 e2: result) :
+  vrel_res r e1 e2 → e1 = e2.
 Proof.
-  intros (v1 & v2 & Eq1 & Eq2 & VREL). rewrite Eq1 /=.
-  rewrite (_: (#v2)%E = of_result (ValR v2)) in Eq2; [|done].
-  apply of_result_inj in Eq2. rewrite Eq2. do 2 f_equal. by eapply vrel_eq.
+  intros (v1 & v2 & Eq1 & Eq2 & VREL). subst. f_equal. by eapply vrel_eq.
 Qed.
 
-Lemma vrel_expr_result r (e1 e2: result) :
-  vrel_expr r e1 e2 → ∃ v1 v2, e1 = ValR v1 ∧ e2 = ValR v2 ∧ vrel_expr r (Val v1) (Val v2).
-Proof.
-  intros (v1 & v2 & Eq1 & Eq2 & VREL). exists v1, v2.
-  rewrite (_: (#v1)%E = of_result (ValR v1)) in Eq1; [|done].
-  apply of_result_inj in Eq1. rewrite Eq1.
-  rewrite (_: (#v2)%E = of_result (ValR v2)) in Eq2; [|done].
-  apply of_result_inj in Eq2. rewrite Eq2.
-  repeat split. exists v1, v2. naive_solver.
-Qed.
-
-Lemma vrel_expr_vrel r (v1 v2: value) :
-  vrel_expr r #v1 #v2 → vrel r v1 v2.
+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) :
@@ -197,8 +184,8 @@ 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_expr_mono (r1 r2 : resUR) (VAL: ✓ r2) :
-  r1 ≼ r2 → ∀ v1 v2, vrel_expr r1 v1 v2 → vrel_expr r2 v1 v2.
+Lemma vrel_res_mono (r1 r2 : resUR) (VAL: ✓ r2) :
+  r1 ≼ r2 → ∀ v1 v2, vrel_res r1 v1 v2 → vrel_res r2 v1 v2.
 Proof.
   move => Le v1 v2 [? [? [? [? /(vrel_mono _ _ VAL Le) ?]]]]. do 2 eexists. eauto.
 Qed.

theories/sim/local_adequacy.v

@@ -55,7 +55,7 @@ Inductive sim_local_frames:
                                 (λ r _ vs σs vt σt,
                                   (∃ c, σt.(scs) = c :: cids) ∧
                                   end_call_sat r σs σt ∧
-                                  vrel_expr r (of_result vs) (of_result vt)))
+                                  vrel_res r vs vt))
   : sim_local_frames
       (r_f ⋅ frame.(rc))
       frame.(callids)
@@ -75,7 +75,7 @@ Inductive sim_local_conf:
                            (λ r _ vs σs vt σt,
                               (∃ c, σt.(scs) = c :: cids) ∧
                               end_call_sat r σs σt ∧
-                              vrel_expr r (of_result vs) (of_result vt)))
+                              vrel_res 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)
@@ -112,31 +112,32 @@ Proof.
     apply tstep_reducible_fill_inv in RED; [|done].
     apply tstep_reducible_fill.
     destruct RED as [e2 [σ2 Eq2]].
-    apply vrel_expr_result in VREL as (v1 & v2 & ? & ? & ?). subst vs' vt.
+    destruct VREL as (v1 & v2 & ? & ? & ?). subst vs' vt.
     move : Eq2. eapply end_call_tstep_src_tgt; eauto.
   - 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. eapply vrel_expr_to_result; eauto.
+    + ii. clarify. erewrite to_of_result. f_equal. eapply vrel_res_eq; eauto.
   - guardH sim_local_body_stuck.
     i. destruct eσ2_tgt as [e2_tgt σ2_tgt].
 
     exploit fill_step_inv_2; eauto. i. des; cycle 1.
     { (* return *)
       exploit sim_local_body_terminal; eauto. i. des.
+      rename x2 into HFRAME0.
 
       inv FRAMES; ss.
       { exfalso. apply result_tstep_stuck in H. naive_solver. }
 
       (* Simulatin EndCall *)
       rename σ_tgt into σt. rename σs' into σs.
-      destruct (vrel_expr_result _ _ _ x4) as (vs1 & vt1 & Eqvs1 & Eqv1 & VREL1).
-      simplify_eq. have VR: vrel r' vs1 vt1 by apply vrel_expr_vrel.
+      destruct x4 as (vs1 & vt1 & Eqvs1 & Eqv1 & VR).
+      simplify_eq.
 
       set Φ : resUR → nat → result → state → result → state → Prop :=
-        λ r2 _ vs2 σs2 vt2 σt2, vrel_expr r2 vs2 vt2 ∧
+        λ r2 _ vs2 σs2 vt2 σt2, vrel_res 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) ∧
@@ -168,14 +169,12 @@ 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. }
-      { exact VR2. }
+      { apply vrel_res_vrel. apply HΦ2. }
       { exploit tstep_end_call_inv; try exact STEPT2; eauto. i. des. subst. ss.
-        rewrite x2 in x7. simplify_eq. ss.
+        rewrite HFRAME0 in x5. simplify_eq. ss.
       }
       intros [idx3 SIMFR]. rename σ2_tgt into σt2.
       do 2 eexists. split.
@@ -221,7 +220,7 @@ Proof.
           pclearbot. esplits; eauto.
         }
         { eapply sim_local_body_post_mono; [|apply SIMf]. simpl.
-          unfold vrel_expr. naive_solver. }
+          unfold vrel_res. naive_solver. }
         { done. }
         { s. rewrite -fill_app. eauto. }
         { ss. rewrite -cmra_assoc; eauto. }

theories/sim/program.v

@@ -31,7 +31,7 @@ Proof.
     intros. simpl. exists 1%nat.
     apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
     intros VALID.
-    have ?: vrel_expr (init_res ⋅ r') (of_result #vs) (of_result #vt).
+    have ?: vrel_res (init_res ⋅ r') (#vs) (#vt).
     { do 2 eexists. do 2 (split; [done|]).
       eapply vrel_mono; [done|apply cmra_included_r|done]. }
     split; last split; [..|done].