Initial manual implementation of CSE

package/version

@@ -1 +1 @@
-0.1.140
+0.1.141

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.140"
+version = "0.1.141"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.140'
+VERSION: Final = '0.1.141'

src/kontrol/__main__.py

@@ -216,6 +216,7 @@ def exec_prove(
     max_iterations: int | None = None,
     reinit: bool = False,
     tests: Iterable[tuple[str, int | None]] = (),
+    include_summaries: Iterable[tuple[str, int | None]] = (),
     workers: int = 1,
     break_every_step: bool = False,
     break_on_jumpi: bool = False,
@@ -294,6 +295,7 @@ def exec_prove(
         prove_options=prove_options,
         rpc_options=rpc_options,
         tests=tests,
+        include_summaries=include_summaries,
     )
     failed = 0
     for proof in results:
@@ -777,6 +779,14 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
         type=file_path,
         help='Path to JSON file containing the summary of the deployment process used for the project.',
     )
+    prove_args.add_argument(
+        '--include-summary',
+        type=_parse_test_version_tuple,
+        dest='include_summaries',
+        default=[],
+        action='append',
+        help='Specify a summary to include as a lemma.',
+    )
 
     show_args = command_parser.add_parser(
         'show',

src/kontrol/prove.py

@@ -44,6 +44,7 @@ def foundry_prove(
     prove_options: ProveOptions,
     rpc_options: RPCOptions,
     tests: Iterable[tuple[str, int | None]] = (),
+    include_summaries: Iterable[tuple[str, int | None]] = (),
 ) -> list[APRProof]:
     if prove_options.workers <= 0:
         raise ValueError(f'Must have at least one worker, found: --workers {prove_options.workers}')
@@ -62,6 +63,15 @@ def foundry_prove(
 
     foundry.mk_proofs_dir()
 
+    summary_ids = (
+        [
+            foundry.get_apr_proof(include_summary.id).id
+            for include_summary in collect_tests(foundry, include_summaries, reinit=False)
+        ]
+        if include_summaries
+        else []
+    )
+
     test_suite = collect_tests(foundry, tests, reinit=prove_options.reinit)
     test_names = [test.name for test in test_suite]
     print(f'Running functions: {test_names}')
@@ -87,30 +97,31 @@ def foundry_prove(
     for test in constructor_tests:
         test.method.update_digest(foundry.digest_file)
 
-    def _run_prover(_test_suite: list[FoundryTest]) -> list[APRProof]:
+    def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False) -> list[APRProof]:
         return _run_cfg_group(
             tests=_test_suite,
             foundry=foundry,
             prove_options=prove_options,
             rpc_options=rpc_options,
+            summary_ids=(summary_ids if include_summaries else []),
         )
 
     if prove_options.run_constructor:
         _LOGGER.info(f'Running initialization code for contracts in parallel: {constructor_names}')
-        results = _run_prover(constructor_tests)
+        results = _run_prover(constructor_tests, include_summaries=False)
         failed = [proof for proof in results if not proof.passed]
         if failed:
             raise ValueError(f'Running initialization code failed for {len(failed)} contracts: {failed}')
 
     _LOGGER.info(f'Running setup functions in parallel: {setup_method_names}')
-    results = _run_prover(setup_method_tests)
+    results = _run_prover(setup_method_tests, include_summaries=False)
 
     failed = [proof for proof in results if not proof.passed]
     if failed:
         raise ValueError(f'Running setUp method failed for {len(failed)} contracts: {failed}')
 
     _LOGGER.info(f'Running test functions in parallel: {test_names}')
-    results = _run_prover(test_suite)
+    results = _run_prover(test_suite, include_summaries=True)
     return results
 
 
@@ -185,6 +196,7 @@ def _run_cfg_group(
     foundry: Foundry,
     prove_options: ProveOptions,
     rpc_options: RPCOptions,
+    summary_ids: Iterable[str],
 ) -> list[APRProof]:
     def init_and_run_proof(test: FoundryTest) -> APRFailureInfo | None:
         if Proof.proof_data_exists(test.id, foundry.proofs_dir):
@@ -214,6 +226,7 @@ def init_and_run_proof(test: FoundryTest) -> APRFailureInfo | None:
                 run_constructor=prove_options.run_constructor,
                 use_gas=prove_options.use_gas,
                 summary_entries=prove_options.summary_entries,
+                summary_ids=summary_ids,
             )
 
             cut_point_rules = KEVMSemantics.cut_point_rules(
@@ -268,6 +281,7 @@ def method_to_apr_proof(
     run_constructor: bool = False,
     use_gas: bool = False,
     summary_entries: Iterable[SummaryEntry] | None = None,
+    summary_ids: Iterable[str] = (),
 ) -> APRProof:
     if Proof.proof_data_exists(test.id, foundry.proofs_dir):
         apr_proof = foundry.get_apr_proof(test.id)
@@ -303,9 +317,12 @@ def method_to_apr_proof(
             {},
             bmc_depth,
             proof_dir=foundry.proofs_dir,
+            subproof_ids=summary_ids,
         )
     else:
-        apr_proof = APRProof(test.id, kcfg, [], init_node_id, target_node_id, {}, proof_dir=foundry.proofs_dir)
+        apr_proof = APRProof(
+            test.id, kcfg, [], init_node_id, target_node_id, {}, proof_dir=foundry.proofs_dir, subproof_ids=summary_ids
+        )
 
     apr_proof.write_proof_data()
     return apr_proof