From 0d3988722945f41c72b5c1cfe122ef176a13d47f Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 11 Jun 2026 17:31:55 +0000 Subject: [PATCH 1/9] kevm-pyk/{cli,__main__}, tests/{conftest,test_prove}: thread --equation-max-local-steps to booster servers Exposes the haskell-backend's new recursive-simplification budget (equation evaluation applied in place at rewritten subterms, hb #4153; backend default 0 = restart-only) through kevm prove and the pytest harness: - cli.py: ProveOptions.equation_max_local_steps + kevm prove flag. - __main__.py: appends the flag to the resolved kore-rpc-booster / booster-dev command; rejects non-booster servers explicitly. - conftest.py / test_prove.py: pytest --equation-max-local-steps option threaded through all prove suites. (cherry picked from commit e6597556e913f1a6340fcb7f959a84422976a772) Co-Authored-By: Claude Fable 5 --- kevm-pyk/src/kevm_pyk/__main__.py | 6 ++++++ kevm-pyk/src/kevm_pyk/cli.py | 13 +++++++++++++ kevm-pyk/src/tests/conftest.py | 15 +++++++++++++++ kevm-pyk/src/tests/integration/test_prove.py | 8 ++++++++ 4 files changed, 42 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 72457cc9a4..0940d6f40c 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -254,6 +254,12 @@ def exec_prove(options: ProveOptions) -> None: else: kore_rpc_command = options.kore_rpc_command + if options.equation_max_local_steps is not None: + # Both booster servers parse the flag (shared Booster.CLOptions); plain kore-rpc does not. + if Path(kore_rpc_command[0]).name not in ('kore-rpc-booster', 'booster-dev'): + raise ValueError(f'--equation-max-local-steps requires a booster server, got: {kore_rpc_command[0]}') + kore_rpc_command += ('--equation-max-local-steps', str(options.equation_max_local_steps)) + def is_functional(claim: KClaim) -> bool: claim_lhs = claim.body if type(claim_lhs) is KRewrite: diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index cf38e22d2c..3bd89d4f6a 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -192,6 +192,17 @@ def _create_argument_parser() -> ArgumentParser: action='store_true', help='Skip the Kore simplification pass after Booster; assume_defined still uses Kore for #Ceil evaluation.', ) + prove_args.add_argument( + '--equation-max-local-steps', + dest='equation_max_local_steps', + type=int, + default=None, + help=( + 'Booster equation budget for in-place evaluation at rewritten subterms before restarting ' + 'traversal from the top (backend default 0 = restart-only). Passed through to ' + 'kore-rpc-booster / booster-dev; requires a haskell-backend that supports the flag.' + ), + ) prove_args.add_argument( '--max-frontier-parallel', type=int, @@ -611,6 +622,7 @@ class ProveOptions( ): reinit: bool booster_only_simplify: bool + equation_max_local_steps: int | None max_frontier_parallel: int @staticmethod @@ -618,6 +630,7 @@ def default() -> dict[str, Any]: return { 'reinit': False, 'booster_only_simplify': False, + 'equation_max_local_steps': None, 'max_frontier_parallel': 1, } diff --git a/kevm-pyk/src/tests/conftest.py b/kevm-pyk/src/tests/conftest.py index f1c6787e2d..03f3f0f9ee 100644 --- a/kevm-pyk/src/tests/conftest.py +++ b/kevm-pyk/src/tests/conftest.py @@ -91,6 +91,16 @@ def pytest_addoption(parser: Parser) -> None: default=False, help='Skip the Kore simplification pass after Booster for all simplify/execute/implies calls.', ) + parser.addoption( + '--equation-max-local-steps', + type=int, + default=None, + help=( + 'Booster equation budget for in-place evaluation at rewritten subterms ' + '(backend default 0 = restart-only). Threaded to kore-rpc-booster / booster-dev ' + 'for all proof tests.' + ), + ) @pytest.fixture @@ -161,3 +171,8 @@ def booster_log_levels(request: FixtureRequest) -> list[str] | None: @pytest.fixture(scope='session') def booster_only_simplify(request: FixtureRequest) -> bool: return request.config.getoption('--booster-only-simplify') + + +@pytest.fixture(scope='session') +def equation_max_local_steps(request: FixtureRequest) -> int | None: + return request.config.getoption('--equation-max-local-steps') diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 0ee7b51922..027f4a857f 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -198,6 +198,7 @@ def _test_prove( workers: int | None = None, direct_subproof_rules: bool = False, booster_only_simplify: bool = False, + equation_max_local_steps: int | None = None, ) -> None: caplog.set_level(logging.INFO) @@ -254,6 +255,7 @@ def _test_prove( 'direct_subproof_rules': direct_subproof_rules, 'booster_only_simplify': booster_only_simplify, 'claim_labels': claim_labels, + 'equation_max_local_steps': equation_max_local_steps, } if haskell_logging: options_dict['haskell_log_entries'] = booster_log_levels or list(HASKELL_LOGGING_ENTRIES) @@ -362,6 +364,7 @@ def test_prove_rules( booster_log_levels: list[str] | None, claim_labels: list[str] | None, booster_only_simplify: bool, + equation_max_local_steps: int | None, ) -> None: _test_prove( spec_file, @@ -378,6 +381,7 @@ def test_prove_rules( booster_log_levels=booster_log_levels, claim_labels=claim_labels, booster_only_simplify=booster_only_simplify, + equation_max_local_steps=equation_max_local_steps, ) @@ -400,6 +404,7 @@ def test_prove_functional( booster_log_levels: list[str] | None, claim_labels: list[str] | None, booster_only_simplify: bool, + equation_max_local_steps: int | None, ) -> None: _test_prove( spec_file, @@ -417,6 +422,7 @@ def test_prove_functional( claim_labels=claim_labels, workers=8, booster_only_simplify=booster_only_simplify, + equation_max_local_steps=equation_max_local_steps, ) @@ -430,6 +436,7 @@ def test_prove_dss( booster_log_levels: list[str] | None, claim_labels: list[str] | None, booster_only_simplify: bool, + equation_max_local_steps: int | None, ) -> None: for spec_file in [REPO_ROOT / 'tests/specs/mcd/vat-spec.k', REPO_ROOT / 'tests/specs/mcd-structured/vat-spec.k']: _test_prove( @@ -449,6 +456,7 @@ def test_prove_dss( workers=8, direct_subproof_rules=True, booster_only_simplify=booster_only_simplify, + equation_max_local_steps=equation_max_local_steps, ) From 0653a7dd59a6a8d38098cc69b696c575ececf2c5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 12 Jun 2026 01:45:11 +0000 Subject: [PATCH 2/9] kevm-pyk/{cli,__main__}, tests/{conftest,test_prove}: default --equation-max-local-steps to 20 Turn the booster recursive-simplification budget on by default (20) for kevm prove and all pytest prove suites, instead of deferring to the backend's restart-only default of 0: - cli.py / conftest.py: default 20; option type narrows to int. - __main__.py: with the budget now always set, a non-booster server skips the flag with a warning instead of raising. Co-Authored-By: Claude Fable 5 --- kevm-pyk/src/kevm_pyk/__main__.py | 9 +++++---- kevm-pyk/src/kevm_pyk/cli.py | 6 +++--- kevm-pyk/src/tests/conftest.py | 6 +++--- kevm-pyk/src/tests/integration/test_prove.py | 8 ++++---- 4 files changed, 15 insertions(+), 14 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 0940d6f40c..d0cc9326f6 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -254,11 +254,12 @@ def exec_prove(options: ProveOptions) -> None: else: kore_rpc_command = options.kore_rpc_command - if options.equation_max_local_steps is not None: - # Both booster servers parse the flag (shared Booster.CLOptions); plain kore-rpc does not. - if Path(kore_rpc_command[0]).name not in ('kore-rpc-booster', 'booster-dev'): - raise ValueError(f'--equation-max-local-steps requires a booster server, got: {kore_rpc_command[0]}') + # Both booster servers parse the flag (shared Booster.CLOptions); plain kore-rpc does not, + # so the budget is skipped (with a warning) rather than rejected now that it defaults on. + if Path(kore_rpc_command[0]).name in ('kore-rpc-booster', 'booster-dev'): kore_rpc_command += ('--equation-max-local-steps', str(options.equation_max_local_steps)) + else: + _LOGGER.warning(f'Ignoring --equation-max-local-steps for non-booster server: {kore_rpc_command[0]}') def is_functional(claim: KClaim) -> bool: claim_lhs = claim.body diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 3bd89d4f6a..65fbd14a4d 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -199,7 +199,7 @@ def _create_argument_parser() -> ArgumentParser: default=None, help=( 'Booster equation budget for in-place evaluation at rewritten subterms before restarting ' - 'traversal from the top (backend default 0 = restart-only). Passed through to ' + 'traversal from the top (default: 20; 0 = restart-only). Passed through to ' 'kore-rpc-booster / booster-dev; requires a haskell-backend that supports the flag.' ), ) @@ -622,7 +622,7 @@ class ProveOptions( ): reinit: bool booster_only_simplify: bool - equation_max_local_steps: int | None + equation_max_local_steps: int max_frontier_parallel: int @staticmethod @@ -630,7 +630,7 @@ def default() -> dict[str, Any]: return { 'reinit': False, 'booster_only_simplify': False, - 'equation_max_local_steps': None, + 'equation_max_local_steps': 20, 'max_frontier_parallel': 1, } diff --git a/kevm-pyk/src/tests/conftest.py b/kevm-pyk/src/tests/conftest.py index 03f3f0f9ee..2a88ee08ed 100644 --- a/kevm-pyk/src/tests/conftest.py +++ b/kevm-pyk/src/tests/conftest.py @@ -94,10 +94,10 @@ def pytest_addoption(parser: Parser) -> None: parser.addoption( '--equation-max-local-steps', type=int, - default=None, + default=20, help=( 'Booster equation budget for in-place evaluation at rewritten subterms ' - '(backend default 0 = restart-only). Threaded to kore-rpc-booster / booster-dev ' + '(default: 20; 0 = restart-only). Threaded to kore-rpc-booster / booster-dev ' 'for all proof tests.' ), ) @@ -174,5 +174,5 @@ def booster_only_simplify(request: FixtureRequest) -> bool: @pytest.fixture(scope='session') -def equation_max_local_steps(request: FixtureRequest) -> int | None: +def equation_max_local_steps(request: FixtureRequest) -> int: return request.config.getoption('--equation-max-local-steps') diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 027f4a857f..ab628db272 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -198,7 +198,7 @@ def _test_prove( workers: int | None = None, direct_subproof_rules: bool = False, booster_only_simplify: bool = False, - equation_max_local_steps: int | None = None, + equation_max_local_steps: int = 20, ) -> None: caplog.set_level(logging.INFO) @@ -364,7 +364,7 @@ def test_prove_rules( booster_log_levels: list[str] | None, claim_labels: list[str] | None, booster_only_simplify: bool, - equation_max_local_steps: int | None, + equation_max_local_steps: int, ) -> None: _test_prove( spec_file, @@ -404,7 +404,7 @@ def test_prove_functional( booster_log_levels: list[str] | None, claim_labels: list[str] | None, booster_only_simplify: bool, - equation_max_local_steps: int | None, + equation_max_local_steps: int, ) -> None: _test_prove( spec_file, @@ -436,7 +436,7 @@ def test_prove_dss( booster_log_levels: list[str] | None, claim_labels: list[str] | None, booster_only_simplify: bool, - equation_max_local_steps: int | None, + equation_max_local_steps: int, ) -> None: for spec_file in [REPO_ROOT / 'tests/specs/mcd/vat-spec.k', REPO_ROOT / 'tests/specs/mcd-structured/vat-spec.k']: _test_prove( From 1dbac5f4e08840a334ffbcfdc204ce6eddc2854e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 14 Jun 2026 18:46:50 +0000 Subject: [PATCH 3/9] tests/specs/functional/asword-eq-false-loop-spec.k, scripts/asword_loop_harness.py: asWord-eq-false loop regression test Adds a functional regression test that guards against reintroducing the non-terminating `asWord-eq-false` simplification (evm-semantics #2859 / kontrol #1153): three claims that evaluate `#asWord ==Int #asWord` known-unequal from the path condition. With the looping rule present each claim's simplification does not terminate and the proof times out; with the rule gone they discharge. Collected by the functional suite (`functional/*-spec.k`) against the shared VERIFICATION definition. `scripts/asword_loop_harness.py` runs such loop specs standalone under a per-claim timeout (LOOP / PASS / FAILED) for local triage, since a non-terminating RPC request produces no per-request log bundle. Co-Authored-By: Claude Fable 5 --- scripts/asword_loop_harness.py | 234 ++++++++++++++++++ .../functional/asword-eq-false-loop-spec.k | 43 ++++ 2 files changed, 277 insertions(+) create mode 100644 scripts/asword_loop_harness.py create mode 100644 tests/specs/functional/asword-eq-false-loop-spec.k diff --git a/scripts/asword_loop_harness.py b/scripts/asword_loop_harness.py new file mode 100644 index 0000000000..7b84e9e0b6 --- /dev/null +++ b/scripts/asword_loop_harness.py @@ -0,0 +1,234 @@ +#!/usr/bin/env python3 +"""Loop-regression harness for functional simplification specs. + +Motivation +---------- +Some simplification lemmas (e.g. `asWord-eq-false`, evm-semantics #2859) are not +loop-safe: on certain term shapes they recurse forever in the Kore simplifier, so +a single `simplify`/`execute` RPC request never returns. A non-terminating request +cannot be caught by the usual per-request Haskell-backend log bundle (that file is +only written when the request *completes*), so the robust signal is wall-clock: run +each claim under a hard timeout and classify by how the prover exits. + +This harness runs every claim of a spec in isolation against a pre-kompiled +definition, bounds each with a timeout, reaps any leftover Kore server, and reports +a per-claim outcome: + + LOOP prover killed at the timeout -> the simplification did not terminate + PASS prover exited 0 -> claim proved (term simplified as expected) + FAILED prover exited non-zero, under bound -> claim did not prove but did terminate + (e.g. left "stuck": loop fixed but the + expected RHS is no longer derivable) + +The three-way split is the point: a fix that stops the loop can land a claim in +either PASS (still proves the expected result) or FAILED (terminates but can no +longer prove it), and those demand different follow-ups. See the header comment of +`tests/specs/functional/asword-eq-false-loop-spec.k` for the worked example. + +The definition is an *input* (kompile separately, never timed here): the lemma under +test is part of the kompiled definition, so each lemma variant -- buggy, guarded, +[smt-lemma], dropped -- is its own `--definition` dir, and comparing variants is just +re-running this harness against each. + +Usage +----- + uv --project kevm-pyk/ run python scripts/asword_loop_harness.py \ + --spec tests/specs/functional/asword-eq-false-loop-spec.k \ + --definition /tmp/asword-exp/buggy-kompiled \ + --timeout 120 \ + --out /tmp/asword-loop-report.md + +`--claims a,b` restricts to specific labels; default is every `claim [label]:` in +the spec. `--spec-module` defaults to the file stem upper-cased (the kevm +convention), matching how the file's module is named. +""" + +from __future__ import annotations + +import argparse +import json +import os +import re +import signal +import subprocess +import sys +import time +from dataclasses import asdict, dataclass +from pathlib import Path + +REPO_ROOT = Path(__file__).resolve().parent.parent +INCLUDES = ( + REPO_ROOT / 'kevm-pyk/src/kevm_pyk/kproj/evm-semantics', + REPO_ROOT / 'kevm-pyk/src/kevm_pyk/kproj/plugin', + # So a loop spec under functional/loops/ keeps the standard `requires "verification.k"` + # (resolved here via -I) and needs no edit when it later moves up into functional/. + REPO_ROOT / 'tests/specs/functional', +) + +# kevm prove server selection; the harness injects the matching flags. +SERVER_FLAGS = { + 'booster': (), # kore-rpc-booster (fallback on) -- the default, the CSE config + 'kore': ('--no-use-booster',), # pure kore-rpc -- loops directly, no booster layer + 'booster-dev': ('--use-booster-dev',), # booster only, no kore fallback +} + +# Kore/booster server process names to reap after each claim (matched with pgrep -x, +# never pkill -f, so we never match this script's own command line). +SERVER_PROCS = ('kore-rpc-booster', 'booster-dev', 'kore-rpc') + + +@dataclass +class ClaimResult: + claim: str + outcome: str # LOOP | PASS | FAILED + exit_code: int + seconds: float + log: str + + +def parse_claim_labels(spec: Path) -> list[str]: + """Every `claim [label]:` in source order.""" + labels = re.findall(r'claim\s*\[([A-Za-z0-9._-]+)\]', spec.read_text()) + if not labels: + raise SystemExit(f'No `claim [label]:` found in {spec}') + return labels + + +def reap_servers() -> None: + for name in SERVER_PROCS: + # pgrep -x: exact process-name match only; avoids killing the harness/shell. + pids = subprocess.run(['pgrep', '-x', name], capture_output=True, text=True).stdout.split() + for pid in pids: + subprocess.run(['kill', '-9', pid], stderr=subprocess.DEVNULL) + + +def run_claim( + spec: Path, + definition: Path, + spec_module: str, + claim: str, + timeout_s: int, + server_mode: str, + eq_max_local_steps: int | None, + workdir: Path, +) -> ClaimResult: + save_dir = workdir / f'save-{claim}' + log_path = workdir / f'run-{claim}.log' + cmd = [ + 'uv', '--project', str(REPO_ROOT / 'kevm-pyk'), 'run', 'kevm', 'prove', + str(spec), + '--definition', str(definition), + '--spec-module', spec_module, + '--claim', f'{spec_module}.{claim}', + '--save-directory', str(save_dir), '--reinit', + *SERVER_FLAGS[server_mode], + '--verbose', + ] # fmt: skip + for inc in INCLUDES: + cmd += ['-I', str(inc)] + if eq_max_local_steps is not None: + cmd += ['--equation-max-local-steps', str(eq_max_local_steps)] + + # Bound the run in-process: start the child in its own session (process group) so a + # timeout can SIGKILL the *whole tree* -- uv, kevm, and the Kore server it spawned -- + # in one shot. Relying on the `timeout` coreutil leaves grandchild Kore servers behind + # (the loop is server-side) and its exit code is awkward to read back through Python. + start = time.monotonic() + timed_out = False + with log_path.open('w') as fh: + proc = subprocess.Popen(cmd, stdout=fh, stderr=subprocess.STDOUT, start_new_session=True) + try: + proc.communicate(timeout=timeout_s) + except subprocess.TimeoutExpired: + timed_out = True + os.killpg(os.getpgid(proc.pid), signal.SIGKILL) + proc.wait() + elapsed = time.monotonic() - start + reap_servers() # belt-and-suspenders for any server that escaped the process group + + if timed_out: + outcome = 'LOOP' + elif proc.returncode == 0: + outcome = 'PASS' + else: + outcome = 'FAILED' + return ClaimResult(claim, outcome, proc.returncode, round(elapsed, 1), str(log_path)) + + +def render_table(results: list[ClaimResult], header: dict[str, str]) -> str: + lines = [f'# asWord loop harness -- {header["spec_module"]}', ''] + for k, v in header.items(): + lines.append(f'- {k}: {v}') + lines.append('') + rows = [('claim', 'outcome', 'exit', 'seconds')] + rows += [(r.claim, r.outcome, str(r.exit_code), f'{r.seconds:.1f}') for r in results] + widths = [max(len(row[i]) for row in rows) for i in range(len(rows[0]))] + for n, row in enumerate(rows): + lines.append('| ' + ' | '.join(c.ljust(widths[i]) for i, c in enumerate(row)) + ' |') + if n == 0: + lines.append('|' + '|'.join('-' * (widths[i] + 2) for i in range(len(row))) + '|') + return '\n'.join(lines) + '\n' + + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--spec', type=Path, required=True, help='Functional spec .k file.') + ap.add_argument('--definition', type=Path, required=True, help='Pre-kompiled definition dir.') + ap.add_argument('--spec-module', help='Spec module name (default: file stem upper-cased).') + ap.add_argument('--claims', help='Comma-separated claim labels (default: all in spec).') + ap.add_argument('--timeout', type=int, default=120, help='Per-claim wall-clock bound, seconds (default 120).') + ap.add_argument('--server-mode', choices=tuple(SERVER_FLAGS), default='booster') + ap.add_argument('--equation-max-local-steps', type=int, default=None, help='Booster local-step budget.') + ap.add_argument('--workdir', type=Path, default=Path('/tmp/asword-exp/runs'), help='Where save dirs and logs land.') + ap.add_argument('--out', type=Path, help='Write the markdown report here (and a .json sidecar).') + args = ap.parse_args() + + spec_module = args.spec_module or args.spec.stem.upper() + claims = args.claims.split(',') if args.claims else parse_claim_labels(args.spec) + args.workdir.mkdir(parents=True, exist_ok=True) + + header = { + 'spec': str(args.spec), + 'spec_module': spec_module, + 'definition': str(args.definition), + 'server_mode': args.server_mode, + 'equation_max_local_steps': str(args.equation_max_local_steps), + 'timeout_s': str(args.timeout), + } + print( + f'Running {len(claims)} claim(s) against {args.definition} [{args.server_mode}, timeout {args.timeout}s]', + file=sys.stderr, + ) + + results: list[ClaimResult] = [] + for claim in claims: + print(f' {claim} ...', end='', flush=True, file=sys.stderr) + r = run_claim( + args.spec, + args.definition, + spec_module, + claim, + args.timeout, + args.server_mode, + args.equation_max_local_steps, + args.workdir, + ) + print(f' {r.outcome} ({r.seconds:.0f}s, exit {r.exit_code})', file=sys.stderr) + results.append(r) + + report = render_table(results, header) + print('\n' + report) + if args.out: + args.out.parent.mkdir(parents=True, exist_ok=True) + args.out.write_text(report) + args.out.with_suffix('.json').write_text( + json.dumps({'header': header, 'results': [asdict(r) for r in results]}, indent=2) + '\n' + ) + print(f'Wrote {args.out} and {args.out.with_suffix(".json")}', file=sys.stderr) + + # Exit non-zero if any claim looped, so the harness is CI-usable. + return 1 if any(r.outcome == 'LOOP' for r in results) else 0 + + +if __name__ == '__main__': + raise SystemExit(main()) diff --git a/tests/specs/functional/asword-eq-false-loop-spec.k b/tests/specs/functional/asword-eq-false-loop-spec.k new file mode 100644 index 0000000000..8b2c361b45 --- /dev/null +++ b/tests/specs/functional/asword-eq-false-loop-spec.k @@ -0,0 +1,43 @@ +requires "verification.k" + +module ASWORD-EQ-FALSE-LOOP-SPEC + imports VERIFICATION + + // Regression test for the non-terminating `asWord-eq-false` simplification loop + // (evm-semantics #2859 / kontrol #1153). The offending rule has been removed from + // `lemmas/evm-int-simplification.k`; these claims guard against it being reintroduced. + // + // The removed rule was: + // rule [asWord-eq-false]: #asWord(B) ==Int X => false requires X =/=Int #asWord(B) [simplification] + // It is loop-safe ONLY when `X` is not itself an `#asWord(_)`. When BOTH sides of the + // `==Int` are `#asWord` terms, applying it rewrites the equality into its own `requires` + // with the two `#asWord` operands swapped — still `#asWord`-on-the-left — so it matches + // again, swaps back, and recurses without bound (observed: one request looping >21 min at + // 96% CPU, the rule nested 5,406 deep in the Kore simplifier). + // + // Each claim below asks the simplifier to evaluate an equality with `#asWord` on BOTH + // sides, known unequal from the path condition. Expected result: `false`, discharged + // against the path condition. If the looping rule is reintroduced, simplification of the + // left-hand `runLemma` term loops and the proof TIMES OUT. `asWord-lt-false` / + // `asWord-le-false` need no analogue: ` runLemma ( #asWord ( B1:Bytes ) ==Int #asWord ( B2:Bytes ) ) => doneLemma ( false ) ... + requires #asWord ( B1 ) =/=Int #asWord ( B2 ) + + // The shape actually observed in the CSE proofs: a plain word vs an `#asWord` over a + // buffer expression (a `+Bytes` of symbolic operands does not reduce, so the right side + // stays `#asWord`, keeping both operands `#asWord` exactly as in the captured loop term). + claim [asword-eq-false-buffer]: + runLemma ( #asWord ( B1:Bytes ) ==Int #asWord ( B2:Bytes +Bytes B3:Bytes ) ) => doneLemma ( false ) ... + requires #asWord ( B1 ) =/=Int #asWord ( B2 +Bytes B3 ) + + // Same hazard reached via `=/=Int` (which desugars to `notBool(_ ==Int_)`), the form in + // which the loop term appeared inside another rule's requires. + claim [asword-neq-true-symmetric]: + runLemma ( #asWord ( B1:Bytes ) =/=Int #asWord ( B2:Bytes ) ) => doneLemma ( true ) ... + requires #asWord ( B1 ) =/=Int #asWord ( B2 ) + +endmodule From 43b158dd76d7d54465e5174bfd62aecc96e8b12c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 14 Jun 2026 18:46:50 +0000 Subject: [PATCH 4/9] lemmas/evm-int-simplification.k: remove non-terminating asWord-eq-false simplification `asWord-eq-false` (added in #2859) loops in the Kore simplifier when both operands of the `==Int` are `#asWord` terms: applying it rewrites the equality into its own `requires` with the operands swapped (still `#asWord`-on-the-left), so it re-matches and recurses without bound. This was the root cause of the CSE-proof timeouts (kontrol #1153). Removing the rule ends the loop; the ` --- .../evm-semantics/lemmas/evm-int-simplification.k | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k index f1735b4664..f04d4ccdd9 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k @@ -136,12 +136,12 @@ module EVM-INT-SIMPLIFICATION // neither rule fires on the other's requires. rule [asWord-lt-false]: #asWord ( B:Bytes ) false requires X <=Int #asWord ( B ) [simplification] rule [asWord-le-false]: #asWord ( B:Bytes ) <=Int X:Int => false requires X false requires X =/=Int #asWord ( B ) [simplification] + // Note: there is intentionally no `asWord-eq-false` analogue of the ` false requires X =/=Int #asWord(B)`) is not loop-safe: when + // both operands are `#asWord`, applying it rewrites the equality into its own `requires` with the + // two operands swapped — still `#asWord`-on-the-left — so it re-matches and recurses without bound + // in the Kore simplifier. ` Date: Sun, 14 Jun 2026 19:41:17 +0000 Subject: [PATCH 5/9] scripts/asword_loop_harness.py: drop loop-triage harness from the PR The asWord-eq-false regression is guarded by the functional spec alone (tests/specs/functional/asword-eq-false-loop-spec.k); the standalone triage harness is not needed in this branch. Co-Authored-By: Claude Fable 5 --- scripts/asword_loop_harness.py | 234 --------------------------------- 1 file changed, 234 deletions(-) delete mode 100644 scripts/asword_loop_harness.py diff --git a/scripts/asword_loop_harness.py b/scripts/asword_loop_harness.py deleted file mode 100644 index 7b84e9e0b6..0000000000 --- a/scripts/asword_loop_harness.py +++ /dev/null @@ -1,234 +0,0 @@ -#!/usr/bin/env python3 -"""Loop-regression harness for functional simplification specs. - -Motivation ----------- -Some simplification lemmas (e.g. `asWord-eq-false`, evm-semantics #2859) are not -loop-safe: on certain term shapes they recurse forever in the Kore simplifier, so -a single `simplify`/`execute` RPC request never returns. A non-terminating request -cannot be caught by the usual per-request Haskell-backend log bundle (that file is -only written when the request *completes*), so the robust signal is wall-clock: run -each claim under a hard timeout and classify by how the prover exits. - -This harness runs every claim of a spec in isolation against a pre-kompiled -definition, bounds each with a timeout, reaps any leftover Kore server, and reports -a per-claim outcome: - - LOOP prover killed at the timeout -> the simplification did not terminate - PASS prover exited 0 -> claim proved (term simplified as expected) - FAILED prover exited non-zero, under bound -> claim did not prove but did terminate - (e.g. left "stuck": loop fixed but the - expected RHS is no longer derivable) - -The three-way split is the point: a fix that stops the loop can land a claim in -either PASS (still proves the expected result) or FAILED (terminates but can no -longer prove it), and those demand different follow-ups. See the header comment of -`tests/specs/functional/asword-eq-false-loop-spec.k` for the worked example. - -The definition is an *input* (kompile separately, never timed here): the lemma under -test is part of the kompiled definition, so each lemma variant -- buggy, guarded, -[smt-lemma], dropped -- is its own `--definition` dir, and comparing variants is just -re-running this harness against each. - -Usage ------ - uv --project kevm-pyk/ run python scripts/asword_loop_harness.py \ - --spec tests/specs/functional/asword-eq-false-loop-spec.k \ - --definition /tmp/asword-exp/buggy-kompiled \ - --timeout 120 \ - --out /tmp/asword-loop-report.md - -`--claims a,b` restricts to specific labels; default is every `claim [label]:` in -the spec. `--spec-module` defaults to the file stem upper-cased (the kevm -convention), matching how the file's module is named. -""" - -from __future__ import annotations - -import argparse -import json -import os -import re -import signal -import subprocess -import sys -import time -from dataclasses import asdict, dataclass -from pathlib import Path - -REPO_ROOT = Path(__file__).resolve().parent.parent -INCLUDES = ( - REPO_ROOT / 'kevm-pyk/src/kevm_pyk/kproj/evm-semantics', - REPO_ROOT / 'kevm-pyk/src/kevm_pyk/kproj/plugin', - # So a loop spec under functional/loops/ keeps the standard `requires "verification.k"` - # (resolved here via -I) and needs no edit when it later moves up into functional/. - REPO_ROOT / 'tests/specs/functional', -) - -# kevm prove server selection; the harness injects the matching flags. -SERVER_FLAGS = { - 'booster': (), # kore-rpc-booster (fallback on) -- the default, the CSE config - 'kore': ('--no-use-booster',), # pure kore-rpc -- loops directly, no booster layer - 'booster-dev': ('--use-booster-dev',), # booster only, no kore fallback -} - -# Kore/booster server process names to reap after each claim (matched with pgrep -x, -# never pkill -f, so we never match this script's own command line). -SERVER_PROCS = ('kore-rpc-booster', 'booster-dev', 'kore-rpc') - - -@dataclass -class ClaimResult: - claim: str - outcome: str # LOOP | PASS | FAILED - exit_code: int - seconds: float - log: str - - -def parse_claim_labels(spec: Path) -> list[str]: - """Every `claim [label]:` in source order.""" - labels = re.findall(r'claim\s*\[([A-Za-z0-9._-]+)\]', spec.read_text()) - if not labels: - raise SystemExit(f'No `claim [label]:` found in {spec}') - return labels - - -def reap_servers() -> None: - for name in SERVER_PROCS: - # pgrep -x: exact process-name match only; avoids killing the harness/shell. - pids = subprocess.run(['pgrep', '-x', name], capture_output=True, text=True).stdout.split() - for pid in pids: - subprocess.run(['kill', '-9', pid], stderr=subprocess.DEVNULL) - - -def run_claim( - spec: Path, - definition: Path, - spec_module: str, - claim: str, - timeout_s: int, - server_mode: str, - eq_max_local_steps: int | None, - workdir: Path, -) -> ClaimResult: - save_dir = workdir / f'save-{claim}' - log_path = workdir / f'run-{claim}.log' - cmd = [ - 'uv', '--project', str(REPO_ROOT / 'kevm-pyk'), 'run', 'kevm', 'prove', - str(spec), - '--definition', str(definition), - '--spec-module', spec_module, - '--claim', f'{spec_module}.{claim}', - '--save-directory', str(save_dir), '--reinit', - *SERVER_FLAGS[server_mode], - '--verbose', - ] # fmt: skip - for inc in INCLUDES: - cmd += ['-I', str(inc)] - if eq_max_local_steps is not None: - cmd += ['--equation-max-local-steps', str(eq_max_local_steps)] - - # Bound the run in-process: start the child in its own session (process group) so a - # timeout can SIGKILL the *whole tree* -- uv, kevm, and the Kore server it spawned -- - # in one shot. Relying on the `timeout` coreutil leaves grandchild Kore servers behind - # (the loop is server-side) and its exit code is awkward to read back through Python. - start = time.monotonic() - timed_out = False - with log_path.open('w') as fh: - proc = subprocess.Popen(cmd, stdout=fh, stderr=subprocess.STDOUT, start_new_session=True) - try: - proc.communicate(timeout=timeout_s) - except subprocess.TimeoutExpired: - timed_out = True - os.killpg(os.getpgid(proc.pid), signal.SIGKILL) - proc.wait() - elapsed = time.monotonic() - start - reap_servers() # belt-and-suspenders for any server that escaped the process group - - if timed_out: - outcome = 'LOOP' - elif proc.returncode == 0: - outcome = 'PASS' - else: - outcome = 'FAILED' - return ClaimResult(claim, outcome, proc.returncode, round(elapsed, 1), str(log_path)) - - -def render_table(results: list[ClaimResult], header: dict[str, str]) -> str: - lines = [f'# asWord loop harness -- {header["spec_module"]}', ''] - for k, v in header.items(): - lines.append(f'- {k}: {v}') - lines.append('') - rows = [('claim', 'outcome', 'exit', 'seconds')] - rows += [(r.claim, r.outcome, str(r.exit_code), f'{r.seconds:.1f}') for r in results] - widths = [max(len(row[i]) for row in rows) for i in range(len(rows[0]))] - for n, row in enumerate(rows): - lines.append('| ' + ' | '.join(c.ljust(widths[i]) for i, c in enumerate(row)) + ' |') - if n == 0: - lines.append('|' + '|'.join('-' * (widths[i] + 2) for i in range(len(row))) + '|') - return '\n'.join(lines) + '\n' - - -def main() -> int: - ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) - ap.add_argument('--spec', type=Path, required=True, help='Functional spec .k file.') - ap.add_argument('--definition', type=Path, required=True, help='Pre-kompiled definition dir.') - ap.add_argument('--spec-module', help='Spec module name (default: file stem upper-cased).') - ap.add_argument('--claims', help='Comma-separated claim labels (default: all in spec).') - ap.add_argument('--timeout', type=int, default=120, help='Per-claim wall-clock bound, seconds (default 120).') - ap.add_argument('--server-mode', choices=tuple(SERVER_FLAGS), default='booster') - ap.add_argument('--equation-max-local-steps', type=int, default=None, help='Booster local-step budget.') - ap.add_argument('--workdir', type=Path, default=Path('/tmp/asword-exp/runs'), help='Where save dirs and logs land.') - ap.add_argument('--out', type=Path, help='Write the markdown report here (and a .json sidecar).') - args = ap.parse_args() - - spec_module = args.spec_module or args.spec.stem.upper() - claims = args.claims.split(',') if args.claims else parse_claim_labels(args.spec) - args.workdir.mkdir(parents=True, exist_ok=True) - - header = { - 'spec': str(args.spec), - 'spec_module': spec_module, - 'definition': str(args.definition), - 'server_mode': args.server_mode, - 'equation_max_local_steps': str(args.equation_max_local_steps), - 'timeout_s': str(args.timeout), - } - print( - f'Running {len(claims)} claim(s) against {args.definition} [{args.server_mode}, timeout {args.timeout}s]', - file=sys.stderr, - ) - - results: list[ClaimResult] = [] - for claim in claims: - print(f' {claim} ...', end='', flush=True, file=sys.stderr) - r = run_claim( - args.spec, - args.definition, - spec_module, - claim, - args.timeout, - args.server_mode, - args.equation_max_local_steps, - args.workdir, - ) - print(f' {r.outcome} ({r.seconds:.0f}s, exit {r.exit_code})', file=sys.stderr) - results.append(r) - - report = render_table(results, header) - print('\n' + report) - if args.out: - args.out.parent.mkdir(parents=True, exist_ok=True) - args.out.write_text(report) - args.out.with_suffix('.json').write_text( - json.dumps({'header': header, 'results': [asdict(r) for r in results]}, indent=2) + '\n' - ) - print(f'Wrote {args.out} and {args.out.with_suffix(".json")}', file=sys.stderr) - - # Exit non-zero if any claim looped, so the harness is CI-usable. - return 1 if any(r.outcome == 'LOOP' for r in results) else 0 - - -if __name__ == '__main__': - raise SystemExit(main()) From eb7de1c1a0f2619858cd6e47d25bc240eb0d81fc Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 14 Jun 2026 21:46:50 +0000 Subject: [PATCH 6/9] tests/specs/functional/loops/eq-false-lt-loop-spec.k: exemplar for the relocated eq-false-lt CSE loop MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Captures the second CSE non-termination layer (evm-semantics #2859 / kontrol #1153) that remains after asWord-eq-false is removed: eq-false-lt × AccountCellMap definedness, a Kore constraint-simplifier fixpoint failure on undetermined account-id comparisons. Kept under loops/ (not collected by the functional suite) because it is UNVERIFIED and, per the change request, does not reproduce in a fresh single proof — the spin only arises on a long-lived server once constraints accumulate. Co-Authored-By: Claude Fable 5 --- .../functional/loops/eq-false-lt-loop-spec.k | 68 +++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 tests/specs/functional/loops/eq-false-lt-loop-spec.k diff --git a/tests/specs/functional/loops/eq-false-lt-loop-spec.k b/tests/specs/functional/loops/eq-false-lt-loop-spec.k new file mode 100644 index 0000000000..b0875c256e --- /dev/null +++ b/tests/specs/functional/loops/eq-false-lt-loop-spec.k @@ -0,0 +1,68 @@ +requires "verification.k" + +module EQ-FALSE-LT-LOOP-SPEC + imports VERIFICATION + + // Regression exemplar for the SECOND CSE non-termination layer (evm-semantics #2859 / kontrol #1153), + // the one that remains after `asWord-eq-false` is removed. See `evm-semantics-cse-loop-change-request.md`. + // + // HOW THIS WAS FOUND: rebuilding KEVM with `asWord-eq-false` deleted (branch `asword-eq-false-loop-fix`, + // == kontrol-side "variant A") does NOT stop the CSE proofs hanging — proof #4 + // `ArithmeticCallTest.test_double_add_sub_external` still spins >25 min in one `execute` request. The + // loop simply RELOCATES. Server-side context logging of the hanging request shows two rules dominating, + // ~16-17k attempts each, in two different engines under the same execute request: + // + // * booster > execute > simplify > … > [eq-false-lt] > smt (15 865 attempts) + // rule [eq-false-lt]: A:Int ==Int B:Int => false requires A execute > constraint > term:90151e4 > > success (17 082 attempts, + // re-firing on the SAME constraint term) + // + // MECHANISM (a two-engine fixpoint failure, NOT a single self-loop like asWord-eq-false): + // 1. `#Ceil( AccountCellMap)` definedness requires the account ids be DISTINCT, i.e. it emits + // predicates of the form `ACCOUNT_ID ==Int => false`. + // 2. `eq-false-lt` (concrete RHS) is invited to discharge each one via its side condition + // `ACCOUNT_ID `. With ACCOUNT_ID a symbolic account id constrained only to a + // range (e.g. `[0, pow160)`) that does NOT decide the comparison, SMT returns (Sat,Sat) — + // UNDETERMINED (2 518 such verdicts captured). The rule cannot fire and the predicate cannot reduce. + // 3. Because the account-distinctness predicate never simplifies to a stable form, the Kore constraint + // simplifier never reaches a fixpoint and re-evaluates the AccountCellMap `#Ceil` on the same term + // thousands of times — each pass paying a fresh ~500 ms undetermined SMT round-trip per account id. + // + // The captured concrete address is `645326474426547203313410069153905908525362434349` (a 160-bit value); + // the symbolic ids were CALLER_ID, ORIGIN_ID, and the deployed-contract ids. + // + // SCOPE / CAVEAT — READ BEFORE RELYING ON THIS: + // The faithful trigger is the INTERACTION of AccountCellMap definedness with `eq-false-lt`, driven by + // the Kore constraint simplifier's lack of a fixpoint guard. A bare `runLemma(ACCT ==Int )` + // (claim 1 below) reproduces the EXPENSIVE-UNDETERMINED-SMT step but will most likely return the term + // undetermined ONCE rather than spin, because the AccountCellMap `#Ceil` that re-presents the predicate + // is absent. Claim 2 adds a two-account `` cell so the definedness machinery is in play; this + // is the closer reproduction, but whether it spins depends on the backend's constraint-simplification + // fixpoint behaviour, which is the real defect. Please run BOTH on the buggy build and report which + // actually loops; the primary recommendation to the team is a backend fixpoint/termination guard plus + // making `eq-false-lt` cheap (or skipped) when `A runLemma ( ACCT_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) + => doneLemma ( ?_RESULT:Bool ) ... + requires 0 <=Int ACCT_ID andBool ACCT_ID cell, so evaluating the + // configuration's definedness invokes the AccountCellMap `#Ceil` that emits the account-distinctness + // predicate `ACCT_ID_1 ==Int ACCT_ID_2 => false`, which `eq-false-lt` then tries (and fails) to discharge. + // Both ids are range-bounded but unordered, so the distinctness comparison is undetermined — the captured + // shape. (Adjust the cell context to match the project's VERIFICATION module if `` is wrapped.) + claim [eq-false-lt-acctmap-definedness]: + runLemma ( .Bytes ) => doneLemma ( .Bytes ) ... + + ACCT_ID_1:Int ... + ACCT_ID_2:Int ... + ... + + requires 0 <=Int ACCT_ID_1 andBool ACCT_ID_1 Date: Sun, 14 Jun 2026 23:43:07 +0000 Subject: [PATCH 7/9] lemmas/int-simplification.k: temporarily disable eq-false-lt (drives CSE Kore non-termination) eq-false-lt (`A ==Int B => false requires A AccountCellMap)`, the account-distinctness predicates `ACCT_ID ==Int => false` invite this rule, whose side condition `A --- .../kproj/evm-semantics/lemmas/int-simplification.k | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 84e1b1c0cb..52318db789 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -287,7 +287,15 @@ module INT-SIMPLIFICATION-COMMON rule A ==Int B => false requires 0 <=Int A andBool B false requires A AccountCellMap)`, the account + // distinctness predicates `ACCT_ID ==Int => false` invite this rule, whose side + // condition `A false requires A true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)] From a4f3a541f5f0cdc88017c0b33a973049b51ffe81 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 15 Jun 2026 02:21:14 +0000 Subject: [PATCH 8/9] tests/specs/functional/eq-false-lt-loop-spec.k: promote eq-false-lt exemplar for CI collection Move the eq-false-lt loop exemplar out of the non-collected loops/ subdir into tests/specs/functional/ so the functional test harness picks it up via spec_files('functional', '*-spec.k'). Co-Authored-By: Claude Fable 5 --- tests/specs/functional/{loops => }/eq-false-lt-loop-spec.k | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename tests/specs/functional/{loops => }/eq-false-lt-loop-spec.k (100%) diff --git a/tests/specs/functional/loops/eq-false-lt-loop-spec.k b/tests/specs/functional/eq-false-lt-loop-spec.k similarity index 100% rename from tests/specs/functional/loops/eq-false-lt-loop-spec.k rename to tests/specs/functional/eq-false-lt-loop-spec.k From bbadb5521247d1818452c9ed290b91dfcd0dac33 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 15 Jun 2026 14:13:55 +0000 Subject: [PATCH 9/9] lemmas/buf.md, lemmas-no-smt-spec.k: add powByteLen-lt-concrete-false to close asWord-unif-03/04 without asWord-eq-false Removing the looping asWord-eq-false lemma un-masked a coverage gap: the lemmas-spec asWord-unif-03/04 claims (#2604) decompose an out-of-range #asWord(B) ==Int CONST via asWord-eq-num into CONST --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md | 7 +++++++ tests/specs/functional/lemmas-no-smt-spec.k | 8 ++++++++ 2 files changed, 15 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md index 1ea46865b8..3a8912d385 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md @@ -48,6 +48,13 @@ module BUF rule [powByteLen-lt-concrete]: CONST true requires 0 <=Int N andBool CONST false + requires 0 <=Int N andBool 2 ^Int (8 *Int N) <=Int CONST + [simplification, concrete(CONST, N), preserves-definedness] rule #write(WM, IDX, VAL) => WM [ IDX := #buf(1, VAL) ] [simplification] rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA) diff --git a/tests/specs/functional/lemmas-no-smt-spec.k b/tests/specs/functional/lemmas-no-smt-spec.k index cf269ed100..f1cf9d9296 100644 --- a/tests/specs/functional/lemmas-no-smt-spec.k +++ b/tests/specs/functional/lemmas-no-smt-spec.k @@ -85,4 +85,12 @@ module LEMMAS-NO-SMT-SPEC claim [powByteLen-lt-concrete]: runLemma ( 31 doneLemma ( true ) ... + // powByteLen-lt-concrete-false: CONST false when CONST does + // not fit into N bytes. The companion false-direction of the rule above; together they + // make the concrete comparison total. Regression for the `asWord-unif-03/04` lemmas-spec + // claims, which decompose an out-of-range `#asWord(B) ==Int CONST` into exactly this + // comparison and previously relied on the (removed, looping) `asWord-eq-false` to close. + claim [powByteLen-lt-concrete-false]: + runLemma ( 2 ^Int 160 doneLemma ( false ) ... + endmodule