forked from runtimeverification/verified-smart-contracts
-
Notifications
You must be signed in to change notification settings - Fork 0
/
spec-diff.patch
135 lines (125 loc) · 4.06 KB
/
spec-diff.patch
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
@@ -46,16 +46,31 @@
[approve]
k: #execute => (RETURN RET_ADDR:Int 32 ~> _)
callData: #abiCallData("approve", #address(SPENDER), #uint256(VALUE))
-localMem: .Map => ( .Map[ RET_ADDR := #asByteStackInWidth(1, 32) ] _:Map )
gas: {GASCAP} => _
+requires:
+ andBool 0 <=Int SPENDER andBool SPENDER <Int (2 ^Int 160)
+ andBool 0 <=Int VALUE andBool VALUE <Int (2 ^Int 256)
+ andBool 0 <=Int ALLOWANCE andBool ALLOWANCE <Int (2 ^Int 256)
+
+[approve-success]
+localMem: .Map => ( .Map[ RET_ADDR := #asByteStackInWidth(1, 32) ] _:Map )
log: _:List ( .List => ListItem(#abiEventLog(ACCT_ID, "Approval", #indexed(#address(CALLER_ID)), #indexed(#address(SPENDER)), #uint256(VALUE))) )
refund: _ => _
storage:
- #hashedLocation({COMPILER}, {_ALLOWANCES}, CALLER_ID SPENDER) |-> (_:Int => VALUE)
+ #hashedLocation({COMPILER}, {_ALLOWANCES}, CALLER_ID SPENDER) |-> (ALLOWANCE => VALUE)
_:Map
-requires:
- andBool 0 <=Int SPENDER andBool SPENDER <Int (2 ^Int 160)
- andBool 0 <=Int VALUE andBool VALUE <Int (2 ^Int 256)
++requires:
+ andBool ( VALUE ==Int 0 orBool ALLOWANCE ==Int 0 )
+
+[approve-failure]
+localMem: .Map => ( .Map[ RET_ADDR := #asByteStackInWidth(0, 32) ] _:Map )
+log: _
+refund: _
+storage:
+ #hashedLocation({COMPILER}, {_ALLOWANCES}, CALLER_ID SPENDER) |-> ALLOWANCE
+ _:Map
++requires:
+ andBool ( VALUE =/=Int 0 andBool ALLOWANCE =/=Int 0 )
[transfer]
callData: #abiCallData("transfer", #address(TO_ID), #uint256(VALUE))
@@ -79,6 +94,7 @@
_:Map
+requires:
andBool CALLER_ID =/=Int TO_ID
+ andBool VALUE >Int 0
andBool VALUE <=Int BAL_FROM
andBool BAL_TO +Int VALUE <Int (2 ^Int 256)
@@ -88,11 +104,13 @@
_:Map
+requires:
andBool CALLER_ID ==Int TO_ID
+ andBool VALUE >Int 0
andBool VALUE <=Int BAL_FROM
+ andBool BAL_FROM +Int VALUE <Int (2 ^Int 256)
[transfer-failure]
-k: #execute => #exception
-localMem: .Map => _:Map
+k: #execute => (RETURN RET_ADDR:Int 32 ~> _)
+localMem: .Map => ( .Map[ RET_ADDR := #asByteStackInWidth(0, 32) ] _:Map )
log: _
[transfer-failure-1]
@@ -102,7 +120,8 @@
_:Map
+requires:
andBool CALLER_ID =/=Int TO_ID
- andBool ( VALUE >Int BAL_FROM
+ andBool ( VALUE <=Int 0
+ orBool VALUE >Int BAL_FROM
orBool BAL_TO +Int VALUE >=Int (2 ^Int 256) )
[transfer-failure-2]
@@ -111,7 +130,9 @@
_:Map
+requires:
andBool CALLER_ID ==Int TO_ID
- andBool VALUE >Int BAL_FROM
+ andBool ( VALUE <=Int 0
+ orBool VALUE >Int BAL_FROM
+ orBool BAL_FROM +Int VALUE >=Int (2 ^Int 256) )
[transferFrom]
callData: #abiCallData("transferFrom", #address(FROM_ID), #address(TO_ID), #uint256(VALUE))
@@ -138,9 +159,10 @@
_:Map
+requires:
andBool FROM_ID =/=Int TO_ID
+ andBool VALUE >Int 0
andBool VALUE <=Int BAL_FROM
- andBool BAL_TO +Int VALUE <Int (2 ^Int 256)
andBool VALUE <=Int ALLOW
+ andBool BAL_TO +Int VALUE <Int (2 ^Int 256)
[transferFrom-success-2]
storage:
@@ -149,12 +171,14 @@
_:Map
+requires:
andBool FROM_ID ==Int TO_ID
+ andBool VALUE >Int 0
andBool VALUE <=Int BAL_FROM
andBool VALUE <=Int ALLOW
+ andBool BAL_FROM +Int VALUE <Int (2 ^Int 256)
[transferFrom-failure]
-k: #execute => #exception
-localMem: .Map => _:Map
+k: #execute => (RETURN RET_ADDR:Int 32 ~> _)
+localMem: .Map => ( .Map[ RET_ADDR := #asByteStackInWidth(0, 32) ] _:Map )
log: _
[transferFrom-failure-1]
@@ -165,9 +189,10 @@
_:Map
+requires:
andBool FROM_ID =/=Int TO_ID
- andBool ( VALUE >Int BAL_FROM
- orBool BAL_TO +Int VALUE >=Int (2 ^Int 256)
- orBool VALUE >Int ALLOW )
+ andBool ( VALUE <=Int 0
+ orBool VALUE >Int BAL_FROM
+ orBool VALUE >Int ALLOW
+ orBool BAL_TO +Int VALUE >=Int (2 ^Int 256) )
[transferFrom-failure-2]
storage:
@@ -176,13 +201,15 @@
_:Map
+requires:
andBool FROM_ID ==Int TO_ID
- andBool ( VALUE >Int BAL_FROM
- orBool VALUE >Int ALLOW )
+ andBool ( VALUE <=Int 0
+ orBool VALUE >Int BAL_FROM
+ orBool VALUE >Int ALLOW
+ orBool BAL_FROM +Int VALUE >=Int (2 ^Int 256) )