Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/haskell-backend

.github/workflows/test-pr.yml

@@ -35,7 +35,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        python-version: ['3.10', '3.11', '3.12']
+        python-version: ['3.10', '3.11', '3.12', '3.13']
     defaults:
       run:
         working-directory: ./pyk

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.98
+0.1.99

flake.nix

@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.98";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.99";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.86";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

pyk/src/pyk/cli/pyk.py

@@ -579,7 +579,9 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s
         if len(profile_list) == 0 or profile_list[0] not in toml_profile:
             return {k: v for k, v in toml_profile.items() if type(v) is not dict}
         elif len(profile_list) == 1:
-            return {k: v for k, v in toml_profile[profile_list[0]].items() if type(v) is not dict}
+            active_profile = {k: v for k, v in toml_profile.get(profile_list[0], {}).items() if type(v) is not dict}
+            default_profile = {k: v for k, v in toml_profile.get('default', {}).items() if type(v) is not dict}
+            return {**default_profile, **active_profile}
         return get_profile(toml_profile[profile_list[0]], profile_list[1:])
 
     toml_args: dict[str, Any] = {}

pyk/src/tests/integration/proof/test_imp.py

@@ -892,31 +892,31 @@ def test_all_path_reachability_prove(
         expected_leaf_number: int,
         tmp_path_factory: TempPathFactory,
     ) -> None:
-        with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir:
-            spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
-            spec_label = f'{spec_module}.{claim_id}'
-            proofs = APRProof.from_spec_modules(
-                kprove.definition,
-                spec_modules,
-                spec_labels=[spec_label],
-                logs={},
-                proof_dir=proof_dir,
-            )
-            proof = single([p for p in proofs if p.id == spec_label])
-            if admit_deps:
-                for subproof in proof.subproofs:
-                    subproof.admit()
-                    subproof.write_proof_data()
+        proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}')
+        spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
+        spec_label = f'{spec_module}.{claim_id}'
+        proofs = APRProof.from_spec_modules(
+            kprove.definition,
+            spec_modules,
+            spec_labels=[spec_label],
+            logs={},
+            proof_dir=proof_dir,
+        )
+        proof = single([p for p in proofs if p.id == spec_label])
+        if admit_deps:
+            for subproof in proof.subproofs:
+                subproof.admit()
+                subproof.write_proof_data()
 
-            prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=cut_rules)
-            prover.advance_proof(proof, max_iterations=max_iterations)
+        prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=cut_rules)
+        prover.advance_proof(proof, max_iterations=max_iterations)
 
-            kcfg_show = KCFGShow(kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True))
-            cfg_lines = kcfg_show.show(proof.kcfg)
-            _LOGGER.info('\n'.join(cfg_lines))
+        kcfg_show = KCFGShow(kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True))
+        cfg_lines = kcfg_show.show(proof.kcfg)
+        _LOGGER.info('\n'.join(cfg_lines))
 
