Merge branch 'ralf/gen-heap-init' into 'master'

provide _big variant of gen_heap_init

Closes #361

See merge request iris/iris!580

CHANGELOG.md

@@ -128,6 +128,8 @@ With this release, we dropped support for Coq 8.9.
   by `gen_heap`.
 * Strengthen `mapsto_valid_2` conclusion from `✓ (q1 + q2)%Qp` to
   `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`.
+* Change `gen_heap_init` to also return ownership of the points-to facts for the
+  initial heap.
 
 **Changes in `program_logic`:**
 

theories/base_logic/lib/gen_heap.v

@@ -126,17 +126,6 @@ Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
 Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
 
-Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
-  ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
-Proof.
-  iMod (own_alloc (gmap_view_auth 1 (σ : gmap L (leibnizO V)))) as (γh) "Hh".
-  { exact: gmap_view_auth_valid. }
-  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L gnameO))) as (γm) "Hm".
-  { exact: gmap_view_auth_valid. }
-  iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
-  iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
-Qed.
-
 Section gen_heap.
   Context {L V} `{Countable L, !gen_heapG L V Σ}.
   Implicit Types P Q : iProp Σ.
@@ -265,7 +254,7 @@ Section gen_heap.
     rewrite !dom_insert_L. set_solver.
   Qed.
 
-  Lemma gen_heap_alloc_gen σ σ' :
+  Lemma gen_heap_alloc_big σ σ' :
     σ' ##ₘ σ →
     gen_heap_interp σ ==∗
     gen_heap_interp (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤).
@@ -300,3 +289,20 @@ Section gen_heap.
     rewrite dom_insert_L. set_solver.
   Qed.
 End gen_heap.
+
+Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
+  ⊢ |==> ∃ _ : gen_heapG L V Σ,
+    gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
+Proof.
+  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (leibnizO V)))) as (γh) "Hh".
+  { exact: gmap_view_auth_valid. }
+  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L gnameO))) as (γm) "Hm".
+  { exact: gmap_view_auth_valid. }
+  pose (gen_heap := GenHeapG L V Σ _ _ _ _ _ γh γm).
+  iExists gen_heap.
+  iAssert (gen_heap_interp ∅) with "[Hh Hm]" as "Hinterp".
+  { iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
+  iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
+  { apply map_disjoint_empty_r. }
+  rewrite right_id_L. done.
+Qed.

theories/heap_lang/adequacy.v

@@ -21,7 +21,7 @@ Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
-  iMod (gen_heap_init σ.(heap)) as (?) "Hh".
+  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
   iModIntro. iExists

theories/heap_lang/primitive_laws.v

@@ -394,7 +394,7 @@ Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (gen_heap_alloc_gen _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
+  iMod (gen_heap_alloc_big _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
   { apply heap_array_map_disjoint.
     rewrite replicate_length Z2Nat.id; auto with lia. }

theories/heap_lang/total_adequacy.v

@@ -9,7 +9,7 @@ Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
   sn erased_step ([e], σ).
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
-  iMod (gen_heap_init σ.(heap)) as (?) "Hh".
+  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
   iModIntro.