Factor out vat arithmetic in proof-reuse for MCD (#2467)

* tests/specs/mcd/vat-arithmetic-spec: single spec file with all vat arithmetic specs

* tests/specs/mcd/vat-spec.k: add single file incorporating all VAT proofs

* tests/specs/mcd/vat-*: update vat specs with more dependencies

* tests/specs/mcd/flopper-cage-pass: formatting

* tests/specs/mcd/vat-*: update with more dependency proofs

* tests/specs/mcd/vat-spec: add missing spec

* tests/specs/mcd/vat-arithmetic-spec: update <useGas> cell, remove unused cells

* tests/specs/mcd: remove now-redundant vat arithmetic pass proofs

* tests/failing: update failing lists

* tests/specs/mcd/vat-flux-diff-pass-spec.k: add useGas cell

* tests/specs/mcd: add useGas cell in several places

* tests/specs/mcd/vat*: reuse specs from vat-arithmetic-spec file

* tests/specs/mcd/vat-spec: update to list all Vat proofs

* tests/specs/mcd: remove exit-code cell from specs

* tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k: add other needed dependencies

* kevm-pyk/kevm: add dummy merge-nodes heuristic

* Makefile, kevm-pyk/: add test of DSS spec reuse

* .github/test-pr: add job for spec-reuse proofs

* tests/test_prove: tests/failing: remove tests/specs/mcd/vat-* from test-pyk-prove test-suite

* kevm-pyk/{utils,cli,__main__,test_prove}: use new field direct_subproof_rules to run test-prove-dss

* Set Version: 1.0.599

* Set Version: 1.0.602

* Revert "kevm-pyk/kevm: add dummy merge-nodes heuristic"

This reverts commit 41a0499.

* kevm-pyk/{conftest,test_prove}: hardcode the number of workers for dss test

---------

Co-authored-by: devops <[email protected]>

.github/workflows/test-pr.yml

@@ -125,6 +125,9 @@ jobs:
           - test-suite: 'test-prove-optimizations'
             test-args:
             timeout: 45
+          - test-suite: 'test-prove-dss'
+            test-args:
+            timeout: 45
     timeout-minutes: ${{ matrix.timeout }}
     steps:
       - name: 'Check out code'

Makefile

@@ -27,7 +27,7 @@ kevm-pyk: poetry-env
 # Tests
 # -----
 
-test: test-integration test-conformance test-prove test-prove-pyk test-prove-kprove test-interactive
+test: test-integration test-conformance test-prove test-prove-pyk test-prove-kprove test-prove-dss test-interactive
 
 
 # Conformance Tests
@@ -50,7 +50,7 @@ test-rest-bchain: poetry
 
 # Proof Tests
 
-test-prove: test-prove-pyk test-prove-kprove test-prove-optimizations
+test-prove: test-prove-pyk test-prove-kprove test-prove-optimizations test-prove-dss
 
 test-prove-pyk: poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_pyk_prove"
@@ -61,6 +61,9 @@ test-prove-kprove: poetry
 test-prove-optimizations: poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_optimizations"
 
+test-prove-dss: poetry
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_dss"
+
 
 # Integration Tests
 

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.601"
+version = "1.0.602"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

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

kevm-pyk/src/kevm_pyk/__main__.py

@@ -381,6 +381,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 fail_fast=options.fail_fast,
                 always_check_subsumption=options.always_check_subsumption,
                 fast_check_subsumption=options.fast_check_subsumption,
+                direct_subproof_rules=options.direct_subproof_rules,
                 max_frontier_parallel=options.max_frontier_parallel,
             )
             end_time = time.time()

kevm-pyk/src/kevm_pyk/cli.py

@@ -416,13 +416,15 @@ class KProveOptions(Options):
     debug_equations: list[str]
     always_check_subsumption: bool
     fast_check_subsumption: bool
+    direct_subproof_rules: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
         return {
             'debug_equations': [],
             'always_check_subsumption': True,
             'fast_check_subsumption': False,
+            'direct_subproof_rules': False,
         }
 
 
@@ -907,6 +909,13 @@ def kprove_args(self) -> ArgumentParser:
             action='store_true',
             help='Use fast-check on k-cell to determine subsumption (experimental).',
         )
+        args.add_argument(
+            '--direct-subproof-rules',
+            dest='direct_subproof_rules',
+            default=None,
+            action='store_true',
+            help='For passing subproofs, construct lemmas directly from initial to target state.',
+        )
         return args
 
     @cached_property

kevm-pyk/src/kevm_pyk/utils.py

@@ -105,6 +105,7 @@ class RunProverParams:
     counterexample_info: bool
     always_check_subsumption: bool
     fast_check_subsumption: bool
