-
Notifications
You must be signed in to change notification settings - Fork 134
/
spec-diff.patch
69 lines (62 loc) · 1.77 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
@@ -81,6 +81,7 @@
andBool CALLER_ID =/=Int TO_ID
andBool VALUE <=Int BAL_FROM
andBool BAL_TO +Int VALUE <Int (2 ^Int 256)
+ andBool TO_ID =/=Int 0
[transfer-success-2]
storage:
@@ -89,6 +90,7 @@
+requires:
andBool CALLER_ID ==Int TO_ID
andBool VALUE <=Int BAL_FROM
+ andBool TO_ID =/=Int 0
[transfer-failure]
k: #execute => #exception
@@ -103,7 +105,8 @@
+requires:
andBool CALLER_ID =/=Int TO_ID
andBool ( VALUE >Int BAL_FROM
- orBool BAL_TO +Int VALUE >=Int (2 ^Int 256) )
+ orBool BAL_TO +Int VALUE >=Int (2 ^Int 256)
+ orBool TO_ID ==Int 0 )
[transfer-failure-2]
storage:
@@ -111,7 +114,8 @@
_:Map
+requires:
andBool CALLER_ID ==Int TO_ID
- andBool VALUE >Int BAL_FROM
+ andBool ( VALUE >Int BAL_FROM
+ orBool TO_ID ==Int 0 )
[transferFrom]
callData: #abiCallData("transferFrom", #address(FROM_ID), #address(TO_ID), #uint256(VALUE))
@@ -141,6 +145,7 @@
andBool VALUE <=Int BAL_FROM
andBool BAL_TO +Int VALUE <Int (2 ^Int 256)
andBool VALUE <=Int ALLOW
+ andBool TO_ID =/=Int 0
[transferFrom-success-2]
storage:
@@ -151,6 +156,7 @@
andBool FROM_ID ==Int TO_ID
andBool VALUE <=Int BAL_FROM
andBool VALUE <=Int ALLOW
+ andBool TO_ID =/=Int 0
[transferFrom-failure]
k: #execute => #exception
@@ -167,7 +173,8 @@
andBool FROM_ID =/=Int TO_ID
andBool ( VALUE >Int BAL_FROM
orBool BAL_TO +Int VALUE >=Int (2 ^Int 256)
- orBool VALUE >Int ALLOW )
+ orBool VALUE >Int ALLOW
+ orBool TO_ID ==Int 0 )
[transferFrom-failure-2]
storage:
@@ -177,12 +184,13 @@
+requires:
andBool FROM_ID ==Int TO_ID
andBool ( VALUE >Int BAL_FROM
- orBool VALUE >Int ALLOW )
+ orBool VALUE >Int ALLOW
+ orBool TO_ID ==Int 0 )