From 564eef6fde55ac46582c13ca6e2df50976fb1553 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 28 Nov 2024 01:29:28 +0700 Subject: [PATCH] Option `--extra-module` for including lemmas modules dynamically in `kontrol prove` (#883) * kontrol/: remove maude backend dispatch option * kontrol/{cli,options,prove}: add CLI option for threading through extra module to Prover * tests/integration/{test-data,test_foundry_prove}: add test of including extra lemmas at prove time * Expected output update * Update src/kontrol/prove.py Co-authored-by: Palina --------- Co-authored-by: Palina --- src/kontrol/cli.py | 28 +++++---------- src/kontrol/foundry.py | 5 --- src/kontrol/options.py | 4 +-- src/kontrol/prove.py | 31 +++++++++-------- .../integration/test-data/foundry-prove-all | 1 + .../integration/test-data/foundry-prove-skip | 1 + .../test-data/foundry/test/Arithmetic.t.sol | 6 ++++ .../test-data/show/contracts.k.expected | 11 ++++++ src/tests/integration/test-data/xor-lemmas.k | 6 ++++ src/tests/integration/test_foundry_prove.py | 34 +++++++++++++++++++ src/tests/unit/test-data/kontrol_test.toml | 3 +- 11 files changed, 88 insertions(+), 42 deletions(-) create mode 100644 src/tests/integration/test-data/xor-lemmas.k diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 6ea7abd2a..559bdff29 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -6,7 +6,6 @@ from typing import TYPE_CHECKING, Any from kevm_pyk.cli import KEVMCLIArgs, node_id_like -from kevm_pyk.kompile import KompileTarget from kevm_pyk.utils import arg_pair_of from pyk.cli.utils import dir_path, file_path from pyk.utils import ensure_dir_path @@ -201,17 +200,6 @@ def k_gen_args(self) -> ArgumentParser: ) return args - @cached_property - def kompile_target_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( - '--target', - type=KompileTarget, - choices=[KompileTarget.HASKELL, KompileTarget.MAUDE], - help='[haskell|maude]', - ) - return args - @cached_property def rpc_args(self) -> ArgumentParser: args = ArgumentParser(add_help=False) @@ -255,12 +243,6 @@ def rpc_args(self) -> ArgumentParser: type=int, help='Use existing RPC server on named port.', ) - args.add_argument( - '--maude-port', - dest='maude_port', - type=int, - help='Use existing Maude RPC server on named port.', - ) return args @@ -304,7 +286,6 @@ def parse(s: str) -> list[T]: kontrol_cli_args.k_gen_args, kontrol_cli_args.kompile_args, kontrol_cli_args.foundry_args, - kontrol_cli_args.kompile_target_args, config_args.config_args, ], ) @@ -588,6 +569,15 @@ def parse(s: str) -> list[T]: 'Assumes running Solidity-compiled bytecode cannot result in a stack overflow/underflow.' ), ) + prove_args.add_argument( + '--extra-module', + dest='extra_module', + default=None, + help=( + 'File and extra module to include for verification (which must import FOUNDRY-MAIN module).' + 'Format is :.' + ), + ) show_args = command_parser.add_parser( 'show', diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 73c89ca7e..a690ea6fd 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -847,7 +847,6 @@ def foundry_show( smt_retry_limit=options.smt_retry_limit, start_server=start_server, port=options.port, - maude_port=options.maude_port, ) as kcfg_explore: res_lines += print_failure_info(proof, kcfg_explore, options.counterexample_info) res_lines += Foundry.help_info() @@ -1111,7 +1110,6 @@ def foundry_simplify_node( log_fail_rewrites=options.log_fail_rewrites, start_server=start_server, port=options.port, - maude_port=options.maude_port, ) as kcfg_explore: new_term, _ = kcfg_explore.cterm_symbolic.simplify(cterm) if options.replace: @@ -1200,7 +1198,6 @@ def foundry_step_node( log_fail_rewrites=options.log_fail_rewrites, start_server=start_server, port=options.port, - maude_port=options.maude_port, ) as kcfg_explore: node = options.node for _i in range(options.repeat): @@ -1277,7 +1274,6 @@ def foundry_section_edge( log_fail_rewrites=options.log_fail_rewrites, start_server=start_server, port=options.port, - maude_port=options.maude_port, ) as kcfg_explore: kcfg_explore.section_edge( apr_proof.kcfg, @@ -1329,7 +1325,6 @@ def foundry_get_model( log_fail_rewrites=options.log_fail_rewrites, start_server=start_server, port=options.port, - maude_port=options.maude_port, ) as kcfg_explore: for node_id in nodes: res_lines.append('') diff --git a/src/kontrol/options.py b/src/kontrol/options.py index de3550c98..016be5706 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -63,7 +63,6 @@ class RpcOptions(Options): kore_rpc_command: str | None use_booster: bool port: int | None - maude_port: int | None @staticmethod def default() -> dict[str, Any]: @@ -73,7 +72,6 @@ def default() -> dict[str, Any]: 'kore_rpc_command': None, 'use_booster': True, 'port': None, - 'maude_port': None, } @@ -386,6 +384,7 @@ class ProveOptions( remove_old_proofs: bool optimize_performance: int | None stack_checks: bool + extra_module: str | None def __init__(self, args: dict[str, Any]) -> None: super().__init__(args) @@ -415,6 +414,7 @@ def default() -> dict[str, Any]: 'remove_old_proofs': False, 'optimize_performance': None, 'stack_checks': True, + 'extra_module': None, } @staticmethod diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index f27de5c46..3f0446730 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -6,6 +6,7 @@ from collections import Counter from copy import copy from functools import partial +from pathlib import Path from subprocess import CalledProcessError from typing import TYPE_CHECKING, Any, ContextManager, NamedTuple @@ -16,9 +17,10 @@ from pyk.cterm import CTerm, CTermSymbolic from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst from pyk.kast.manip import flatten_label, free_vars, set_cell +from pyk.kast.outer import KFlatModule, KRule from pyk.kcfg import KCFG, KCFGExplore from pyk.kcfg.minimize import KCFGMinimizer -from pyk.kore.rpc import KoreClient, TransportType, kore_server +from pyk.kore.rpc import KoreClient, kore_server from pyk.prelude.bytes import bytesToken from pyk.prelude.collections import list_empty, map_empty, map_item, map_of, set_empty from pyk.prelude.k import GENERATED_TOP_CELL @@ -30,7 +32,7 @@ from pyk.proof import ProofStatus from pyk.proof.proof import Proof from pyk.proof.reachability import APRFailureInfo, APRProof -from pyk.utils import hash_str, run_process_2, unique +from pyk.utils import hash_str, run_process_2, single, unique from rich.progress import Progress, SpinnerColumn, TaskID, TextColumn, TimeElapsedColumn from .foundry import Foundry, foundry_to_xml @@ -364,24 +366,12 @@ def select_server() -> OptionalKoreServer: with select_server() as server: def create_kcfg_explore() -> KCFGExplore: - if options.maude_port is None: - dispatch = None - else: - dispatch = { - 'execute': [('localhost', options.maude_port, TransportType.HTTP)], - 'simplify': [('localhost', options.maude_port, TransportType.HTTP)], - 'add-module': [ - ('localhost', options.maude_port, TransportType.HTTP), - ('localhost', server.port(), TransportType.SINGLE_SOCKET), - ], - } bug_report_id = None if options.bug_report is None else test.id client = KoreClient( 'localhost', server.port(), bug_report=options.bug_report, bug_report_id=bug_report_id, - dispatch=dispatch, ) cterm_symbolic = CTermSymbolic( client, @@ -451,6 +441,18 @@ def create_kcfg_explore() -> KCFGExplore: rule.label for rule in foundry.kevm.definition.all_modules_dict['KONTROL-ASSERTIONS'].rules ) + extra_lemmas_module: KFlatModule | None = None + if options.extra_module: + extra_module_file, extra_module_name, *_ = options.extra_module.split(':') + extra_module_path = Path(extra_module_file) + if not extra_module_path.is_file(): + raise ValueError(f'Supplied --extra-module path is not a file: {extra_module_path}') + modules = foundry.kevm.parse_modules(extra_module_path, module_name=extra_module_name) + extra_lemmas_module = single(module for module in modules.modules if module.name == extra_module_name) + non_rule_sentences = [sent for sent in extra_lemmas_module.sentences if not isinstance(sent, KRule)] + if non_rule_sentences: + raise ValueError(f'Supplied --extra-module contains non-Rule sentences: {non_rule_sentences}') + if progress is not None and task is not None: progress.update( task, @@ -472,6 +474,7 @@ def create_kcfg_explore() -> KCFGExplore: task_id=task, maintenance_rate=options.maintenance_rate, assume_defined=options.assume_defined, + extra_module=extra_lemmas_module, ) if progress is not None and task is not None: diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index 902e40937..e7add4429 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/src/tests/integration/test-data/foundry-prove-all @@ -40,6 +40,7 @@ ArithmeticTest.test_wmul_rounding(uint256,uint256) ArithmeticTest.test_wmul_wdiv_inverse(uint256,uint256) ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256) ArithmeticTest.test_wmul_weakly_increasing_positive(uint256,uint256) +ArithmeticTest.test_xor(uint256,uint256) AssertTest.test_assert_false() AssertTest.test_assert_true() AssertTest.prove_assert_true() diff --git a/src/tests/integration/test-data/foundry-prove-skip b/src/tests/integration/test-data/foundry-prove-skip index 55ab9ad42..c4f39567b 100644 --- a/src/tests/integration/test-data/foundry-prove-skip +++ b/src/tests/integration/test-data/foundry-prove-skip @@ -23,6 +23,7 @@ ArithmeticTest.test_wmul_rounding(uint256,uint256) ArithmeticTest.test_wmul_wdiv_inverse(uint256,uint256) ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256) ArithmeticTest.test_wmul_weakly_increasing_positive(uint256,uint256) +ArithmeticTest.test_xor(uint256,uint256) AssertTest.test_assert_false() AssertTest.testFail_assert_true() AssertTest.testFail_expect_revert() diff --git a/src/tests/integration/test-data/foundry/test/Arithmetic.t.sol b/src/tests/integration/test-data/foundry/test/Arithmetic.t.sol index 9ebbe5174..339a8fbef 100644 --- a/src/tests/integration/test-data/foundry/test/Arithmetic.t.sol +++ b/src/tests/integration/test-data/foundry/test/Arithmetic.t.sol @@ -23,6 +23,12 @@ contract ArithmeticTest is Test { assertEq(c + 1, a); } + function test_xor(uint256 a, uint256 b) external { + vm.assume(a == b); + uint256 res = a ^ b; + assertEq(res, 0); + } + function max2(uint256 x, uint256 y) internal pure returns (uint256) { if (x < y && x != 2**100 - 1337) { return y; diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index 37be9e4fb..710ba3295 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -677,6 +677,8 @@ module S2KtestZModArithmeticTest-CONTRACT syntax S2KtestZModArithmeticTestMethod ::= "S2KtestZUndwmulZUndweaklyZUndincreasingZUndpositive" "(" Int ":" "uint256" "," Int ":" "uint256" ")" [symbol("method_test%ArithmeticTest_S2KtestZUndwmulZUndweaklyZUndincreasingZUndpositive_uint256_uint256")] + syntax S2KtestZModArithmeticTestMethod ::= "S2KtestZUndxor" "(" Int ":" "uint256" "," Int ":" "uint256" ")" [symbol("method_test%ArithmeticTest_S2KtestZUndxor_uint256_uint256")] + rule ( S2KtestZModArithmeticTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) ) @@ -785,6 +787,12 @@ module S2KtestZModArithmeticTest-CONTRACT )) + rule ( S2KtestZModArithmeticTest . S2KtestZUndxor ( KV0_a : uint256 , KV1_b : uint256 ) => #abiCallData ( "test_xor" , ( #uint256 ( KV0_a ) , ( #uint256 ( KV1_b ) , .TypedArgs ) ) ) ) + ensures ( #rangeUInt ( 256 , KV0_a ) + andBool ( #rangeUInt ( 256 , KV1_b ) + )) + + rule ( selector ( "IS_TEST()" ) => 4202047188 ) @@ -853,6 +861,9 @@ module S2KtestZModArithmeticTest-CONTRACT rule ( selector ( "test_wmul_weakly_increasing_positive(uint256,uint256)" ) => 1421647895 ) + + rule ( selector ( "test_xor(uint256,uint256)" ) => 2156875273 ) + endmodule diff --git a/src/tests/integration/test-data/xor-lemmas.k b/src/tests/integration/test-data/xor-lemmas.k new file mode 100644 index 000000000..3c83b9f9f --- /dev/null +++ b/src/tests/integration/test-data/xor-lemmas.k @@ -0,0 +1,6 @@ +module XOR-LEMMAS + imports FOUNDRY-MAIN + + rule A xorInt A => 0 [simplification] + +endmodule diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index 946f5036d..e41b51280 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -985,6 +985,40 @@ def test_foundry_refute_node( assert_pass(test, single(prove_res_3)) +def test_foundry_extra_lemmas( + foundry: Foundry, + update_expected_output: bool, + bug_report: BugReport | None, + server: KoreServer, + no_use_booster: bool, + force_sequential: bool, +) -> None: + if no_use_booster: + pytest.skip() + + test = 'ArithmeticTest.test_xor(uint256,uint256)' + lemmas_file = 'xor-lemmas.k' + + if bug_report is not None: + server._populate_bug_report(bug_report) + + prove_res = foundry_prove( + foundry=foundry, + options=ProveOptions( + { + 'tests': [(test, None)], + 'bug_report': bug_report, + 'break_on_calls': True, + 'port': server.port, + 'force_sequential': force_sequential, + 'extra_module': f'{TEST_DATA_DIR / lemmas_file}:XOR-LEMMAS', + } + ), + ) + + assert_pass(test, single(prove_res)) + + def test_foundry_xml_report( foundry: Foundry, bug_report: BugReport | None, diff --git a/src/tests/unit/test-data/kontrol_test.toml b/src/tests/unit/test-data/kontrol_test.toml index 10347e033..6c6dd8a85 100644 --- a/src/tests/unit/test-data/kontrol_test.toml +++ b/src/tests/unit/test-data/kontrol_test.toml @@ -7,7 +7,6 @@ foundry-project-root = '.' verbose = false debug = false optimization-level = 3 -target = 'maude' [prove.b_profile] verbose = true @@ -19,4 +18,4 @@ smt-timeout = 1000 version = 3 verbose = true debug = true -node-delta = '10,#target' \ No newline at end of file +node-delta = '10,#target'