Skip to content

Optimize how we run proofs with booster #2571

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 9 commits into
base: master
Choose a base branch
from
Draft

Optimize how we run proofs with booster #2571

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
9fbf4e9
tests/specs/examples: replace symbol(), klabel(X) with symbol(X)
ehildenb Aug 9, 2024
0cb068f
kevm_pyk/test_prove: optimize how we run the proofs
ehildenb Aug 9, 2024
f350719
kevm_pyk/{cli,utils}: set defaults for CLI to fastest options too
ehildenb Aug 9, 2024
43dde61
Set Version: 1.0.678
rv-auditor Aug 9, 2024
d5e28ac
kevm_pyk/utils: correct imports
ehildenb Aug 9, 2024
bd2958f
kevm_pyk/{utils,cli,__main__}: only pass fallback reasons for booster…
ehildenb Aug 9, 2024
bb3c11b
kevm_pyk/__main__: make sure not to set --no-post-exec-simplify for n…
ehildenb Aug 9, 2024
2205c68
kevm_pyk/test_prove: remove options which now have default handling
ehildenb Aug 9, 2024
f6477eb
Merge branch 'master' into optimize-proofs
anvacaru Aug 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion kevm-pyk/src/kevm_pyk/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -233,10 +233,14 @@ 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:
options.fallback_on = [FallbackReason.ABORTED, FallbackReason.STUCK]
elif isinstance(options.kore_rpc_command, str):
kore_rpc_command = tuple(options.kore_rpc_command.split())
else:
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/cli.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ def default() -> dict[str, Any]:
'kore_rpc_command': None,
'use_booster': True,
'fallback_on': [],
'post_exec_simplify': True,
'post_exec_simplify': False,
'interim_simplification': None,
'port': None,
'maude_port': None,
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/utils.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -354,7 +354,7 @@ 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
if start_server:
Expand Down
34 changes: 17 additions & 17 deletions tests/specs/examples/erc20-bin-runtime.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )

Expand All @@ -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 )
Expand Down
Loading
Loading