Merge branch 'master' into _update-deps/runtimeverification/k

.github/workflows/test-pr.yml

@@ -114,10 +114,10 @@ jobs:
             test-args:
             timeout: 45
           - test-suite: 'test-prove-pyk'
-            test-args:
+            test-args: '--no-use-booster'
             timeout: 180
           - test-suite: 'test-prove-pyk'
-            test-args: '--use-booster'
+            test-args:
             timeout: 150
     timeout-minutes: ${{ matrix.timeout }}
     steps:

kevm-pyk/src/kevm_pyk/__main__.py

@@ -36,14 +36,7 @@
 from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile
-from .utils import (
-    claim_dependency_dict,
-    ensure_ksequence_on_k_cell,
-    get_apr_proof_for_spec,
-    legacy_explore,
-    print_failure_info,
-    run_prover,
-)
+from .utils import claim_dependency_dict, get_apr_proof_for_spec, legacy_explore, print_failure_info, run_prover
 
 if TYPE_CHECKING:
     from argparse import Namespace
@@ -293,13 +286,29 @@ def is_functional(claim: KClaim) -> bool:
     claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name)
 
     def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
+        proof_problem: Proof
         claim = claim_job.claim
         up_to_date = claim_job.up_to_date(digest_file)
         if up_to_date:
             _LOGGER.info(f'Claim is up to date: {claim.label}')
         else:
             _LOGGER.info(f'Claim reinitialized because it is out of date: {claim.label}')
         claim_job.update_digest(digest_file)
+
+        if is_functional(claim):
+            if not options.reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory):
+                proof_problem = EqualityProof.read_proof_data(save_directory, claim.label)
+            else:
+                proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory)
+        else:
+            if not options.reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory):
+                proof_problem = APRProof.read_proof_data(save_directory, claim.label)
+            else:
+                proof_problem = APRProof.from_claim(kevm.definition, claim, {}, proof_dir=save_directory)
+        if proof_problem.passed and not proof_problem.admitted:
+            _LOGGER.info(f'Proof already passed: {proof_problem.id}')
+            return (True, [])
+
         with legacy_explore(
             kevm,
             kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas),
@@ -333,48 +342,24 @@ def create_kcfg_explore() -> KCFGExplore:
                     id=claim.label,
                 )
 
-            proof_problem: Proof
-            if is_functional(claim):
-                if not options.reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory):
-                    proof_problem = EqualityProof.read_proof_data(save_directory, claim.label)
-                else:
-                    proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory)
-            else:
-                if not options.reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory):
-                    proof_problem = APRProof.read_proof_data(save_directory, claim.label)
-
-                else:
-                    _LOGGER.info(f'Converting claim to KCFG: {claim.label}')
-                    kcfg, init_node_id, target_node_id = KCFG.from_claim(kevm.definition, claim)
-
-                    new_init = ensure_ksequence_on_k_cell(kcfg.node(init_node_id).cterm)
-                    new_target = ensure_ksequence_on_k_cell(kcfg.node(target_node_id).cterm)
-
-                    _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}')
-                    new_init = kcfg_explore.cterm_symbolic.assume_defined(new_init)
-
-                    _LOGGER.info(f'Simplifying initial and target node: {claim.label}')
-                    new_init, _ = kcfg_explore.cterm_symbolic.simplify(new_init)
-                    new_target, _ = kcfg_explore.cterm_symbolic.simplify(new_target)
-                    if is_bottom(new_init.kast, weak=True):
-                        raise ValueError('Simplifying initial node led to #Bottom, are you sure your LHS is defined?')
-                    if is_top(new_target.kast, weak=True):
-                        raise ValueError('Simplifying target node led to #Bottom, are you sure your RHS is defined?')
-
-                    kcfg.let_node(init_node_id, cterm=new_init)
-                    kcfg.let_node(target_node_id, cterm=new_target)
-
-                    proof_problem = APRProof(
-                        claim.label,
-                        kcfg,
-                        [],
-                        init_node_id,
-                        target_node_id,
-                        {},
-                        proof_dir=save_directory,
-                        subproof_ids=claims_graph[claim.label],
-                        admitted=claim.is_trusted,
-                    )
+            if not is_functional(claim) and (options.reinit or not up_to_date):
+                assert type(proof_problem) is APRProof
+                init_cterm = proof_problem.kcfg.node(proof_problem.init).cterm
+                target_cterm = proof_problem.kcfg.node(proof_problem.target).cterm
+
+                _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}')
+                init_cterm = kcfg_explore.cterm_symbolic.assume_defined(init_cterm)
+
+                _LOGGER.info(f'Simplifying initial and target node: {claim.label}')
+                init_cterm, _ = kcfg_explore.cterm_symbolic.simplify(init_cterm)
+                target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(target_cterm)
+                if is_bottom(init_cterm.kast, weak=True):
+                    raise ValueError('Simplifying initial node led to #Bottom, are you sure your LHS is defined?')
+                if is_top(target_cterm.kast, weak=True):
+                    raise ValueError('Simplifying target node led to #Bottom, are you sure your RHS is defined?')
+
+                proof_problem.kcfg.let_node(proof_problem.init, cterm=init_cterm)
+                proof_problem.kcfg.let_node(proof_problem.target, cterm=target_cterm)
 
             if proof_problem.admitted:
                 proof_problem.write_proof_data()
