module 0x42::Test {
    struct R<T> has key {
        x: u64,
        s: S,
        t: T,
    }

    struct S has copy, drop, store {
        y: u64
    }

    spec R {
        invariant x > s.y;
    }

    spec S {
        invariant y > 0;
    }

    public fun test_borrow_imm<T: store>(): u64 acquires R {
        let r = borrow_global<R<T>>(@0x1);
        r.x
    }

    public fun test_borrow_mut<T: store>(): u64 acquires R {
        let r = borrow_global_mut<R<T>>(@0x1);
        r.s.y = 2;
        r.x = 3;
        r.x
    }

    public fun test_borrow_mut_local(): R<u64> {
        let d = R{x: 2, s: S{y:1}, t: 0};
        let r = &mut d;
        r.s.y = 2;
        r.x = 3;
        d
    }
}