Thread by @zachobront

I was recently working on an audit that used Solady FixedPointMathLib by @optimizoor.

@daejunpark had some concerns with the square root function. What if there were edge cases where the Yul didn’t behave?

Fuzzing didn’t find any, but we couldn’t know for sure.

…or could we?

Enter HALMOS.

It's a symbolic bounded model checker.

What this means is that it takes in EVM bytecode, converts it to a series of equations, and uses the Z3 Theorem Prover to verify the assertion (or find counterexamples).

github.com/a16z/halmos

It runs directly from existing Foundry fuzz tests, so it's shockingly easy to set up relative to more "formal" formal verification.

Let's take it for a spin and see if we can prove the sqrt() function.

First, we'll copy the function out of the library and dump it into our test file (Halmos doesn't support libraries yet).

Now we need a way to compare it's results to the "ground truth".

The easiest way to do this is to work backwards:
- pick a random number i
- square it
- add any number n where n < i

Now we know sqrt(i ** 2 + n) == i.

That was easy, let's run out test, formally prove the function, and move on with our day...

Uh oh. When a symbolic model checker says "unknown" that means Z3 wasn't able to definitively solve the system of equations.

This is often because we're doing too much, but can also be from using large numbers or division.

Some things we can do to help with this:
- use vm.assume() instead of bound()
- use vm.assume(n < i) instead of i = i % n

But we've already done those things, and it's still not provable.

We can run a Foundry fuzz test to ensure that our setup was correct. The test passes fine.

The problem is just that the function is too complex.

So what can we do? Well, this function is an optimized version of Solmate's sqrt() function.

If we can't prove it's correct, at least we might be able to prove that they're equivalent?

If we look at the two functions, we notice something promising:

All the division happens in the "Babylonian method cycles" at the end, and that part of the function is identical between the two implementations.

That means we can remove it to test equivalence.

Let's try that. First, we'll abstract the identical Babylonian cycles out from the functions.

We run a fuzz test to make sure that both still work correctly, and the removed portions are, in fact, identical.

Now we can finally recreate our Halmos test, but focus it only on proving equivalence between the two functions up until the the point where the Babylonian cycles begin.

After a moment of waiting...

Bingo.

We can now say with 100% confidence that the Solady and Solmate implementations of sqrt() produce the same result.

@daejunpark can sleep easy.

I've started a repo to formally verify some of the other Solady math functions.

Besides @transmissions11 needing to save me from an idiotic false alarm, it's been going well.

If you're interested in Halmos, check it out for some fun & simple examples: github.com/zobront/halmos…