Skip to content

lemmas: add bool2Word simplification for symbolic Bool expressions #2848

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Stevengre wants to merge 4 commits into
base: master
Choose a base branch
from
+53 −0
Draft

lemmas: add bool2Word simplification for symbolic Bool expressions #2848

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
55a2659
evm-types: rewrite bool2Word rules with side conditions
May 25, 2026
11588e7
bool2Word-symbolic-spec: drop redundant inline comments
May 25, 2026
6757536
switch to simplification lemmas in lemmas.k
May 26, 2026
a7ee100
lemmas: trim bool2Word simplification comment
May 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
// bool2Word reasoning
// ########################

// Reduce when the path condition only implies the argument.
rule [b2w-true]: bool2Word(B) => 1 requires B [simplification]
rule [b2w-false]: bool2Word(B) => 0 requires notBool B [simplification]

// Range
rule [b2w-lb]: 0 <=Int bool2Word(_) => true [simplification, smt-lemma]
rule [b2w-ub]: bool2Word(_) <=Int 1 => true [simplification, smt-lemma]
Expand Down
1 change: 1 addition & 0 deletions kevm-pyk/src/tests/integration/test_prove.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,7 @@ def exclude_list(exclude_file: Path) -> list[Path]:
'functional/lemmas-no-smt-spec.k': 'lemmas-no-smt-spec.k',
'functional/lemmas-spec.k': 'lemmas-spec.k',
'functional/abi-spec.k': 'abi-spec.k',
'functional/bool2Word-symbolic-spec.k': 'bool2Word-symbolic-spec.k',
'functional/merkle-spec.k': 'merkle-spec.k',
'functional/slot-updates-spec.k': 'slot-updates-spec.k',
'functional/storageRoot-spec.k': 'storageRoot-spec.k',
Expand Down
48 changes: 48 additions & 0 deletions tests/specs/functional/bool2Word-symbolic-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
requires "edsl.md"
requires "lemmas/lemmas.k"

module VERIFICATION
imports EDSL
imports LEMMAS

syntax StepSort ::= Int | Bool
// ------------------------------

syntax KItem ::= runLemma ( StepSort ) [symbol(runLemma)]
| doneLemma( StepSort )
// --------------------------------------
rule runLemma( T ) => doneLemma( T )

endmodule

// Without the `b2w-true` / `b2w-false` simplification lemmas in lemmas.k,
// claims 5-6 fail: the path condition implies but does not equate the
// argument, so the function-rule matcher cannot discharge it without SMT.
// With the simplification lemmas, all six claims pass.
module BOOL2WORD-SYMBOLIC-SPEC
imports VERIFICATION

claim [b2w-var-true]:
<k> runLemma ( bool2Word(B:Bool) ) => doneLemma( 1 ) ... </k>
requires B

claim [b2w-var-false]:
<k> runLemma ( bool2Word(B:Bool) ) => doneLemma( 0 ) ... </k>
requires notBool B

claim [b2w-expr-eq-true]:
<k> runLemma ( bool2Word(X >Int Y) ) => doneLemma( 1 ) ... </k>
requires X >Int Y

claim [b2w-expr-eq-false]:
<k> runLemma ( bool2Word(X >Int Y) ) => doneLemma( 0 ) ... </k>
requires notBool (X >Int Y)

claim [b2w-implied-true]:
<k> runLemma ( bool2Word(X >=Int 0) ) => doneLemma( 1 ) ... </k>
requires X >Int 0

claim [b2w-implied-false]:
<k> runLemma ( bool2Word(X <Int 0) ) => doneLemma( 0 ) ... </k>
requires X >Int 0
endmodule
Loading