Skip to content

Instantly share code, notes, and snippets.

@nanexcool

nanexcool/db3df1bcdc106f54b6eb2df9459cb6e2208425e11cada230078d5e651e3ab039.k

Created October 30, 2019 19:34
Show Gist options
  • Save nanexcool/91fe387c924fea2680cadd5563fdbf5f to your computer and use it in GitHub Desktop.
Save nanexcool/91fe387c924fea2680cadd5563fdbf5f to your computer and use it in GitHub Desktop.
Download ZIP
db3df1bcdc106f54b6eb2df9459cb6e2208425e11cada230078d5e651e3ab039.k
Raw
db3df1bcdc106f54b6eb2df9459cb6e2208425e11cada230078d5e651e3ab039.k
requires "../rules.k"
requires "../bin_runtime.k"
module DB3DF1BCDC106F54B6EB2DF9459CB6E2208425E11CADA230078D5E651E3AB039
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
imports BIN_RUNTIME
// DssCdpManager_open
rule [DssCdpManager.open.pass.rough]:
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> PETERSBURG </schedule>
<ethereum>
<evm>
<output> _ => #asByteStackInWidthaux(Cdpi +Int 1, 31, 32, .WordStack) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<callStack> VCallStack </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
<callState>
<program> #asMapOpCodes(#dasmOpCodes(DssCdpManager_bin_runtime, PETERSBURG)) </program>
<programBytes> DssCdpManager_bin_runtime </programBytes>
<id> ACCT_ID </id>
<caller> CALLER_ID </caller>
<callData> #abiCallData("open", #bytes32(ABI_ilk), #address(ABI_usr)) ++ CD => _ </callData>
<callValue> VCallValue </callValue>
<wordStack> .WordStack => _ </wordStack>
<localMem> .Map => _ </localMem>
<pc> 0 => _ </pc>
<gas> VGas => _ </gas>
<memoryUsed> 0 => _ </memoryUsed>
<callGas> _ => _ </callGas>
<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) ACTIVE_ACCOUNTS_PRECOMPILES ACTIVE_ACCOUNTS_REST (.Set => SetItem(UrnHandler)) </activeAccounts>
<accounts>
<account>
<acctID> ACCT_ID </acctID>
<balance> ACCT_ID_balance </balance>
<code> DssCdpManager_bin_runtime </code>
<storage>
.Map
[#DssCdpManager.vat <- (Vat => Vat)]
[#DssCdpManager.cdpi <- (Cdpi => Cdpi +Int 1)]
[#DssCdpManager.urns[Cdpi +Int 1] <- (Urn => NewUrn)]
[#DssCdpManager.last[ABI_usr] <- (Last => Cdpi +Int 1)]
[#DssCdpManager.count[ABI_usr] <- (Count => Count +Int 1)]
[#DssCdpManager.owns[Cdpi +Int 1] <- (Own => ABI_usr)]
[#DssCdpManager.ilks[Cdpi +Int 1] <- (Ilk => ABI_ilk)]
[#DssCdpManager.first[ABI_usr] <- (First => #if First ==Int 0 #then Cdpi +Int 1 #else First #fi)]
[#DssCdpManager.list[Cdpi +Int 1].prev <- (Prev => #if Last =/=Int 0 #then Last #else Prev #fi)]
[#DssCdpManager.list[Last].next <- (Next => #if Last =/=Int 0 #then Cdpi +Int 1 #else Next #fi)]
_:Map
</storage>
<origStorage> _ </origStorage>
<nonce> ACCT_NONCE </nonce>
</account>
<account>
<acctID> 1 </acctID>
<balance> ECREC_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> 2 </acctID>
<balance> SHA256_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> 3 </acctID>
<balance> RIP160_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> 4 </acctID>
<balance> ID_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> 5 </acctID>
<balance> MODEXP_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> 6 </acctID>
<balance> ECADD_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> 7 </acctID>
<balance> ECMUL_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> 8 </acctID>
<balance> ECPAIRING_BAL </balance>
<code> .WordStack </code>
<storage> _:Map </storage>
<origStorage> _ </origStorage>
<nonce> _ </nonce>
</account>
<account>
<acctID> #newAddr(ACCT_ID, ACCT_NONCE) </acctID>
<balance> 0 </balance>
<code> .WordStack => UrnHandler_bin_runtime </code>
<storage> .Map </storage>
<origStorage> .Map </origStorage>
<nonce> 0 </nonce>
</account>
...
</accounts>
<txOrder> _ </txOrder>
<txPending> _ </txPending>
<messages> _ </messages>
</network>
</ethereum>
requires #rangeAddress(ACCT_ID)
andBool #notPrecompileAddress(ACCT_ID)
// bind ACTIVE_ACCOUNTS_PRECOMPILES
andBool (ACTIVE_ACCOUNTS_PRECOMPILES:Set ==K (
SetItem(1)
SetItem(2)
SetItem(3)
SetItem(4)
SetItem(5)
SetItem(6)
SetItem(7)
SetItem(8)))
// bind UrnHandler
andBool (UrnHandler ==K #newAddress(ACCT_ID, ACCT_NONCE))
// no collision with existing accounts
andBool (notBool (UrnHandler in (SetItem(ACCT_ID) ACTIVE_ACCOUNTS_PRECOMPILES ACTIVE_ACCOUNTS_REST)))
andBool (notBool (UrnHandler ==K Vat))
andBool #rangeAddress(CALLER_ID)
andBool #rangeAddress(ORIGIN_ID)
andBool #rangeUInt(256, TIME)
andBool #rangeUInt(256, ACCT_ID_balance)
andBool #rangeUInt(256, ECREC_BAL)
andBool #rangeUInt(256, SHA256_BAL)
andBool #rangeUInt(256, RIP160_BAL)
andBool #rangeUInt(256, ID_BAL)
andBool #rangeUInt(256, MODEXP_BAL)
andBool #rangeUInt(256, ECADD_BAL)
andBool #rangeUInt(256, ECMUL_BAL)
andBool #rangeUInt(256, ECPAIRING_BAL)
andBool VCallDepth <=Int 1024
andBool #rangeUInt(256, VCallValue)
andBool (#rangeBytes(32, ABI_ilk)
andBool (#rangeAddress(ABI_usr)
andBool (#rangeAddress(Vat)
andBool (#rangeUInt(256, Cdpi)
andBool (#rangeAddress(Urn)
andBool (#rangeAddress(NewUrn)
andBool (#rangeUInt(256, Last)
andBool (#rangeUInt(256, Count)
andBool (#rangeAddress(Own)
andBool (#rangeBytes(32, Ilk)
andBool (#rangeUInt(256, First)
andBool (#rangeUInt(256, Prev)
andBool (#rangeUInt(256, Next)
andBool (#sizeWordStack(CD) <=Int 1250000000
andBool (#notPrecompileAddress(Vat)
andBool (#notPrecompileAddress(Urn)
andBool (#notPrecompileAddress(NewUrn)
andBool (#notPrecompileAddress(Own)
andBool (VGas >=Int 3000000
andBool (((#rangeUInt(256, Cdpi +Int 1)))
andBool (((#rangeUInt(256, Count +Int 1)))
andBool ((VCallValue ==Int 0)
andBool ((ABI_usr =/=Int 0))))))))))))))))))))))))
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment