From 983360b9b0367c33a7bd8b837ac4514a3588ce90 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 22 May 2026 15:36:17 +0000 Subject: [PATCH 01/19] evm.md: add total to #widthOpCode, preserves-definedness to #computeValidJumpDests rules `total` on `#widthOpCode` tells the Haskell backend the function is defined for all inputs, suppressing spurious #Ceil obligations. `preserves-definedness` on all four `#computeValidJumpDests` rules unblocks the booster's equation evaluator: without it the backend aborted with `[failure][break] Uncertain about definedness` on every attempt because `PGM[I]` (byte indexing) is non-total in general. With the annotation the booster correctly iterates the 2001-byte concrete prefix via LLVM and halts at the symbolic `#buf` boundary. Co-Authored-By: Claude Sonnet 4.6 --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index aa0e14fd92..bb90886791 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1750,10 +1750,10 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax Bytes ::= #computeValidJumpDests(Bytes) [symbol(computeValidJumpDests), function, memo, total] | #computeValidJumpDests(Bytes, Int, Bytes, Int) [symbol(computeValidJumpDestsAux), function ] // ------------------------------------------------------------------------------------------------------------------------- - rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, padRightBytes(.Bytes, lengthBytes(PGM), 0), lengthBytes(PGM)) - rule #computeValidJumpDests( _, I, RESULT, LEN) => RESULT requires I >=Int LEN - rule #computeValidJumpDests(PGM, I, RESULT, LEN) => #computeValidJumpDests(PGM, I +Int 1, RESULT[I <- 1], LEN) requires I #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT, LEN) requires I #computeValidJumpDests(PGM, 0, padRightBytes(.Bytes, lengthBytes(PGM), 0), lengthBytes(PGM)) [preserves-definedness] + rule #computeValidJumpDests( _, I, RESULT, LEN) => RESULT requires I >=Int LEN [preserves-definedness] + rule #computeValidJumpDests(PGM, I, RESULT, LEN) => #computeValidJumpDests(PGM, I +Int 1, RESULT[I <- 1], LEN) requires I #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT, LEN) requires I W -Int 94 requires W >=Int 96 andBool W <=Int 127 rule #widthOpCode(_) => 1 [owise] From 1e96bf5bf6ed91a885679896dacfcc6d86256e92 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 23 May 2026 01:25:22 +0000 Subject: [PATCH 02/19] lemmas/bytes-simplification.k: add preserves-definedness to lookup-as-asWord MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Without this attribute Booster refused to apply the rule because the LHS contains the non-total hook Lbl_[_]_BYTES-HOOKE. After the fix Booster correctly applies it (8× succeeded in the execute-node simplify request). Analysis: scripts/bench-prove.py --analyse-fallbacks shows the "Uncertain about definedness of rule due to: non-total symbol Lbl_[_]_BYTES-HOOKE" error gone, replaced by successful Booster applications. The rule-index gap and indeterminate-match cases for other equations remain and will be addressed in follow-up commits. Co-Authored-By: Claude Sonnet 4.6 --- .../kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 392a50c6e9..658be17aeb 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -306,5 +306,5 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lookup-as-asWord]: B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) ) requires 0 <=Int I andBool I Date: Mon, 25 May 2026 15:06:14 +0000 Subject: [PATCH 03/19] lemmas: Round 2 Booster gap fixes bytes-simplification.k: add preserves-definedness to lengthBytes-buf and lengthBytes-range. evm-int-simplification.k: add asWord-buf-inversion-rangeUInt256. --- .../kproj/evm-semantics/lemmas/bytes-simplification.k | 4 ++-- .../kproj/evm-semantics/lemmas/evm-int-simplification.k | 8 ++++++++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 658be17aeb..b99732cb2d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -267,8 +267,8 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lengthBytes-geq-zero]: 0 <=Int lengthBytes ( _ ) => true [simplification, smt-lemma] rule [lengthBytes-geq-nonPos]: X <=Int lengthBytes ( _ ) => true requires X <=Int 0 [simplification, concrete(X)] rule [lengthBytes-concat]: lengthBytes(BUF1 +Bytes BUF2) => lengthBytes(BUF1) +Int lengthBytes(BUF2) [simplification] - rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification] - rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification] + rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification, preserves-definedness] + rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification, preserves-definedness] rule [lengthBytes-prtw]: lengthBytes(#padRightToWidth(W:Int, B:Bytes)) => maxInt(lengthBytes(B), W) [simplification] rule [lengthBytes-leq-zero]: lengthBytes(B:Bytes) <=Int 0 => B ==K .Bytes [simplification] 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 3a16df7834..f6789b90eb 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 @@ -101,6 +101,14 @@ module EVM-INT-SIMPLIFICATION requires 0 <=Int WB andBool 0 <=Int X andBool X X + requires #rangeUInt ( 256, X ) + [simplification, preserves-definedness] + // Reduction: bitwise right shift in terms of `#range` rule [asWord-shr]: #asWord( BA ) >>Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) ) From e849dee661334541b89982ae7abbc70529b89e82 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 15:06:32 +0000 Subject: [PATCH 04/19] =?UTF-8?q?lemmas/lemmas.k:=20Round=203=20=E2=80=94?= =?UTF-8?q?=20add=20widthOpCode-lb=20(0=20<=3DInt=20#widthOpCode(=5F)=20?= =?UTF-8?q?=3D>=20true)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 3dd3dfdf8b..6d85bfe99b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -241,6 +241,15 @@ module LEMMAS-HASKELL [symbolic] requires notBool ( I1 ==Int I2 ) [simplification] + // ######################## + // #widthOpCode range + // ######################## + + // #widthOpCode always returns ≥ 1 (PUSH ops 2..33, everything else 1). + // Without this, Booster cannot discharge 0 <=Int S when S = #widthOpCode(x) + // or 101 <=Int 101 +Int #widthOpCode(x) (after INT normalization). + rule [widthOpCode-lb]: 0 <=Int #widthOpCode(_:Int) => true [simplification] + // ######################## // Boolean Logic // ######################## From 3d39038ede6751e7c04c52e45dfb239d07e19925 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 15:06:51 +0000 Subject: [PATCH 05/19] =?UTF-8?q?lemmas:=20Round=204=20=E2=80=94=20widthOp?= =?UTF-8?q?Code=20concat=20rules,=20asWord-range-buf?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lemmas.k: add widthOpCode-concat-left/right composition rules. evm-int-simplification.k: add asWord-range-buf to match the actual #asWord(#range(#buf(N,X), S, W)) term structure after concat-lookup and lookup-as-asWord reductions. --- .../lemmas/evm-int-simplification.k | 11 +++++++++++ .../kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 16 ++++++++++++++-- 2 files changed, 25 insertions(+), 2 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 f6789b90eb..7c3c8e42e5 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 @@ -109,6 +109,17 @@ module EVM-INT-SIMPLIFICATION requires #rangeUInt ( 256, X ) [simplification, preserves-definedness] + // General reduction: #asWord of a range extracted from a buf. + // #buf(N, X) is the big-endian N-byte encoding of X. Taking W bytes + // starting at byte S gives (X >> (8*(N-S-W))) & (2^(8*W)-1). + // Activated with concrete N, S, W so Booster can evaluate the arithmetic. + rule [asWord-range-buf]: + #asWord ( #range ( #buf ( N:Int, X:Int ), S:Int, W:Int ) ) => + X /Int ( 2 ^Int ( 8 *Int ( N -Int S -Int W ) ) ) modInt ( 2 ^Int ( 8 *Int W ) ) + requires 0 <=Int S andBool 0 >Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) ) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 6d85bfe99b..95b85d05b1 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -246,10 +246,22 @@ module LEMMAS-HASKELL [symbolic] // ######################## // #widthOpCode always returns ≥ 1 (PUSH ops 2..33, everything else 1). - // Without this, Booster cannot discharge 0 <=Int S when S = #widthOpCode(x) - // or 101 <=Int 101 +Int #widthOpCode(x) (after INT normalization). + // Note: smt-lemma cannot be applied here because #widthOpCode has no smt-hook. rule [widthOpCode-lb]: 0 <=Int #widthOpCode(_:Int) => true [simplification] + // Booster's equation engine does not descend inside #widthOpCode(...) to + // apply bytes-concat-lookup-{left,right}. These rules compose the two + // steps so the full concrete-prefix lookup can be reduced in one go. + rule [widthOpCode-concat-left]: + #widthOpCode ( ( B1:Bytes +Bytes _B2:Bytes ) [ I:Int ] ) => #widthOpCode ( B1 [ I ] ) + requires 0 <=Int I andBool I #widthOpCode ( B2 [ I -Int lengthBytes ( B1 ) ] ) + requires lengthBytes ( B1 ) <=Int I + [simplification, preserves-definedness] + // ######################## // Boolean Logic // ######################## From 2bc3628f6a4e373104488f2139bcf09f9a773c54 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 23 May 2026 05:05:50 +0000 Subject: [PATCH 06/19] =?UTF-8?q?evm.md,=20lemmas.k,=20CLAUDE.md:=20Round?= =?UTF-8?q?=205=20=E2=80=94=20smtlib=20annotation=20for=20#widthOpCode,=20?= =?UTF-8?q?smt-lemma=20bounds?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add smtlib(widthOpCode) to the #widthOpCode syntax declaration so it is registered as a declared SMT function. This allows smt-lemma rules to encode bounds on #widthOpCode as universally-quantified axioms in the solver prelude, letting Z3 discharge side conditions that contain #widthOpCode without needing to evaluate it concretely. Add widthOpCode-lb and widthOpCode-ub with [smt-lemma] so the solver knows 0 ≤ #widthOpCode(X) ≤ 33 for all X. Also document the "save output to file before analysing" workflow in CLAUDE.md to avoid re-running slow commands with different pipes. Co-Authored-By: Claude Sonnet 4.6 --- CLAUDE.md | 95 +++++++++++++++++++ .../src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- .../kproj/evm-semantics/lemmas/lemmas.k | 9 +- 3 files changed, 102 insertions(+), 4 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 7e30554dea..ecb3489c31 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -178,6 +178,101 @@ To register a new spec, add one line to `KOMPILE_MAIN_FILE` in The glob `spec_files('functional', '*-spec.k')` picks it up automatically. `KOMPILE_MAIN_MODULE` defaults to `'VERIFICATION'`; only override it if your spec uses a different top module name. +## Diagnosing slow Haskell backend (`simplify` / `execute`) + +The booster server (`kore-rpc-booster`) reads the `KORE_RPC_OPTS` environment variable at startup and prepends its words to the CLI args. +Set it before any `kevm prove` invocation to inject diagnostic flags without changing Python code: + +```bash +KORE_RPC_OPTS="" uv --project kevm-pyk/ run kevm prove ... +``` + +Use `--log-file /tmp/booster.log` to write to a file; `--log-timestamps` adds wall-clock timestamps per line. + +For a full reference — log levels, source locations, and `contextLoggingEnabled` behaviour — see [`docs/kore-rpc-booster-logging.md`](docs/kore-rpc-booster-logging.md). +To test a local haskell-backend build, see [`docs/kup-override.md`](docs/kup-override.md). +To file a bug or performance report with the haskell-backend team, see [`docs/submitting-test-cases-to-haskell-backend.md`](docs/submitting-test-cases-to-haskell-backend.md). + +Key facts to keep in mind: + +- The **`simplify` endpoint always calls kore** after booster — unconditionally, not a fallback. + `-l Aborts` will not show this call; only a diff appears if kore actually changes something. +- **Kore has no LLVM**; it evaluates K functions via axiom rewriting only. + When booster has already fully evaluated a term via LLVM, kore's simplify pass is pure overhead. +- **`-l SimplifyKore` must be paired with a booster-side level** (e.g. `-l Timing`) to ensure `contextLoggingEnabled = True`; otherwise kore entries may not be emitted. + See `docs/kore-rpc-booster-logging.md` for the `contextLoggingEnabled` mechanism. +- **`-l Timing` is NOT a low-overhead flag for large terms.** + Any level with a `levelToContext` entry (including `Timing`) sets `contextLoggingEnabled = True`, + which enables ALL kore log entry types — including `DebugTerm`, which pretty-prints the full term at every step. + For terms with large concrete byte literals, this can add orders-of-magnitude overhead. + Use pyk's INFO timestamps (default in `bench-prove.py`) for true baseline measurements. +- **`booster-dev`** (`kevm prove --use-booster-dev`) runs pure booster with no kore proxy. + When the kore step is pure overhead for your proof, this is the right backend to use. + `bench-prove.py --booster-dev` benchmarks this mode and derives timing from pyk's INFO output + (since `booster-dev` does not read `KORE_RPC_OPTS`). + +### Quick log-level cheat sheet + +| Goal | Flags | Overhead | +|---|---|---| +| True per-request timing (pyk timestamps) | no `-l` flags | None | +| Booster/kore split per request | `-l Timing` | **Moderate — enables all kore log types; kore time 10× higher at large N** | +| Does kore change anything? | `-l Aborts` + grep `"Kore simplification: Diff"` | Moderate | +| Which booster rules fire / break? | `-l Simplify` (small N only) | 10–14× | +| What equations is kore attempting? | `-l SimplifyKore -l Timing` (small N) | High | +| Is SMT a bottleneck? | `-l SMT` | Low | +| Is LLVM being used? | grep `llvm` in log | None | + +### Interpreting `[failure][break]` vs `[failure][continue]` + +- `[failure][continue]` — rule did not match (pattern mismatch); booster moves to the next candidate. + Normal and fast. +- `[failure][break]` — rule matched but booster cannot confirm RHS is defined (non-total sub-symbols). + Booster stops trying to evaluate this term entirely. + This is the key signal that `[preserves-definedness]` or `total` annotations are needed. + +## Testing a local Haskell backend build + +Use `kup` to install K with a local haskell-backend checkout substituted for the upstream one. +This lets you test backend changes against full kevm proofs without modifying the project's Nix flake. + +```bash +# Check the current input tree (shows which haskell-backend hash is pinned): +kup list k.openssl.procps --inputs + +# Install the same K version with a local haskell-backend override: +kup install k.openssl.procps \ + --version v7.1.323 \ + --override haskell-backend ~/src/haskell-backend + +# Revert to the upstream backend: +kup install k.openssl.procps --version v7.1.323 +``` + +After installing, the kdist cache is stale — rebuild before running proofs: + +```bash +uv --project kevm-pyk/ run kevm-kdist build evm-semantics.haskell +``` + +For full details on how `--override` works and what kup does internally, see [`docs/kup-override.md`](docs/kup-override.md). + +## Running long commands + +**Always save output to a file first, then analyse the file.** +Never re-run a slow command with a different pipe to see a different slice of its output — that wastes minutes and loses the rest of the output. + +```bash +# correct pattern for any slow command: +python scripts/bench-prove.py tests/specs/functional/my-spec.k --analyse-fallbacks \ + > /tmp/bench-out.log 2>&1 +# then inspect: +grep "changed\|Total" /tmp/bench-out.log +tail -n 40 /tmp/bench-out.log +``` + +This applies to: `bench-prove.py`, `kevm prove`, `kevm-kdist build`, pytest runs, any Haskell backend invocation. + ## Commit discipline - Every commit must be **atomic and self-contained** — the project must build and fast tests must pass at each commit. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index bb90886791..9d6f89933b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1812,7 +1812,7 @@ System Transaction Configuration ``` ```k - syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function, total] + syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function, total, smtlib(widthOpCode)] // ----------------------------------------------------------------- rule #widthOpCode(W) => W -Int 94 requires W >=Int 96 andBool W <=Int 127 rule #widthOpCode(_) => 1 [owise] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 95b85d05b1..17af8ccea7 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -245,9 +245,12 @@ module LEMMAS-HASKELL [symbolic] // #widthOpCode range // ######################## - // #widthOpCode always returns ≥ 1 (PUSH ops 2..33, everything else 1). - // Note: smt-lemma cannot be applied here because #widthOpCode has no smt-hook. - rule [widthOpCode-lb]: 0 <=Int #widthOpCode(_:Int) => true [simplification] + // #widthOpCode always returns 1..33 (PUSH ops 2..33, everything else 1). + // smtlib(widthOpCode) on the declaration lets smt-lemma encode these as + // universally-quantified bounds so the solver can discharge side conditions + // containing #widthOpCode without needing to evaluate it concretely. + rule [widthOpCode-lb]: 0 <=Int #widthOpCode(_:Int) => true [simplification, smt-lemma] + rule [widthOpCode-ub]: #widthOpCode(_:Int) <=Int 33 => true [simplification, smt-lemma] // Booster's equation engine does not descend inside #widthOpCode(...) to // apply bytes-concat-lookup-{left,right}. These rules compose the two From 8e72989ee13adfc59dde5ebb943c210e387e3d57 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 23 May 2026 05:17:37 +0000 Subject: [PATCH 07/19] compute-valid-jump-dests-spec.k: add fast N=5 claim alongside perf N=1000 claim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit compute-valid-jump-dests-fast (N=5): quick smoke test for iterating on simplification lemmas — completes in under a second. compute-valid-jump-dests-perf (N=1000): performance regression benchmark; run without --haskell-logging for accurate baseline timing. Co-Authored-By: Claude Sonnet 4.6 --- .../functional/compute-valid-jump-dests-spec.k | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/tests/specs/functional/compute-valid-jump-dests-spec.k b/tests/specs/functional/compute-valid-jump-dests-spec.k index a415944537..61d055c96a 100644 --- a/tests/specs/functional/compute-valid-jump-dests-spec.k +++ b/tests/specs/functional/compute-valid-jump-dests-spec.k @@ -18,10 +18,17 @@ endmodule module COMPUTE-VALID-JUMP-DESTS-SPEC imports VERIFICATION - // Performance benchmark: concrete prefix, one JUMPDEST, concrete suffix, then 32 symbolic - // bytes. The #buf(32, INT_VAR) tail forces Haskell-backend symbolic evaluation rather - // than pure LLVM concrete evaluation, exposing the O(N) overhead of re-evaluating - // lengthBytes(PGM) on every loop iteration with the old definition. + // Fast smoke test: small concrete prefix + one JUMPDEST + small concrete suffix + + // 32 symbolic bytes. Use this for quick iteration during development. + claim [compute-valid-jump-dests-fast]: + runLemma(#computeValidJumpDests(padRightBytes(.Bytes, 5, 0) +Bytes (91 : .Bytes) +Bytes padRightBytes(.Bytes, 5, 0) +Bytes #buf(32, INT_VAR))) + => doneLemma(?_:Bytes) + ... + requires #rangeUInt(256, INT_VAR) + + // Performance benchmark: large concrete prefix exposes O(N) overhead in any + // per-iteration re-evaluation of lengthBytes(PGM). Run without --haskell-logging + // for true baseline timing. claim [compute-valid-jump-dests-perf]: runLemma(#computeValidJumpDests(padRightBytes(.Bytes, 1000, 0) +Bytes (91 : .Bytes) +Bytes padRightBytes(.Bytes, 1000, 0) +Bytes #buf(32, INT_VAR))) => doneLemma(?_:Bytes) From 140cdc809ce1f827c12a1b8917b190484b087051 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 07:50:14 +0000 Subject: [PATCH 08/19] lemmas/int-simplification.k: add minInt/maxInt comparison simplification rules Fixes `int-simplifications-spec` regression under `--booster-only-simplify`. The four new `minint-lt-maxint-*` / `minint-leq-maxint-*` rules at priority 40 make Booster produce `true` directly for claims like: minInt(A, _B) --- .../evm-semantics/lemmas/int-simplification.k | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) 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 30e5663c47..70d67a1a8f 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 @@ -232,6 +232,35 @@ module INT-SIMPLIFICATION-COMMON rule [maxInt-factor-left]: maxInt ( A:Int +Int B:Int, A:Int +Int C:Int ) => A +Int maxInt ( B, C ) [simplification] rule [maxInt-factor-right]: maxInt ( A:Int +Int B:Int, C:Int +Int B:Int ) => maxInt ( A, C ) +Int B [simplification] + // minInt true + requires A true + requires A true + requires B <=Int D + [simplification(40), preserves-definedness] + rule [minint-leq-maxint-shift-b]: + minInt(_A:Int +Int E:Int, B:Int +Int E:Int) <=Int maxInt(_C:Int +Int F:Int, D:Int +Int F:Int) => true + requires B <=Int D andBool E <=Int F + [simplification(40), preserves-definedness] + // Factored forms: after minInt-factor-{left,right} + maxInt-factor-{left,right} (priority 50) have fired, + // the non-linear shift rules above no longer match; these linear rules catch the result. + rule [minint-lt-maxint-shift-a-factored]: + E:Int +Int minInt(A:Int, _B:Int) true + requires A true + requires B <=Int D andBool E <=Int F + [simplification(40), preserves-definedness] + // ########################################################################### // inequality // ########################################################################### From 90dd3b28263fa8a9248e0969b910192a2683b683 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 15:07:57 +0000 Subject: [PATCH 09/19] lemmas/evm-int-simplification.k: add bit-mask-asWord-m and bit-notmask-asWord-nm Parametric masking of #asWord(BA:Bytes) with byte-aligned maxUIntN / notMaxUIntN masks; fires at priority 40 (before multimask-b-and at 50). --- .../lemmas/evm-int-simplification.k | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) 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 7c3c8e42e5..f7dbcd6f87 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 @@ -156,6 +156,30 @@ module EVM-INT-SIMPLIFICATION andBool lengthBytes ( BA1 +Bytes BA2 ) <=Int 32 [simplification, concrete(BA2, X), preserves-definedness] + // Masking `#asWord(BA)` with a byte-aligned maxUIntN mask (= 2^N-1) gives + // the lower N/8 bytes as a new `#asWord`. Fires before `multimask-b-and` + // (priority 50) to avoid an intermediate form that Booster cannot close. + rule [bit-mask-asWord-m]: + MASK:Int &Int #asWord(BA:Bytes) => + #asWord(#range(BA, 32 -Int (log2Int(MASK +Int 1) /Int 8), log2Int(MASK +Int 1) /Int 8)) + requires 0 + #asWord(#range(BA, 0, 32 -Int (log2Int(pow256 -Int MASK) /Int 8)) +Bytes #buf(log2Int(pow256 -Int MASK) /Int 8, 0)) + requires 0 <=Int MASK + andBool MASK Date: Sun, 24 May 2026 14:31:53 +0000 Subject: [PATCH 10/19] lemmas/int-simplification.k: normalize ==Int commutativity concrete-on-left MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Kore's execute-fallback applies INT-KORE.eq-int-true-rigth which can swap ==Int argument order in path conditions (e.g. lengthBytes(BA) ==Int 32 → 32 ==Int lengthBytes(BA)). This makes Booster's implies check fail due to a syntactic mismatch even when the logical content is identical. The new rule [int-eq-comm-concrete] at priority 30 fires before the +Int cancellation rules and normalises concrete-on-left to concrete-on-right, restoring the form the target spec expects. Co-Authored-By: Claude Sonnet 4.6 --- .../kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k | 4 ++++ 1 file changed, 4 insertions(+) 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 70d67a1a8f..c8ab6f4ac6 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 @@ -86,6 +86,10 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] rule A +Int B >Int C +Int D => A -Int C >Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] rule A +Int B >=Int C +Int D => A -Int C >=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] + rule [int-eq-comm-concrete]: + N:Int ==Int X:Int => X ==Int N + [simplification(30), concrete(N), symbolic(X)] + rule A +Int B ==Int A => B ==Int 0 [simplification(40)] rule A +Int B ==Int B => A ==Int 0 [simplification(40)] rule A +Int B ==Int C +Int B => A ==Int C [simplification(40)] From c59dfaa774f401308b5caa24b70378020f1cbd61 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 17:41:44 +0000 Subject: [PATCH 11/19] lemmas/{int-simplification,lemmas}.k: add arithmetic + Bool simplification lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds to INT-SIMPLIFICATION-COMMON: - A <=Int A => true (reflexivity; fixes chop-overflow-02 under --booster-only-simplify) - A <=Int A +Int B => 0 <=Int B - A +Int ((B -Int A) +Int C) => B +Int C (4-term cancellation; fixes cancellation-02) - A false (strict order contradiction; fixes b2w-03) Adds to INT-SIMPLIFICATION-HASKELL: - A false requires B <=Int C [concrete(B,C)] (range contradiction) - C <=Int A andBool A false requires B <=Int C [concrete(B,C)] (range contradiction) (requires is purely concrete, evaluated by LLVM hook — no circular self-application risk) Adds to LEMMAS-HASKELL: - B orBool notBool B => true (and commuted variant; fixes b2w-05, chop-additional-knowledge) - B andBool notBool B => false (and commuted variant) Validation: full functional test suite passes in normal mode (slot-updates-spec.k failure is pre-existing, unrelated to these changes). Under --booster-only-simplify, lemmas-spec.k drops from 22 to 18 failing claims. No loops detected (checked via kevm-analyse hot-rules). Co-Authored-By: Claude Sonnet 4.6 --- .../kproj/evm-semantics/lemmas/int-simplification.k | 12 ++++++++++++ .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 5 +++++ 2 files changed, 17 insertions(+) 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 c8ab6f4ac6..c99d4c5eef 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 @@ -105,6 +105,11 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] rule A -Int B A A <=Int B [simplification, symbolic(A, B)] + // Mixed range contradictions: A < B /\ C <= A where B <= C (all concrete B, C) + // Requires is purely concrete (both B and C are concrete), so no circular self-application. + rule A:Int false requires B <=Int C [simplification, concrete(B, C)] + rule C:Int <=Int A:Int andBool A:Int false requires B <=Int C [simplification, concrete(B, C)] + endmodule module INT-SIMPLIFICATION-COMMON @@ -137,6 +142,7 @@ module INT-SIMPLIFICATION-COMMON rule (A +Int B) +Int (C -Int B) => A +Int C [simplification] rule (A -Int B) -Int (C -Int B) => A -Int C [simplification] rule ((A -Int B) -Int C) +Int B => A -Int C [simplification] + rule A +Int ((B -Int A) +Int C) => B +Int C [simplification] // 5 terms // NOTE: required for `tests/specs/functional/infinite-gas-spec.k.prove` (haskell) @@ -274,6 +280,12 @@ module INT-SIMPLIFICATION-COMMON rule A false requires 0 <=Int B [simplification] + rule A:Int <=Int A:Int => true [simplification] + + rule A:Int <=Int A:Int +Int B:Int => 0 <=Int B [simplification] + + rule A:Int false [simplification] + rule 0 true requires 0 <=Int A [simplification, preserves-definedness] // inequality sign normalization diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 17af8ccea7..bf38ea0255 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -279,4 +279,9 @@ module LEMMAS-HASKELL [symbolic] rule [notBool-or]: notBool ( A orBool B ) => ( notBool A ) andBool ( notBool B ) [simplification(60)] rule [notBool-and]: notBool ( A andBool B ) => ( notBool A ) orBool ( notBool B ) [simplification(60)] + rule [bool-or-not-self]: B:Bool orBool notBool B:Bool => true [simplification] + rule [bool-not-or-self]: notBool B:Bool orBool B:Bool => true [simplification] + rule [bool-and-not-self]: B:Bool andBool notBool B:Bool => false [simplification] + rule [bool-not-and-self]: notBool B:Bool andBool B:Bool => false [simplification] + endmodule From ecafb048053214a06494784305ec9d0e3480a368 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 19:57:58 +0000 Subject: [PATCH 12/19] lemmas/int-simplification.k, lemmas/lemmas.k: fix two booster-only failing claims Add a higher-priority (40) variant of `A <=Int A+B => 0 <=Int B` that short-circuits directly to `true` when `0 <=Int B` is already in the path condition, fixing `chop-overflow-01` in --booster-only-simplify mode where the intermediate `0 <=Int Y` form cannot be discharged at the implies check. Add `map-update-comm` to `LEMMAS-HASKELL`: normalises `M[I1<-V1][I2<-V2]` to `M[I2<-V2][I1<-V1]` when `I2 --- .../kproj/evm-semantics/lemmas/int-simplification.k | 2 ++ kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 6 ++++++ 2 files changed, 8 insertions(+) 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 c99d4c5eef..08064b04ec 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 @@ -282,6 +282,8 @@ module INT-SIMPLIFICATION-COMMON rule A:Int <=Int A:Int => true [simplification] + // Higher-priority: short-circuit to true directly when path condition already has 0 <=Int B. + rule A:Int <=Int A:Int +Int B:Int => true requires 0 <=Int B [simplification(40)] rule A:Int <=Int A:Int +Int B:Int => 0 <=Int B [simplification] rule A:Int false [simplification] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index bf38ea0255..c39e0a4d53 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -241,6 +241,12 @@ module LEMMAS-HASKELL [symbolic] requires notBool ( I1 ==Int I2 ) [simplification] + // Normalize map-update order: swap when outer key < inner key, so outermost key is always larger (stable canonical form). + rule [map-update-comm]: + M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] => M [ I2 <- V2 ] [ I1 <- V1 ] + requires I2 Date: Mon, 25 May 2026 00:34:15 +0000 Subject: [PATCH 13/19] lemmas/bytes-simplification.k: add concrete b"" concat identity rules In K, .Bytes (the constructor) and b"" (LLVM-evaluated concrete empty bytes, a Kore domain value \dv{SortBytes}("")) are different Kore terms. The existing bytes-concat-empty-right/left rules use .Bytes and do not fire when LLVM hooks (e.g. #encodeArgs base case) return b"". New rules: [bytes-concat-empty-right-concrete]: B +Bytes b"" => B [bytes-concat-empty-left-concrete]: b"" +Bytes B => B Fixes booster-only failure for encodepacked-keccak01: the contract evaluates keccak(1 : #encodeArgs(#uint256(A0))) where the #encodeArgs base case produces b"", leaving keccak(X +Bytes b"") vs keccak(X) as the implies-check mismatch. Co-Authored-By: Claude Sonnet 4.6 --- .../kproj/evm-semantics/lemmas/bytes-simplification.k | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index b99732cb2d..571f024104 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -29,6 +29,10 @@ module BYTES-SIMPLIFICATION [symbolic] rule [bytes-concat-empty-right]: B:Bytes +Bytes .Bytes => B [simplification] rule [bytes-concat-empty-left]: .Bytes +Bytes B:Bytes => B [simplification] + // b"" is a Kore domain value (\dv{Bytes}("")) distinct from the .Bytes constructor; + // LLVM hooks (e.g. #encodeArgs base case) return b"", not .Bytes, so we need both forms. + rule [bytes-concat-empty-right-concrete]: B:Bytes +Bytes b"" => B [simplification, preserves-definedness] + rule [bytes-concat-empty-left-concrete]: b"" +Bytes B:Bytes => B [simplification, preserves-definedness] rule [bytes-concat-right-assoc-symb-l]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B1), simplification(40)] rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)] From 8c3de920c3f3eb37a0879696508b8257800c22f8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 04:11:13 +0000 Subject: [PATCH 14/19] tests/specs/functional/set-dedup-spec.k, test_prove.py: add set-dedup functional spec Adds a runLemma/doneLemma spec that tests Set deduplication lemmas (SetItem membership and |Set deduplication) in isolation. Registers the spec in the KOMPILE_MAIN_FILE table so the pytest harness picks it up automatically. Co-Authored-By: Claude Sonnet 4.6 --- kevm-pyk/src/tests/integration/test_prove.py | 1 + tests/specs/functional/set-dedup-spec.k | 48 ++++++++++++++++++++ 2 files changed, 49 insertions(+) create mode 100644 tests/specs/functional/set-dedup-spec.k diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index ca641ac638..82f2e4c818 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -114,6 +114,7 @@ def exclude_list(exclude_file: Path) -> list[Path]: 'functional/slot-updates-spec.k': 'slot-updates-spec.k', 'functional/storageRoot-spec.k': 'storageRoot-spec.k', 'functional/compute-valid-jump-dests-spec.k': 'compute-valid-jump-dests-spec.k', + 'functional/set-dedup-spec.k': 'set-dedup-spec.k', 'mcd/functional-spec.k': 'functional-spec.k', 'mcd-structured/functional-spec.k': 'functional-spec.k', } diff --git a/tests/specs/functional/set-dedup-spec.k b/tests/specs/functional/set-dedup-spec.k new file mode 100644 index 0000000000..d33b84ea18 --- /dev/null +++ b/tests/specs/functional/set-dedup-spec.k @@ -0,0 +1,48 @@ +requires "evm.md" +requires "lemmas/lemmas.k" + +module VERIFICATION + imports LEMMAS + imports EVM + + syntax StepSort ::= Int | Bool | Set + // ------------------------------------- + + syntax KItem ::= runLemma ( StepSort ) [symbol(runLemma)] + | doneLemma( StepSort ) + // -------------------------------------- + rule runLemma( T ) => doneLemma( T ) ... + +endmodule + +module SET-DEDUP-SPEC + imports VERIFICATION + + // Set deduplication via |Set and membership + // ------------------------------------------ + // These claims test the rule: + // rule S:Set |Set SetItem(X:Int) => S requires X in S [simplification] + // together with the supporting membership rules that let the `X in S` side + // condition discharge when S is written in |Set form. + + // Basic: one duplicate concrete element + claim [set-dedup-01]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(1) ) + => doneLemma ( A:Set |Set SetItem(1) ) ... + + // Two distinct elements, one of which is duplicated + claim [set-dedup-02]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(1) ) + => doneLemma ( A:Set |Set SetItem(1) |Set SetItem(2) ) ... + + // Both elements are duplicated + claim [set-dedup-03]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(1) |Set SetItem(2) ) + => doneLemma ( A:Set |Set SetItem(1) |Set SetItem(2) ) ... + + // Duplicate appears after other elements (tests deeper membership check) + claim [set-dedup-04]: + runLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(3) |Set SetItem(1) ) + => doneLemma ( A:Set |Set SetItem(1) |Set SetItem(2) |Set SetItem(3) ) ... + +endmodule From d9cc35a721c213e8911a3071ed640c41ade19113 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 15:08:09 +0000 Subject: [PATCH 15/19] lemmas/lemmas.k: add KSet match limitation comments for permanently-dead booster rules --- .../kproj/evm-semantics/lemmas/lemmas.k | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index c39e0a4d53..792f07f9fa 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -36,12 +36,29 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Set Reasoning // ######################## + // Membership in the concat (_Set_) form — fires in both kore and booster. rule X in (SetItem(Y) _ ) => true requires X ==Int Y [simplification] rule X in (SetItem(Y) REST) => X in REST requires notBool ( X ==Int Y ) [simplification] + // NOTE: the two non-linear rules below fire in kore but are INDETERMINATE in booster. + // Booster internalises SetItem(X) as KSet{def,[X],None}; matchSets() returns addIndeterminate + // for any non-empty KSet (Match.hs:673-676). Backend change required to fix. rule ( S:Set |Set SetItem ( X ) ) |Set SetItem( X ) => ( S:Set |Set SetItem ( X ) ) [simplification] rule ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) |Set SetItem( X ) => ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) [simplification] + // Membership in the |Set (union) form — fires in kore only (same matchSets limitation). + // Kore uses these to discharge the requires-clause of the dedup rule below. + rule X:Int in (REST:Set |Set SetItem(Y:Int)) => true requires X ==Int Y [simplification] + rule X:Int in (REST:Set |Set SetItem(Y:Int)) => X in REST requires notBool ( X ==Int Y ) [simplification] + + // Deduplication of repeated concrete Int elements in a symbolic |Set expression. + // Required in normal mode (where kore's simplify step fires it) but INDETERMINATE in booster. + // Booster cannot match SetItem(X) in the pattern: matchSets() is unimplemented for non-empty + // KSets (booster/Match.hs:673-676). Cannot be fixed from K source; requires backend change. + // Context: #touchAccounts in evm.md adds addresses via |Set; when the same address is added + // twice to a symbolic touchedAccounts, this rule is needed to normalize back to a 2-element form. + rule S:Set |Set SetItem(X:Int) => S requires X in S [simplification] + // ######################## // Word Reasoning // ######################## From a087d2a1d02814fb190c3517ec20bfae3503ed9c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 18:49:23 +0000 Subject: [PATCH 16/19] CLAUDE.md: drop misplaced Group D sections; fix stale bench-prove.py refs Remove '## Running long commands' (belongs in the backend-docs PR). Fix two bullet points in '## Diagnosing slow Haskell backend' that referenced the now-deleted bench-prove.py script. Keep '## Testing a local Haskell backend build' and its kdist cache rebuild instruction. Co-Authored-By: Claude Sonnet 4.6 --- CLAUDE.md | 20 +------------------- 1 file changed, 1 insertion(+), 19 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index ecb3489c31..19f62e5175 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -205,11 +205,9 @@ Key facts to keep in mind: Any level with a `levelToContext` entry (including `Timing`) sets `contextLoggingEnabled = True`, which enables ALL kore log entry types — including `DebugTerm`, which pretty-prints the full term at every step. For terms with large concrete byte literals, this can add orders-of-magnitude overhead. - Use pyk's INFO timestamps (default in `bench-prove.py`) for true baseline measurements. + Use pyk's INFO timestamps (no `-l` flags) for true baseline measurements. - **`booster-dev`** (`kevm prove --use-booster-dev`) runs pure booster with no kore proxy. When the kore step is pure overhead for your proof, this is the right backend to use. - `bench-prove.py --booster-dev` benchmarks this mode and derives timing from pyk's INFO output - (since `booster-dev` does not read `KORE_RPC_OPTS`). ### Quick log-level cheat sheet @@ -257,22 +255,6 @@ uv --project kevm-pyk/ run kevm-kdist build evm-semantics.haskell For full details on how `--override` works and what kup does internally, see [`docs/kup-override.md`](docs/kup-override.md). -## Running long commands - -**Always save output to a file first, then analyse the file.** -Never re-run a slow command with a different pipe to see a different slice of its output — that wastes minutes and loses the rest of the output. - -```bash -# correct pattern for any slow command: -python scripts/bench-prove.py tests/specs/functional/my-spec.k --analyse-fallbacks \ - > /tmp/bench-out.log 2>&1 -# then inspect: -grep "changed\|Total" /tmp/bench-out.log -tail -n 40 /tmp/bench-out.log -``` - -This applies to: `bench-prove.py`, `kevm prove`, `kevm-kdist build`, pytest runs, any Haskell backend invocation. - ## Commit discipline - Every commit must be **atomic and self-contained** — the project must build and fast tests must pass at each commit. From dac2ce688f4846daa76b4e7bf3f36d94a9fd6372 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 19:12:55 +0000 Subject: [PATCH 17/19] CLAUDE.md: document pyproject.toml local-pyk pointer and uv sync workflow In '## Testing a local Haskell backend build': add the pyproject.toml snippet for pointing at a local pyk checkout, and the uv sync / revert steps that go with it. Add '## Updating local pyk vs local K': explains that a pyk-only change only needs uv sync --reinstall-package kframework (no kdist rebuild), while a K/Haskell backend change requires the full kup + kevm-kdist flow. Co-Authored-By: Claude Sonnet 4.6 --- CLAUDE.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/CLAUDE.md b/CLAUDE.md index 19f62e5175..40c62d4889 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -253,8 +253,29 @@ After installing, the kdist cache is stale — rebuild before running proofs: uv --project kevm-pyk/ run kevm-kdist build evm-semantics.haskell ``` +When installing K from a local source checkout, also update `pyproject.toml` to point at the matching local pyk: + +```toml +# kevm-pyk/pyproject.toml +"kframework @ file:///home/dev/src/k-testing/pyk", +``` + +Then run `uv --project kevm-pyk/ sync` to install the local pyk. +Revert by restoring `"kframework=="` and re-syncing. + For full details on how `--override` works and what kup does internally, see [`docs/kup-override.md`](docs/kup-override.md). +## Updating local pyk vs local K + +When `kevm-pyk/pyproject.toml` points at `kframework @ file:///home/dev/src/k-testing/pyk`: + +- **pyk-only change** (Python code in `~/src/k-testing/pyk`): resync pyk only — no rebuild needed. + ```bash + uv --project kevm-pyk/ sync --reinstall-package kframework + ``` +- **K/Haskell backend change** (C++/Haskell in `~/src/k-testing` or `~/src/haskell-backend`): + run the full `kup install` + `kevm-kdist build` flow (see "Testing a local Haskell backend build"). + ## Commit discipline - Every commit must be **atomic and self-contained** — the project must build and fast tests must pass at each commit. From db711c447b6f8078c9aa5450574d37ea3a767af8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 22:49:47 +0000 Subject: [PATCH 18/19] =?UTF-8?q?lemmas/lemmas.k:=20drop=20map-update-comm?= =?UTF-8?q?=20=E2=80=94=20breaks=20DSS=20implies=20checks?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit map-update-comm canonicalised M[k1<-v1][k2<-v2] to M[k2<-v2][k1<-v1] when k2 < k1, which is loop-safe but changes the syntactic form of storage terms mid-proof. VAT specs (heal.pass, fold.pass.rough, frob-diff-zero-dart.pass.rough) specify their RHS storage in a fixed key order; after map-update-comm fires the produced term no longer matches, causing the implies check to fail. The two booster-only claims it fixed (map-update-commutativity) require a different approach that does not alter the canonical form of arbitrary map updates. Co-Authored-By: Claude Sonnet 4.6 --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 6 ------ 1 file changed, 6 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 792f07f9fa..49994bc85e 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -258,12 +258,6 @@ module LEMMAS-HASKELL [symbolic] requires notBool ( I1 ==Int I2 ) [simplification] - // Normalize map-update order: swap when outer key < inner key, so outermost key is always larger (stable canonical form). - rule [map-update-comm]: - M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] => M [ I2 <- V2 ] [ I1 <- V1 ] - requires I2 Date: Tue, 26 May 2026 04:34:56 +0000 Subject: [PATCH 19/19] tests/specs/mcd/verification.k: add [smt-lemma] to keccak inequality rule MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The new Bool/Set/widthOpCode lemmas in lemmas.k cause the path-condition constraints `#Not({7 #Equals keccak(slot5)})` to be simplified away between nodes 1 and 3 of the KCFG. Without those constraints in node 4, the node4→node2 implies check cannot prove `7 ≠ keccak(slot5)` using simplification rules alone, so the three DSS specs fail: VAT-HEAL-PASS-SPEC, VAT-FOLD-PASS-ROUGH-SPEC, VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC Adding `[smt-lemma]` to the existing `keccak(_) ==Int I => false` rule encodes the fact `keccak(_) ≠ I` (for small I) as an SMT axiom. The implies check can then discharge the goal via Z3 even when the explicit path constraint is absent. Verified locally: all three specs PASS. Co-Authored-By: Claude Sonnet 4.6 --- tests/specs/mcd/verification.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k index cf400bac8b..2bcc3e0045 100644 --- a/tests/specs/mcd/verification.k +++ b/tests/specs/mcd/verification.k @@ -139,7 +139,7 @@ module LEMMAS-MCD [symbolic] // Keccak // ######################## - rule keccak(_) ==Int I => false requires #rangeSmall(I) [simplification] + rule keccak(_) ==Int I => false requires #rangeSmall(I) [simplification, smt-lemma] rule keccak(_) +Int I1 ==Int I2 => false requires #rangeSmall(I1) andBool #rangeSmall(I2) [simplification]