Merge branch 'ralf/gc' into 'master'

Add heap_lang lib for "invariant locations": locations with a (pure) invariant attached to them

See merge request iris/iris!289

CHANGELOG.md

@@ -17,6 +17,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * In the axiomatization of ectx languages we replace the axiom of positivity of
   context composition with an axiom that says if `fill K e` takes a head step,
   then either `K` is the empty evaluation context or `e` is a value.
+* Added a library for "invariant locations": heap locations that will not be
+  deallocated (i.e., they are GC-managed) and satisfy some pure, Coq-level
+  invariant.  See `iris.base_logic.lib.gen_inv_heap` for details.
 
 **Changes in Coq:**
 

_CoqProject

@@ -82,6 +82,7 @@ theories/base_logic/lib/boxes.v
 theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/gen_heap.v
+theories/base_logic/lib/gen_inv_heap.v
 theories/base_logic/lib/fancy_updates_from_vs.v
 theories/base_logic/lib/proph_map.v
 theories/program_logic/adequacy.v

tests/heap_lang.v

+From iris.base_logic.lib Require Import gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
@@ -202,6 +203,14 @@ Section tests.
 
 End tests.
 
+Section notation_tests.
+  Context `{!heapG Σ, inv_heapG loc val Σ}.
+
+  (* Make sure these parse and type-check. *)
+  Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
+  Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
+End notation_tests.
+
 Section printing_tests.
   Context `{!heapG Σ}.
 

theories/base_logic/lib/gen_inv_heap.v

