1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
module 0x42::Test { struct R has drop { x: u64, s: vector<vector<S>>, } struct S has drop { y: u64 } spec S { invariant y > 0; } public fun test(_r: R) { } }