Merge branch 'view-bij' into 'master'

Implement monotone partial bijections as a view

See merge request iris/iris!543

CHANGELOG.md

@@ -58,6 +58,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Add `mono_nat`, a wrapper for `auth max_nat`. The result is an authoritative
   `nat` where a fragment is a lower bound whose ownership is persistent.
   See [algebra.lib.mono_nat](iris/algebra/lib/mono_nat.v) for further information.
+* Add the `gset_bij` resource algebra for monotone partial bijections.
+  See [algebra.lib.gset_bij](iris/algebra/lib/gset_bij.v) for further information.
 * Change `*_valid` lemma statements involving fractions to use `Qp` addition and
   inequality instead of RA composition and validity (also in `base_logic` and
   the higher layers).
@@ -128,6 +130,9 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Define a ghost state library on top of the `mono_nat` resource algebra.
   See [base_logic.lib.mono_nat](iris/base_logic/lib/mono_nat.v) for further
   information.
+* Define a ghost state library on top of the `gset_bij` resource algebra.
+  See [base_logic.lib.gset_bij](iris/base_logic/lib/gset_bij.v) for further
+  information.
 * Remove the `gen_heap` notations `l ↦ -` and `l ↦{q} -`. They were barely used
   and looked very confusing in context: `l ↦ - ∗ P` looks like a magic wand.
 * Change `gen_inv_heap` notation `l ↦□ I` to `l ↦_I □`, so that `↦□` can be used

_CoqProject

@@ -50,6 +50,7 @@ iris/algebra/lib/ufrac_auth.v
 iris/algebra/lib/frac_agree.v
 iris/algebra/lib/gmap_view.v
 iris/algebra/lib/mono_nat.v
+iris/algebra/lib/gset_bij.v
 iris/si_logic/siprop.v
 iris/si_logic/bi.v
 iris/bi/notation.v
@@ -99,6 +100,7 @@ iris/base_logic/lib/fancy_updates_from_vs.v
 iris/base_logic/lib/proph_map.v
 iris/base_logic/lib/ghost_var.v
 iris/base_logic/lib/mono_nat.v
+iris/base_logic/lib/gset_bij.v
 iris/program_logic/adequacy.v
 iris/program_logic/lifting.v
 iris/program_logic/weakestpre.v

iris/algebra/lib/gset_bij.v

