Skip to content

Conversation

@bsdinis
Copy link
Collaborator

@bsdinis bsdinis commented Nov 29, 2025

Context

Currently, GhostMapAuth (resp. GhostSetAuth) only give out exclusive access to a submap. It is generally useful to have non-exclusive access to some subset of keys, by persisting the submap (i.e., after it's persisted, it can never be removed/updated). This allows for a duplicable resource asserting knowledge of a subset of values in the Map (resp. Set).

Implementation;

This PR is broken into three commits:

  1. Update the resource algebra for the map
  2. Add GhostPersistentSubmap and GhostPersistentPointsTo to vstd/tokens/map.rs.
  3. Add GhostPersistentSubset and GhostPersistentSingleton to vstd/tokens/set.rs.

I'm happy to break this PR in two (map vs. set) if it sounds useful.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@bsdinis bsdinis requested review from tjhance and zeldovich November 29, 2025 02:02
@bsdinis bsdinis force-pushed the bsdinis/zmn branch 3 times, most recently from a0192bb to 46d4c6a Compare November 29, 2025 18:53
@bsdinis bsdinis marked this pull request as draft November 29, 2025 18:56
@bsdinis bsdinis marked this pull request as ready for review November 29, 2025 19:38
@bsdinis bsdinis requested review from tjhance and zeldovich November 29, 2025 19:38
@bsdinis bsdinis merged commit 0c6e631 into main Dec 1, 2025
12 checks passed
@bsdinis bsdinis deleted the bsdinis/zmn branch December 1, 2025 17:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants