Branch Explosion in `halmos` (Yices SMT Solver) Due to PR #693

[pcaversaccio]

Summary

In 🐍 snekmate, I run symbolic execution nightly tests in the CI based on halmos (latest master version) using the Yices SMT solver version 2.6.4:

• https://github.com/pcaversaccio/snekmate/blob/main/.github/workflows/halmos.yml,
• https://github.com/pcaversaccio/snekmate/blob/main/.github/workflows/halmos-venom.yml.

3 days ago the nightly tests started failing since they were running out of time (i.e. beyond the standard 3hrs GitHub threshold):

• https://github.com/pcaversaccio/snekmate/actions/workflows/halmos.yml,
• https://github.com/pcaversaccio/snekmate/actions/workflows/halmos-venom.yml.

After careful (and time-consuming lol) investigation, I was able to find the issue. I updated 4 days ago to the latest forge-std master commit c7be2a3. After running and testing the CI for hours, the following commit introduces the "regression": 276ccaa.

So what's the underlying problem? Specifically, my ERC1155TestHalmos test contract and its test testHalmosAssertNoBackdoor is running out of time. You can see the usage of assertLe and assertGe here:

for (uint256 i = 0; i < tokenIds.length; i++) {
    assertLe(erc1155.balanceOf(caller, tokenIds[i]), oldBalanceCaller[i]);
    assertGe(erc1155.balanceOf(other, tokenIds[i]), oldBalanceOther[i]);
}

But also the test testHalmosSafeTransferFrom struggles since I use assertEq here:

if (from != to) {
    assertEq(newBalanceFrom, oldBalanceFrom - amounts[0]);
    assertEq(newBalanceTo, oldBalanceTo + amounts[0]);
} else {
    assertEq(newBalanceFrom, oldBalanceFrom);
    assertEq(newBalanceTo, oldBalanceTo);
}

assertEq(newBalanceOther, oldBalanceOther);

The commit 276ccaa (and the refactor later 349b909) introduce additional branching conditions which produce a path explosion. I'm not a formal verification expert, so I can't explain exactly why, but you can see the tests here:

• https://github.com/pcaversaccio/snekmate/actions/runs/16704445274 (this is based on commit 369dd01 which is the last commit before you introduce the new logic),
• https://github.com/pcaversaccio/snekmate/actions/runs/16706057262 (this is based on commit 276ccaa).

There are 2 ways forward for me in the current status quo:

1. Pin an older forge-std version -> not sustainable
2. Directly use vm.assertGe and vm.assertLe -> ugly solution

I'm not sure if you are open to reconsider this change, but it's important to understand that such small optimisation changes can have breaking impacts downstream.

[daejunpark]

I'm not a formal verification expert, so I can't explain exactly why ...

I can confirm that the new assert logic causes path explosion in halmos. Specifically, each new assert introduces two (identical) symbolic paths, which leads to exponential growth in the number of paths as the number of asserts increases.

Previously, assertTrue(cond) worked like this:

if (!cond)
  revert

This didn't introduce a new active path, because the reverting branch is terminal.

But now, it effectively becomes:

if (!cond)
  if (!cond)
    revert

This results in two active paths with the same path constraint cond == true.

Technically, it's possible to detect and eliminate such identical paths. Halmos doesn't currently implement this optimization, as this kind of duplicated branching hasn't been common in practice. We're looking into a possible quick fix for the issue.

[pcaversaccio]

The issue has been resolved on the halmos side via a16z/halmos#572. The main reason why I don't close the issue for now is that it might also impact other formal verification frameworks like kontrol. Maybe @palinatolmach can comment on this issue from their side.

[lucasmt]

@palinatolmach asked me to double-check this, and I can confirm this is not an issue on Kontrol's side. Testing the same condition twice on the same path doesn't introduce any extra branching in Kontrol, since after the first test its truth value is already determined. I have tested this on a simplified example, and it doesn't branch any more than necessary.

[pcaversaccio]

@palinatolmach asked me to double-check this, and I can confirm this is not an issue on Kontrol's side. Testing the same condition twice on the same path doesn't introduce any extra branching in Kontrol, since after the first test its truth value is already determined. I have tested this on a simplified example, and it doesn't branch any more than necessary.

Thx for confirming! In that case, I will close this issue.