Struct GhostMapAuthCopy item path

fn example_use() {
    let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]);

    // Allocate some more keys in the auth map, receiving a new submap.
    let tracked sub2 = auth.insert(map![4u8 => 4u64, 5u8 => 5u64]);
    proof { sub.combine(sub2); }

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

    // Split the submap into a multiple submaps.
    let tracked sub4 = sub.split(set![1u8, 5u8]);

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

    assert(sub4[1u8] == auth[1u8]);
    assert(sub4[5u8] == auth[5u8]);
    assert(sub[2u8] == auth[2u8]);

    // Update keys using ownership of submaps.
    proof { sub.update(&mut auth, map![2u8 => 22u64]); }
    proof { sub4.update(&mut auth, map![1u8 => 11u64]); }
    assert(auth[1u8] == 11u64);
    assert(auth[2u8] == 22u64);

    // Not shown in this simple example is the main use case of this resource:
    // maintaining an invariant between GhostMapAuth<K, V> and some exec-mode
    // shared state with a map view (e.g., HashMap<K, V>), which states that
    // the Map<K, V> view of GhostMapAuth<K, V> is the same as the view of the
    // HashMap<K, V>, and then handing out a GhostSubmap<K, V> to different
    // clients that might need to operate on different keys in this map.
}