From 4e205a0ecca0629b01b3fa2fd99debb405e73645 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 9 Oct 2020 18:50:31 +0200
Subject: [PATCH] changelog entry and some more comments at the top of the file
---
CHANGELOG.md | 5 +++++
theories/algebra/lib/gmap_view.v | 18 ++++++++++++++++--
2 files changed, 21 insertions(+), 2 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index e85bdf9e8..7998e6a77 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -41,6 +41,11 @@ With this release, we dropped support for Coq 8.9.
the normal fractional camera. See `theories/algebra/dfrac.v` for further information.
* Rename `cmra_monotone_valid` into `cmra_morphism_valid` (this rename was
forgotten in !56).
+* Add `gmap_view`, a camera providing a "view of a `gmap`". The authoritative
+ element is any `gmap`; the fragment provides fractional ownership of a single
+ key, including support for persistent read-only ownership through `dfrac`.
+ See `theories/algebra/lib/gmap_view.v` for further information.
+ NOTE: The API surface for `gmap_view` is experimental and subject to change.
**Changes in `proofmode`:**
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index d22a706a6..31b6f850a 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -6,8 +6,22 @@ From iris.algebra Require Import local_updates proofmode_classes.
From iris.base_logic Require Import base_logic.
From iris Require Import options.
-(** * Authoritative CMRA over a map.
-The elements of the map are of type [dfrac * agree T]. *)
+(** * CMRA for a "view of a gmap".
+
+The authoritative element [gmap_view_auth] is any [gmap K V]. The fragments
+[gmap_view_frag] represent ownership of a single key in that map. Ownership is
+governed by a discardable fraction, which provides the possibiltiy to obtain
+persistent read-only ownership of a key.
+
+The key frame-preserving updates are [gmap_view_alloc] to allocate a new key,
+[gmap_view_update] to update a key given full ownership of the corresponding
+fragment, and [gmap_view_freeze] to make a key read-only by discarding any
+fraction of the corresponding fragment. Crucially, the latter does not require
+owning the authoritative element.
+
+NOTE: The API surface for [gmap_view] is experimental and subject to change. We
+plan to add notations for authoritative elements and fragments, and hope to
+support arbitrary maps as fragments. *)
Local Definition gmap_view_fragUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
gmapUR K (prodR dfracR (agreeR V)).
--
GitLab