forked from runtimeverification/verified-smart-contracts
-
Notifications
You must be signed in to change notification settings - Fork 0
/
collectToken-spec.ini
85 lines (81 loc) · 4.72 KB
/
collectToken-spec.ini
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
[collectToken]
k: #execute => #halt
output: _ => #asByteStackInWidth(1, 32)
statusCode: _ => EVMC_SUCCESS
memoryUsed: 0 => _
calldata: #abiCallData("collectToken", #uint256(NOW), #uint256(START))
wordStack: .WordStack => _
localMem: .Map => _
pc: 0 => _
gas: GASCAP => _
log: _
refund: _ => _
storage:
#hashedLocation({COMPILER}, {COLLECTEDTOKENS}, .IntList) |-> (COLLECTED => COLLECTED +Int VALUE)
#hashedLocation({COMPILER}, {BALANCE}, .IntList) |-> (BAL => BAL -Int VALUE)
_:Map
requires:
andBool 0 <=Int COLLECTED andBool COLLECTED <Int (2 ^Int 256)
andBool 0 <=Int BAL andBool BAL <Int (2 ^Int 256)
andBool 0 <=Int START andBool START <Int (2 ^Int 256)
andBool 0 <=Int (COLLECTED +Int BAL) andBool (COLLECTED +Int BAL) *Int 3153600 <Int (2 ^Int 256)
andBool 0 <Int (NOW -Int START) andBool (NOW -Int START) <Int (2 ^Int 256)
// canExtract >= 0
andBool #accumulatedReleasedTokens(BAL, COLLECTED, START, NOW) >Int COLLECTED +Int 3
// canExtract > balance
andBool #accumulatedReleasedTokens(BAL, COLLECTED, START, NOW) <Int (BAL +Int COLLECTED) -Int 10
// Max Gas
andBool GASCAP >=Int (293 *Int ((NOW -Int START) /Int 31536000)) +Int 43000
ensures: ensures VALUE ==Int @canExtractThisYear(COLLECTED +Int BAL, NOW, START) +Int BAL -Int @remainingTokens(COLLECTED +Int BAL, NOW, START)
attribute:
[loop]
k: #execute => #execute
output: _
statusCode: _
memoryUsed: MU
callData: _
wordStack: CANEXTRACT : CANEXTRACTTHISYEAR : TOTALREWARDTHISYEAR : INDEX : YEARCOUNT : REMAINING : TOTAL : RETURNVAL : START : NOW : RPC : FUNID : .WordStack
=> CANEXTRACT : CANEXTRACTTHISYEAR : TOTALREWARDTHISYEAR : YEARCOUNT : YEARCOUNT : #roundpower(REMAINING, 90, 100, YEARCOUNT -Int INDEX) : TOTAL : RETURNVAL : START : NOW : RPC : FUNID : .WordStack
localMem: _
pc: 498 => 545
gas: GASCAP => GASCAP -Int (293 *Int (YEARCOUNT -Int INDEX)) -Int 26
log: _
refund: _
storage: _
requires:
andBool 0 <=Int MU andBool MU <Int (2 ^Int 256)
andBool 0 <=Int INDEX andBool INDEX <=Int YEARCOUNT
andBool 0 <=Int YEARCOUNT andBool YEARCOUNT <Int (2 ^Int 256)
andBool 0 <=Int REMAINING andBool REMAINING *Int 90 <Int (2 ^Int 256)
andBool GASCAP >=Int ((293 *Int (YEARCOUNT -Int INDEX)) +Int 26)
ensures:
attribute:
[ds-math-mul]
k: #execute => #execute
output: _
statusCode: _
memoryUsed: MU
calldata: _
wordStack: Y : X : RET : WS => X : Y : RET : X *Int Y : WS
localMem: _
pc: 750 => 793
gas: GASCAP => GASCAP -Int 114
log: _
refund: _
storage: _
requires:
andBool 0 <=Int X andBool X <Int (2 ^Int 256)
andBool 0 <=Int Y andBool Y <Int (2 ^Int 256)
andBool 0 <=Int X *Int Y andBool X *Int Y <Int (2 ^Int 256)
andBool 0 <=Int MU andBool MU <Int (2 ^Int 256)
//
andBool #sizeWordStack(WS) <Int 20
//
andBool GASCAP >=Int 114 // for the current spec
ensures:
attribute: [trusted]
[pgm]
compiler: "Solidity"
collectedTokens: 0
balance : 1
code: "0x60606040526004361061006d576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680630e4aed3f1461007257806340ba126b1461009b578063787e9137146100db578063b69ef8a814610104578063b93e2cdb1461012d575b600080fd5b341561007d57600080fd5b610085610171565b6040518082815260200191505060405180910390f35b34156100a657600080fd5b6100c56004808035906020019091908035906020019091905050610176565b6040518082815260200191505060405180910390f35b34156100e657600080fd5b6100ee6101a8565b6040518082815260200191505060405180910390f35b341561010f57600080fd5b6101176101ae565b6040518082815260200191505060405180910390f35b341561013857600080fd5b61015760048080359060200190919080359060200190919050506101b4565b604051808215151515815260200191505060405180910390f35b600a81565b600081831061019d576301e1338061018e84846102bc565b81151561019757fe5b046101a0565b60005b905092915050565b60005481565b60015481565b600080600080600080600080888a1115156101ce57600080fd5b6101dc6000546001546102d5565b96508695506101eb8a8a610176565b9450600093505b848410156102215761021261020b87600a6064036102ee565b606461031c565b955083806001019450506101f2565b61023661022f87600a6102ee565b606461031c565b9250610260610256846301e133808c8e0381151561025057fe5b066102ee565b6301e1338061031c565b915085870382019050610275816000546102bc565b90506001548111156102875760015490505b610293600054826102d5565b6000819055506102a5600154826102bc565b600181905550600197505050505050505092915050565b600082828403915081111515156102cf57fe5b92915050565b600082828401915081101515156102e857fe5b92915050565b60008183029050600083148061030e575081838281151561030b57fe5b04145b151561031657fe5b92915050565b6000818381151561032957fe5b049050929150505600a165627a7a72305820d8edeeb44c8346eca139385cfaecddeb8b02fcc380c3b54473746e8103ff62e70029"