Optimize summary rules #2732

Stevengre · 2025-04-02T14:14:08Z

remove unneccessary summaries with statusCode changes, like EVM_STACK_OVERFLOW
remove unneccessary constraints for the preconditions
remove ensures clauses that might not be satified by the preconditions.

- remove unneccessary summaries with `statusCode` changes, like `EVM_STACK_OVERFLOW` - remove unneccessary constraints for the preconditions - remove ensures clauses that might not be satified by the preconditions.

tothtamas28

LGTM. I'll let @JuanCoRo approve the PR though, as he has a better understanding of the implications of this change on the proving process.

tothtamas28 · 2025-04-02T15:01:56Z

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -289,6 +289,35 @@ def get_todo_list() -> list[str]:
    return todo_list


+def stack_added(opcode_id: str) -> int:


Suggested change

def stack_added(opcode_id: str) -> int:

def stack_added(opcode: str) -> int:

(Similarly for the rest.)

I'm working on the better rule id and will fix it latter!

After that, I hope that @JuanCoRo can just use <opcode name>-SUMMARY-USEGAS to generate the lean code.

Hey @Stevengre! Should the -SUMMARY-USEGAS labeling be in place already? For what I see in the last commit it's still using the old one (e.g., rule [ADD-SUMMARY-0]:)
Is this meant for a follow up PR? Thank you!

Sure, I'll provide the better names in the next PR. Just after merging this one.

For this one, I make the require clause more feasible for some opcode and reduce the rules to make it easier to generate better names.

There are still some problems for some opcodes, like balance. But I think that I can resolve it when you need.

- Updated the `stack_added`, `stack_needed`, and `stack_delta` functions to accept `opcode` as a parameter instead of `opcode_id`, improving clarity and consistency in the codebase.

JuanCoRo · 2025-04-03T10:41:12Z

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/pushzero-summary.k

-       andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
-       andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
+       andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023


These conditions here are not exactly equivalent, right? I think we would still need something like

0 <=Int #sizeWordStack ( WS:WordStack , 0 )

Am I missing something?

This is generated automatically, since I don't provide any not underflow condition for the opcodes. This follows the same principle as the not overflow before opcode execution that you might need to add this assumption in the theorems.

Do you know why there's an overflow requirement but not an underflow? I'm just trying to understand where this condition get s dropped.

Wait a minute... Let me check the semantics...

Reason for this:

The following new-introduced code provides not overflow precondition for the opcode summaries.

evm-semantics/kevm-pyk/src/kevm_pyk/summarizer.py

Line 624 in e7498c3

init_constraints.append(_le(_ws_size(stack_needed(op)), KToken(str(1024 - delta), 'Int')))

As a result, the following rule applies without a split according to the conditions.

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

Lines 347 to 356 in e7498c3

rule <k> #next [ OP:OpCode ]

=> #addr [ OP ]

~> #exec [ OP ]

~> #pc [ OP ]

...

</k>

<wordStack> WS </wordStack>

<static> STATIC:Bool </static>

requires notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) )

andBool notBool ( STATIC andBool #changesState(OP, WS) )

However, without this new precondition, there will be a split for

notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) ) andBool notBool ( STATIC andBool #changesState(OP, WS) )

And it seems like the haskell backend doesn't reduce notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) ) to its simplest conjunctive normal form (CNF) -- notBool #stackUnderflow(WS, OP) andBool notBool #stackOverflow(WS, OP).

Therefore, when notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) ) is false, since #stackUnderflow(WS, OP) is always false for pushzero, then this constraint is reduced to #stackOverflow(WS, OP) and evaluate to 1023 <Int #sizeWordStack ( _WS:WordStack , 0 ).

When notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) ) is true, ???

Sorry, forget it... It looks strange to me. It might also relate to the existing simplifcation rules like:

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

Line 49 in e7498c3

rule N <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]

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

Lines 218 to 219 in e7498c3

rule notBool (A <Int B) => B <=Int A [simplification]

rule notBool (A <=Int B) => B <Int A [simplification]

And it might also relate to the way that the backend tackle the side conditions and simplication rules.

I'm sorry, Juan. I'm actually not quite sure why such a strange condition was generated previously. This is indeed an interesting issue. I think @ehildenb and @jberthold might have more thoughts on what could be causing this result.