+From iris.algebra Require Import auth excl gmap.
+From iris.base_logic.lib Require Import own invariants gen_heap.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+(** An "invariant" location is a location that has some invariant about its
+value attached to it, and that can never be deallocated explicitly by the
+program.  It provides a persistent witness that will always allow reading the
+location, guaranteeing that the value read will satisfy the invariant.
+
+This is useful for data structures like RDCSS that need to read locations long
+after their ownership has been passed back to the client, but do not care *what*
+it is that they are reading in that case. In that extreme case, the invariant
+may just be [True].
+
+Since invariant locations cannot be deallocated, they only make sense when
+modelling languages with garbage collection.  Note that heap_lang does not
+actually have explicit dealloaction. However, the proof rules we provide for
+heap operations currently are conservative in the sense that they do not expose
+this fact.  By making "invariant" locations a separate assertion, we can keep
+all the other proofs that do not need it conservative.  *)
+
+Definition inv_heapN: namespace := nroot .@ "inv_heap".
+Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
+
+Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmraT := gmapUR L $ prodR
+  (optionR $ exclR $ leibnizO V)
+  (agreeR (V -d> PropO)).
+
+Definition to_inv_heap {L V : Type} `{Countable L}
+    (h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
+  prod_map (λ x, Excl' x) to_agree <$> h.
+
+Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
+  inv_heap_inG :> inG Σ (authR (inv_heap_mapUR L V));
+  inv_heap_name : gname
+}.
+Arguments Inv_HeapG _ _ {_ _ _ _}.
+Arguments inv_heap_name {_ _ _ _ _} _ : assert.
+
+Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
+}.
+
+Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
+  #[ GFunctor (authR (inv_heap_mapUR L V)) ].
+
+Instance subG_inv_heapPreG (L V : Type) `{Countable L} {Σ} :
+  subG (inv_heapΣ L V) Σ → inv_heapPreG L V Σ.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context {L V : Type} `{Countable L}.
+  Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
+
+  Definition inv_heap_inv_P : iProp Σ :=
+    (∃ h : gmap L (V * (V -d> PropO)),
+        own (inv_heap_name gG) (● to_inv_heap h) ∗
+        [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1)%I.
+
+  Definition inv_heap_inv : iProp Σ := inv inv_heapN inv_heap_inv_P.
+
+  Definition inv_mapsto_own (l : L) (v : V) (I : V → Prop) : iProp Σ :=
+    own (inv_heap_name gG) (◯ {[l := (Excl' v, to_agree I) ]}).
+
+  Definition inv_mapsto (l : L) (I : V → Prop) : iProp Σ :=
+    own (inv_heap_name gG) (◯ {[l := (None, to_agree I)]}).
+
+End definitions.
+
+Local Notation "l '↦□' I" := (inv_mapsto l I%stdpp%type)
+  (at level 20, format "l  '↦□'  I") : bi_scope.
+
+Local Notation "l '↦_' I  v" := (inv_mapsto_own l v I%stdpp%type)
+  (at level 20, I at level 9, format "l  '↦_' I  v") : bi_scope.
+
+(* [inv_heap_inv] has no parameters to infer the types from, so we need to
+   make them explicit. *)
+Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.
+
+Instance: Params (@inv_mapsto_own) 8 := {}.
+Instance: Params (@inv_mapsto) 7 := {}.
+
+Section to_inv_heap.
+  Context {L V : Type} `{Countable L}.
+  Implicit Types (h : gmap L (V * (V -d> PropO))).
+
+  Lemma to_inv_heap_valid h : ✓ to_inv_heap h.
+  Proof. intros l. rewrite lookup_fmap. by case (h !! l). Qed.
+
+  Lemma to_inv_heap_singleton l v I :
+    to_inv_heap {[l := (v, I)]} =@{inv_heap_mapUR L V} {[l := (Excl' v, to_agree I)]}.
+  Proof. by rewrite /to_inv_heap fmap_insert fmap_empty. Qed.
+
+  Lemma to_inv_heap_insert l v I h :
+    to_inv_heap (<[l := (v, I)]> h) = <[l := (Excl' v, to_agree I)]> (to_inv_heap h).
+  Proof. by rewrite /to_inv_heap fmap_insert. Qed.
+
+  Lemma lookup_to_inv_heap_None h l :
+    h !! l = None → to_inv_heap h !! l = None.
+  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.
+
+  Lemma lookup_to_inv_heap_Some h l v I :
+    h !! l = Some (v, I) → to_inv_heap h !! l = Some (Excl' v, to_agree I).
+  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.
+
+  Lemma lookup_to_inv_heap_Some_2 h l v' I' :
+    to_inv_heap h !! l ≡ Some (v', I') →
+    ∃ v I, v' = Excl' v ∧ I' ≡ to_agree I ∧ h !! l = Some (v, I).
+  Proof.
+    rewrite /to_inv_heap /prod_map lookup_fmap. rewrite fmap_Some_equiv.
+    intros ([] & Hsome & [Heqv HeqI]); simplify_eq/=; eauto.
+  Qed.
+End to_inv_heap.
+
+Lemma inv_heap_init {L V : Type} `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E:
+  ⊢ |==> ∃ _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V.
+Proof.
+  iMod (own_alloc (● (to_inv_heap ∅))) as (γ) "H●".
+  { rewrite auth_auth_valid. exact: to_inv_heap_valid. }
+  iModIntro.
+  iExists (Inv_HeapG L V γ).
+  iAssert (inv_heap_inv_P (gG := Inv_HeapG L V γ)) with "[H●]" as "P".
+  { iExists _. iFrame. done. }
+  iApply (inv_alloc inv_heapN E inv_heap_inv_P with "P").
+Qed.
+
+Section inv_heap.
+  Context {L V : Type} `{Countable L}.
+  Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
+  Implicit Types (l : L) (v : V) (I : V → Prop).
+  Implicit Types (h : gmap L (V * (V -d> PropO))).
+
+  (** * Helpers *)
+
+  Lemma inv_mapsto_lookup_Some l h I :
+    l ↦□ I -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
+    ⌜∃ v I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
+  Proof.
+    iIntros "Hl_inv H◯".
+    iDestruct (own_valid_2 with "H◯ Hl_inv") as %[Hincl Hvalid]%auth_both_valid.
+    iPureIntro.
+    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
+    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
+    move: Hincl; rewrite HI Some_included_total pair_included
+      to_agree_included; intros [??]; eauto.
+  Qed.
+
+  Lemma inv_mapsto_own_lookup_Some l v h I :
+    l ↦_I v -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
+    ⌜ ∃ I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
+  Proof.
+    iIntros "Hl_inv H●".
+    iDestruct (own_valid_2 with "H● Hl_inv") as %[Hincl Hvalid]%auth_both_valid.
+    iPureIntro.
+    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
+    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
+    move: Hincl; rewrite HI Some_included_total pair_included
+      Excl_included to_agree_included; intros [-> ?]; eauto.
+  Qed.
+
+  (** * Typeclass instances *)
+
+  (* FIXME(Coq #6294): needs new unification
+  The uses of [apply:] and [move: ..; rewrite ..] (by lack of [apply: .. in ..])
+  in this file are needed because Coq's default unification algorithm fails. *)
+  Global Instance inv_mapsto_own_proper l v :
+    Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto_own l v).
+  Proof.
+    intros I1 I2 ?. rewrite /inv_mapsto_own. do 2 f_equiv.
+    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
+  Qed.
+  Global Instance inv_mapsto_proper l :
+    Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto l).
+  Proof.
+    intros I1 I2 ?. rewrite /inv_mapsto. do 2 f_equiv.
+    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
+  Qed.
+
+  Global Instance inv_mapsto_persistent l I : Persistent (l ↦□ I).
+  Proof. rewrite /inv_mapsto. apply _. Qed.
+
+  Global Instance inv_mapsto_timeless l I : Timeless (l ↦□ I).
+  Proof. rewrite /inv_mapsto. apply _. Qed.
+
+  Global Instance inv_mapsto_own_timeless l v I : Timeless (l ↦_I v).
+  Proof. rewrite /inv_mapsto. apply _. Qed.
+
+  (** * Public lemmas *)
+
+  Lemma make_inv_mapsto l v I E :
+    ↑inv_heapN ⊆ E →
+    I v →
+    inv_heap_inv L V -∗ l ↦ v ={E}=∗ l ↦_I v.
+  Proof.
+    iIntros (HN HI) "#Hinv Hl".
+    iMod (inv_acc_timeless _ inv_heapN with "Hinv") as "[HP Hclose]"; first done.
+    iDestruct "HP" as (h) "[H● HsepM]".
+    destruct (h !! l) as [v'| ] eqn: Hlookup.
+    - (* auth map contains l --> contradiction *)
+      iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
+      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
+    - iMod (own_update with "H●") as "[H● H◯]".
+      { apply lookup_to_inv_heap_None in Hlookup.
+        apply (auth_update_alloc _
+          (to_inv_heap (<[l:=(v,I)]> h)) (to_inv_heap ({[l:=(v,I)]}))).
+        rewrite to_inv_heap_insert to_inv_heap_singleton.
+        by apply: alloc_singleton_local_update. }
+      iMod ("Hclose" with "[H● HsepM Hl]").
+      + iExists _.
+        iDestruct (big_sepM_insert _ _ _ (_,_) with "[$HsepM $Hl]")
+          as "HsepM"; auto with iFrame.
+      + iModIntro. by rewrite /inv_mapsto_own to_inv_heap_singleton.
+  Qed.
+
+  Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦□ I.
+  Proof.
+    apply own_mono, auth_frag_mono. rewrite singleton_included pair_included.
+    right. split; [apply: ucmra_unit_least|done].
+  Qed.
+
+  (** An accessor to make use of [inv_mapsto_own].
+    This opens the invariant *before* consuming [inv_mapsto_own] so that you can use
+    this before opening an atomic update that provides [inv_mapsto_own]!. *)
+  Lemma inv_mapsto_own_acc_strong E :
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv L V ={E, E ∖ ↑inv_heapN}=∗ ∀ l v I, l ↦_I v -∗
+      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗
+        inv_mapsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
+  Proof.
+    iIntros (HN) "#Hinv".
+    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
+    iIntros "!>" (l v I) "Hl_inv".
+    iDestruct "HP" as (h) "[H● HsepM]".
+    iDestruct (inv_mapsto_own_lookup_Some with "Hl_inv H●") as %(I'&?&HI').
+    setoid_rewrite HI'.
+    iDestruct (big_sepM_delete with "HsepM") as "[[HI Hl] HsepM]"; first done.
+    iIntros "{$HI $Hl}" (w ?) "Hl".
+    iMod (own_update_2 with "H● Hl_inv") as "[H● H◯]".
+    { apply (auth_update _ _ (<[l := (Excl' w, to_agree I')]> (to_inv_heap h))
+             {[l := (Excl' w, to_agree I)]}).
+      apply: singleton_local_update.
+      { by apply lookup_to_inv_heap_Some. }
+      apply: prod_local_update_1. apply: option_local_update.
+      apply: exclusive_local_update. done. }
+    iDestruct (big_sepM_insert _ _ _ (w, I') with "[$HsepM $Hl //]") as "HsepM".
+    { apply lookup_delete. }
+    rewrite insert_delete -to_inv_heap_insert. iIntros "!> {$H◯}".
+    iApply ("Hclose" with "[H● HsepM]"). iExists _; by iFrame.
+  Qed.
+
+  (** Derive a more standard accessor. *)
+  Lemma inv_mapsto_own_acc E l v I:
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv L V -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
+      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
+  Proof.
+    iIntros (?) "#Hinv Hl".
+    iMod (inv_mapsto_own_acc_strong with "Hinv") as "Hacc"; first done.
+    iDestruct ("Hacc" with "Hl") as "(HI & Hl & Hclose)".
+    iIntros "!> {$HI $Hl}" (w) "HI Hl".
+    iMod ("Hclose" with "HI Hl") as "[$ $]".
+  Qed.
+
+  Lemma inv_mapsto_acc l I E :
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv L V -∗ l ↦□ I ={E, E ∖ ↑inv_heapN}=∗
+    ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
+  Proof.
+    iIntros (HN) "#Hinv Hl_inv".
+    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
+    iModIntro.
+    iDestruct "HP" as (h) "[H● HsepM]".
+    iDestruct (inv_mapsto_lookup_Some with "Hl_inv H●") as %(v&I'&?&HI').
+    iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"; first done.
+    setoid_rewrite HI'.
+    iExists _. iIntros "{$HI $Hl} Hl".
+    iMod ("Hclose" with "[H● HsepM Hl]"); last done.
+    iExists _. iFrame "H●". iApply ("HsepM" with "[$Hl //]").
+  Qed.
+
+End inv_heap.
+
+Typeclasses Opaque inv_mapsto inv_mapsto_own.

theories/heap_lang/adequacy.v

 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
-From iris.base_logic.lib Require Import proph_map.
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
@@ -8,10 +7,11 @@ Set Default Proof Using "Type".
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
   heap_preG_heap :> gen_heapPreG loc val Σ;
-  heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ
+  heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
 }.
 
-Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
+Definition heapΣ : gFunctors :=
+  #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 

theories/heap_lang/lifting.v

 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
-From iris.base_logic Require Export gen_heap.
-From iris.base_logic.lib Require Export proph_map.
+From iris.base_logic.lib Require Export gen_heap proph_map.
+From iris.base_logic.lib Require Import gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
@@ -12,7 +12,7 @@ Set Default Proof Using "Type".
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
   heapG_gen_heapG :> gen_heapG loc val Σ;
-  heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ
+  heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
 }.
 
 Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
@@ -31,6 +31,11 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
+Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
+  (at level 20, format "l  ↦□  I") : bi_scope.
+Notation "l ↦_ I  v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
+  (at level 20, I at level 9, format "l  ↦_ I   v") : bi_scope.
+
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
 simplifies hypothesis related to conversions from and to values, and finite map