Simplification lemmas to improve Haskell booster coverage (#2859)

* lemmas/bytes-simplification.k: add preserves-definedness to lookup-as-asWord

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 <noreply@anthropic.com>
(cherry picked from commit 25e00d935ac1f9ce25394e40865dbb36c0cbd80b)
(cherry picked from commit 6ae0def0a1de63aa5ffb13d1cdb2abe7d5c3651d)

* 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.

(cherry picked from commit d4dad3335e7e98d76057c9c0b07387a21a20c0b2)
(cherry picked from commit c60634bc589f05a98aa30b06409df4ed478d407f)

* lemmas/int-simplification.k: normalize ==Int commutativity concrete-on-left

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 <noreply@anthropic.com>
(cherry picked from commit 1d384970bda6669b479959a31f152c0e8aedde35)
(cherry picked from commit 2cf8e8c620fee897758f02f5b2b512595428fbec)

* lemmas/{int-simplification,lemmas}.k: add arithmetic + Bool simplification lemmas

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 <Int B andBool B <Int A => false  (strict order contradiction; fixes b2w-03)

Adds to INT-SIMPLIFICATION-HASKELL:
- A <Int B andBool C <=Int A => false requires B <=Int C [concrete(B,C)]  (range contradiction)
- C <=Int A andBool A <Int B => 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 <noreply@anthropic.com>
(cherry picked from commit 3bb01297db74cacf75fa138f0550440882df8de1)
(cherry picked from commit 4c13678fdb82d593bfc495cf0418804a3e505c90)

* lemmas/int-simplification.k: short-circuit A <=Int A+Int B to true when 0 <=Int B

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.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
(cherry picked from commit bfb0225f96a28cbf42ddd520dd49773b234944e5)

* 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 <noreply@anthropic.com>
(cherry picked from commit 829d293906d6efb769649002b2cea2ebf90235fc)
(cherry picked from commit a4669b0942edb8c974750490affdad4e1ed1d54d)

* buf.md, abi-spec.k: add [preserves-definedness] to 2^(8*SIZE) simplification, add coverage claim

The rule `2 ^Int (8 *Int SIZE) => #powByteLen(SIZE)` was [mixed] in booster: it
sometimes matched successfully but sometimes failed because booster rejected the
rewrite without proof that #powByteLen(SIZE) is defined. Since #powByteLen is a
function symbol with no-evaluators (always yields a defined term), adding
[preserves-definedness] is safe and fixes the gap.

This was the root cause of the kore-vs-booster gap in ecrecoverloop02-sig1-invalid
and ecrecoverloop02-sigs-valid benchmarks specs.

The new abi-spec.k claim pow-byte-len-simplify exercises this rule directly in
booster-only mode and passes after the fix.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
(cherry picked from commit efa0e111609946d7c3506e3a7ae2c6d52cef16e4)
(cherry picked from commit fcab3c84c70d9034bee5d6a3b3152c306b6e9d00)

* int-simplification.k, int-simplifications-spec.k: add [preserves-definedness] to 46 comparison normalization rules, add coverage claims

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
(cherry picked from commit ccce6b5dc1442f51df8939c71b3e378cf74c5894)
(cherry picked from commit 2b7099cf814c7ed27e8bc5af007cd52591e7b869)

* lemmas.k, lemmas-no-smt-spec.k: add bool #Equals workaround rules for BOOL-KORE @-variable patterns, add coverage claim

The BOOL-KORE module in K's domains.md defines 8 rules using @-prefixed
"here variables" (e.g., {true #Equals notBool @b}) which booster cannot
match.  Add equivalent rules with regular B:Bool variables to LEMMAS-HASKELL
so booster can apply the same normalizations.  Add a functional spec claim
exercising the notBool case, which passes in booster-only mode.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
(cherry picked from commit 80ed6938ac79faf1a98ef55ddc2a0226a3ae39b2)
(cherry picked from commit c498024497ff2a65fd6cc58916db745813f5acf4)

* lemmas/bytes-simplification.k, tests/functional/lemmas-no-smt-spec.k: add preserves-definedness to range-empty

The range-empty rule (#range(_,S,W) => .Bytes when S<0 or W<=0) previously
lacked [preserves-definedness], so booster refused to apply it during the
implies check.  Tag it accordingly and add two coverage claims to
lemmas-no-smt-spec.k to verify it fires in booster.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
(cherry picked from commit 666ba06c5956d8b9b540446089f73b6a45fba000)
(cherry picked from commit f30c2ff9ac9e7bdf0af6f10b47f716f5e0f1728e)

* buf.md, lemmas-no-smt-spec.k: add powByteLen-lt-concrete concrete comparison rule

After commit 5d0d8083c added [preserves-definedness] to the
2^Int(8*SIZE) => #powByteLen(SIZE) rule, booster fires it consistently
even when SIZE is concrete (the rule fires before path-condition lookup
makes the argument concrete).  Because #powByteLen has no-evaluators,
the result #powByteLen(N) cannot self-evaluate, leaving CONST <Int

Add [powByteLen-lt-concrete] to bridge that gap: when both CONST and N
are concrete the requires-clause delegates back to 2^Int arithmetic,
which can be evaluated directly.

Add a coverage claim in lemmas-no-smt-spec.k to verify the rule fires.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
(cherry picked from commit 8b4972c4cc410995c3ec2360ca6dd50c189d374b)
(cherry picked from commit 11b7050dfc88d903d1e1c1cb62802b6db25b9187)

* evm-semantics/evm-types.md: mark #asAccount as [total]

#asAccount is total over its Bytes domain — the two rules
(lengthBytes == 0 → .Account; [owise] → #asWord(BS)) are jointly
exhaustive. Marking it [total] lets booster's definedness checker
clear the RHS-definedness gate on rules that contain #asAccount in
their RHS — notably [call.delegatedAuthority] at evm.md:1633, where
the symbolic argument #range(CODE, 3, 20) prevents concrete evaluation
and previously caused booster to abort with "Uncertain about
definedness of rule due to: non-total symbol Lbl#asAccount", yielding
to kore for the rewrite step.

The recover-mode sweep across functional + examples + erc20 +
benchmarks identified 12 kore-execute handoffs (all benchmarks
ecrecover variants) that traced to exactly this definedness abort.
Validated locally on benchmarks/ecrecover00-siginvalid-spec.k:
2 handoffs → 0, proof still passes.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
(cherry picked from commit 33c04ff6558c339ffc06759dcaa49cd139222ef8)
(cherry picked from commit 4ce956c09bb03a7d06fdf533f95b2cfaa40b0dc7)

* lemmas/int-simplification.k: add minInt<maxInt / minInt<=maxInt base comparison rules

Tier-1 subset of upstream 258a68c71: keep the two base rules (sound since
minInt(A,_) <= A and C <= maxInt(C,_)); drop the non-linear shift/factored
variants pending review.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* lemmas/evm-int-simplification.k: add asWord comparison-false simplifications

Tier-1 subset of upstream 584462824: the asWord-{lt,le,eq}-false rules
(contrapositives of path-condition facts; RHS is false, so trivially
definedness-preserving). Drops that commit's slot-updates-spec.k edits
(claims regressed PASS->FAIL and need investigation). Coverage claims for
these rules are already in lemmas-no-smt-spec.k.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* lemmas/int-simplification.k: add eq-false-lt simplification

Tier-1 subset of upstream d0f4bdec3: keep eq-false-lt (A ==Int B => false
when A <Int B, B concrete). Drops le-1073741824-maxUInt64, whose 2^30 bound
is a non-general magic constant pending review. Coverage claim is already in
lemmas-no-smt-spec.k.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* evm.md, lemmas/lemmas.k: mark #widthOpCode [total, smtlib] and add bound + concat-lookup simplifications

Consolidates the Tier-1 #widthOpCode work from upstream Rounds 2-5 (which
iteratively rewrote the same lines): #widthOpCode is total (PUSH ops -> 2..33,
owise -> 1) and gets an smtlib symbol; widthOpCode-lb/ub encode its 0..33 range
as smt-lemmas; widthOpCode-concat-{left,right} push a concrete-prefix byte
lookup through +Bytes. Drops the Round-4 asWord-range-buf and the
#computeValidJumpDests preserves-definedness riders pending review.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* lemmas: drop redundant [preserves-definedness] from all-total simplification rules

For a [simplification] rule the booster's definedness obligation is the set of
non-total, non-constructor symbols on the LHS and RHS (Internalise.hs); when that
set is empty the rule is determined definedness-preserving automatically and the
attribute is a no-op. Removed it from the 66 rules added here whose every symbol
is total (`+Int -Int *Int` / comparisons / `minInt maxInt lengthBytes +Bytes
notBool` / the `total` functions `#asWord #buf #range #widthOpCode`), i.e. the
comparison-normalization block, eq-false-lt, the minInt<maxInt base rules,
asWord-{lt,le,eq}-false, asWord-buf-inversion, range-empty, lengthBytes-buf/range,
b"" concat identities, and the Bool #Equals distributions.

Kept on the 5 rules that root a partial symbol (where the attribute does real
work): the two #powByteLen rules (no-evaluators), lookup-as-asWord and
widthOpCode-concat-{left,right} (partial BYTES.get `_[_]`).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* evm.md: formatting

* buf.md: relax powByteLen-lt-concrete to concrete(CONST) only (review)

Per review: N need not be syntactically concrete -- once N is concrete the
`requires CONST <Int 2^Int(8*N)` reduces to a linear inequality, and if N is
symbolic the requires is undischargeable so the rule simply does not fire.
(It does not subsume `SIZE <Int #powByteLen(SIZE)`, which is the diagonal
same-variable case.)

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* lemmas/lemmas.k: drop widthOpCode-concat-{left,right} (review)

Per review: bytes-simplification.k already provides bytes-concat-lookup-{left,
right}, so these were only a workaround for booster not descending into
#widthOpCode(...) to apply them. Remove rather than duplicate per-function; if
the non-descent persists it should be addressed in the backend.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* lemmas/lemmas.k, tests/specs/functional/lemmas-no-smt-spec.k: drop unused bool-eq #Equals rules

Whole-prove-suite rule-firing measurement (booster Simplify + kore SimplifyKore
logging over functional/benchmarks/erc20/examples/kontrol/mcd) shows the eight
bool-eq-* ML-#Equals distribution rules are never applied by the booster: five
fire in no engine at all, and three (bool-eq-not-true-l/r, bool-eq-and-true-l)
fire only in the kore-rpc implies/subsumption path. Since this PR targets booster
performance and these proofs already discharge those goals under kore without the
rules, all eight are removed. The bool-*-self rules are kept (they fire in the
booster). The bool-eq-not-false coverage claim, which was discharged by
bool-eq-not-true-l rather than by the not-false rules, is removed with them.

Verified: lemmas-no-smt-spec proves all 22 remaining claims under --use-booster.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* tests/specs/mcd/verification.k: mark keccak disequality [smt-lemma] to fix DSS/MCD implies failures

The new tier1 simplification lemmas simplify away the keccak path-condition
constraint during EVM execution, so the final subsumption check can no longer
prove `keccak(_) =/=Int smallInt` from the path condition alone. Encoding the
rule as an SMT lemma lets Z3 discharge it independently of the path condition.

This matches the treatment already present in mcd-structured/verification.k,
whose sibling proofs pass; the plain mcd suite lacked the annotation. Fixes the
heal/fold/frob-diff-zero-dart DSS proofs and the mcd flopper-tick/end-pack rule
proofs. Verified mcd/end-pack-pass-rough-spec.k passes with the change.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* Revert "buf.md: relax powByteLen-lt-concrete to concrete(CONST) only (review)"

This reverts commit 6cd5f0d.

* tests/failing-symbolic.haskell-booster-dev: drop 5 specs now passing under booster-dev

Verified by running the booster-dev binary over the full skip-list on this branch:
mcd-structured/dsvalue-peek-pass-rough now passes under tier1's lemmas (failed on
master), and 4 entries (functional/bitwise-{asword,simplifications},
mcd[-structured]/dsvalue-read-pass-summarize) were stale (already passing on master).
bitwise-mask-shift-spec.k is intentionally kept: it regresses under booster-dev on
this branch.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* tests/failing-symbolic.haskell-booster-dev: re-add 2 dsvalue-read-pass-summarize specs failing booster-dev in CI

PR #2859 CI 'Proofs: Rules (booster-dev)' failed on mcd/dsvalue-read-pass-summarize
and mcd-structured/dsvalue-read-pass-summarize (SystemExit: 1); local verification
diverged from CI. Re-add them; the other three drops (mcd-structured/dsvalue-peek-pass-rough
and functional/bitwise-{asword,simplifications}) pass in CI and stay removed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: ehildenb

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md

@@ -37,10 +37,17 @@ module BUF
     syntax Int ::= #powByteLen ( Int ) [symbol(#powByteLen), function, no-evaluators]
  // ---------------------------------------------------------------------------------
  // rule #powByteLen(SIZE) => 2 ^Int (8 *Int SIZE)
-    rule 2 ^Int (8 *Int SIZE) => #powByteLen(SIZE) [symbolic(SIZE), simplification]
+    rule 2 ^Int (8 *Int SIZE) => #powByteLen(SIZE) [symbolic(SIZE), simplification, preserves-definedness]
 
     rule 0    <Int #powByteLen(SIZE) => true requires 0 <=Int SIZE [simplification, preserves-definedness]
     rule SIZE <Int #powByteLen(SIZE) => true requires 0 <=Int SIZE [simplification, preserves-definedness]
+    // Concrete comparison: CONST < #powByteLen(N) evaluates when both arguments are concrete.
+    // Needed because 2^Int(8*N) is rewritten to #powByteLen(N) even for concrete N (via the
+    // symbolic(N) rule firing before path-condition lookup makes N concrete), but #powByteLen
+    // has no-evaluators so the result can't be computed directly.
+    rule [powByteLen-lt-concrete]: CONST <Int #powByteLen(N) => true
+        requires 0 <=Int N andBool CONST <Int 2 ^Int (8 *Int N)
+        [simplification, concrete(CONST, N), preserves-definedness]
     rule #write(WM, IDX, VAL) => WM [ IDX := #buf(1, VAL) ] [simplification]
 
     rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA)

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md

@@ -358,8 +358,8 @@ Bytes helper functions
  // -------------------------------------------------------------------------
     rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete]
 