+    direct_subproof_rules: bool
 
 
 class APRProofStrategy(ABC):
@@ -141,6 +142,7 @@ def create_prover() -> APRProver:
                 counterexample_info=self.params.counterexample_info,
                 always_check_subsumption=self.params.always_check_subsumption,
                 fast_check_subsumption=self.params.fast_check_subsumption,
+                direct_subproof_rules=self.params.direct_subproof_rules,
             )
 
         parallel_advance_proof(
@@ -168,6 +170,7 @@ def prove(self, proof: APRProof, max_iterations: int | None = None, fail_fast: b
             counterexample_info=self.params.counterexample_info,
             always_check_subsumption=self.params.always_check_subsumption,
             fast_check_subsumption=self.params.fast_check_subsumption,
+            direct_subproof_rules=self.params.direct_subproof_rules,
         )
         prover.advance_proof(fail_fast=fail_fast, max_iterations=max_iterations, proof=proof)
 
@@ -215,6 +218,7 @@ def run_prover(
     counterexample_info: bool = False,
     always_check_subsumption: bool = False,
     fast_check_subsumption: bool = False,
+    direct_subproof_rules: bool = False,
     max_frontier_parallel: int = 1,
 ) -> bool:
     prover: APRProver | ImpliesProver
@@ -231,6 +235,7 @@ def run_prover(
                     execute_depth=max_depth,
                     fast_check_subsumption=fast_check_subsumption,
                     terminal_rules=terminal_rules,
+                    direct_subproof_rules=direct_subproof_rules,
                 ),
             )
             strategy.prove(fail_fast=fail_fast, max_iterations=max_iterations, proof=proof)

kevm-pyk/src/tests/integration/test_prove.py

@@ -2,6 +2,7 @@
 
 import logging
 import sys
+from pathlib import Path
 from typing import TYPE_CHECKING, NamedTuple
 
 import pytest
@@ -24,7 +25,6 @@
 
 if TYPE_CHECKING:
     from collections.abc import Callable
-    from pathlib import Path
     from typing import Any, Final
 
     from pyk.utils import BugReport
@@ -57,6 +57,8 @@ def spec_files(dir_name: str, glob: str) -> tuple[Path, ...]:
 ERC20_TESTS: Final = spec_files('erc20', '*/*-spec.k')
 EXAMPLES_TESTS: Final = spec_files('examples', '*-spec.k') + spec_files('examples', '*-spec.md')
 MCD_TESTS: Final = spec_files('mcd', '*-spec.k')
+VAT_TESTS: Final = spec_files('mcd', 'vat*-spec.k')
+NON_VAT_MCD_TESTS: Final = tuple(test for test in MCD_TESTS if test not in VAT_TESTS)
 KONTROL_TESTS: Final = spec_files('kontrol', '*-spec.k')
 
 ALL_TESTS: Final = sum(
@@ -65,7 +67,7 @@ def spec_files(dir_name: str, glob: str) -> tuple[Path, ...]:
         FUNCTIONAL_TESTS,
         ERC20_TESTS,
         EXAMPLES_TESTS,
-        MCD_TESTS,
+        NON_VAT_MCD_TESTS,
         KONTROL_TESTS,
     ],
     (),
@@ -357,6 +359,48 @@ def _get_optimization_proofs() -> list[APRProof]:
             assert proof.passed
 
 
+def test_prove_dss(
+    kompiled_target_for: Callable[[Path], Path],
+    tmp_path: Path,
+    caplog: LogCaptureFixture,
+    bug_report: BugReport | None,
+    spec_name: str | None,
+) -> None:
+    spec_file = Path('../tests/specs/mcd/vat-spec.k')
+    caplog.set_level(logging.INFO)
+
+    if spec_name is not None and str(spec_file).find(spec_name) < 0:
+        pytest.skip()
+
+    # Given
+    log_file = tmp_path / 'log.txt'
+    use_directory = tmp_path / 'kprove'
+    use_directory.mkdir()
+
+    # When
+    try:
+        definition_dir = kompiled_target_for(spec_file)
+        options = ProveOptions(
+            {
+                'spec_file': spec_file,
+                'definition_dir': definition_dir,
+                'includes': [str(include_dir) for include_dir in config.INCLUDE_DIRS],
+                'save_directory': use_directory,
+                'md_selector': 'foo',  # TODO Ignored flag, this is to avoid KeyError
+                'use_booster': True,
+                'bug_report': bug_report,
+                'break_on_calls': False,
+                'workers': 8,
+                'direct_subproof_rules': True,
+            }
+        )
+        exec_prove(options=options)
+    except BaseException:
+        raise
+    finally:
+        log_file.write_text(caplog.text)
+
+
 # ------------
 # Legacy tests
 # ------------

