kevm-pyk/{utils,cli,__main__,test_prove}: use new field direct_subpro…

…of_rules to run test-prove-dss

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

@@ -383,6 +383,7 @@ def test_prove_dss(
                 'bug_report': bug_report,
                 'break_on_calls': False,
                 'workers': workers,
+                'direct_subproof_rules': True,
             }
         )
         exec_prove(options=options)