Update/generalize option to include lemmas at prove time (#979)

* src/kontrol/{cli,options,__main__}: add more general option --lemmas to RpcOptions, deprecate --extra-module

* src/{foundry,prove}: factor out logic for loading a lemmas modules

* src/kontrol/foundry: enable extra lemmas for all commands involving RPC server

* kontrol/{utils,foundry}: make sure to build modules that can be included at prove time

* kontrol/cli: correct CLI message

* src/kontrol/utils: correct the basic lemmas file

* src/kontrol/cli: correct help message

* src/kontrol/{cli,options}: remove k_gen_args and inline into build_args

* src/kontrol/foundry: correct build name

Author: ehildenb

src/kontrol/__main__.py

@@ -171,6 +171,12 @@ def exec_build(options: BuildOptions) -> None:
 def exec_prove(options: ProveOptions) -> None:
     _LOGGER.debug(options)
 
+    if options.extra_module is not None:
+        _LOGGER.warning('Option --extra-module is being deprecated in favor of option --lemmas.')
+        if options.lemmas is not None:
+            raise ValueError('Cannot specify both --extra-module and --lemmas, prefer --lemmas.')
+        options.lemmas = options.extra_module
+
     if options.recorded_diff_state_path and options.recorded_dump_state_path:
         raise AssertionError('Provide only one file for recorded state updates')
 

src/kontrol/cli.py

@@ -179,23 +179,6 @@ def foundry_test_args(self) -> ArgumentParser:
         args.add_argument('--version', type=int, required=False, help='Version of the test to use')
         return args
 
-    @cached_property
-    def k_gen_args(self) -> ArgumentParser:
-        args = ArgumentParser(add_help=False)
-        args.add_argument(
-            '--require',
-            dest='requires',
-            action='append',
-            help='Extra K requires to include in generated output.',
-        )
-        args.add_argument(
-            '--module-import',
-            dest='imports',
-            action='append',
-            help='Extra modules to import into generated main module.',
-        )
-        return args
-
     @cached_property
     def rpc_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)
@@ -239,6 +222,15 @@ def rpc_args(self) -> ArgumentParser:
             type=int,
             help='Use existing RPC server on named port.',
         )
+        args.add_argument(
+            '--lemmas',
+            dest='lemmas',
+            default=None,
+            help=(
+                'File and extra module to include for verification (which must import the KONTROL-MAIN module).'
+                'Format is <file>:<module name>.'
+            ),
+        )
         return args
 
 
@@ -266,7 +258,6 @@ def parse(s: str) -> list[T]:
         parents=[
             kontrol_cli_args.logging_args,
             kontrol_cli_args.k_args,
-            kontrol_cli_args.k_gen_args,
             kontrol_cli_args.kompile_args,
             kontrol_cli_args.foundry_args,
             config_args.config_args,
@@ -328,6 +319,18 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='Include auxiliary Kontrol lemmas.',
     )
+    build.add_argument(
+        '--require',
+        dest='requires',
+        action='append',
+        help='Extra K requires to include in generated output.',
+    )
+    build.add_argument(
+        '--module-import',
+        dest='imports',
+        action='append',
+        help='Extra modules to import into generated main module.',
+    )
 
     state_diff_args = command_parser.add_parser(
         'load-state',
@@ -569,10 +572,7 @@ def parse(s: str) -> list[T]:
         '--extra-module',
         dest='extra_module',
         default=None,
-        help=(
-            'File and extra module to include for verification (which must import KONTROL-MAIN module).'
-            'Format is <file>:<module name>.'
-        ),
+        help='Deprecated alias for --lemmas.',
     )
     prove_args.add_argument(
         '--symbolic-caller',

src/kontrol/foundry.py

@@ -30,7 +30,7 @@
     set_cell,
     top_down,
 )
-from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire
+from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire, KRule
 from pyk.kcfg import KCFG
 from pyk.kcfg.kcfg import Step
 from pyk.kcfg.minimize import KCFGMinimizer
@@ -552,6 +552,22 @@ def build(self, metadata: bool) -> None:
         except CalledProcessError as err:
             raise RuntimeError(f"Couldn't forge build! {err.stderr.strip()}") from err
 
+    def load_lemmas(self, lemmas_id: str | None) -> KFlatModule | None:
+        if lemmas_id is None:
+            return None
+        lemmas_file, lemmas_name, *_ = lemmas_id.split(':')
+        lemmas_path = Path(lemmas_file)
+        if not lemmas_path.is_file():
+            raise ValueError(f'Supplied lemmas path is not a file: {lemmas_path}')
+        modules = self.kevm.parse_modules(
+            lemmas_path, module_name=lemmas_name, include_dirs=(kdist.get('kontrol.base'),)
+        )
+        lemmas_module = single(module for module in modules.modules if module.name == lemmas_name)
+        non_rule_sentences = [sent for sent in lemmas_module.sentences if not isinstance(sent, KRule)]
+        if non_rule_sentences:
+            raise ValueError(f'Supplied lemmas module contains non-Rule sentences: {non_rule_sentences}')
+        return lemmas_module
+
     @cached_property
     def all_tests(self) -> list[str]:
         test_dir = os.path.join(self.profile.get('test', 'test'), '')
@@ -971,6 +987,7 @@ def foundry_show(
             smt_retry_limit=options.smt_retry_limit,
             start_server=start_server,
             port=options.port,
+            extra_module=foundry.load_lemmas(options.lemmas),
         ) as kcfg_explore:
             res_lines += print_failure_info(proof, kcfg_explore, options.counterexample_info)
             res_lines += Foundry.help_info()
