Lemmas tier1#2859
Draft
ehildenb wants to merge 22 commits into
Draft
Conversation
…-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)
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)
…n-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)
…ation 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)
…en 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)
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)
…ication, 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)
…nedness] 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)
… 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)
… 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)
…parison 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)
#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)
…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>
…cations
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>
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>
…und + 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>
…ication 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>
ehildenb
commented
Jun 4, 2026
Comment on lines
+134
to
+144
| // 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] |
Member
Author
There was a problem hiding this comment.
These lemmas seem like they could be made more generic, just with Int variables on each side of the binary comparson operator instead. The last one may result in a loop because =/=Int may simplify down to ==Int.
Member
Author
There was a problem hiding this comment.
The naive generalization loops the same way =/= does: generic lt/le rewrite each other's <=/< requires. The #asWord LHS-vs-requires asymmetry is what keeps these loop-safe, so I kept them specific. Happy to add a loop-safe (e.g. concrete-guarded) generic variant if you'd prefer.
ehildenb
commented
Jun 4, 2026
ehildenb
commented
Jun 4, 2026
Comment on lines
+43
to
+50
| 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] |
Member
Author
There was a problem hiding this comment.
Dose this generalize the previous lemma? I guess not since the previous one applies for all SIZE, not just concrete SIZE. Also, I think this lemma could be non-concrete in N and it should be OK, if N is concrete we simplify down to basic linear arithmetic inequalities, and so that shouldn't cause any solver issues.
Member
Author
There was a problem hiding this comment.
Right, it doesn't generalize the diagonal SIZE <Int #powByteLen(SIZE) (same var both sides). Relaxed to concrete(CONST) — once N is concrete the requires is a linear inequality; symbolic N just doesn't fire. 6cd5f0d
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>
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>
ehildenb
commented
Jun 5, 2026
Comment on lines
+104
to
+111
| // 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] | ||
|
|
Member
Author
There was a problem hiding this comment.
Doesn't this end up being a less general rule than the asWord-buf-inversion above?
…used 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>
…o 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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.