Add mnat library for monotonic nat ghost state

Implemented as an algebra for rules about `auth max_natUR` and a
logic-level wrapper for the auth element (a nat) and fragment (a
persistent lower-bound).

Fixes #327.

CHANGELOG.md

@@ -51,6 +51,8 @@ With this release, we dropped support for Coq 8.9.
   available everywhere without further changes.
 * The authoritative fragment `✓ (◯ b : auth A)` is no longer definitionally
   equal to `✓ b`.
+* Add `mnat_auth`, a wrapper for `auth max_nat`. The result is an authoritative
+  `nat` where a fragment is a lower bound whose ownership is persistent.
 
 **Changes in `proofmode`:**
 
@@ -105,6 +107,9 @@ With this release, we dropped support for Coq 8.9.
   `uPred.discrete_fun_validI` to the new `base_logic.algebra` module. That
   module is exported by `base_logic.base_logic` so these names are now usually
   available everywhere, and no longer inside the `uPred` module.
+* Add an `mnat` library on top of `mnat_auth` that supports ghost state which is
+  an authoritative, monotonically-increasing `nat` with a proposition giving a
+  persistent lower bound. See `base_logic.lib.mnat` for further details.
 
 **Changes in `program_logic`:**
 

_CoqProject

@@ -40,6 +40,7 @@ theories/algebra/lib/frac_auth.v
 theories/algebra/lib/ufrac_auth.v
 theories/algebra/lib/frac_agree.v
 theories/algebra/lib/gmap_view.v
+theories/algebra/lib/mnat_auth.v
 theories/si_logic/siprop.v
 theories/si_logic/bi.v
 theories/bi/notation.v
@@ -89,6 +90,7 @@ 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/base_logic/lib/ghost_var.v
+theories/base_logic/lib/mnat.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v

theories/algebra/lib/mnat_auth.v

+From iris.algebra Require Export auth.
+From iris.algebra Require Import numbers updates.
+From iris Require Import options.
+
+(** Authoritative CMRA for [max_nat]. The authoritative element is a
+monotonically increasing [nat], while a fragment is a lower bound. *)
+
+Definition mnat_auth   := auth max_natUR.
+Definition mnat_authR  := authR max_natUR.
+Definition mnat_authUR := authUR max_natUR.
+
+Section mnat_auth.
+  Implicit Types (n : nat).
+
+  Definition mnat_auth_auth (q : Qp) (n : nat) : mnat_auth := ●{q} MaxNat n.
+  Definition mnat_auth_frag          (n : nat) : mnat_auth := ◯ MaxNat n.
+
+  Global Instance mnat_auth_frag_core_id n : CoreId (mnat_auth_frag n).
+  Proof. apply _. Qed.
+
+  Lemma mnat_auth_auth_frac_op q1 q2 n :
+    mnat_auth_auth q1 n ⋅ mnat_auth_auth q2 n ≡ mnat_auth_auth (q1 + q2) n.
+  Proof. rewrite /mnat_auth_auth auth_auth_frac_op //. Qed.
+
+  Lemma mnat_auth_auth_op_valid n1 n2 :
+    ✓ (mnat_auth_auth 1 n1 ⋅ mnat_auth_auth 1 n2) ↔ False.
+  Proof. rewrite auth_auth_op_valid //. Qed.
+
+  Lemma mnat_auth_frac_op_valid q1 q2 n1 n2 :
+    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ ✓ (q1 + q2)%Qp ∧ n1 = n2.
+  Proof. rewrite auth_auth_frac_op_valid. naive_solver. Qed.
+
+  Lemma mnat_auth_frag_op n1 n2 :
+    mnat_auth_frag n1 ⋅ mnat_auth_frag n2 = mnat_auth_frag (n1 `max` n2).
+  Proof. rewrite -auth_frag_op max_nat_op_max //. Qed.
+
+  (** rephrasing of [mnat_auth_frag_op] useful for weakening a fragment to a
+  smaller lower-bound *)
+  Lemma mnat_auth_frag_op_le_l n n' :
+    n' ≤ n →
+    mnat_auth_frag n = mnat_auth_frag n' ⋅ mnat_auth_frag n.
+  Proof.
+    intros Hle.
+    rewrite mnat_auth_frag_op.
+    rewrite Nat.max_r //.
+  Qed.
+
+  Lemma mnat_auth_both_frac_valid q n m :
+    ✓ (mnat_auth_auth q n ⋅ mnat_auth_frag m) ↔ ✓ q ∧ m ≤ n.
+  Proof.
+    rewrite auth_both_frac_valid_discrete.
+    rewrite max_nat_included /=.
+    naive_solver.
+  Qed.
+
+  Lemma mnat_auth_both_valid n m :
+    ✓ (mnat_auth_auth 1 n ⋅ mnat_auth_frag m) ↔ m ≤ n.
+  Proof. rewrite mnat_auth_both_frac_valid frac_valid'. naive_solver. Qed.
+
+  Lemma mnat_auth_auth_valid n : ✓ mnat_auth_auth 1 n.
+  Proof. apply auth_auth_valid; done. Qed.
+
+  Lemma mnat_auth_update n n' :
+    n ≤ n' →
+    mnat_auth_auth 1 n ~~> mnat_auth_auth 1 n' ⋅ mnat_auth_frag n'.
+  Proof.
+    intros Hle.
+    apply auth_update_alloc, max_nat_local_update; done.
+  Qed.
+
+  Lemma mnat_auth_alloc_frag q n :
+    mnat_auth_auth q n ~~> mnat_auth_auth q n ⋅ mnat_auth_frag n.
+  Proof. by apply (auth_update_frac_alloc _ _ _). Qed.
+End mnat_auth.
+
+Typeclasses Opaque mnat_auth_auth mnat_auth_frag.

