forked from runtimeverification/verified-smart-contracts
-
Notifications
You must be signed in to change notification settings - Fork 0
/
forwardToHotWallet-spec.ini
89 lines (82 loc) · 12.2 KB
/
forwardToHotWallet-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
86
87
88
89
[forwardToHotWallet]
memoryUsed: 0 => _
callData: #abiCallData("forwardToHotWallet", #uint256(AMOUNT))
wordStack: .WordStack => _
pc: 0 => _
gas: {GASCAP} => _
log: _
refund: _
requires:
andBool 0 <=Int AMOUNT andBool AMOUNT <Int (2 ^Int 256)
andBool 0 <=Int WITHDRAWER andBool WITHDRAWER <Int (2 ^Int 160)
andBool 0 <=Int WITHDRAWLIMIT andBool WITHDRAWLIMIT <Int (2 ^Int 256)
andBool 0 <=Int LASTWITHDRAWTIME andBool LASTWITHDRAWTIME <Int (2 ^Int 256)
andBool 0 <=Int PAUSED andBool PAUSED <Int (2 ^Int 256)
ensures:
attribute:
[forwardToHotWallet-success]
k: #execute => #halt
statusCode: _ => EVMC_SUCCESS
output: _ => #asByteStackInWidth(RET_VAL, 32)
localMem: .Map => _
storage:
#hashedLocation({COMPILER}, {_WITHDRAWER}, .IntList) |-> WITHDRAWER
#hashedLocation({COMPILER}, {_WITHDRAWLIMIT}, .IntList) |-> WITHDRAWLIMIT
#hashedLocation({COMPILER}, {_LASTWITHDRAWTIME}, .IntList) |-> ( LASTWITHDRAWTIME => NOW )
#hashedLocation({COMPILER}, {_PAUSED}, .IntList) |-> PAUSED
_:Map
+requires:
andBool PAUSED ==Int 0 // notPaused
andBool CALLER_ID ==Int WITHDRAWER // onlyWithdrawer
andBool AMOUNT >Int 0 // require(_amount > 0);
andBool NOW >Int LASTWITHDRAWTIME +Word (24 *Int 3600) // require(_time > (lastWithdrawTime + 24 hours));
// NOTE: +Word instead of +Int
[forwardToHotWallet-success-1]
+requires:
andBool AMOUNT <=Int WITHDRAWLIMIT // if (amount > withdrawLimit) { ... }
ensures RET_VAL ==Int AMOUNT
[forwardToHotWallet-success-2]
+requires:
andBool AMOUNT >Int WITHDRAWLIMIT // if (amount > withdrawLimit) { ... }
ensures RET_VAL ==Int WITHDRAWLIMIT
[forwardToHotWallet-failure]
k: #execute => #halt
output: _ => _
statusCode: _ => EVMC_REVERT
localMem: .Map => _
storage:
#hashedLocation({COMPILER}, {_WITHDRAWER}, .IntList) |-> WITHDRAWER
#hashedLocation({COMPILER}, {_WITHDRAWLIMIT}, .IntList) |-> WITHDRAWLIMIT
#hashedLocation({COMPILER}, {_LASTWITHDRAWTIME}, .IntList) |-> LASTWITHDRAWTIME
#hashedLocation({COMPILER}, {_PAUSED}, .IntList) |-> PAUSED
_:Map
; TODO: have a single spec with orBool
;+requires:
; andBool (
; PAUSED ==Int 1 <<Int (20 *Int 8) // notPaused // NOTE: `paused` packed with `owner`
; orBool CALLER_ID =/=Int WITHDRAWER // onlyWithdrawer
; orBool AMOUNT <=Int 0 // require(_amount > 0);
; orBool NOW <=Int LASTWITHDRAWTIME +Word (24 *Int 3600) // require(_time > (lastWithdrawTime + 24 hours));
; )
[forwardToHotWallet-failure-1]
+requires:
andBool PAUSED ==Int 1 <<Int (20 *Int 8) // notPaused
[forwardToHotWallet-failure-2]
+requires:
andBool CALLER_ID =/=Int WITHDRAWER // onlyWithdrawer
[forwardToHotWallet-failure-3]
+requires:
andBool AMOUNT <=Int 0 // require(_amount > 0);
[forwardToHotWallet-failure-4]
+requires:
andBool NOW <=Int LASTWITHDRAWTIME +Word (24 *Int 3600) // require(_time > (lastWithdrawTime + 24 hours));
[pgm]
compiler: "Solidity"
_withdrawer : 3
_withdrawLimit : 4
_lastWithdrawTime : 5
_paused : 6
code: "0x6060604052600436106100f0576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806257e8d4146100f55780630d174c241461012c57806313af40351461016557806316ada5471461019e57806329113bc8146101c75780633943380c1461021c5780634abdf2e0146102715780634af350eb146102945780635c975abb146102f55780636be13c92146103225780638da5cb5b146103775780639550276b146103cc578063ab231511146103e1578063bde27f4a1461040a578063cdc1842414610441578063d87522ae14610496578063f848d541146104ab575b600080fd5b341561010057600080fd5b61011660048080359060200190919050506104d4565b6040518082815260200191505060405180910390f35b341561013757600080fd5b610163600480803573ffffffffffffffffffffffffffffffffffffffff16906020019091905050610549565b005b341561017057600080fd5b61019c600480803573ffffffffffffffffffffffffffffffffffffffff16906020019091905050610668565b005b34156101a957600080fd5b6101b161074b565b6040518082815260200191505060405180910390f35b34156101d257600080fd5b6101da610753565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561022757600080fd5b61022f610779565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561027c57600080fd5b610292600480803590602001909190505061079e565b005b341561029f57600080fd5b6102f3600480803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803590602001909190803573ffffffffffffffffffffffffffffffffffffffff16906020019091905050610861565b005b341561030057600080fd5b6103086109f5565b604051808215151515815260200191505060405180910390f35b341561032d57600080fd5b610335610a08565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561038257600080fd5b61038a610a2e565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b34156103d757600080fd5b6103df610a54565b005b34156103ec57600080fd5b6103f4610acd565b6040518082815260200191505060405180910390f35b341561041557600080fd5b61042b6004808035906020019091905050610ad3565b6040518082815260200191505060405180910390f35b341561044c57600080fd5b610454610ba2565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b34156104a157600080fd5b6104a9610bc8565b005b34156104b657600080fd5b6104be610c41565b6040518082815260200191505060405180910390f35b6000600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff1614151561053257600080fd5b60008211151561054157600080fd5b819050919050565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff161415156105a557600080fd5b600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff16141515156105e157600080fd5b80600360006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff1602179055508073ffffffffffffffffffffffffffffffffffffffff167f91ea294e4187e15075dc6da5e9abb3161ca1a608c538e1a1c6528fc644b1b6f560405160405180910390a250565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff161415156106c457600080fd5b80600660006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff1602179055508073ffffffffffffffffffffffffffffffffffffffff167fce241d7ca1f669fee44b6fc00b8eba2df3bb514eed0f6f668f8f89096e81ed9460405160405180910390a250565b600042905090565b600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff161415156107fa57600080fd5b60008111151561080957600080fd5b806004819055503373ffffffffffffffffffffffffffffffffffffffff167fd9f754a3457d492d875ed93adbb513556202c51d9d6e0f9de8d9d4e7cf232008826040518082815260200191505060405180910390a250565b6000600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff161415156108bf57600080fd5b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff161415151561091b57600080fd5b60008311156109ef578190508073ffffffffffffffffffffffffffffffffffffffff1663a9059cbb85856000604051602001526040518363ffffffff167c0100000000000000000000000000000000000000000000000000000000028152600401808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200182815260200192505050602060405180830381600087803b15156109d257600080fd5b6102c65a03f115156109e357600080fd5b50505060405180519050505b50505050565b600660149054906101000a900460ff1681565b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff16141515610ab057600080fd5b6001600660146101000a81548160ff021916908315150217905550565b60055481565b6000806000600660149054906101000a900460ff16151515610af457600080fd5b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff16141515610b5057600080fd5b600084111515610b5f57600080fd5b610b6761074b565b9150620151806005540182111515610b7e57600080fd5b839050600454811115610b915760045490505b816005819055508092505050919050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff16141515610c2457600080fd5b6000600660146101000a81548160ff021916908315150217905550565b600454815600a165627a7a72305820f1e3e5a9cf1054e7c34a3f0f60ea3dc352ed9f0cd000953a1113bacc56ddb77e0029"
; simpler
; code: "0x6060604052600436106100a4576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806316ada547146100a957806329113bc8146100d25780633943380c146101275780635c975abb1461017c5780636be13c92146101a95780638da5cb5b146101fe578063ab23151114610253578063bde27f4a1461027c578063cdc18424146102b3578063f848d54114610308575b600080fd5b34156100b457600080fd5b6100bc610331565b6040518082815260200191505060405180910390f35b34156100dd57600080fd5b6100e5610339565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561013257600080fd5b61013a61035f565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561018757600080fd5b61018f610384565b604051808215151515815260200191505060405180910390f35b34156101b457600080fd5b6101bc610397565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561020957600080fd5b6102116103bd565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561025e57600080fd5b6102666103e3565b6040518082815260200191505060405180910390f35b341561028757600080fd5b61029d60048080359060200190919050506103e9565b6040518082815260200191505060405180910390f35b34156102be57600080fd5b6102c66104b8565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561031357600080fd5b61031b6104de565b6040518082815260200191505060405180910390f35b600042905090565b600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b600660149054906101000a900460ff1681565b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60055481565b6000806000600660149054906101000a900460ff1615151561040a57600080fd5b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff1614151561046657600080fd5b60008411151561047557600080fd5b61047d610331565b915062015180600554018211151561049457600080fd5b8390506004548111156104a75760045490505b816005819055508092505050919050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b600454815600a165627a7a723058205ef4dd4b46242121ef284c2e4e845500e9d0eb84ebd7c272212a1f3a94e295fc0029"
gasCap: 22000