From 8f9b0063f9a415544f36b83cb354881ed771edf0 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 25 Sep 2023 23:42:01 +0200 Subject: [PATCH] Utilize dependency claims when discharging KClaim style proofs (#1926) * test: from with reuse * latest pyk * update PyK; look for dependencies before proving anything and specify subproofs * frob: fix dependencies * use graphlib's topological sorter for deps * Set Version: 1.0.226 * test-frob.sh * Set Version: 1.0.232 * no max-iterations * Set Version: 1.0.242 * fix KEVM_PREFIX * smt timeout; slow.haskell * slip test * test leaf number * check * pyupgrade * check * remove old testing file * Set Version: 1.0.250 * Address review comments * format * Set Version: 1.0.265 * make `pyupgrade` happy * make linters happy * --dont-extract-branches * Revert "--dont-extract-branches" This reverts commit 9411b8b7024d3026d770c083c19a92061e269ec7. * Set Version: 1.0.293 * Set Version: 1.0.294 * remove the `*-reuse-spec.k` file * Set Version: 1.0.305 * tests/specs/mcd/vat-move-diff-rough: separate out dependencies into separate module * kevm-pyk/__main__: correctly qualify dependency names if needed * tests/specs/mcd/vat-move-diff-rough: adjust specs for RPC prover * tests/failing*: run vat-move proof on RPC provers * kevm-pyk/{utils,__main__: factor out claim_dependency_dict helper * kevm-pyk/__main__: calculate claim dependency graph ahead of time * kevm-pyk/__main__: make sure to use calculated qualified names for claim dependencies * kevm-pyk/utils: remove QA comment thats not needed anymore * tests/failing*: enable vat-slip-pass-rough --------- Co-authored-by: devops Co-authored-by: Everett Hildenbrandt --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 89 ++++++++++++++------ kevm-pyk/src/kevm_pyk/utils.py | 22 ++++- kevm-pyk/src/tests/integration/test_prove.py | 30 +++++++ package/version | 2 +- tests/failing-symbolic.haskell | 1 + tests/failing-symbolic.haskell-booster | 2 - tests/failing-symbolic.pyk | 2 - tests/specs/mcd/vat-move-diff-rough-spec.k | 27 +++--- tests/specs/mcd/vat-slip-pass-rough-spec.k | 19 ++--- 11 files changed, 143 insertions(+), 55 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 14f31e8565..e97e69e740 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.304" +version = "1.0.305" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 83b038eb13..2d1849c21c 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.304' +VERSION: Final = '1.0.305' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 291844ab77..e985a9a302 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -1,7 +1,10 @@ from __future__ import annotations +import contextlib +import graphlib import json import logging +import os import sys from argparse import ArgumentParser from pathlib import Path @@ -28,11 +31,18 @@ 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 ensure_ksequence_on_k_cell, get_apr_proof_for_spec, kevm_prove, legacy_explore, print_failure_info +from .utils import ( + claim_dependency_dict, + ensure_ksequence_on_k_cell, + get_apr_proof_for_spec, + kevm_prove, + legacy_explore, + print_failure_info, +) if TYPE_CHECKING: from argparse import Namespace - from collections.abc import Callable, Iterable + from collections.abc import Callable, Iterable, Iterator from typing import Any, Final, TypeVar from pyk.kast.outer import KClaim @@ -172,6 +182,20 @@ def exec_prove_legacy( raise SystemExit(1) +class ZeroProcessPool: + def map(self, f: Callable[[Any], Any], xs: list[Any]) -> list[Any]: + return [f(x) for x in xs] + + +@contextlib.contextmanager +def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | ProcessPool]: + if workers <= 1: + yield ZeroProcessPool() + else: + with ProcessPool(ncpus=workers) as pp: + yield pp + + def exec_prove( spec_file: Path, includes: Iterable[str], @@ -214,19 +238,6 @@ def exec_prove( include_dirs = [Path(include) for include in includes] include_dirs += config.INCLUDE_DIRS - _LOGGER.info(f'Extracting claims from file: {spec_file}') - claims = kevm.get_claims( - spec_file, - spec_module_name=spec_module, - include_dirs=include_dirs, - md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, - ) - - if not claims: - raise ValueError(f'No claims found in file: {spec_file}') - if kore_rpc_command is None: kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',) elif isinstance(kore_rpc_command, str): @@ -240,6 +251,21 @@ def is_functional(claim: KClaim) -> bool: llvm_definition_dir = definition_dir / 'llvm-library' if use_booster else None + _LOGGER.info(f'Extracting claims from file: {spec_file}') + all_claims = kevm.get_claims( + spec_file, + spec_module_name=spec_module, + include_dirs=include_dirs, + md_selector=md_selector, + claim_labels=None, + exclude_claim_labels=exclude_claim_labels, + ) + if all_claims is None: + raise ValueError(f'No claims found in file: {spec_file}') + all_claims_by_label: dict[str, KClaim] = {c.label: c for c in all_claims} + spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper() + claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) + def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: with legacy_explore( kevm, @@ -297,7 +323,14 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: kcfg.replace_node(target_node_id, new_target) proof_problem = APRProof( - claim.label, kcfg, [], init_node_id, target_node_id, {}, proof_dir=save_directory + claim.label, + kcfg, + [], + init_node_id, + target_node_id, + {}, + proof_dir=save_directory, + subproof_ids=claims_graph[claim.label], ) passed = kevm_prove( @@ -316,17 +349,23 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: return passed, failure_log - results: list[tuple[bool, list[str] | None]] - if workers > 1: - with ProcessPool(ncpus=workers) as process_pool: - results = process_pool.map(_init_and_run_proof, claims) - else: - results = [] - for claim in claims: - results.append(_init_and_run_proof(claim)) + topological_sorter = graphlib.TopologicalSorter(claims_graph) + topological_sorter.prepare() + with wrap_process_pool(workers=workers) as process_pool: + selected_results: list[tuple[bool, list[str] | None]] = [] + selected_claims = [] + while topological_sorter.is_active(): + ready = topological_sorter.get_ready() + _LOGGER.info(f'Discharging proof obligations: {ready}') + curr_claim_list = [all_claims_by_label[label] for label in ready] + results: list[tuple[bool, list[str] | None]] = process_pool.map(_init_and_run_proof, curr_claim_list) + for label in ready: + topological_sorter.done(label) + selected_results.extend(results) + selected_claims.extend(curr_claim_list) failed = 0 - for claim, r in zip(claims, results, strict=True): + for claim, r in zip(selected_claims, selected_results, strict=True): passed, failure_log = r if passed: print(f'PROOF PASSED: {claim.label}') diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index b85f875514..712f746779 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -27,7 +27,7 @@ from collections.abc import Callable, Collection, Iterable, Iterator from typing import Final, TypeVar - from pyk.kast.outer import KDefinition + from pyk.kast.outer import KClaim, KDefinition from pyk.kcfg import KCFG from pyk.kcfg.semantics import KCFGSemantics from pyk.ktool.kprint import KPrint @@ -41,7 +41,25 @@ _LOGGER: Final = logging.getLogger(__name__) -def get_apr_proof_for_spec( # noqa: N802 +def claim_dependency_dict(claims: Iterable[KClaim], spec_module_name: str | None = None) -> dict[str, list[str]]: + claims_by_label = {claim.label: claim for claim in claims} + graph: dict[str, list[str]] = {} + for claim in claims: + graph[claim.label] = [] + for dependency in claim.dependencies: + if dependency not in claims_by_label: + if spec_module_name is None: + raise ValueError(f'Could not find dependency and no spec_module provided: {dependency}') + else: + spec_dependency = f'{spec_module_name}.{dependency}' + if spec_dependency not in claims_by_label: + raise ValueError(f'Could not find dependency: {dependency} or {spec_dependency}') + dependency = spec_dependency + graph[claim.label].append(dependency) + return graph + + +def get_apr_proof_for_spec( kprove: KProve, spec_file: Path, save_directory: Path | None, diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 7f36e0d87a..cb3e1732fc 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -1,11 +1,13 @@ from __future__ import annotations +import dataclasses import logging import sys from typing import TYPE_CHECKING, NamedTuple import pytest from pyk.cterm import CTerm +from pyk.proof.reachability import APRProof from kevm_pyk import config from kevm_pyk.__main__ import exec_prove @@ -199,6 +201,24 @@ def _target_for_spec(spec_file: Path, use_booster: bool) -> Target: # --------- +@dataclasses.dataclass(frozen=True) +class TParams: + main_claim_id: str + leaf_number: int | None + + +TEST_PARAMS: dict[str, TParams] = { + r'mcd/vat-slip-pass-rough-spec.k': TParams( + main_claim_id='VAT-SLIP-PASS-ROUGH-SPEC.Vat.slip.pass.rough', leaf_number=1 + ) +} + + +def leaf_number(proof: APRProof) -> int: + non_target_leaves = [nd for nd in proof.kcfg.leaves if not proof.is_target(nd.id)] + return len(non_target_leaves) + len(proof.kcfg.predecessors(proof.target)) + + @pytest.mark.parametrize( 'spec_file', ALL_TESTS, @@ -236,6 +256,16 @@ def test_pyk_prove( use_booster=use_booster, bug_report=bug_report, ) + name = str(spec_file.relative_to(SPEC_DIR)) + if name in TEST_PARAMS: + params = TEST_PARAMS[name] + apr_proof = APRProof.read_proof_data( + proof_dir=use_directory, + id=params.main_claim_id, + ) + expected_leaf_number = params.leaf_number + actual_leaf_number = leaf_number(apr_proof) + assert expected_leaf_number == actual_leaf_number except BaseException: raise finally: diff --git a/package/version b/package/version index 337b234bea..ef6675fd8e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.304 +1.0.305 diff --git a/tests/failing-symbolic.haskell b/tests/failing-symbolic.haskell index a8977a731a..d6469ae85e 100644 --- a/tests/failing-symbolic.haskell +++ b/tests/failing-symbolic.haskell @@ -109,6 +109,7 @@ 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 diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster index 14bd7d5a93..6cc20db2ad 100644 --- a/tests/failing-symbolic.haskell-booster +++ b/tests/failing-symbolic.haskell-booster @@ -31,8 +31,6 @@ 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-cage-deficit-pass-rough-spec.k tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k tests/specs/mcd/vow-fess-fail-rough-spec.k diff --git a/tests/failing-symbolic.pyk b/tests/failing-symbolic.pyk index bc3f33fb71..2917d0a91c 100644 --- a/tests/failing-symbolic.pyk +++ b/tests/failing-symbolic.pyk @@ -32,8 +32,6 @@ 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-cage-deficit-pass-rough-spec.k tests/specs/mcd/vow-cage-surplus-pass-rough-spec.k tests/specs/mcd/vow-fess-fail-rough-spec.k diff --git a/tests/specs/mcd/vat-move-diff-rough-spec.k b/tests/specs/mcd/vat-move-diff-rough-spec.k index f4c62057ca..3a35744b15 100644 --- a/tests/specs/mcd/vat-move-diff-rough-spec.k +++ b/tests/specs/mcd/vat-move-diff-rough-spec.k @@ -1,7 +1,8 @@ requires "verification.k" + module VAT-MOVE-DIFF-ROUGH-SPEC - imports VERIFICATION + imports VAT-MOVE-DIFF-ROUGH-ARITH-SPEC // Vat_move-diff claim [Vat.move-diff.pass.rough]: @@ -118,10 +119,17 @@ module VAT-MOVE-DIFF-ROUGH-SPEC andBool #Vat.can[ABI_src][CALLER_ID] =/=Int #Vat.dai[ABI_src] andBool #Vat.can[ABI_src][CALLER_ID] =/=Int #Vat.dai[ABI_dst] andBool #Vat.dai[ABI_src] =/=Int #Vat.dai[ABI_dst] + [depends(VAT-MOVE-DIFF-ROUGH-ARITH-SPEC.Vat.adduu.pass,VAT-MOVE-DIFF-ROUGH-ARITH-SPEC.Vat.subuu.pass)] + +endmodule + + +module VAT-MOVE-DIFF-ROUGH-ARITH-SPEC + imports VERIFICATION // Vat_adduu claim [Vat.adduu.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION 1 NORMAL ISTANBUL @@ -139,10 +147,10 @@ module VAT-MOVE-DIFF-ROUGH-SPEC CALLER_ID _ => ?_ VCallValue - ABI_y : ABI_x : JMPTO : WS => JMPTO : ABI_x +Int ABI_y : WS + ABI_y : ABI_x : JMPTO : WS => ABI_x +Int ABI_y : WS _ 13086 => 13111 - #gas(VGas) => #gas ( ( VGas +Int 54 ) ) + #gas(VGas) => #gas ( ( VGas -Int 62 ) ) VMemoryUsed _ => ?_ _ @@ -214,12 +222,10 @@ module VAT-MOVE-DIFF-ROUGH-SPEC andBool ((#sizeWordStack(WS) <=Int 100) andBool (#rangeUInt(256, VMemoryUsed) andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - [trusted] - // Vat_subuu claim [Vat.subuu.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION 1 NORMAL ISTANBUL @@ -237,10 +243,10 @@ module VAT-MOVE-DIFF-ROUGH-SPEC CALLER_ID _ => ?_ VCallValue - ABI_y : ABI_x : JMPTO : WS => JMPTO : ABI_x -Int ABI_y : WS + ABI_y : ABI_x : JMPTO : WS => ABI_x -Int ABI_y : WS _ 13060 => 13085 - #gas(VGas) => #gas ( ( VGas +Int 54 ) ) + #gas(VGas) => #gas ( ( VGas -Int 62 ) ) VMemoryUsed _ => ?_ _ @@ -312,7 +318,6 @@ module VAT-MOVE-DIFF-ROUGH-SPEC andBool ((#sizeWordStack(WS) <=Int 100) andBool (#rangeUInt(256, VMemoryUsed) andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) - [trusted] - endmodule + diff --git a/tests/specs/mcd/vat-slip-pass-rough-spec.k b/tests/specs/mcd/vat-slip-pass-rough-spec.k index e085d90961..fde29916ac 100644 --- a/tests/specs/mcd/vat-slip-pass-rough-spec.k +++ b/tests/specs/mcd/vat-slip-pass-rough-spec.k @@ -110,9 +110,11 @@ module VAT-SLIP-PASS-ROUGH-SPEC andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.gem[ABI_ilk][ABI_usr]) ==Int Junk_1 andBool #Vat.wards[CALLER_ID] =/=Int #Vat.gem[ABI_ilk][ABI_usr] + [depends(Vat.addui.pass)] + // Vat_addui claim [Vat.addui.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION 1 NORMAL ISTANBUL @@ -130,14 +132,14 @@ module VAT-SLIP-PASS-ROUGH-SPEC CALLER_ID _ => ?_ VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => JMPTO : ABI_x +Int ABI_y : WS + chop(ABI_y) : ABI_x : JMPTO : WS => ABI_x +Int ABI_y : WS _ 13112 => 13174 - #gas(VGas) => #if ( ABI_y #gas(VGas) => #if ( ABI_y VMemoryUsed @@ -212,7 +214,4 @@ module VAT-SLIP-PASS-ROUGH-SPEC andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - [trusted] - - endmodule