bump Iris, fix for gen_heap supporting heap metadata

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-09.3.31bf88ff") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-10.2.47f304f6") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/logrel/F_mu_ref/rules.v

@@ -65,7 +65,7 @@ Section lang_rules.
     iApply wp_lift_atomic_head_step_no_fork; auto.
     iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
     iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
-    iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+    iMod (@gen_heap_alloc with "Hσ") as "(Hσ & Hl & _)"; first done.
     iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
   Qed.
 

theories/logrel/F_mu_ref/soundness.v

@@ -16,10 +16,9 @@ Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ _); eauto.
   iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
-  iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
-  set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
+  iMod (gen_heap_init σ) as (Hheap) "Hh".
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  set (HeapΣ := (HeapG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
     iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).

theories/logrel/F_mu_ref/soundness_binary.v

@@ -15,8 +15,7 @@ Proof.
   { destruct 1; naive_solver. }
   eapply (wp_adequacy Σ); first by apply _.
   iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
+  iMod (gen_heap_init (∅: state)) as (Hheap) "Hh".
   iMod (own_alloc (● (Excl' e', ∅)
     ⋅ ◯ ((Excl' e', ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
   { apply auth_both_valid. split=>//. }
@@ -25,8 +24,8 @@ Proof.
   { iNext. iExists e', ∅. iSplit; eauto.
     rewrite /to_gen_heap fin_maps.map_fmap_empty.
     iFrame. }
-  set (HeapΣ := HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ)).
-  iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
+  set (HeapΣ := HeapG Σ Hinv Hheap).
+  iExists (λ σ _, gen_heap_ctx σ); iFrame.
   iApply wp_fupd. iApply (wp_wand with "[-]").
   - iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
     { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }

theories/logrel/F_mu_ref_conc/rules.v

@@ -60,7 +60,7 @@ Section lang_rules.
     iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
     iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
     iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
-    iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+    iMod (@gen_heap_alloc with "Hσ") as "(Hσ & Hl & _)"; first done.
     iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
   Qed.
 

theories/logrel/F_mu_ref_conc/soundness_binary.v

@@ -14,16 +14,15 @@ Proof.
   cut (adequate NotStuck e ∅ (λ _ _, ∃ thp' h v, rtc erased_step ([e'], ∅) (of_val v :: thp', h))).
   { destruct 1; naive_solver. }
   eapply (wp_adequacy Σ _); iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
+  iMod (gen_heap_init (∅: state)) as (Hheap) "Hh".
   iMod (own_alloc (● (to_tpool [e'], ∅)
     ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
   { apply auth_both_valid. split=>//. split=>//. apply to_tpool_valid. }
   set (Hcfg := CFGSG _ _ γc).
   iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
-  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
-  iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
+  set (HeapΣ := (HeapIG Σ Hinv Hheap)).
+  iExists (λ σ _, gen_heap_ctx σ); iFrame.
   iApply wp_fupd. iApply wp_wand_r.
   iSplitL.
   iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel".

theories/logrel/F_mu_ref_conc/soundness_unary.v

@@ -15,10 +15,9 @@ Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
 Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ _). iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
-  iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
-  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
+  iMod (gen_heap_init σ) as (Hheap) "Hh".
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  set (HeapΣ := (HeapIG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
     iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).