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 9411b8b. * 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 <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]>
runtimeverification · Sep 25, 2023 · 8f9b006 · 8f9b006
1 parent 85d786e
commit 8f9b006
Show file tree

Hide file tree

Showing 11 changed files with 143 additions and 55 deletions.
diff --git 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. <[email protected]>",

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -1 +1 @@
-1.0.304
+1.0.305
diff --git 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
@@ -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
@@ -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
@@ -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]:
-      <k> #execute ~> CONTINUATION => #execute ~> CONTINUATION </k>
+      <k> #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION </k>
       <exit-code> 1 </exit-code>
       <mode> NORMAL </mode>
       <schedule> ISTANBUL </schedule>
@@ -139,10 +147,10 @@ module VAT-MOVE-DIFF-ROUGH-SPEC
             <caller> CALLER_ID </caller>
             <callData> _ => ?_ </callData>
             <callValue> VCallValue </callValue>
-            <wordStack> ABI_y : ABI_x : JMPTO : WS  =>  JMPTO : ABI_x +Int ABI_y : WS </wordStack>
+            <wordStack> ABI_y : ABI_x : JMPTO : WS  =>  ABI_x +Int ABI_y : WS </wordStack>
             <localMem> _ </localMem>
             <pc> 13086 => 13111 </pc>
-            <gas> #gas(VGas) => #gas ( ( VGas +Int 54 ) ) </gas>
+            <gas> #gas(VGas) => #gas ( ( VGas -Int 62 ) ) </gas>
             <memoryUsed> VMemoryUsed </memoryUsed>
             <callGas> _ => ?_ </callGas>
             <static> _ </static>
@@ -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]:
-      <k> #execute ~> CONTINUATION => #execute ~> CONTINUATION </k>
+      <k> #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION </k>
       <exit-code> 1 </exit-code>
       <mode> NORMAL </mode>
       <schedule> ISTANBUL </schedule>
@@ -237,10 +243,10 @@ module VAT-MOVE-DIFF-ROUGH-SPEC
             <caller> CALLER_ID </caller>
             <callData> _ => ?_ </callData>
             <callValue> VCallValue </callValue>
-            <wordStack> ABI_y : ABI_x : JMPTO : WS  =>  JMPTO : ABI_x -Int ABI_y : WS </wordStack>
+            <wordStack> ABI_y : ABI_x : JMPTO : WS  =>  ABI_x -Int ABI_y : WS </wordStack>
             <localMem> _ </localMem>
             <pc> 13060 => 13085 </pc>
-            <gas> #gas(VGas) => #gas ( ( VGas +Int 54 ) ) </gas>
+            <gas> #gas(VGas) => #gas ( ( VGas -Int 62 ) ) </gas>
             <memoryUsed> VMemoryUsed </memoryUsed>
             <callGas> _ => ?_ </callGas>
             <static> _ </static>
@@ -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
@@ -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]:
-      <k> #execute ~> CONTINUATION => #execute ~> CONTINUATION </k>
+      <k> #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION </k>
       <exit-code> 1 </exit-code>
       <mode> NORMAL </mode>
       <schedule> ISTANBUL </schedule>
@@ -130,14 +132,14 @@ module VAT-SLIP-PASS-ROUGH-SPEC
             <caller> CALLER_ID </caller>
             <callData> _ => ?_ </callData>
             <callValue> VCallValue </callValue>
-            <wordStack> chop(ABI_y) : ABI_x : JMPTO : WS  =>  JMPTO : ABI_x +Int ABI_y : WS </wordStack>
+            <wordStack> chop(ABI_y) : ABI_x : JMPTO : WS  => ABI_x +Int ABI_y : WS </wordStack>
             <localMem> _ </localMem>
             <pc> 13112 => 13174 </pc>
-            <gas> #gas(VGas) => #if ( ABI_y <Int 0 andBool 0 <=Int ( ABI_x +Int ABI_y ) )
-              #then   #gas ( ( VGas +Int -128 ) )
-              #else   #if chop( ABI_y ) <=Int 0
-                #then   #gas ( ( VGas +Int -114 ) )
-                #else   #gas ( ( VGas +Int -128 ) )
+            <gas> #gas(VGas) => #if ( ABI_y <Int 0 andBool ( minSInt256 <=Int ABI_y andBool ( ABI_y <=Int maxSInt256 andBool 0 <=Int ( ABI_x +Int ABI_y ) ) ) )
+              #then   #gas ( ( VGas +Int -136 ) )
+              #else   #if ABI_y <=Int 0
+                #then   #gas ( ( VGas +Int -122 ) )
+                #else   #gas ( ( VGas +Int -136 ) )
               #fi
             #fi </gas>
             <memoryUsed> VMemoryUsed </memoryUsed>
@@ -212,7 +214,4 @@ module VAT-SLIP-PASS-ROUGH-SPEC
        andBool ((#rangeUInt(256, ABI_x +Int ABI_y)))))))
 
 
-    [trusted]
-
-
 endmodule