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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

============ initial translation from Move ================

[variant baseline]
fun InvRelevance::inner<#0>($t0|s: &signer, $t1|t: #0) {
     var $t2: &signer
     var $t3: #0
     var $t4: InvRelevance::R<#0>
  0: $t2 := move($t0)
  1: $t3 := move($t1)
  2: $t4 := pack InvRelevance::R<#0>($t3)
  3: move_to<InvRelevance::R<#0>>($t4, $t2)
  4: return ()
}


[variant baseline]
public fun InvRelevance::outer_T<#0>($t0|s: &signer, $t1|t: #0) {
     var $t2: &signer
     var $t3: #0
  0: $t2 := move($t0)
  1: $t3 := move($t1)
  2: InvRelevance::inner<#0>($t2, $t3)
  3: return ()
}


[variant baseline]
public fun InvRelevance::outer_bool($t0|s: &signer, $t1|t: bool) {
     var $t2: &signer
     var $t3: bool
  0: $t2 := move($t0)
  1: $t3 := move($t1)
  2: InvRelevance::inner<bool>($t2, $t3)
  3: return ()
}


[variant baseline]
public fun InvRelevance::outer_u64($t0|s: &signer, $t1|t: u64) {
     var $t2: &signer
     var $t3: u64
  0: $t2 := move($t0)
  1: $t3 := move($t1)
  2: InvRelevance::inner<u64>($t2, $t3)
  3: return ()
}

============ after pipeline `verification_analysis` ================

[variant baseline]
fun InvRelevance::inner<#0>($t0|s: signer, $t1|t: #0) {
     var $t2: InvRelevance::R<#0>
  0: $t2 := pack InvRelevance::R<#0>($t1)
  1: move_to<InvRelevance::R<#0>>($t2, $t0)
  2: return ()
}


[variant baseline]
public fun InvRelevance::outer_T<#0>($t0|s: signer, $t1|t: #0) {
  0: InvRelevance::inner<#0>($t0, $t1)
  1: return ()
}


[variant baseline]
public fun InvRelevance::outer_bool($t0|s: signer, $t1|t: bool) {
  0: InvRelevance::inner<bool>($t0, $t1)
  1: return ()
}


[variant baseline]
public fun InvRelevance::outer_u64($t0|s: signer, $t1|t: u64) {
  0: InvRelevance::inner<u64>($t0, $t1)
  1: return ()
}


********* Result of verification analysis *********

functions that defer invariant checking at return: [
]

functions that delegate invariants to its callers: [
  InvRelevance::inner
]

invariant applicability: [
  InvRelevance::inner: {
    accessed: [@0*]
    modified: [@0*]
    directly accessed: [@0*]
    directly modified: [@0*]
  }
  InvRelevance::outer_T: {
    accessed: [@0*, @1*]
    modified: [@0*, @1*]
    directly accessed: [@1*]
    directly modified: [@1*]
  }
  InvRelevance::outer_bool: {
    accessed: [@0*]
    modified: [@0*]
    directly accessed: []
    directly modified: []
  }
  InvRelevance::outer_u64: {
    accessed: [@1*]
    modified: [@1*]
    directly accessed: [@1*]
    directly modified: [@1*]
  }
]

verification analysis: [
  InvRelevance::inner: verified + inlined
  InvRelevance::outer_T: verified
  InvRelevance::outer_bool: verified
  InvRelevance::outer_u64: verified
]