package/version

@@ -1 +1 @@
-1.0.601
+1.0.602

tests/failing-symbolic.haskell

@@ -114,19 +114,5 @@ tests/specs/mcd/flopper-kick-pass-rough-spec.k
 tests/specs/mcd/flopper-tick-pass-rough-spec.k
 tests/specs/mcd/functional-spec.k
 tests/specs/mcd/pot-join-pass-rough-spec.k
-tests/specs/mcd/vat-addui-fail-rough-spec.k
-tests/specs/mcd/vat-addui-pass-spec.k
-tests/specs/mcd/vat-deny-diff-fail-rough-spec.k
-tests/specs/mcd/vat-flux-diff-pass-rough-spec.k
-tests/specs/mcd/vat-fold-pass-rough-spec.k
-tests/specs/mcd/vat-fork-diff-pass-rough-spec.k
-tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k
-tests/specs/mcd/vat-move-diff-rough-spec.k
-tests/specs/mcd/vat-mului-pass-spec.k
-tests/specs/mcd/vat-muluu-pass-spec.k
-tests/specs/mcd/vat-slip-pass-rough-spec.k
-tests/specs/mcd/vat-subui-fail-rough-spec.k
-tests/specs/mcd/vat-subui-pass-rough-spec.k
-tests/specs/mcd/vat-subui-pass-spec.k
 tests/specs/mcd/vow-fess-fail-rough-spec.k
 tests/specs/mcd/vow-flog-fail-rough-spec.k

tests/failing-symbolic.haskell-booster

@@ -3,6 +3,3 @@ tests/specs/examples/sum-to-n-foundry-spec.k
 tests/specs/examples/sum-to-n-spec.k
 tests/specs/functional/merkle-spec.k
 tests/specs/functional/storageRoot-spec.k
-tests/specs/mcd/vat-fold-pass-rough-spec.k
-tests/specs/mcd/vat-fork-diff-pass-rough-spec.k
-tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k

tests/failing-symbolic.haskell-booster-dev

@@ -111,19 +111,5 @@ tests/specs/mcd/flopper-kick-pass-rough-spec.k
 tests/specs/mcd/flopper-tick-pass-rough-spec.k
 tests/specs/mcd/functional-spec.k
 tests/specs/mcd/pot-join-pass-rough-spec.k
-tests/specs/mcd/vat-addui-fail-rough-spec.k
-tests/specs/mcd/vat-addui-pass-spec.k
-tests/specs/mcd/vat-deny-diff-fail-rough-spec.k
-tests/specs/mcd/vat-flux-diff-pass-rough-spec.k
-tests/specs/mcd/vat-fold-pass-rough-spec.k
-tests/specs/mcd/vat-fork-diff-pass-rough-spec.k
-tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k
-tests/specs/mcd/vat-move-diff-rough-spec.k
-tests/specs/mcd/vat-mului-pass-spec.k
-tests/specs/mcd/vat-muluu-pass-spec.k
-tests/specs/mcd/vat-slip-pass-rough-spec.k
-tests/specs/mcd/vat-subui-fail-rough-spec.k
-tests/specs/mcd/vat-subui-pass-rough-spec.k
-tests/specs/mcd/vat-subui-pass-spec.k
 tests/specs/mcd/vow-fess-fail-rough-spec.k
 tests/specs/mcd/vow-flog-fail-rough-spec.k

tests/failing-symbolic.pyk

@@ -55,11 +55,5 @@ tests/specs/mcd/flopper-kick-pass-rough-spec.k
 tests/specs/mcd/flopper-tick-pass-rough-spec.k
 tests/specs/mcd/functional-spec.k
 tests/specs/mcd/pot-join-pass-rough-spec.k
-tests/specs/mcd/vat-flux-diff-pass-rough-spec.k
-tests/specs/mcd/vat-fold-pass-rough-spec.k
-tests/specs/mcd/vat-fork-diff-pass-rough-spec.k
-tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k
-tests/specs/mcd/vat-move-diff-rough-spec.k
-tests/specs/mcd/vat-slip-pass-rough-spec.k
 tests/specs/mcd/vow-fess-fail-rough-spec.k
 tests/specs/mcd/vow-flog-fail-rough-spec.k

tests/specs/mcd/flopper-cage-pass-spec.k

@@ -3,7 +3,6 @@ requires "verification.k"
 module FLOPPER-CAGE-PASS-SPEC
     imports VERIFICATION
 
-    // Flopper_cage
     claim [Flopper.cage.pass]:
       <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
       <mode> NORMAL </mode>