@@ -461,6 +446,7 @@ def exec_prune(options: PruneOptions) -> None:
             md_selector=md_selector,
             claim_labels=options.claim_labels,
             exclude_claim_labels=options.exclude_claim_labels,
+            include_dependencies=False,
         )
     )
 
@@ -501,6 +487,7 @@ def exec_section_edge(options: SectionEdgeOptions) -> None:
             md_selector=md_selector,
             claim_labels=options.claim_labels,
             exclude_claim_labels=options.exclude_claim_labels,
+            include_dependencies=False,
         )
     )
 
@@ -517,9 +504,10 @@ def exec_section_edge(options: SectionEdgeOptions) -> None:
         trace_rewrites=options.trace_rewrites,
         llvm_definition_dir=llvm_definition_dir,
     ) as kcfg_explore:
-        kcfg, _ = kcfg_explore.section_edge(
+        node_ids = kcfg_explore.section_edge(
             proof.kcfg, source_id=int(source_id), target_id=int(target_id), logs=proof.logs, sections=options.sections
         )
+        _LOGGER.info(f'Added nodes on edge {(source_id, target_id)}: {node_ids}')
     proof.write_proof_data()
 
 
@@ -540,6 +528,7 @@ def exec_show_kcfg(options: ShowKCFGOptions) -> None:
         md_selector=options.md_selector,
         claim_labels=options.claim_labels,
         exclude_claim_labels=options.exclude_claim_labels,
+        include_dependencies=False,
     )
 
     nodes = options.nodes
@@ -585,6 +574,7 @@ def exec_view_kcfg(options: ViewKCFGOptions) -> None:
         md_selector=options.md_selector,
         claim_labels=options.claim_labels,
         exclude_claim_labels=options.exclude_claim_labels,
+        include_dependencies=False,
     )
 
     node_printer = kevm_node_printer(kevm, proof)

kevm-pyk/src/kevm_pyk/cli.py

@@ -198,13 +198,6 @@ def _create_argument_parser() -> ArgumentParser:
     )
     section_edge_args.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.')
     section_edge_args.add_argument('--sections', type=int, help='Number of sections to make from edge (>= 2).')
-    section_edge_args.add_argument(
-        '--use-booster',
-        dest='use_booster',
-        default=None,
-        action='store_true',
-        help="Use the booster RPC server instead of kore-rpc. Requires calling kompile with '--target haskell-booster' flag",
-    )
 
     prove_legacy_args = command_parser.add_parser(
         'prove-legacy',
@@ -367,7 +360,7 @@ def default() -> dict[str, Any]:
         return {
             'trace_rewrites': False,
             'kore_rpc_command': None,
-            'use_booster': False,
+            'use_booster': True,
             'fallback_on': [],
             'post_exec_simplify': True,
             'interim_simplification': None,
@@ -693,7 +686,6 @@ class SectionEdgeOptions(
     def default() -> dict[str, Any]:
         return {
             'sections': 2,
-            'use_booster': False,
         }
 
     @staticmethod
@@ -1026,6 +1018,13 @@ def rpc_args(self) -> ArgumentParser:
             action='store_true',
             help='Use the booster RPC server instead of kore-rpc.',
         )
+        args.add_argument(
+            '--no-use-booster',
+            dest='use_booster',
+            default=None,
+            action='store_false',
+            help='Do not the booster RPC server instead of kore-rpc.',
+        )
         args.add_argument(
             '--fallback-on',
             dest='fallback_on',

kevm-pyk/src/kevm_pyk/utils.py

@@ -7,19 +7,17 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
-from pyk.cterm import CTerm, CTermSymbolic
+from pyk.cterm import CTermSymbolic
 from pyk.kast import Atts
 from pyk.kast.inner import KApply, KInner, KRewrite, KVariable, Subst
 from pyk.kast.manip import (
     abstract_term_safely,
     bottom_up,
     free_vars,
     is_anon_var,
-    set_cell,
     split_config_and_constraints,
     split_config_from,
 )
-from pyk.kast.outer import KSequence
 from pyk.kcfg import KCFGExplore
 from pyk.kore.rpc import KoreClient, KoreExecLogFormat, TransportType, kore_server
 from pyk.ktool import TypeInferenceMode
@@ -74,6 +72,7 @@ def get_apr_proof_for_spec(
     md_selector: str | None = None,
     claim_labels: Iterable[str] | None = None,
     exclude_claim_labels: Iterable[str] | None = None,
+    include_dependencies: bool = True,
 ) -> APRProof:
     if save_directory is None:
         save_directory = Path('.')
@@ -89,6 +88,7 @@ def get_apr_proof_for_spec(
             claim_labels=claim_labels,
             exclude_claim_labels=exclude_claim_labels,
             type_inference_mode=TypeInferenceMode.SIMPLESUB,
+            include_dependencies=include_dependencies,
         )
     )
 
@@ -380,14 +380,6 @@ def abstract_cell_vars(cterm: KInner, keep_vars: Collection[KVariable] = ()) ->
     return Subst(subst)(config)
 
 
-def ensure_ksequence_on_k_cell(cterm: CTerm) -> CTerm:
-    k_cell = cterm.cell('K_CELL')
-    if type(k_cell) is not KSequence:
-        _LOGGER.info('Introducing artificial KSequence on <k> cell.')
-        return CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence([k_cell])))
-    return cterm
-
-
 def constraints_for(vars: list[str], constraints: Iterable[KInner]) -> Iterable[KInner]:
     accounts_constraints = []
     constraints_changed = True