-            assert proof.status == proof_status
-            assert leaf_number(proof) == expected_leaf_number
+        assert proof.status == proof_status
+        assert leaf_number(proof) == expected_leaf_number
 
     def test_terminal_node_subsumption(
         self,
@@ -929,24 +929,24 @@ def test_terminal_node_subsumption(
         spec_module: str = 'IMP-SIMPLE-SPEC'
         claim_id: str = 'terminal-node-subsumption'
         cut_rules: Iterable[str] = []
-        with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir:
-            spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
-            spec_label = f'{spec_module}.{claim_id}'
-            proofs = APRProof.from_spec_modules(
-                kprove.definition,
-                spec_modules,
-                spec_labels=[spec_label],
-                logs={},
-                proof_dir=proof_dir,
-            )
-            proof = single([p for p in proofs if p.id == spec_label])
-            prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=7, cut_point_rules=cut_rules)
-            prover.advance_proof(proof, max_iterations=1)
-            # We have reached a terminal node, but not yet checked subsumption
-            assert proof.status != ProofStatus.PASSED
-            # The next advance only checks subsumption
-            prover.advance_proof(proof, max_iterations=1)
-            assert proof.status == ProofStatus.PASSED
+        proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}')
+        spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
+        spec_label = f'{spec_module}.{claim_id}'
+        proofs = APRProof.from_spec_modules(
+            kprove.definition,
+            spec_modules,
+            spec_labels=[spec_label],
+            logs={},
+            proof_dir=proof_dir,
+        )
+        proof = single([p for p in proofs if p.id == spec_label])
+        prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=7, cut_point_rules=cut_rules)
+        prover.advance_proof(proof, max_iterations=1)
+        # We have reached a terminal node, but not yet checked subsumption
+        assert proof.status != ProofStatus.PASSED
+        # The next advance only checks subsumption
+        prover.advance_proof(proof, max_iterations=1)
+        assert proof.status == ProofStatus.PASSED
 
     @pytest.mark.parametrize(
         'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,terminal_rules,cut_rules,expected_constraint',
@@ -1440,34 +1440,32 @@ def test_all_path_reachability_prove_parallel(
         tmp_path_factory: TempPathFactory,
         create_prover: Callable[[int, Iterable[str]], Prover],
     ) -> None:
-        with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir:
-            spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
-            spec_label = f'{spec_module}.{claim_id}'
-            proofs = APRProof.from_spec_modules(
-                kprove.definition,
-                spec_modules,
-                spec_labels=[spec_label],
-                logs={},
-                proof_dir=proof_dir,
-            )
-            proof = single([p for p in proofs if p.id == spec_label])
-            if admit_deps:
-                for subproof in proof.subproofs:
-                    subproof.admit()
-                    subproof.write_proof_data()
+        proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}')
+        spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
+        spec_label = f'{spec_module}.{claim_id}'
+        proofs = APRProof.from_spec_modules(
+            kprove.definition,
+            spec_modules,
+            spec_labels=[spec_label],
+            logs={},
+            proof_dir=proof_dir,
+        )
+        proof = single([p for p in proofs if p.id == spec_label])
+        if admit_deps:
+            for subproof in proof.subproofs:
+                subproof.admit()
+                subproof.write_proof_data()
 
-            _create_prover = partial(create_prover, max_depth, cut_rules)
+        _create_prover = partial(create_prover, max_depth, cut_rules)
 
-            parallel_advance_proof(
-                proof=proof, max_iterations=max_iterations, create_prover=_create_prover, max_workers=2
-            )
+        parallel_advance_proof(proof=proof, max_iterations=max_iterations, create_prover=_create_prover, max_workers=2)
 
-            kcfg_show = KCFGShow(kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True))
-            cfg_lines = kcfg_show.show(proof.kcfg)
-            _LOGGER.info('\n'.join(cfg_lines))
+        kcfg_show = KCFGShow(kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True))
+        cfg_lines = kcfg_show.show(proof.kcfg)
+        _LOGGER.info('\n'.join(cfg_lines))
 
-            assert proof.status == proof_status
-            assert leaf_number(proof) == expected_leaf_number
+        assert proof.status == proof_status
+        assert leaf_number(proof) == expected_leaf_number
 
     def test_all_path_reachability_prove_parallel_resources(
         self,
@@ -1481,39 +1479,37 @@ def test_all_path_reachability_prove_parallel_resources(
         spec_module = 'IMP-SIMPLE-SPEC'
         claim_id = 'addition-1'
 
-        with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir:
-            spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
-            spec_label = f'{spec_module}.{claim_id}'
-            proofs = APRProof.from_spec_modules(
-                kprove.definition,
-                spec_modules,
-                spec_labels=[spec_label],
-                logs={},
-                proof_dir=proof_dir,
-            )
-            proof = single([p for p in proofs if p.id == spec_label])
+        proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}')
+        spec_modules = kprove.get_claim_modules(Path(spec_file), spec_module_name=spec_module)
+        spec_label = f'{spec_module}.{claim_id}'
+        proofs = APRProof.from_spec_modules(
+            kprove.definition,
+            spec_modules,
+            spec_labels=[spec_label],
+            logs={},
+            proof_dir=proof_dir,
+        )
+        proof = single([p for p in proofs if p.id == spec_label])
 
-            _create_prover = partial(create_prover, 1, [])
+        _create_prover = partial(create_prover, 1, [])
 
-            provers_created = 0
+        provers_created = 0
 
-            class MyAPRProver(APRProver):
-                provers_closed: int = 0
+        class MyAPRProver(APRProver):
+            provers_closed: int = 0
 
-                def close(self) -> None:
-                    MyAPRProver.provers_closed += 1
-                    super().close()
+            def close(self) -> None:
+                MyAPRProver.provers_closed += 1
+                super().close()
 
-            def create_prover_res_counter() -> APRProver:
-                nonlocal provers_created
-                provers_created += 1
-                prover = _create_prover()
-                prover.__class__ = MyAPRProver
-                assert type(prover) is MyAPRProver
-                return prover
+        def create_prover_res_counter() -> APRProver:
+            nonlocal provers_created
+            provers_created += 1
+            prover = _create_prover()
+            prover.__class__ = MyAPRProver
+            assert type(prover) is MyAPRProver
+            return prover
 
-            parallel_advance_proof(
-                proof=proof, max_iterations=2, create_prover=create_prover_res_counter, max_workers=2
-            )
+        parallel_advance_proof(proof=proof, max_iterations=2, create_prover=create_prover_res_counter, max_workers=2)
 
-            assert provers_created == MyAPRProver.provers_closed
+        assert provers_created == MyAPRProver.provers_closed

pyk/src/tests/integration/proof/test_mini_kevm.py

@@ -76,33 +76,29 @@ def test_all_path_reachability_prove(
         expected_leaf_number: int,
         tmp_path_factory: TempPathFactory,
     ) -> None:
-        with tmp_path_factory.mktemp('apr_tmp_proofs') as proof_dir:
-            claim = single(
-                kprove.get_claims(
-                    Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id}']
-                )
-            )
-            proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir)
-
-            new_init_cterm = kcfg_explore.cterm_symbolic.assume_defined(proof.kcfg.node(proof.init).cterm)
-            proof.kcfg.let_node(proof.init, cterm=new_init_cterm)
-            kcfg_explore.simplify(proof.kcfg, {})
-
-            prover = APRProver(
-                kcfg_explore=kcfg_explore,
-                execute_depth=max_depth,
-                cut_point_rules=cut_rules,
-            )
-            prover.advance_proof(proof, max_iterations=max_iterations)
-
-            kcfg_show = KCFGShow(
-                kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False)
-            )
-            cfg_lines = kcfg_show.show(proof.kcfg)
-            _LOGGER.info('\n'.join(cfg_lines))
-
-            assert proof.status == proof_status
-            assert leaf_number(proof) == expected_leaf_number
+        proof_dir = tmp_path_factory.mktemp('apr_tmp_proofs')
+        claim = single(
+            kprove.get_claims(Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id}'])
+        )
+        proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir)
+
+        new_init_cterm = kcfg_explore.cterm_symbolic.assume_defined(proof.kcfg.node(proof.init).cterm)
+        proof.kcfg.let_node(proof.init, cterm=new_init_cterm)
+        kcfg_explore.simplify(proof.kcfg, {})
+
+        prover = APRProver(
+            kcfg_explore=kcfg_explore,
+            execute_depth=max_depth,
+            cut_point_rules=cut_rules,
+        )
+        prover.advance_proof(proof, max_iterations=max_iterations)
+
+        kcfg_show = KCFGShow(kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False))
+        cfg_lines = kcfg_show.show(proof.kcfg)
+        _LOGGER.info('\n'.join(cfg_lines))
+
+        assert proof.status == proof_status
+        assert leaf_number(proof) == expected_leaf_number
 
     def test_implication_failure_reason_cell_mismatch(
         self,

pyk/src/tests/unit/test-data/pyk_toml_test.toml

@@ -6,9 +6,12 @@ definition = "/tmp"
 input = "kast-json"
 no-minimize = true
 
-[prove-legacy]
+[prove-legacy.default]
 kArgs = ["arg 1","args 2"]
 
+[prove-legacy.verbose]
+verbose = true
+
 [coverage.a_profile]
 verbose = true
 output = "a-profile-file"

pyk/src/tests/unit/test_toml_args.py

@@ -62,6 +62,28 @@ def test_prove_legacy_kargs() -> None:
     assert len(args_dict['k_args']) == 2
 
 
+def test_prove_legacy_profiles() -> None:
+    parser = create_argument_parser()
+    cmd_args = [
+        'prove-legacy',
+        '--config-file',
+        str(TEST_TOML),
+        '--config-profile',
+        'verbose',
+        tempfile.gettempdir(),
+        str(TEST_TOML),
+        str(TEST_TOML),
+        'spec-module',
+        'cmd_args',
+    ]
+    args = parser.parse_args(cmd_args)
+    args_dict = parse_toml_args(args)
+    assert len(args_dict['k_args']) == 2
+    assert hasattr(args, 'verbose')
+    assert 'verbose' in args_dict
+    assert args_dict['verbose']
+
+
 def test_toml_read() -> None:
     change_in_toml('definition = "(.*)"', f'definition = "{tempfile.gettempdir()}"')
     parser = create_argument_parser()