// dep: ../../move-stdlib/sources/vector.move

module 0x1::VecEq {
    use std::vector;

    struct G { v: vector<u64> }

    spec G {
        invariant v == vec<u64>(10);
    }

    public fun new(): G {
        G { v: vector::singleton(10) }
    }

    // should complain
    public fun leak_v(g: &mut G): &mut vector<u64> {
        &mut g.v
    }

    // should also complain
    public fun leak_index_into_v(g: &mut G): &mut u64 {
        vector::borrow_mut(&mut g.v, 0)
    }
}