lemmas: add bool2Word simplification for symbolic Bool expressions#2848
Draft
Stevengre wants to merge 4 commits into
Draft
lemmas: add bool2Word simplification for symbolic Bool expressions#2848Stevengre wants to merge 4 commits into
Stevengre wants to merge 4 commits into
Conversation
The legacy rules
rule bool2Word( true ) => 1
rule bool2Word( false ) => 0
pattern-match on the argument position. Pattern matching only runs the
simplifier, not the path-condition + SMT reasoning, so a goal like
bool2Word(X >=Int 0) => 1 under path condition X >Int 0
leaves `bool2Word(X >=Int 0)` un-reduced even though the path condition
strictly implies the argument. The implication check at the end then
fails, and the proof gets stuck.
Rewriting the rules as
rule bool2Word( B:Bool ) => 1 requires B ==Bool true
rule bool2Word( B:Bool ) => 0 requires notBool B ==Bool true
moves the same question to a side condition, which Kore discharges
against the full path condition (with SMT). The two forms agree on
concrete inputs and on free Bool variables (Kore canonicalizes `requires
B` into a substitution `B |-> true` before the rule is tried), but the
new form additionally handles symbolic Bool *expressions* whose truth
the path condition only implies.
The new functional spec `tests/specs/functional/bool2Word-symbolic-spec.k`
documents the behavior: claims 1-4 (free variable, syntactic equality)
pass under both forms; claims 5-6 (path condition implies but does not
equate the argument) fail under the legacy rules and pass under the new
ones.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Each claim's behavior is already evident from the path condition and target; the file-level comment retains the one fact that matters (why claims 5-6 are the diagnostic ones). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
ehildenb
reviewed
May 25, 2026
Comment on lines
+32
to
+33
| rule bool2Word( B:Bool ) => 1 requires B ==Bool true | ||
| rule bool2Word( B:Bool ) => 0 requires notBool B ==Bool true |
Member
There was a problem hiding this comment.
Suggested change
| rule bool2Word( B:Bool ) => 1 requires B ==Bool true | |
| rule bool2Word( B:Bool ) => 0 requires notBool B ==Bool true | |
| rule bool2Word( B:Bool ) => 1 requires B | |
| rule bool2Word( B:Bool ) => 0 requires notBool B |
Does it work like this instead?
Member
There was a problem hiding this comment.
And you may consider, instead, just writing additional simplification lemmas in lemmas.k, and see if that works:
rule bool2Word(B) => 1 requires B [simplification]
rule bool2Word(B) => 0 requires notBool B [simplification]
Member
There was a problem hiding this comment.
That way we get hte better booster performance, and we keep LLVM backend fast path.
Contributor
Author
There was a problem hiding this comment.
Switched to this approach in 6757536 — simplification lemmas in lemmas/lemmas.k, evm-types.md untouched. Verified all 6 test claims still pass on the new path (legacy form: 2 stuck; either approach: 6 trivial). Timed both approaches at ~2.5s on the micro-spec — indistinguishable within noise.
Per @ehildenb's review (#2848): rather than rewrite the bool2Word function rules in evm-types.md, add two [simplification] lemmas in lemmas/lemmas.k. Equivalent end behavior on the new spec, but: - Core semantics unchanged - Only spec files importing LEMMAS see the new behavior - Concrete bool2Word inputs still go through the original function rules at zero cost - Co-locates with the existing bool2Word simplification lemmas Reverts the evm-types.md change. Updates the spec comment. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Stevengre
changed the title
Co-Authored-By: Claude Opus 4.7 (1M context) <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
2 participants
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.
Add two
[simplification]lemmas inlemmas/lemmas.kso thatbool2Word(B)reduces when the path condition impliesBbut does notsyntactically equate it. The function rules in
evm-types.mdareunchanged — concrete inputs still take the original zero-overhead path.
In Kore, the existing function rules pattern-match on
true/falseinthe argument position, which only runs the simplifier (no SMT against
the path condition). The new simplification lemmas bind
Bunconditionally and discharge the side condition with the full path
condition, so a goal like
bool2Word(X >=Int 0) => 1under pathcondition
X >Int 0now reduces.Tests
tests/specs/functional/bool2Word-symbolic-spec.kpins this with 6claims:
BBBnotBool BX >Int YX >Int YX >Int YnotBool (X >Int Y)X >=Int 0X >Int 0X <Int 0X >Int 0History
The original commits on this branch modified the
bool2Wordfunctionrules in
evm-types.mddirectly. Per @ehildenb's review feedback,switched to the
[simplification]lemma approach — equivalent on thisspec, less invasive, opt-in via
imports LEMMAS.Test plan
make test-prove-functional(in particularlemmas-spec.kregressions — many existing
bool2Wordlemmas live next to the newones)
make test-prove-rules/test-prove-optimizationsDraft pending full suite run.
🤖 Generated with Claude Code