Skip to content

Commit 0a98f60

Browse files
nwatson22rv-auditorPetarMax
authored
Use parallel prover branch (#2400)
* Use parallel prover * Update nix flake with parallel pyk branch * Set Version: 1.0.533 * Fix create_kcfg_explore * Add single-proof parallel workers option * Point to k branch * Set Version: 1.0.534 * Undo update poetry deps * Set Version: 1.0.535 * Update to new pyk version * Set Version: 1.0.536 * Update poetry.lock * Update flake.lock * Update to use server thread parameter * Update flake.lock * Set Version: 1.0.542 * Add max-frontier-parallel option to kevm prove * Preserve interface to avoid breaking kontrol * Set Version: 1.0.545 * Use alternate strategies explicitly to do parallel proving vs sequential * Set Version: 1.0.546 * Simplify Proof strategy names * Set Version: 1.0.547 * Improve strategy pattern * Apply suggestions --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
1 parent 2911fda commit 0a98f60

File tree

5 files changed

+172
-15
lines changed

5 files changed

+172
-15
lines changed

‎kevm-pyk/pyproject.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kevm-pyk"
7-
version = "1.0.546"
7+
version = "1.0.547"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

‎kevm-pyk/src/kevm_pyk/__init__.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,4 @@
66
from typing import Final
77

88

9-
VERSION: Final = '1.0.546'
9+
VERSION: Final = '1.0.547'

‎kevm-pyk/src/kevm_pyk/__main__.py

Lines changed: 35 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,12 @@
2626
SpecOptions,
2727
)
2828
from pyk.cli.utils import file_path
29+
from pyk.cterm import CTermSymbolic
2930
from pyk.kast.outer import KApply, KRewrite, KSort, KToken
3031
from pyk.kcfg import KCFG
32+
from pyk.kcfg.explore import KCFGExplore
3133
from pyk.kdist import kdist
34+
from pyk.kore.rpc import KoreClient
3235
from pyk.kore.tools import PrintOutput, kore_print
3336
from pyk.ktool.kompile import LLVMKompileType
3437
from pyk.ktool.krun import KRunOutput
@@ -320,11 +323,13 @@ class ProveOptions(
320323
KProveOptions,
321324
):
322325
reinit: bool
326+
max_frontier_parallel: int
323327

324328
@staticmethod
325329
def default() -> dict[str, Any]:
326330
return {
327331
'reinit': False,
332+
'max_frontier_parallel': 1,
328333
}
329334

330335

@@ -397,7 +402,28 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
397402
fallback_on=options.fallback_on,
398403
interim_simplification=options.interim_simplification,
399404
no_post_exec_simplify=(not options.post_exec_simplify),
405+
port=options.port,
406+
haskell_threads=options.max_frontier_parallel,
400407
) as kcfg_explore:
408+
409+
def create_kcfg_explore() -> KCFGExplore:
410+
dispatch = None
411+
client = KoreClient(
412+
'localhost',
413+
kcfg_explore.cterm_symbolic._kore_client.port,
414+
bug_report=options.bug_report,
415+
bug_report_id=claim.label,
416+
dispatch=dispatch,
417+
)
418+
cterm_symbolic = CTermSymbolic(
419+
client, kevm.definition, kevm.kompiled_kore, trace_rewrites=options.trace_rewrites
420+
)
421+
return KCFGExplore(
422+
cterm_symbolic,
423+
kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas),
424+
id=claim.label,
425+
)
426+
401427
proof_problem: Proof
402428
if is_functional(claim):
403429
if not options.reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory):
@@ -449,7 +475,7 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
449475
start_time = time.time()
450476
passed = run_prover(
451477
proof_problem,
452-
kcfg_explore,
478+
create_kcfg_explore=create_kcfg_explore,
453479
max_depth=options.max_depth,
454480
max_iterations=options.max_iterations,
455481
cut_point_rules=KEVMSemantics.cut_point_rules(
@@ -462,6 +488,7 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
462488
fail_fast=options.fail_fast,
463489
always_check_subsumption=options.always_check_subsumption,
464490
fast_check_subsumption=options.fast_check_subsumption,
491+
max_frontier_parallel=options.max_frontier_parallel,
465492
)
466493
end_time = time.time()
467494
_LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s')
@@ -844,6 +871,13 @@ def parse(s: str) -> list[T]:
844871
action='store_true',
845872
help='Reinitialize CFGs even if they already exist.',
846873
)
874+
prove_args.add_argument(
875+
'--max-frontier-parallel',
876+
type=int,
877+
dest='max_frontier_parallel',
878+
default=None,
879+
help='Maximum number of branches of a single proof to explore in parallel.',
880+
)
847881

