Add an environment for semantic types (relations)

Modify the logical relation judment to include an environment Δ that
contains a list of semantic types to interpret free type variables.

F_mu_ref_conc/context_refinement.v

@@ -230,12 +230,15 @@ Ltac fold_interp :=
 Section bin_log_related_under_typed_ctx.
   Context `{logrelG Σ}.
 
-  Ltac fundamental :=
+  Ltac fundamental := simpl;
     try (solve_ndisj);
     lazymatch goal with
-    | [ H : _ ⊢ₜ ?e : _ |- (_ ⊢ ?Γ ⊨ ?e ≤log≤ ?e : _)] =>
+    | [ H : _ ⊢ₜ ?e : _ |- (_ ⊢ {_,_;_;?Γ} ⊨ ?e ≤log≤ ?e : _)] =>
       let Z := iFresh in
-      iPoseProof (binary_fundamental _ e _) as Z; [apply H | iFrame Z]
+      iPoseProof (binary_fundamental_masked ⊤ _ _ e _) as Z;
+       [ solve_ndisj..
+       | apply H
+       | try iFrame Z ]
     end.
   Ltac solve_closed_typed :=
     lazymatch goal with
@@ -247,30 +250,32 @@ Section bin_log_related_under_typed_ctx.
     (Closed (dom _ Γ) e) →
     (Closed (dom _ Γ) e') →
     typed_ctx K Γ τ Γ' τ' →
-    □ (Γ ⊨ e ≤log≤ e' : τ) -∗ Γ' ⊨ fill_ctx K e ≤log≤ fill_ctx K e' : τ'.
-  Proof.  
+    (□ (∀ Δ, ({⊤,⊤;Δ;Γ} ⊨ e ≤log≤ e' : τ)) -∗
+     ∀ Δ, □ ({⊤,⊤;Δ;Γ'} ⊨ fill_ctx K e ≤log≤ fill_ctx K e' : τ'))%I.
+  Proof.
     revert Γ τ Γ' τ' e e'.
     induction K as [|k K]=> Γ τ Γ' τ' e e' H1 H2; simpl.
-    - inversion_clear 1; trivial. iIntros "#H"; eauto.
+    - inversion_clear 1; trivial. iIntros "#H".
+      iIntros (Δ) "!#". by iApply "H".
     - inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2].
-      iIntros "#Hrel".
       specialize (IHK _ _ _ _ e e' H1 H2 Hx2).
-      inversion Hx1; subst; simpl; try fold_interp.    
-      + iApply (bin_log_related_rec with "[]"); auto;
+      inversion Hx1; subst; simpl; try fold_interp; iIntros "#Hrel";
+        iIntros (Δ) "!#".
+      + iApply (bin_log_related_rec with "[-]"); auto;
         rewrite ?cons_binder_union.
-        replace ({[x]} ∪ ({[f]} ∪ dom (gset string) Γ'))
-        with  (dom _ (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ')));
-          last by rewrite ?dom_insert_binder.
+        replace ({[x]} ∪ ({[f]} ∪ dom (gset string) _))
+        with  (dom _ (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ'))); last first.
+        { by rewrite !dom_insert_binder. }
         eapply typed_ctx_closed; eauto.
-        replace ({[x]} ∪ ({[f]} ∪ dom (gset string) Γ'))
-        with  (dom _ (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ')));
-          last by rewrite ?dom_insert_binder.
+        replace ({[x]} ∪ ({[f]} ∪ dom (gset string) _))
+        with  (dom _ (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ'))); last first.
+        { by rewrite !dom_insert_binder. }
         eapply typed_ctx_closed; eauto.
         iAlways. iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_app with "[]").
         iApply (IHK with "[Hrel]"); auto.
         fundamental.
-      + iApply (bin_log_related_app with "[]"); try fundamental.
+      + iApply (bin_log_related_app _ _ _ _ _ _ _ τ2 with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_pair with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
@@ -298,15 +303,15 @@ Section bin_log_related_under_typed_ctx.
         end.
         iApply (bin_log_related_case with "[] []"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_if with "[] []"); try fundamental.        
+      + iApply (bin_log_related_if with "[] []"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_if with "[] []"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_if with "[] []"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_nat_binop with "[]"); try fundamental.
+      + iApply (bin_log_related_nat_binop with "[]"); try fundamental; eauto.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_nat_binop with "[]"); try fundamental.
+      + iApply (bin_log_related_nat_binop with "[]"); try fundamental; eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_fold with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
@@ -314,16 +319,17 @@ Section bin_log_related_under_typed_ctx.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_tlam with "[]"); try fundamental.
         (* TODO something wrong with setoids here *)
-        replace (dom (gset string) Γ')
+        replace (dom (gset string) _)
         with (dom (gset string) (subst (ren (+1)) <$> Γ')); last first.
-        { unfold_leibniz. by rewrite dom_fmap. }
+        { unfold_leibniz. by rewrite !dom_fmap. }
         eapply typed_ctx_closed; eauto.
-        replace (dom (gset string) Γ')
+        replace (dom (gset string) _)
         with (dom (gset string) (subst (ren (+1)) <$> Γ')); last first.
-        { unfold_leibniz. by rewrite dom_fmap. }
+        { unfold_leibniz. by rewrite !dom_fmap. }
         eapply typed_ctx_closed; eauto.
-        iAlways. iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_tapp with "[]"); try fundamental.
+        iIntros (τi) "%". iAlways.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_tapp' with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_fork with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
@@ -341,5 +347,5 @@ Section bin_log_related_under_typed_ctx.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_CAS with "[] []"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
-  Qed. 
+  Qed.
 End bin_log_related_under_typed_ctx.

F_mu_ref_conc/examples/counter.v

@@ -31,6 +31,7 @@ Definition FG_counter : val := λ: <>,
 
 Section CG_Counter.
   Context `{logrelG Σ}.
