Skip to content
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

Some bitwise and bool2Word lemmas #2241

Closed
wants to merge 11 commits into from
Closed

Some bitwise and bool2Word lemmas #2241

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
1a865c0
kproj/evm: avoid generating cell fragments
ehildenb Dec 23, 2023
42ef32d
lemmas/bitwise-simplification, specs/int-simplifications-spec: add si…
ehildenb Dec 24, 2023
eaaac0c
lemmas/int-simplification, specs/lemmas-spec: add simplifications for…
ehildenb Dec 24, 2023
a1f6689
Set Version: 1.0.408
Jan 9, 2024
1df4d57
Merge branch 'master' into bitwise-lemmas
ehildenb Jan 9, 2024
9d1328a
Set Version: 1.0.409
Jan 9, 2024
1ae7b01
Merge remote-tracking branch 'upstream/master' into bitwise-lemmas
ehildenb Jan 10, 2024
a668e48
Set Version: 1.0.411
Jan 10, 2024
980998f
lemmas/bitwise-simplification: generalize lemma
ehildenb Jan 10, 2024
cf808b8
Merge branch 'master' into bitwise-lemmas
PetarMax Jan 11, 2024
00aedfb
Set Version: 1.0.413
Jan 11, 2024
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
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kevm-pyk"
version = "1.0.408"
version = "1.0.409"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
from typing import Final


VERSION: Final = '1.0.408'
VERSION: Final = '1.0.409'
20 changes: 10 additions & 10 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -203,13 +203,13 @@ The `callStack` cell stores a list of previous VM execution states.
syntax InternalOp ::= "#pushCallStack"
// --------------------------------------
rule <k> #pushCallStack => . ... </k>
<callStack> STACK => ListItem(CALLSTATE) STACK </callStack>
<callStack> STACK => ListItem(<callState> CALLSTATE </callState>) STACK </callStack>
<callState> CALLSTATE </callState>

syntax InternalOp ::= "#popCallStack"
// -------------------------------------
rule <k> #popCallStack => . ... </k>
<callStack> ListItem(CALLSTATE) REST => REST </callStack>
<callStack> ListItem(<callState> CALLSTATE </callState>) REST => REST </callStack>
<callState> _ => CALLSTATE </callState>

syntax InternalOp ::= "#dropCallStack"
Expand All @@ -227,22 +227,22 @@ The `interimStates` cell stores a list of previous world states.
- `#dropWorldState` removes the top element of the `interimStates`.

```k
syntax Accounts ::= "{" AccountsCellFragment "|" SubstateCellFragment "}"
// -------------------------------------------------------------------------
syntax Accounts ::= "{" AccountsCell "|" SubstateCell "}"
// ---------------------------------------------------------

syntax InternalOp ::= "#pushWorldState"
// ---------------------------------------
rule <k> #pushWorldState => .K ... </k>
<interimStates> STATES => ListItem({ ACCTDATA | SUBSTATE }) STATES </interimStates>
<accounts> ACCTDATA </accounts>
<substate> SUBSTATE </substate>
<interimStates> STATES => ListItem({ <accounts> ACCTDATA </accounts> | <substate> SUBSTATE </substate> }) STATES </interimStates>
<accounts> ACCTDATA </accounts>
<substate> SUBSTATE </substate>

syntax InternalOp ::= "#popWorldState"
// --------------------------------------
rule <k> #popWorldState => .K ... </k>
<interimStates> ListItem({ ACCTDATA | SUBSTATE }) REST => REST </interimStates>
<accounts> _ => ACCTDATA </accounts>
<substate> _ => SUBSTATE </substate>
<interimStates> ListItem({ <accounts> ACCTDATA </accounts> | <substate> SUBSTATE </substate> }) REST => REST </interimStates>
<accounts> _ => ACCTDATA </accounts>
<substate> _ => SUBSTATE </substate>

syntax InternalOp ::= "#dropWorldState"
// ---------------------------------------
Expand Down
6 changes: 6 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,12 @@ module BITWISE-SIMPLIFICATION [symbolic]
lengthBytes(X) +Int 32 >Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true
[simplification, smt-lemma]

// ###########################################################################
// bit-xor
// ###########################################################################

rule X xorInt Y <Int 0 -Int X => false requires 0 <=Int X andBool 0 <=Int Y [simplification]

// ###########################################################################
// shift
// ###########################################################################
Expand Down
7 changes: 7 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,4 +243,11 @@ module INT-SIMPLIFICATION-COMMON
requires 0 <Int Y
[simplification, comm]

// ###########################################################################
// comparisons
// ###########################################################################

rule X ==Int 0 => true requires 0 <=Int X andBool X <=Int 0 [simplification, comm]
rule X ==Int 0 => false requires 0 <Int X [simplification, comm]
Comment on lines +250 to +251
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lemmas like these tend to slow down the execution. @dwightguth has flagged this in the Maude backend, I've also noticed a considerable speedup once I commented slightly more general lemmas that we had out of the work on symbolic calldata. The CI is currently timing out and lasting almost double the time it did before.

I remember introducing these more general lemmas for Optimism because of the looping on the symbolic size of a bytes parameter, getting constraints of the form 37 <=Int X and X <=Int 37, and the backend not understanding without SMT that X ==Int 37. The lemmas were:

rule   A <=Int B                =>   A  ==Int  B   requires B <=Int A [simplification, concrete(A)]
rule { A <=Int B #Equals true } => { A #Equals B } requires B <=Int A [simplification, concrete(A)]
rule { true #Equals A <=Int B } => { A #Equals B } requires B <=Int A [simplification, concrete(A)]

How did these two lemmas come up?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The tests added are exactly the expressions that came up causing these lemmas to be added. I can try out the lemmas you suggest.

Whenever I run into something unsimplified that I want simplified, the first thing I do is snip out that expression and add it as a test to KEVM. Then I begin working on that test directly.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I understand that. I'm not suggesting that you replace your lemmas with the ones I suggest. All that I am saying is that I had similar lemmas that were slowing down the performance. I suspect that your lemmas are causing a slowdown that resulted in the CI failure. Have you got a performance comparison of this branch vs master?


endmodule
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.408
1.0.409
4 changes: 4 additions & 0 deletions tests/specs/functional/int-simplifications-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,4 +36,8 @@ module INT-SIMPLIFICATIONS-SPEC
<k> runLemma ( minInt(_A +Int E, B +Int E) <=Int maxInt(_C +Int F, D +Int F) ) => doneLemma ( true ) ... </k>
requires B <=Int D andBool E <=Int F

claim [xor-maxuint256]:
<k> runLemma ( notBool ( 0 -Int V0 <=Int V0 xorInt maxUInt256 ) ) => doneLemma ( false ) ... </k>
requires #rangeUInt(96, V0)

endmodule
3 changes: 3 additions & 0 deletions tests/specs/functional/lemmas-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,9 @@ module LEMMAS-SPEC

claim <k> runLemma ( bool2Word((UINT8 ==K 0) ==K false) ) => doneLemma ( UINT8 ) ... </k> requires #rangeBool(UINT8)

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

// sizeBytes
// -------------

Expand Down
Loading