You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This section analyzes the development of an EVM Opcode Summarization System by our team from March 6 to April 22, 2025, within the evm-semantics project for the zkEVM formal verification project. This system provides critical infrastructure for EVM formal verification initiative.
Key Deliverables
We successfully delivered a complete EVM opcode summarization system from the ground up, including:
Core Architecture: Designed and implemented a comprehensive KEVMSummarizer framework supporting automated summarization of 68 major EVM opcodes
Complete Coverage: Created 7,225 lines of standardized summary rules for all major EVM opcode categories (arithmetic, logical, storage, control flow, system calls, etc.)
Engineering Excellence: Established complete CLI tools, automated testing frameworks, and CI/CD integration, ensuring code quality and system stability
Performance Optimization: Achieved significant efficiency improvements through multiple optimization rounds, eliminating 871 lines of redundant code
Business Value
The system provides critical technical infrastructure for the EVM ecosystem:
Equivalence Verification Support: Provides unified opcode summary specifications for equivalence verification between different EVM implementations, such as Nethermind's EvmYul and Runtime Verification's KEVM
Ecosystem Impact: Lays an important foundation for the entire EVM formal verification ecosystem, supporting more efficient symbolic execution and concrete execution, while providing optimization potential for downstream tools based on EVM formal semantics (such as Kontrol)
Technical Highlights
Modular Design: Independent summary files for each opcode, supporting incremental updates and maintenance
End-to-End Integration: Complete solution from core algorithms to CLI tools and testing frameworks
High Code Quality: Unified naming conventions, standardized labeling systems, and rigorous code review processes
Performance-Oriented: Efficient batch processing capabilities through deep optimization and algorithmic improvements
Project Statistics
Total Commits: 10 commits
Time Span: March 6 - April 22, 2025 (approximately 1.5 months)
Commit Frequency: Average of 6.7 commits per month
Pull Requests: 10 (100% of commits have corresponding PRs)
1. EVM Opcode Summarization System (Core Contribution)
Our primary contribution focuses on creating and refining the summarization system for EVM opcodes, providing infrastructure for EVM equivalence verification:
Provide core framework implementation for KEVMSummarizer to summarize all instruction rules. This is the foundational commit for the entire summarization system, introducing the complete KEVMSummarizer class and related infrastructure.
Modified Files
1. kevm-pyk/src/kevm_pyk/cli.py
Changes: Added CLI support for summarize command
Specific Updates:
Added 'summarize': ProveOptions(args) to generate_options function
Added summarize command option handling in get_option_string_destination and get_argument_type_setter
Added summarize subcommand parser in _create_argument_parser with related parameter groups
2. kevm-pyk/src/kevm_pyk/main.py
Changes: Added exec_summarize function and imported batch_summarize
Specific Updates:
Imported from kevm_pyk.summarizer import batch_summarize
Added exec_summarize(options: ProveOptions) function, currently calling batch_summarize()
3. kevm-pyk/src/kevm_pyk/kevm.py
Changes: Added static helper methods to KEVM class supporting summarization functionality
Specific Updates:
Added account_cell_in_keys static method for account cell mapping key checks
Added wordstack static method for constructing WordStack structures
Added next_opcode and end_basic_block static methods for opcode processing
These methods provide necessary K expression construction tools for summarization
4. kevm-pyk/src/kevm_pyk/summarizer.py (New File)
Changes: Created complete KEVMSummarizer class with 680 lines of code
Specific Updates:
Defined OPCODES constant dictionary containing K expression mappings for all EVM opcodes
Defined OPCODES_SUMMARY_STATUS dictionary tracking summarization status of each opcode
Implemented KEVMSummarizer class with core methods:
build_spec(): Build symbolic execution specification for opcodes
summarize(): Summarize individual opcodes
batch_summarize(): Batch process all opcodes
accounts_cell(): Create account cell mappings
show_proof(): Display proof results
Used frozendict for immutable data structures, improving type safety and performance
Changes: Added multiple wrapper functions supporting symbolic execution in summarization
Specific Updates:
Added verifyKZGProofWrapper and Sha256rawWrapper
Added cryptographic function wrappers like BN128AddWrapper, BN128MulWrapper
Added Blake2CompressWrapper and isValidPointWrapper
These wrappers provide symbolic execution-friendly interfaces while maintaining concrete execution functionality
8. kevm-pyk/src/tests/integration/test_summarize.py (New File)
Changes: Created integration tests for summarization functionality
Specific Updates:
Implemented parameterized tests for all opcodes
Tests verify correctness of summarization results:
Confirm no stuck, failed, or bounded nodes
Verify initial node has only one successor
Check edge termination and coverage
Includes proof correctness verification logic (currently commented out)
9. Other Configuration Files
kevm-pyk/poetry.lock and kevm-pyk/pyproject.toml: Added frozendict dependency
kevm-pyk/.gitignore: Added ignores for proofs and summaries directories
Makefile: Added test-summarize target
.github/workflows/test-pr.yml: Added Summarization test job with timeout and parallel execution configuration
Functional Improvements
1. Core Architecture Establishment
Established complete EVM opcode summarization architecture
Provided complete conversion pipeline from symbolic execution to summary rules
Supports summarization of 68 major EVM opcodes
2. Modular Design
Achieved modularization of summarization functionality through EDSL module refactoring
Each opcode's summarization process is independent, improving maintainability
Supports both batch processing and individual processing modes
3. Performance Optimization
Used frozendict for immutable data structures, improving performance
Added specialized simplification rules, reducing proof time
Optimized symbolic execution process through wrapper functions
4. Testing and Verification
Provided complete integration testing framework
Supports automated correctness verification
Integrated CI/CD pipeline ensuring code quality
5. CLI Integration
Provided user-friendly command-line interface
Supports operation through kevm summarize command
Integrated with existing CLI parameter system
6. Formal Verification Support
Provided infrastructure for EVM equivalence verification
Supports generation of summary rules meeting formal verification requirements
Provided interfaces with other verification tools
This commit builds the foundation for the entire summarization system, providing a solid base for subsequent optimization and expansion. It not only implements core functionality but also establishes complete development, testing, and deployment processes.
Reduce KEVMSummarizer's max_depth parameter from the default value to 1 to improve proof exploration efficiency. This is a performance optimization measure aimed at reducing computational complexity in the summarization process.
Modified Files
1. .github/workflows/test-pr.yml
Changes: Updated CI configuration to adapt to new depth settings
Specific Updates: Adjusted timeout configuration for Summarization tests
2. kevm-pyk/src/kevm_pyk/summarizer.py
Changes: Modified max_depth parameter in KEVMSummarizer
Specific Updates: Changed exploration depth from default value to 1, reducing symbolic execution search space
Use the upstream llvm_interpret function, replacing the custom implementation to improve code consistency and maintainability. This is a technical debt cleanup commit aimed at staying synchronized with the upstream K framework.
Refactor the summarize command and options, improving code structure in cli.py and main.py. This commit focuses on improving user experience and code organization.
Simplify summary rules for DUP, SWAP, and LOG operations. This commit focuses on optimizing processing logic for specific opcodes, improving summarization efficiency and accuracy.
Add gas cost summarization support for all supported opcodes. This commit extends the summarization system's functionality to accurately calculate and summarize gas consumption for each opcode.
Integrate opcode semantic summarization functionality. This is a major functional integration commit that formally integrates all opcode summary files into the system and creates 68 independent opcode summary files.
Optimize summary rules by removing redundant code and simplifying logic to improve system performance. This commit focuses on code cleanup and performance optimization.
Use the _XXX naming convention for unused variables in summary rules. This commit focuses on code standardization, improving code quality and maintainability.
Modified Files
1. 71 Opcode Summary Files
Changes: Renamed all unused variables
Specific Updates:
Renamed unused variables to _XXX format
Unified variable naming conventions
Improved code readability
Eliminated compiler warnings
2. kevm-pyk/src/kevm_pyk/summarizer.py
Changes: Updated variable naming-related logic
Specific Updates:
Adapted to new variable naming conventions
Updated variable processing logic
Improved code generation quality
Functional Improvements
1. Code Standardization
Established unified variable naming conventions
Improved code professionalism
Reduced potential confusion
2. Maintainability
Clearly identified unused variables
Simplified code understanding and maintenance
Improved code review efficiency
3. Quality Enhancement
Eliminated compiler warnings
Improved overall code quality
Enhanced code consistency
Technical Architecture Analysis
Summarization System Architecture
We designed a complete opcode summarization system as follows:
kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/
├── summaries.k (main entry)
├── {opcode}-summary.k (68 opcode files)
└── Each file contains:
├── Formal specification of the opcode
├── Gas cost calculations
├── Preconditions and postconditions
└── State transition rules
Implementation Features
Modular Design: Independent summary files for each opcode
Standardized Templates: Unified format and naming conventions
Completeness: Coverage of all major EVM opcodes
Extensibility: Easy to add new opcode support
Quality Assurance
Test Coverage: Added integration tests
CI Integration: Integrated testing in GitHub Actions
Code Review: All changes went through PR review
Impact Assessment
1. Project Impact
Functional Completeness: Provided complete opcode summarization support for EVM semantics
Maintainability: Modular design makes maintenance and updates easier
Performance Optimization: Reduced proof time through summary rules
2. Technical Contributions
Formal Verification: Provided formal specifications for EVM opcodes
Standardization: Established standard format for opcode summarization
3. Ecosystem Impact
EVM Equivalence Verification: Provides foundation for equivalence verification between Nethermind's EvmYul and Runtime Verification's KEVM
Downstream Tool Optimization: Enhanced verification efficiency of tools based on EVM formal semantics (such as kontrol)
Symbolic Execution Enhancement: Supports more efficient symbolic execution and concrete execution
Cross-Project Collaboration: Promotes consistency verification between different EVM implementations
Development Process
1. Development Workflow
PR-Driven: 100% of commits have corresponding PRs
Incremental Development: Progressive development from basic framework to complete implementation
Continuous Optimization: Ongoing improvement and refinement of existing functionality
2. Code Review
All major changes underwent PR review
Focus on code quality and consistency
Timely response and issue resolution
Comprehensive Summary
These 10 commits demonstrate the complete development process of an EVM opcode summarization system. Our contributions to the evm-semantics project primarily focus on designing and implementing the EVM opcode summarization system, providing important infrastructure for EVM ecosystem equivalence verification and formal verification.
Development Journey Analysis
Foundation Architecture (Commit 1): Established complete KEVMSummarizer framework
Performance Optimization (Commits 2, 3, 8): Improved performance through parameter adjustment, upstream function usage, and rule optimization
User Experience Improvements (Commits 4, 5): Refactored CLI and simplified specific opcode handling
Feature Expansion (Commits 6, 7): Added gas cost support and complete opcode integration
Systematic Thinking: Complete consideration from overall architecture to specific implementation
High-Quality Code: Focus on code standards and best practices
Continuous Improvement: Ongoing optimization and refinement of existing functionality
Team Collaboration: Good PR workflow and code review participation
Core Value
These contributions not only significantly enhanced the functional completeness and toolchain capabilities of the evm-semantics project, but more importantly, provided a unified opcode summarization framework for the EVM ecosystem. This framework supports:
Equivalence verification between different EVM implementations
Optimization of execution based on formal semantics
Efficiency enhancement of downstream formal verification tools
Cross-project technical standardization
The entire development process demonstrates software engineering best practices: from architectural design to implementation, from optimization to standardization, ultimately forming a complete, efficient, and maintainable EVM opcode summarization system. This work lays an important foundation for the EVM formal verification ecosystem, promoting consistency and interoperability between different EVM implementations.
Executive Summary
This section analyzes the development of an EVM Opcode Summarization System by our team from March 6 to April 22, 2025, within the evm-semantics project for the zkEVM formal verification project. This system provides critical infrastructure for EVM formal verification initiative.
Key Deliverables
We successfully delivered a complete EVM opcode summarization system from the ground up, including:
KEVMSummarizerframework supporting automated summarization of 68 major EVM opcodesBusiness Value
The system provides critical technical infrastructure for the EVM ecosystem:
Equivalence Verification Support: Provides unified opcode summary specifications for equivalence verification between different EVM implementations, such as Nethermind's EvmYul and Runtime Verification's KEVM
Standardization Contribution: Establishes industry-standard formats for EVM opcode summarization, promoting cross-project technical interoperability
Ecosystem Impact: Lays an important foundation for the entire EVM formal verification ecosystem, supporting more efficient symbolic execution and concrete execution, while providing optimization potential for downstream tools based on EVM formal semantics (such as Kontrol)
Technical Highlights
Project Statistics
Development Timeline
2025 Milestones
KEVMSummarizerto sammarize rules for all the instruction rules #2676) - Major feature additionllvm_interpretfunction #2723)DUP,SWAP, andLOG. #2726)_XXXnaming convention for unused variables (Use_XXXfor unused variables for summary rules. #2744)Major Contribution Areas Overview
1. EVM Opcode Summarization System (Core Contribution)
Our primary contribution focuses on creating and refining the summarization system for EVM opcodes, providing infrastructure for EVM equivalence verification:
Created Summary Files (2025-04-02, #2728):
{opcode}-summary.kMajor Opcode Categories:
2. Code Quality Improvements
_XXXnaming convention for unused variables3. System Architecture Improvements
4. Technical Stack Integration
Code Change Statistics
File Change Patterns
_XXXfor unused variables for summary rules. #2744) - Modified 71 files, primarily variable renamingPrimary File Types
.k): Opcode summarization specifications.py): Summarizer implementation and CLI.md): Documentation and specificationsDetailed Commit Analysis
Commit 1: a4d59d3 (2025-03-06)
Purpose
Provide core framework implementation for
KEVMSummarizerto summarize all instruction rules. This is the foundational commit for the entire summarization system, introducing the complete KEVMSummarizer class and related infrastructure.Modified Files
1. kevm-pyk/src/kevm_pyk/cli.py
summarizecommand'summarize': ProveOptions(args)togenerate_optionsfunctionget_option_string_destinationandget_argument_type_settersummarizesubcommand parser in_create_argument_parserwith related parameter groups2. kevm-pyk/src/kevm_pyk/main.py
exec_summarizefunction and importedbatch_summarizefrom kevm_pyk.summarizer import batch_summarizeexec_summarize(options: ProveOptions)function, currently callingbatch_summarize()3. kevm-pyk/src/kevm_pyk/kevm.py
account_cell_in_keysstatic method for account cell mapping key checkswordstackstatic method for constructing WordStack structuresnext_opcodeandend_basic_blockstatic methods for opcode processing4. kevm-pyk/src/kevm_pyk/summarizer.py (New File)
OPCODESconstant dictionary containing K expression mappings for all EVM opcodesOPCODES_SUMMARY_STATUSdictionary tracking summarization status of each opcodeKEVMSummarizerclass with core methods:build_spec(): Build symbolic execution specification for opcodessummarize(): Summarize individual opcodesbatch_summarize(): Batch process all opcodesaccounts_cell(): Create account cell mappingsshow_proof(): Display proof resultsfrozendictfor immutable data structures, improving type safety and performance5. kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md
EDSL-SUMmodule specifically for summarizationEDSLmodule intoEDSL-PUREandEDSLlemmas/lemmas.kandlemmas/summarization-simplification.k6. kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summarization-simplification.k (New File)
log2Intfunction:#Ceil ( log2Int ( X:Int ) ) => { true #Equals X >Int 0 }#newAddrfunction:#Ceil(#newAddr(@ACCT, @NONCE)) => #Ceil(@ACCT) #And #Ceil(@NONCE)7. kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
verifyKZGProofWrapperandSha256rawWrapperBN128AddWrapper,BN128MulWrapperBlake2CompressWrapperandisValidPointWrapper8. kevm-pyk/src/tests/integration/test_summarize.py (New File)
9. Other Configuration Files
frozendictdependencytest-summarizetargetFunctional Improvements
1. Core Architecture Establishment
2. Modular Design
3. Performance Optimization
frozendictfor immutable data structures, improving performance4. Testing and Verification
5. CLI Integration
kevm summarizecommand6. Formal Verification Support
This commit builds the foundation for the entire summarization system, providing a solid base for subsequent optimization and expansion. It not only implements core functionality but also establishes complete development, testing, and deployment processes.
Commit 2: c7f7099 (2025-03-12)
Purpose
Reduce KEVMSummarizer's max_depth parameter from the default value to 1 to improve proof exploration efficiency. This is a performance optimization measure aimed at reducing computational complexity in the summarization process.
Modified Files
1. .github/workflows/test-pr.yml
2. kevm-pyk/src/kevm_pyk/summarizer.py
3. kevm-pyk/src/tests/integration/test_summarize.py
Functional Improvements
1. Performance Optimization
2. Resource Management
3. Stability Enhancement
Commit 3: a225bcb (2025-03-17)
Purpose
Use the upstream
llvm_interpretfunction, replacing the custom implementation to improve code consistency and maintainability. This is a technical debt cleanup commit aimed at staying synchronized with the upstream K framework.Modified Files
1. kevm-pyk/src/kevm_pyk/interpreter.py
llvm_interpretfunctionFunctional Improvements
1. Code Consistency
2. Maintainability
3. Stability
Commit 4: 710742c (2025-03-19)
Purpose
Refactor the summarize command and options, improving code structure in cli.py and main.py. This commit focuses on improving user experience and code organization.
Modified Files
1. kevm-pyk/src/kevm_pyk/main.py
2. kevm-pyk/src/kevm_pyk/cli.py
3. kevm-pyk/src/kevm_pyk/summarizer.py
Functional Improvements
1. User Experience Improvements
2. Code Quality
3. Maintainability
Commit 5: aeef1bd (2025-03-20)
Purpose
Simplify summary rules for DUP, SWAP, and LOG operations. This commit focuses on optimizing processing logic for specific opcodes, improving summarization efficiency and accuracy.
Modified Files
1. kevm-pyk/src/kevm_pyk/kevm.py
2. kevm-pyk/src/kevm_pyk/summarizer.py
3. kevm-pyk/src/tests/integration/test_summarize.py
Functional Improvements
1. Specific Opcode Optimization
2. Algorithm Improvements
3. Performance Enhancement
Commit 6: 4709f66 (2025-03-24)
Purpose
Add gas cost summarization support for all supported opcodes. This commit extends the summarization system's functionality to accurately calculate and summarize gas consumption for each opcode.
Modified Files
1. kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
2. kevm-pyk/src/kevm_pyk/summarizer.py
Functional Improvements
1. Completeness
2. Precision
3. Utility
Commit 7: bf5a247 (2025-04-02)
Purpose
Integrate opcode semantic summarization functionality. This is a major functional integration commit that formally integrates all opcode summary files into the system and creates 68 independent opcode summary files.
Modified Files
1. 68 Opcode Summary Files (New)
kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/{opcode}-summary.k2. kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summaries.k (New)
3. kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
4. kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md
5. kevm-pyk/src/kevm_pyk/kdist/plugin.py
6. kevm-pyk/src/kevm_pyk/cli.py
7. kevm-pyk/src/kevm_pyk/summarizer.py
8. kevm-pyk/src/tests/integration/test_prove.py
9. Configuration File Updates
Functional Improvements
1. Complete Opcode Support
2. Modular Architecture
3. Integrated Verification
4. Performance Optimization
5. Standardization
Commit 8: 13cfef5 (2025-04-07)
Purpose
Optimize summary rules by removing redundant code and simplifying logic to improve system performance. This commit focuses on code cleanup and performance optimization.
Modified Files
1. Multiple Opcode Summary File Optimizations
2. kevm-pyk/src/kevm_pyk/summarizer.py
Functional Improvements
1. Code Streamlining
2. Performance Enhancement
3. Consistency Improvements
Commit 9: db7d25e (2025-04-10)
Purpose
Update opcode summarization to standardize labels and improve clarity. This commit focuses on improving code readability and maintainability.
Modified Files
1. 71 Opcode Summary Files
2. kevm-pyk/src/kevm_pyk/summarizer.py
Functional Improvements
1. Standardization
2. Clarity Enhancement
3. Systematization
Commit 10: 1d02e19 (2025-04-22)
Purpose
Use the
_XXXnaming convention for unused variables in summary rules. This commit focuses on code standardization, improving code quality and maintainability.Modified Files
1. 71 Opcode Summary Files
_XXXformat2. kevm-pyk/src/kevm_pyk/summarizer.py
Functional Improvements
1. Code Standardization
2. Maintainability
3. Quality Enhancement
Technical Architecture Analysis
Summarization System Architecture
We designed a complete opcode summarization system as follows:
Implementation Features
Quality Assurance
Impact Assessment
1. Project Impact
2. Technical Contributions
3. Ecosystem Impact
Development Process
1. Development Workflow
2. Code Review
Comprehensive Summary
These 10 commits demonstrate the complete development process of an EVM opcode summarization system. Our contributions to the evm-semantics project primarily focus on designing and implementing the EVM opcode summarization system, providing important infrastructure for EVM ecosystem equivalence verification and formal verification.
Development Journey Analysis
Technical Characteristics
Our work characteristics include:
Core Value
These contributions not only significantly enhanced the functional completeness and toolchain capabilities of the evm-semantics project, but more importantly, provided a unified opcode summarization framework for the EVM ecosystem. This framework supports:
The entire development process demonstrates software engineering best practices: from architectural design to implementation, from optimization to standardization, ultimately forming a complete, efficient, and maintainable EVM opcode summarization system. This work lays an important foundation for the EVM formal verification ecosystem, promoting consistency and interoperability between different EVM implementations.