Skip to content

Instantly share code, notes, and snippets.

@nrryuya

nrryuya/[ERC721]transferFrom-success-1-spec.k

Created December 16, 2018 02:52
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save nrryuya/a5d0eff3e37ad025326b1fd8e31bf10b to your computer and use it in GitHub Desktop.
Save nrryuya/a5d0eff3e37ad025326b1fd8e31bf10b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
[ERC721]transferFrom-success-1-spec.k
requires "abstract-semantics.k"
requires "verification.k"
module TRANSFERFROM-SUCCESS-1-SPEC
imports ETHEREUM-SIMULATION
imports ABSTRACT-SEMANTICS
imports VERIFICATION
// transferFrom-success-1
rule
<k> #execute => #halt </k>
<exit-code> 1 </exit-code>
<mode> NORMAL </mode>
<schedule> CONSTANTINOPLE </schedule>
<analysis> .Map </analysis> // not part of evm
<ethereum>
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
<callState>
<program> #asMapOpCodes(#dasmOpCodes(#parseByteStack("0x600035601c52740100000000000000000000000000000000000000006020526f7fffffffffffffffffffffffffffffff6040527fffffffffffffffffffffffffffffffff8000000000000000000000000000000060605274012a05f1fffffffffffffffffffffffffdabf41c006080527ffffffffffffffffffffffffed5fa0e000000000000000000000000000000000060a05263f175355060005114156100d057602060046101403734156100b457600080fd5b60056101405160e05260c052604060c0205460005260206000f3005b6370a08231600051141561013057602060046101403734156100f157600080fd5b600435602051811061010257600080fd5b50600061014051141561011457600080fd5b60026101405160e05260c052604060c0205460005260206000f3005b636352211e6000511415610186576020600461014037341561015157600080fd5b60006101405160e05260c052604060c0205461016052600061016051141561017857600080fd5b6101605160005260206000f3005b63081812fc60005114156101e257602060046101403734156101a757600080fd5b600060006101405160e05260c052604060c0205414156101c657600080fd5b60016101405160e05260c052604060c0205460005260206000f3005b63e985e9c56000511415610252576040600461014037341561020357600080fd5b600435602051811061021457600080fd5b50602435602051811061022657600080fd5b5060036101405160e05260c052604060c0206101605160e05260c052604060c0205460005260206000f3005b6000156102e5575b61018052610140526101605260006101605160e05260c052604060c020546101a052610140516101a051146101c05260016101605160e05260c052604060c0205461014051146101e05260036101a05160e05260c052604060c0206101405160e05260c052604060c0205461020052610200516101e0516101c0511717600052600051610180515650005b60001561035c575b61018052610140526101605260006101605160e05260c052604060c020541561031557600080fd5b6101405160006101605160e05260c052604060c0205560026101405160e05260c052604060c02080546001825401101561034e57600080fd5b600181540181555061018051565b6000156103d2575b6101805261014052610160526101405160006101605160e05260c052604060c020541461039057600080fd5b600060006101605160e05260c052604060c0205560026101405160e05260c052604060c0206001815410156103c457600080fd5b600181540381555061018051565b60001561043c575b6101805261014052610160526101405160006101605160e05260c052604060c020541461040657600080fd5b600060016101605160e05260c052604060c0205414151561043657600060016101605160e05260c052604060c020555b61018051565b60001561070b575b6101c0526101405261016052610180526101a0526101405161016051610180516101a0516101c051634cdc95496101e0526101a05161020052610180516102205261022051610200516006580161025a565b610280526101c0526101a052610180526101605261014052610280516104bb57600080fd5b60006101605114156104cc57600080fd5b6101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516391127c1f6102a052610140516102c052610180516102e0526102e0516102c051600658016103da565b61028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e0516103005161032051639260587e6103405261014051610360526101805161038052610380516103605160065801610364565b61032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e05161030051610320516103405161036051610380516103a0516103c05163ff5ce3786103e052610160516104005261018051610420526104205161040051600658016102ed565b6103c0526103a05261038052610360526103405261032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101805161016051610140517fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a46101c051565b6323b872dd60005114156107ac576060600461014037341561072c57600080fd5b600435602051811061073d57600080fd5b50602435602051811061074f57600080fd5b5061014051610160516101805163092863fe6101a052610140516101c052610160516101e0526101805161020052336102205261022051610200516101e0516101c05160065801610444565b610180526101605261014052600050005b6342842e0e60005114156107ea576000610600526106008051602001806101c0828460006004600a8704601201f16107e357600080fd5b5050610837565b63b88d4fde600051141561082f576104206064356004016101c03761040060643560040135111561081a57600080fd5b6104406064356004016101c037600050610837565b600015610abd575b6060600461014037341561084a57600080fd5b600435602051811061085b57600080fd5b50602435602051811061086d57600080fd5b506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e05161030051610320516103405161036051610380516103a0516103c0516103e05161040051610420516104405161046051610480516104a0516104c0516104e05161050051610520516105405161056051610580516105a0516105c0516105e051610600516106205163092863fe6106405261014051610660526101605161068052610180516106a052336106c0526106c0516106a051610680516106605160065801610444565b61062052610600526105e0526105c0526105a05261058052610560526105405261052052610500526104e0526104c0526104a05261048052610460526104405261042052610400526103e0526103c0526103a05261038052610360526103405261032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506000610160513b1315610abb57610160513b610a0b57600080fd5b61016051301415610a1b57600080fd5b6020610c406104a4608063150b7a026107405233610760526101405161078052610180516107a052806107c0526101c0808051602001808461076001828460006004600a8704601201f1610a6e57600080fd5b50508051820160206001820306601f820103905060200191505061075c9050610160515afa610a9c57600080fd5b600050610c40516107205263150b7a026107205114610aba57600080fd5b5b005b63095ea7b36000511415610bc05760406004610140373415610ade57600080fd5b6004356020518110610aef57600080fd5b5060006101605160e05260c052604060c02054610180526000610180511415610b1757600080fd5b61018051610140511415610b2a57600080fd5b3360006101605160e05260c052604060c02054146101a05260036101805160e05260c052604060c0203360e05260c052604060c020546101c0526101c0516101a05117610b7657600080fd5b6101405160016101605160e05260c052604060c020556101605161014051610180517f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b92560006000a4005b63a22cb4656000511415610c6c5760406004610140373415610be157600080fd5b6004356020518110610bf257600080fd5b5060243560028110610c0357600080fd5b5033610140511415610c1457600080fd5b6101605160033360e05260c052604060c0206101405160e05260c052604060c02055610160516101805261014051337f17307eab39ab6107e8899845ad3d59bd9653f200f220920489ca2b5937696c316020610180a3005b6340c10f196000511415610d375760406004610140373415610c8d57600080fd5b6004356020518110610c9e57600080fd5b506004543314610cad57600080fd5b6000610140511415610cbe57600080fd5b610140516101605163ff5ce37861018052610140516101a052610160516101c0526101c0516101a051600658016102ed565b6101605261014052600050610160516101405160007fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a4600160005260206000f3005b6342966c686000511415610ef35760206004610140373415610d5857600080fd5b61014051634cdc9549610160523361018052610140516101a0526101a051610180516006580161025a565b610200526101405261020051610d9857600080fd5b60006101405160e05260c052604060c02054610220526000610220511415610dbf57600080fd5b6101405161016051610180516101a0516101c0516101e05161020051610220516391127c1f61024052610220516102605261014051610280526102805161026051600658016103da565b61022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c051639260587e6102e05261022051610300526101405161032052610320516103005160065801610364565b6102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a052610180526101605261014052600050610140516000610220517fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a4005b60006000fd"), CONSTANTINOPLE)) </program>
<programBytes> #parseByteStack("0x600035601c52740100000000000000000000000000000000000000006020526f7fffffffffffffffffffffffffffffff6040527fffffffffffffffffffffffffffffffff8000000000000000000000000000000060605274012a05f1fffffffffffffffffffffffffdabf41c006080527ffffffffffffffffffffffffed5fa0e000000000000000000000000000000000060a05263f175355060005114156100d057602060046101403734156100b457600080fd5b60056101405160e05260c052604060c0205460005260206000f3005b6370a08231600051141561013057602060046101403734156100f157600080fd5b600435602051811061010257600080fd5b50600061014051141561011457600080fd5b60026101405160e05260c052604060c0205460005260206000f3005b636352211e6000511415610186576020600461014037341561015157600080fd5b60006101405160e05260c052604060c0205461016052600061016051141561017857600080fd5b6101605160005260206000f3005b63081812fc60005114156101e257602060046101403734156101a757600080fd5b600060006101405160e05260c052604060c0205414156101c657600080fd5b60016101405160e05260c052604060c0205460005260206000f3005b63e985e9c56000511415610252576040600461014037341561020357600080fd5b600435602051811061021457600080fd5b50602435602051811061022657600080fd5b5060036101405160e05260c052604060c0206101605160e05260c052604060c0205460005260206000f3005b6000156102e5575b61018052610140526101605260006101605160e05260c052604060c020546101a052610140516101a051146101c05260016101605160e05260c052604060c0205461014051146101e05260036101a05160e05260c052604060c0206101405160e05260c052604060c0205461020052610200516101e0516101c0511717600052600051610180515650005b60001561035c575b61018052610140526101605260006101605160e05260c052604060c020541561031557600080fd5b6101405160006101605160e05260c052604060c0205560026101405160e05260c052604060c02080546001825401101561034e57600080fd5b600181540181555061018051565b6000156103d2575b6101805261014052610160526101405160006101605160e05260c052604060c020541461039057600080fd5b600060006101605160e05260c052604060c0205560026101405160e05260c052604060c0206001815410156103c457600080fd5b600181540381555061018051565b60001561043c575b6101805261014052610160526101405160006101605160e05260c052604060c020541461040657600080fd5b600060016101605160e05260c052604060c0205414151561043657600060016101605160e05260c052604060c020555b61018051565b60001561070b575b6101c0526101405261016052610180526101a0526101405161016051610180516101a0516101c051634cdc95496101e0526101a05161020052610180516102205261022051610200516006580161025a565b610280526101c0526101a052610180526101605261014052610280516104bb57600080fd5b60006101605114156104cc57600080fd5b6101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516391127c1f6102a052610140516102c052610180516102e0526102e0516102c051600658016103da565b61028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e0516103005161032051639260587e6103405261014051610360526101805161038052610380516103605160065801610364565b61032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e05161030051610320516103405161036051610380516103a0516103c05163ff5ce3786103e052610160516104005261018051610420526104205161040051600658016102ed565b6103c0526103a05261038052610360526103405261032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101805161016051610140517fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a46101c051565b6323b872dd60005114156107ac576060600461014037341561072c57600080fd5b600435602051811061073d57600080fd5b50602435602051811061074f57600080fd5b5061014051610160516101805163092863fe6101a052610140516101c052610160516101e0526101805161020052336102205261022051610200516101e0516101c05160065801610444565b610180526101605261014052600050005b6342842e0e60005114156107ea576000610600526106008051602001806101c0828460006004600a8704601201f16107e357600080fd5b5050610837565b63b88d4fde600051141561082f576104206064356004016101c03761040060643560040135111561081a57600080fd5b6104406064356004016101c037600050610837565b600015610abd575b6060600461014037341561084a57600080fd5b600435602051811061085b57600080fd5b50602435602051811061086d57600080fd5b506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e05161030051610320516103405161036051610380516103a0516103c0516103e05161040051610420516104405161046051610480516104a0516104c0516104e05161050051610520516105405161056051610580516105a0516105c0516105e051610600516106205163092863fe6106405261014051610660526101605161068052610180516106a052336106c0526106c0516106a051610680516106605160065801610444565b61062052610600526105e0526105c0526105a05261058052610560526105405261052052610500526104e0526104c0526104a05261048052610460526104405261042052610400526103e0526103c0526103a05261038052610360526103405261032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506000610160513b1315610abb57610160513b610a0b57600080fd5b61016051301415610a1b57600080fd5b6020610c406104a4608063150b7a026107405233610760526101405161078052610180516107a052806107c0526101c0808051602001808461076001828460006004600a8704601201f1610a6e57600080fd5b50508051820160206001820306601f820103905060200191505061075c9050610160515afa610a9c57600080fd5b600050610c40516107205263150b7a026107205114610aba57600080fd5b5b005b63095ea7b36000511415610bc05760406004610140373415610ade57600080fd5b6004356020518110610aef57600080fd5b5060006101605160e05260c052604060c02054610180526000610180511415610b1757600080fd5b61018051610140511415610b2a57600080fd5b3360006101605160e05260c052604060c02054146101a05260036101805160e05260c052604060c0203360e05260c052604060c020546101c0526101c0516101a05117610b7657600080fd5b6101405160016101605160e05260c052604060c020556101605161014051610180517f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b92560006000a4005b63a22cb4656000511415610c6c5760406004610140373415610be157600080fd5b6004356020518110610bf257600080fd5b5060243560028110610c0357600080fd5b5033610140511415610c1457600080fd5b6101605160033360e05260c052604060c0206101405160e05260c052604060c02055610160516101805261014051337f17307eab39ab6107e8899845ad3d59bd9653f200f220920489ca2b5937696c316020610180a3005b6340c10f196000511415610d375760406004610140373415610c8d57600080fd5b6004356020518110610c9e57600080fd5b506004543314610cad57600080fd5b6000610140511415610cbe57600080fd5b610140516101605163ff5ce37861018052610140516101a052610160516101c0526101c0516101a051600658016102ed565b6101605261014052600050610160516101405160007fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a4600160005260206000f3005b6342966c686000511415610ef35760206004610140373415610d5857600080fd5b61014051634cdc9549610160523361018052610140516101a0526101a051610180516006580161025a565b610200526101405261020051610d9857600080fd5b60006101405160e05260c052604060c02054610220526000610220511415610dbf57600080fd5b6101405161016051610180516101a0516101c0516101e05161020051610220516391127c1f61024052610220516102605261014051610280526102805161026051600658016103da565b61022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c051639260587e6102e05261022051610300526101405161032052610320516103005160065801610364565b6102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a052610180526101605261014052600050610140516000610220517fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a4005b60006000fd") </programBytes>
<id> ACCT_ID </id> // contract owner
<caller> CALLER_ID </caller> // who called this contract; in the begining, origin // msg.sender
<callData> #abiCallData("transferFrom", #address(FROM_ID), #address(TO_ID), #uint256(TOKEN_ID)) </callData>
<callValue> 0 </callValue>
<wordStack> .WordStack => _ </wordStack>
<localMem> .Map => _ </localMem>
<pc> 0 => _ </pc>
<gas> 100000 => _ </gas>
<memoryUsed> 0 => _ </memoryUsed>
<previousGas> _ => _ </previousGas>
<static> false </static> // NOTE: non-static call
<callDepth> CALL_DEPTH </callDepth>
</callState>
<substate>
<selfDestruct> _ </selfDestruct>
<log> _:List ( .List => ListItem(#abiEventLog(ACCT_ID, "Transfer", #indexed(#address(FROM_ID)), #indexed(#address(TO_ID)), #indexed(#uint256(TOKEN_ID)))) ) </log>
<refund> _ </refund> // TODO: more detail
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin> // who fires tx
<previousHash> _ </previousHash>
<ommersHash> _ </ommersHash>
<coinbase> _ </coinbase>
<stateRoot> _ </stateRoot>
<transactionsRoot> _ </transactionsRoot>
<receiptsRoot> _ </receiptsRoot>
<logsBloom> _ </logsBloom>
<difficulty> _ </difficulty>
<number> _ </number>
<gasLimit> _ </gasLimit>
<gasUsed> _ </gasUsed>
<timestamp> _ </timestamp>
<extraData> _ </extraData>
<mixHash> _ </mixHash>
<blockNonce> _ </blockNonce>
<ommerBlockHeaders> _ </ommerBlockHeaders>
<blockhash> _ </blockhash>
</evm>
<network>
<activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
<accounts>
<account>
<acctID> ACCT_ID </acctID>
<balance> _ </balance>
<code> #parseByteStack("0x600035601c52740100000000000000000000000000000000000000006020526f7fffffffffffffffffffffffffffffff6040527fffffffffffffffffffffffffffffffff8000000000000000000000000000000060605274012a05f1fffffffffffffffffffffffffdabf41c006080527ffffffffffffffffffffffffed5fa0e000000000000000000000000000000000060a05263f175355060005114156100d057602060046101403734156100b457600080fd5b60056101405160e05260c052604060c0205460005260206000f3005b6370a08231600051141561013057602060046101403734156100f157600080fd5b600435602051811061010257600080fd5b50600061014051141561011457600080fd5b60026101405160e05260c052604060c0205460005260206000f3005b636352211e6000511415610186576020600461014037341561015157600080fd5b60006101405160e05260c052604060c0205461016052600061016051141561017857600080fd5b6101605160005260206000f3005b63081812fc60005114156101e257602060046101403734156101a757600080fd5b600060006101405160e05260c052604060c0205414156101c657600080fd5b60016101405160e05260c052604060c0205460005260206000f3005b63e985e9c56000511415610252576040600461014037341561020357600080fd5b600435602051811061021457600080fd5b50602435602051811061022657600080fd5b5060036101405160e05260c052604060c0206101605160e05260c052604060c0205460005260206000f3005b6000156102e5575b61018052610140526101605260006101605160e05260c052604060c020546101a052610140516101a051146101c05260016101605160e05260c052604060c0205461014051146101e05260036101a05160e05260c052604060c0206101405160e05260c052604060c0205461020052610200516101e0516101c0511717600052600051610180515650005b60001561035c575b61018052610140526101605260006101605160e05260c052604060c020541561031557600080fd5b6101405160006101605160e05260c052604060c0205560026101405160e05260c052604060c02080546001825401101561034e57600080fd5b600181540181555061018051565b6000156103d2575b6101805261014052610160526101405160006101605160e05260c052604060c020541461039057600080fd5b600060006101605160e05260c052604060c0205560026101405160e05260c052604060c0206001815410156103c457600080fd5b600181540381555061018051565b60001561043c575b6101805261014052610160526101405160006101605160e05260c052604060c020541461040657600080fd5b600060016101605160e05260c052604060c0205414151561043657600060016101605160e05260c052604060c020555b61018051565b60001561070b575b6101c0526101405261016052610180526101a0526101405161016051610180516101a0516101c051634cdc95496101e0526101a05161020052610180516102205261022051610200516006580161025a565b610280526101c0526101a052610180526101605261014052610280516104bb57600080fd5b60006101605114156104cc57600080fd5b6101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516391127c1f6102a052610140516102c052610180516102e0526102e0516102c051600658016103da565b61028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e0516103005161032051639260587e6103405261014051610360526101805161038052610380516103605160065801610364565b61032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e05161030051610320516103405161036051610380516103a0516103c05163ff5ce3786103e052610160516104005261018051610420526104205161040051600658016102ed565b6103c0526103a05261038052610360526103405261032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506101805161016051610140517fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a46101c051565b6323b872dd60005114156107ac576060600461014037341561072c57600080fd5b600435602051811061073d57600080fd5b50602435602051811061074f57600080fd5b5061014051610160516101805163092863fe6101a052610140516101c052610160516101e0526101805161020052336102205261022051610200516101e0516101c05160065801610444565b610180526101605261014052600050005b6342842e0e60005114156107ea576000610600526106008051602001806101c0828460006004600a8704601201f16107e357600080fd5b5050610837565b63b88d4fde600051141561082f576104206064356004016101c03761040060643560040135111561081a57600080fd5b6104406064356004016101c037600050610837565b600015610abd575b6060600461014037341561084a57600080fd5b600435602051811061085b57600080fd5b50602435602051811061086d57600080fd5b506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c0516102e05161030051610320516103405161036051610380516103a0516103c0516103e05161040051610420516104405161046051610480516104a0516104c0516104e05161050051610520516105405161056051610580516105a0516105c0516105e051610600516106205163092863fe6106405261014051610660526101605161068052610180516106a052336106c0526106c0516106a051610680516106605160065801610444565b61062052610600526105e0526105c0526105a05261058052610560526105405261052052610500526104e0526104c0526104a05261048052610460526104405261042052610400526103e0526103c0526103a05261038052610360526103405261032052610300526102e0526102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a0526101805261016052610140526000506000610160513b1315610abb57610160513b610a0b57600080fd5b61016051301415610a1b57600080fd5b6020610c406104a4608063150b7a026107405233610760526101405161078052610180516107a052806107c0526101c0808051602001808461076001828460006004600a8704601201f1610a6e57600080fd5b50508051820160206001820306601f820103905060200191505061075c9050610160515afa610a9c57600080fd5b600050610c40516107205263150b7a026107205114610aba57600080fd5b5b005b63095ea7b36000511415610bc05760406004610140373415610ade57600080fd5b6004356020518110610aef57600080fd5b5060006101605160e05260c052604060c02054610180526000610180511415610b1757600080fd5b61018051610140511415610b2a57600080fd5b3360006101605160e05260c052604060c02054146101a05260036101805160e05260c052604060c0203360e05260c052604060c020546101c0526101c0516101a05117610b7657600080fd5b6101405160016101605160e05260c052604060c020556101605161014051610180517f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b92560006000a4005b63a22cb4656000511415610c6c5760406004610140373415610be157600080fd5b6004356020518110610bf257600080fd5b5060243560028110610c0357600080fd5b5033610140511415610c1457600080fd5b6101605160033360e05260c052604060c0206101405160e05260c052604060c02055610160516101805261014051337f17307eab39ab6107e8899845ad3d59bd9653f200f220920489ca2b5937696c316020610180a3005b6340c10f196000511415610d375760406004610140373415610c8d57600080fd5b6004356020518110610c9e57600080fd5b506004543314610cad57600080fd5b6000610140511415610cbe57600080fd5b610140516101605163ff5ce37861018052610140516101a052610160516101c0526101c0516101a051600658016102ed565b6101605261014052600050610160516101405160007fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a4600160005260206000f3005b6342966c686000511415610ef35760206004610140373415610d5857600080fd5b61014051634cdc9549610160523361018052610140516101a0526101a051610180516006580161025a565b610200526101405261020051610d9857600080fd5b60006101405160e05260c052604060c02054610220526000610220511415610dbf57600080fd5b6101405161016051610180516101a0516101c0516101e05161020051610220516391127c1f61024052610220516102605261014051610280526102805161026051600658016103da565b61022052610200526101e0526101c0526101a0526101805261016052610140526000506101405161016051610180516101a0516101c0516101e05161020051610220516102405161026051610280516102a0516102c051639260587e6102e05261022051610300526101405161032052610320516103005160065801610364565b6102c0526102a05261028052610260526102405261022052610200526101e0526101c0526101a052610180526101605261014052600050610140516000610220517fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60006000a4005b60006000fd") </code>
<storage> #hashedLocation("Vyper", 0, TOKEN_ID) |-> (OWNER => TO_ID)
#hashedLocation("Vyper", 1, TOKEN_ID) |-> (APPROVED => 0)
#hashedLocation("Vyper", 3, OWNER CALLER_ID) |-> ISAPPROVED
#hashedLocation("Vyper", 2, OWNER) |-> (OWNER_BAL => OWNER_BAL -Int 1)
#hashedLocation("Vyper", 2, TO_ID) |-> (TO_BAL => TO_BAL +Int 1)
_:Map </storage>
<origStorage> #hashedLocation("Vyper", 0, TOKEN_ID) |-> OWNER
#hashedLocation("Vyper", 1, TOKEN_ID) |-> APPROVED
#hashedLocation("Vyper", 3, OWNER CALLER_ID) |-> ISAPPROVED
#hashedLocation("Vyper", 2, OWNER) |-> OWNER_BAL
#hashedLocation("Vyper", 2, TO_ID) |-> TO_BAL
_:Map </origStorage>
<nonce> _ </nonce>
</account>
// ... // TODO: fix
</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 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
andBool #rangeUInt(256, TOKEN_ID)
andBool #rangeAddress(FROM_ID)
andBool #rangeAddress(TO_ID)
andBool #rangeAddress(OWNER)
andBool #rangeAddress(APPROVED)
andBool 0 <=Int ISAPPROVED andBool ISAPPROVED <=Int 1
andBool #rangeUInt(256, OWNER_BAL)
andBool #rangeUInt(256, TO_BAL)
andBool (CALLER_ID ==Int OWNER orBool CALLER_ID ==Int APPROVED orBool ISAPPROVED ==Int 1)
andBool FROM_ID ==Int OWNER
andBool TO_ID =/=Int 0
andBool OWNER =/=Int 0
andBool FROM_ID =/=Int TO_ID
andBool 0 <=Int (OWNER_BAL -Int 1)
andBool (TO_BAL +Int 1) <Int (2 ^Int 256)
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment