Add Halmos support #5034

ernestognw · 2024-05-08T19:17:01Z

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 · 2024-05-08T19:17:05Z

⚠️ 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 · 2024-05-13T20:29:13Z

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

This reverts commit 61e8ab7.

This reverts commit 5d61e47.

fv-requirements.txt

.github/workflows/formal-verification.yml

test/utils/Arrays.t.sol

test/utils/SlotDerivation.t.sol

Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>

scripts/generate/templates/SlotDerivation.t.js

socket-security · 2024-05-22T12:56:06Z

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 · 2024-05-22T13:00:39Z

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 · 2024-05-22T16:03:20Z

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 added 2 commits May 8, 2024 20:05

Add Halmos support

d23da5c

solhint disable

8db40c6

Fix lint

bdc2398

ernestognw added the ignore-changeset label May 8, 2024

ernestognw added 6 commits May 10, 2024 20:33

Apply Halmos team suggestions

14afaf4

Remove commented failing tests

7c6b5ce

Update workflow

5e10b1f

Move halmos check to formal verification workflow

9a0eb4c

Remove testSymbolicLog2 due to timeout

4484df4

Merge branch 'master' into chore/use-halmos

6368717

ernestognw marked this pull request as ready for review May 13, 2024 19:35

ernestognw added 3 commits May 13, 2024 13:46

Fix workflow lint

da8990c

Fix SlotDerivation tests generation

ca59b7e

Add missing description

809a5d6

ernestognw requested a review from Amxx May 13, 2024 20:29

ernestognw added 10 commits May 13, 2024 18:52

Merge branch 'master' into chore/use-halmos

0c22458

Upgrade python-version

61e8ab7

Revert "Upgrade python-version"

05d479d

This reverts commit 61e8ab7.

Set python version when building docs

5d61e47

Revert "Set python version when building docs"

6e84212

This reverts commit 5d61e47.

Remove requirements.txt when building docs for netlfify

6c429a3

Change requirements.txt file name

6729d16

Fix wrong file reference

6e0ce0c

Add cache-dependency-path

3b94a82

Add explaining comment for requirements filename

01912ba