theories/base_logic/lib/mnat.v

+(** Ghost state for a monotonically increasing nat, wrapping the [mnat_authR]
+RA. Provides an authoritative proposition [mnat_own_auth γ q n] for the
+underlying number [n] and a persistent proposition [mnat_own_lb γ m] witnessing that
+the authoritative nat is at least m.
+
+The key rules are [mnat_own_lb_valid], which asserts that an auth at [n] and a
+lower-bound at [m] imply that [m ≤ n], and [mnat_update], which allows to
+increase the auth element. At any time the auth nat can be "snapshotted" with
+[mnat_get_lb] to produce a persistent lower-bound proposition. *)
+
+From iris.proofmode Require Import tactics.
+From iris.algebra.lib Require Import mnat_auth.
+From iris.bi.lib Require Import fractional.
+From iris.base_logic.lib Require Export own.
+From iris Require Import options.
+
+Class mnatG Σ :=
+  MnatG { mnatG_inG :> inG Σ mnat_authR; }.
+Definition mnatΣ : gFunctors := #[ GFunctor mnat_authR ].
+Instance subG_mnatΣ Σ : subG mnatΣ Σ → mnatG Σ.
+Proof. solve_inG. Qed.
+
+(** [mnat_own_auth] is the authoritative nat. The definition includes the
+fragment at the same value so that [mnat_get_lb] does not require an
+update modality. *)
+Definition mnat_own_auth `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
+  own γ (mnat_auth_auth q n ⋅ mnat_auth_frag n).
+Definition mnat_own_lb `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
+  own γ (mnat_auth_frag n).
+
+Section mnat.
+  Context `{!mnatG Σ}.
+  Implicit Types (n m : nat).
+
+  Global Instance mnat_own_auth_timeless γ q n : Timeless (mnat_own_auth γ q n).
+  Proof. apply _. Qed.
+  Global Instance mnat_own_lb_timeless γ n : Timeless (mnat_own_lb γ n).
+  Proof. apply _. Qed.
+  Global Instance mnat_own_lb_persistent γ n : Persistent (mnat_own_lb γ n).
+  Proof. apply _. Qed.
+
+  Global Instance mnat_own_auth_fractional γ n : Fractional (λ q, mnat_own_auth γ q n).
+  Proof.
+    rewrite /mnat_own_auth. setoid_rewrite own_op.
+    apply fractional_sep; [|apply _].
+    intros p q. rewrite -own_op mnat_auth_auth_frac_op //.
+  Qed.
+
+  Global Instance mnat_own_auth_as_fractional γ q n :
+    AsFractional (mnat_own_auth γ q n) (λ q, mnat_own_auth γ q n) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma mnat_own_auth_agree γ q1 q2 n1 n2 :
+    mnat_own_auth γ q1 n1 -∗ mnat_own_auth γ q2 n2 -∗ ⌜✓ (q1 + q2)%Qp ∧ n1 = n2⌝.
+  Proof.
+    iIntros "[H1 _] [H2 _]".
+    iDestruct (own_valid_2 with "H1 H2") as %?%mnat_auth_frac_op_valid; done.
+  Qed.
+
+  Lemma mnat_own_auth_exclusive γ n1 n2 :
+    mnat_own_auth γ 1 n1 -∗ mnat_own_auth γ 1 n2 -∗ False.
+  Proof.
+    iIntros "[H1 _] [H2 _]".
+    iDestruct (own_valid_2 with "H1 H2") as %[]%mnat_auth_auth_op_valid.
+  Qed.
+
+  (** The conclusion of this lemma is persistent; the proofmode will preserve the
+  [mnat_own_auth] in the premise as long as the conclusion is introduced to the
+  persistent context, for example with [iDestruct (mnat_get_lb with
+  "Hauth") as "#Hfrag"]. *)
+  Lemma mnat_get_lb γ q n :
+    mnat_own_auth γ q n -∗ mnat_own_lb γ n.
+  Proof. iIntros "[_ $]". Qed.
+
+  Lemma mnat_alloc n :
+    ⊢ |==> ∃ γ, mnat_own_auth γ 1 n ∗ mnat_own_lb γ n.
+  Proof.
+    iMod (own_alloc (mnat_auth_auth 1 n ⋅ mnat_auth_frag n)) as (γ) "Hauth".
+    { apply mnat_auth_both_valid; auto. }
+    iModIntro. iExists γ.
+    iDestruct (mnat_get_lb with "Hauth") as "#Hlb".
+    auto.
+  Qed.
+
+  Lemma mnat_own_lb_valid γ q n m :
+    mnat_own_auth γ q n -∗ mnat_own_lb γ m -∗ ⌜✓ q ∧ m ≤ n⌝.
+  Proof.
+    iIntros "[Hauth _] Hlb".
+    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mnat_auth_both_frac_valid.
+    auto.
+  Qed.
+
+  Lemma mnat_own_lb_le γ n n' :
+    n' ≤ n →
+    mnat_own_lb γ n -∗ mnat_own_lb γ n'.
+  Proof.
+    intros Hle.
+    rewrite /mnat_own_lb.
+    rewrite (mnat_auth_frag_op_le_l n n') //.
+    iIntros "[$ _]".
+  Qed.
+
+  Lemma mnat_update n' γ n :
+    n ≤ n' →
+    mnat_own_auth γ 1 n ==∗ mnat_own_auth γ 1 n'.
+  Proof.
+    iIntros (Hlb) "[Hauth _]".
+    iMod (own_update with "Hauth") as "$"; [|done].
+    apply mnat_auth_update; auto.
+  Qed.
+
+  Lemma mnat_update_with_lb γ n n' :
+    n ≤ n' →
+    mnat_own_auth γ 1 n ==∗ mnat_own_auth γ 1 n' ∗ mnat_own_lb γ n'.
+  Proof.
+    iIntros (Hlb) "Hauth".
+    iMod (mnat_update n' with "Hauth") as "Hauth"; auto.
+    iDestruct (mnat_get_lb with "Hauth") as "#Hlb".
+    auto.
+  Qed.
+End mnat.
+
+Typeclasses Opaque mnat_own_auth mnat_own_lb.

theories/bi/lib/fractional.v

@@ -25,6 +25,14 @@ Section fractional.
   Implicit Types Φ : Qp → PROP.
   Implicit Types q : Qp.
 
+  Global Instance Fractional_proper :
+    Proper (pointwise_relation _ (≡) ==> iff) (@Fractional PROP).
+  Proof.
+    rewrite /Fractional.
+    intros Φ1 Φ2 Hequiv.
+    by setoid_rewrite Hequiv.
+  Qed.
+
   Lemma fractional_split P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
     P ⊣⊢ P1 ∗ P2.