The act looks like:
behaviour canCall-true of MkrAuthority
interface canCall(address src, address dst, bytes4 sig)
types
May : uint256
storage
wards[src] |-> May
iff
VCallValue == 0
if
(sig == 2646777772) or ((sig == 1086394137) and (May == 1))
returns 1
The generated spec is:
requires "../rules.k"
requires "../bin_runtime.k"
module 88FFFE422BD85DAE8B54766E152B4EA8003F01869FCA66E6FD177B87B5A8CEDA
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
imports BIN_RUNTIME
// MkrAuthority_canCall-true
rule [MkrAuthority.canCall-true.pass.rough]:
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> PETERSBURG </schedule>
<ethereum>
<evm>
<output> _ => #asByteStackInWidthaux(1, 31, 32, .WordStack) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<callStack> VCallStack </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
<callState>
<program> #asMapOpCodes(#dasmOpCodes(MkrAuthority_bin_runtime, PETERSBURG)) </program>
<programBytes> MkrAuthority_bin_runtime </programBytes>
<id> ACCT_ID </id>
<caller> CALLER_ID </caller>
<callData> #abiCallData("canCall", #address(ABI_src), #address(ABI_dst), #bytes4(ABI_sig)) ++ CD => _ </callData>
<callValue> VCallValue </callValue>
<wordStack> .WordStack => _ </wordStack>
<localMem> .Map => _ </localMem>
<pc> 0 => _ </pc>
<gas> VGas => _ </gas>
<memoryUsed> 0 => _ </memoryUsed>
<callGas> _ => _ </callGas>
<static> _ </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)
SetItem(1)
SetItem(2)
SetItem(3)
SetItem(4)
SetItem(5)
SetItem(6)
SetItem(7)
SetItem(8) _ </activeAccounts>
<accounts>
<account>
<acctID> ACCT_ID </acctID>
<balance> ACCT_ID_balance </balance>
<code> MkrAuthority_bin_runtime </code>
<storage>
.Map
[#MkrAuthority.wards[ABI_src] <- (May => May)]
_: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(ABI_src)
andBool (#rangeAddress(ABI_dst)
andBool (#rangeUInt(256, May)
andBool ((#sizeWordStack(CD) <=Int 1250000000)
andBool (((ABI_sig ==Int 2646777772) orBool ((ABI_sig ==Int 1086394137) andBool (May ==Int 1)))
andBool (VGas >=Int 3000000
andBool ((VCallValue ==Int 0))))))))
endmodule