Module iset 

Implementation of a resource for ownership of subsets of values in a set

• GhostISetAuth<T> represents authoritative ownership of the entire set;
• GhostISubset<T> represents client ownership of some subset;
• GhostPersistentISubset<T> represents duplicable client knowledge of some persistent subset;
• GhostISingleton<T> represents client ownership of a singleton.
• GhostPersistentISingleton<T> represents duplicable client knowledge of a persistent singleton;

Updating the authoritative GhostISetAuth<T> requires a GhostISubset<T> containing the values being updated.

GhostISubset<T>s can be combined or split. Whenever a GhostISubset<T> can be used, we can instead use a GhostISingleton<T> (but not vice-versa).

GhostPersistentISubset<T>s can be combined or split. Whenever a GhostPersistentISubset<T> can be used, we can instead use a GhostPersistentISingleton<T> (but not vice-versa).

Example

fn example_use() {
    let tracked (mut auth, mut sub) = GhostISetAuth::new(set![1u8, 2u8, 3u8]);

    // Allocate some more values in the auth set, receiving a new subset.
    let tracked sub2 = auth.insert_set(set![4u8, 5u8]);
    proof { sub.combine(sub2); }

    // Allocate a single value in the auth set, receiving a points to
    let tracked pt1 = auth.insert(6u8);
    proof { sub.combine_points_to(pt1); }

    // Delete some values in the auth set, by returning corresponding subset.
    let tracked sub3 = sub.split(set![3u8, 4u8]);
    proof { auth.delete(sub3); }

    // Split the subset into a singleton and a subset
    let tracked pt1 = sub.split_singleton(1u8);
    let tracked sub4 = sub.split(set![5u8, 6u8]);

    // In general, we might need to call agree() to establish the fact that
    // a singleton/subset has the same values as the auth set.  Here, Verus
    // doesn't need agree because it can track where both the auth, singleton
    // and subset came from.
    proof { sub.agree(&auth); }
    proof { pt1.agree(&auth); }
    proof { sub4.agree(&auth); }

    assert(auth@.contains(pt1@));
    assert(sub4@ <= auth@);
    assert(sub@ <= auth@);

    // Persist and duplicate the submap
    let mut psub1 = sub.persist();
    assert(psub1.contains(2u8));
    let psub2 = psub1.duplicate();
    assert(psub2.contains(2u8));

    // Not shown in this simple example is the main use case of this resource:
    // maintaining an invariant between GhostISetAuth<T> and some exec-mode
    // shared state with a map view (e.g., HashISet<T>), which states that
    // the ISet<T> view of GhostISetAuth<T> is the same as the view of the
    // HashISet<T>, and then handing out a GhostISubset<T> to different
    // clients that might need to operate on different values in the set
}

Structs

GhostISetAuth

A resource that has the authoritative ownership on the entire set

GhostISingleton

A resource that has client ownership of a singleton

GhostISubset

A resource that has client ownership of a subset

GhostPersistentISingleton

A resource that asserts duplicable client knowledge of a persistent singleton

GhostPersistentISubset

A resource that asserts duplicable client knowledge of a persistent subset