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
23
24

module 0x1::GlobalSpecRelevance {
    invariant forall a: address where exists<Nonzero>(a): global<Nonzero>(a).i > 0;

    struct Nonzero has key { i: u64, j: u64 }

    // 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 {
        Nonzero { i, j }
    }

    public fun publish(account: &signer, n: Nonzero) {
        assert!(n.i > 0, 0);
        move_to(account, n)
    }
}