move-stackless-bytecode 0.3.2

Move stackless bytecode
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

module 0x1::StructSpecRelevance {
    struct Nonzero { i: u64, j: u64 }

    spec Nonzero {
        invariant i > 0;
    }

    // Can't leak i because it's involved in a spec
    public fun leak_i_bad(n: &mut Nonzero): &mut u64 {
        &mut n.i
    }

    // Leaking j is ok because specs say nothing about it
    public fun leak_j_ok(n: &mut Nonzero): &mut u64 {
        &mut n.j
    }

    public fun create(i: u64, j: u64): Nonzero {
        assert!(i > 0, 0);
        Nonzero { i, j }
    }
}