Integrate summaries of opcode automatically into the evm semantics #2710

Stevengre · 2025-02-27T13:32:30Z

This PR is based on #2676, integrating all the summaries into the evm semantics. Specifically, it includes the following changes:

Enhance summarize command with opcode-specific and clear options.
Modify the function to generate correct summary files that can be used directly.
Provide new kdist build targets using these summary rules.
Modify the .gitignore to integrate the summary files by default.

tothtamas28

Please add a description for the PR, and make sure tests pass.

Stevengre · 2025-03-07T13:56:53Z

Change files:

summarizer.py: Although there are 113 change files, the key file to this PR is summarizer.py, where I modify the summarize function to print kompileable K files.
summaries/: All the K files in summaries are generated automatically through the summarizer.py and tested by the kidst build.
driver.md & edsl.md: I provided two new modules for the kidst to target.
__main.py & cli.py: Here, I made a better option for the summarize command.

Stevengre · 2025-03-07T13:57:03Z

Should I provide tests to test the summary rules? Just like what we've done for the exising one, showing that the summary rules do the same as the previous ones. Or should we verify if the rules are correct or not?

Should we provide these tests inside of the CI? Should delete the previous CI test for the summarzation after we've provided the one for testing/verifying the summarization result.

Stevengre · 2025-03-07T14:27:58Z

Or maybe I can verify the correctness of these summary rules and migrate all the tests through the normal semantics to the summary ones?

tothtamas28 · 2025-03-11T13:54:24Z

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

+module EDSL-SUMMARY
+    imports EDSL-PURE
+    imports SUMMARY
+endmodule
+
+module EDSL-SUMMARIZE


What's the difference between these two modules?

SUMMARY is to use the summary rules.
SUMMARIZE is used to generate the summary rules.

