testing: invariants

[varunsrin]

Explore foundry's new invariant test model, which maple finance has implemented here.

We might be able to use this to assert invariants while fuzzing, but needs more investigation and there are no docs yet. Probably easiest to wait for a while until docs come out since we have other higher pri items right now.

[varunsrin]

After some trial and error with invariant testing the problem is that it does not seem to guarantee the invariant as we walk through all other tests in the file. Rather, it fuzzes a series of inputs (sender_address, target_address and calldata) and checks if the invariants are ever violated.

This is fine for asserting that invariants hold within a single function, but there are many logical branches that can only reach when another function has been called with another parameter. Is there any way to such cases?

Next step might be to write out a sample test and prove that the invariant test misses (or catches) such cases, before determining whether to integrate it into our suite. Either way, lower priority for now.

Resources:

• Invariant Testing foundry-rs/foundry#69
• feat(forge): Invariant Testing v2 foundry-rs/foundry#1572
• https://github.com/dapphub/dapptools/blob/master/src/dapp/README.md#invariant-testing

[joshieDo]

Saw it linked and wanted to give my take.

but there are many logical branches that can only reach when another function has been called with another parameter. Is there any way to such cases?

Invariant testing does catch these kind of scenarios. But it depends on the complexity and on the probability of such events happening during the testing run. However there are certain branches that it will be very improbable to catch. See this thread for more: foundry-rs/foundry#2851 . We do have some tweaks to catch some: eg if x == CONSTANT, CONSTANT is a PUSHX operation that we add to dictionary, and thus, increase the probability that it will get tested.

To conclude that invariant testing is still a valuable tool to add . But just like any tool, it's incomplete by itself.

[varunsrin]

@joshieDo thanks for the details - is it possible to write invariants for map values?

for instance, an invariant I want to test is idOf[address] != 0 if recoveryClockOf[idOf[address]] != 0

[varunsrin]

also see: https://mirror.xyz/horsefacts.eth/Jex2YVaO65dda6zEyfM_-DXlXhOWCAoSpOx5PLocYgw

[horsefacts]

I'm interested in picking this one up.