Skip to content

Navigation Menu

Explore
By company size
By use case
By industry
View all solutions
Topics
- AI
- DevOps
- Security
- Software Development
- View all
Explore
- GitHub Sponsors
  Fund open source developers
- The ReadME Project
  GitHub community articles
Repositories
- Enterprise platform
  AI-powered developer platform
Available add-ons
Pricing

Search code, repositories, users, issues, pull requests...

Search

Clear

Search syntax tips

Provide feedback

We read every piece of feedback, and take your input very seriously.

Include my email address so I can be contacted

Saved searches

Use saved searches to filter your results more quickly

Name

Query

To see all available qualifiers, see our documentation.

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

runtimeverification / evm-semantics Public

Notifications You must be signed in to change notification settings
Fork 152
Star 521

Code
Issues 68
Pull requests 11
Actions
Projects 1
Wiki
Security
Insights

Additional navigation options

Code
Issues
Pull requests
Actions
Projects
Wiki
Security
Insights

Integrate summaries of opcode automatically into the evm semantics#2710

Open

Stevengre wants to merge 130 commits intomasterruntimeverification/evm-semantics:masterfrom jh/summary-integrationruntimeverification/evm-semantics:jh/summary-integrationCopy head branch name to clipboard

Conversation Commits130 (130)Checks Files changed

Commits

Commits on Mar 14, 2025

provide KEVMSummarizer to sammarize rules for all the instruction rule. This commit includes build_spec and explore to constrcut a specification for all instructions and explore it.
Stevengre
committed
solve error call for legacy_explore and incorrect name for #next[_]
Stevengre
committed
kevm-pyk/: get code passing basic type checking issues

ehildenb
authored and
Stevengre
committed
qupdate poetry to 2.0.0
Stevengre
committed
add new command summarize for summarizing evm instructions
Stevengre
committed
don't use summarize but kevm summarize instead.
Stevengre
committed
provide spec with initial and target node that are not terminal according to KEVMSemantics
Stevengre
committed
make format & make check
Stevengre
committed
print nodes and add summarize function to generate optimized rules for instructions
Stevengre
committed
make format & make check
Stevengre
committed
add ignore
Stevengre
committed
allow_symbolic_program
Stevengre
committed
summarize instructions one by one
Stevengre
committed
summarize STOP
Stevengre
committed
solve the unhook problem during summarizing ADD.
Stevengre
committed
summarize all the evm opcode using KEVMSummarizer.batch_summarize. Leave the verification log nohup.out to track.
Stevengre
committed
fix the summarization for STOP.
Stevengre
committed
update the status of STOP.
Stevengre
committed
don't use optimizations during summarization
Stevengre
committed
summarize ADD successfully with new simplification rules, wrapper rules, and concrete WordStack
Stevengre
committed
summarized MUL
Stevengre
committed
summarized SUB
Stevengre
committed
summarized DIV
Stevengre
committed
summarized SDIV
Stevengre
committed
summarized MOD
Stevengre
committed
summarized SMOD
Stevengre
committed
summarized ADDMOD.
Stevengre
committed
summarized MULMOD
Stevengre
committed
try to summarize all the opcode, under checking.
Stevengre
committed
check all the finished summarization.
Stevengre
committed
update the summarization result
Stevengre
committed
update the summarization statuses.
Stevengre
committed
fix the summarization of EXP
Stevengre
committed
fix the summarization of ADDRESS
Stevengre
committed
fix summarization of
Stevengre
committed
fixed the summarization of ORIGIN and EXTCODECOPY
Stevengre
committed
fix summarization of CALLER
Stevengre
committed
fix summarization of EXTCODESIZE
Stevengre
committed
fix the summarization of RETURNDATASIZE
Stevengre
committed
fix the summarization of MLOAD
Stevengre
committed
fix summarization of MLOAD
Stevengre
committed
fix the summarization of MSTORE8
Stevengre
committed
fix the summarization of
Stevengre
committed
fix the summarization of JUMPI
Stevengre
committed
fix the summarization of PUSH
Stevengre
committed
fix the summarization of LOG.
Stevengre
committed
backup all the useful informations in the PR before preparing the merge
Stevengre
committed
delete the logs
Stevengre
committed
delete all the proof and summary files
Stevengre
committed
ignore the proofs and summaries.
Stevengre
committed
back up to keep my thinking of debuging
Stevengre
committed
finish the test process on STOP
Stevengre
committed
simlify the implementation
Stevengre
committed
comment rule generation validation for faster check
Stevengre
committed
fix make format & check
Stevengre
committed
poetry lock 2.0.1
Stevengre
committed
delete analysis codes in exec_summarize
Stevengre
committed
make format
Stevengre
committed
recover the definition and create a new target for summarization
Stevengre
committed
delete useless lemma comments.
Stevengre
committed
test all the passed opcodes
Stevengre
committed
fix poetry.lock
Stevengre
committed
update summarization results using nohup.out
Stevengre
committed
simplify the implementation & fix the summarization for BALANCE
Stevengre
committed
try to fix all ACCOUNT_QUERIES_OPCODES but failed. fix SELFBALANCE success.
Stevengre
committed
make format & make check
Stevengre
committed
delete log file
Stevengre
committed
poetry update
Stevengre
committed
keep edsl unchanged
Stevengre
committed
Revert submodule ethereum-tests to c30599
Stevengre
committed
more detailed help info for summarize command.

