-
Notifications
You must be signed in to change notification settings - Fork 25
/
Copy pathproof-Vat_tune_succ.k
129 lines (125 loc) · 16.1 KB
/
proof-Vat_tune_succ.k
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
requires "../rules.k"
module PROOF-VAT_TUNE_SUCC
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
// Vat_tune
rule
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> BYZANTIUM </schedule>
<analysis> .Map </analysis>
<ethereum>
<evm>
<output> .WordStack </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<callStack> VCallStack </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
<callState>
<program> #asMapOpCodes(#dasmOpCodes(#parseByteStack("0x608060405234801561001057600080fd5b507c01000000000000000000000000000000000000000000000000000000006000350463bf353dbb8114156100575761004c600435600061067e565b805460405260206040f35b6365fae35e8114156100885761006b610667565b1561007557600080fd5b610082600435600061067e565b60018155005b639c52a7f18114156100b95761009c610667565b156100a657600080fd5b6100b3600435600061067e565b60008155005b63d9638d368114156100f5576100d2600435600161067e565b805460405260018101546060526002810154608052600381015460a05260806040f35b6326e27482811415610123576101116024356004356002610695565b80546040526001810154606052604080f35b63c091268381141561014a5761013f6024356004356003610695565b805460405260206040f35b63f53e4e6981141561016e57610163600435600461067e565b805460405260206040f35b63a60f1d3e81141561019257610187600435600561067e565b805460405260206040f35b630dca59c18114156101aa5760065460405260206040f35b632d61a3558114156101c25760075460405260206040f35b633b663195811415610233576101d6610667565b156101e057600080fd5b6101ed600435600161067e565b600081541415156101fd57600080fd5b6000600182015414151561021057600080fd5b6b033b2e3c9fd0803ce800000081556b033b2e3c9fd0803ce80000006001820155005b6378f1947081141561028b57610247610667565b1561025157600080fd5b61025e600435600461067e565b61026b60443582546106f6565b815561027a602435600461067e565b61028760443582546106b9565b8155005b6342066cbb8114156102ca5761029f610667565b156102a957600080fd5b6102b96024356004356003610695565b6102c660443582546106b9565b8155005b63a6e41821811415610328576102de610667565b156102e857600080fd5b6102f86024356004356003610695565b61030560643582546106f6565b81556103176044356004356003610695565b61032460643582546106b9565b8155005b635dd6471a8114156104165761033c610667565b1561034657600080fd5b6103566024356004356002610695565b61036360843582546106b9565b815561037560a43560018301546106b9565b6001820155610387600435600161067e565b61039760843560028301546106b9565b60028201556103ac60a43560038301546106b9565b60038201556103be6084358254610733565b6103ce6044356004356003610695565b6103d98282546106f6565b81556103eb60a4356001850154610733565b6103f8606435600461067e565b6104038282546106b9565b8155610411826006546106b9565b600655005b633690ae4c8114156105045761042a610667565b1561043457600080fd5b6104446024356004356002610695565b61045160843582546106b9565b815561046360a43560018301546106b9565b6001820155610475600435600161067e565b61048560843560028301546106b9565b600282015561049a60a43560038301546106b9565b60038201556104ac6084358254610733565b6104bc6044356004356003610695565b6104c78282546106f6565b81556104d960a4356001850154610733565b6104e6606435600561067e565b6104f18282546106f6565b81556104ff826007546106f6565b600755005b63990a5f6381141561057e57610518610667565b1561052257600080fd5b61052f600435600561067e565b61053c60443582546106f6565b815561054b602435600461067e565b61055860443582546106f6565b81556105686044356007546106f6565b6007556105796044356006546106f6565b600655005b63e6a6a64d8114156105f957610592610667565b1561059c57600080fd5b6105a9600435600161067e565b6105b960443560018301546106b9565b60018201556105ce6044356003830154610733565b6105db602435600461067e565b6105e68282546106b9565b81556105f4826006546106b9565b600655005b6309b7a0b58114156106625761060d610667565b1561061757600080fd5b610624600435600161067e565b61063160443582546106b9565b81556106436044356002830154610733565b6106536024356004356003610695565b61065e8282546106f6565b8155005b600080fd5b600061067433600061067e565b5460011415905090565b600082600052816020526040600020905092915050565b60008360005282602052816040526040602020602052604060002090509392505050565b6000828201905060008313156106d85781811115156106d757600080fd5b5b60008312156106f05781811015156106ef57600080fd5b5b92915050565b60008282039050600083121561071557818111151561071457600080fd5b5b600083131561072d57818110151561072c57600080fd5b5b92915050565b60008282029050600082121561074857600080fd5b600083141515610763578183820514151561076257600080fd5b5b929150505600a165627a7a723058201fcd622e26e92262e34259d46a2cb321a6b6f16f239ee5bf5a42f6e2b76c16ac0029"), BYZANTIUM)) </program>
<programBytes> #parseByteStack("0x608060405234801561001057600080fd5b507c01000000000000000000000000000000000000000000000000000000006000350463bf353dbb8114156100575761004c600435600061067e565b805460405260206040f35b6365fae35e8114156100885761006b610667565b1561007557600080fd5b610082600435600061067e565b60018155005b639c52a7f18114156100b95761009c610667565b156100a657600080fd5b6100b3600435600061067e565b60008155005b63d9638d368114156100f5576100d2600435600161067e565b805460405260018101546060526002810154608052600381015460a05260806040f35b6326e27482811415610123576101116024356004356002610695565b80546040526001810154606052604080f35b63c091268381141561014a5761013f6024356004356003610695565b805460405260206040f35b63f53e4e6981141561016e57610163600435600461067e565b805460405260206040f35b63a60f1d3e81141561019257610187600435600561067e565b805460405260206040f35b630dca59c18114156101aa5760065460405260206040f35b632d61a3558114156101c25760075460405260206040f35b633b663195811415610233576101d6610667565b156101e057600080fd5b6101ed600435600161067e565b600081541415156101fd57600080fd5b6000600182015414151561021057600080fd5b6b033b2e3c9fd0803ce800000081556b033b2e3c9fd0803ce80000006001820155005b6378f1947081141561028b57610247610667565b1561025157600080fd5b61025e600435600461067e565b61026b60443582546106f6565b815561027a602435600461067e565b61028760443582546106b9565b8155005b6342066cbb8114156102ca5761029f610667565b156102a957600080fd5b6102b96024356004356003610695565b6102c660443582546106b9565b8155005b63a6e41821811415610328576102de610667565b156102e857600080fd5b6102f86024356004356003610695565b61030560643582546106f6565b81556103176044356004356003610695565b61032460643582546106b9565b8155005b635dd6471a8114156104165761033c610667565b1561034657600080fd5b6103566024356004356002610695565b61036360843582546106b9565b815561037560a43560018301546106b9565b6001820155610387600435600161067e565b61039760843560028301546106b9565b60028201556103ac60a43560038301546106b9565b60038201556103be6084358254610733565b6103ce6044356004356003610695565b6103d98282546106f6565b81556103eb60a4356001850154610733565b6103f8606435600461067e565b6104038282546106b9565b8155610411826006546106b9565b600655005b633690ae4c8114156105045761042a610667565b1561043457600080fd5b6104446024356004356002610695565b61045160843582546106b9565b815561046360a43560018301546106b9565b6001820155610475600435600161067e565b61048560843560028301546106b9565b600282015561049a60a43560038301546106b9565b60038201556104ac6084358254610733565b6104bc6044356004356003610695565b6104c78282546106f6565b81556104d960a4356001850154610733565b6104e6606435600561067e565b6104f18282546106f6565b81556104ff826007546106f6565b600755005b63990a5f6381141561057e57610518610667565b1561052257600080fd5b61052f600435600561067e565b61053c60443582546106f6565b815561054b602435600461067e565b61055860443582546106f6565b81556105686044356007546106f6565b6007556105796044356006546106f6565b600655005b63e6a6a64d8114156105f957610592610667565b1561059c57600080fd5b6105a9600435600161067e565b6105b960443560018301546106b9565b60018201556105ce6044356003830154610733565b6105db602435600461067e565b6105e68282546106b9565b81556105f4826006546106b9565b600655005b6309b7a0b58114156106625761060d610667565b1561061757600080fd5b610624600435600161067e565b61063160443582546106b9565b81556106436044356002830154610733565b6106536024356004356003610695565b61065e8282546106f6565b8155005b600080fd5b600061067433600061067e565b5460011415905090565b600082600052816020526040600020905092915050565b60008360005282602052816040526040602020602052604060002090509392505050565b6000828201905060008313156106d85781811115156106d757600080fd5b5b60008312156106f05781811015156106ef57600080fd5b5b92915050565b60008282039050600083121561071557818111151561071457600080fd5b5b600083131561072d57818110151561072c57600080fd5b5b92915050565b60008282029050600082121561074857600080fd5b600083141515610763578183820514151561076257600080fd5b5b929150505600a165627a7a723058201fcd622e26e92262e34259d46a2cb321a6b6f16f239ee5bf5a42f6e2b76c16ac0029") </programBytes>
<id> ACCT_ID </id>
<caller> CALLER_ID </caller>
<callData> #abiCallData("tune", #bytes32(ABI_i), #bytes32(ABI_u), #bytes32(ABI_v), #bytes32(ABI_w), #int256(ABI_dink), #int256(ABI_dart)) </callData>
<callValue> 0 </callValue>
<wordStack> .WordStack => _ </wordStack>
<localMem> .Map => _ </localMem>
<pc> 0 => _ </pc>
<gas> VGas => _ </gas>
<memoryUsed> 0 => _ </memoryUsed>
<previousGas> _ => _ </previousGas>
<static> false </static>
<callDepth> VCallDepth => _ </callDepth>
</callState>
<substate>
<selfDestruct> VSelfDestruct </selfDestruct>
<log> _ => VLog </log>
<refund> _ => VRefund </refund>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
<previousHash> _ </previousHash>
<ommersHash> _ </ommersHash>
<coinbase> _ </coinbase>
<stateRoot> _ </stateRoot>
<transactionsRoot> _ </transactionsRoot>
<receiptsRoot> _ </receiptsRoot>
<logsBloom> _ </logsBloom>
<difficulty> _ </difficulty>
<number> _ </number>
<gasLimit> _ </gasLimit>
<gasUsed> _ </gasUsed>
<timestamp> TIME </timestamp>
<extraData> _ </extraData>
<mixHash> _ </mixHash>
<blockNonce> _ </blockNonce>
<ommerBlockHeaders> _ </ommerBlockHeaders>
<blockhash> _ </blockhash>
</evm>
<network>
<activeAccounts> SetItem(ACCT_ID) _ </activeAccounts>
<accounts>
<account>
<acctID> ACCT_ID </acctID>
<balance> BAL </balance>
<code> #parseByteStack("0x608060405234801561001057600080fd5b507c01000000000000000000000000000000000000000000000000000000006000350463bf353dbb8114156100575761004c600435600061067e565b805460405260206040f35b6365fae35e8114156100885761006b610667565b1561007557600080fd5b610082600435600061067e565b60018155005b639c52a7f18114156100b95761009c610667565b156100a657600080fd5b6100b3600435600061067e565b60008155005b63d9638d368114156100f5576100d2600435600161067e565b805460405260018101546060526002810154608052600381015460a05260806040f35b6326e27482811415610123576101116024356004356002610695565b80546040526001810154606052604080f35b63c091268381141561014a5761013f6024356004356003610695565b805460405260206040f35b63f53e4e6981141561016e57610163600435600461067e565b805460405260206040f35b63a60f1d3e81141561019257610187600435600561067e565b805460405260206040f35b630dca59c18114156101aa5760065460405260206040f35b632d61a3558114156101c25760075460405260206040f35b633b663195811415610233576101d6610667565b156101e057600080fd5b6101ed600435600161067e565b600081541415156101fd57600080fd5b6000600182015414151561021057600080fd5b6b033b2e3c9fd0803ce800000081556b033b2e3c9fd0803ce80000006001820155005b6378f1947081141561028b57610247610667565b1561025157600080fd5b61025e600435600461067e565b61026b60443582546106f6565b815561027a602435600461067e565b61028760443582546106b9565b8155005b6342066cbb8114156102ca5761029f610667565b156102a957600080fd5b6102b96024356004356003610695565b6102c660443582546106b9565b8155005b63a6e41821811415610328576102de610667565b156102e857600080fd5b6102f86024356004356003610695565b61030560643582546106f6565b81556103176044356004356003610695565b61032460643582546106b9565b8155005b635dd6471a8114156104165761033c610667565b1561034657600080fd5b6103566024356004356002610695565b61036360843582546106b9565b815561037560a43560018301546106b9565b6001820155610387600435600161067e565b61039760843560028301546106b9565b60028201556103ac60a43560038301546106b9565b60038201556103be6084358254610733565b6103ce6044356004356003610695565b6103d98282546106f6565b81556103eb60a4356001850154610733565b6103f8606435600461067e565b6104038282546106b9565b8155610411826006546106b9565b600655005b633690ae4c8114156105045761042a610667565b1561043457600080fd5b6104446024356004356002610695565b61045160843582546106b9565b815561046360a43560018301546106b9565b6001820155610475600435600161067e565b61048560843560028301546106b9565b600282015561049a60a43560038301546106b9565b60038201556104ac6084358254610733565b6104bc6044356004356003610695565b6104c78282546106f6565b81556104d960a4356001850154610733565b6104e6606435600561067e565b6104f18282546106f6565b81556104ff826007546106f6565b600755005b63990a5f6381141561057e57610518610667565b1561052257600080fd5b61052f600435600561067e565b61053c60443582546106f6565b815561054b602435600461067e565b61055860443582546106f6565b81556105686044356007546106f6565b6007556105796044356006546106f6565b600655005b63e6a6a64d8114156105f957610592610667565b1561059c57600080fd5b6105a9600435600161067e565b6105b960443560018301546106b9565b60018201556105ce6044356003830154610733565b6105db602435600461067e565b6105e68282546106b9565b81556105f4826006546106b9565b600655005b6309b7a0b58114156106625761060d610667565b1561061757600080fd5b610624600435600161067e565b61063160443582546106b9565b81556106436044356002830154610733565b6106536024356004356003610695565b61065e8282546106f6565b8155005b600080fd5b600061067433600061067e565b5460011415905090565b600082600052816020526040600020905092915050565b60008360005282602052816040526040602020602052604060002090509392505050565b6000828201905060008313156106d85781811115156106d757600080fd5b5b60008312156106f05781811015156106ef57600080fd5b5b92915050565b60008282039050600083121561071557818111151561071457600080fd5b5b600083131561072d57818110151561072c57600080fd5b5b92915050565b60008282029050600082121561074857600080fd5b600083141515610763578183820514151561076257600080fd5b5b929150505600a165627a7a723058201fcd622e26e92262e34259d46a2cb321a6b6f16f239ee5bf5a42f6e2b76c16ac0029") </code>
<storage> (_:Map
(#Vat.debt |-> (Debt => Debt +Int (Rate *Int ABI_dart))
(#Vat.dai[ABI_w] |-> (Dai_w => Dai_w +Int (Rate *Int ABI_dart))
(#Vat.gem[ABI_i][ABI_v] |-> (Gem_iv => Gem_iv -Int (Take *Int ABI_dink))
(#Vat.ilks[ABI_i].Art |-> (Art_i => Art_i +Int ABI_dart)
(#Vat.ilks[ABI_i].Ink |-> (Ink_i => Ink_i +Int ABI_dink)
(#Vat.urns[ABI_i][ABI_u].art |-> (Art_iu => Art_iu +Int ABI_dart)
(#Vat.urns[ABI_i][ABI_u].ink |-> (Ink_iu => Ink_iu +Int ABI_dink)
(#Vat.ilks[ABI_i].rate |-> (Rate)
(#Vat.ilks[ABI_i].take |-> (Take)
(#Vat.wards[CALLER_ID] |-> (Can))))))))))))
</storage>
<nonce> _ </nonce>
</account>
...
</accounts>
<txOrder> _ </txOrder>
<txPending> _ </txPending>
<messages> _ </messages>
</network>
</ethereum>
requires #rangeAddress(ACCT_ID)
andBool #notPrecompileAddress(ACCT_ID)
andBool #rangeAddress(CALLER_ID)
andBool #rangeAddress(ORIGIN_ID)
andBool #rangeUInt(48, TIME)
andBool #rangeUInt(256, BAL)
andBool VCallDepth <=Int 1024
andBool (#rangeBytes(32, ABI_i)
andBool (#rangeBytes(32, ABI_u)
andBool (#rangeBytes(32, ABI_v)
andBool (#rangeBytes(32, ABI_w)
andBool (#rangeSInt(256, ABI_dink)
andBool (#rangeSInt(256, ABI_dart)
andBool (#rangeUInt(256, Can)
andBool (#rangeUInt(256, Take)
andBool (#rangeUInt(256, Rate)
andBool (#rangeUInt(256, Ink_iu)
andBool (#rangeUInt(256, Art_iu)
andBool (#rangeUInt(256, Ink_i)
andBool (#rangeUInt(256, Art_i)
andBool (#rangeUInt(256, Gem_iv)
andBool (#rangeUInt(256, Dai_w)
andBool (#rangeUInt(256, Debt)
andBool (VGas >Int 300000
andBool (Can ==Int 1
andBool (#rangeUInt(256, Ink_iu +Int ABI_dink)
andBool (#rangeUInt(256, Art_iu +Int ABI_dart)
andBool (#rangeUInt(256, Ink_i +Int ABI_dink)
andBool (#rangeUInt(256, Art_i +Int ABI_dart)
andBool (#rangeUInt(256, Gem_iv -Int (Take *Int ABI_dink))
andBool (#rangeUInt(256, Dai_w +Int (Rate *Int ABI_dart))
andBool (#rangeUInt(256, Debt +Int (Rate *Int ABI_dart))
andBool (#rangeSInt(256, Take)
andBool (#rangeSInt(256, Rate)
andBool (#rangeSInt(256, Take *Int ABI_dink)
andBool (#rangeSInt(256, Rate *Int ABI_dart))))))))))))))))))))))))))))))
endmodule