Invariant shrinking does not find the smallest sequence of transactions

[aviggiano]

Component

Forge

Have you ensured that all of these are up to date?

• Foundry
• Foundryup

What version of Foundry are you on?

forge 0.2.0 (67ab870 2023-12-28T00:18:11.567460000Z)

What command(s) is the bug in?

forge test --mc FoundryTester

Operating System

macOS (Apple Silicon)

Describe the bug

I am running a Foundry invariant test campaign, and I know for a fact that only 1 transaction is required to break the invariant. However, Foundry consistently fails to shrink down to that one.

I restarted the run 10 times and took note of how many txs it was able to shrink to:

1. 6
2. 12
3. 3
4. 10
5. 15
6. 12
7. 13
8. 10
9. 12
10. 1

I also tried doubling the shrink_run_limit parameter up to 524288, but it made no difference, neither in the "performance" of the shrinking algorithm nor in the time to shrink. This is unexpected. I'd like to crank the "shrinking" limit up to infinity and be able to get to "the" smallest possible.

[mds1]

@aviggiano can you share the test case to reproduce with?

cc @brockelmore

[aviggiano]

@mds1 The codebase is still private, but I'll create a generic MWE.
I'll share it when it's done.

[aviggiano]

@mds1 I was able to create a very simple MWE using the sample Foundry project:

https://github.com/aviggiano/shrinking-mwe

Tests:

[I] ➜ i=0; while [ $i -lt 10 ]; do; forge test | grep -o sender= | wc -l; i=$((i+1)); done;
      22
      22
      28
       4
      30
      26
       4
       8
      18
       6

[mds1]

I think the issue here (though I’ll let @brockelmore confirm) is that forge’s shrinking can only find the local minimal sequence based on the initial sequence and that broke the invariant, and does not back out to look for a global minimal sequence.

For example, if you can break the invariant with a single call of addThree OR three calls of increment, forge won’t shrink to the global minimum of a single addThree call if that method was never called in the original sequence.

I’m not familiar with echidna’s approach, but does it consistently find the global minimum?

[aviggiano]

I’m not familiar with echidna’s approach, but does it consistently find the global minimum?

Both Echidna and Medusa will attempt to find the "global minimum", and I expect them to eventually find it if I increase the shrink limit. See below:

# Echidna
[I] ➜ i=0; while [ $i -lt 10 ]; do; echidna . --contract CryticTester --config echidna.yaml | grep -v '^\[' | grep '(' | wc -l; i=$((i+1)); done;
       1
       2
       2
       4
       5
       1
       1
       2
       4
       5

# Medusa
[I] ➜ i=0; while [ $i -lt 10 ]; do; medusa fuzz | grep -o '^[0-9]\+) ' | wc -l; i=$((i+1)); done;
       2
       2
       2
       2
       1
       1
       2
       2
       2
       2

I've updated the MWE to support those 2 fuzzers as a benchmark.

[brockelmore]

hmm interesting

I would expect all of them to reduce down to at most 3 or 4. I will take a look, thanks for repro.

What’s strange is that if the initial sequence is < 13 calls long, we use a power set so we are guaranteed to get the minimum number of calls (without modifying the calldata, i.e. 3 increments won’t shrink to a setNumber(3)).

[grandizzy]

the reason is that we're updating the min sequence only when an revert see https://github.com/foundry-rs/foundry/blob/master/crates/evm/evm/src/executors/invariant/error.rs#L222-L227

so pretty sure if you update this line in your project
https://github.com/aviggiano/shrinking-mwe/blob/main/test/Counter.t.sol#L26
with

require(counter.number() != 3);

then you'll get proper shrinked sequence

[brockelmore]

Aaahh nice find @grandizzy. We should just change that line to perform the invariant check as a test would such that it would shrink if the invariant fails not just revert.

[grandizzy]

Aaahh nice find @grandizzy. We should just change that line to perform the invariant check as a test would such that it would shrink if the invariant fails not just revert.

makes sense, I can look into and craft a pr for 👍

[grandizzy]

Aaahh nice find @grandizzy. We should just change that line to perform the invariant check as a test would such that it would shrink if the invariant fails not just revert.

here's pr #7257 and a little goodie on top of it while testing #7256