Modify the relational interpretation to account for masks/invariants

F_mu_ref_conc/examples/lock.v

 From iris.proofmode Require Import tactics.
 From iris_logrel.F_mu_ref_conc Require Import tactics.
-From iris_logrel.F_mu_ref_conc Require Export rules_binary typing fundamental_binary.
+From iris_logrel.F_mu_ref_conc Require Export rules_binary typing fundamental_binary relational_properties.
 From iris.base_logic Require Import namespaces.
 
 (** [newlock = alloc false] *)
@@ -206,18 +206,19 @@ Section proof.
     by iFrame.
   Qed.
 
-  Lemma bin_log_related_with_lock_r Γ K P Q e v w l t τ :
+  Lemma bin_log_related_with_lock_r Γ K E1 E2 P Q e v w l t τ :
+    (nclose specN ⊆ E1) →
     (∀ f, e.[f] = e) (* e is a closed term *) →
     (∀ f, (of_val v).[f] = of_val v) (* v is a closed term *) →
     (∀ f, (of_val w).[f] = of_val w) (* w is a closed term *) →
     (∀ ρ j K', spec_ctx ρ -∗ P -∗ j ⤇ fill K' (App e (of_val w))
-            ={⊤}=∗ j ⤇ fill K' (of_val v) ∗ Q) →
+            ={E1}=∗ j ⤇ fill K' (of_val v) ∗ Q) →
     P -∗
     l ↦ₛ (#♭v false) -∗
-    (l ↦ₛ (#♭v false) -∗ Q -∗ Γ ⊨ t ≤log≤ fill K (of_val v) : τ)%I
-    -∗ Γ ⊨ t ≤log≤ fill K (App (with_lock e (Loc l)) (of_val w)) : τ.
+    (l ↦ₛ (#♭v false) -∗ Q -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (of_val v) : τ)%I
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App (with_lock e (Loc l)) (of_val w)) : τ.
   Proof.
-    iIntros (????) "HP Hl Hlog".
+    iIntros (?????) "HP Hl Hlog".
     pose (Φ := (fun (w: val) => ⌜w = v⌝ ∗ Q ∗ l ↦ₛ (#♭v false))%I).
     iApply (bin_log_related_step_r Φ with "[HP Hl]").
     { intros. 

F_mu_ref_conc/examples/stack/refinement.v

@@ -92,8 +92,9 @@ Section Stack_refinement.
       tp_bind j (App (of_val f2) _).
       iSpecialize ("Hff" $! (y1, y2) with "[Hy]"); first by iFrame.
       iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl.
+      iApply fupd_wp. iMod "Hff". iModIntro.
       iApply (wp_wand with "Hff").
-      iIntros (v). iDestruct 1 as (v2) "[Hj [% %]]".
+      iIntros (v). iMod 1 as (v2) "[Hj [% %]]".
       tp_normalise j. asimpl.
       iApply fupd_wp. tp_rec j; auto using to_of_val.
       asimpl.
@@ -161,7 +162,8 @@ Section Stack_refinement.
       congruence. iNext. iIntros "Hst".
       close_sinv "Hclose" "[HLK Hst Hoe Hl Hst' Histk']".
       iApply wp_if_false. iNext.
-      iApply "IH". iFrame.
+      iMod ("IH" with "Hj") as "IH'".
+      iApply "IH'". 
   Qed.
 
   Lemma FG_CG_pop_refinement ρ st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ}:
@@ -198,7 +200,7 @@ Section Stack_refinement.
       iApply wp_case_inl; auto. iNext.
       iApply wp_value; auto. 
       iExists (InjLV ())%V. iFrame "Hj".
-      iLeft. iExists (_,_). iSplit; auto.
+      iLeft. iExists (_,_). iModIntro. iSplit; auto.
     + close_sinv "Hclose" "[Hoe Hst' Hst Hl]".
       wp_bind (Unfold _). iApply wp_fold; first auto. iNext.
       iApply wp_rec; first auto. iNext. asimpl.
@@ -250,14 +252,14 @@ Section Stack_refinement.
         iModIntro.
         iApply wp_value; try by rewrite /= ?to_of_val /=.
         iExists (InjRV zn1). iFrame "Hj".
-        iRight. iExists (_,_). simpl. iSplit; auto.
+        iRight. iExists (_,_). simpl. iModIntro. iSplit; auto.
       * (* CAS fails *)
         iApply (wp_cas_fail with "Hst"); try by (rewrite /= ?to_of_val /=).
         congruence.        
         iNext. iIntros "Hst".
         close_sinv "Hclose" "[-Hj]".
         iApply wp_if_false. iNext. 
-        by iApply "IH".
+        by iMod ("IH" with "Hj").
   Qed.
     
   (* ∀ α. (α → Unit) * (Unit → Unit + α) * ((α → Unit) → Unit) *)
@@ -278,7 +280,7 @@ Section Stack_refinement.
            (TArrow (TVar 0) TUnit)
            (TArrow TUnit (TSum TUnit (TVar 0))))
            (TArrow (TArrow (TVar 0) TUnit) TUnit))).
-    clear j K. iAlways. iIntros (τi) "%". 
+    clear j K. iModIntro. iAlways. iIntros (τi) "%". 
     iIntros (j K) "Hj /=".
     iApply fupd_wp.
     tp_tlam j.
@@ -324,7 +326,7 @@ Section Stack_refinement.
     iApply wp_value; first by eauto. 
     iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (RecV _)).
     simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj".   
-    iExists (_, _), (_, _); iSplit; eauto.
+    iExists (_, _), (_, _); iModIntro; iSplit; eauto.
     iSplit.
     (* refinement of push and pop *)
     - iExists (_, _), (_, _); iSplit; eauto. iSplit.
@@ -332,7 +334,7 @@ Section Stack_refinement.
         (* TODO: fold (interp (...)) does not work here *)
         change (□ (∀ vv : prodC valC valC,
      □ τi vv
-     → interp_expr interp_unit (τi :: Δ)
+     → interp_expr ⊤ ⊤ interp_unit (τi :: Δ)
          ((rec: (rec: if: CAS #stk (Var 1)
                             (Fold (ref InjR (Var 3, Var 1)))
                       then () else (Var 2) (Var 3)) 

F_mu_ref_conc/logrel_binary.v

@@ -32,13 +32,13 @@ Section logrel.
   Implicit Types Δ : listC D.
   Implicit Types interp : listC D → D.
 
-  Definition interp_expr (τi : listC D -n> D) (Δ : listC D)
+  Definition interp_expr (E1 E2 : coPset) (τi : listC D -n> D) (Δ : listC D)
       (ee : expr * expr) : iProp Σ := (∀ j K,
     j ⤇ fill K (ee.2) -∗
-    WP ee.1 {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
-  Global Instance interp_expr_ne n :
-    Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr.
-  Proof. solve_proper. Qed.
+    |={E1,E2}=> WP ee.1 @ E2 {{ v, |={E2}=> ∃ v', j ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
+  Global Instance interp_expr_ne n E1 E2:
+    Proper (dist n ==> dist n ==> (=) ==> dist n) (interp_expr E1 E2).
+  Proof. solve_proper. Qed.       
 
   Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ ww,
     (□ from_option id (cconst True)%I (Δ !! x) ww)%I.
@@ -71,7 +71,7 @@ Section logrel.
           (interp1 interp2 : listC D -n> D) : listC D -n> D :=
     λne Δ ww,
     (□ ∀ vv, interp1 Δ vv →
-             interp_expr
+             interp_expr ⊤ ⊤
                interp2 Δ (App (of_val (ww.1)) (of_val (vv.1)),
                           App (of_val (ww.2)) (of_val (vv.2))))%I.
   Solve Obligations with solve_proper. 
@@ -80,7 +80,7 @@ Section logrel.
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
     (□ ∀ τi,
           ⌜∀ ww, PersistentP (τi ww)⌝ →
-          interp_expr
+          interp_expr ⊤ ⊤
             interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
   Solve Obligations with solve_proper.
 
@@ -245,5 +245,5 @@ End logrel.
 
 Typeclasses Opaque interp_env.
 Notation "⟦ τ ⟧" := (interp τ).
-Notation "⟦ τ ⟧ₑ" := (interp_expr (interp τ)).
+Notation "⟦ τ ⟧ₑ" := (interp_expr ⊤ ⊤ (interp τ)).
 Notation "⟦ Γ ⟧*" := (interp_env Γ).

F_mu_ref_conc/soundness_binary.v

@@ -25,15 +25,20 @@ Proof.
   { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
   set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
   iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
-  iApply wp_fupd. iApply wp_wand_r.
+  iApply wp_fupd.
+  iApply wp_wand_r.
   iSplitL.
   iPoseProof (Hlog _ _) as "Hrel". 
   iSpecialize ("Hrel" $! [] [] with "* [$Hcfg] []").
   { iAlways. iApply logrel_binary.interp_env_nil.  }
   simpl.
-  rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
+  rewrite empty_env_subst empty_env_subst. 
+  iSpecialize ("Hrel" $! 0 []).
+  iAssert (0 ⤇ e')%I with "[Hcfg2]" as "H0".
   { rewrite tpool_mapsto_eq /tpool_mapsto_def. asimpl. iFrame. }
-  iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
+  iApply fupd_wp. iApply "Hrel"; auto.
+  iIntros (v1).
+  iMod 1 as (v2) "[Hj #Hinterp]". 
   iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
   rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
   iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.

F_mu_ref_conc/weakestpre.v

@@ -14,8 +14,8 @@ Implicit Types v : val.
 Implicit Types e : expr.
 
 (* Inverse bind lemma *)
-Lemma wp_bind_inv K  e Φ :
-  WP fill K e {{ Φ }} ⊢ WP e {{ v, WP fill K (of_val v)  {{ Φ }} }}.
+Lemma wp_bind_inv K E e Φ :
+  WP fill K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (e Φ). rewrite wp_unfold /wp_pre.
   iDestruct "H" as "[Hv|[% H]]".
@@ -33,7 +33,7 @@ Proof.
   destruct eval.
   - iApply wp_value. symmetry. eauto.
     replace e with (of_val v) in H; last first.
-    { by rewrite (of_to_val e). }
+    { by rewrite (of_to_val e). } 
     rewrite wp_unfold /wp_pre; iRight; iSplit; eauto.
     iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]".
     iModIntro; iSplit.

_CoqProject

@@ -29,6 +29,7 @@ F_mu_ref_conc/rules.v
 F_mu_ref_conc/typing.v
 F_mu_ref_conc/logrel_unary.v
 F_mu_ref_conc/fundamental_unary.v
+F_mu_ref_conc/relational_properties.v
 F_mu_ref_conc/rules_binary.v
 F_mu_ref_conc/logrel_binary.v
 F_mu_ref_conc/weakestpre.v

prelude/base.v

@@ -31,6 +31,7 @@ Ltac properness :=
   | |- (WP _ {{ _ }})%I ≡ (WP _ {{ _ }})%I => apply wp_proper =>?
   | |- (▷ _)%I ≡ (▷ _)%I => apply later_proper
   | |- (□ _)%I ≡ (□ _)%I => apply always_proper
+  | |- (|={_,_}=> _ )%I ≡ (|={_,_}=> _ )%I => apply fupd_proper
   | |- (_ ∗ _)%I ≡ (_ ∗ _)%I => apply sep_proper
   | |- (inv _ _)%I ≡ (inv _ _)%I => apply (contractive_proper _)
   end.