Skip to content

Instantly share code, notes, and snippets.

@MrChico

MrChico/Heal with import

Last active September 17, 2018 15:42
Show Gist options
  • Save MrChico/3a08a49f3aa724206feb17aa8c0ba602 to your computer and use it in GitHub Desktop.
Save MrChico/3a08a49f3aa724206feb17aa8c0ba602 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Heal with import
requires "../rules.k"
module PROOF-VOW_HEAL_SUCC
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
// heal-success of Vow
rule
<k> #execute => #halt </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("0x608060405234801561001057600080fd5b507c01000000000000000000000000000000000000000000000000000000006000350463bf353dbb8114156100575761004c60043560006108b9565b805460405260206040f35b6365fae35e8114156100885761006b6108a2565b1561007557600080fd5b61008260043560006108b9565b60018155005b639c52a7f18114156100b95761009c6108a2565b156100a657600080fd5b6100b360043560006108b9565b60008155005b6336569e778114156100d15760015460405260206040f35b63dfbf306d8114156100e95760025460405260206040f35b6370904ded8114156101015760035460405260206040f35b637f49edc48114156101255761011a60043560046108b9565b805460405260206040f35b63d0adc35f81141561013d5760055460405260206040f35b6349dd5bb28114156101555760065460405260206040f35b632a1d2b3c81141561016d5760075460405260206040f35b6364bd70138114156101855760085460405260206040f35b63c349d36281141561019d5760095460405260206040f35b6368110b2f8114156101b557600a5460405260206040f35b631b8e8cfa8114156101cd57600b5460405260206040f35b63143e55e08114156101e3574260405260206040f35b6305db4538811415610200576101f7610819565b60405260206040f35b6307a832b481141561021d57610214610839565b60405260206040f35b6329ae8114811415610301576102316108a2565b1561023b57600080fd5b7f7761697400000000000000000000000000000000000000000000000000000000600435141561026c576024356008555b7f73756d7000000000000000000000000000000000000000000000000000000000600435141561029d576024356009555b7f62756d700000000000000000000000000000000000000000000000000000000060043514156102ce57602435600a555b7f68756d700000000000000000000000000000000000000000000000000000000060043514156102ff57602435600b555b005b63d4e8be838114156103b4576103156108a2565b1561031f57600080fd5b7f666c6170000000000000000000000000000000000000000000000000000000006004351415610350576024356002555b7f666c6f70000000000000000000000000000000000000000000000000000000006004351415610381576024356003555b7f766174000000000000000000000000000000000000000000000000000000000060043514156103b2576024356001555b005b63f37ac61c811415610455576006546103db6b033b2e3c9fd0803ce8000000600435610904565b6000811282600435116103ec610839565b600435111717156103fc57600080fd5b610408600435836108ea565b6005557f990a5f630000000000000000000000000000000000000000000000000000000060005230600452306024528060445260008060646000806001545af1151561045357600080fd5b005b632506855a8114156104f65760075461047c6b033b2e3c9fd0803ce8000000600435610904565b60008112610488610839565b60043511836004351117171561049d57600080fd5b6104a9600435836108ea565b6006557f990a5f630000000000000000000000000000000000000000000000000000000060005230600452306024528060445260008060646000806001545af115156104f457600080fd5b005b63697efb788114156105485761050a6108a2565b1561051457600080fd5b61052661051f6107d4565b60046108b9565b61053360043582546108d0565b81556105436004356005546108d0565b600555005b6335aee16f8114156105a85761055c6107d4565b61056a6008546004356108d0565b111561057557600080fd5b61058260043560046108b9565b8054610590816005546108ea565b60055561059f816006546108d0565b60065560008255005b63bbbb0d7b81141561066857600654600954808210156105c757600080fd5b60006105d1610839565b1415156105dd57600080fd5b6105e781836108ea565b6006556105f6816007546108d0565b6007557fb7e9cd2400000000000000000000000000000000000000000000000000000000600052306004527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff602452806044526020604060646000806003545af1151561066257600080fd5b60206040f35b630e01198b8114156107cf57600a54610693600b5461068e83610689610819565b6108d0565b6108d0565b61069b610839565b10156106a657600080fd5b60006006541415156106b757600080fd5b7ff4b9fa75000000000000000000000000000000000000000000000000000000006000526020604060046000806002545af115156106f457600080fd5b6040517fa3b22fc4000000000000000000000000000000000000000000000000000000006000526002546004526000806024600080855af1151561073757600080fd5b7fb7e9cd240000000000000000000000000000000000000000000000000000000060005260006004528160245260006044526020604060646000806002545af1151561078257600080fd5b6040517fdc4d20fa000000000000000000000000000000000000000000000000000000006000526002546004526000806024600080865af115156107c557600080fd5b8060405260206040f35b600080fd5b60007f143e55e000000000000000000000000000000000000000000000000000000000600052602060006004600080305af1151561081157600080fd5b600051905090565b600061083460075461082f6006546006546108d0565b6108d0565b905090565b60007ff53e4e6900000000000000000000000000000000000000000000000000000000600052306004526020600060246000806001545af1151561087c57600080fd5b600051600081101561088d57600080fd5b6b033b2e3c9fd0803ce8000000810491505090565b60006108af3360006108b9565b5460011415905090565b600082600052816020526040600020905092915050565b60008282019050818110156108e457600080fd5b92915050565b60008282039050818111156108fe57600080fd5b92915050565b6000828202905081838204146000841417151561092057600080fd5b929150505600a165627a7a72305820dc1ef531d6c15e053cdc5cc877acb2f9409218529131c81b955466205c333dbe0029"), BYZANTIUM)) </program>
<programBytes> #parseByteStack("0x608060405234801561001057600080fd5b507c01000000000000000000000000000000000000000000000000000000006000350463bf353dbb8114156100575761004c60043560006108b9565b805460405260206040f35b6365fae35e8114156100885761006b6108a2565b1561007557600080fd5b61008260043560006108b9565b60018155005b639c52a7f18114156100b95761009c6108a2565b156100a657600080fd5b6100b360043560006108b9565b60008155005b6336569e778114156100d15760015460405260206040f35b63dfbf306d8114156100e95760025460405260206040f35b6370904ded8114156101015760035460405260206040f35b637f49edc48114156101255761011a60043560046108b9565b805460405260206040f35b63d0adc35f81141561013d5760055460405260206040f35b6349dd5bb28114156101555760065460405260206040f35b632a1d2b3c81141561016d5760075460405260206040f35b6364bd70138114156101855760085460405260206040f35b63c349d36281141561019d5760095460405260206040f35b6368110b2f8114156101b557600a5460405260206040f35b631b8e8cfa8114156101cd57600b5460405260206040f35b63143e55e08114156101e3574260405260206040f35b6305db4538811415610200576101f7610819565b60405260206040f35b6307a832b481141561021d57610214610839565b60405260206040f35b6329ae8114811415610301576102316108a2565b1561023b57600080fd5b7f7761697400000000000000000000000000000000000000000000000000000000600435141561026c576024356008555b7f73756d7000000000000000000000000000000000000000000000000000000000600435141561029d576024356009555b7f62756d700000000000000000000000000000000000000000000000000000000060043514156102ce57602435600a555b7f68756d700000000000000000000000000000000000000000000000000000000060043514156102ff57602435600b555b005b63d4e8be838114156103b4576103156108a2565b1561031f57600080fd5b7f666c6170000000000000000000000000000000000000000000000000000000006004351415610350576024356002555b7f666c6f70000000000000000000000000000000000000000000000000000000006004351415610381576024356003555b7f766174000000000000000000000000000000000000000000000000000000000060043514156103b2576024356001555b005b63f37ac61c811415610455576006546103db6b033b2e3c9fd0803ce8000000600435610904565b6000811282600435116103ec610839565b600435111717156103fc57600080fd5b610408600435836108ea565b6005557f990a5f630000000000000000000000000000000000000000000000000000000060005230600452306024528060445260008060646000806001545af1151561045357600080fd5b005b632506855a8114156104f65760075461047c6b033b2e3c9fd0803ce8000000600435610904565b60008112610488610839565b60043511836004351117171561049d57600080fd5b6104a9600435836108ea565b6006557f990a5f630000000000000000000000000000000000000000000000000000000060005230600452306024528060445260008060646000806001545af115156104f457600080fd5b005b63697efb788114156105485761050a6108a2565b1561051457600080fd5b61052661051f6107d4565b60046108b9565b61053360043582546108d0565b81556105436004356005546108d0565b600555005b6335aee16f8114156105a85761055c6107d4565b61056a6008546004356108d0565b111561057557600080fd5b61058260043560046108b9565b8054610590816005546108ea565b60055561059f816006546108d0565b60065560008255005b63bbbb0d7b81141561066857600654600954808210156105c757600080fd5b60006105d1610839565b1415156105dd57600080fd5b6105e781836108ea565b6006556105f6816007546108d0565b6007557fb7e9cd2400000000000000000000000000000000000000000000000000000000600052306004527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff602452806044526020604060646000806003545af1151561066257600080fd5b60206040f35b630e01198b8114156107cf57600a54610693600b5461068e83610689610819565b6108d0565b6108d0565b61069b610839565b10156106a657600080fd5b60006006541415156106b757600080fd5b7ff4b9fa75000000000000000000000000000000000000000000000000000000006000526020604060046000806002545af115156106f457600080fd5b6040517fa3b22fc4000000000000000000000000000000000000000000000000000000006000526002546004526000806024600080855af1151561073757600080fd5b7fb7e9cd240000000000000000000000000000000000000000000000000000000060005260006004528160245260006044526020604060646000806002545af1151561078257600080fd5b6040517fdc4d20fa000000000000000000000000000000000000000000000000000000006000526002546004526000806024600080865af115156107c557600080fd5b8060405260206040f35b600080fd5b60007f143e55e000000000000000000000000000000000000000000000000000000000600052602060006004600080305af1151561081157600080fd5b600051905090565b600061083460075461082f6006546006546108d0565b6108d0565b905090565b60007ff53e4e6900000000000000000000000000000000000000000000000000000000600052306004526020600060246000806001545af1151561087c57600080fd5b600051600081101561088d57600080fd5b6b033b2e3c9fd0803ce8000000810491505090565b60006108af3360006108b9565b5460011415905090565b600082600052816020526040600020905092915050565b60008282019050818110156108e457600080fd5b92915050565b60008282039050818111156108fe57600080fd5b92915050565b6000828202905081838204146000841417151561092057600080fd5b929150505600a165627a7a72305820dc1ef531d6c15e053cdc5cc877acb2f9409218529131c81b955466205c333dbe0029") </programBytes>
<id> ACCT_ID </id>
<caller> CALLER_ID </caller>
<callData> #abiCallData("heal", #uint256(ABI_wad)) </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> CALL_DEPTH => _ </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)
SetItem(Vat) </activeAccounts>
<accounts>
<account>
<acctID> Vat </acctID>
<balance> Vat_balance </balance>
<code> #parseByteStack("0x608060405234801561001057600080fd5b507c01000000000000000000000000000000000000000000000000000000006000350463bf353dbb8114156100575761004c600435600061067e565b805460405260206040f35b6365fae35e8114156100885761006b610667565b1561007557600080fd5b610082600435600061067e565b60018155005b639c52a7f18114156100b95761009c610667565b156100a657600080fd5b6100b3600435600061067e565b60008155005b63d9638d368114156100f5576100d2600435600161067e565b805460405260018101546060526002810154608052600381015460a05260806040f35b6326e27482811415610123576101116024356004356002610695565b80546040526001810154606052604080f35b63c091268381141561014a5761013f6024356004356003610695565b805460405260206040f35b63f53e4e6981141561016e57610163600435600461067e565b805460405260206040f35b63a60f1d3e81141561019257610187600435600561067e565b805460405260206040f35b630dca59c18114156101aa5760065460405260206040f35b632d61a3558114156101c25760075460405260206040f35b633b663195811415610233576101d6610667565b156101e057600080fd5b6101ed600435600161067e565b600081541415156101fd57600080fd5b6000600182015414151561021057600080fd5b6b033b2e3c9fd0803ce800000081556b033b2e3c9fd0803ce80000006001820155005b6378f1947081141561028b57610247610667565b1561025157600080fd5b61025e600435600461067e565b61026b60443582546106f6565b815561027a602435600461067e565b61028760443582546106b9565b8155005b6342066cbb8114156102ca5761029f610667565b156102a957600080fd5b6102b96024356004356003610695565b6102c660443582546106b9565b8155005b63a6e41821811415610328576102de610667565b156102e857600080fd5b6102f86024356004356003610695565b61030560643582546106f6565b81556103176044356004356003610695565b61032460643582546106b9565b8155005b635dd6471a8114156104165761033c610667565b1561034657600080fd5b6103566024356004356002610695565b61036360843582546106b9565b815561037560a43560018301546106b9565b6001820155610387600435600161067e565b61039760843560028301546106b9565b60028201556103ac60a43560038301546106b9565b60038201556103be6084358254610733565b6103ce6044356004356003610695565b6103d98282546106f6565b81556103eb60a4356001850154610733565b6103f8606435600461067e565b6104038282546106b9565b8155610411826006546106b9565b600655005b633690ae4c8114156105045761042a610667565b1561043457600080fd5b6104446024356004356002610695565b61045160843582546106b9565b815561046360a43560018301546106b9565b6001820155610475600435600161067e565b61048560843560028301546106b9565b600282015561049a60a43560038301546106b9565b60038201556104ac6084358254610733565b6104bc6044356004356003610695565b6104c78282546106f6565b81556104d960a4356001850154610733565b6104e6606435600561067e565b6104f18282546106f6565b81556104ff826007546106f6565b600755005b63990a5f6381141561057e57610518610667565b1561052257600080fd5b61052f600435600561067e565b61053c60443582546106f6565b815561054b602435600461067e565b61055860443582546106f6565b81556105686044356007546106f6565b6007556105796044356006546106f6565b600655005b63e6a6a64d8114156105f957610592610667565b1561059c57600080fd5b6105a9600435600161067e565b6105b960443560018301546106b9565b60018201556105ce6044356003830154610733565b6105db602435600461067e565b6105e68282546106b9565b81556105f4826006546106b9565b600655005b6309b7a0b58114156106625761060d610667565b1561061757600080fd5b610624600435600161067e565b61063160443582546106b9565b81556106436044356002830154610733565b6106536024356004356003610695565b61065e8282546106f6565b8155005b600080fd5b600061067433600061067e565b5460011415905090565b600082600052816020526040600020905092915050565b60008360005282602052816040526040602020602052604060002090509392505050565b6000828201905060008313156106d85781811115156106d757600080fd5b5b60008312156106f05781811015156106ef57600080fd5b5b92915050565b60008282039050600083121561071557818111151561071457600080fd5b5b600083131561072d57818110151561072c57600080fd5b5b92915050565b60008282029050600082121561074857600080fd5b600083141515610763578183820514151561076257600080fd5b5b929150505600a165627a7a723058201fcd622e26e92262e34259d46a2cb321a6b6f16f239ee5bf5a42f6e2b76c16ac0029") </code>
<storage> #Vat.wards(ACCT_ID) |-> (Can)
#Vat.dai(ACCT_ID) |-> (Dai => Dai -Int #Ray *Int ABI_wad)
#Vat.sin(ACCT_ID) |-> (Sin => Sin -Int #Ray *Int ABI_wad)
#Vat.vice |-> (Vice => Vice -Int #Ray *Int ABI_wad)
#Vat.debt |-> (Debt => Debt -Int #Ray *Int ABI_wad) </storage>
<nonce> _ </nonce>
</account>
<account>
<acctID> ACCT_ID </acctID>
<balance> BAL </balance>
<code> #parseByteStack("0x608060405234801561001057600080fd5b507c01000000000000000000000000000000000000000000000000000000006000350463bf353dbb8114156100575761004c60043560006108b9565b805460405260206040f35b6365fae35e8114156100885761006b6108a2565b1561007557600080fd5b61008260043560006108b9565b60018155005b639c52a7f18114156100b95761009c6108a2565b156100a657600080fd5b6100b360043560006108b9565b60008155005b6336569e778114156100d15760015460405260206040f35b63dfbf306d8114156100e95760025460405260206040f35b6370904ded8114156101015760035460405260206040f35b637f49edc48114156101255761011a60043560046108b9565b805460405260206040f35b63d0adc35f81141561013d5760055460405260206040f35b6349dd5bb28114156101555760065460405260206040f35b632a1d2b3c81141561016d5760075460405260206040f35b6364bd70138114156101855760085460405260206040f35b63c349d36281141561019d5760095460405260206040f35b6368110b2f8114156101b557600a5460405260206040f35b631b8e8cfa8114156101cd57600b5460405260206040f35b63143e55e08114156101e3574260405260206040f35b6305db4538811415610200576101f7610819565b60405260206040f35b6307a832b481141561021d57610214610839565b60405260206040f35b6329ae8114811415610301576102316108a2565b1561023b57600080fd5b7f7761697400000000000000000000000000000000000000000000000000000000600435141561026c576024356008555b7f73756d7000000000000000000000000000000000000000000000000000000000600435141561029d576024356009555b7f62756d700000000000000000000000000000000000000000000000000000000060043514156102ce57602435600a555b7f68756d700000000000000000000000000000000000000000000000000000000060043514156102ff57602435600b555b005b63d4e8be838114156103b4576103156108a2565b1561031f57600080fd5b7f666c6170000000000000000000000000000000000000000000000000000000006004351415610350576024356002555b7f666c6f70000000000000000000000000000000000000000000000000000000006004351415610381576024356003555b7f766174000000000000000000000000000000000000000000000000000000000060043514156103b2576024356001555b005b63f37ac61c811415610455576006546103db6b033b2e3c9fd0803ce8000000600435610904565b6000811282600435116103ec610839565b600435111717156103fc57600080fd5b610408600435836108ea565b6005557f990a5f630000000000000000000000000000000000000000000000000000000060005230600452306024528060445260008060646000806001545af1151561045357600080fd5b005b632506855a8114156104f65760075461047c6b033b2e3c9fd0803ce8000000600435610904565b60008112610488610839565b60043511836004351117171561049d57600080fd5b6104a9600435836108ea565b6006557f990a5f630000000000000000000000000000000000000000000000000000000060005230600452306024528060445260008060646000806001545af115156104f457600080fd5b005b63697efb788114156105485761050a6108a2565b1561051457600080fd5b61052661051f6107d4565b60046108b9565b61053360043582546108d0565b81556105436004356005546108d0565b600555005b6335aee16f8114156105a85761055c6107d4565b61056a6008546004356108d0565b111561057557600080fd5b61058260043560046108b9565b8054610590816005546108ea565b60055561059f816006546108d0565b60065560008255005b63bbbb0d7b81141561066857600654600954808210156105c757600080fd5b60006105d1610839565b1415156105dd57600080fd5b6105e781836108ea565b6006556105f6816007546108d0565b6007557fb7e9cd2400000000000000000000000000000000000000000000000000000000600052306004527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff602452806044526020604060646000806003545af1151561066257600080fd5b60206040f35b630e01198b8114156107cf57600a54610693600b5461068e83610689610819565b6108d0565b6108d0565b61069b610839565b10156106a657600080fd5b60006006541415156106b757600080fd5b7ff4b9fa75000000000000000000000000000000000000000000000000000000006000526020604060046000806002545af115156106f457600080fd5b6040517fa3b22fc4000000000000000000000000000000000000000000000000000000006000526002546004526000806024600080855af1151561073757600080fd5b7fb7e9cd240000000000000000000000000000000000000000000000000000000060005260006004528160245260006044526020604060646000806002545af1151561078257600080fd5b6040517fdc4d20fa000000000000000000000000000000000000000000000000000000006000526002546004526000806024600080865af115156107c557600080fd5b8060405260206040f35b600080fd5b60007f143e55e000000000000000000000000000000000000000000000000000000000600052602060006004600080305af1151561081157600080fd5b600051905090565b600061083460075461082f6006546006546108d0565b6108d0565b905090565b60007ff53e4e6900000000000000000000000000000000000000000000000000000000600052306004526020600060246000806001545af1151561087c57600080fd5b600051600081101561088d57600080fd5b6b033b2e3c9fd0803ce8000000810491505090565b60006108af3360006108b9565b5460011415905090565b600082600052816020526040600020905092915050565b60008282019050818110156108e457600080fd5b92915050565b60008282039050818111156108fe57600080fd5b92915050565b6000828202905081838204146000841417151561092057600080fd5b929150505600a165627a7a72305820dc1ef531d6c15e053cdc5cc877acb2f9409218529131c81b955466205c333dbe0029") </code>
<storage> #Vow.vat |-> (Vat)
#Vow.Woe |-> (Woe => Woe -Int ABI_wad)
_:Map
</storage>
<nonce> _ </nonce>
</account>
...
</accounts>
<txOrder> _ </txOrder>
<txPending> _ </txPending>
<messages> _ </messages>
</network>
</ethereum>
requires 0 <=Int ACCT_ID andBool ACCT_ID <Int (2 ^Int 160)
andBool 0 <=Int CALLER_ID andBool CALLER_ID <Int (2 ^Int 160)
andBool 0 <=Int ORIGIN_ID andBool ORIGIN_ID <Int (2 ^Int 160)
andBool #rangeUInt(256, ABI_wad)
andBool #rangeUInt(256, Can)
andBool #rangeAddress(Vat)
andBool #rangeUInt(256, Woe)
andBool #rangeUInt(256, Dai)
andBool #rangeUInt(256, Sin)
andBool #rangeUInt(256, Vice)
andBool #rangeUInt(256, Debt)
andBool #rangeUInt(256, Vat_balance)
andBool Can ==Int 1
andBool ABI_wad <=Int Dai /Int 1000000000000000000000000000
andBool ABI_wad <=Int Woe
andBool #rangeUInt(256, Woe -Int ABI_wad)
andBool #rangeUInt(256, Dai -Int #Ray *Int ABI_wad)
andBool #rangeUInt(256, Sin -Int #Ray *Int ABI_wad)
andBool #rangeUInt(256, Vice -Int #Ray *Int ABI_wad)
andBool #rangeUInt(256, Debt -Int #Ray *Int ABI_wad)
andBool #rangeSInt(256, #Ray *Int ABI_wad)
// heal-success of Vat
rule
<k> #execute ~> ... => #halt ~> ... </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> BYZANTIUM </schedule>
<analysis> .Map </analysis>
<ethereum>
<evm>
<output> .WordStack </output>
<statusCode> _ </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("heal", #bytes32(ABI_u), #bytes32(ABI_v), #int256(ABI_rad)) </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> CALL_DEPTH => _ </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> #Vat.wards(CALLER_ID) |-> (Can)
#Vat.dai(ABI_v) |-> (Dai_v => Dai_v -Int ABI_rad)
#Vat.sin(ABI_u) |-> (Sin_u => Sin_u -Int ABI_rad)
#Vat.debt |-> (Debt => Debt -Int ABI_rad)
#Vat.vice |-> (Vice => Vice -Int ABI_rad)
_:Map
</storage>
<nonce> _ </nonce>
</account>
...
</accounts>
<txOrder> _ </txOrder>
<txPending> _ </txPending>
<messages> _ </messages>
</network>
</ethereum>
requires 0 <=Int ACCT_ID andBool ACCT_ID <Int (2 ^Int 160)
andBool 0 <=Int CALLER_ID andBool CALLER_ID <Int (2 ^Int 160)
andBool 0 <=Int ORIGIN_ID andBool ORIGIN_ID <Int (2 ^Int 160)
andBool #rangeBytes(32, ABI_u)
andBool #rangeBytes(32, ABI_v)
andBool #rangeSInt(256, ABI_rad)
andBool #rangeUInt(256, Can)
andBool #rangeUInt(256, Dai_v)
andBool #rangeUInt(256, Sin_u)
andBool #rangeUInt(256, Debt)
andBool #rangeUInt(256, Vice)
andBool VGas >Int 300000
andBool Can ==Int 1
andBool #rangeUInt(256, Dai_v -Int ABI_rad)
andBool #rangeUInt(256, Sin_u -Int ABI_rad)
andBool #rangeUInt(256, Debt -Int ABI_rad)
andBool #rangeUInt(256, Vice -Int ABI_rad)
// heal-fail of Vat
rule
<k> #execute ~> ... => #halt ~> ... </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> BYZANTIUM </schedule>
<analysis> .Map </analysis>
<ethereum>
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </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("heal", #bytes32(ABI_u), #bytes32(ABI_v), #int256(ABI_rad)) </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> CALL_DEPTH => _ </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> #Vat.wards(CALLER_ID) |-> (Can)
#Vat.dai(ABI_v) |-> (Dai_v => _ )
#Vat.sin(ABI_u) |-> (Sin_u => _ )
#Vat.debt |-> (Debt => _ )
#Vat.vice |-> (Vice => _ )
_:Map
</storage>
<nonce> _ </nonce>
</account>
...
</accounts>
<txOrder> _ </txOrder>
<txPending> _ </txPending>
<messages> _ </messages>
</network>
</ethereum>
requires 0 <=Int ACCT_ID andBool ACCT_ID <Int (2 ^Int 160)
andBool 0 <=Int CALLER_ID andBool CALLER_ID <Int (2 ^Int 160)
andBool 0 <=Int ORIGIN_ID andBool ORIGIN_ID <Int (2 ^Int 160)
andBool #rangeBytes(32, ABI_u)
andBool #rangeBytes(32, ABI_v)
andBool #rangeSInt(256, ABI_rad)
andBool #rangeUInt(256, Can)
andBool #rangeUInt(256, Dai_v)
andBool #rangeUInt(256, Sin_u)
andBool #rangeUInt(256, Debt)
andBool #rangeUInt(256, Vice)
andBool VGas >Int 300000
andBool notBool (
Can ==Int 1
andBool #rangeUInt(256, Dai_v -Int ABI_rad)
andBool #rangeUInt(256, Sin_u -Int ABI_rad)
andBool #rangeUInt(256, Debt -Int ABI_rad)
andBool #rangeUInt(256, Vice -Int ABI_rad)
)
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment