Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Add symbolic bytes cheatcode #254

Merged
merged 84 commits into from
Feb 22, 2024
Merged

Add symbolic bytes cheatcode #254

merged 84 commits into from
Feb 22, 2024

Conversation

nwatson22
Copy link
Member

@nwatson22 nwatson22 commented Dec 19, 2023 •
edited by PetarMax
Loading

  • Cheatcode for generating a symbolic byte array, including limited support for a symbolic length as well
  • New tests for generating symbolic byte array with this cheatcode, checking the length, passing it to a function which overwrites some parts of it, and generating a symbolic byte array with symbolic length.

Blocked on this KEVM PR.
Blocked on this KEVM PR.

N.B. The FreshBytesTest.test_symbolic_bytes_2 does not pass yet (but should eventually) due to high complexity of the associated symbolic reasoning. This, however, is orthogonal to the correct generation of symbolic bytes, which is tested by the other two tests.

@nwatson22 nwatson22 self-assigned this Dec 19, 2023
@nwatson22 nwatson22 linked an issue Dec 19, 2023 that may be closed by this pull request
Add cheatcode for symbolic bytes #203
Closed
@nwatson22 nwatson22 added the enhancement New feature or request label Dec 19, 2023
PetarMax
PetarMax reviewed Jan 10, 2024
View reviewed changes
src/kontrol/kdist/cheatcodes.md Outdated Show resolved Hide resolved
lemmas.k Outdated Show resolved Hide resolved
src/kontrol/kdist/cheatcodes.md Outdated Show resolved Hide resolved
@nwatson22 nwatson22 mentioned this pull request Jan 10, 2024
Merged
@mds1 mds1 mentioned this pull request Jan 12, 2024
Merged
@JuanCoRo JuanCoRo mentioned this pull request Jan 12, 2024
Closed
@PetarMax PetarMax mentioned this pull request Feb 21, 2024
Merged
@PetarMax PetarMax merged commit 370fc04 into master Feb 22, 2024
11 checks passed
@PetarMax PetarMax deleted the noah/symbolic-bytes branch February 22, 2024 17:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@PetarMax PetarMax PetarMax approved these changes

Assignees

@nwatson22 nwatson22

Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Add cheatcode for symbolic bytes
2 participants
@nwatson22 @PetarMax