//# publish
module 0x1.M {
    import 0x1.vector;

    struct R has key { v: vector<u64> }

    public publish(s: &signer) {
        let v: vector<u64>;
    label b0:
        v = vector.empty<u64>();
        vector.push_back<u64>(&mut v, 100);
        vector.push_back<u64>(&mut v, 200);
        move_to<R>(move(s), R { v: move(v) });
        return;
    }

    public borrow_and_pop(addr: address) acquires R {
    label b0:
        assert(vector.pop_back<u64>(&mut borrow_global_mut<R>(move(addr)).R::v) == 200, 1000);
        return;
    }

    public verify_effects(addr: address) acquires R {
    label b0:
        assert(vector.length<u64>(&borrow_global<R>(move(addr)).R::v) == 1, 1001);
        return;
    }
}

//# run --signers 0x1
import 0x1.M;

main(s: signer) {
label b0:
    M.publish(&s);
    return;
}


//# run --signers 0x1
import 0x1.M;
import 0x1.signer;

main(s: signer) {
label b0:
    M.borrow_and_pop(signer.address_of(&s));
    return;
}

//# run --signers 0x1
import 0x1.M;
import 0x1.signer;

main(s: signer) {
label b0:
    M.verify_effects(signer.address_of(&s));
    return;
}