Clarification on HAVOC in Call Trace After Linking External Contracts

[dayday2019]

Hi Certora team,

I have a question regarding the reliability of Certora's analysis results in the presence of HAVOC steps in the call trace.

I understand that when Certora encounters an external function whose implementation is unknown, it models the return value using HAVOC. However, after I use the --link option to link the actual external contract, I still see many red HAVOC steps in the call trace. At the same time, in the "Contracts Call Resolutions" section, there are no longer any alerts related to unresolved calls.

Could you please clarify:

1. Why are there still so many HAVOC steps in the call trace after linking the external contract?
2. In such a case, can I still trust the rule evaluation results, even when the execution trace contains many HAVOC steps?
3. Does the presence of many HAVOC steps necessarily imply that the rule result is unreliable?

As an example, here is a link where there are no more unresolved call alerts in "Contracts Call Resolutions", but the call trace still shows many HAVOC steps. Is the result of this rule considered trustworthy?

https://prover.certora.com/output/5562613/96e11c341033427fb84e48b04ecc7a61/

Thank you very much for your help!

[dayday2019]

@certora-bot @abakst @shallem @jhoenicke I really need your help, Thank you very much!

[dayday2019]

@naftali-g @urikirsh @rahav-certora Can I still trust the rule evaluation results, even when the execution trace contains many HAVOC steps?

[naftali-g]

Hi @dayday2019, All the red HAVOCs you see are about the source of the storage state. It's telling you at different points of the calltrace how the specific values of the state variables were chosen. So you can see in the beginning of the calltrace all values were chosen arbitrarily (i.e. HAVOC), and most of them didn't change during the whole run of the rule so it's just showing you the same info over and over. The only value that actually changed during the run is the totalDeposits storage field, inside the redeem function. There it shows after that change that the reason for the specific value is HAVOC DEPENDENT meaning that this value depends on havoced values - specifically the previous value of totalDeposits and the amount.
So bottom line - yes I think you could trust the results.

[dayday2019]

Hi @dayday2019, All the red HAVOCs you see are about the source of the storage state. It's telling you at different points of the calltrace how the specific values of the state variables were chosen. So you can see in the beginning of the calltrace all values were chosen arbitrarily (i.e. HAVOC), and most of them didn't change during the whole run of the rule so it's just showing you the same info over and over. The only value that actually changed during the run is the totalDeposits storage field, inside the redeem function. There it shows after that change that the reason for the specific value is HAVOC DEPENDENT meaning that this value depends on havoced values - specifically the previous value of totalDeposits and the amount. So bottom line - yes I think you could trust the results.

@naftali-g Thank you for your help.

I also wonder about the meaning of DEFAULT_HAVOC and under what circumstances this value would be returned.
I think it will be returned when the callee function is missing, right?

CertoraProver/src/main/kotlin/report/calltrace/CallTrace.kt

Line 37 in b945191

DEFAULT_HAVOC("DEFAULT HAVOC"),