These conditions here are not exactly equivalent, right? I think we would still need something like

0 <=Int #sizeWordStack ( WS:WordStack , 0 )

Am I missing something?

Reason for this:
...

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

Line 49 in e7498c3

rule N <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]

I think the simplification that @Stevengre points out makes the 0 <= ... condition redundant (specialise N == 0 in the lemma).

And just to clarify:

And it seems like the haskell backend doesn't reduce notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) ) to its simplest conjunctive normal form (CNF) -- notBool #stackUnderflow(WS, OP) andBool notBool #stackOverflow(WS, OP).

Correct for the booster backend, we are trying to not transform predicates to CNF (the only transformation we do is to turn ML predicates into 1st-order ones). The legacy backend might have logic to transform to CNF but this is actually not a desired thing - we want all simplifications to be readable K code rather than backend magic.

In this case, we could maybe just write the CNF into the rule in the first place?

Thank you @Stevengre and @jberthold!!
It makes sense to me now, so I'll approve the PR!

Thank you @jberthold! It makes a lot of sence! But I think that we can also make this CNF during the frontend process. I'll make an issue to record this.

Stevengre added 2 commits April 2, 2025 20:44

optimize the summary rules

47ea4ed

- remove unneccessary summaries with `statusCode` changes, like `EVM_STACK_OVERFLOW` - remove unneccessary constraints for the preconditions - remove ensures clauses that might not be satified by the preconditions.

fix error spec file name

3e0ea64

Stevengre requested review from tothtamas28 and JuanCoRo April 2, 2025 14:18

Stevengre self-assigned this Apr 2, 2025

Stevengre marked this pull request as ready for review April 2, 2025 14:18

tothtamas28 reviewed Apr 2, 2025

View reviewed changes

Refactor stack functions to use opcode parameter instead of opcode_id

e7498c3

- Updated the `stack_added`, `stack_needed`, and `stack_delta` functions to accept `opcode` as a parameter instead of `opcode_id`, improving clarity and consistency in the codebase.

JuanCoRo reviewed Apr 3, 2025

View reviewed changes

JuanCoRo approved these changes Apr 7, 2025

View reviewed changes

Stevengre mentioned this pull request Apr 7, 2025

Optimize the side conditions in the semantics to help the booster backend reasoning #2736

Open

Merge branch 'master' into optimize-summary-rules

87e2d8f

Stevengre merged commit 13cfef5 into master Apr 7, 2025
12 checks passed

Stevengre deleted the optimize-summary-rules branch April 7, 2025 13:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Optimize summary rules #2732

Optimize summary rules #2732

Stevengre commented Apr 2, 2025 •

edited

Loading

tothtamas28 left a comment

tothtamas28 Apr 2, 2025

Stevengre Apr 2, 2025

Stevengre Apr 2, 2025 •

edited

Loading

Stevengre Apr 2, 2025

JuanCoRo Apr 2, 2025

Stevengre Apr 2, 2025

Stevengre Apr 2, 2025

Stevengre Apr 2, 2025

JuanCoRo Apr 3, 2025

Stevengre Apr 3, 2025

JuanCoRo Apr 3, 2025

Stevengre Apr 3, 2025

Stevengre Apr 3, 2025

jberthold Apr 3, 2025

JuanCoRo Apr 7, 2025

Stevengre Apr 7, 2025

		@@ -289,6 +289,35 @@ def get_todo_list() -> list[str]:
		return todo_list


		def stack_added(opcode_id: str) -> int:

	def stack_added(opcode_id: str) -> int:
	def stack_added(opcode: str) -> int:

	rule <k> #next [ OP:OpCode ]
	=> #addr [ OP ]
	~> #exec [ OP ]
	~> #pc [ OP ]
	...
	</k>
	<wordStack> WS </wordStack>
	<static> STATIC:Bool </static>
	requires notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) )
	andBool notBool ( STATIC andBool #changesState(OP, WS) )

	rule notBool (A <Int B) => B <=Int A [simplification]
	rule notBool (A <=Int B) => B <Int A [simplification]

Optimize summary rules #2732

Optimize summary rules #2732

Conversation

Stevengre commented Apr 2, 2025 • edited Loading

tothtamas28 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Stevengre Apr 2, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Stevengre commented Apr 2, 2025 •

edited

Loading

Stevengre Apr 2, 2025 •

edited

Loading