Struct InvCell Copy item path

fn example1() {
    // We can create a cell with an invariant: `v == 5 || v == 13`.
    // Thus only 5 or 13 can be stored in the cell.
    let cell = InvCell::<u64, spec_fn(u64) -> bool>::new(5, Ghost(|v| v == 5 || v == 13));

    let ref1 = &cell;
    let ref2 = &cell;

    let x = ref1.get();
    assert(x == 5 || x == 13);

    ref1.set(13);

    let y = ref2.get();
    assert(y == 5 || y == 13);
}

pub struct FixedParity {
    pub parity: int,
}

impl Predicate<u64> for FixedParity {
    open spec fn predicate(&self, v: u64) -> bool {
        v % 2 == self.parity
    }
}

fn example2() {
    // Create a cell that can only store even integers
    let cell_even = InvCell::<u64, FixedParity>::new(20, Ghost(FixedParity { parity: 0 }));

    // Create a cell that can only store odd integers
    let cell_odd = InvCell::<u64, FixedParity>::new(23, Ghost(FixedParity { parity: 1 }));

    let x = cell_even.get();
    assert(x % 2 == 0);

    let y = cell_odd.get();
    assert(y % 2 == 1);
}