848882
prune_args = command_parser.add_parser(
849883
'prune',

‎kevm-pyk/src/kevm_pyk/utils.py

Lines changed: 134 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
from __future__ import annotations
22

33
import logging
4+
from abc import ABC, abstractmethod
45
from contextlib import contextmanager
6+
from dataclasses import dataclass
57
from pathlib import Path
68
from typing import TYPE_CHECKING
79

@@ -22,6 +24,7 @@
2224
from pyk.kore.rpc import KoreClient, KoreExecLogFormat, TransportType, kore_server
2325
from pyk.proof import APRProof, APRProver
2426
from pyk.proof.implies import EqualityProof, ImpliesProver
27+
from pyk.proof.proof import parallel_advance_proof
2528
from pyk.utils import single
2629

2730
if TYPE_CHECKING:
@@ -91,9 +94,116 @@ def get_apr_proof_for_spec(
9194
return apr_proof
9295

9396

97+
@dataclass
98+
class RunProverParams:
99+
execute_depth: int
100+
terminal_rules: Iterable[str]
101+
cut_point_rules: Iterable[str]
102+
counterexample_info: bool
103+
always_check_subsumption: bool
104+
fast_check_subsumption: bool
105+
106+
107+
class APRProofStrategy(ABC):
108+
params: RunProverParams
109+
110+
def __init__(self, params: RunProverParams) -> None:
111+
self.params = params
112+
113+
@abstractmethod
114+
def prove(self, proof: APRProof, max_iterations: int | None = None, fail_fast: bool = False) -> None: ...
115+
116+
117+
class ParallelStrategy(APRProofStrategy):
118+
_create_kcfg_explore: Callable[[], KCFGExplore]
119+
_max_workers = 1
120+
121+
def __init__(
122+
self,
123+
create_kcfg_explore: Callable[[], KCFGExplore],
124+
params: RunProverParams,
125+
max_workers: int = 1,
126+
) -> None:
127+
self._create_kcfg_explore = create_kcfg_explore
128+
self._max_workers = max_workers
129+
super().__init__(params)
130+
131+
def prove(self, proof: APRProof, max_iterations: int | None = None, fail_fast: bool = False) -> None:
132+
def create_prover() -> APRProver:
133+
return APRProver(
134+
self._create_kcfg_explore(),
135+
execute_depth=self.params.execute_depth,
136+
terminal_rules=self.params.terminal_rules,
137+
cut_point_rules=self.params.cut_point_rules,
138+
counterexample_info=self.params.counterexample_info,
139+
always_check_subsumption=self.params.always_check_subsumption,
140+
fast_check_subsumption=self.params.fast_check_subsumption,
141+
)
142+
143+
parallel_advance_proof(
144+
proof=proof,
145+
create_prover=create_prover,
146+
max_iterations=max_iterations,
147+
fail_fast=fail_fast,
148+
max_workers=self._max_workers,
149+
)
150+
151+
152+
class SequentialStrategy(APRProofStrategy):
153+
_kcfg_explore: KCFGExplore
154+
155+
def __init__(self, kcfg_explore: KCFGExplore, params: RunProverParams) -> None:
156+
self._kcfg_explore = kcfg_explore
157+
super().__init__(params)
158+
159+
def prove(self, proof: APRProof, max_iterations: int | None = None, fail_fast: bool = False) -> None:
160+
prover = APRProver(
161+
self._kcfg_explore,
162+
execute_depth=self.params.execute_depth,
163+
terminal_rules=self.params.terminal_rules,
164+
cut_point_rules=self.params.cut_point_rules,
165+
counterexample_info=self.params.counterexample_info,
166+
always_check_subsumption=self.params.always_check_subsumption,
167+
fast_check_subsumption=self.params.fast_check_subsumption,
168+
)
169+
prover.advance_proof(fail_fast=fail_fast, max_iterations=max_iterations, proof=proof)
170+
171+
172+
def select_apr_strategy(
173+
params: RunProverParams,
174+
max_frontier_parallel: int,
175+
kcfg_explore: KCFGExplore | None = None,
176+
create_kcfg_explore: Callable[[], KCFGExplore] | None = None,
177+
) -> APRProofStrategy:
178+
strategy: APRProofStrategy
179+
180+
if max_frontier_parallel > 1 and create_kcfg_explore is not None:
181+
strategy = ParallelStrategy(
182+
max_workers=max_frontier_parallel,
183+
create_kcfg_explore=create_kcfg_explore,
184+
params=params,
185+
)
186+
elif kcfg_explore is not None or create_kcfg_explore is not None:
187+
if kcfg_explore is not None:
188+
_kcfg_explore = kcfg_explore
189+
else:
190+
assert create_kcfg_explore is not None
191+
_kcfg_explore = create_kcfg_explore()
192+
strategy = SequentialStrategy(
193+
kcfg_explore=_kcfg_explore,
194+
params=params,
195+
)
196+
else:
197+
raise ValueError(
198+
'Must provide at least one of kcfg_explore or create_kcfg_explore, or provide create_kcfg_explore if using max_frontier_parallel > 1.'
199+
)
200+
return strategy
201+
202+
94203
def run_prover(
95204
proof: Proof,
96-
kcfg_explore: KCFGExplore,
205+
kcfg_explore: KCFGExplore | None = None,
206+
create_kcfg_explore: Callable[[], KCFGExplore] | None = None,
97207
max_depth: int = 1000,
98208
max_iterations: int | None = None,
99209
cut_point_rules: Iterable[str] = (),
@@ -102,22 +212,33 @@ def run_prover(
102212
counterexample_info: bool = False,
103213
always_check_subsumption: bool = False,
104214
fast_check_subsumption: bool = False,
215+
max_frontier_parallel: int = 1,
105216
) -> bool:
106217
prover: APRProver | ImpliesProver
107218
try:
108219
if type(proof) is APRProof:
109-
prover = APRProver(
110-
kcfg_explore,
111-
execute_depth=max_depth,
112-
terminal_rules=terminal_rules,
113-
cut_point_rules=cut_point_rules,
114-
counterexample_info=counterexample_info,
115-
always_check_subsumption=always_check_subsumption,
116-
fast_check_subsumption=fast_check_subsumption,
220+
strategy = select_apr_strategy(
221+
create_kcfg_explore=create_kcfg_explore,
222+
kcfg_explore=kcfg_explore,
223+
max_frontier_parallel=max_frontier_parallel,
224+
params=RunProverParams(
225+
always_check_subsumption=always_check_subsumption,
226+
counterexample_info=counterexample_info,
227+
cut_point_rules=cut_point_rules,
228+
execute_depth=max_depth,
229+
fast_check_subsumption=fast_check_subsumption,
230+
terminal_rules=terminal_rules,
231+
),
117232
)
118-
prover.advance_proof(proof, max_iterations=max_iterations, fail_fast=fail_fast)
233+
strategy.prove(fail_fast=fail_fast, max_iterations=max_iterations, proof=proof)
234+
119235
elif type(proof) is EqualityProof:
120-
prover = ImpliesProver(proof, kcfg_explore=kcfg_explore)
236+
if kcfg_explore is not None:
237+
prover = ImpliesProver(proof, kcfg_explore=kcfg_explore)
238+
elif create_kcfg_explore is not None:
239+
prover = ImpliesProver(proof, kcfg_explore=create_kcfg_explore())
240+
else:
241+
raise ValueError('Must provide at least one of kcfg_explore or create_kcfg_explore for EqualityProof.')
121242
prover.advance_proof(proof)
122243
else:
123244
raise ValueError(f'Do not know how to build prover for proof: {proof}')
@@ -293,6 +414,7 @@ def legacy_explore(
293414
bug_report: BugReport | None = None,
294415
haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
295416
haskell_log_entries: Iterable[str] = (),
417+
haskell_threads: int | None = None,
296418
log_axioms_file: Path | None = None,
297419
trace_rewrites: bool = False,
298420
start_server: bool = True,
@@ -315,6 +437,7 @@ def legacy_explore(
315437
smt_tactic=smt_tactic,
316438
haskell_log_format=haskell_log_format,
317439
haskell_log_entries=haskell_log_entries,
440+
haskell_threads=haskell_threads,
318441
log_axioms_file=log_axioms_file,
319442
fallback_on=fallback_on,
320443
interim_simplification=interim_simplification,

‎package/version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
1.0.546
1+
1.0.547

0 commit comments

Comments
 (0)