From 28c2e8e3dc6767a91447a317a8f702d60373c37a Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 27 Oct 2020 15:47:09 +0100
Subject: [PATCH] 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 | 5 ++
_CoqProject | 2 +
theories/algebra/lib/mnat_auth.v | 76 +++++++++++++++++++
theories/base_logic/lib/mnat.v | 123 +++++++++++++++++++++++++++++++
theories/bi/lib/fractional.v | 8 ++
5 files changed, 214 insertions(+)
create mode 100644 theories/algebra/lib/mnat_auth.v
create mode 100644 theories/base_logic/lib/mnat.v
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 59ed387ae..1e91b7250 100644
--- a/CHANGELOG.md
+++ b/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`:**
diff --git a/_CoqProject b/_CoqProject
index a8bfee56a..d61142069 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/algebra/lib/mnat_auth.v b/theories/algebra/lib/mnat_auth.v
new file mode 100644
index 000000000..eb72b677e
--- /dev/null
+++ b/theories/algebra/lib/mnat_auth.v
@@ -0,0 +1,76 @@
+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.
diff --git a/theories/base_logic/lib/mnat.v b/theories/base_logic/lib/mnat.v
new file mode 100644
index 000000000..866200227
--- /dev/null
+++ b/theories/base_logic/lib/mnat.v
@@ -0,0 +1,123 @@
+(** 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.
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index f5e18141b..bfbd80e3d 100644
--- a/theories/bi/lib/fractional.v
+++ b/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.
--
GitLab