Implement monotone partial bijections as a view

This is an alternative to !91, which was written prior to views. Using
the view CMRA we factor the implementation into purely algebraic library
and a logic-level wrapper. The logic-level wrapper exports resources
which seal away the underlying ownership and has theorems which handle
the ownership reasoning.

_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/bij_view.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/bij.v
 iris/program_logic/adequacy.v
 iris/program_logic/lifting.v
 iris/program_logic/weakestpre.v

iris/algebra/lib/bij_view.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)). *)
+
+From iris.algebra Require Import view gset updates.
+From iris.prelude Require Import options.
+
+Section partial_bijection.
+  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 partial_bijection.
+
+Section bij.
+  Context `{Countable A, Countable B}.
+  Implicit Types (bijL : gset (A * B)) (L : gsetUR (A * B)).
+
+  Local Definition bij_view_rel_raw (n : nat) bijL L: Prop :=
+    L ⊆ bijL ∧ gset_bijective bijL.
+
+  Local Lemma bij_view_rel_raw_mono n1 n2 bijL1 bijL2 L1 L2 :
+    bij_view_rel_raw n1 bijL1 L1 →
+    bijL1 ≡{n2}≡ bijL2 →
+    L2 ≼{n2} L1 →
+    n2 ≤ n1 →
+    bij_view_rel_raw n2 bijL2 L2.
+  Proof.
+    rewrite /bij_view_rel_raw.
+    intros [HL1sub ?].
+    intros <-%(discrete_iff _ _)%leibniz_equiv HL2sub%gset_included _.
+    split; [|done].
+    by trans L1.
+  Qed.
+
+  Local Lemma bij_view_rel_raw_valid n bijL L :
+    bij_view_rel_raw n bijL L → ✓{n}L.
+  Proof. intros _. hnf; auto. Qed.
+
+  Local Lemma bij_view_rel_raw_unit n :
+    ∃ bijL, bij_view_rel_raw n bijL ε.
+  Proof. exists ∅. hnf; eauto using gset_bijective_empty. Qed.
+
+  Canonical Structure bij_view_rel : view_rel (gsetO (A * B)) (gsetUR (A * B)) :=
+    ViewRel bij_view_rel_raw bij_view_rel_raw_mono bij_view_rel_raw_valid bij_view_rel_raw_unit.
+
+  Global Instance bij_view_rel_discrete : ViewRelDiscrete bij_view_rel.
+  Proof.
+    intros ???. intros [Hsub Hbij].
+    split; auto.
+  Qed.
+
+  Local Lemma bij_view_rel_iff n bijL L :
+    bij_view_rel n bijL L ↔ (L ⊆ bijL ∧ gset_bijective bijL).
+  Proof. done. Qed.
+End bij.
+
+Definition bij_view A B `{Countable A, Countable B} := (view (bij_view_rel_raw (A:=A) (B:=B))).
+Definition bij_viewO A B `{Countable A, Countable B} : ofeT := viewO (bij_view_rel (A:=A) (B:=B)).
+Definition bij_viewR A B `{Countable A, Countable B} : cmraT := viewR (bij_view_rel (A:=A) (B:=B)).
+Definition bij_viewUR A B `{Countable A, Countable B} : ucmraT := viewUR (bij_view_rel (A:=A) (B:=B)).
+
+Section bij.
+  Context {A B : Type} `{Countable A, Countable B}.
+  Implicit Types (a:A) (b:B).
+  Implicit Types (L : gset (A*B)).
+
+  Definition bij_auth L : bij_view A B := ●V L.
+  Definition bij_subrel L : bij_view A B := ◯V L.
+  Definition bij_elem a b : bij_view A B := bij_subrel {[a, b]}.
+
+  Global Instance bij_subrel_core_id L : CoreId (bij_subrel L).
+  Proof. apply _. Qed.
+
+  Global Instance bij_elem_core_id a b : CoreId (bij_elem a b).
+  Proof. apply _. Qed.
+
+  Lemma bij_subrel_insert L a b :
+    bij_subrel ({[a, b]} ∪ L) = bij_elem a b ⋅ bij_subrel L.
+  Proof.
+    rewrite /bij_elem /bij_subrel.
+    rewrite -view_frag_op //.
+  Qed.
+
+  Lemma bij_auth_valid L : ✓ bij_auth L ↔ gset_bijective L.
+  Proof.
+    rewrite /bij_auth.
+    rewrite view_auth_valid.
+    setoid_rewrite bij_view_rel_iff.
+    split; [naive_solver eauto using O|].
+    intros; split; [ apply empty_subseteq | done ].
+  Qed.
+
+  Lemma bij_auth_valid_empty : ✓ bij_auth ∅.
+  Proof.
+    rewrite bij_auth_valid.
+    apply gset_bijective_empty.
+  Qed.
+
+  Lemma bij_both_subrel_valid L L' :
+    ✓ (bij_auth L ⋅ bij_subrel L') ↔ gset_bijective L ∧ L' ⊆ L.
+  Proof.
+    rewrite view_both_valid.
+    setoid_rewrite bij_view_rel_iff.
+    naive_solver eauto using O.
+  Qed.
+
+  Lemma bij_both_el_valid L a b :
+    ✓ (bij_auth L ⋅ bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
+  Proof.
+    rewrite /bij_elem bij_both_subrel_valid.
+    rewrite elem_of_subseteq_singleton //.
+  Qed.
+
+  Lemma bij_subrel_valid L : ✓ bij_subrel L ↔ gset_bijective L.
+  Proof.
+    rewrite view_frag_valid.
+    setoid_rewrite bij_view_rel_iff.
+    split; [|by eauto].
+    intros Hrel; destruct (Hrel 0) as [L' [? ?]].
+    eauto using subseteq_gset_bijective.
+  Qed.
+
+  Lemma bij_elem_agree a1 b1 a2 b2 :
+    ✓ (bij_elem a1 b1 ⋅ bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
+  Proof.
+    rewrite /bij_elem.
+    rewrite -view_frag_op gset_op_union.
+    rewrite bij_subrel_valid.
+    apply gset_bijective_pair.
+  Qed.
+
+  Lemma bij_auth_extend {L} a b :
+    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
+    bij_auth L ~~> bij_auth (({[(a, b)]} : gset (A * B)) ∪ L) ⋅ bij_elem a b.
+  Proof.
+    intros.
+    apply view_update_alloc.
+    intros n bijL.
+    rewrite !bij_view_rel_iff gset_op_union.
+    intros [Hsub Hbij].
+    split.
+    - apply union_mono_l; auto.
+    - eauto using gset_bijective_extend.
+  Qed.
+
+  Lemma bij_auth_extend' {L} a b :
+    ¬(∃ b', (a, b') ∈ L) → ¬(∃ a', (a', b) ∈ L) →
+    bij_auth L ~~> bij_auth (({[(a, b)]} : gset (A * B)) ∪ L) ⋅ bij_elem a b.
+  Proof. by intros ??; apply bij_auth_extend; naive_solver. Qed.
+End bij.

iris/base_logic/lib/bij.v

+(** Propositions for reasoning about monotone partial bijections.
+
+This library provides two propositions [bij_own_auth γ L] and [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 [bij_own_auth γ L] is an authoritative bijection [L]
+while [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 [bij_own_extend] update
+theorem enforces that new mappings respect this property, and [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
+[bij_own_elem].
+
+This library is a logical, ownership-based wrapper around bij_view.v. *)
+
+From iris.algebra Require Import view gset lib.bij_view.
+From iris.base_logic.lib Require Import own.
+From iris.proofmode Require Import tactics.
+From iris.prelude Require Import options.
+
+Section bij.
+  Context {A B : Type}.
+  Context `{Countable A, Countable B}.
+
+  (* The uCMRA we need. *)
+  Class bijG Σ :=
+    BijG { bijG_inG :> inG Σ (bij_viewR A B); }.
+
+  Definition bijΣ : gFunctors := #[ GFunctor (bij_viewR A B) ].
+  Global Instance subG_bijΣ Σ : subG bijΣ Σ → bijG Σ.
+  Proof. solve_inG. Qed.
+
+  Context `{!bijG Σ}.
+  Implicit Types (L: gsetO (A * B)).
+  Implicit Types (a:A) (b:B).
+
+  Definition bij_own_auth_def γ L : iProp Σ := own γ (bij_auth L ⋅ bij_subrel L).
+  Definition bij_own_auth_aux : seal (@bij_own_auth_def). Proof. by eexists. Qed.
+  Definition bij_own_auth := unseal bij_own_auth_aux.
+  Definition bij_own_auth_eq : @bij_own_auth = @bij_own_auth_def := seal_eq bij_own_auth_aux.
+
+  Definition bij_own_elem_def γ a b: iProp Σ := own γ (bij_elem a b).
+  Definition bij_own_elem_aux : seal (@bij_own_elem_def). Proof. by eexists. Qed.
+  Definition bij_own_elem := unseal bij_own_elem_aux.
+  Definition bij_own_elem_eq : @bij_own_elem = @bij_own_elem_def := seal_eq bij_own_elem_aux.
+
+  Local Ltac unseal :=
+    rewrite ?bij_own_auth_eq /bij_own_auth_def ?bij_own_elem_eq /bij_own_elem_def.
+
+  Global Instance bij_own_auth_timeless γ L : Timeless (bij_own_auth γ L).
+  Proof. unseal. apply _. Qed.
+
+  Global Instance bij_own_elem_timeless γ a b : Timeless (bij_own_elem γ a b).
+  Proof. unseal. apply _. Qed.
+
+  Global Instance bij_own_elem_persistent γ a b : Persistent (bij_own_elem γ a b).
+  Proof. unseal. apply _. Qed.
+
+  Local Lemma bij_own_subrel_to_big_sepS γ L :
+    own γ (bij_subrel L) -∗ [∗ set] ab ∈ L, own γ (bij_elem ab.1 ab.2).
+  Proof.
+    induction L as [|[a b] L] using set_ind_L.
+    - rewrite big_sepS_empty. by iIntros "_".
+    - rewrite bij_subrel_insert own_op.
+      rewrite big_sepS_insert //=.
+      rewrite IHL //.
+  Qed.
+
+  Lemma bij_own_alloc L :
+    gset_bijective L →
+    ⊢ |==> ∃ γ, bij_own_auth γ L ∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
+  Proof.
+    unseal.
+    intros Hbij.
+    iMod (own_alloc (bij_auth L ⋅ bij_subrel L)) as (γ) "[Hauth #Hsub]".
+    { apply bij_both_subrel_valid; auto. }
+    iModIntro. iExists γ.
+    rewrite own_op. iFrame "Hsub ∗".
+    iApply bij_own_subrel_to_big_sepS; auto.
+  Qed.
+
+  Lemma bij_own_alloc_empty : ⊢ |==> ∃ γ, bij_own_auth γ ∅.
+  Proof.
+    iMod (bij_own_alloc ∅) as (γ) "[Hauth _]";
+      eauto using gset_bijective_empty.
+  Qed.
+
+  Lemma bij_own_bijective γ L :
+    bij_own_auth γ L -∗ ⌜gset_bijective L⌝.
+  Proof.
+    unseal.
+    rewrite own_op.
+    iIntros "[Hauth _]".
+    iDestruct (own_valid with "Hauth") as %?%bij_auth_valid; done.
+  Qed.
+
+  Lemma bij_own_elem_of γ L a b :
+    (a, b) ∈ L →
+    bij_own_auth γ L -∗ bij_own_elem γ a b.
+  Proof.
+    unseal.
+    iIntros (Hel) "[_ Hfrag]".
+    iDestruct (bij_own_subrel_to_big_sepS with "Hfrag") as "Hels".
+    iDestruct (big_sepS_elem_of _ _ _ Hel with "Hels") as "$".
+  Qed.
+
+  Lemma bij_own_extend γ L a b :
+    (∀ y, (a, y) ∉ L) → (∀ x, (x, b) ∉ L) →
+    bij_own_auth γ L ==∗
+    bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
+  Proof.
+    unseal.
+    iIntros (Ha Hb) "[HL Hfrag]".
+    rewrite own_op.
+    iMod (own_update with "HL") as "HL".
+    { apply (bij_auth_extend a b); eauto. }
+    iModIntro.
+    iDestruct "HL" as "[$ #Hsub]".
+    iFrame "Hsub".
+    rewrite bij_subrel_insert own_op; iFrame "#∗".
+  Qed.
+
+  Lemma bij_own_extend_internal γ L a b :
+    (∀ y, bij_own_elem γ a y -∗ False) -∗
+    (∀ x, bij_own_elem γ x b -∗ False) -∗
+    bij_own_auth γ L ==∗
+    bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
+  Proof.
+    iIntros "Ha Hb HL".
+    iAssert (⌜∀ y, (a, y) ∉ L⌝)%I as %Ha.
+    { iIntros (y Hel).
+      iApply ("Ha" $! y).
+      iApply (bij_own_elem_of with "HL"); eauto. }
+    iAssert (⌜∀ x, (x, b) ∉ L⌝)%I as %Hb.
+    { iIntros (x Hel).
+      iApply ("Hb" $! x).
+      iApply (bij_own_elem_of with "HL"); eauto. }
+    iApply (bij_own_extend with "HL"); eauto.
+  Qed.
+
+  Lemma bij_own_extend' γ L a b :
+    ¬(∃ y, (a, y) ∈ L) → ¬(∃ x, (x, b) ∈ L) →
+    bij_own_auth γ L ==∗
+    bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
+  Proof.
+    intros.
+    iApply bij_own_extend; naive_solver.
+  Qed.
+
+  Lemma bij_own_elem_agree γ L a a' b b' :
+    bij_own_elem γ a b -∗ bij_own_elem γ a' b' -∗
+    ⌜a = a' ↔ b = b'⌝.
+  Proof.
+    unseal.
+    iIntros "Hel1 Hel2".
+    iDestruct (own_valid_2 with "Hel1 Hel2") as %?%bij_elem_agree.
+    auto.
+  Qed.
+End bij.
+
+Arguments bijG A B {_ _ _ _} _ : assert.
+Arguments bijΣ A B {_ _ _ _} : assert.