Add persistent (duplicable) variants of GhostSubmap/GhostSubset (#2019)

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).

* ghost_map: extend resource algebra to allow for duplicable maps

* ghost_map: add persistent, duplicable variants of `GhostSubmap` and `GhostPointsTo`

* ghost_set: add persistent, duplicable variants of `GhostSubset` and `GhostSingleton`

Author: bsdinis