-    syntax Account ::= #asAccount ( Bytes )             [symbol(#asAccount), function]
- // ----------------------------------------------------------------------------------
+    syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function, total]
+ // -----------------------------------------------------------------------------
     rule #asAccount(BS) => .Account    requires lengthBytes(BS) ==Int 0
     rule #asAccount(BS) => #asWord(BS) [owise]
 

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -1812,8 +1812,8 @@ 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]
+    rule [bytes-concat-empty-left-concrete]:  b"" +Bytes B:Bytes => B [simplification]
 
     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)]
@@ -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,14 @@ 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]
+
   // 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 ) ) )
@@ -123,6 +131,18 @@ module EVM-INT-SIMPLIFICATION
   // Comparison: `#asWord(B)` is certainly less than or equal to something that is not less than the max number fitting into `lengthBytes(B)` bytes
   rule [asWord-le]:  #asWord ( B ) <=Int X:Int => true  requires ( 2 ^Int (8 *Int minInt(32, lengthBytes(B))) -Int 1 ) <=Int X [simplification, preserves-definedness]
 
+  // Comparison: `#asWord(B) < X` is false when the path condition says X <= #asWord(B).
+  // Loop-safe with asWord-le-false: requires clauses have #asWord on the RIGHT, so
+  // neither rule fires on the other's requires.
+  rule [asWord-lt-false]: #asWord ( B:Bytes )  <Int X:Int => false requires X <=Int #asWord ( B ) [simplification]
+  rule [asWord-le-false]: #asWord ( B:Bytes ) <=Int X:Int => false requires X  <Int #asWord ( B ) [simplification]
+  // Comparison: `#asWord(B) == X` is false when the path condition says X =/= #asWord(B).
+  // The requires X =/=Int #asWord(B) expands to notBool(X ==Int #asWord(B)) via the K builtin;
+  // since ==Int is comm, this matches the path condition fact notBool(#asWord(B) ==Int X).
+  // No loop: our rule matches #asWord on the LEFT; after builtin expansion the recursive
+  // term X ==Int #asWord(B) has X on the LEFT, so this rule does not fire on it.
+  rule [asWord-eq-false]: #asWord ( B:Bytes ) ==Int X:Int => false requires X =/=Int #asWord ( B ) [simplification]
+
   // Comparison: `#asWord` of `+Bytes` when lower bytes match, with `<Int`
   rule [asWord-concat-lt]:
     #asWord ( BA1 +Bytes BA2 ) <Int X:Int => #asWord ( BA1 ) <Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )

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,18 @@ 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.
+    // Sound: minInt(A,_) <=Int A and C <=Int maxInt(C,_), so A <Int C implies minInt(A,_) <Int maxInt(C,_).
+    rule [minint-lt-maxint-a]:
+        minInt(A:Int, _B:Int) <Int maxInt(C:Int, _D:Int) => true
+        requires A <Int C
+        [simplification(40)]
+    rule [minint-leq-maxint-b]:
+        minInt(_A:Int, B:Int) <=Int maxInt(_C:Int, D:Int) => true
+        requires B <=Int D
+        [simplification(40)]
+
   // ###########################################################################
   // inequality
   // ###########################################################################
