Struct GhostSeqAuthCopy item path

fn example_use() {
    let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0);

    // Split the subsequence into a multiple subseqs.
    let tracked sub2 = sub.split(3);

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

    assert(sub[0] == auth[0]);
    assert(sub2[0] == auth[3]);

    // Update the sequence using ownership of subseqs.
    // The update() method on GhostSubseq updates the entire subrange.
    proof { sub.update(&mut auth, seq![10u64, 11u64, 12u64]); }
    assert(auth[0] == 10u64);
    assert(sub[0] == 10u64);

    // The update_subrange_with() method on GhostSeqAuth allows updating
    // arbitrary parts of a subseq's subrange.
    proof { auth.update_subrange_with(&mut sub2, 4, seq![24u64, 25u64]); }
    assert(auth[3] == 3u64);
    assert(auth[4] == 24u64);
    assert(sub2[1] == 24u64);

    // Not shown in this simple example is the main use case of this resource:
    // maintaining an invariant between GhostSeqAuth<V> and some exec-mode
    // shared state with a seq view (e.g., the contents of a file or a disk),
    // which states that the Seq<V> view of GhostSeqAuth<V> is the same as the
    // view of the state (e.g., file or disk contents), and then handing out a
    // GhostSubseq<V> to different clients that might need to operate on
    // different subranges of the shared state (e.g., different concurrent
    // transactions that operate on different parts of the file/disk).
}