+(** RA for monotone partial bijections.
+
+This RA is a view where the authoritative element is a partial bijection between
+types [A] and [B] and the fragments are subrels of the bijection. The data for
+the bijection is represented as a set of pairs [A * B], and the view relation
+enforces when an authoritative element is valid it is a bijection (that is, it
+is deterministic as a function from [A → option B] and [B → option A]).
+
+The fragments compose by set union, which means that fragments are their own
+core, ownership of a fragment is persistent, and the authoritative element can
+only grow (in that it can only map more pairs [(a,b)]). *)
+
+(* [algebra.view] needs to be exported for the canonical instances *)
+From iris.algebra Require Export view gset.
+From iris.algebra Require Import updates.
+From iris.prelude Require Import options.
+
+Section gset_bijective.
+  Context `{Countable A, Countable B}.
+  Implicit Types (a : A) (b : B).
+
+  (** [gset_bijective] states that for a graph [L] of [(a, b)] pairs, [L] maps
+  from [A] to [B] and back deterministically. The key property characterizing
+  [gset_bijective] is [gset_bijective_eq_iff]. *)
+  Definition gset_bijective (L : gset (A * B)) :=
+    ∀ a b, (a, b) ∈ L →
+    (∀ b', (a, b') ∈ L → b' = b) ∧ (∀ a', (a', b) ∈ L → a' = a).
+
+  (* Properties of [gset_bijective]. *)
+  Lemma gset_bijective_empty : gset_bijective (∅ : gset (A * B)).
+  Proof. by intros ?? []%not_elem_of_empty. Qed.
+
+  (* a bijective graph [L] can be extended with a new mapping [(a,b)] as long as
+  neither [a] nor [b] is currently mapped to anything. *)
+  Lemma gset_bijective_extend L a b :
+    gset_bijective L →
+    (∀ b', (a, b') ∉ L) →
+    (∀ a', (a', b) ∉ L) →
+    gset_bijective ({[(a, b)]} ∪ L).
+  Proof. rewrite /gset_bijective. set_solver. Qed.
+
+  Lemma gset_bijective_eq_iff L (a1 a2 : A) (b1 b2 : B) :
+    gset_bijective L →
+    (a1, b1) ∈ L →
+    (a2, b2) ∈ L →
+    a1 = a2 ↔ b1 = b2.
+  Proof. rewrite /gset_bijective. set_solver. Qed.
+
+  Lemma gset_bijective_pair a1 b1 a2 b2 :
+    gset_bijective {[(a1, b1); (a2, b2)]} →
+    (a1 = a2 ↔ b1 = b2).
+  Proof. rewrite /gset_bijective. set_solver. Qed.
+
+  Lemma subseteq_gset_bijective L L' :
+    gset_bijective L →
+    L' ⊆ L →
+    gset_bijective L'.
+  Proof. rewrite /gset_bijective. set_solver. Qed.
+End gset_bijective.
+
+Section gset_bij_view_rel.
+  Context `{Countable A, Countable B}.
+  Implicit Types (bijL : gset (A * B)) (L : gsetUR (A * B)).
+
+  Local Definition gset_bij_view_rel_raw (n : nat) bijL L: Prop :=
+    L ⊆ bijL ∧ gset_bijective bijL.
+
+  Local Lemma gset_bij_view_rel_raw_mono n1 n2 bijL1 bijL2 L1 L2 :
+    gset_bij_view_rel_raw n1 bijL1 L1 →
+    bijL1 ≡{n2}≡ bijL2 →
+    L2 ≼{n2} L1 →
+    n2 ≤ n1 →
+    gset_bij_view_rel_raw n2 bijL2 L2.
+  Proof.
+    intros [??] <-%(discrete_iff _ _)%leibniz_equiv ?%gset_included _.
+    split; [|done]. by trans L1.
+  Qed.
+
+  Local Lemma gset_bij_view_rel_raw_valid n bijL L :
+    gset_bij_view_rel_raw n bijL L → ✓{n}L.
+  Proof. by intros _. Qed.
+
+  Local Lemma gset_bij_view_rel_raw_unit n :
+    ∃ bijL, gset_bij_view_rel_raw n bijL ε.
+  Proof. exists ∅. split; eauto using gset_bijective_empty. Qed.
+
+  Canonical Structure gset_bij_view_rel : view_rel (gsetO (A * B)) (gsetUR (A * B)) :=
+    ViewRel gset_bij_view_rel_raw gset_bij_view_rel_raw_mono
+            gset_bij_view_rel_raw_valid gset_bij_view_rel_raw_unit.
+
+  Global Instance gset_bij_view_rel_discrete : ViewRelDiscrete gset_bij_view_rel.
+  Proof. intros n bijL L [??]. split; auto. Qed.
+
+  Local Lemma gset_bij_view_rel_iff n bijL L :
+    gset_bij_view_rel n bijL L ↔ L ⊆ bijL ∧ gset_bijective bijL.
+  Proof. done. Qed.
+End gset_bij_view_rel.
+
+Definition gset_bij A B `{Countable A, Countable B} :=
+  view (gset_bij_view_rel_raw (A:=A) (B:=B)).
+Definition gset_bijO A B `{Countable A, Countable B} : ofeT :=
+  viewO (gset_bij_view_rel (A:=A) (B:=B)).
+Definition gset_bijR A B `{Countable A, Countable B} : cmraT :=
+  viewR (gset_bij_view_rel (A:=A) (B:=B)).
+Definition gset_bijUR A B `{Countable A, Countable B} : ucmraT :=
+  viewUR (gset_bij_view_rel (A:=A) (B:=B)).
+
+Definition gset_bij_auth `{Countable A, Countable B}
+  (q : Qp) (L : gset (A * B)) : gset_bij A B := ●V{q} L ⋅ ◯V L.
+Definition gset_bij_elem `{Countable A, Countable B}
+  (a : A) (b : B) : gset_bij A B := ◯V {[a, b]}.
+
+Section gset_bij.
+  Context `{Countable A, Countable B}.
+  Implicit Types (a:A) (b:B).
+  Implicit Types (L : gset (A*B)).
+
+  Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
+  Proof. apply _. Qed.
+
+  Lemma gset_bij_auth_frac_op q1 q2 L :
+    gset_bij_auth q1 L ⋅ gset_bij_auth q2 L ≡ gset_bij_auth (q1 + q2) L.
+  Proof.
+    rewrite /gset_bij_auth view_auth_frac_op.
+    rewrite (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    by rewrite -core_id_dup (comm _ (◯V _)).
+  Qed.
+
+  Lemma gset_bij_auth_frac_valid q L : ✓ gset_bij_auth q L ↔ ✓ q ∧ gset_bijective L.
+  Proof.
+    rewrite /gset_bij_auth view_both_frac_valid.
+    setoid_rewrite gset_bij_view_rel_iff.
+    naive_solver eauto using O.
+  Qed.
+  Lemma gset_bij_auth_valid L : ✓ gset_bij_auth 1 L ↔ gset_bijective L.
+  Proof. rewrite gset_bij_auth_frac_valid. naive_solver by done. Qed.
+
+  Lemma gset_bij_auth_empty_frac_valid q : ✓ gset_bij_auth (A:=A) (B:=B) q ∅ ↔ ✓ q.
+  Proof.
+    rewrite gset_bij_auth_frac_valid. naive_solver eauto using gset_bijective_empty.
+  Qed.
+  Lemma gset_bij_auth_empty_valid : ✓ gset_bij_auth (A:=A) (B:=B) 1 ∅.
+  Proof. by apply gset_bij_auth_empty_frac_valid. Qed.
+
+  Lemma gset_bij_auth_frac_op_valid q1 q2 L1 L2 :
+    ✓ (gset_bij_auth q1 L1 ⋅ gset_bij_auth q2 L2)
+    ↔ ✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1.
+  Proof.
+    rewrite /gset_bij_auth (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    rewrite -view_frag_op (comm _ (◯V _)) assoc. split.
+    - move=> /cmra_valid_op_l /view_auth_frac_op_valid.
+      setoid_rewrite gset_bij_view_rel_iff. naive_solver eauto using 0.
+    - intros (?&->&?). rewrite -core_id_dup -view_auth_frac_op.
+      apply view_both_frac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
+  Qed.
+  Lemma gset_bij_auth_op_valid L1 L2 :
+    ✓ (gset_bij_auth 1 L1 ⋅ gset_bij_auth 1 L2) ↔ False.
+  Proof. rewrite gset_bij_auth_frac_op_valid. naive_solver. Qed.
+
+  Lemma bij_both_frac_valid q L a b :
+    ✓ (gset_bij_auth q L ⋅ gset_bij_elem a b) ↔ ✓ q ∧ gset_bijective L ∧ (a, b) ∈ L.
+  Proof.
+    rewrite /gset_bij_auth /gset_bij_elem -assoc -view_frag_op view_both_frac_valid.
+    setoid_rewrite gset_bij_view_rel_iff.
+    set_solver by eauto using O.
+  Qed.
+  Lemma bij_both_valid L a b :
+    ✓ (gset_bij_auth 1 L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
+  Proof. rewrite bij_both_frac_valid. naive_solver by done. Qed.
+
+  Lemma gset_bij_elem_agree a1 b1 a2 b2 :
+    ✓ (gset_bij_elem a1 b1 ⋅ gset_bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
+  Proof.
+    rewrite /gset_bij_elem -view_frag_op gset_op_union view_frag_valid.
+    setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
+    naive_solver eauto using subseteq_gset_bijective, O.
+  Qed.
+
+  Lemma bij_view_included q L a b :
+    (a,b) ∈ L → gset_bij_elem a b ≼ gset_bij_auth q L.
+  Proof.
+    intros. etrans; [|apply cmra_included_r].
+    apply view_frag_mono, gset_included. set_solver.
+  Qed.
+
+  Lemma gset_bij_auth_extend {L} a b :
+    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
+    gset_bij_auth 1 L ~~> gset_bij_auth 1 ({[(a, b)]} ∪ L).
+  Proof.
+    intros. apply view_update=> n bijL.
+    rewrite !gset_bij_view_rel_iff gset_op_union.
+    set_solver by eauto using gset_bijective_extend.
+  Qed.
+End gset_bij.

iris/base_logic/lib/gset_bij.v

+(** Propositions for reasoning about monotone partial bijections.
+
+This library provides two propositions [gset_bij_own_auth γ L] and
+[gset_bij_own_elem γ a b], where [L] is a bijection between types [A] and [B]
+represented by a set of associations [gset (A * B)]. The idea is that
+[gset_bij_own_auth γ L] is an authoritative bijection [L], while
+[gset_bij_own_elem γ a b] is a persistent resource saying [L] associates [a]
+and [b].
+
+The main use case is in a logical relation-based proof where [L] maintains the
+association between locations [A] in one execution and [B] in another (perhaps
+of different types, if the logical relation relates two different semantics).
+
+The association [L] is always bijective, so that if [a] is mapped to [b], there
+should be no other mappings for either [a] or [b]; the [gset_bij_own_extend]
+update theorem enforces that new mappings respect this property, and
+[gset_bij_own_elem_agree] allows the user to exploit bijectivity. The bijection
+grows monotonically, so that the set of associations only grows; this is
+captured by the persistence of [gset_bij_own_elem].
+
+This library is a logical, ownership-based wrapper around [gset_bij]. *)
+
+From iris.algebra.lib Require Import gset_bij.
+From iris.bi.lib Require Import fractional.
+From iris.base_logic.lib Require Import own.
+From iris.proofmode Require Import tactics.
+From iris.prelude Require Import options.
+
+(* The uCMRA we need. *)
+Class gset_bijG A B `{Countable A, Countable B} Σ :=
+  GsetBijG { gset_bijG_inG :> inG Σ (gset_bijR A B); }.
+
+Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
+  #[ GFunctor (gset_bijR A B) ].
+Global Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
+  subG (gset_bijΣ A B) Σ → gset_bijG A B Σ.
+Proof. solve_inG. Qed.
+
+Definition gset_bij_own_auth_def `{gset_bijG A B Σ} (γ : gname)
+    (q : Qp) (L : gset (A * B)) : iProp Σ :=
+  own γ (gset_bij_auth q L).
+Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexists. Qed.
+Definition gset_bij_own_auth := unseal gset_bij_own_auth_aux.
+Definition gset_bij_own_auth_eq :
+  @gset_bij_own_auth = @gset_bij_own_auth_def := seal_eq gset_bij_own_auth_aux.
+Arguments gset_bij_own_auth {_ _ _ _ _ _ _ _}.
+
+Definition gset_bij_own_elem_def `{gset_bijG A B Σ} (γ : gname)
+  (a : A) (b : B) : iProp Σ := own γ (gset_bij_elem a b).
+Definition gset_bij_own_elem_aux : seal (@gset_bij_own_elem_def). Proof. by eexists. Qed.
+Definition gset_bij_own_elem := unseal gset_bij_own_elem_aux.
+Definition gset_bij_own_elem_eq :
+  @gset_bij_own_elem = @gset_bij_own_elem_def := seal_eq gset_bij_own_elem_aux.
+Arguments gset_bij_own_elem {_ _ _ _ _ _ _ _}.
+
+Section gset_bij.
+  Context `{gset_bijG A B Σ}.
+  Implicit Types (L : gset (A * B)) (a : A) (b : B).
+
+  Global Instance gset_bij_own_auth_timeless γ q L :
+    Timeless (gset_bij_own_auth γ q L).
+  Proof. rewrite gset_bij_own_auth_eq. apply _. Qed.
+  Global Instance gset_bij_own_elem_timeless γ a b :
+    Timeless (gset_bij_own_elem γ a b).
+  Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
+  Global Instance gset_bij_own_elem_persistent γ a b :
+    Persistent (gset_bij_own_elem γ a b).
+  Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
+
+  Global Instance gset_bij_own_auth_fractional γ L :
+    Fractional (λ q, gset_bij_own_auth γ q L).
+  Proof.
+    intros p q. rewrite gset_bij_own_auth_eq -own_op gset_bij_auth_frac_op //.
+  Qed.
+  Global Instance gset_bij_own_auth_as_fractional γ q L :
+    AsFractional (gset_bij_own_auth γ q L) (λ q, gset_bij_own_auth γ q L) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma gset_bij_own_auth_agree γ q1 q2 L1 L2 :
+    gset_bij_own_auth γ q1 L1 -∗ gset_bij_own_auth γ q2 L2 -∗
+    ⌜✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1⌝.
+  Proof.
+    rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
+    by iDestruct (own_valid_2 with "H1 H2") as %?%gset_bij_auth_frac_op_valid.
+  Qed.
+  Lemma gset_bij_own_auth_exclusive γ L1 L2 :
+    gset_bij_own_auth γ 1 L1 -∗ gset_bij_own_auth γ 1 L2 -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    by iDestruct (gset_bij_own_auth_agree with "H1 H2") as %[[] _].
+  Qed.
+
+  Lemma gset_bij_own_valid γ q L :
+    gset_bij_own_auth γ q L -∗ ⌜✓ q ∧ gset_bijective L⌝.
+  Proof.
+    rewrite gset_bij_own_auth_eq. iIntros "Hauth".
+    by iDestruct (own_valid with "Hauth") as %?%gset_bij_auth_frac_valid.
+  Qed.
+
+  Lemma gset_bij_own_elem_agree γ L a a' b b' :
+    gset_bij_own_elem γ a b -∗ gset_bij_own_elem γ a' b' -∗
+    ⌜a = a' ↔ b = b'⌝.
+  Proof.
+    rewrite gset_bij_own_elem_eq. iIntros "Hel1 Hel2".
+    by iDestruct (own_valid_2 with "Hel1 Hel2") as %?%gset_bij_elem_agree.
+  Qed.
+
+  Lemma gset_bij_own_elem_get {γ q L} a b :
+    (a, b) ∈ L →
+    gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b.
+  Proof.
+    intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
+    by apply own_mono, bij_view_included.
+  Qed.
+  Lemma gset_bij_own_elem_get_big γ q L :
+    gset_bij_own_auth γ q L -∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
+  Proof.
+    iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
+    by iApply gset_bij_own_elem_get.
+  Qed.
+
+  Lemma gset_bij_own_alloc L :
+    gset_bijective L →
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 L ∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
+  Proof.
+    intro. iAssert (∃ γ, gset_bij_own_auth γ 1 L)%I with "[>]" as (γ) "Hauth".
+    { rewrite gset_bij_own_auth_eq. iApply own_alloc. by apply gset_bij_auth_valid. }
+    iExists γ. iModIntro. iSplit; [done|].
+    by iApply gset_bij_own_elem_get_big.
+  Qed.
+  Lemma gset_bij_own_alloc_empty :
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 ∅.
+  Proof. iMod (gset_bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
+
+  Lemma gset_bij_own_extend {γ L} a b :
+    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
+    gset_bij_own_auth γ 1 L ==∗
+    gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+  Proof.
+    iIntros (??) "Hauth".
+    iAssert (gset_bij_own_auth γ 1 ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
+    { rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
+      by apply gset_bij_auth_extend. }
+    iModIntro. iSplit; [done|].
+    iApply (gset_bij_own_elem_get with "Hauth"). set_solver.
+  Qed.
+
+  Lemma gset_bij_own_extend_internal {γ L} a b :
+    (∀ b', gset_bij_own_elem γ a b' -∗ False) -∗
+    (∀ a', gset_bij_own_elem γ a' b -∗ False) -∗
+    gset_bij_own_auth γ 1 L ==∗
+    gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+  Proof.
+    iIntros "Ha Hb HL".
+    iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.
+    { iIntros (b' ?). iApply ("Ha" $! b'). by iApply gset_bij_own_elem_get. }
+    iAssert ⌜∀ a', (a', b) ∉ L⌝%I as %?.
+    { iIntros (a' ?). iApply ("Hb" $! a'). by iApply gset_bij_own_elem_get. }
+    by iApply (gset_bij_own_extend with "HL").
+  Qed.
+End gset_bij.