@@ -241,6 +263,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
@@ -256,6 +286,9 @@ module INT-SIMPLIFICATION-COMMON
 
     rule A ==Int B => false requires 0 <=Int A andBool B <Int 0 [simplification, concrete(B)]
 
+    // A ==Int B is false when A < B is a known path-condition fact (B concrete).
+    rule [eq-false-lt]: A:Int ==Int B:Int => false requires A <Int B [simplification, concrete(B)]
+
     rule 0 <Int X => true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)]
 
     rule X <=Int maxUInt256 => X <Int pow256 [simplification]

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

@@ -245,6 +245,17 @@ module LEMMAS-HASKELL [symbolic]
       requires notBool ( I1 ==Int I2 )
       [simplification]
 
+  // ########################
+  // #widthOpCode range
+  // ########################
+
+    // #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]
+
   // ########################
   // Boolean Logic
   // ########################
@@ -259,4 +270,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

tests/failing-symbolic.haskell-booster-dev

@@ -59,9 +59,7 @@ tests/specs/examples/solidity-code-spec.md
 tests/specs/examples/storage-spec.md
 tests/specs/examples/sum-to-n-foundry-spec.k
 tests/specs/examples/sum-to-n-spec.k
-tests/specs/functional/bitwise-asword-spec.k
 tests/specs/functional/bitwise-mask-shift-spec.k
