Skip to content

Instantly share code, notes, and snippets.

@desaperados

desaperados/out.k

Created January 30, 2020 22:23
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save desaperados/b6fdc9aa3d618c252a6227596aba4d49 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save desaperados/b6fdc9aa3d618c252a6227596aba4d49 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
out.k
requires "../rules.k"
requires "../bin_runtime.k"
module F87CBA36744EF68A848546773B864B33F68180DE212454D6D855448961B64AD6
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
imports BIN_RUNTIME
// Mom_create
rule [Mom.create.pass.rough]:
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> PETERSBURG </schedule>
<ethereum>
<evm>
<output> .WordStack </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<callStack> VCallStack </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
<callState>
<program> #asMapOpCodes(#dasmOpCodes(Mom_bin_runtime, PETERSBURG)) </program>
<programBytes> Mom_bin_runtime </programBytes>
<id> ACCT_ID </id>
<caller> CALLER_ID </caller>
<callData> #abiCallData("create", .TypedArgs) ++ 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> BLOCK_NUMBER </number>
<gasLimit> _ </gasLimit>
<gasUsed> _ </gasUsed>
<timestamp> TIME </timestamp>
<extraData> _ </extraData>
<mixHash> _ </mixHash>
<blockNonce> _ </blockNonce>
<ommerBlockHeaders> _ </ommerBlockHeaders>
<blockhash> _ </blockhash>
</evm>
<network>
<activeAccounts>
ACCTS:Set
(.Set => SetItem(#newAddr(KID, NONCE)))
SetItem(ACCT_ID)
SetItem(1)
SetItem(2)
SetItem(3)
SetItem(4)
SetItem(5)
SetItem(6)
SetItem(7)
SetItem(8) _ </activeAccounts>
<accounts>
( .Bag =>
<account>
<acctID> #newAddr(KID, NONCE) </acctID>
<balance> KID_balance </balance>
<code> Kid_bin_runtime </code>
<storage>
.Map
[#Kid.parent <- (Parent) ]
_:Map
</storage>
<origStorage> _ </origStorage>
<nonce> 1 </nonce>
</account>
)
<account>
<acctID> ACCT_ID </acctID>
<balance> ACCT_ID_balance </balance>
<code> Mom_bin_runtime </code>
<storage>
.Map
[#Mom.child <- (Junk_0) => KID]
_:Map
</storage>
<origStorage> _ </origStorage>
<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>
...
</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(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 (#rangeAddress(Parent)
andBool (#rangeAddress(KID)
andBool (#rangeUInt(256, KID_balance)
andBool (#sizeWordStack(CD) <=Int 1250000000
andBool (#notPrecompileAddress(Parent)
andBool (#notPrecompileAddress(KID)
andBool (ACCT_ID =/=Int KID
andBool (VGas >=Int 3000000
andBool (#rangeUInt(256, Junk_0)
andBool ((VCallValue ==Int 0)))))))))))
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment