UNRESOLVED Auto summary


When verifying a property, Certora reported a call resolution for this function swapper.pool.exchange_underlying(swapper.tokenI, swapper.underlyingI, _amount, minAmount) as an UNRESOLVED Auto Summary. Then, following Certora’s documentation, I augmented the scene with a new contract and get exchange_underlying(int128,int128,uint256,uint256). What can I do to fix this problem?


Hey @acmCertora,

UNRESOLVED Auto Summary basically happens whenever an external call is being made that the Prover doesn’t know how to handle because it wasn’t specified the way. When that happens the Prover will havoc the entire state of the contract, meaning the it will “randomize” the data it collected so far, or in other word, forget any relations made in this rule’s history. It happens in order to achieve over-approximation and simulate a potential malicious behavior of the external call.

What you can do about it - If havocing is not the way to go, you need to specify to the prover how it should behave with every external call it encounters. Roughly dividing the solution into 2 categories you can:

  1. Summarize the method in question by commanding the prover to return a non deterministic value, or a constant, etc. When you do that you need to make sure to consider what is an accurate or over approximating summary for that call to make sure you’re not over simplifying and over look some feasible states of the system. under approximating will put you in danger of missing issues.

  2. You can supply an implementation of the external contracts and methods and command the prover to execute the specific them by using DISPATCHER or linking. This method can add up some complexity to the runs, depends on what the methods actually do, but may be the way to go for you if you want to make sure some action on the other side of the call is doing it’s part of the job like transferring assets back to your contract, etc.

As a rule of thumb you should always look for an over-approximation (or an accurate representation if you can ensure its accurate), and work as little as possible to summarize. If returning a non-deterministic value at every call to a getter is good enough for you, dont waste your time recreating the original contract and implementing getters.

Read more about handling calls here

hope that helps.