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 Halmos support #5034

Merged
merged 30 commits into from May 23, 2024
Merged

Add Halmos support #5034

merged 30 commits into from May 23, 2024
+197 −38

Conversation

ernestognw
Copy link
Member

@ernestognw ernestognw commented May 8, 2024 •
edited

So far we've been maintaining our Formal Verification workflows with Certora. Though, Halmos has got lots of improvements lately. This PR is to test it out in our current fuzz tests. Note that our rule of thumb so far has been to formally verify when possible and fuzz otherwise, so it's expected that some of theses tests won't be working.

Currently, we added a decent amount of extra Formal Verification tests that are working good and really fast within our regular checks pipeline.

An important note from the Halmos team is that they don't recommend removing fuzz tests even if they're already formally verified. This is because the bounded model in which both Certora and Halmos only test for fixed size arrays.

PR Checklist

  • Tests
  • Documentation
  • Changeset entry (run npx changeset add)

@changeset-bot changeset-bot
Copy link

changeset-bot bot commented May 8, 2024 •
edited

⚠️ No Changeset found

Latest commit: 8366a6d

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@ernestognw ernestognw marked this pull request as ready for review May 13, 2024 19:35
@ernestognw
Copy link
Member Author

The approach of this PR was to formally verify those cases when there's a fuzz test, some of these obviously didn't work given they were also difficult to formally verify with Certora in the first place.

These are my notes about the tests that didn't work so were skipped:

Base64

The algorithm is a loop. Although attempted, tests failed with something similar to:

Encountered symbolic memory offset: 289 + Concat(0, Extract(63, 58, halmos_EncodeInput_bytes_01))

ShortStrings

In the case of testing if toShortString reverted with long strings, there seems to be an edge case with the selector of some function (perhaps when calling this.shortString). Couldn't figure out what's going on so I decided to move forward. For reference, this is what I got

Encountered Unsupported cheat code: calldata = Concat(0xf28dceb300000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000144305a27a900000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000100, halmos_RevertLongInput_string_01(), 0x00000000000000000000000000000000000000000000000000000000)

Governor

Doesn't make sense to formally verify for the description with proposer since we need to increase the loop bound and the string length less than 52 (which is 12 loops given 52 - 40) will always return true. Using a bigger string makes the test timeout.

Checkpoints

Depends heavily on loops. Some variables might be worth making symbolic but not moving into that yet imo.

SignedMath

Average

Encountered Unsupported cheat code: calldata = Concat(0xa322c40e, Extract(+(0x4000000000000000000000000000000000000000000000000000000000000000, *(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff, Concat(0x00, +(0x4000000000000000000000000000000000000000000000000000000000000001, ~(Extract(p_a_int256()))))))), +(0xff, *(0xff, ~(Extract(p_a_int256())))))

Math

CeilDiv / Sqrt / MulDiv

WARNING:Halmos:Counterexample: unknown
(see https://github.com/a16z/halmos/wiki/warnings#counterexample-unknown)
[TIMEOUT] check_CeilDiv(uint256,uint256) (paths: 7, time: 1.44s, bounds: [])

InvMod

Depends heavily on loops

Log2 / Log10 / Log256

Log2 works locally but times out in the CI. I don't think it makes sense to keep them formally verified.

WARNING:Halmos:Counterexample (potentially invalid):
p_input_uint256 = 0x00000290967f152f6cc310785e8e806ebcb3a077e59a091c0000000000001005 (17701574136214187778346309088771581813280962368749720433162010073501701)
p_r_uint8 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0)
(see https://github.com/a16z/halmos/wiki/warnings#counterexample-invalid)

MulDivDomain

WARNING:Halmos:Encountered Unsupported cheat code: calldata = 0xf28dceb3000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000244e487b71000000000000000000000000000000000000000000000000000000000000001200000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)

Modexp

[ERROR] check_ModExp(uint256,uint256,uint256) (paths: 2, time: 0.03s, bounds: [])
WARNING:Halmos:Encountered Unsupported cheat code: calldata = 0xf28dceb3000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000244e487b71000000000000000000000000000000000000000000000000000000000000001200000000000000000000000000000000000000000000000000000000

TryModexp

[ERROR] check_TryModExp(uint256,uint256,uint256) (paths: 2, time: 0.02s, bounds: [])
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000005; calldata = Concat(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000020, p_b_uint256(), p_e_uint256(), p_m_uint256()); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)

ModExpMemory

Running 1 tests for test/utils/math/Math.t.sol:MathTest
[ERROR] check_ModExpMemory(uint256,uint256,uint256) (paths: 4, time: 0.07s, bounds: [])
WARNING:Halmos:Encountered Unsupported cheat code: calldata = 0xf28dceb3000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000244e487b71000000000000000000000000000000000000000000000000000000000000001200000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000005; calldata = Concat(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000020, p_b_uint256(), p_e_uint256(), p_m_uint256()); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000005; calldata = Concat(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000020, p_b_uint256(), p_e_uint256(), p_m_uint256()); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000005; calldata = Concat(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000020, p_b_uint256(), p_e_uint256(), p_m_uint256()); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:Halmos:check_ModExpMemory(uint256,uint256,uint256): paths have not been fully explored due to the loop unrolling bound: 2
(see https://github.com/a16z/halmos/wiki/warnings#loop-bound)
Symbolic test result: 0 passed; 1 failed; time: 0.09s

TryModExpMemory

Running 1 tests for test/utils/math/Math.t.sol:MathTest
[ERROR] check_TryModExpMemory(uint256,uint256,uint256) (paths: 3, time: 0.06s, bounds: [])
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000005; calldata = Concat(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000020, p_b_uint256(), p_e_uint256(), p_m_uint256()); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000005; calldata = Concat(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000020, p_b_uint256(), p_e_uint256(), p_m_uint256()); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000005; calldata = Concat(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000020, p_b_uint256(), p_e_uint256(), p_m_uint256()); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:Halmos:check_TryModExpMemory(uint256,uint256,uint256): paths have not been fully explored due to the loop unrolling bound: 2
(see https://github.com/a16z/halmos/wiki/warnings#loop-bound)
Symbolic test result: 0 passed; 1 failed; time: 0.07s

ERC2771Forwarder

ExecuteAvoidsETHStuck

[ERROR] check_ExecuteAvoidsETHStuck(uint256,uint256,bool) (paths: 163, time: 13.57s, bounds: [])
WARNING:Halmos:Encountered Unsupported cheat code: calldata = 0xf4844814
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)

The batch version is a loop.

ERC712Consecutive

Loops

@ernestognw ernestognw requested a review from Amxx May 13, 2024 20:29
Amxx
Amxx reviewed May 17, 2024
View reviewed changes
fv-requirements.txt Outdated Show resolved Hide resolved
@ernestognw ernestognw requested a review from Amxx May 21, 2024 21:17
@socket-security Socket Security
Copy link

socket-security bot commented May 22, 2024 •
edited

New and removed dependencies detected. Learn more about Socket for GitHub ↗︎

Package New capabilities Transitives Size Publisher
pypi/halmos@0.1.12 eval, filesystem, shell 0 660 kB daejunpark, justin_gerard

View full report↗︎

@Amxx
Copy link
Collaborator

Amxx commented May 22, 2024

Looks mostly good. Before merging I'd like to discuss the prefixes. Currently we have:

  • testXxxx
  • testSymbolicXxxx
  • checkSymbolicXxxx

I'd like use to consider alternatives, maybe

  • testXxxx
  • testSymbolicXxxx
  • symbolicXxxx

Lets discuss that on today's call.

@ernestognw
Copy link
Member Author

I'd like use to consider alternatives, maybe

  • testXxxx
  • testSymbolicXxxx
  • symbolicXxxx

I'd be fine with symbolic though. Just proposed checkSymbolic as it was my best alternative lol
Will update

@ernestognw ernestognw merged commit f1a69f1 into OpenZeppelin:master May 23, 2024
20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Amxx Amxx Amxx approved these changes

Assignees
No one assigned
Labels
ignore-changeset
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@ernestognw @Amxx