tothtamas28 · 2025-03-12T07:52:04Z

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -643,13 +698,12 @@ def batch_summarize(num_processes: int = 4) -> None:
        num_processes: Number of parallel processes to use. Defaults to 4.
    """

-    opcodes_to_process = OPCODES.keys()
+    OPCODES.keys()


Suggested change

OPCODES.keys()

tothtamas28 · 2025-03-12T07:53:35Z

kevm-pyk/src/kevm_pyk/summarizer.py

+        def _remove_inf_gas(res_line: str) -> str:
+            return re.sub(r'#gas (\([^)]*\))', r'\1', res_line)


Would it be possible to do these transformations directly on the KRule produced by summarization?

I think it is possible. But I don't know if it is possible for all. I'll give it a try.

…ule. This commit includes build_spec and explore to constrcut a specification for all instructions and explore it.

…ding to KEVMSemantics

…r instructions

- Remove unnecessary account constraints and DotAccountVar references - Modify summarizer to handle complex regex replacements for cleaner spec files - Update opcode symbol parsing to handle parentheses in opcode names - Remove redundant requires and andBool conditions in summary specs - Rename an undefined opcode summary file to fix import syntax

…constraints - Modify summarizer to comment out complex regex replacements - Update summary files to use simpler account representation - Remove parenthesized account and DotAccountVar references - Restore _use_legal_remainder function with commented-out complex logic

- Update summary files for numerous EVM opcodes - Modify basic block rules in summary specification files - Systematically process and generate summary files for various EVM instructions

- Add function to replace LHS function with assignment in summary-balance specs - Modify account ID representation in balance summary files - Update regex transformation to simplify account ID constraints

- Reduce summarization test timeout from 360 to 150 seconds - Remove duplicate method in KEVM class - Update poetry.lock dependencies and extras - Modify batch summarization processing logic - Clean up regex transformations in summary specification generation

- Modify Poetry lock file to add platform-specific extras and dependency constraints - Update Poetry version from 2.0.1 to 2.1.1 - Add conditional dependencies for different Python implementations and versions - Refine package extras with more precise platform and version requirements

- Upgrade Hypothesis from 6.125.2 to 6.127.9 - Update setuptools from 75.8.0 to 75.8.2 - Add watchdog dependency to Hypothesis extras - Refresh package hashes and version constraints

- Modify account ID replacement logic in summarizer - Remove commented-out explanatory notes - Streamline regex pattern for summary-balance specifications

- Reformat target argument definition for better readability - Maintain existing target choices for KEVM CLI

…nd summaried one.

- Reduced timeout for the 'Summarization' test suite from 150 to 30 seconds. - Updated dependencies: filelock to version 3.18.0, hypothesis to version 6.129.1, and setuptools to version 76.0.0 in poetry.lock.

…from summarizer and summary.k files to address potential issues with log2 calculations.

…rences - Enhanced error handling in the interpreter to raise a RuntimeError with detailed information if the interpreter fails or returns empty output. - Restored references to 'summary-exp-2-spec.k' and 'SUMMARY-EXP-2-SPEC' in the summarizer and summary.k files to ensure proper functionality after previous removals.

Stevengre · 2025-03-17T10:20:09Z

Performances

pure is kdist target without EVM-OPTIMIZATIONS; summary is kdist target with SUMMARY.

command	kdist	real	user	sys
make test-conformance	llvm-pure	5m37.384s	12m5.376s	1m42.848s
make test-conformance	llvm	5m15.323s	11m19.932s	1m38.279s
make test-conformance	llvm-summary	5m3.396	11m25.853s	1m37.160s
make test-prove-rules	haskell-pure
make test-prove-rules	haskell
make test-prove-rules	haskell-summary
make test-prove-functional	haskell-pure
make test-prove-functional	haskell
make test-prove-functional	haskell-summary
make test-prove-dss	haskell-pure
make test-prove-dss	haskell
make test-prove-dss	haskell-summary

For concrete execution,
- The summary rules perform better than the semantics without EVM-OPTIMIZATIONS, but worse than the one with EVM-OPTIMIZATIONS. It shows that the summary rules do summarize the rules for the opcode like EVM-OPTIMIZATIONS, but the summarization is not good as EVM-OPTIMIZATIONS. For example, EVM-OPTIMIZATIONS only use one rule for ADD, however, SUMMARY-ADD-2-SPEC takes two. What makes it worse should be the summary rules for dup, swap and log, because they consumes mutable wordstack which ends up with more modules for them under current summarization implementation. Moreover, some opcodes don't support use-gas summarization, which cannot be used for concrete execution.
- Time reduction is less than what I expected (10+ steps into 1 step). It might due to the programs under tested are small and it costs more time to do something else rather than run opcodes. I'm not sure for this analysis.
- Here is another result for summary rules (real 3m34.911s; user 11m15.463s; sys 1m37.799s) (real 3m35.102s; user 11m12.657s; sys 1m35.723s). Therefore, summary rules might not be worse than optimization rules. But llvm (real 3m32.791s; user 11m3.709s; sys 1m36.085s)

Stevengre requested review from tothtamas28 and anvacaru March 4, 2025 06:45

tothtamas28 reviewed Mar 4, 2025

View reviewed changes

Stevengre self-assigned this Mar 4, 2025

Stevengre force-pushed the jh/summary-integration branch from f6646f4 to 82c51a7 Compare March 7, 2025 13:12

Stevengre requested a review from ehildenb March 7, 2025 14:08

Stevengre marked this pull request as ready for review March 7, 2025 14:08

Stevengre requested a review from tothtamas28 March 7, 2025 14:30

JuanCoRo mentioned this pull request Mar 10, 2025

Generate Lean code from intended summaries runtimeverification/evm-equivalence#3

Merged

Stevengre force-pushed the jh/summary-integration branch from f96c3c7 to 0e86747 Compare March 11, 2025 11:44

tothtamas28 reviewed Mar 11, 2025

View reviewed changes

tothtamas28 reviewed Mar 12, 2025

View reviewed changes

Stevengre force-pushed the jh/summary-integration branch from ce061ca to 12fe54e Compare March 12, 2025 17:07

Stevengre and others added 14 commits March 14, 2025 18:00

provide KEVMSummarizer to sammarize rules for all the instruction r…

ce37bb1

…ule. This commit includes build_spec and explore to constrcut a specification for all instructions and explore it.

solve error call for legacy_explore and incorrect name for #next[_]

e159c31

kevm-pyk/: get code passing basic type checking issues

a8a5c1c

qupdate poetry to 2.0.0

6942dce

add new command summarize for summarizing evm instructions

2bbdc04

don't use summarize but kevm summarize instead.

10d9534

provide spec with initial and target node that are not terminal accor…

c207fc2

…ding to KEVMSemantics

make format & make check

4127ce0

print nodes and add summarize function to generate optimized rules fo…

ae80f65

…r instructions

make format & make check

4ddfc0a

add ignore

c28a58e

allow_symbolic_program

1652b8f

summarize instructions one by one

ad173a1

summarize STOP

73d8d88

Stevengre added 22 commits March 14, 2025 18:00

new way to remove inf gas

0ae7674

remove_dash_from_var

55671b6

Generate summary specification files for multiple EVM opcodes

572d4fe

- Update summary files for numerous EVM opcodes - Modify basic block rules in summary specification files - Systematically process and generate summary files for various EVM instructions

Enhance summary specification file generation for balance opcode

3fdefd2

- Add function to replace LHS function with assignment in summary-balance specs - Modify account ID representation in balance summary files - Update regex transformation to simplify account ID constraints

Update poetry.lock with Hypothesis and setuptools version bumps

c77f67e

- Upgrade Hypothesis from 6.125.2 to 6.127.9 - Update setuptools from 75.8.0 to 75.8.2 - Add watchdog dependency to Hypothesis extras - Refresh package hashes and version constraints

bring back the modification in the master branch

7b51cf4

Simplify summary-balance account ID regex transformation

a9c71c2

- Modify account ID replacement logic in summarizer - Remove commented-out explanatory notes - Streamline regex pattern for summary-balance specifications

Add new target options for KEVM CLI summary targets

8b0697b

Improve CLI target argument formatting

65d78f6

- Reformat target argument definition for better readability - Maintain existing target choices for KEVM CLI

update expected file with new module name

e5c4c77

provide a basic way to verify the summaries

88d3441

change the require to pass the verification

97c23cd

try to add gas gaurd automatically

2cfbbf0

try to provide gas guard automatically

53de37f

solved out of gas problem for most opcode summaries

f59cbec

fix summaries for the summaries of opcode like return

9a59d44

make test-prove-summaries passed

9033bda

[to delete] add concrete execution result for both normal semantics a…

3423f02

…nd summaried one.

Stevengre force-pushed the jh/summary-integration branch from 30a0dcc to 3423f02 Compare March 14, 2025 18:00

Stevengre added 4 commits March 14, 2025 18:12

Update test timeout and dependencies in poetry.lock

6fbcbe0

- Reduced timeout for the 'Summarization' test suite from 150 to 30 seconds. - Updated dependencies: filelock to version 3.18.0, hypothesis to version 6.129.1, and setuptools to version 76.0.0 in poetry.lock.

Remove references to 'summary-exp-2-spec.k' and 'SUMMARY-EXP-2-SPEC' …

0c9b396

…from summarizer and summary.k files to address potential issues with log2 calculations.

[to delete] update the concrete execution result of the summary rules.

8a64faf

Stevengre closed this Mar 18, 2025

JuanCoRo mentioned this pull request Mar 19, 2025

Update generated Lean code runtimeverification/evm-equivalence#5

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Integrate summaries of opcode automatically into the evm semantics #2710

Integrate summaries of opcode automatically into the evm semantics #2710

Stevengre commented Feb 27, 2025 •

edited

Loading

tothtamas28 left a comment

Stevengre commented Mar 7, 2025

Stevengre commented Mar 7, 2025 •

edited

Loading

Stevengre commented Mar 7, 2025

tothtamas28 Mar 11, 2025

Stevengre Mar 17, 2025

tothtamas28 Mar 12, 2025

tothtamas28 Mar 12, 2025

Stevengre Mar 17, 2025 •

edited

Loading

Stevengre commented Mar 17, 2025 •

edited

Loading

		def _remove_inf_gas(res_line: str) -> str:
		return re.sub(r'#gas (\([^)]*\))', r'\1', res_line)

Integrate summaries of opcode automatically into the evm semantics #2710

Integrate summaries of opcode automatically into the evm semantics #2710

Conversation

Stevengre commented Feb 27, 2025 • edited Loading

tothtamas28 left a comment

Choose a reason for hiding this comment

Stevengre commented Mar 7, 2025

Stevengre commented Mar 7, 2025 • edited Loading

Stevengre commented Mar 7, 2025

tothtamas28 Mar 11, 2025

Choose a reason for hiding this comment

Stevengre Mar 17, 2025

Choose a reason for hiding this comment

tothtamas28 Mar 12, 2025

Choose a reason for hiding this comment

tothtamas28 Mar 12, 2025

Choose a reason for hiding this comment

Stevengre Mar 17, 2025 • edited Loading

Choose a reason for hiding this comment

Stevengre commented Mar 17, 2025 • edited Loading

Performances

Stevengre commented Feb 27, 2025 •

edited

Loading

Stevengre commented Mar 7, 2025 •

edited

Loading

Stevengre Mar 17, 2025 •

edited

Loading

Stevengre commented Mar 17, 2025 •

edited

Loading