Stevengre
and
anvacaru
committed
reduce duplification for semantics
Stevengre
committed
delete unecessary import
Stevengre
committed
Apply suggestions from code review

Stevengre
and
anvacaru
committed
upstream word_stack function to KEVM
Stevengre
committed
provide detailed comments for exec_summarize
Stevengre
committed
Consolidate EDSL-SUM module into edsl.md
Stevengre
committed
Remove unnecessary serialization import from EVM module
Stevengre
committed
Rename word_stack method to wordstack in KEVM class
Stevengre
committed
Add frozendict for immutable dictionary types in summarizer
Stevengre
committed
Remove commented-out 'ALL' key from OPCODES_SUMMARY_STATUS
Stevengre
committed
Enhance accounts_cell function documentation
Stevengre
committed
Prepare build_stack_underflow_spec method for implementation
Stevengre
committed
Improve documentation for build_spec method in KEVMSummarizer
Stevengre
committed
Simplify default argument handling in build_spec method
Stevengre
committed
Refactor KEVM and summarizer methods to use static helper methods
Stevengre
committed
Remove trailing whitespace in KEVM and summarizer modules
Stevengre
committed
Update test-summarize workflow and opcode summary statuses
Stevengre
committed
Update Poetry lock file dependencies and version constraints
Stevengre
committed
Update test-pr workflow to initialize specific submodules
Stevengre
committed
delete simplification rule
Stevengre
committed
Add summarization simplification lemmas and update imports
Stevengre
committed
Remove test-summarize job from GitHub Actions workflow
Stevengre
committed
Add Summarization test suite to GitHub Actions workflow
Stevengre
committed
Increase Summarization test suite timeout to 720 seconds
Stevengre
committed
Adjust Summarization test suite configuration
Stevengre
committed
Increase Summarization test suite timeout to 240 seconds
Stevengre
committed
Increase Summarization test suite timeout to 360 seconds
Stevengre
committed
use summaries to keep all the opcode summaries
Stevengre
committed
Enhance summarize command with opcode-specific and clear options
Stevengre
committed
Remove the KCFG.
Stevengre
committed
Modify summary file generation to include EVM imports and requires
Stevengre
committed
Refactor summary generation and module structure
Stevengre
committed
Modify batch summarization to process passed opcodes instead of unpassed
Stevengre
committed
Add comprehensive EVM opcode summary imports to summary.k
Stevengre
committed
Refactor summary file generation to simplify and clean up specifications
Stevengre
committed
new way to remove inf gas
Stevengre
committed
remove_dash_from_var
Stevengre
committed
Simplify summary specification files by removing unnecessary account constraints
Stevengre
committed
Generate summary specification files for multiple EVM opcodes
Stevengre
committed
Enhance summary specification file generation for balance opcode
Stevengre
committed
Refine summarizer and workflow configuration
Stevengre
committed
Update poetry.lock with platform-specific dependency constraints
Stevengre
committed
Update poetry.lock with Hypothesis and setuptools version bumps
Stevengre
committed
bring back the modification in the master branch
Stevengre
committed
Simplify summary-balance account ID regex transformation
Stevengre
committed
Add new target options for KEVM CLI summary targets
Stevengre
committed
Improve CLI target argument formatting
Stevengre
committed
update expected file with new module name
Stevengre
committed
provide a basic way to verify the summaries
Stevengre
committed
change the require to pass the verification
Stevengre
committed
try to add gas gaurd automatically
Stevengre
committed
try to provide gas guard automatically
Stevengre
committed
solved out of gas problem for most opcode summaries
Stevengre
committed
fix summaries for the summaries of opcode like return
Stevengre
committed
make test-prove-summaries passed
Stevengre
committed
[to delete] add concrete execution result for both normal semantics and summaried one.
Stevengre
committed
Update test timeout and dependencies in poetry.lock
Stevengre
committed
Remove references to 'summary-exp-2-spec.k' and 'SUMMARY-EXP-2-SPEC' from summarizer and summary.k files to address potential issues with log2 calculations.
Stevengre
committed
[to delete] update the concrete execution result of the summary rules.
Stevengre
committed

Footer

© 2025 GitHub, Inc.

Footer navigation

Terms
Privacy
Security
Status
Docs
Contact

You can’t perform that action at this time.