Created
February 5, 2020 01:41
-
-
Save mhhf/92154ffe83390f1e0f851d41927df6c3 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
requires "../rules.k" | |
requires "../bin_runtime.k" | |
module 0A6A1BB57DF4B6950C126D3D10AF302A7CA8A395FA7E5CB2A6CB8BCB99573285 | |
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> ISTANBUL </schedule> | |
<ethereum> | |
<evm> | |
<output> .WordStack </output> | |
<statusCode> _ => EVMC_SUCCESS </statusCode> | |
<callStack> VCallStack </callStack> | |
<interimStates> _ </interimStates> | |
<touchedAccounts> _ => _ </touchedAccounts> | |
<callState> | |
<program> Mom_bin_runtime </program> | |
<jumpDests> #computeValidJumpDests(Mom_bin_runtime) </jumpDests> | |
<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> | |
<blockhashes> _ </blockhashes> | |
<block> | |
<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> | |
</block> | |
</evm> | |
<network> | |
<activeAccounts> | |
SetItem(1) | |
SetItem(2) | |
SetItem(3) | |
SetItem(4) | |
SetItem(5) | |
SetItem(6) | |
SetItem(7) | |
SetItem(ACCT_ID) | |
SetItem(8) | |
SetItem(KID) | |
_ </activeAccounts> | |
<accounts> | |
<account> | |
<acctID> KID </acctID> | |
<balance> 0 => 0 </balance> | |
<code> .WordStack => Kid_bin_runtime </code> | |
<storage> | |
.Map => (.Map | |
[#Kid.parent <- (ACCT_ID) ] | |
) | |
</storage> | |
<origStorage> | |
.Map | |
</origStorage> | |
<nonce> 0 => 1 </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> ACCT_ID </acctID> | |
<balance> ACCT_ID_balance </balance> | |
<code> Mom_bin_runtime </code> | |
<storage> | |
.Map | |
[#Mom.child <- 0 => KID] | |
_:Map | |
</storage> | |
<origStorage> | |
.Map | |
[#Mom.child <- 0] | |
_:Map | |
</origStorage> | |
<nonce> 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, NONCE) | |
andBool #rangeUInt(256, ECPAIRING_BAL) | |
andBool VCallDepth <=Int 1024 | |
andBool #rangeUInt(256, VCallValue) | |
andBool (#rangeAddress(ACCT_ID) | |
andBool (#rangeAddress(KID) | |
andBool (#rangeUInt(256, KID_balance) | |
andBool (#sizeByteArray(CD) <=Int 1250000000 | |
andBool (#notPrecompileAddress(ACCT_ID) | |
andBool (#notPrecompileAddress(KID) | |
andBool (ACCT_ID =/=Int KID | |
andBool (0 =/=Int KID | |
andBool (#newAddr(ACCT_ID, NONCE) ==Int KID | |
andBool (NONCE >Int 0 | |
andBool (VGas >=Int 3000000 | |
andBool (VCallDepth <Int 1024 | |
andBool ((VCallValue ==Int 0)))))))))))))) | |
endmodule |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment