Skip to content

Collect keccaks during concrete running and inject them into the Props during query #806

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
Merged
msooseth merged 1 commit into from
Jul 30, 2025
Merged

Collect keccaks during concrete running and inject them into the Props during query #806

msooseth merged 1 commit into from
Jul 30, 2025

Conversation

@msooseth
Copy link
Collaborator

@msooseth msooseth commented Jul 22, 2025 •
edited
Loading

Description

Fixes #804:

$ cabal run -f devel exe:hevm -- test --match '.*bad_addr.*' --root tmp --debug --solver bitwuzla --smtdebug  --trace --max-depth 32 --max-iterations 20 --num-solvers 2  --loop-detection-heuristic Naive
-> debug of func: prove_bad_addr Failure at the end of expr: Revert (ConcreteBuf "")
symRun -- (cex,warnings,unexpectedAllRevert): (True,False,False)
   [FAIL] prove_bad_addr
   Counterexample:
     calldata: prove_bad_addr(0x0000000000000000000000000000000000001234)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

The following changes were also made:

  • Cleaned up clitest.hs -- no more warnings
  • Added test to clitest.hs -- we can now run forge tests in cli mode, too

Can only be merged after #809 has been merged.

Checklist

  • tested locally
  • added automated tests
  • updated the docs
  • updated the changelog

@msooseth msooseth force-pushed the fix-missing-keccak-assertions branch 6 times, most recently from 268bb3d to dc77101 Compare July 28, 2025 15:58
@msooseth msooseth marked this pull request as ready for review July 28, 2025 15:59
@msooseth msooseth requested a review from blishko July 28, 2025 15:59
@msooseth msooseth force-pushed the fix-missing-keccak-assertions branch 3 times, most recently from 96c7474 to be503b3 Compare July 30, 2025 09:31
@msooseth msooseth force-pushed the fix-missing-keccak-assertions branch from be503b3 to c34d4d6 Compare July 30, 2025 10:52
@msooseth msooseth merged commit 1ee94f7 into main Jul 30, 2025
8 of 9 checks passed
@msooseth msooseth deleted the fix-missing-keccak-assertions branch July 30, 2025 11:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@blishko blishko Awaiting requested review from blishko

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Bug in keccak computations

2 participants

@msooseth