From 01d3ab043a170c6570974caa77939872dc54aa59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 9 Oct 2024 09:34:46 +0200 Subject: [PATCH] Add Python 3.13 to `pyk` code quality CI job (#4656) - Fix a few `TypeError`-s - Add Python 3.13 to code quality matrix --- .github/workflows/test-pr.yml | 2 +- pyk/src/tests/integration/proof/test_imp.py | 182 +++++++++--------- .../tests/integration/proof/test_mini_kevm.py | 50 +++-- 3 files changed, 113 insertions(+), 121 deletions(-) diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index a32a018ee22..3e4c05270ff 100644 --- a/.github/workflows/test-pr.yml +++ b/.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 diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index a5231d43bdd..55ef85ca96a 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/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 diff --git a/pyk/src/tests/integration/proof/test_mini_kevm.py b/pyk/src/tests/integration/proof/test_mini_kevm.py index af651edc19c..f7f78576603 100644 --- a/pyk/src/tests/integration/proof/test_mini_kevm.py +++ b/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,