-tests/specs/functional/bitwise-simplifications-spec.k
 tests/specs/functional/bytes-range-spec.k
 tests/specs/functional/evm-int-simplifications-spec.k
 tests/specs/functional/infinite-gas-spec.k
@@ -116,7 +114,6 @@ tests/specs/mcd-structured/cat-exhaustiveness-spec.k
 tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k
 tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k
 tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k
-tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k
 tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k
 tests/specs/mcd-structured/end-cash-pass-rough-spec.k
 tests/specs/mcd-structured/end-pack-pass-rough-spec.k

tests/specs/functional/abi-spec.k

@@ -3,8 +3,8 @@ requires "abi.md"
 module VERIFICATION
     imports EVM-ABI
 
-    syntax Step ::= Bool | Bytes
- // ------------------------------
+    syntax Step ::= Bool | Bytes | Int
+ // -----------------------------------
 
     syntax KItem ::= runLemma ( Step ) [symbol(runLemma)]
                    | doneLemma( Step )
@@ -43,22 +43,26 @@ module ABI-SPEC
       <k> runLemma(
         #sizeOfDynamicType(
           #array(
-            #bytes(b"\x00"), 
-            3, 
+            #bytes(b"\x00"),
+            3,
             #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc")
           )
         )
         ==Int
         lengthBytes(#enc(
           #array(
-            #bytes(b"\x00"), 
-            3, 
+            #bytes(b"\x00"),
+            3,
             #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc")
           )
         ))