kevm-pyk/src/tests/conftest.py

@@ -17,10 +17,10 @@ def pytest_addoption(parser: Parser) -> None:
         help='Write expected output files for proof tests',
     )
     parser.addoption(
-        '--use-booster',
+        '--no-use-booster',
         action='store_true',
         default=False,
-        help='Use the kore-rpc-booster binary instead of kore-rpc',
+        help='Do not the kore-rpc-booster binary instead of kore-rpc',
     )
     parser.addoption(
         '--spec-name',
@@ -41,8 +41,8 @@ def update_expected_output(request: FixtureRequest) -> bool:
 
 
 @pytest.fixture(scope='session')
-def use_booster(request: FixtureRequest) -> bool:
-    return request.config.getoption('--use-booster')
+def no_use_booster(request: FixtureRequest) -> bool:
+    return request.config.getoption('--no-use-booster')
 
 
 @pytest.fixture(scope='session')

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

@@ -243,13 +243,15 @@ def test_pyk_prove(
     kompiled_target_for: Callable[[Path], Path],
     tmp_path: Path,
     caplog: LogCaptureFixture,
-    use_booster: bool,
+    no_use_booster: bool,
     bug_report: BugReport | None,
     spec_name: str | None,
 ) -> None:
     caplog.set_level(logging.INFO)
 
-    if (not use_booster and spec_file in FAILING_PYK_TESTS) or (use_booster and spec_file in FAILING_BOOSTER_TESTS):
+    if (no_use_booster and spec_file in FAILING_PYK_TESTS) or (
+        not no_use_booster and spec_file in FAILING_BOOSTER_TESTS
+    ):
         pytest.skip()
 
     if spec_name is not None and str(spec_file).find(spec_name) < 0:
@@ -272,7 +274,7 @@ def test_pyk_prove(
                 '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': use_booster,
+                'use_booster': not no_use_booster,
                 'bug_report': bug_report,
                 'break_on_calls': break_on_calls,
             }

package/test-package.sh

@@ -37,11 +37,9 @@ kevm kompile-spec tests/specs/benchmarks/verification.k             \
 kevm prove tests/specs/benchmarks/structarg00-spec.k         \
     --definition tests/specs/benchmarks/verification/haskell \
     --save-directory proofs                                  \
-    --verbose                                                \
-    --use-booster
+    --verbose
 
 kevm prove tests/specs/benchmarks/structarg01-spec.k         \
     --definition tests/specs/benchmarks/verification/haskell \
     --save-directory proofs                                  \
-    --verbose                                                \
-    --use-booster
+    --verbose

tests/specs/benchmarks/address00-spec.k

@@ -6,7 +6,6 @@ module ADDRESS00-SPEC
   // fn-execute
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>

tests/specs/benchmarks/bytes00-spec.k

@@ -6,7 +6,6 @@ module BYTES00-SPEC
   // fn-execute
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>

tests/specs/benchmarks/dynamicarray00-spec.k

@@ -6,7 +6,6 @@ module DYNAMICARRAY00-SPEC
   // fn-execute
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>

tests/specs/benchmarks/ecrecover00-siginvalid-spec.k

@@ -6,7 +6,6 @@ module ECRECOVER00-SIGINVALID-SPEC
   // fn-execute-siginvalid
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>

tests/specs/benchmarks/ecrecover00-sigvalid-spec.k

@@ -6,7 +6,6 @@ module ECRECOVER00-SIGVALID-SPEC
   // fn-execute-sigvalid
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>

tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k

@@ -6,7 +6,6 @@ module ECRECOVERLOOP00-SIG0-INVALID-SPEC
   // fn-execute-sig0-invalid
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>

tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k

@@ -6,7 +6,6 @@ module ECRECOVERLOOP00-SIG1-INVALID-SPEC
   // fn-execute-sig1-invalid
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>

tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k

@@ -6,7 +6,6 @@ module ECRECOVERLOOP00-SIGS-VALID-SPEC
   // fn-execute-sigs-valid
   claim
     <k> (#execute => #halt) ~> _ </k>
-    <exit-code> 1 </exit-code>
     <mode> NORMAL </mode>
     <schedule> ISTANBUL </schedule>
     <useGas> true </useGas>