lemmas: booster-only gap fixes — widthOpCode, int/bytes simplifications, preserves-definedness

CLAUDE.md

@@ -178,6 +178,104 @@ 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="<flags>" 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 (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.
+
+### 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
+```
+
+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==<version>"` 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.

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 <Int LEN andBool PGM [ I ] ==Int 91
-    rule #computeValidJumpDests(PGM, I, RESULT, LEN) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT,          LEN) requires I <Int LEN andBool notBool PGM [ I ] ==Int 91
+    rule #computeValidJumpDests(PGM)                 => #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 <Int LEN andBool PGM [ I ] ==Int 91                                      [preserves-definedness]
+    rule #computeValidJumpDests(PGM, I, RESULT, LEN) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT,          LEN) requires I <Int LEN andBool notBool PGM [ I ] ==Int 91                              [preserves-definedness]
 ```
 
 System Calls
@@ -1812,7 +1812,7 @@ System Transaction Configuration
 ```
 
 ```k
-    syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function]
+    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]

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)]
@@ -267,8 +271,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]
@@ -306,5 +310,5 @@ module BYTES-SIMPLIFICATION [symbolic]
     rule [lookup-as-asWord]:
       B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) )
       requires 0 <=Int I andBool I <Int lengthBytes(B)
-      [simplification(60)]
+      [simplification(60), preserves-definedness]
 endmodule

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k

@@ -101,6 +101,25 @@ module EVM-INT-SIMPLIFICATION
     requires 0 <=Int WB andBool 0 <=Int X andBool X <Int minInt ( 2 ^Int (8 *Int WB), pow256 )
     [simplification, concrete(WB), preserves-definedness]
 
+  // Specialisation for 32-byte buf with rangeUInt(256) side-condition: avoids
+  // the minInt(2^256, pow256) evaluation that Booster cannot match against the
+  // path condition's 2^Int 256 tree form.
+  rule [asWord-buf-inversion-rangeUInt256]:
+    #asWord ( #buf ( 32, X:Int ) ) => X
+    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 W andBool S +Int W <=Int N
+     andBool 0 <=Int X andBool X <Int 2 ^Int ( 8 *Int N )
+    [simplification, concrete(N, S, W), 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 ) ) )
@@ -137,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 <Int MASK
+     andBool MASK +Int 1 ==Int 2 ^Int log2Int(MASK +Int 1)
+     andBool log2Int(MASK +Int 1) modInt 8 ==Int 0
+     andBool lengthBytes(BA) ==Int 32
+    [simplification(40), concrete(MASK), preserves-definedness]
+
+  // Masking `#asWord(BA)` with a byte-aligned notMaxUIntN mask (complement of
+  // 2^N-1 within 256 bits) zeroes the lower N/8 bytes and keeps the rest.
+  rule [bit-notmask-asWord-nm]:
+    MASK:Int &Int #asWord(BA:Bytes) =>
+      #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 <Int pow256
+     andBool pow256 -Int MASK ==Int 2 ^Int log2Int(pow256 -Int MASK)
+     andBool log2Int(pow256 -Int MASK) modInt 8 ==Int 0
+     andBool lengthBytes(BA) ==Int 32
+    [simplification(40), concrete(MASK), preserves-definedness]
+
   // ###########################################################################
   // chop
   // ###########################################################################

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)]
@@ -101,6 +105,11 @@ module INT-SIMPLIFICATION-HASKELL [symbolic]
     rule A -Int B  <Int 0 => A  <Int B [simplification, symbolic(A, B)]
     rule A -Int B <=Int 0 => 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  <Int B:Int andBool C:Int <=Int A:Int => false requires B <=Int C [simplification, concrete(B, C)]
+    rule C:Int <=Int A:Int andBool A:Int  <Int B:Int => false requires B <=Int C [simplification, concrete(B, C)]
+
 endmodule
 
 module INT-SIMPLIFICATION-COMMON
@@ -133,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)
@@ -232,6 +242,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 <Int maxInt / minInt <=Int maxInt: priority 40 fires before the default-priority (50) expansion rules,
+    // so Booster sees `true` directly rather than a disjunction requiring path-condition reasoning.
+    rule [minint-lt-maxint-a]:
+        minInt(A:Int, _B:Int) <Int maxInt(C:Int, _D:Int) => true
+        requires A <Int C
+        [simplification(40), preserves-definedness]
+    rule [minint-lt-maxint-shift-a]:
+        minInt(E:Int +Int A:Int, E:Int +Int _B:Int) <Int maxInt(F:Int +Int C:Int, F:Int +Int _D:Int) => true
+        requires A <Int C andBool E <=Int F
+        [simplification(40), preserves-definedness]
+    rule [minint-leq-maxint-b]:
+        minInt(_A:Int, B:Int) <=Int maxInt(_C:Int, D:Int) => 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) <Int F:Int +Int maxInt(C:Int, _D:Int) => true
+        requires A <Int C andBool E <=Int F
+        [simplification(40), preserves-definedness]
+    rule [minint-leq-maxint-shift-b-factored]:
+        minInt(_A:Int, B:Int) +Int E:Int <=Int maxInt(_C:Int, D:Int) +Int F:Int => true
+        requires B <=Int D andBool E <=Int F
+        [simplification(40), preserves-definedness]
+
   // ###########################################################################
   // inequality
   // ###########################################################################
@@ -241,6 +280,14 @@ module INT-SIMPLIFICATION-COMMON
 
     rule A <Int A -Int B => false requires 0 <=Int B [simplification]
 
+    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 <Int B:Int andBool B:Int <Int A:Int => false [simplification]
+
     rule 0 <Int 1 <<Int A => true requires 0 <=Int A [simplification, preserves-definedness]
 
     // inequality sign normalization