Skip to content

Gas simplification for Csstore, named rules #1560

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.

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

Merged
merged 13 commits into from
Feb 13, 2023
Merged

Gas simplification for Csstore, named rules #1560

merged 13 commits into from
Feb 13, 2023

Conversation

ehildenb
Copy link
Member

@ehildenb ehildenb commented Feb 12, 2023

This PR pulls out several components of which can get merged standalone: #1538

  • Some simple gas simplification lemmas for Csstore that is fairly simple (and failing tests). These missing simplifications were causing lots of unnecessary branches when doing foundry proofs without infinite gas.
  • Corrections to logging level in kevm-pyk.
  • Correctly pass through the --debug option from bin/kevm to kevm-pyk.
  • Name various rules of interest in semantics for making automated break points.
  • A small fix to how the single-byte 00 is produced for Foundry proofs.

This change makes it so that none of the proofs in the KEVM foundry test-suite are breaking every opcode due to out-of-gas errors (which makes them significantly faster). Now all the basic blocks that are found in that proof suite are actually due to control-flow branches, and reaching the 1000 step max-depth limit.

@ehildenb ehildenb marked this pull request as ready for review February 12, 2023 22:42
@rv-jenkins rv-jenkins merged commit a978756 into master Feb 13, 2023
@rv-jenkins rv-jenkins deleted the gas-lemma branch February 13, 2023 19:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants