Update F_mu_ref_conc to Iris 3

sans examples

F_mu_ref_conc/fundamental_unary.v

@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 
 Definition log_typed `{heapIG Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs,
   env_PersistentP Δ →
-  heapI_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs].
+  ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs].
 Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
 
 Section typed_interp.
@@ -15,13 +15,13 @@ Section typed_interp.
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
     iApply (wp_bind [ctx]);
     iApply wp_wand_l;
-    iSplitL; [| iApply Hp; trivial]; [iIntros (v) Hv|iSplit; trivial]; cbn.
+    iSplitR; [|iApply Hp; trivial]; iIntros (v) Hv; cbn.
 
   Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
 
   Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ.
   Proof.
-    induction 1; iIntros (Δ vs HΔ) "#[Hheap HΓ] /=".
+    induction 1; iIntros (Δ vs HΔ) "#HΓ /=".
     - (* var *)
       iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
       rewrite /env_subst. simplify_option_eq. by value_case.
@@ -32,7 +32,7 @@ Section typed_interp.
       smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHtyped1.
       smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHtyped2.
       iDestruct "Hv" as (n) "%"; iDestruct "Hv'" as (n') "%"; simplify_eq/=.
-      iApply wp_nat_binop. iNext. iIntros "!> {Hheap HΓ}".
+      iApply wp_nat_binop. iNext. iIntros "!>".
       destruct op; simpl; try destruct eq_nat_dec;
         try destruct le_dec; try destruct lt_dec; eauto 10.
     - (* pair *)
@@ -59,22 +59,22 @@ Section typed_interp.
       iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
       + iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext.
         erewrite typed_subst_head_simpl by naive_solver.
-        iApply (IHtyped2 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto.
+        iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
       + iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext.
         erewrite typed_subst_head_simpl by naive_solver.
-        iApply (IHtyped3 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto.
+        iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
     - (* If *)
       smart_wp_bind (IfCtx _ _) v "#Hv" IHtyped1; cbn.
       iDestruct "Hv" as ([]) "%"; subst; simpl;
         [iApply wp_if_true| iApply wp_if_false]; iNext;
       [iApply IHtyped2| iApply IHtyped3]; auto.
     - (* Rec *)
-      value_case; iAlways. simpl. iLöb as "IH"; iIntros (w) "#Hw".
+      value_case. simpl. iAlways. iLöb as "IH". iIntros (w) "#Hw".
       iDestruct (interp_env_length with "HΓ") as %?.
       iApply wp_rec; auto 1 using to_of_val. iNext.
       asimpl. change (Rec _) with (of_val (RecV e.[upn 2 (env_subst vs)])) at 2.
       erewrite typed_subst_head_simpl_2 by naive_solver.
-      iApply (IHtyped Δ (_ :: w :: vs)). iSplit; [done|].
+      iApply (IHtyped Δ (_ :: w :: vs)). 
       iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto.
     - (* app *)
       smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
@@ -83,7 +83,7 @@ Section typed_interp.
     - (* TLam *)
       value_case.
       iAlways; iIntros (τi) "%". iApply wp_tlam; iNext.
-      iApply IHtyped. iFrame "Hheap". by iApply interp_env_ren.
+      iApply IHtyped. by iApply interp_env_ren.
     - (* TApp *)
       smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
       iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (⟦ τ' ⟧ Δ)); iPureIntro; apply _|]; cbn.
@@ -107,37 +107,40 @@ Section typed_interp.
       iApply wp_wand_l. iSplitL; [|iApply IHtyped; auto]; auto.
     - (* Alloc *)
       smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iApply wp_fupd.
-      iApply (wp_alloc with "Hheap []"); auto 1 using to_of_val.
+      iApply wp_alloc; auto 1 using to_of_val.
       iNext; iIntros (l) "Hl".
       iMod (inv_alloc _ with "[Hl]") as "HN";
         [| iModIntro; iExists _; iSplit; trivial]; eauto.
     - (* Load *)
       smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
       iDestruct "Hv" as (l) "[% #Hv]"; subst.
-      iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
-      iApply ((wp_load _ _ 1) with "[Hw1] [Hclose]"); [|iFrame "Hheap"|];
-      trivial. solve_ndisj. iNext.
-      iIntros "Hw1". iMod ("Hclose" with "[-]"); eauto.
+      iApply wp_atomic; eauto.
+      iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".      
+      iApply (wp_load with "Hw1"). 
+      iNext.
+      iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.      
     - (* Store *)
       smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
       smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
       iDestruct "Hv" as (l) "[% #Hv]"; subst.
+      iApply wp_atomic; eauto.
       iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
-      iApply (wp_store with "[Hz1] [Hclose]"); [| |iFrame "Hheap Hz1"|].
-      by rewrite to_of_val. solve_ndisj. iNext.
-      iIntros "Hz1". iMod ("Hclose" with "[-]"); eauto.
+      iApply (wp_store with "Hz1"); auto using to_of_val. 
+      iNext.
+      iIntros "Hz1". iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
     - (* CAS *)
       smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHtyped1; cbn.
       smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHtyped2; cbn.
       smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHtyped3; cbn. iClear "HΓ".
-      iDestruct "Hv1" as (l) "[% Hinv]"; subst.
+      iDestruct "Hv1" as (l) "[% Hv1]"; subst.
+      iApply wp_atomic; eauto.
       iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
       destruct (decide (v2 = w)) as [|Hneq]; subst.
-      + iApply (wp_cas_suc with "[Hw1] [Hclose]"); [| | |iFrame "Hheap Hw1"|];
-          eauto using to_of_val. solve_ndisj. iNext.
-        iIntros "Hw1". iMod ("Hclose" with "[-]"); eauto.
-      + iApply (wp_cas_fail with "[Hw1] [Hclose]"); [| | | |iFrame "Hheap Hw1"|];
-          eauto using to_of_val. solve_ndisj. iNext.
-        iIntros "Hw1". iMod ("Hclose" with "[-]"); eauto.
+      + iApply (wp_cas_suc with "Hw1"); auto using to_of_val.
+        iNext.
+        iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
+      + iApply (wp_cas_fail with "Hw1"); auto using to_of_val.
+        iNext.
+        iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
   Qed.
 End typed_interp.

F_mu_ref_conc/lang.v

 From iris.program_logic Require Export ectx_language ectxi_language.
 From iris_logrel.prelude Require Export base.
-From iris.algebra Require Export cofe.
+From iris.algebra Require Export ofe.
 From iris.prelude Require Import gmap.
 
 Module lang.
@@ -299,10 +299,14 @@ Definition is_atomic (e : expr) : Prop :=
   | CAS e0 e1 e2 => is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
   | _ => False
   end.
+
+Local Hint Resolve language.val_irreducible.
+Local Hint Resolve to_of_val.
+Local Hint Unfold language.irreducible.
 Lemma is_atomic_correct e : is_atomic e → language.atomic e.
 Proof.
   intros ?; apply ectx_language_atomic.
-  - destruct 1; simpl; by eauto using to_of_val.
+  - destruct 1; simpl; eauto.
   - intros [|Ki K] e' -> Hval%eq_None_not_Some; [done|].
     destruct Hval; apply (fill_val K e'). destruct Ki; naive_solver.
 Qed.

F_mu_ref_conc/logrel_binary.v

@@ -7,7 +7,7 @@ From iris.prelude Require Import tactics.
 Import uPred.
 
 (* HACK: move somewhere else *)
-Ltac auto_equiv ::=
+Ltac auto_equiv :=
   (* Deal with "pointwise_relation" *)
   repeat lazymatch goal with
   | |- pointwise_relation _ _ _ _ => intros ?
@@ -20,6 +20,8 @@ Ltac auto_equiv ::=
   (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
   try (f_equiv; fast_done || auto_equiv).
 
+Ltac solve_proper ::= (preprocess_solve_proper; auto_equiv).
+
 Definition logN : namespace := nroot .@ "logN".
 
 (** interp : is a unary logical relation. *)
@@ -43,26 +45,27 @@ Section logrel.
   Solve Obligations with solve_proper_alt.
 
   Program Definition interp_unit : listC D -n> D := λne Δ ww,
-    (ww.1 = UnitV ∧ ww.2 = UnitV)%I.
+    (⌜ww.1 = UnitV⌝ ∧ ⌜ww.2 = UnitV⌝)%I.
   Solve Obligations with solve_proper_alt.
   Program Definition interp_nat : listC D -n> D := λne Δ ww,
-    (∃ n : nat, ww.1 = #nv n ∧ ww.2 = #nv n)%I.
-  Solve Obligations with solve_proper.
+    (∃ n : nat, ⌜ww.1 = #nv n⌝ ∧ ⌜ww.2 = #nv n⌝)%I.
+  Solve Obligations with solve_proper. 
+
   Program Definition interp_bool : listC D -n> D := λne Δ ww,
-    (∃ b : bool, ww.1 = #♭v b ∧ ww.2 = #♭v b)%I.
-  Solve Obligations with solve_proper.
+    (∃ b : bool, ⌜ww.1 = #♭v b⌝ ∧ ⌜ww.2 = #♭v b⌝)%I.
+  Solve Obligations with solve_proper. 
 
   Program Definition interp_prod
       (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
-    (∃ vv1 vv2, ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2)) ∧
+    (∃ vv1 vv2, ⌜ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2))⌝ ∧
                 interp1 Δ vv1 ∧ interp2 Δ vv2)%I.
-  Solve Obligations with solve_proper.
+  Solve Obligations with solve_proper. 
 
   Program Definition interp_sum
       (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
-    ((∃ vv, ww = (InjLV (vv.1), InjLV (vv.2)) ∧ interp1 Δ vv) ∨
-     (∃ vv, ww = (InjRV (vv.1), InjRV (vv.2)) ∧ interp2 Δ vv))%I.
-  Solve Obligations with solve_proper.
+    ((∃ vv, ⌜ww = (InjLV (vv.1), InjLV (vv.2))⌝ ∧ interp1 Δ vv) ∨
+     (∃ vv, ⌜ww = (InjRV (vv.1), InjRV (vv.2))⌝ ∧ interp2 Δ vv))%I.
+  Solve Obligations with solve_proper. 
 
   Program Definition interp_arrow
           (interp1 interp2 : listC D -n> D) : listC D -n> D :=
@@ -71,28 +74,24 @@ Section logrel.
              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.
+  Solve Obligations with solve_proper. 
 
   Program Definition interp_forall
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
     (□ ∀ τi,
-          (■ ∀ ww, PersistentP (τi ww)) →
+          ⌜∀ ww, PersistentP (τi ww)⌝ →
           interp_expr
             interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
   Solve Obligations with solve_proper.
 
   Program Definition interp_rec1
       (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
-    (□ ∃ vv, ww = (FoldV (vv.1), FoldV (vv.2)) ∧ ▷ interp (τi :: Δ) vv)%I.
+    (□ ∃ vv, ⌜ww = (FoldV (vv.1), FoldV (vv.2))⌝ ∧ ▷ interp (τi :: Δ) vv)%I.
   Solve Obligations with solve_proper.
 
   Global Instance interp_rec1_contractive
     (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
-  Proof.
-    intros n τi1 τi2 Hτi ww; cbn.
-    apply always_ne, exist_ne; intros vv; apply and_ne; trivial.
-    apply later_contractive =>i Hi. by rewrite Hτi.
-  Qed.
+  Proof. solve_contractive. Qed.
 
   Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
     fixpoint (interp_rec1 interp Δ).
@@ -106,7 +105,7 @@ Section logrel.
 
   Program Definition interp_ref
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
-    (∃ ll, ww = (LocV (ll.1), LocV (ll.2)) ∧
+    (∃ ll, ⌜ww = (LocV (ll.1), LocV (ll.2))⌝ ∧
            inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
   Solve Obligations with solve_proper.
 
@@ -127,7 +126,7 @@ Section logrel.
 
   Definition interp_env (Γ : list type)
       (Δ : listC D) (vvs : list (val * val)) : iProp Σ :=
-    (length Γ = length vvs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
+    (⌜length Γ = length vvs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
   Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
   Class env_PersistentP Δ :=
@@ -155,9 +154,6 @@ Section logrel.
     ≡ ⟦ τ ⟧ (Δ1 ++ Δ2).
   Proof.
     revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
-    - intros ww; simpl; properness; auto.
-    - intros ww; simpl; properness; auto.
-    - intros ww; simpl; properness; auto.
     - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
     - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
     - unfold interp_expr.
@@ -166,7 +162,7 @@ Section logrel.
       properness; auto. apply (IHτ (_ :: _)).
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
-      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
+      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
     - unfold interp_expr.
       intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
     - intros ww; simpl; properness; auto. by apply IHτ.
@@ -177,9 +173,6 @@ Section logrel.
     ≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2).
   Proof.
     revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto.
-    - intros ww; simpl; properness; auto.
-    - intros ww; simpl; properness; auto.
-    - intros ww; simpl; properness; auto.
     - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
     - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
     - unfold interp_expr.
@@ -191,7 +184,7 @@ Section logrel.
       rewrite !lookup_app_r; [|lia ..].
       destruct (x - length Δ1) as [|n] eqn:?; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
+      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
     - unfold interp_expr.
       intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
     - intros ww; simpl; properness; auto. by apply IHτ.
@@ -200,11 +193,11 @@ Section logrel.
   Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2.
   Proof. apply (interp_subst_up []). Qed.
 
-  Lemma interp_env_length Δ Γ vvs : ⟦ Γ ⟧* Δ vvs ⊢ length Γ = length vvs.
+  Lemma interp_env_length Δ Γ vvs : ⟦ Γ ⟧* Δ vvs ⊢ ⌜length Γ = length vvs⌝.
   Proof. by iIntros "[% ?]". Qed.
 
   Lemma interp_env_Some_l Δ Γ vvs x τ :
-    Γ !! x = Some τ → ⟦ Γ ⟧* Δ vvs ⊢ ∃ vv, vvs !! x = Some vv ∧ ⟦ τ ⟧ Δ vv.
+    Γ !! x = Some τ → ⟦ Γ ⟧* Δ vvs ⊢ ∃ vv, ⌜vvs !! x = Some vv⌝ ∧ ⟦ τ ⟧ Δ vv.
   Proof.
     iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
     destruct (lookup_lt_is_Some_2 vvs x) as [v Hv].
@@ -219,7 +212,7 @@ Section logrel.
   Lemma interp_env_cons Δ Γ vvs τ vv :
     ⟦ τ :: Γ ⟧* Δ (vv :: vvs) ⊣⊢ ⟦ τ ⟧ Δ vv ∗ ⟦ Γ ⟧* Δ vvs.
   Proof.
-    rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
+    rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ ⌜(_ = _)⌝%I) -assoc.
     by apply sep_proper; [apply pure_proper; omega|].
   Qed.
 
@@ -232,7 +225,7 @@ Section logrel.
   Qed.
 
   Lemma interp_EqType_agree τ v v' Δ :
-    env_PersistentP Δ → EqType τ → interp τ Δ (v, v') ⊢ ■ (v = v').
+    env_PersistentP Δ → EqType τ → interp τ Δ (v, v') ⊢ ⌜v = v'⌝.
   Proof.
     intros ? Hτ; revert v v'; induction Hτ; iIntros (v v') "#H1 /=".
     - by iDestruct "H1" as "[% %]"; subst.

F_mu_ref_conc/logrel_unary.v

@@ -19,18 +19,18 @@ Section logrel.
     from_option id (cconst True)%I (Δ !! x).
   Solve Obligations with solve_proper_alt.
 
-  Definition interp_unit : listC D -n> D := λne Δ w, (w = UnitV)%I.
-  Definition interp_nat : listC D -n> D := λne Δ w, (∃ n, w = #nv n)%I.
-  Definition interp_bool : listC D -n> D := λne Δ w, (∃ n, w = #♭v n)%I.
+  Definition interp_unit : listC D -n> D := λne Δ w, ⌜w = UnitV⌝%I.
+  Definition interp_nat : listC D -n> D := λne Δ w, ⌜∃ n, w = #nv n⌝%I.
+  Definition interp_bool : listC D -n> D := λne Δ w, ⌜∃ n, w = #♭v n⌝%I.
 
   Program Definition interp_prod
       (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
-    (∃ w1 w2, w = PairV w1 w2 ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
+    (∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
   Solve Obligations with solve_proper.
 
   Program Definition interp_sum
       (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
-    ((∃ w1, w = InjLV w1 ∧ interp1 Δ w1) ∨ (∃ w2, w = InjRV w2 ∧ interp2 Δ w2))%I.
+    ((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I.
   Solve Obligations with solve_proper.
 
   Program Definition interp_arrow
@@ -41,24 +41,20 @@ Section logrel.
   Program Definition interp_forall
       (interp : listC D -n> D) : listC D -n> D := λne Δ w,
     (□ ∀ τi : D,
-      ■ (∀ v, PersistentP (τi v)) → WP TApp (of_val w) {{ interp (τi :: Δ) }})%I.
+      ⌜∀ v, PersistentP (τi v)⌝ → WP TApp (of_val w) {{ interp (τi :: Δ) }})%I.
   Solve Obligations with solve_proper.
 
   Definition interp_rec1
       (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
-    (□ (∃ v, w = FoldV v ∧ ▷ interp (τi :: Δ) v))%I.
+    (□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I.
 
   Global Instance interp_rec1_contractive
     (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
-  Proof.
-    intros n τi1 τi2 Hτi w; cbn.
-    apply always_ne, exist_ne; intros v; apply and_ne; trivial.
-    apply later_contractive =>i Hi. by rewrite Hτi.
-  Qed.
+  Proof. by solve_contractive. Qed.
 
   Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
     fixpoint (interp_rec1 interp Δ).
-  Next Obligation.
+  Next Obligation. 
     intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
   Qed.
 
@@ -68,7 +64,7 @@ Section logrel.
 
   Program Definition interp_ref
       (interp : listC D -n> D) : listC D -n> D := λne Δ w,
-    (∃ l, w = LocV l ∧ inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
+    (∃ l, ⌜w = LocV l⌝ ∧ inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
   Solve Obligations with solve_proper.
 
   Fixpoint interp (τ : type) : listC D -n> D :=
@@ -88,7 +84,7 @@ Section logrel.
 
   Definition interp_env (Γ : list type)
       (Δ : listC D) (vs : list val) : iProp Σ :=
-    (length Γ = length vs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
+    (⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
   Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
   Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
@@ -126,7 +122,7 @@ Section logrel.
       properness; auto. apply (IHτ (_ :: _)).
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
-      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
+      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
     - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
     - intros w; simpl; properness; auto. by apply IHτ.
   Qed.
@@ -146,7 +142,7 @@ Section logrel.
       rewrite !lookup_app_r; [|lia ..].
       destruct (x - length Δ1) as [|n] eqn:?; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
-      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
+      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
     - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
     - intros w; simpl; properness; auto. by apply IHτ.
   Qed.
@@ -154,11 +150,11 @@ Section logrel.
   Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2.
   Proof. apply (interp_subst_up []). Qed.
 
-  Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ length Γ = length vs.
+  Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ ⌜length Γ = length vs⌝.
   Proof. by iIntros "[% ?]". Qed.
 
   Lemma interp_env_Some_l Δ Γ vs x τ :
-    Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, vs !! x = Some v ∧ ⟦ τ ⟧ Δ v.
+    Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, ⌜vs !! x = Some v⌝ ∧ ⟦ τ ⟧ Δ v.
   Proof.
     iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
     destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
@@ -173,7 +169,7 @@ Section logrel.
   Lemma interp_env_cons Δ Γ vs τ v :
     ⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs.
   Proof.
-    rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
+    rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ ⌜(_ = _)⌝%I) -assoc.
     by apply sep_proper; [apply pure_proper; omega|].
   Qed.
 

F_mu_ref_conc/soundness_binary.v

 From iris_logrel.F_mu_ref_conc Require Export context_refinement.
-From iris.algebra Require Import frac dec_agree.
-From iris.base_logic Require Import big_op auth.
+From iris.algebra Require Import frac agree.
+From iris.base_logic Require Import big_op.
+From iris.base_logic Require Export auth.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import adequacy.
+From iris_logrel.F_mu_ref_conc Require Import soundness_unary.
 
-Lemma basic_soundness Σ `{irisPreG lang Σ, authG Σ heapUR, authG Σ cfgUR}
+Lemma basic_soundness Σ `{heapPreIG Σ, authG Σ cfgUR}
     e e' τ v thp hp :
-  (∀ `{cfgSG Σ}, [] ⊨ e ≤log≤ e' : τ) →
+  (∀ `{cfgSG Σ} `{heapIG Σ}, [] ⊨ e ≤log≤ e' : τ) →
   rtc step ([e], ∅) (of_val v :: thp, hp) →
   (∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp')).
 Proof.
   intros Hlog Hsteps.
   cut (adequate e ∅ (λ _, ∃ thp' h v, rtc step ([e'], ∅) (of_val v :: thp', h))).
   { destruct 1; naive_solver. }
-  eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iMod (auth_alloc to_heap ownP heapN _ ∅ with "[Hσ]")
-    as (γh) "[#Hh1 Hh2]"; auto; first done.
+  eapply (wp_adequacy Σ _); iIntros (Hinv). 
+  iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
+  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ ∅)). }
   iMod (own_alloc (● (to_tpool [e'], ∅)
-    ⋅ ◯ (({[ 0 := Excl e' ]} : tpoolUR, ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
+    ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
   { apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
-  set (Hcfg := CFGSG _ (HeapIG _ _ _ γh) _ γc).
+  set (Hcfg := CFGSG _ _ γc).  
   iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
-  { iNext. iExists [e'], ∅. rewrite {2}/to_heap fin_maps.map_fmap_empty. auto. }
-  rewrite -(empty_env_subst e).
-  iApply wp_fupd; iApply wp_wand_r; iSplitL; [iApply (bin_log_related_alt
-    (Hlog _) [] [] ([e'], ∅) 0 [])|]; simpl.
-  { rewrite /heapI_ctx /spec_ctx /auth_ctx /tpool_mapsto /auth_own /=.
-    rewrite empty_env_subst -interp_env_nil. by iFrame "Hh1 Hcfg Hcfg2". }
+  { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
+  set (HΣ := IrisG _ _ Hinv (λ σ, own γ (● to_gen_heap σ))%I).
+  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
+  iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
+  iApply wp_fupd. iApply wp_wand_r.
+  iSplitL.
+  iPoseProof ((Hlog _ _ [] [] ([e'], ∅)) with "[$Hcfg]") as "Hrel".
+  { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
+  simpl.
+  rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
+  { rewrite /tpool_mapsto. asimpl. iFrame. }
   iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
   iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
   rewrite /tpool_mapsto /auth.auth_own /=.
@@ -38,13 +45,13 @@ Proof.
   iIntros "!> !%"; eauto.
 Qed.
 
-Lemma binary_soundness Σ `{irisPreG lang Σ, authG Σ heapUR, authG Σ cfgUR}
+Lemma binary_soundness Σ `{heapPreIG Σ, authG Σ cfgUR}
     Γ e e' τ :
   (∀ f, e.[upn (length Γ) f] = e) →
   (∀ f, e'.[upn (length Γ) f] = e') →
-  (∀ `{cfgSG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
+  (∀ `{cfgSG Σ} `{heapIG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
   Γ ⊨ e ≤ctx≤ e' : τ.
 Proof.
-  intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ)=> ?.
+  intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ _)=> ??.
   eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
 Qed.

F_mu_ref_conc/soundness_unary.v

@@ -3,18 +3,28 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import adequacy.
 From iris.base_logic Require Import auth.
 
+Class heapPreIG Σ := HeapPreIG {
+  heap_preG_iris :> invPreG Σ;
+  heap_preG_heap :> gen_heapPreG loc val Σ
+}.
 
-Theorem soundness Σ `{irisPreG lang Σ, authG Σ heapUR} e τ e' thp σ σ' :
+Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
   (∀ `{heapIG Σ}, log_typed [] e τ) →
   rtc step ([e], σ) (thp, σ') → e' ∈ thp →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
   intros Hlog ??. cut (adequate e σ (λ _, True)); first (intros [_ ?]; eauto).
-  eapply (wp_adequacy Σ); iIntros (?) "Hσ". rewrite -(empty_env_subst e).
-  iMod (auth_alloc to_heap ownP heapN _ σ with "[Hσ]") as (γ) "[??]"; auto.
-  - auto using to_heap_valid.
-  - iApply wp_wand_l; iSplitR; [|iApply (Hlog (HeapIG _ _ _ γ))]; eauto.
-    iSplit. by rewrite /heapI_ctx. iApply (@interp_env_nil _ (HeapIG _ _ _ γ)).
+  eapply (wp_adequacy Σ _). 
+  iIntros (Hinv). 
+  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
+  - apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)).
+  - iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
+    set (HΣ := IrisG _ _ Hinv (λ σ, own γ (● to_gen_heap σ))%I).
+    iApply wp_wand_r.
+    iSplitR. rewrite -(empty_env_subst e).
+    set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
+    iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
+    eauto.
 Qed.
 
 Corollary type_soundness e τ e' thp σ σ' :
@@ -22,6 +32,7 @@ Corollary type_soundness e τ e' thp σ σ' :
   rtc step ([e], σ) (thp, σ') → e' ∈ thp →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
-  intros ??. set (Σ := #[irisΣ state ; authΣ heapUR ]).
+  intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]).
+  set (HG := HeapPreIG Σ _ _). 
   eapply (soundness Σ); eauto using fundamental.
 Qed.