@@ -1234,6 +1251,7 @@ def foundry_simplify_node(
         log_fail_rewrites=options.log_fail_rewrites,
         start_server=start_server,
         port=options.port,
+        extra_module=foundry.load_lemmas(options.lemmas),
     ) as kcfg_explore:
         new_term, _ = kcfg_explore.cterm_symbolic.simplify(cterm)
     if options.replace:
@@ -1322,6 +1340,7 @@ def foundry_step_node(
         log_fail_rewrites=options.log_fail_rewrites,
         start_server=start_server,
         port=options.port,
+        extra_module=foundry.load_lemmas(options.lemmas),
     ) as kcfg_explore:
         node = options.node
         for _i in range(options.repeat):
@@ -1398,6 +1417,7 @@ def foundry_section_edge(
         log_fail_rewrites=options.log_fail_rewrites,
         start_server=start_server,
         port=options.port,
+        extra_module=foundry.load_lemmas(options.lemmas),
     ) as kcfg_explore:
         kcfg_explore.section_edge(
             apr_proof.kcfg,
@@ -1449,6 +1469,7 @@ def foundry_get_model(
         log_fail_rewrites=options.log_fail_rewrites,
         start_server=start_server,
         port=options.port,
+        extra_module=foundry.load_lemmas(options.lemmas),
     ) as kcfg_explore:
         for node_id in nodes:
             res_lines.append('')

src/kontrol/options.py

@@ -63,6 +63,7 @@ class RpcOptions(Options):
     kore_rpc_command: str | None
     use_booster: bool
     port: int | None
+    lemmas: str | None
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -72,6 +73,7 @@ def default() -> dict[str, Any]:
             'kore_rpc_command': None,
             'use_booster': True,
             'port': None,
+            'lemmas': None,
         }
 
     @staticmethod
@@ -206,32 +208,6 @@ def get_argument_type() -> dict[str, Callable]:
         }
 
 
-class KGenOptions(Options):
-    requires: list[str]
-    imports: list[str]
-
-    @staticmethod
-    def default() -> dict[str, Any]:
-        return {
-            'requires': [],
-            'imports': [],
-        }
-
-    @staticmethod
-    def from_option_string() -> dict[str, str]:
-        return {
-            'require': 'requires',
-            'module-import': 'imports',
-        }
-
-    @staticmethod
-    def get_argument_type() -> dict[str, Callable]:
-        return {
-            'require': list_of(str),
-            'module-import': list_of(str),
-        }
-
-
 class KompileTargetOptions(Options):
     target: KompileTarget
 
@@ -836,14 +812,16 @@ def get_argument_type() -> dict[str, Callable]:
         )
 
 
-class BuildOptions(LoggingOptions, KOptions, KGenOptions, KompileOptions, FoundryOptions, KompileTargetOptions):
+class BuildOptions(LoggingOptions, KOptions, KompileOptions, FoundryOptions, KompileTargetOptions):
     regen: bool
     rekompile: bool
     forge_build: bool
     silence_warnings: bool
     metadata: bool
     keccak_lemmas: bool
     auxiliary_lemmas: bool
+    requires: list[str]
+    imports: list[str]
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -856,6 +834,8 @@ def default() -> dict[str, Any]:
             'metadata': True,
             'keccak_lemmas': True,
             'auxiliary_lemmas': False,
+            'requires': [],
+            'imports': [],
         }
 
     @staticmethod
@@ -864,7 +844,6 @@ def from_option_string() -> dict[str, str]:
             FoundryOptions.from_option_string()
             | LoggingOptions.from_option_string()
             | KOptions.from_option_string()
-            | KGenOptions.from_option_string()
             | KompileOptions.from_option_string()
             | KompileTargetOptions.from_option_string()
         )
@@ -875,7 +854,6 @@ def get_argument_type() -> dict[str, Callable]:
             FoundryOptions.get_argument_type()
             | LoggingOptions.get_argument_type()
             | KOptions.get_argument_type()
-            | KGenOptions.get_argument_type()
             | KompileOptions.get_argument_type()
             | KompileTargetOptions.get_argument_type()
         )

src/kontrol/prove.py

@@ -6,7 +6,6 @@
 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
 
@@ -17,7 +16,6 @@
 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, kore_server
@@ -32,7 +30,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, single, unique
+from pyk.utils import hash_str, run_process_2, unique
 from rich.progress import Progress, SpinnerColumn, TaskID, TextColumn, TimeElapsedColumn
 
 from .foundry import Foundry, KontrolSemantics, foundry_to_xml
@@ -438,17 +436,7 @@ 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}')
+            lemmas_module = foundry.load_lemmas(options.lemmas)
 
             if progress is not None and task is not None:
                 progress.update(
@@ -471,7 +459,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 task_id=task,
                 maintenance_rate=options.maintenance_rate,
                 assume_defined=options.assume_defined,
-                extra_module=extra_lemmas_module,
+                extra_module=lemmas_module,
                 optimize_kcfg=options.optimize_kcfg,
             )
 

src/kontrol/utils.py

@@ -146,9 +146,10 @@ def append_to_file(file_path: Path, content: str) -> None:
 
 
 def empty_lemmas_file_contents() -> str:
-    return """requires "foundry.md"
+    return """requires "kontrol.md"
 
 module KONTROL-LEMMAS
+    imports KONTROL-BASE
 
 // Your lemmas go here
 // Not sure what to do next? Try checking the documentation for writing lemmas: https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/kevm-lemmas

src/tests/integration/test_foundry_prove.py

@@ -1006,7 +1006,7 @@ def test_foundry_extra_lemmas(
                 'break_on_calls': True,
                 'port': server.port,
                 'force_sequential': force_sequential,
-                'extra_module': f'{TEST_DATA_DIR / lemmas_file}:XOR-LEMMAS',
+                'lemmas': f'{TEST_DATA_DIR / lemmas_file}:XOR-LEMMAS',
             }
         ),
     )