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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102

// flag: --v2
address 0x0 {
module A {
    struct S has key {
        x: u64
    }
    public fun read_at(addr: address): u64 acquires S {
        let s = borrow_global<S>(addr);
        s.x
    }
    spec read_at {
        pragma opaque = true;
        aborts_if !exists<S>(addr);
        ensures result == global<S>(addr).x;
    }

    public fun mutate_at(addr: address) acquires S {
        let s = borrow_global_mut<S>(addr);
        s.x = 2;
    }
    spec mutate_at {
        pragma opaque = true;
        ensures global<S>(addr).x == 2;
        aborts_if !exists<S>(addr);
        modifies global<S>(addr);
    }
}

module B {
    use 0x0::A;

    struct T has key {
        x: u64
    }

    public fun mutate_at_test_incorrect(addr1: address, addr2: address) acquires T {
        let x0 = A::read_at(addr2);
        let t = borrow_global_mut<T>(addr1);
        t.x = 2;
        let x1 = A::read_at(addr2);
        spec {
            assert x0 == x1;
        };
    }
    spec mutate_at_test_incorrect {
        pragma opaque = true;
        modifies global<T>(addr2);
    }

    public fun move_to_test_incorrect(account: &signer, addr2: address) {
        let x0 = A::read_at(addr2);
        move_to<T>(account, T{x: 2});
        let x1 = A::read_at(addr2);
        spec {
            assert x0 == x1;
        };
    }
    spec move_to_test_incorrect {
        pragma opaque = true;
        modifies global<T>(addr2);
    }

    public fun move_from_test_incorrect(addr1: address, addr2: address): T acquires T {
        let x0 = A::read_at(addr2);
        let v = move_from<T>(addr1);
        let x1 = A::read_at(addr2);
        spec {
            assert x0 == x1;
        };
        v
    }
    spec move_from_test_incorrect {
        pragma opaque = true;
        modifies global<T>(addr2);
    }

    public fun mutate_S_test1_incorrect(addr1: address, addr2: address) {
        let x0 = A::read_at(addr2);
        A::mutate_at(addr1);
        let x1 = A::read_at(addr2);
        spec {
            assert x0 == x1;
        };
    }
    spec mutate_S_test1_incorrect {
        requires addr1 != addr2;
        modifies global<A::S>(addr2);
    }

    public fun mutate_S_test2_incorrect(addr: address) {
        let x0 = A::read_at(addr);
        A::mutate_at(addr);
        let x1 = A::read_at(addr);
        spec {
            assert x0 == x1;
        };
    }
    spec mutate_S_test2_incorrect {
        modifies global<A::S>(addr);
    }
}
}