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 <[email protected]> --------- Co-authored-by: Palina <[email protected]>
runtimeverification · Nov 27, 2024 · 564eef6 · 564eef6
1 parent 853ef88
commit 564eef6
Show file tree

Hide file tree

Showing 11 changed files with 88 additions and 42 deletions.
diff --git 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 <file>:<module name>.'
+        ),
+    )
 
     show_args = command_parser.add_parser(
         'show',

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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'
+node-delta              = '10,#target'