+  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
   
   (* Coarse-grained increment *)  
   Lemma CG_increment_type Γ :
@@ -43,8 +44,8 @@ Section CG_Counter.
     nclose specN ⊆ E1 →
     (x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false) -∗
     (x ↦ₛ (#nv S n) -∗ l ↦ₛ (#♭v false) -∗
-      ({E1,E2;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)) -∗
-    {E1,E2;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ LocV x $/ LocV l) Unit)%E : τ)%I.
+      ({E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)) -∗
+    {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ LocV x $/ LocV l) Unit)%E : τ)%I.
   Proof.
     iIntros (?) "Hx Hl Hlog".
     unfold CG_increment. unlock. simpl_subst/=.
@@ -81,8 +82,8 @@ Section CG_Counter.
 
   Lemma bin_log_FG_increment_l Γ K E x n t τ :
     x ↦ᵢ (#nv n) -∗
-    (x ↦ᵢ (#nv (S n)) -∗ {E,E;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ) -∗
-    {E,E;Γ} ⊨ fill K (FG_increment (Loc x) Unit) ≤log≤ t : τ.
+    (x ↦ᵢ (#nv (S n)) -∗ {E,E;Δ;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ) -∗
+    {E,E;Δ;Γ} ⊨ fill K (FG_increment (Loc x) Unit) ≤log≤ t : τ.
   Proof.
     iIntros "Hx Hlog".
     iApply bin_log_related_wp_l.
@@ -123,8 +124,8 @@ Section CG_Counter.
     (Hspec : nclose specN ⊆ E1) :
     x ↦ₛ (#nv n)
     -∗ (x ↦ₛ (#nv n)
-         -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (#n n)%E : τ)%I
-    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (lamsubst counter_read (LocV x) #())%E : τ.
+         -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#n n)%E : τ)%I
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (lamsubst counter_read (LocV x) #())%E : τ.
   Proof.
     iIntros "Hx Hlog".
     unfold counter_read. unlock. simpl.
@@ -140,8 +141,8 @@ Section CG_Counter.
     □ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗
        ((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
         (∀ m, x ↦ᵢ (#nv (S m)) ∗ R(m) -∗ 
-            {E2,E1;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ))
-    -∗ ({E1,E1;Γ} ⊨ fill K ((FG_increment $/ LocV x) Unit)%E ≤log≤ t : τ).
+            {E2,E1;Δ;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ))
+    -∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment $/ LocV x) Unit)%E ≤log≤ t : τ).
   Proof.
     iIntros "#H".
     unfold FG_increment. unlock. simpl.
@@ -167,12 +168,12 @@ Section CG_Counter.
       iIntros "_ !> Hx". simpl.
       iDestruct "HQ" as "[_ HQ]".
       iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
-      iApply (bin_log_related_if_true_masked_l _ _ _ K); auto.   
+      iApply bin_log_related_if_true_masked_l; auto.
     - iExists (#nv n'). iFrame. 
       iSplitL; eauto; last first.
       { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
       iIntros "_ !> Hx". simpl.
-      iApply (bin_log_related_if_false_masked_l _ _ _ K); auto.
+      iApply bin_log_related_if_false_masked_l; auto.
       iDestruct "HQ" as "[HQ _]".
       iMod ("HQ" with "[Hx HR]").
       { iExists _; iFrame. }
@@ -184,13 +185,13 @@ Section CG_Counter.
     □ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗
        ((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
         (∀ m, x ↦ᵢ (#nv m) ∗ R(m) -∗
-            {E2,E1;Γ} ⊨ fill K (#n m) ≤log≤ t : τ))
-    -∗ {E1,E1;Γ} ⊨ fill K ((counter_read $/ LocV x) #())%E ≤log≤ t : τ.
+            {E2,E1;Δ;Γ} ⊨ fill K (#n m) ≤log≤ t : τ))
+    -∗ {E1,E1;Δ;Γ} ⊨ fill K ((counter_read $/ LocV x) #())%E ≤log≤ t : τ.
   Proof.
     iIntros "#H".
     unfold counter_read. unlock. simpl.
     rel_rec_l.
-    iApply (bin_log_related_load_l).
+    iApply bin_log_related_load_l.
     iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
     iExists _; iFrame "Hx". iNext.
     iIntros "Hx".
@@ -201,7 +202,7 @@ Section CG_Counter.
   (* TODO: try to use with_lock rules *)
   Lemma FG_CG_increment_refinement l cnt cnt' Γ :
     inv counterN (counter_inv l cnt cnt') -∗
-    Γ ⊨ FG_increment $/ LocV cnt ≤log≤ CG_increment $/ LocV cnt' $/ LocV l : TArrow TUnit TUnit.
+    {⊤,⊤;Δ;Γ} ⊨ FG_increment $/ LocV cnt ≤log≤ CG_increment $/ LocV cnt' $/ LocV l : TArrow TUnit TUnit.
   Proof.
     iIntros "#Hinv".
     iApply bin_log_related_arrow.
@@ -210,7 +211,7 @@ Section CG_Counter.
     { unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
     { unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
 
-    iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
+    iAlways. iIntros ([v v']) "[% %]"; simpl in *; subst.
     iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
     iAlways.
     iInv counterN as ">Hcnt" "Hcl". iModIntro.
@@ -232,7 +233,7 @@ Section CG_Counter.
 
   Lemma counter_read_refinement l cnt cnt' Γ :
     inv counterN (counter_inv l cnt cnt') -∗
-    Γ ⊨ counter_read $/ #cnt ≤log≤ counter_read $/ #cnt' : TArrow TUnit TNat.
+    {⊤,⊤;Δ;Γ} ⊨ counter_read $/ #cnt ≤log≤ counter_read $/ #cnt' : TArrow TUnit TNat.
   Proof.
     iIntros "#Hinv".
     iApply bin_log_related_arrow.
@@ -240,7 +241,7 @@ Section CG_Counter.
     { unfold counter_read. unlock. simpl. reflexivity. }
     { unfold counter_read. unlock. simpl. solve_closed. }
     { unfold counter_read. unlock. simpl. solve_closed. }
-    iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
+    iAlways. iIntros ([v v']) "[% %]"; simpl in *; subst.
     iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
     iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". 
     iModIntro. 
@@ -254,16 +255,16 @@ Section CG_Counter.
       iIntros "Hcnt'".
       iMod ("Hclose" with "[Hl Hcnt Hcnt']"); simpl.
       { iNext. iExists _. by iFrame. }
-      iApply bin_log_related_val; intros; simpl; eauto.
+      rel_vals. simpl. eauto.
   Qed.
 
   Lemma FG_CG_counter_refinement :
-    ∅ ⊨ FG_counter ≤log≤ CG_counter :
+    {⊤,⊤;Δ;∅} ⊨ FG_counter ≤log≤ CG_counter :
           TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
   Proof.
     unfold FG_counter, CG_counter.
     iApply bin_log_related_arrow; try by (unlock; eauto).
-    iAlways. iIntros (? [? ?]) "/= [% %]"; simplify_eq/=.
+    iAlways. iIntros ([? ?]) "/= [% %]"; simplify_eq/=.
     unlock. rel_rec_l. rel_rec_r.
     rel_bind_r (newlock #())%E.
     iApply (bin_log_related_newlock_r); auto; simpl.
@@ -294,7 +295,6 @@ Section CG_Counter.
       rel_rec_r.
       iApply (counter_read_refinement with "Hinv").
   Qed.
-
 End CG_Counter.
 
 Theorem counter_ctx_refinement :

F_mu_ref_conc/examples/lateearlychoice.v

@@ -42,10 +42,10 @@ Section Refinement.
         iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
   Qed.
 
-  Lemma rand_l Γ E1 K ρ t τ :
+  Lemma rand_l Δ Γ E1 K ρ t τ :
     ↑choiceN ⊆ E1 →
-    spec_ctx ρ -∗ (∀ b, {E1,E1;Γ} ⊨ fill K (#♭ b) ≤log≤ t : τ)
-    -∗ {E1,E1;Γ} ⊨ fill K (rand #())%E ≤log≤ t : τ.
+    spec_ctx ρ -∗ (∀ b, {E1,E1;Δ;Γ} ⊨ fill K (#♭ b) ≤log≤ t : τ)
+    -∗ {E1,E1;Δ;Γ} ⊨ fill K (rand #())%E ≤log≤ t : τ.
   Proof.
     iIntros (?) "#Hs Hlog".
     unfold rand. unlock. simpl.
@@ -74,12 +74,12 @@ Section Refinement.
       done. 
   Qed.
 
-  Lemma rand_r b Γ E1 E2 K ρ t τ :
+  Lemma rand_r b Δ Γ E1 E2 K ρ t τ :
     ↑specN ⊆ E1 →
     ↑choiceN ⊆ E1 →
     spec_ctx ρ -∗
-    {E1,E2;Γ} ⊨ t ≤log≤ fill K (#♭ b) : τ -∗
-    {E1,E2;Γ} ⊨ t ≤log≤ fill K (rand #())%E : τ.
+    {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#♭ b) : τ -∗
+    {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (rand #())%E : τ.
   Proof.
     iIntros (??) "#Hs Hlog".
     unfold rand. unlock.
@@ -94,11 +94,11 @@ Section Refinement.
     - by rel_load_r.
   Qed.
 
-  Lemma lateChoice_l Γ x v ρ t :
+  Lemma lateChoice_l Δ Γ x v ρ t :
     spec_ctx ρ -∗ x ↦ᵢ v -∗
-    (x ↦ᵢ (#nv 0) -∗ ∀ b, Γ ⊨ #♭ b ≤log≤ t : TBool) -∗
-    Γ ⊨ lateChoice #x ≤log≤ t : TBool.
-  Proof.  
+    (x ↦ᵢ (#nv 0) -∗ ∀ b, {⊤,⊤;Δ;Γ} ⊨ #♭ b ≤log≤ t : TBool) -∗
+    {⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ t : TBool.
+  Proof.
     iIntros "#Hs Hx Hlog".
     unfold lateChoice. unlock.
     rel_rec_l.
@@ -109,9 +109,9 @@ Section Refinement.
     by iApply "Hlog".
   Qed.
    
-  Lemma prerefinement Γ x x' n ρ :
+  Lemma prerefinement Δ Γ x x' n ρ :
     (spec_ctx ρ -∗ x ↦ᵢ (#nv n) -∗ x' ↦ₛ (#nv n) -∗
-      Γ ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool)%I.
+      {⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool)%I.
   Proof.
     iIntros "#Hspec Hx Hx'".
     iApply (lateChoice_l with "Hspec Hx"). iIntros "Hx".
@@ -124,12 +124,12 @@ Section Refinement.
     rel_rec_r.
     rel_store_r. simpl.
     rel_rec_r.
-    rel_vals; eauto.
+    rel_vals; simpl; eauto.
   Qed.
 
-  Lemma prerefinement2 Γ x x' n ρ :
+  Lemma prerefinement2 Δ Γ x x' n ρ :
     (spec_ctx ρ -∗ x ↦ᵢ (#nv n) -∗ x' ↦ₛ (#nv n) -∗
-      Γ ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool)%I.
+      {⊤,⊤;Δ;Γ} ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool)%I.
   Proof.
     iIntros "#Hspec Hx Hx'".
     unfold earlyChoice. unlock.
@@ -147,7 +147,7 @@ Section Refinement.
 
     rel_store_l. simpl.
     rel_rec_l.
-    rel_vals; eauto.
+    rel_vals; simpl; eauto.
   Qed.
     
 End Refinement.

F_mu_ref_conc/examples/lock.v

@@ -43,6 +43,7 @@ Hint Resolve with_lock_type : typeable.
 Section proof.
   Context `{logrelG Σ}.
   Variable (E1 E2 : coPset).
+  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
 
   Lemma steps_newlock ρ j K
     (Hcl : nclose specN ⊆ E1) :
@@ -58,8 +59,8 @@ Section proof.
 
   Lemma bin_log_related_newlock_r Γ K t τ 
     (Hcl : nclose specN ⊆ E1) :
-    (∀ l : loc, l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Loc l) : τ)%I
-    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (newlock #())%E: τ.
+    (∀ l : loc, l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Loc l) : τ)%I
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock #())%E: τ.
   Proof.
     iIntros "Hlog".
     unfold newlock. unlock.
@@ -87,8 +88,8 @@ Section proof.
   Lemma bin_log_related_acquire_r Γ K l t τ
     (Hcl : nclose specN ⊆ E1) :
     l ↦ₛ (#♭v false) -∗
-    (l ↦ₛ (#♭v true) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I
-    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
+    (l ↦ₛ (#♭v true) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
     unfold acquire. unlock.
@@ -115,8 +116,8 @@ Section proof.
   Lemma bin_log_related_release_r Γ K l t τ b
     (Hcl : nclose specN ⊆ E1) :
     l ↦ₛ (#♭v b) -∗
-    (l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I
-    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App release (Loc l)) : τ.
+    (l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App release (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
     unfold release. unlock.
@@ -160,11 +161,11 @@ Section proof.
     (to_val ev = Some v) →
     (to_val ew = Some w) →
     (nclose specN ⊆ E1) →
-    (∀ K, (Q -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗
-        {E1,E2;Γ} ⊨ t ≤log≤ fill K (App e ew) : τ) -∗
+    (∀ K, (Q -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗
+        {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App e ew) : τ) -∗
     l ↦ₛ (#♭v false) -∗
-    (Q -∗ l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K ev : τ)%I
-    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (with_lock e (Loc l) ew) : τ.
+    (Q -∗ l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ev : τ)%I
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (with_lock e (Loc l) ew) : τ.
   Proof.
     iIntros (????) "HA Hl Hlog".
     rel_bind_r (with_lock e).

F_mu_ref_conc/examples/par.v

@@ -28,12 +28,12 @@ Hint Resolve par_type : typeable.
 Section compatibility.
   Context `{logrelG Σ}.
 
-  Lemma bin_log_related_par Γ E e1 e2 e1' e2' τ1 τ2 :
+  Lemma bin_log_related_par Δ Γ E e1 e2 e1' e2' τ1 τ2 :
     ↑specN ⊆ E →
     ↑logN ⊆ E →
-    {E,E;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit τ1 -∗
-    {E,E;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit τ2 -∗
-    {E,E;Γ} ⊨ par e1 e2 ≤log≤ par e1' e2' : TProd τ1 τ2.
+    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit τ1 -∗
+    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit τ2 -∗
+    {E,E;Δ;Γ} ⊨ par e1 e2 ≤log≤ par e1' e2' : TProd τ1 τ2.
   Proof.
     iIntros (??) "He1 He2".
     iApply (bin_log_related_app with "[He1] He2").

F_mu_ref_conc/hax.v

@@ -17,19 +17,19 @@ Section hax.
   Notation D := (prodC valC valC -n> iProp Σ).
   Implicit Types Δ : listC D.
 
-  Lemma bin_log_related_arrow Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
+  Lemma bin_log_related_arrow Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
     e = (rec: f x := eb)%E →
     e' = (rec: f' x' := eb')%E →
     Closed ∅ e →
     Closed ∅ e' →
-    □(∀ Δ vv, ⟦ τ ⟧ Δ vv -∗
-      Γ ⊨ App e (of_val (vv.1)) ≤log≤ App e' (of_val (vv.2)) : τ') -∗
-    {E,E;Γ} ⊨ e ≤log≤ e' : TArrow τ τ'.
+    □(∀ vv, ⟦ τ ⟧ Δ vv -∗
+      {⊤,⊤;Δ;Γ} ⊨ App e (of_val (vv.1)) ≤log≤ App e' (of_val (vv.2)) : τ') -∗
+    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TArrow τ τ'.
   Proof.
     iIntros (????) "#H".
     subst e e'.
     rewrite bin_log_related_eq.
-    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
+    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
     cbn-[subst_p].
     iModIntro.
     rewrite {2}/env_subst Closed_subst_p_id.
@@ -38,8 +38,7 @@ Section hax.
     rewrite /env_subst Closed_subst_p_id.
     iExists (RecV f' x' eb').
     iFrame "Hj". iAlways. iIntros (vv) "Hvv".
-    iSpecialize ("H" $! Δ vv with "Hvv").
-    iSpecialize ("H" $! Δ with "Hs []").
+    iSpecialize ("H" $! vv with "Hvv Hs []").
     { iAlways. iApply "HΓ". }    
     Unshelve. all: trivial.
     assert (Closed ∅ ((rec: f x := eb) (vv.1))%E).

F_mu_ref_conc/logrel_binary.v

@@ -341,8 +341,8 @@ Section logrel.
 
   (* TODO: derive this from [interp_EqType_agree] *)
   (* This formulation is more suitable for proving soundness of the logical relation in [soundness_binary.v] *)
-  Lemma interp_ObsType_agree τ : ∀ (v v' : val),
-    ⟦ τ ⟧ [] (v, v') ⊢ ⌜ObsType τ → v = v'⌝.
+  Lemma interp_ObsType_agree Δ τ : ∀ (v v' : val),
+    ⟦ τ ⟧ Δ (v, v') ⊢ ⌜ObsType τ → v = v'⌝.
   Proof.
     induction τ; iIntros (v v') "HI"; simpl; eauto;
       try by (iPureIntro; inversion 1).
@@ -375,7 +375,7 @@ Section bin_log_def.
   Context `{logrelG Σ}.
   Notation D := (prodC valC valC -n> iProp Σ).
 
-  Definition bin_log_related_def (E1 E2 : coPset) (Γ : stringmap type) (e e' : expr) (τ : type) : iProp Σ := (∀ Δ (vvs : stringmap (val * val)) ρ,  
+  Definition bin_log_related_def (E1 E2 : coPset) (Δ : list D) (Γ : stringmap type) (e e' : expr) (τ : type) : iProp Σ := (∀ (vvs : stringmap (val * val)) ρ,  
     spec_ctx ρ -∗
     □ interp_env Γ ⊤ ⊤ Δ vvs 
     -∗ interp_expr E1 E2 (interp ⊤ ⊤ τ) Δ
@@ -386,7 +386,11 @@ Section bin_log_def.
     seal_eq bin_log_related_aux.
 End bin_log_def.
 
+Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
+  (bin_log_related E1 E2 Δ Γ e e' τ) (at level 74, E1,E2, e, e', τ at next level).
 Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
-  (bin_log_related E1 E2 Γ e e' τ) (at level 74, E1,E2, e, e', τ at next level).
+  (bin_log_related E1 E2 [] Γ e e' τ) (at level 74, E1,E2, e, e', τ at next level).
+(* Notation "Δ ',' Γ ⊨ e '≤log≤' e' : τ" := *)
+(*   (bin_log_related ⊤ ⊤ [] Γ e e' τ) (at level 74, e, e', τ at next level). *)
 Notation "Γ ⊨ e '≤log≤' e' : τ" :=
-  (bin_log_related ⊤ ⊤ Γ e e' τ) (at level 74, e, e', τ at next level).
+  (bin_log_related ⊤ ⊤ [] Γ e e' τ) (at level 74, e, e', τ at next level).

F_mu_ref_conc/soundness_binary.v

@@ -13,8 +13,8 @@ Instance subG_heapPreG {Σ} : subG logrelΣ Σ → logrelPreG Σ.
 Proof. solve_inG. Qed.
 
 Lemma logrel_adequate Σ `{logrelPreG Σ}
-    e e' τ σ :
-  (∀ `{logrelG Σ}, ∅ ⊨ e ≤log≤ e' : τ) →
+  Δ e e' τ σ :
+  (∀ `{logrelG Σ}, {⊤,⊤;Δ;∅} ⊨ e ≤log≤ e' : τ) →
   adequate e σ (λ v, ∃ thp' h v', rtc step ([e'], ∅) (of_val v' :: thp', h) 
     ∧ (ObsType τ → v = v')).
 Proof.
@@ -31,7 +31,7 @@ Proof.
   iSplitL.
   - iPoseProof (Hlog _) as "Hrel".
     rewrite bin_log_related_eq /bin_log_related_def.
-    iSpecialize ("Hrel" $! [] with "[$Hcfg] []").
+    iSpecialize ("Hrel" with "[$Hcfg] []").
     { iApply logrel_binary.interp_env_nil. }
     rewrite /env_subst !fmap_empty !subst_p_empty. 
     iApply fupd_wp.
@@ -52,8 +52,8 @@ Proof.
 Qed.
 
 
-Theorem logrel_typesafety Σ `{logrelPreG Σ} e τ e' thp σ σ' :
-  (∀ `{logrelG Σ}, ∅ ⊨ e ≤log≤ e : τ) →
+Theorem logrel_typesafety Σ `{logrelPreG Σ} Δ e e' τ thp σ σ' :
+  (∀ `{logrelG Σ}, {⊤,⊤;Δ;∅} ⊨ e ≤log≤ e : τ) →
   rtc step ([e], σ) (thp, σ') → e' ∈ thp →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
@@ -63,8 +63,8 @@ Proof.
 Qed.
 
 Lemma logrel_simul Σ `{logrelPreG Σ}
-    e e' τ v thp hp :
-  (∀ `{logrelG Σ}, ∅ ⊨ e ≤log≤ e' : τ) →
+  Δ  e e' τ v thp hp :
+  (∀ `{logrelG Σ}, {⊤,⊤;Δ;∅} ⊨ e ≤log≤ e' : τ) →
   rtc step ([e], ∅) (of_val v :: thp, hp) →
   (∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp') ∧ (ObsType τ → v = v')).
 Proof.
@@ -77,14 +77,16 @@ Qed.
 Lemma logrel_ctxequiv Σ `{logrelPreG Σ} Γ e e' τ :
   Closed (dom _ Γ) e →
   Closed (dom _ Γ) e' →
-  (∀ `{logrelG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
+  (∀ `{logrelG Σ} Δ, {⊤,⊤;Δ;Γ} ⊨ e ≤log≤ e' : τ) →
   Γ ⊨ e ≤ctx≤ e' : τ.
 Proof.
   intros He He' Hlog K thp σ ? τ' ? ? Hstep.
   cut (∃ thp' hp' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', hp') ∧ (ObsType τ'  → v = v')).
   { naive_solver. }
-  eapply (logrel_simul Σ _); last by apply Hstep.
+  eapply (logrel_simul Σ []); last by apply Hstep.
   intros ?.
-  iApply (bin_log_related_under_typed_ctx _ _ _ _ ∅); eauto.
-  iPoseProof (Hlog _) as "Hrel". auto.
+  iStartProof.
+  iAssert (□ ∀ Δ, {⊤, ⊤; Δ; Γ}⊨ e ≤log≤ e' : τ)%I as "Hlog".
+  { iAlways. iIntros (Δ). iApply Hlog. }
+  iApply (bin_log_related_under_typed_ctx with "[Hlog]"); eauto.
 Qed.