diff --git a/CHANGELOG.md b/CHANGELOG.md index e85bdf9e8cada096d74c4193c852c7c10c79c78b..7998e6a776a379fa66f8e083dcf624eaf67b1ece 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 d22a706a644d2df3b2bef02844d82ac9024c7b9a..31b6f850a90f002e6121f16b9daf513cba4cfd9d 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)).