-      ) 
-      => doneLemma(true) 
-      ... 
+      )
+      => doneLemma(true)
+      ...
       </k>
 
+    claim [pow-byte-len-simplify]:
+      <k> runLemma ( 2 ^Int (8 *Int N:Int) ) => doneLemma ( #powByteLen(N:Int) ) ... </k>
+      requires 0 <=Int N
+
 endmodule

tests/specs/functional/int-simplifications-spec.k

@@ -127,4 +127,19 @@ module INT-SIMPLIFICATIONS-SPEC
 
     claim [le-maxuint256]: <k> runLemma ( X <=Int maxUInt256 ) => doneLemma ( X <Int pow256 ) ... </k>
 
+ // Comparison normalization coverage (int-simplification.k [preserves-definedness])
+ // ---------------------------------------------------------------------------------
+
+    claim [int-comp-norm-add-lt]:
+      <k> runLemma ( X:Int +Int 3 <Int 10 ) => doneLemma ( X:Int <Int 7 ) ... </k>
+
+    claim [int-comp-norm-add-le]:
+      <k> runLemma ( X:Int +Int 3 <=Int 10 ) => doneLemma ( X:Int <=Int 7 ) ... </k>
+
+    claim [int-comp-norm-sub-lt]:
+      <k> runLemma ( X:Int -Int 3 <Int 10 ) => doneLemma ( X:Int <Int 13 ) ... </k>
+
+    claim [int-comp-norm-rhs-add-lt]:
+      <k> runLemma ( 7 <Int X:Int +Int 3 ) => doneLemma ( 4 <Int X:Int ) ... </k>
+
 endmodule