Skip to content

Add forge-symbolic-tests bug suite#1074

Merged
msooseth merged 9 commits into
mainfrom
add-symbolic-bug-tests
Jul 6, 2026
Merged

Add forge-symbolic-tests bug suite#1074
msooseth merged 9 commits into
mainfrom
add-symbolic-bug-tests

Conversation

@msooseth

Copy link
Copy Markdown
Collaborator

Description

Forge now has a symbolic execution engine, and it is promoted as being able to find these bugs. hevm can find them, too, so let's vendor them in as a test suite.

Checklist

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

@msooseth msooseth requested a review from gustavo-grieco June 18, 2026 15:01
@msooseth msooseth force-pushed the add-symbolic-bug-tests branch from f102c1a to 8212a38 Compare June 22, 2026 09:38
@msooseth msooseth marked this pull request as ready for review June 22, 2026 09:38
Comment thread forge-symbolic-tests/README.md Outdated
- `symbolic-bug-suite/` — the vendored submodule (`src/NN_*.sol` reproducers and
`test/NN_*.t.sol` symbolic invariants).
- The Haskell runner lives at [`../test/SymbolicTestSuite.hs`](../test/SymbolicTestSuite.hs)
and is registered as the `symbolic-test` cabal test suite.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we maybe call it forge-symbolic-test?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, good point. Fixed now. What do you think of it in general? I think it's kinda OK and not too noisy addition?

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I think it's fine!

msooseth added 8 commits July 6, 2026 11:37
Vendor grandizzy/symbolic-bug-suite as a git submodule, add minimal hevm runner

The new `symbolic-test` cabal suite to run them and check for FAIL +
validation. Run it as as part of CI.

Update

Cleanup

Cleanup
@msooseth msooseth merged commit ade06ec into main Jul 6, 2026
10 checks passed
@msooseth msooseth deleted the add-symbolic-bug-tests branch July 6, 2026 13:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants