From 9fbf4e9fbc2c7eed899eab8ab813c4cef45b4ee5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Aug 2024 14:00:08 +0000 Subject: [PATCH 1/8] tests/specs/examples: replace symbol(), klabel(X) with symbol(X) --- tests/specs/examples/erc20-bin-runtime.k | 34 +-- tests/specs/examples/erc721-bin-runtime.k | 42 +-- tests/specs/examples/storage-bin-runtime.k | 282 ++++++++++----------- 3 files changed, 179 insertions(+), 179 deletions(-) diff --git a/tests/specs/examples/erc20-bin-runtime.k b/tests/specs/examples/erc20-bin-runtime.k index 2c37f00a6f..c04a3ab0fa 100644 --- a/tests/specs/examples/erc20-bin-runtime.k +++ b/tests/specs/examples/erc20-bin-runtime.k @@ -5,24 +5,24 @@ module ERC20-CONTRACT syntax Contract ::= S2KERC20Contract - syntax S2KERC20Contract ::= "S2KERC20" [symbol(), klabel(contract_ERC20)] + syntax S2KERC20Contract ::= "S2KERC20" [symbol(contract_ERC20)] rule ( #binRuntime ( S2KERC20 ) => #parseByteStack ( "0x608060405234801561001057600080fd5b50600436106100935760003560e01c8063313ce56711610066578063313ce5671461013457806370a082311461015257806395d89b4114610182578063a9059cbb146101a0578063dd62ed3e146101d057610093565b806306fdde0314610098578063095ea7b3146100b657806318160ddd146100e657806323b872dd14610104575b600080fd5b6100a0610200565b6040516100ad919061098b565b60405180910390f35b6100d060048036038101906100cb9190610a46565b610292565b6040516100dd9190610aa1565b60405180910390f35b6100ee6102a9565b6040516100fb9190610acb565b60405180910390f35b61011e60048036038101906101199190610ae6565b6102b3565b60405161012b9190610aa1565b60405180910390f35b61013c6103a6565b6040516101499190610acb565b60405180910390f35b61016c60048036038101906101679190610b39565b6103c0565b6040516101799190610acb565b60405180910390f35b61018a610408565b604051610197919061098b565b60405180910390f35b6101ba60048036038101906101b59190610a46565b61049a565b6040516101c79190610aa1565b60405180910390f35b6101ea60048036038101906101e59190610b66565b6104b1565b6040516101f79190610acb565b60405180910390f35b60606004805461020f90610bd5565b80601f016020809104026020016040519081016040528092919081815260200182805461023b90610bd5565b80156102885780601f1061025d57610100808354040283529160200191610288565b820191906000526020600020905b81548152906001019060200180831161026b57829003601f168201915b5050505050905090565b600061029f338484610538565b6001905092915050565b6000600254905090565b60006102c084848461069c565b6000600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905082811015610384576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161037b90610c78565b60405180910390fd5b61039a853385846103959190610cc7565b610538565b60019150509392505050565b6000600360009054906101000a900460ff1660ff16905090565b60008060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b60606005805461041790610bd5565b80601f016020809104026020016040519081016040528092919081815260200182805461044390610bd5565b80156104905780601f1061046557610100808354040283529160200191610490565b820191906000526020600020905b81548152906001019060200180831161047357829003601f168201915b5050505050905090565b60006104a733848461069c565b6001905092915050565b6000600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905092915050565b600073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff16036105a7576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161059e90610d6d565b60405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff1603610616576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161060d90610dff565b60405180910390fd5b80600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550505050565b600073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff160361070b576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161070290610e91565b60405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff160361077a576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161077190610f23565b60405180910390fd5b60008060008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905060008060008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905082811015610843576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161083a90610fb5565b60405180910390fd5b600083826108519190610cc7565b9050600084846108619190610fd5565b9050816000808973ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550806000808873ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555050505050505050565b600081519050919050565b600082825260208201905092915050565b60005b8381101561092c578082015181840152602081019050610911565b8381111561093b576000848401525b50505050565b6000601f19601f8301169050919050565b600061095d826108f2565b61096781856108fd565b935061097781856020860161090e565b61098081610941565b840191505092915050565b600060208201905081810360008301526109a58184610952565b905092915050565b600080fd5b600073ffffffffffffffffffffffffffffffffffffffff82169050919050565b60006109dd826109b2565b9050919050565b6109ed816109d2565b81146109f857600080fd5b50565b600081359050610a0a816109e4565b92915050565b6000819050919050565b610a2381610a10565b8114610a2e57600080fd5b50565b600081359050610a4081610a1a565b92915050565b60008060408385031215610a5d57610a5c6109ad565b5b6000610a6b858286016109fb565b9250506020610a7c85828601610a31565b9150509250929050565b60008115159050919050565b610a9b81610a86565b82525050565b6000602082019050610ab66000830184610a92565b92915050565b610ac581610a10565b82525050565b6000602082019050610ae06000830184610abc565b92915050565b600080600060608486031215610aff57610afe6109ad565b5b6000610b0d868287016109fb565b9350506020610b1e868287016109fb565b9250506040610b2f86828701610a31565b9150509250925092565b600060208284031215610b4f57610b4e6109ad565b5b6000610b5d848285016109fb565b91505092915050565b60008060408385031215610b7d57610b7c6109ad565b5b6000610b8b858286016109fb565b9250506020610b9c858286016109fb565b9150509250929050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052602260045260246000fd5b60006002820490506001821680610bed57607f821691505b602082108103610c0057610bff610ba6565b5b50919050565b7f45524332303a207472616e7366657220616d6f756e742065786365656473206160008201527f6c6c6f77616e6365000000000000000000000000000000000000000000000000602082015250565b6000610c626028836108fd565b9150610c6d82610c06565b604082019050919050565b60006020820190508181036000830152610c9181610c55565b9050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b6000610cd282610a10565b9150610cdd83610a10565b925082821015610cf057610cef610c98565b5b828203905092915050565b7f45524332303a20617070726f76652066726f6d20746865207a65726f2061646460008201527f7265737300000000000000000000000000000000000000000000000000000000602082015250565b6000610d576024836108fd565b9150610d6282610cfb565b604082019050919050565b60006020820190508181036000830152610d8681610d4a565b9050919050565b7f45524332303a20617070726f766520746f20746865207a65726f20616464726560008201527f7373000000000000000000000000000000000000000000000000000000000000602082015250565b6000610de96022836108fd565b9150610df482610d8d565b604082019050919050565b60006020820190508181036000830152610e1881610ddc565b9050919050565b7f45524332303a207472616e736665722066726f6d20746865207a65726f20616460008201527f6472657373000000000000000000000000000000000000000000000000000000602082015250565b6000610e7b6025836108fd565b9150610e8682610e1f565b604082019050919050565b60006020820190508181036000830152610eaa81610e6e565b9050919050565b7f45524332303a207472616e7366657220746f20746865207a65726f206164647260008201527f6573730000000000000000000000000000000000000000000000000000000000602082015250565b6000610f0d6023836108fd565b9150610f1882610eb1565b604082019050919050565b60006020820190508181036000830152610f3c81610f00565b9050919050565b7f45524332303a207472616e7366657220616d6f756e742065786365656473206260008201527f616c616e63650000000000000000000000000000000000000000000000000000602082015250565b6000610f9f6026836108fd565b9150610faa82610f43565b604082019050919050565b60006020820190508181036000830152610fce81610f92565b9050919050565b6000610fe082610a10565b9150610feb83610a10565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156110205761101f610c98565b5b82820190509291505056fea2646970667358221220f0099f9a0198681f813e72904e1ac296b2e55f71057febf64d98a19b63dfc0c564736f6c634300080d0033" ) ) syntax Field ::= ERC20Field - syntax ERC20Field ::= "_balances" [symbol(), klabel(field_ERC20__balances)] + syntax ERC20Field ::= "_balances" [symbol(field_ERC20__balances)] - syntax ERC20Field ::= "_allowances" [symbol(), klabel(field_ERC20__allowances)] + syntax ERC20Field ::= "_allowances" [symbol(field_ERC20__allowances)] - syntax ERC20Field ::= "_totalSupply" [symbol(), klabel(field_ERC20__totalSupply)] + syntax ERC20Field ::= "_totalSupply" [symbol(field_ERC20__totalSupply)] - syntax ERC20Field ::= "_decimals" [symbol(), klabel(field_ERC20__decimals)] + syntax ERC20Field ::= "_decimals" [symbol(field_ERC20__decimals)] - syntax ERC20Field ::= "_name" [symbol(), klabel(field_ERC20__name)] + syntax ERC20Field ::= "_name" [symbol(field_ERC20__name)] - syntax ERC20Field ::= "_symbol" [symbol(), klabel(field_ERC20__symbol)] + syntax ERC20Field ::= "_symbol" [symbol(field_ERC20__symbol)] rule ( #loc ( S2KERC20 . _balances ) => 0 ) @@ -42,25 +42,25 @@ module ERC20-CONTRACT rule ( #loc ( S2KERC20 . _symbol ) => 5 ) - syntax Bytes ::= S2KERC20Contract "." S2KERC20Method [function(), symbol(), klabel(method_ERC20)] + syntax Bytes ::= S2KERC20Contract "." S2KERC20Method [function(), symbol(method_ERC20)] - syntax S2KERC20Method ::= "S2Kallowance" "(" Int ":" "address" "," Int ":" "address" ")" [symbol(), klabel(method_ERC20_S2Kallowance_address_address)] + syntax S2KERC20Method ::= "S2Kallowance" "(" Int ":" "address" "," Int ":" "address" ")" [symbol(method_ERC20_S2Kallowance_address_address)] - syntax S2KERC20Method ::= "S2Kapprove" "(" Int ":" "address" "," Int ":" "uint256" ")" [symbol(), klabel(method_ERC20_S2Kapprove_address_uint256)] + syntax S2KERC20Method ::= "S2Kapprove" "(" Int ":" "address" "," Int ":" "uint256" ")" [symbol(method_ERC20_S2Kapprove_address_uint256)] - syntax S2KERC20Method ::= "S2KbalanceOf" "(" Int ":" "address" ")" [symbol(), klabel(method_ERC20_S2KbalanceOf_address)] + syntax S2KERC20Method ::= "S2KbalanceOf" "(" Int ":" "address" ")" [symbol(method_ERC20_S2KbalanceOf_address)] - syntax S2KERC20Method ::= "S2Kdecimals" "(" ")" [symbol(), klabel(method_ERC20_S2Kdecimals_)] + syntax S2KERC20Method ::= "S2Kdecimals" "(" ")" [symbol(method_ERC20_S2Kdecimals_)] - syntax S2KERC20Method ::= "S2Kname" "(" ")" [symbol(), klabel(method_ERC20_S2Kname_)] + syntax S2KERC20Method ::= "S2Kname" "(" ")" [symbol(method_ERC20_S2Kname_)] - syntax S2KERC20Method ::= "S2Ksymbol" "(" ")" [symbol(), klabel(method_ERC20_S2Ksymbol_)] + syntax S2KERC20Method ::= "S2Ksymbol" "(" ")" [symbol(method_ERC20_S2Ksymbol_)] - syntax S2KERC20Method ::= "S2KtotalSupply" "(" ")" [symbol(), klabel(method_ERC20_S2KtotalSupply_)] + syntax S2KERC20Method ::= "S2KtotalSupply" "(" ")" [symbol(method_ERC20_S2KtotalSupply_)] - syntax S2KERC20Method ::= "S2Ktransfer" "(" Int ":" "address" "," Int ":" "uint256" ")" [symbol(), klabel(method_ERC20_S2Ktransfer_address_uint256)] + syntax S2KERC20Method ::= "S2Ktransfer" "(" Int ":" "address" "," Int ":" "uint256" ")" [symbol(method_ERC20_S2Ktransfer_address_uint256)] - syntax S2KERC20Method ::= "S2KtransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" ")" [symbol(), klabel(method_ERC20_S2KtransferFrom_address_address_uint256)] + syntax S2KERC20Method ::= "S2KtransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" ")" [symbol(method_ERC20_S2KtransferFrom_address_address_uint256)] rule ( S2KERC20 . S2Kallowance ( V0_owner : address , V1_spender : address ) => #abiCallData ( "allowance" , #address ( V0_owner ) , #address ( V1_spender ) , .TypedArgs ) ) ensures ( #rangeAddress ( V0_owner ) diff --git a/tests/specs/examples/erc721-bin-runtime.k b/tests/specs/examples/erc721-bin-runtime.k index 65c6c8b837..ad3b4f5db9 100644 --- a/tests/specs/examples/erc721-bin-runtime.k +++ b/tests/specs/examples/erc721-bin-runtime.k @@ -5,24 +5,24 @@ module ERC721-CONTRACT syntax Contract ::= S2KERC721Contract - syntax S2KERC721Contract ::= "S2KERC721" [symbol(), klabel(contract_ERC721)] + syntax S2KERC721Contract ::= "S2KERC721" [symbol(contract_ERC721)] rule ( #binRuntime ( S2KERC721 ) => #parseByteStack ( "0x608060405234801561001057600080fd5b50600436106100cf5760003560e01c80636352211e1161008c578063a22cb46511610066578063a22cb46514610224578063b88d4fde14610240578063c87b56dd1461025c578063e985e9c51461028c576100cf565b80636352211e146101a657806370a08231146101d657806395d89b4114610206576100cf565b806301ffc9a7146100d457806306fdde0314610104578063081812fc14610122578063095ea7b31461015257806323b872dd1461016e57806342842e0e1461018a575b600080fd5b6100ee60048036038101906100e99190611433565b6102bc565b6040516100fb919061147b565b60405180910390f35b61010c61039e565b604051610119919061152f565b60405180910390f35b61013c60048036038101906101379190611587565b610430565b60405161014991906115f5565b60405180910390f35b61016c6004803603810190610167919061163c565b6104b5565b005b6101886004803603810190610183919061167c565b6105cc565b005b6101a4600480360381019061019f919061167c565b61062c565b005b6101c060048036038101906101bb9190611587565b61064c565b6040516101cd91906115f5565b60405180910390f35b6101f060048036038101906101eb91906116cf565b6106fd565b6040516101fd919061170b565b60405180910390f35b61020e6107b4565b60405161021b919061152f565b60405180910390f35b61023e60048036038101906102399190611752565b610846565b005b61025a600480360381019061025591906118c7565b61085c565b005b61027660048036038101906102719190611587565b6108be565b604051610283919061152f565b60405180910390f35b6102a660048036038101906102a1919061194a565b610965565b6040516102b3919061147b565b60405180910390f35b60007f80ac58cd000000000000000000000000000000000000000000000000000000007bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916148061038757507f5b5e139f000000000000000000000000000000000000000000000000000000007bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916145b806103975750610396826109f9565b5b9050919050565b6060600080546103ad906119b9565b80601f01602080910402602001604051908101604052809291908181526020018280546103d9906119b9565b80156104265780601f106103fb57610100808354040283529160200191610426565b820191906000526020600020905b81548152906001019060200180831161040957829003601f168201915b5050505050905090565b600061043b82610a63565b61047a576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161047190611a5c565b60405180910390fd5b6004600083815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff169050919050565b60006104c08261064c565b90508073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff1603610530576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161052790611aee565b60405180910390fd5b8073ffffffffffffffffffffffffffffffffffffffff1661054f610acf565b73ffffffffffffffffffffffffffffffffffffffff16148061057e575061057d81610578610acf565b610965565b5b6105bd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016105b490611b80565b60405180910390fd5b6105c78383610ad7565b505050565b6105dd6105d7610acf565b82610b90565b61061c576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161061390611c12565b60405180910390fd5b610627838383610c6e565b505050565b6106478383836040518060200160405280600081525061085c565b505050565b6000806002600084815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff169050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff16036106f4576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016106eb90611ca4565b60405180910390fd5b80915050919050565b60008073ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff160361076d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161076490611d36565b60405180910390fd5b600360008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b6060600180546107c3906119b9565b80601f01602080910402602001604051908101604052809291908181526020018280546107ef906119b9565b801561083c5780601f106108115761010080835404028352916020019161083c565b820191906000526020600020905b81548152906001019060200180831161081f57829003601f168201915b5050505050905090565b610858610851610acf565b8383610ed4565b5050565b61086d610867610acf565b83610b90565b6108ac576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016108a390611c12565b60405180910390fd5b6108b884848484611040565b50505050565b60606108c982610a63565b610908576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016108ff90611dc8565b60405180910390fd5b600061091261109c565b90506000815111610932576040518060200160405280600081525061095d565b8061093c846110b3565b60405160200161094d929190611e24565b6040516020818303038152906040525b915050919050565b6000600560008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060009054906101000a900460ff16905092915050565b60007f01ffc9a7000000000000000000000000000000000000000000000000000000007bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916149050919050565b60008073ffffffffffffffffffffffffffffffffffffffff166002600084815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1614159050919050565b600033905090565b816004600083815260200190815260200160002060006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550808273ffffffffffffffffffffffffffffffffffffffff16610b4a8361064c565b73ffffffffffffffffffffffffffffffffffffffff167f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b92560405160405180910390a45050565b6000610b9b82610a63565b610bda576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610bd190611eba565b60405180910390fd5b6000610be58361064c565b90508073ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff161480610c5457508373ffffffffffffffffffffffffffffffffffffffff16610c3c84610430565b73ffffffffffffffffffffffffffffffffffffffff16145b80610c655750610c648185610965565b5b91505092915050565b8273ffffffffffffffffffffffffffffffffffffffff16610c8e8261064c565b73ffffffffffffffffffffffffffffffffffffffff1614610ce4576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610cdb90611f4c565b60405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff1603610d53576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610d4a90611fde565b60405180910390fd5b610d5e838383611213565b610d69600082610ad7565b6001600360008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254610db9919061202d565b925050819055506001600360008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254610e109190612061565b92505081905550816002600083815260200190815260200160002060006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550808273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60405160405180910390a4610ecf838383611218565b505050565b8173ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff1603610f42576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610f3990612103565b60405180910390fd5b80600560008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060006101000a81548160ff0219169083151502179055508173ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff167f17307eab39ab6107e8899845ad3d59bd9653f200f220920489ca2b5937696c3183604051611033919061147b565b60405180910390a3505050565b61104b848484610c6e565b6110578484848461121d565b611096576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161108d90612195565b60405180910390fd5b50505050565b606060405180602001604052806000815250905090565b6060600082036110fa576040518060400160405280600181526020017f3000000000000000000000000000000000000000000000000000000000000000815250905061120e565b600082905060005b6000821461112c578080611115906121b5565b915050600a82611125919061222c565b9150611102565b60008167ffffffffffffffff8111156111485761114761179c565b5b6040519080825280601f01601f19166020018201604052801561117a5781602001600182028036833780820191505090505b5090505b6000851461120757600182611193919061202d565b9150600a856111a2919061225d565b60306111ae9190612061565b60f81b8183815181106111c4576111c361228e565b5b60200101907effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916908160001a905350600a85611200919061222c565b945061117e565b8093505050505b919050565b505050565b505050565b600061123e8473ffffffffffffffffffffffffffffffffffffffff166113a4565b15611397578373ffffffffffffffffffffffffffffffffffffffff1663150b7a02611267610acf565b8786866040518563ffffffff1660e01b81526004016112899493929190612312565b6020604051808303816000875af19250505080156112c557506040513d601f19601f820116820180604052508101906112c29190612373565b60015b611347573d80600081146112f5576040519150601f19603f3d011682016040523d82523d6000602084013e6112fa565b606091505b50600081510361133f576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161133690612195565b60405180910390fd5b805181602001fd5b63150b7a0260e01b7bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1916817bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19161491505061139c565b600190505b949350505050565b6000808273ffffffffffffffffffffffffffffffffffffffff163b119050919050565b6000604051905090565b600080fd5b600080fd5b60007fffffffff0000000000000000000000000000000000000000000000000000000082169050919050565b611410816113db565b811461141b57600080fd5b50565b60008135905061142d81611407565b92915050565b600060208284031215611449576114486113d1565b5b60006114578482850161141e565b91505092915050565b60008115159050919050565b61147581611460565b82525050565b6000602082019050611490600083018461146c565b92915050565b600081519050919050565b600082825260208201905092915050565b60005b838110156114d05780820151818401526020810190506114b5565b838111156114df576000848401525b50505050565b6000601f19601f8301169050919050565b600061150182611496565b61150b81856114a1565b935061151b8185602086016114b2565b611524816114e5565b840191505092915050565b6000602082019050818103600083015261154981846114f6565b905092915050565b6000819050919050565b61156481611551565b811461156f57600080fd5b50565b6000813590506115818161155b565b92915050565b60006020828403121561159d5761159c6113d1565b5b60006115ab84828501611572565b91505092915050565b600073ffffffffffffffffffffffffffffffffffffffff82169050919050565b60006115df826115b4565b9050919050565b6115ef816115d4565b82525050565b600060208201905061160a60008301846115e6565b92915050565b611619816115d4565b811461162457600080fd5b50565b60008135905061163681611610565b92915050565b60008060408385031215611653576116526113d1565b5b600061166185828601611627565b925050602061167285828601611572565b9150509250929050565b600080600060608486031215611695576116946113d1565b5b60006116a386828701611627565b93505060206116b486828701611627565b92505060406116c586828701611572565b9150509250925092565b6000602082840312156116e5576116e46113d1565b5b60006116f384828501611627565b91505092915050565b61170581611551565b82525050565b600060208201905061172060008301846116fc565b92915050565b61172f81611460565b811461173a57600080fd5b50565b60008135905061174c81611726565b92915050565b60008060408385031215611769576117686113d1565b5b600061177785828601611627565b92505060206117888582860161173d565b9150509250929050565b600080fd5b600080fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052604160045260246000fd5b6117d4826114e5565b810181811067ffffffffffffffff821117156117f3576117f261179c565b5b80604052505050565b60006118066113c7565b905061181282826117cb565b919050565b600067ffffffffffffffff8211156118325761183161179c565b5b61183b826114e5565b9050602081019050919050565b82818337600083830152505050565b600061186a61186584611817565b6117fc565b90508281526020810184848401111561188657611885611797565b5b611891848285611848565b509392505050565b600082601f8301126118ae576118ad611792565b5b81356118be848260208601611857565b91505092915050565b600080600080608085870312156118e1576118e06113d1565b5b60006118ef87828801611627565b945050602061190087828801611627565b935050604061191187828801611572565b925050606085013567ffffffffffffffff811115611932576119316113d6565b5b61193e87828801611899565b91505092959194509250565b60008060408385031215611961576119606113d1565b5b600061196f85828601611627565b925050602061198085828601611627565b9150509250929050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052602260045260246000fd5b600060028204905060018216806119d157607f821691505b6020821081036119e4576119e361198a565b5b50919050565b7f4552433732313a20617070726f76656420717565727920666f72206e6f6e657860008201527f697374656e7420746f6b656e0000000000000000000000000000000000000000602082015250565b6000611a46602c836114a1565b9150611a51826119ea565b604082019050919050565b60006020820190508181036000830152611a7581611a39565b9050919050565b7f4552433732313a20617070726f76616c20746f2063757272656e74206f776e6560008201527f7200000000000000000000000000000000000000000000000000000000000000602082015250565b6000611ad86021836114a1565b9150611ae382611a7c565b604082019050919050565b60006020820190508181036000830152611b0781611acb565b9050919050565b7f4552433732313a20617070726f76652063616c6c6572206973206e6f74206f7760008201527f6e6572206e6f7220617070726f76656420666f7220616c6c0000000000000000602082015250565b6000611b6a6038836114a1565b9150611b7582611b0e565b604082019050919050565b60006020820190508181036000830152611b9981611b5d565b9050919050565b7f4552433732313a207472616e736665722063616c6c6572206973206e6f74206f60008201527f776e6572206e6f7220617070726f766564000000000000000000000000000000602082015250565b6000611bfc6031836114a1565b9150611c0782611ba0565b604082019050919050565b60006020820190508181036000830152611c2b81611bef565b9050919050565b7f4552433732313a206f776e657220717565727920666f72206e6f6e657869737460008201527f656e7420746f6b656e0000000000000000000000000000000000000000000000602082015250565b6000611c8e6029836114a1565b9150611c9982611c32565b604082019050919050565b60006020820190508181036000830152611cbd81611c81565b9050919050565b7f4552433732313a2062616c616e636520717565727920666f7220746865207a6560008201527f726f206164647265737300000000000000000000000000000000000000000000602082015250565b6000611d20602a836114a1565b9150611d2b82611cc4565b604082019050919050565b60006020820190508181036000830152611d4f81611d13565b9050919050565b7f4552433732314d657461646174613a2055524920717565727920666f72206e6f60008201527f6e6578697374656e7420746f6b656e0000000000000000000000000000000000602082015250565b6000611db2602f836114a1565b9150611dbd82611d56565b604082019050919050565b60006020820190508181036000830152611de181611da5565b9050919050565b600081905092915050565b6000611dfe82611496565b611e088185611de8565b9350611e188185602086016114b2565b80840191505092915050565b6000611e308285611df3565b9150611e3c8284611df3565b91508190509392505050565b7f4552433732313a206f70657261746f7220717565727920666f72206e6f6e657860008201527f697374656e7420746f6b656e0000000000000000000000000000000000000000602082015250565b6000611ea4602c836114a1565b9150611eaf82611e48565b604082019050919050565b60006020820190508181036000830152611ed381611e97565b9050919050565b7f4552433732313a207472616e736665722066726f6d20696e636f72726563742060008201527f6f776e6572000000000000000000000000000000000000000000000000000000602082015250565b6000611f366025836114a1565b9150611f4182611eda565b604082019050919050565b60006020820190508181036000830152611f6581611f29565b9050919050565b7f4552433732313a207472616e7366657220746f20746865207a65726f2061646460008201527f7265737300000000000000000000000000000000000000000000000000000000602082015250565b6000611fc86024836114a1565b9150611fd382611f6c565b604082019050919050565b60006020820190508181036000830152611ff781611fbb565b9050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b600061203882611551565b915061204383611551565b92508282101561205657612055611ffe565b5b828203905092915050565b600061206c82611551565b915061207783611551565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156120ac576120ab611ffe565b5b828201905092915050565b7f4552433732313a20617070726f766520746f2063616c6c657200000000000000600082015250565b60006120ed6019836114a1565b91506120f8826120b7565b602082019050919050565b6000602082019050818103600083015261211c816120e0565b9050919050565b7f4552433732313a207472616e7366657220746f206e6f6e20455243373231526560008201527f63656976657220696d706c656d656e7465720000000000000000000000000000602082015250565b600061217f6032836114a1565b915061218a82612123565b604082019050919050565b600060208201905081810360008301526121ae81612172565b9050919050565b60006121c082611551565b91507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff82036121f2576121f1611ffe565b5b600182019050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b600061223782611551565b915061224283611551565b925082612252576122516121fd565b5b828204905092915050565b600061226882611551565b915061227383611551565b925082612283576122826121fd565b5b828206905092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b600081519050919050565b600082825260208201905092915050565b60006122e4826122bd565b6122ee81856122c8565b93506122fe8185602086016114b2565b612307816114e5565b840191505092915050565b600060808201905061232760008301876115e6565b61233460208301866115e6565b61234160408301856116fc565b818103606083015261235381846122d9565b905095945050505050565b60008151905061236d81611407565b92915050565b600060208284031215612389576123886113d1565b5b60006123978482850161235e565b9150509291505056fea2646970667358221220376610b0c4cb4eebd2681c826bc639cd81500f4f2fbdb98cfefb31572fe03af964736f6c634300080d0033" ) ) syntax Field ::= ERC721Field - syntax ERC721Field ::= "_name" [symbol(), klabel(field_ERC721__name)] + syntax ERC721Field ::= "_name" [symbol(field_ERC721__name)] - syntax ERC721Field ::= "_symbol" [symbol(), klabel(field_ERC721__symbol)] + syntax ERC721Field ::= "_symbol" [symbol(field_ERC721__symbol)] - syntax ERC721Field ::= "_owners" [symbol(), klabel(field_ERC721__owners)] + syntax ERC721Field ::= "_owners" [symbol(field_ERC721__owners)] - syntax ERC721Field ::= "_balances" [symbol(), klabel(field_ERC721__balances)] + syntax ERC721Field ::= "_balances" [symbol(field_ERC721__balances)] - syntax ERC721Field ::= "_tokenApprovals" [symbol(), klabel(field_ERC721__tokenApprovals)] + syntax ERC721Field ::= "_tokenApprovals" [symbol(field_ERC721__tokenApprovals)] - syntax ERC721Field ::= "_operatorApprovals" [symbol(), klabel(field_ERC721__operatorApprovals)] + syntax ERC721Field ::= "_operatorApprovals" [symbol(field_ERC721__operatorApprovals)] rule ( #loc ( S2KERC721 . _name ) => 0 ) @@ -42,33 +42,33 @@ module ERC721-CONTRACT rule ( #loc ( S2KERC721 . _operatorApprovals ) => 5 ) - syntax Bytes ::= S2KERC721Contract "." S2KERC721Method [function(), symbol(), klabel(method_ERC721)] + syntax Bytes ::= S2KERC721Contract "." S2KERC721Method [function(), symbol(method_ERC721)] - syntax S2KERC721Method ::= "S2Kapprove" "(" Int ":" "address" "," Int ":" "uint256" ")" [symbol(), klabel(method_ERC721_S2Kapprove_address_uint256)] + syntax S2KERC721Method ::= "S2Kapprove" "(" Int ":" "address" "," Int ":" "uint256" ")" [symbol(method_ERC721_S2Kapprove_address_uint256)] - syntax S2KERC721Method ::= "S2KbalanceOf" "(" Int ":" "address" ")" [symbol(), klabel(method_ERC721_S2KbalanceOf_address)] + syntax S2KERC721Method ::= "S2KbalanceOf" "(" Int ":" "address" ")" [symbol(method_ERC721_S2KbalanceOf_address)] - syntax S2KERC721Method ::= "S2KgetApproved" "(" Int ":" "uint256" ")" [symbol(), klabel(method_ERC721_S2KgetApproved_uint256)] + syntax S2KERC721Method ::= "S2KgetApproved" "(" Int ":" "uint256" ")" [symbol(method_ERC721_S2KgetApproved_uint256)] - syntax S2KERC721Method ::= "S2KisApprovedForAll" "(" Int ":" "address" "," Int ":" "address" ")" [symbol(), klabel(method_ERC721_S2KisApprovedForAll_address_address)] + syntax S2KERC721Method ::= "S2KisApprovedForAll" "(" Int ":" "address" "," Int ":" "address" ")" [symbol(method_ERC721_S2KisApprovedForAll_address_address)] - syntax S2KERC721Method ::= "S2Kname" "(" ")" [symbol(), klabel(method_ERC721_S2Kname_)] + syntax S2KERC721Method ::= "S2Kname" "(" ")" [symbol(method_ERC721_S2Kname_)] - syntax S2KERC721Method ::= "S2KownerOf" "(" Int ":" "uint256" ")" [symbol(), klabel(method_ERC721_S2KownerOf_uint256)] + syntax S2KERC721Method ::= "S2KownerOf" "(" Int ":" "uint256" ")" [symbol(method_ERC721_S2KownerOf_uint256)] - syntax S2KERC721Method ::= "S2KsafeTransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" ")" [symbol(), klabel(method_ERC721_S2KsafeTransferFrom_address_address_uint256)] + syntax S2KERC721Method ::= "S2KsafeTransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" ")" [symbol(method_ERC721_S2KsafeTransferFrom_address_address_uint256)] - syntax S2KERC721Method ::= "S2KsafeTransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" "," Bytes ":" "bytes" ")" [symbol(), klabel(method_ERC721_S2KsafeTransferFrom_address_address_uint256_bytes)] + syntax S2KERC721Method ::= "S2KsafeTransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" "," Bytes ":" "bytes" ")" [symbol(method_ERC721_S2KsafeTransferFrom_address_address_uint256_bytes)] - syntax S2KERC721Method ::= "S2KsetApprovalForAll" "(" Int ":" "address" "," Int ":" "bool" ")" [symbol(), klabel(method_ERC721_S2KsetApprovalForAll_address_bool)] + syntax S2KERC721Method ::= "S2KsetApprovalForAll" "(" Int ":" "address" "," Int ":" "bool" ")" [symbol(method_ERC721_S2KsetApprovalForAll_address_bool)] - syntax S2KERC721Method ::= "S2KsupportsInterface" "(" Int ":" "bytes4" ")" [symbol(), klabel(method_ERC721_S2KsupportsInterface_bytes4)] + syntax S2KERC721Method ::= "S2KsupportsInterface" "(" Int ":" "bytes4" ")" [symbol(method_ERC721_S2KsupportsInterface_bytes4)] - syntax S2KERC721Method ::= "S2Ksymbol" "(" ")" [symbol(), klabel(method_ERC721_S2Ksymbol_)] + syntax S2KERC721Method ::= "S2Ksymbol" "(" ")" [symbol(method_ERC721_S2Ksymbol_)] - syntax S2KERC721Method ::= "S2KtokenURI" "(" Int ":" "uint256" ")" [symbol(), klabel(method_ERC721_S2KtokenURI_uint256)] + syntax S2KERC721Method ::= "S2KtokenURI" "(" Int ":" "uint256" ")" [symbol(method_ERC721_S2KtokenURI_uint256)] - syntax S2KERC721Method ::= "S2KtransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" ")" [symbol(), klabel(method_ERC721_S2KtransferFrom_address_address_uint256)] + syntax S2KERC721Method ::= "S2KtransferFrom" "(" Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" ")" [symbol(method_ERC721_S2KtransferFrom_address_address_uint256)] rule ( S2KERC721 . S2Kapprove ( V0_to : address , V1_tokenId : uint256 ) => #abiCallData ( "approve" , #address ( V0_to ) , #uint256 ( V1_tokenId ) , .TypedArgs ) ) ensures ( #rangeAddress ( V0_to ) diff --git a/tests/specs/examples/storage-bin-runtime.k b/tests/specs/examples/storage-bin-runtime.k index 355472831c..6911db73d4 100644 --- a/tests/specs/examples/storage-bin-runtime.k +++ b/tests/specs/examples/storage-bin-runtime.k @@ -5,154 +5,154 @@ module Storage-CONTRACT syntax Contract ::= S2KStorageContract - syntax S2KStorageContract ::= "S2KStorage" [symbol(), klabel(contract_Storage)] + syntax S2KStorageContract ::= "S2KStorage" [symbol(contract_Storage)] rule ( #binRuntime ( S2KStorage ) => #parseByteStack ( "0x608060405234801561001057600080fd5b50600436106103fc5760003560e01c80637288e87c11610215578063a03b52fd11610125578063d88ed1d7116100b8578063eb1b30d911610087578063eb1b30d914610b63578063f08d610314610b7f578063f616964a14610b9d578063f8be065114610bbb578063fc94ae0914610bd9576103fc565b8063d88ed1d714610aeb578063e0b1524f14610b09578063e2a4b2af14610b27578063e898852414610b45576103fc565b8063b4aadf23116100f4578063b4aadf2314610a73578063b6e3197e14610a91578063b8bf41b214610aaf578063c3ff504014610acd576103fc565b8063a03b52fd146109fb578063a7dbce1c14610a19578063a84631ba14610a37578063abac82bd14610a55576103fc565b806387d6ef18116101a857806391f9a0ef1161017757806391f9a0ef146109655780639375ab821461098357806398c2d5ee146109a157806399282470146109bf5780639b6a236f146109dd576103fc565b806387d6ef18146108ed57806389d70f951461090b5780638e2dc2cb146109295780638f56f49114610947576103fc565b80637ecc9e89116101e45780637ecc9e89146108755780637f2482961461089357806382266dbc146108b1578063848aefe7146108cf576103fc565b80637288e87c146107fd578063734b1e531461081b578063775a974214610839578063794d1dda14610857576103fc565b80633ed5a1b91161031057806350fa9586116102a35780636652754f116102725780636652754f146107675780636cd7c55d146107855780636deecdbe146107a35780636e92c39e146107c1578063712f4602146107df576103fc565b806350fa9586146106ef578063512c8e2f1461070d578063527400331461072b5780635507c8fa14610749576103fc565b806345d12877116102df57806345d128771461067757806345e6eb4314610695578063492bfa18146106b35780634d70c615146106d1576103fc565b80633ed5a1b9146105ff5780633ef9ce951461061d5780633f066ec31461063b57806343f9f4d014610659576103fc565b8063120d999f1161039357806326e05a9b1161036257806326e05a9b14610569578063377172b91461058757806337aa1527146105a557806338719ee5146105c35780633c2cfbae146105e1576103fc565b8063120d999f146104f157806313a8ebd51461050f578063157813861461052d578063184256ed1461054b576103fc565b80630abf5438116103cf5780630abf5438146104795780630b9031f7146104975780630db0d3a6146104b5578063118b7864146104d3576103fc565b806303d5c6a014610401578063060b4f311461041f578063062811381461043d57806309a407f61461045b575b600080fd5b610409610bf7565b60405161041691906113d1565b60405180910390f35b610427610c0a565b6040516104349190611412565b60405180910390f35b610445610c27565b6040516104529190611449565b60405180910390f35b610463610c3a565b6040516104709190611498565b60405180910390f35b610481610c65565b60405161048e91906114cf565b60405180910390f35b61049f610c78565b6040516104ac9190611506565b60405180910390f35b6104bd610c8b565b6040516104ca9190611554565b60405180910390f35b6104db610cb5565b6040516104e8919061158b565b60405180910390f35b6104f9610cc8565b60405161050691906115c5565b60405180910390f35b610517610cde565b6040516105249190611604565b60405180910390f35b610535610cf9565b604051610542919061164d565b60405180910390f35b610553610d1e565b604051610560919061169a565b60405180910390f35b610571610d47565b60405161057e91906116d1565b60405180910390f35b61058f610d5a565b60405161059c9190611705565b60405180910390f35b6105ad610d60565b6040516105ba919061173c565b60405180910390f35b6105cb610d73565b6040516105d89190611775565b60405180910390f35b6105e9610d88565b6040516105f691906117c0565b60405180910390f35b610607610daf565b60405161061491906117f7565b60405180910390f35b610625610dc2565b6040516106329190611835565b60405180910390f35b610643610ddc565b604051610650919061188a565b60405180910390f35b610661610e0d565b60405161066e91906118c1565b60405180910390f35b61067f610e20565b60405161068c91906118f8565b60405180910390f35b61069d610e33565b6040516106aa919061192f565b60405180910390f35b6106bb610e46565b6040516106c891906119e3565b60405180910390f35b6106d9610ed4565b6040516106e69190611a21565b60405180910390f35b6106f7610ee7565b6040516107049190611a58565b60405180910390f35b610715610efa565b6040516107229190611a8f565b60405180910390f35b610733610f0d565b6040516107409190611ad9565b60405180910390f35b610751610f33565b60405161075e9190611b10565b60405180910390f35b61076f610f44565b60405161077c9190611b47565b60405180910390f35b61078d610f57565b60405161079a9190611b7e565b60405180910390f35b6107ab610f6a565b6040516107b89190611bb4565b60405180910390f35b6107c9610f7b565b6040516107d69190611beb565b60405180910390f35b6107e7610f8e565b6040516107f49190611c5b565b60405180910390f35b61080561101c565b6040516108129190611c99565b60405180910390f35b61082361102f565b6040516108309190611ceb565b60405180910390f35b61084161105d565b60405161084e9190611d22565b60405180910390f35b61085f611070565b60405161086c9190611d5e565b60405180910390f35b61087d611088565b60405161088a9190611da4565b60405180910390f35b61089b6110aa565b6040516108a89190611ddf565b60405180910390f35b6108b96110c1565b6040516108c69190611e16565b60405180910390f35b6108d76110d4565b6040516108e49190611e6a565b60405180910390f35b6108f5611104565b6040516109029190611eaa565b60405180910390f35b610913611120565b6040516109209190611eee565b60405180910390f35b610931611140565b60405161093e9190611f26565b60405180910390f35b61094f611154565b60405161095c9190611f72565b60405180910390f35b61096d61117c565b60405161097a9190611fa9565b60405180910390f35b61098b61118f565b6040516109989190611fe0565b60405180910390f35b6109a96111a2565b6040516109b69190612023565b60405180910390f35b6109c76111c1565b6040516109d49190612076565b60405180910390f35b6109e56111f0565b6040516109f291906120ad565b60405180910390f35b610a03611203565b604051610a1091906120e4565b60405180910390f35b610a21611216565b604051610a2e9190612118565b60405180910390f35b610a3f61121c565b604051610a4c919061215a565b60405180910390f35b610a5d61123a565b604051610a6a9190612191565b60405180910390f35b610a7b61124d565b604051610a8891906121c8565b60405180910390f35b610a99611260565b604051610aa6919061220d565b60405180910390f35b610ab7611281565b604051610ac4919061224a565b60405180910390f35b610ad561129a565b604051610ae2919061229b565b60405180910390f35b610af36112c7565b604051610b0091906122eb565b60405180910390f35b610b116112f3565b604051610b1e9190612322565b60405180910390f35b610b2f611306565b604051610b3c9190612359565b60405180910390f35b610b4d611319565b604051610b5a9190612390565b60405180910390f35b610b7d6004803603810190610b7891906123dc565b61132c565b005b610b87611348565b604051610b949190612436565b60405180910390f35b610ba561136c565b604051610bb2919061246d565b60405180910390f35b610bc361137f565b604051610bd091906124b4565b60405180910390f35b610be16113a2565b604051610bee91906124eb565b60405180910390f35b601e60009054906101000a900460140b81565b600260009054906101000a90046affffffffffffffffffffff1681565b602360009054906101000a900460190b81565b600d60009054906101000a900478ffffffffffffffffffffffffffffffffffffffffffffffffff1681565b601560039054906101000a900460020b81565b602760009054906101000a9004601d0b81565b600c60009054906101000a900477ffffffffffffffffffffffffffffffffffffffffffffffff1681565b6015600f9054906101000a900460050b81565b600060079054906101000a900463ffffffff1681565b600160089054906101000a900468ffffffffffffffffff1681565b600760009054906101000a900472ffffffffffffffffffffffffffffffffffffff1681565b600b60009054906101000a900476ffffffffffffffffffffffffffffffffffffffffffffff1681565b601560069054906101000a900460030b81565b60295481565b602060009054906101000a900460160b81565b600060049054906101000a900462ffffff1681565b600960009054906101000a900474ffffffffffffffffffffffffffffffffffffffffff1681565b602560009054906101000a9004601b0b81565b600160009054906101000a900467ffffffffffffffff1681565b601360009054906101000a90047effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1681565b6017600b9054906101000a9004600b0b81565b6019600f9054906101000a9004600f0b81565b602860009054906101000a9004601e0b81565b602a8054610e5390612535565b80601f0160208091040260200160405190810160405280929190818152602001828054610e7f90612535565b8015610ecc5780601f10610ea157610100808354040283529160200191610ecc565b820191906000526020600020905b815481529060010190602001808311610eaf57829003601f168201915b505050505081565b602660009054906101000a9004601c0b81565b601660089054906101000a900460080b81565b6018600d9054906101000a9004600d0b81565b600860009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60158054906101000a900460060b81565b601560019054906101000a900460010b81565b601660009054906101000a900460070b81565b60008054906101000a900460ff1681565b601560009054906101000a900460000b81565b602b8054610f9b90612535565b80601f0160208091040260200160405190810160405280929190818152602001828054610fc790612535565b80156110145780601f10610fe957610100808354040283529160200191611014565b820191906000526020600020905b815481529060010190602001808311610ff757829003601f168201915b505050505081565b601a60009054906101000a900460100b81565b601060009054906101000a90047bffffffffffffffffffffffffffffffffffffffffffffffffffffffff1681565b602260009054906101000a900460180b81565b600060109054906101000a900465ffffffffffff1681565b6004600f9054906101000a90046fffffffffffffffffffffffffffffffff1681565b6000600b9054906101000a900464ffffffffff1681565b601c60009054906101000a900460120b81565b601260009054906101000a90047dffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1681565b600160119054906101000a900469ffffffffffffffffffff1681565b6003600d9054906101000a90046dffffffffffffffffffffffffffff1681565b600060029054906101000a900461ffff1681565b600a60009054906101000a900475ffffffffffffffffffffffffffffffffffffffffffff1681565b601960009054906101000a9004600e0b81565b601f60009054906101000a900460150b81565b600360009054906101000a90046cffffffffffffffffffffffffff1681565b601160009054906101000a90047cffffffffffffffffffffffffffffffffffffffffffffffffffffffffff1681565b601660119054906101000a900460090b81565b6015600a9054906101000a900460040b81565b60145481565b6002600b9054906101000a90046bffffffffffffffffffffffff1681565b601d60009054906101000a900460130b81565b601b60009054906101000a900460110b81565b600460009054906101000a90046effffffffffffffffffffffffffffff1681565b600060169054906101000a900466ffffffffffffff1681565b600f60009054906101000a90047affffffffffffffffffffffffffffffffffffffffffffffffffffff1681565b600e60009054906101000a900479ffffffffffffffffffffffffffffffffffffffffffffffffffff1681565b601860009054906101000a9004600c0b81565b600060019054906101000a900460ff1681565b602160009054906101000a900460170b81565b806000806101000a81548160ff02191690831515021790555050565b600660009054906101000a900471ffffffffffffffffffffffffffffffffffff1681565b602460009054906101000a9004601a0b81565b600560009054906101000a900470ffffffffffffffffffffffffffffffffff1681565b601760009054906101000a9004600a0b81565b60008160140b9050919050565b6113cb816113b5565b82525050565b60006020820190506113e660008301846113c2565b92915050565b60006affffffffffffffffffffff82169050919050565b61140c816113ec565b82525050565b60006020820190506114276000830184611403565b92915050565b60008160190b9050919050565b6114438161142d565b82525050565b600060208201905061145e600083018461143a565b92915050565b600078ffffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b61149281611464565b82525050565b60006020820190506114ad6000830184611489565b92915050565b60008160020b9050919050565b6114c9816114b3565b82525050565b60006020820190506114e460008301846114c0565b92915050565b600081601d0b9050919050565b611500816114ea565b82525050565b600060208201905061151b60008301846114f7565b92915050565b600077ffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b61154e81611521565b82525050565b60006020820190506115696000830184611545565b92915050565b60008160050b9050919050565b6115858161156f565b82525050565b60006020820190506115a0600083018461157c565b92915050565b600063ffffffff82169050919050565b6115bf816115a6565b82525050565b60006020820190506115da60008301846115b6565b92915050565b600068ffffffffffffffffff82169050919050565b6115fe816115e0565b82525050565b600060208201905061161960008301846115f5565b92915050565b600072ffffffffffffffffffffffffffffffffffffff82169050919050565b6116478161161f565b82525050565b6000602082019050611662600083018461163e565b92915050565b600076ffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b61169481611668565b82525050565b60006020820190506116af600083018461168b565b92915050565b60008160030b9050919050565b6116cb816116b5565b82525050565b60006020820190506116e660008301846116c2565b92915050565b6000819050919050565b6116ff816116ec565b82525050565b600060208201905061171a60008301846116f6565b92915050565b60008160160b9050919050565b61173681611720565b82525050565b6000602082019050611751600083018461172d565b92915050565b600062ffffff82169050919050565b61176f81611757565b82525050565b600060208201905061178a6000830184611766565b92915050565b600074ffffffffffffffffffffffffffffffffffffffffff82169050919050565b6117ba81611790565b82525050565b60006020820190506117d560008301846117b1565b92915050565b600081601b0b9050919050565b6117f1816117db565b82525050565b600060208201905061180c60008301846117e8565b92915050565b600067ffffffffffffffff82169050919050565b61182f81611812565b82525050565b600060208201905061184a6000830184611826565b92915050565b60007effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b61188481611850565b82525050565b600060208201905061189f600083018461187b565b92915050565b600081600b0b9050919050565b6118bb816118a5565b82525050565b60006020820190506118d660008301846118b2565b92915050565b600081600f0b9050919050565b6118f2816118dc565b82525050565b600060208201905061190d60008301846118e9565b92915050565b600081601e0b9050919050565b61192981611913565b82525050565b60006020820190506119446000830184611920565b92915050565b600081519050919050565b600082825260208201905092915050565b60005b83811015611984578082015181840152602081019050611969565b83811115611993576000848401525b50505050565b6000601f19601f8301169050919050565b60006119b58261194a565b6119bf8185611955565b93506119cf818560208601611966565b6119d881611999565b840191505092915050565b600060208201905081810360008301526119fd81846119aa565b905092915050565b600081601c0b9050919050565b611a1b81611a05565b82525050565b6000602082019050611a366000830184611a12565b92915050565b60008160080b9050919050565b611a5281611a3c565b82525050565b6000602082019050611a6d6000830184611a49565b92915050565b600081600d0b9050919050565b611a8981611a73565b82525050565b6000602082019050611aa46000830184611a80565b92915050565b600073ffffffffffffffffffffffffffffffffffffffff82169050919050565b611ad381611aaa565b82525050565b6000602082019050611aee6000830184611aca565b92915050565b60008160060b9050919050565b611b0a81611af4565b82525050565b6000602082019050611b256000830184611b01565b92915050565b60008160010b9050919050565b611b4181611b2b565b82525050565b6000602082019050611b5c6000830184611b38565b92915050565b60008160070b9050919050565b611b7881611b62565b82525050565b6000602082019050611b936000830184611b6f565b92915050565b60008115159050919050565b611bae81611b99565b82525050565b6000602082019050611bc96000830184611ba5565b92915050565b60008160000b9050919050565b611be581611bcf565b82525050565b6000602082019050611c006000830184611bdc565b92915050565b600081519050919050565b600082825260208201905092915050565b6000611c2d82611c06565b611c378185611c11565b9350611c47818560208601611966565b611c5081611999565b840191505092915050565b60006020820190508181036000830152611c758184611c22565b905092915050565b60008160100b9050919050565b611c9381611c7d565b82525050565b6000602082019050611cae6000830184611c8a565b92915050565b60007bffffffffffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b611ce581611cb4565b82525050565b6000602082019050611d006000830184611cdc565b92915050565b60008160180b9050919050565b611d1c81611d06565b82525050565b6000602082019050611d376000830184611d13565b92915050565b600065ffffffffffff82169050919050565b611d5881611d3d565b82525050565b6000602082019050611d736000830184611d4f565b92915050565b60006fffffffffffffffffffffffffffffffff82169050919050565b611d9e81611d79565b82525050565b6000602082019050611db96000830184611d95565b92915050565b600064ffffffffff82169050919050565b611dd981611dbf565b82525050565b6000602082019050611df46000830184611dd0565b92915050565b60008160120b9050919050565b611e1081611dfa565b82525050565b6000602082019050611e2b6000830184611e07565b92915050565b60007dffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b611e6481611e31565b82525050565b6000602082019050611e7f6000830184611e5b565b92915050565b600069ffffffffffffffffffff82169050919050565b611ea481611e85565b82525050565b6000602082019050611ebf6000830184611e9b565b92915050565b60006dffffffffffffffffffffffffffff82169050919050565b611ee881611ec5565b82525050565b6000602082019050611f036000830184611edf565b92915050565b600061ffff82169050919050565b611f2081611f09565b82525050565b6000602082019050611f3b6000830184611f17565b92915050565b600075ffffffffffffffffffffffffffffffffffffffffffff82169050919050565b611f6c81611f41565b82525050565b6000602082019050611f876000830184611f63565b92915050565b600081600e0b9050919050565b611fa381611f8d565b82525050565b6000602082019050611fbe6000830184611f9a565b92915050565b60008160150b9050919050565b611fda81611fc4565b82525050565b6000602082019050611ff56000830184611fd1565b92915050565b60006cffffffffffffffffffffffffff82169050919050565b61201d81611ffb565b82525050565b60006020820190506120386000830184612014565b92915050565b60007cffffffffffffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b6120708161203e565b82525050565b600060208201905061208b6000830184612067565b92915050565b60008160090b9050919050565b6120a781612091565b82525050565b60006020820190506120c2600083018461209e565b92915050565b60008160040b9050919050565b6120de816120c8565b82525050565b60006020820190506120f960008301846120d5565b92915050565b6000819050919050565b612112816120ff565b82525050565b600060208201905061212d6000830184612109565b92915050565b60006bffffffffffffffffffffffff82169050919050565b61215481612133565b82525050565b600060208201905061216f600083018461214b565b92915050565b60008160130b9050919050565b61218b81612175565b82525050565b60006020820190506121a66000830184612182565b92915050565b60008160110b9050919050565b6121c2816121ac565b82525050565b60006020820190506121dd60008301846121b9565b92915050565b60006effffffffffffffffffffffffffffff82169050919050565b612207816121e3565b82525050565b600060208201905061222260008301846121fe565b92915050565b600066ffffffffffffff82169050919050565b61224481612228565b82525050565b600060208201905061225f600083018461223b565b92915050565b60007affffffffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b61229581612265565b82525050565b60006020820190506122b0600083018461228c565b92915050565b600079ffffffffffffffffffffffffffffffffffffffffffffffffffff82169050919050565b6122e5816122b6565b82525050565b600060208201905061230060008301846122dc565b92915050565b600081600c0b9050919050565b61231c81612306565b82525050565b60006020820190506123376000830184612313565b92915050565b600060ff82169050919050565b6123538161233d565b82525050565b600060208201905061236e600083018461234a565b92915050565b60008160170b9050919050565b61238a81612374565b82525050565b60006020820190506123a56000830184612381565b92915050565b600080fd5b6123b981611b99565b81146123c457600080fd5b50565b6000813590506123d6816123b0565b92915050565b6000602082840312156123f2576123f16123ab565b5b6000612400848285016123c7565b91505092915050565b600071ffffffffffffffffffffffffffffffffffff82169050919050565b61243081612409565b82525050565b600060208201905061244b6000830184612427565b92915050565b600081601a0b9050919050565b61246781612451565b82525050565b6000602082019050612482600083018461245e565b92915050565b600070ffffffffffffffffffffffffffffffffff82169050919050565b6124ae81612488565b82525050565b60006020820190506124c960008301846124a5565b92915050565b600081600a0b9050919050565b6124e5816124cf565b82525050565b600060208201905061250060008301846124dc565b92915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052602260045260246000fd5b6000600282049050600182168061254d57607f821691505b6020821081036125605761255f612506565b5b5091905056fea26469706673582212209d89f7186a163d8a4087cae2caff77f1894ba5c5c5c78eacabc4b169156d4fa064736f6c634300080d0033" ) ) syntax Field ::= StorageField - syntax StorageField ::= "myBool" [symbol(), klabel(field_Storage_myBool)] + syntax StorageField ::= "myBool" [symbol(field_Storage_myBool)] - syntax StorageField ::= "myUint8" [symbol(), klabel(field_Storage_myUint8)] + syntax StorageField ::= "myUint8" [symbol(field_Storage_myUint8)] - syntax StorageField ::= "myUint16" [symbol(), klabel(field_Storage_myUint16)] + syntax StorageField ::= "myUint16" [symbol(field_Storage_myUint16)] - syntax StorageField ::= "myUint24" [symbol(), klabel(field_Storage_myUint24)] + syntax StorageField ::= "myUint24" [symbol(field_Storage_myUint24)] - syntax StorageField ::= "myUint32" [symbol(), klabel(field_Storage_myUint32)] + syntax StorageField ::= "myUint32" [symbol(field_Storage_myUint32)] - syntax StorageField ::= "myUint40" [symbol(), klabel(field_Storage_myUint40)] + syntax StorageField ::= "myUint40" [symbol(field_Storage_myUint40)] - syntax StorageField ::= "myUint48" [symbol(), klabel(field_Storage_myUint48)] + syntax StorageField ::= "myUint48" [symbol(field_Storage_myUint48)] - syntax StorageField ::= "myUint56" [symbol(), klabel(field_Storage_myUint56)] + syntax StorageField ::= "myUint56" [symbol(field_Storage_myUint56)] - syntax StorageField ::= "myUint64" [symbol(), klabel(field_Storage_myUint64)] + syntax StorageField ::= "myUint64" [symbol(field_Storage_myUint64)] - syntax StorageField ::= "myUint72" [symbol(), klabel(field_Storage_myUint72)] + syntax StorageField ::= "myUint72" [symbol(field_Storage_myUint72)] - syntax StorageField ::= "myUint80" [symbol(), klabel(field_Storage_myUint80)] + syntax StorageField ::= "myUint80" [symbol(field_Storage_myUint80)] - syntax StorageField ::= "myUint88" [symbol(), klabel(field_Storage_myUint88)] + syntax StorageField ::= "myUint88" [symbol(field_Storage_myUint88)] - syntax StorageField ::= "myUint96" [symbol(), klabel(field_Storage_myUint96)] + syntax StorageField ::= "myUint96" [symbol(field_Storage_myUint96)] - syntax StorageField ::= "myUint104" [symbol(), klabel(field_Storage_myUint104)] + syntax StorageField ::= "myUint104" [symbol(field_Storage_myUint104)] - syntax StorageField ::= "myUint112" [symbol(), klabel(field_Storage_myUint112)] + syntax StorageField ::= "myUint112" [symbol(field_Storage_myUint112)] - syntax StorageField ::= "myUint120" [symbol(), klabel(field_Storage_myUint120)] + syntax StorageField ::= "myUint120" [symbol(field_Storage_myUint120)] - syntax StorageField ::= "myUint128" [symbol(), klabel(field_Storage_myUint128)] + syntax StorageField ::= "myUint128" [symbol(field_Storage_myUint128)] - syntax StorageField ::= "myUint136" [symbol(), klabel(field_Storage_myUint136)] + syntax StorageField ::= "myUint136" [symbol(field_Storage_myUint136)] - syntax StorageField ::= "myUint144" [symbol(), klabel(field_Storage_myUint144)] + syntax StorageField ::= "myUint144" [symbol(field_Storage_myUint144)] - syntax StorageField ::= "myUint152" [symbol(), klabel(field_Storage_myUint152)] + syntax StorageField ::= "myUint152" [symbol(field_Storage_myUint152)] - syntax StorageField ::= "myUint160" [symbol(), klabel(field_Storage_myUint160)] + syntax StorageField ::= "myUint160" [symbol(field_Storage_myUint160)] - syntax StorageField ::= "myUint168" [symbol(), klabel(field_Storage_myUint168)] + syntax StorageField ::= "myUint168" [symbol(field_Storage_myUint168)] - syntax StorageField ::= "myUint176" [symbol(), klabel(field_Storage_myUint176)] + syntax StorageField ::= "myUint176" [symbol(field_Storage_myUint176)] - syntax StorageField ::= "myUint184" [symbol(), klabel(field_Storage_myUint184)] + syntax StorageField ::= "myUint184" [symbol(field_Storage_myUint184)] - syntax StorageField ::= "myUint192" [symbol(), klabel(field_Storage_myUint192)] + syntax StorageField ::= "myUint192" [symbol(field_Storage_myUint192)] - syntax StorageField ::= "myUint200" [symbol(), klabel(field_Storage_myUint200)] + syntax StorageField ::= "myUint200" [symbol(field_Storage_myUint200)] - syntax StorageField ::= "myUint208" [symbol(), klabel(field_Storage_myUint208)] + syntax StorageField ::= "myUint208" [symbol(field_Storage_myUint208)] - syntax StorageField ::= "myUint216" [symbol(), klabel(field_Storage_myUint216)] + syntax StorageField ::= "myUint216" [symbol(field_Storage_myUint216)] - syntax StorageField ::= "myUint224" [symbol(), klabel(field_Storage_myUint224)] + syntax StorageField ::= "myUint224" [symbol(field_Storage_myUint224)] - syntax StorageField ::= "myUint232" [symbol(), klabel(field_Storage_myUint232)] + syntax StorageField ::= "myUint232" [symbol(field_Storage_myUint232)] - syntax StorageField ::= "myUint240" [symbol(), klabel(field_Storage_myUint240)] + syntax StorageField ::= "myUint240" [symbol(field_Storage_myUint240)] - syntax StorageField ::= "myUint248" [symbol(), klabel(field_Storage_myUint248)] + syntax StorageField ::= "myUint248" [symbol(field_Storage_myUint248)] - syntax StorageField ::= "myUint256" [symbol(), klabel(field_Storage_myUint256)] + syntax StorageField ::= "myUint256" [symbol(field_Storage_myUint256)] - syntax StorageField ::= "myInt8" [symbol(), klabel(field_Storage_myInt8)] + syntax StorageField ::= "myInt8" [symbol(field_Storage_myInt8)] - syntax StorageField ::= "myInt16" [symbol(), klabel(field_Storage_myInt16)] + syntax StorageField ::= "myInt16" [symbol(field_Storage_myInt16)] - syntax StorageField ::= "myInt24" [symbol(), klabel(field_Storage_myInt24)] + syntax StorageField ::= "myInt24" [symbol(field_Storage_myInt24)] - syntax StorageField ::= "myInt32" [symbol(), klabel(field_Storage_myInt32)] + syntax StorageField ::= "myInt32" [symbol(field_Storage_myInt32)] - syntax StorageField ::= "myInt40" [symbol(), klabel(field_Storage_myInt40)] + syntax StorageField ::= "myInt40" [symbol(field_Storage_myInt40)] - syntax StorageField ::= "myInt48" [symbol(), klabel(field_Storage_myInt48)] + syntax StorageField ::= "myInt48" [symbol(field_Storage_myInt48)] - syntax StorageField ::= "myInt56" [symbol(), klabel(field_Storage_myInt56)] + syntax StorageField ::= "myInt56" [symbol(field_Storage_myInt56)] - syntax StorageField ::= "myInt64" [symbol(), klabel(field_Storage_myInt64)] + syntax StorageField ::= "myInt64" [symbol(field_Storage_myInt64)] - syntax StorageField ::= "myInt72" [symbol(), klabel(field_Storage_myInt72)] + syntax StorageField ::= "myInt72" [symbol(field_Storage_myInt72)] - syntax StorageField ::= "myInt80" [symbol(), klabel(field_Storage_myInt80)] + syntax StorageField ::= "myInt80" [symbol(field_Storage_myInt80)] - syntax StorageField ::= "myInt88" [symbol(), klabel(field_Storage_myInt88)] + syntax StorageField ::= "myInt88" [symbol(field_Storage_myInt88)] - syntax StorageField ::= "myInt96" [symbol(), klabel(field_Storage_myInt96)] + syntax StorageField ::= "myInt96" [symbol(field_Storage_myInt96)] - syntax StorageField ::= "myInt104" [symbol(), klabel(field_Storage_myInt104)] + syntax StorageField ::= "myInt104" [symbol(field_Storage_myInt104)] - syntax StorageField ::= "myInt112" [symbol(), klabel(field_Storage_myInt112)] + syntax StorageField ::= "myInt112" [symbol(field_Storage_myInt112)] - syntax StorageField ::= "myInt120" [symbol(), klabel(field_Storage_myInt120)] + syntax StorageField ::= "myInt120" [symbol(field_Storage_myInt120)] - syntax StorageField ::= "myInt128" [symbol(), klabel(field_Storage_myInt128)] + syntax StorageField ::= "myInt128" [symbol(field_Storage_myInt128)] - syntax StorageField ::= "myInt136" [symbol(), klabel(field_Storage_myInt136)] + syntax StorageField ::= "myInt136" [symbol(field_Storage_myInt136)] - syntax StorageField ::= "myInt144" [symbol(), klabel(field_Storage_myInt144)] + syntax StorageField ::= "myInt144" [symbol(field_Storage_myInt144)] - syntax StorageField ::= "myInt152" [symbol(), klabel(field_Storage_myInt152)] + syntax StorageField ::= "myInt152" [symbol(field_Storage_myInt152)] - syntax StorageField ::= "myInt160" [symbol(), klabel(field_Storage_myInt160)] + syntax StorageField ::= "myInt160" [symbol(field_Storage_myInt160)] - syntax StorageField ::= "myInt168" [symbol(), klabel(field_Storage_myInt168)] + syntax StorageField ::= "myInt168" [symbol(field_Storage_myInt168)] - syntax StorageField ::= "myInt176" [symbol(), klabel(field_Storage_myInt176)] + syntax StorageField ::= "myInt176" [symbol(field_Storage_myInt176)] - syntax StorageField ::= "myInt184" [symbol(), klabel(field_Storage_myInt184)] + syntax StorageField ::= "myInt184" [symbol(field_Storage_myInt184)] - syntax StorageField ::= "myInt192" [symbol(), klabel(field_Storage_myInt192)] + syntax StorageField ::= "myInt192" [symbol(field_Storage_myInt192)] - syntax StorageField ::= "myInt200" [symbol(), klabel(field_Storage_myInt200)] + syntax StorageField ::= "myInt200" [symbol(field_Storage_myInt200)] - syntax StorageField ::= "myInt208" [symbol(), klabel(field_Storage_myInt208)] + syntax StorageField ::= "myInt208" [symbol(field_Storage_myInt208)] - syntax StorageField ::= "myInt216" [symbol(), klabel(field_Storage_myInt216)] + syntax StorageField ::= "myInt216" [symbol(field_Storage_myInt216)] - syntax StorageField ::= "myInt224" [symbol(), klabel(field_Storage_myInt224)] + syntax StorageField ::= "myInt224" [symbol(field_Storage_myInt224)] - syntax StorageField ::= "myInt232" [symbol(), klabel(field_Storage_myInt232)] + syntax StorageField ::= "myInt232" [symbol(field_Storage_myInt232)] - syntax StorageField ::= "myInt240" [symbol(), klabel(field_Storage_myInt240)] + syntax StorageField ::= "myInt240" [symbol(field_Storage_myInt240)] - syntax StorageField ::= "myInt248" [symbol(), klabel(field_Storage_myInt248)] + syntax StorageField ::= "myInt248" [symbol(field_Storage_myInt248)] - syntax StorageField ::= "myInt256" [symbol(), klabel(field_Storage_myInt256)] + syntax StorageField ::= "myInt256" [symbol(field_Storage_myInt256)] - syntax StorageField ::= "myString" [symbol(), klabel(field_Storage_myString)] + syntax StorageField ::= "myString" [symbol(field_Storage_myString)] - syntax StorageField ::= "myBytes" [symbol(), klabel(field_Storage_myBytes)] + syntax StorageField ::= "myBytes" [symbol(field_Storage_myBytes)] - syntax StorageField ::= "myUint128s" [symbol(), klabel(field_Storage_myUint128s)] + syntax StorageField ::= "myUint128s" [symbol(field_Storage_myUint128s)] - syntax StorageField ::= "myUint64s" [symbol(), klabel(field_Storage_myUint64s)] + syntax StorageField ::= "myUint64s" [symbol(field_Storage_myUint64s)] - syntax StorageField ::= "myFoo" [symbol(), klabel(field_Storage_myFoo)] + syntax StorageField ::= "myFoo" [symbol(field_Storage_myFoo)] - syntax StorageField ::= "myFoos" [symbol(), klabel(field_Storage_myFoos)] + syntax StorageField ::= "myFoos" [symbol(field_Storage_myFoos)] rule ( #loc ( S2KStorage . myBool ) => 0 ) @@ -367,143 +367,143 @@ module Storage-CONTRACT rule ( #loc ( S2KStorage . myFoos ) => 49 ) - syntax Bytes ::= S2KStorageContract "." S2KStorageMethod [function(), symbol(), klabel(method_Storage)] + syntax Bytes ::= S2KStorageContract "." S2KStorageMethod [function(), symbol(method_Storage)] - syntax S2KStorageMethod ::= "S2KmyBool" "(" ")" [symbol(), klabel(method_Storage_S2KmyBool_)] + syntax S2KStorageMethod ::= "S2KmyBool" "(" ")" [symbol(method_Storage_S2KmyBool_)] - syntax S2KStorageMethod ::= "S2KmyBytes" "(" ")" [symbol(), klabel(method_Storage_S2KmyBytes_)] + syntax S2KStorageMethod ::= "S2KmyBytes" "(" ")" [symbol(method_Storage_S2KmyBytes_)] - syntax S2KStorageMethod ::= "S2KmyInt104" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt104_)] + syntax S2KStorageMethod ::= "S2KmyInt104" "(" ")" [symbol(method_Storage_S2KmyInt104_)] - syntax S2KStorageMethod ::= "S2KmyInt112" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt112_)] + syntax S2KStorageMethod ::= "S2KmyInt112" "(" ")" [symbol(method_Storage_S2KmyInt112_)] - syntax S2KStorageMethod ::= "S2KmyInt120" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt120_)] + syntax S2KStorageMethod ::= "S2KmyInt120" "(" ")" [symbol(method_Storage_S2KmyInt120_)] - syntax S2KStorageMethod ::= "S2KmyInt128" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt128_)] + syntax S2KStorageMethod ::= "S2KmyInt128" "(" ")" [symbol(method_Storage_S2KmyInt128_)] - syntax S2KStorageMethod ::= "S2KmyInt136" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt136_)] + syntax S2KStorageMethod ::= "S2KmyInt136" "(" ")" [symbol(method_Storage_S2KmyInt136_)] - syntax S2KStorageMethod ::= "S2KmyInt144" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt144_)] + syntax S2KStorageMethod ::= "S2KmyInt144" "(" ")" [symbol(method_Storage_S2KmyInt144_)] - syntax S2KStorageMethod ::= "S2KmyInt152" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt152_)] + syntax S2KStorageMethod ::= "S2KmyInt152" "(" ")" [symbol(method_Storage_S2KmyInt152_)] - syntax S2KStorageMethod ::= "S2KmyInt16" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt16_)] + syntax S2KStorageMethod ::= "S2KmyInt16" "(" ")" [symbol(method_Storage_S2KmyInt16_)] - syntax S2KStorageMethod ::= "S2KmyInt160" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt160_)] + syntax S2KStorageMethod ::= "S2KmyInt160" "(" ")" [symbol(method_Storage_S2KmyInt160_)] - syntax S2KStorageMethod ::= "S2KmyInt168" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt168_)] + syntax S2KStorageMethod ::= "S2KmyInt168" "(" ")" [symbol(method_Storage_S2KmyInt168_)] - syntax S2KStorageMethod ::= "S2KmyInt176" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt176_)] + syntax S2KStorageMethod ::= "S2KmyInt176" "(" ")" [symbol(method_Storage_S2KmyInt176_)] - syntax S2KStorageMethod ::= "S2KmyInt184" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt184_)] + syntax S2KStorageMethod ::= "S2KmyInt184" "(" ")" [symbol(method_Storage_S2KmyInt184_)] - syntax S2KStorageMethod ::= "S2KmyInt192" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt192_)] + syntax S2KStorageMethod ::= "S2KmyInt192" "(" ")" [symbol(method_Storage_S2KmyInt192_)] - syntax S2KStorageMethod ::= "S2KmyInt200" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt200_)] + syntax S2KStorageMethod ::= "S2KmyInt200" "(" ")" [symbol(method_Storage_S2KmyInt200_)] - syntax S2KStorageMethod ::= "S2KmyInt208" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt208_)] + syntax S2KStorageMethod ::= "S2KmyInt208" "(" ")" [symbol(method_Storage_S2KmyInt208_)] - syntax S2KStorageMethod ::= "S2KmyInt216" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt216_)] + syntax S2KStorageMethod ::= "S2KmyInt216" "(" ")" [symbol(method_Storage_S2KmyInt216_)] - syntax S2KStorageMethod ::= "S2KmyInt224" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt224_)] + syntax S2KStorageMethod ::= "S2KmyInt224" "(" ")" [symbol(method_Storage_S2KmyInt224_)] - syntax S2KStorageMethod ::= "S2KmyInt232" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt232_)] + syntax S2KStorageMethod ::= "S2KmyInt232" "(" ")" [symbol(method_Storage_S2KmyInt232_)] - syntax S2KStorageMethod ::= "S2KmyInt24" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt24_)] + syntax S2KStorageMethod ::= "S2KmyInt24" "(" ")" [symbol(method_Storage_S2KmyInt24_)] - syntax S2KStorageMethod ::= "S2KmyInt240" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt240_)] + syntax S2KStorageMethod ::= "S2KmyInt240" "(" ")" [symbol(method_Storage_S2KmyInt240_)] - syntax S2KStorageMethod ::= "S2KmyInt248" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt248_)] + syntax S2KStorageMethod ::= "S2KmyInt248" "(" ")" [symbol(method_Storage_S2KmyInt248_)] - syntax S2KStorageMethod ::= "S2KmyInt256" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt256_)] + syntax S2KStorageMethod ::= "S2KmyInt256" "(" ")" [symbol(method_Storage_S2KmyInt256_)] - syntax S2KStorageMethod ::= "S2KmyInt32" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt32_)] + syntax S2KStorageMethod ::= "S2KmyInt32" "(" ")" [symbol(method_Storage_S2KmyInt32_)] - syntax S2KStorageMethod ::= "S2KmyInt40" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt40_)] + syntax S2KStorageMethod ::= "S2KmyInt40" "(" ")" [symbol(method_Storage_S2KmyInt40_)] - syntax S2KStorageMethod ::= "S2KmyInt48" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt48_)] + syntax S2KStorageMethod ::= "S2KmyInt48" "(" ")" [symbol(method_Storage_S2KmyInt48_)] - syntax S2KStorageMethod ::= "S2KmyInt56" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt56_)] + syntax S2KStorageMethod ::= "S2KmyInt56" "(" ")" [symbol(method_Storage_S2KmyInt56_)] - syntax S2KStorageMethod ::= "S2KmyInt64" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt64_)] + syntax S2KStorageMethod ::= "S2KmyInt64" "(" ")" [symbol(method_Storage_S2KmyInt64_)] - syntax S2KStorageMethod ::= "S2KmyInt72" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt72_)] + syntax S2KStorageMethod ::= "S2KmyInt72" "(" ")" [symbol(method_Storage_S2KmyInt72_)] - syntax S2KStorageMethod ::= "S2KmyInt8" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt8_)] + syntax S2KStorageMethod ::= "S2KmyInt8" "(" ")" [symbol(method_Storage_S2KmyInt8_)] - syntax S2KStorageMethod ::= "S2KmyInt80" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt80_)] + syntax S2KStorageMethod ::= "S2KmyInt80" "(" ")" [symbol(method_Storage_S2KmyInt80_)] - syntax S2KStorageMethod ::= "S2KmyInt88" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt88_)] + syntax S2KStorageMethod ::= "S2KmyInt88" "(" ")" [symbol(method_Storage_S2KmyInt88_)] - syntax S2KStorageMethod ::= "S2KmyInt96" "(" ")" [symbol(), klabel(method_Storage_S2KmyInt96_)] + syntax S2KStorageMethod ::= "S2KmyInt96" "(" ")" [symbol(method_Storage_S2KmyInt96_)] - syntax S2KStorageMethod ::= "S2KmyString" "(" ")" [symbol(), klabel(method_Storage_S2KmyString_)] + syntax S2KStorageMethod ::= "S2KmyString" "(" ")" [symbol(method_Storage_S2KmyString_)] - syntax S2KStorageMethod ::= "S2KmyUint104" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint104_)] + syntax S2KStorageMethod ::= "S2KmyUint104" "(" ")" [symbol(method_Storage_S2KmyUint104_)] - syntax S2KStorageMethod ::= "S2KmyUint112" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint112_)] + syntax S2KStorageMethod ::= "S2KmyUint112" "(" ")" [symbol(method_Storage_S2KmyUint112_)] - syntax S2KStorageMethod ::= "S2KmyUint120" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint120_)] + syntax S2KStorageMethod ::= "S2KmyUint120" "(" ")" [symbol(method_Storage_S2KmyUint120_)] - syntax S2KStorageMethod ::= "S2KmyUint128" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint128_)] + syntax S2KStorageMethod ::= "S2KmyUint128" "(" ")" [symbol(method_Storage_S2KmyUint128_)] - syntax S2KStorageMethod ::= "S2KmyUint136" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint136_)] + syntax S2KStorageMethod ::= "S2KmyUint136" "(" ")" [symbol(method_Storage_S2KmyUint136_)] - syntax S2KStorageMethod ::= "S2KmyUint144" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint144_)] + syntax S2KStorageMethod ::= "S2KmyUint144" "(" ")" [symbol(method_Storage_S2KmyUint144_)] - syntax S2KStorageMethod ::= "S2KmyUint152" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint152_)] + syntax S2KStorageMethod ::= "S2KmyUint152" "(" ")" [symbol(method_Storage_S2KmyUint152_)] - syntax S2KStorageMethod ::= "S2KmyUint16" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint16_)] + syntax S2KStorageMethod ::= "S2KmyUint16" "(" ")" [symbol(method_Storage_S2KmyUint16_)] - syntax S2KStorageMethod ::= "S2KmyUint160" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint160_)] + syntax S2KStorageMethod ::= "S2KmyUint160" "(" ")" [symbol(method_Storage_S2KmyUint160_)] - syntax S2KStorageMethod ::= "S2KmyUint168" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint168_)] + syntax S2KStorageMethod ::= "S2KmyUint168" "(" ")" [symbol(method_Storage_S2KmyUint168_)] - syntax S2KStorageMethod ::= "S2KmyUint176" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint176_)] + syntax S2KStorageMethod ::= "S2KmyUint176" "(" ")" [symbol(method_Storage_S2KmyUint176_)] - syntax S2KStorageMethod ::= "S2KmyUint184" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint184_)] + syntax S2KStorageMethod ::= "S2KmyUint184" "(" ")" [symbol(method_Storage_S2KmyUint184_)] - syntax S2KStorageMethod ::= "S2KmyUint192" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint192_)] + syntax S2KStorageMethod ::= "S2KmyUint192" "(" ")" [symbol(method_Storage_S2KmyUint192_)] - syntax S2KStorageMethod ::= "S2KmyUint200" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint200_)] + syntax S2KStorageMethod ::= "S2KmyUint200" "(" ")" [symbol(method_Storage_S2KmyUint200_)] - syntax S2KStorageMethod ::= "S2KmyUint208" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint208_)] + syntax S2KStorageMethod ::= "S2KmyUint208" "(" ")" [symbol(method_Storage_S2KmyUint208_)] - syntax S2KStorageMethod ::= "S2KmyUint216" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint216_)] + syntax S2KStorageMethod ::= "S2KmyUint216" "(" ")" [symbol(method_Storage_S2KmyUint216_)] - syntax S2KStorageMethod ::= "S2KmyUint224" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint224_)] + syntax S2KStorageMethod ::= "S2KmyUint224" "(" ")" [symbol(method_Storage_S2KmyUint224_)] - syntax S2KStorageMethod ::= "S2KmyUint232" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint232_)] + syntax S2KStorageMethod ::= "S2KmyUint232" "(" ")" [symbol(method_Storage_S2KmyUint232_)] - syntax S2KStorageMethod ::= "S2KmyUint24" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint24_)] + syntax S2KStorageMethod ::= "S2KmyUint24" "(" ")" [symbol(method_Storage_S2KmyUint24_)] - syntax S2KStorageMethod ::= "S2KmyUint240" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint240_)] + syntax S2KStorageMethod ::= "S2KmyUint240" "(" ")" [symbol(method_Storage_S2KmyUint240_)] - syntax S2KStorageMethod ::= "S2KmyUint248" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint248_)] + syntax S2KStorageMethod ::= "S2KmyUint248" "(" ")" [symbol(method_Storage_S2KmyUint248_)] - syntax S2KStorageMethod ::= "S2KmyUint256" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint256_)] + syntax S2KStorageMethod ::= "S2KmyUint256" "(" ")" [symbol(method_Storage_S2KmyUint256_)] - syntax S2KStorageMethod ::= "S2KmyUint32" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint32_)] + syntax S2KStorageMethod ::= "S2KmyUint32" "(" ")" [symbol(method_Storage_S2KmyUint32_)] - syntax S2KStorageMethod ::= "S2KmyUint40" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint40_)] + syntax S2KStorageMethod ::= "S2KmyUint40" "(" ")" [symbol(method_Storage_S2KmyUint40_)] - syntax S2KStorageMethod ::= "S2KmyUint48" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint48_)] + syntax S2KStorageMethod ::= "S2KmyUint48" "(" ")" [symbol(method_Storage_S2KmyUint48_)] - syntax S2KStorageMethod ::= "S2KmyUint56" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint56_)] + syntax S2KStorageMethod ::= "S2KmyUint56" "(" ")" [symbol(method_Storage_S2KmyUint56_)] - syntax S2KStorageMethod ::= "S2KmyUint64" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint64_)] + syntax S2KStorageMethod ::= "S2KmyUint64" "(" ")" [symbol(method_Storage_S2KmyUint64_)] - syntax S2KStorageMethod ::= "S2KmyUint72" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint72_)] + syntax S2KStorageMethod ::= "S2KmyUint72" "(" ")" [symbol(method_Storage_S2KmyUint72_)] - syntax S2KStorageMethod ::= "S2KmyUint8" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint8_)] + syntax S2KStorageMethod ::= "S2KmyUint8" "(" ")" [symbol(method_Storage_S2KmyUint8_)] - syntax S2KStorageMethod ::= "S2KmyUint80" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint80_)] + syntax S2KStorageMethod ::= "S2KmyUint80" "(" ")" [symbol(method_Storage_S2KmyUint80_)] - syntax S2KStorageMethod ::= "S2KmyUint88" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint88_)] + syntax S2KStorageMethod ::= "S2KmyUint88" "(" ")" [symbol(method_Storage_S2KmyUint88_)] - syntax S2KStorageMethod ::= "S2KmyUint96" "(" ")" [symbol(), klabel(method_Storage_S2KmyUint96_)] + syntax S2KStorageMethod ::= "S2KmyUint96" "(" ")" [symbol(method_Storage_S2KmyUint96_)] - syntax S2KStorageMethod ::= "S2KsetMyBool" "(" Int ":" "bool" ")" [symbol(), klabel(method_Storage_S2KsetMyBool_bool)] + syntax S2KStorageMethod ::= "S2KsetMyBool" "(" Int ":" "bool" ")" [symbol(method_Storage_S2KsetMyBool_bool)] rule ( S2KStorage . S2KmyBool ( ) => #abiCallData ( "myBool" , .TypedArgs ) ) From 0cb068f559a80ccc5b3620b7333fbba8c96eb041 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Aug 2024 14:00:59 +0000 Subject: [PATCH 2/8] kevm_pyk/test_prove: optimize how we run the proofs --- kevm-pyk/src/tests/integration/test_prove.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 35605a4260..9e272524bf 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -9,6 +9,7 @@ from pyk.kast.att import AttEntry, Atts, KAtt from pyk.kast.outer import KClaim from pyk.kdist import kdist +from pyk.kore.rpc import FallbackReason from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofShow @@ -224,6 +225,8 @@ def _test_prove( 'break_on_basic_blocks': break_on_basic_blocks, 'workers': workers, 'direct_subproof_rules': direct_subproof_rules, + 'post_exec_simplify': False, + 'fallback_on': [FallbackReason.ABORTED, FallbackReason.STUCK], } ) exec_prove(options=options) From f35071902f43e5715ed7a0b1d28bbd0a12103b82 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Aug 2024 16:39:45 +0000 Subject: [PATCH 3/8] kevm_pyk/{cli,utils}: set defaults for CLI to fastest options too --- kevm-pyk/src/kevm_pyk/cli.py | 4 ++-- kevm-pyk/src/kevm_pyk/utils.py | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 1b4f62e718..a48b149d37 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -316,8 +316,8 @@ def default() -> dict[str, Any]: 'trace_rewrites': False, 'kore_rpc_command': None, 'use_booster': True, - 'fallback_on': [], - 'post_exec_simplify': True, + 'fallback_on': [FallbackReason.ABORTED, FallbackReason.STUCK], + 'post_exec_simplify': False, 'interim_simplification': None, 'port': None, 'maude_port': None, diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 315aeddb55..ae8b662b82 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -353,9 +353,10 @@ def legacy_explore( maude_port: int | None = None, fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, - no_post_exec_simplify: bool = False, + no_post_exec_simplify: bool = True, ) -> Iterator[KCFGExplore]: bug_report_id = None if bug_report is None else id + fallback_on = [FallbackReason.ABORTED, FallbackReason.STUCK] if fallback_on is None else fallback_on if start_server: # Old way of handling KCFGExplore, to be removed with kore_server( From 43dde61d7510b1433f399582b7c76691d4470159 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 9 Aug 2024 16:41:55 +0000 Subject: [PATCH 4/8] Set Version: 1.0.678 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 7d353e2a50..449ef4c79b 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.677" +version = "1.0.678" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index a86ecc590d..9da4b42fd3 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '1.0.677' +VERSION: Final = '1.0.678' diff --git a/package/version b/package/version index 968e24a388..a2ef791639 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.677 +1.0.678 From d5e28acaa6515d4bc6c45efcd0f423fc1d0cd818 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Aug 2024 16:45:34 +0000 Subject: [PATCH 5/8] kevm_pyk/utils: correct imports --- kevm-pyk/src/kevm_pyk/utils.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index ae8b662b82..f0ecb2df24 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -17,7 +17,7 @@ split_config_from, ) from pyk.kcfg import KCFGExplore -from pyk.kore.rpc import KoreClient, KoreExecLogFormat, TransportType, kore_server +from pyk.kore.rpc import FallbackReason, KoreClient, KoreExecLogFormat, TransportType, kore_server from pyk.ktool import TypeInferenceMode from pyk.ktool.claim_loader import ClaimLoader from pyk.prelude.ml import is_bottom, is_top @@ -33,7 +33,6 @@ from pyk.kast.outer import KClaim, KDefinition from pyk.kcfg import KCFG from pyk.kcfg.semantics import KCFGSemantics - from pyk.kore.rpc import FallbackReason from pyk.ktool.kprint import KPrint from pyk.ktool.kprove import KProve from pyk.proof.proof import Proof From bd2958f1ccd54cf2487021d7f4e9f43d11774bbb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Aug 2024 17:38:23 +0000 Subject: [PATCH 6/8] kevm_pyk/{utils,cli,__main__}: only pass fallback reasons for booster executions --- kevm-pyk/src/kevm_pyk/__main__.py | 4 +++- kevm-pyk/src/kevm_pyk/cli.py | 2 +- kevm-pyk/src/kevm_pyk/utils.py | 4 ++-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index cf5df3e531..278f2cc78a 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -21,7 +21,7 @@ from pyk.kcfg import KCFG from pyk.kcfg.explore import KCFGExplore from pyk.kdist import kdist -from pyk.kore.rpc import KoreClient +from pyk.kore.rpc import FallbackReason, KoreClient from pyk.kore.tools import kore_print from pyk.ktool.claim_loader import ClaimLoader from pyk.ktool.kompile import LLVMKompileType @@ -237,6 +237,8 @@ def exec_prove(options: ProveOptions) -> None: kore_rpc_command = ('kore-rpc',) else: kore_rpc_command = ('kore-rpc-booster',) + if options.fallback_on is None: + options.fallback_on = [FallbackReason.ABORTED, FallbackReason.STUCK] elif isinstance(options.kore_rpc_command, str): kore_rpc_command = tuple(options.kore_rpc_command.split()) else: diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index a48b149d37..3ac03173ec 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -316,7 +316,7 @@ def default() -> dict[str, Any]: 'trace_rewrites': False, 'kore_rpc_command': None, 'use_booster': True, - 'fallback_on': [FallbackReason.ABORTED, FallbackReason.STUCK], + 'fallback_on': [], 'post_exec_simplify': False, 'interim_simplification': None, 'port': None, diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index f0ecb2df24..6bb47b564a 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -17,7 +17,7 @@ split_config_from, ) from pyk.kcfg import KCFGExplore -from pyk.kore.rpc import FallbackReason, KoreClient, KoreExecLogFormat, TransportType, kore_server +from pyk.kore.rpc import KoreClient, KoreExecLogFormat, TransportType, kore_server from pyk.ktool import TypeInferenceMode from pyk.ktool.claim_loader import ClaimLoader from pyk.prelude.ml import is_bottom, is_top @@ -33,6 +33,7 @@ from pyk.kast.outer import KClaim, KDefinition from pyk.kcfg import KCFG from pyk.kcfg.semantics import KCFGSemantics + from pyk.kore.rpc import FallbackReason from pyk.ktool.kprint import KPrint from pyk.ktool.kprove import KProve from pyk.proof.proof import Proof @@ -355,7 +356,6 @@ def legacy_explore( no_post_exec_simplify: bool = True, ) -> Iterator[KCFGExplore]: bug_report_id = None if bug_report is None else id - fallback_on = [FallbackReason.ABORTED, FallbackReason.STUCK] if fallback_on is None else fallback_on if start_server: # Old way of handling KCFGExplore, to be removed with kore_server( From bb3c11bc58bd29d7012871dcb13d056538c50954 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Aug 2024 17:39:58 +0000 Subject: [PATCH 7/8] kevm_pyk/__main__: make sure not to set --no-post-exec-simplify for non-booster executions --- kevm-pyk/src/kevm_pyk/__main__.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 278f2cc78a..1199e9bd6d 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -233,8 +233,10 @@ def exec_prove(options: ProveOptions) -> None: if options.kore_rpc_command is None: if options.use_booster_dev: kore_rpc_command = ('booster-dev',) + options.post_exec_simplify = True elif not options.use_booster: kore_rpc_command = ('kore-rpc',) + options.post_exec_simplify = True else: kore_rpc_command = ('kore-rpc-booster',) if options.fallback_on is None: From 2205c68514d80f1b069501bfc22d60f27e8e6454 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 Aug 2024 18:07:15 +0000 Subject: [PATCH 8/8] kevm_pyk/test_prove: remove options which now have default handling --- kevm-pyk/src/tests/integration/test_prove.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 9e272524bf..35605a4260 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -9,7 +9,6 @@ from pyk.kast.att import AttEntry, Atts, KAtt from pyk.kast.outer import KClaim from pyk.kdist import kdist -from pyk.kore.rpc import FallbackReason from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofShow @@ -225,8 +224,6 @@ def _test_prove( 'break_on_basic_blocks': break_on_basic_blocks, 'workers': workers, 'direct_subproof_rules': direct_subproof_rules, - 'post_exec_simplify': False, - 'fallback_on': [FallbackReason.ABORTED, FallbackReason.STUCK], } ) exec_prove(options=options)