certora: summarize oracle price() to fix NoDebtWithoutCollateral SMT timeout#1077
certora: summarize oracle price() to fix NoDebtWithoutCollateral SMT timeout#1077claude[bot] wants to merge 4 commits into
Conversation
…e loop The `verify (NoDebtWithoutCollateral)` CI leg flaked between a ~9-minute pass and a 2h SMT timeout. Root cause: the liquidate() preserved block unrolls the `while (_collateralBitmap != 0)` loop 5x, and each iteration calls IOracle(...).price(). With `-havocAllByDefault true`, every unresolved price() external call forces a full HAVOC_ALL of storage that the solver re-proves across the loop unrolling and the 10-seed z3 portfolio -- the dominant cost behind the timeout. Summarize `_.price()` as PER_CALLEE_CONSTANT, matching the sibling spec CollateralBitmap.spec which already proves the analogous loop in seconds. price() is a view (staticcall) and cannot mutate state, so the summary does not weaken the reentrancy modeling `-havocAllByDefault` provides for the genuinely state-changing external calls (onLiquidate callback, token transfers). No budget knobs (loop_iter, smt_timeout, seed portfolio, havocAllByDefault) are changed.
Switch the _.price() summary from PER_CALLEE_CONSTANT to NONDET so the prover may return different adversarial values across reads of the same oracle (e.g. across the onLiquidate reentrancy). price() is a view (staticcall), so it cannot mutate state or reenter with side effects; the summary removes only the impossible HAVOC_ALL of storage, not real behavior. NONDET is strictly more adversarial on the return value, so it cannot hide a bug that depends on the price varying.
There was a problem hiding this comment.
I don't think it should change anything: havocAllByDefault only affects non-static calls, so the AUTO summary should summarize price as NONDET already
There was a problem hiding this comment.
You're right, thanks for catching this. I verified it in the prover source (Havocer.kt): the HavocAllByDefault → HavocType.All branch is guarded by callType != STATIC, and a view call like price() falls through to HavocType.Static (NONDET). So -havocAllByDefault never havocs price(), and _.price() => NONDET is a no-op — my root cause was wrong.
Checking the record properly, the leg times out ~45% of the time on main regardless of this summary (6-8 of the last ~15 runs), so the green runs here were luck, not a fix. The real cost drivers look like the HAVOC_ALL on the genuine state-changing calls in liquidate (the callback + token transfers) plus the quantified nonlinear mulDiv/RCF arithmetic. A real fix is more likely the requireInvariant bitmap hints plus bounding the WAD*WAD - lif*lltv denominator. Sorting out the path with the team before pushing anything.
Generated by Claude Code
|
Closing this — the Generated by Claude Code |
3 participants
Requested by Mathis GD · Slack thread
Fixes the flaky SMT timeout on the
verify (NoDebtWithoutCollateral)leg (rulelockedOrNoDebtWithoutCollateral). The invariant'sliquidatepreserved case unrolls the collateral loop, and each iteration's unresolvedIOracle.price()call triggers a fullHAVOC_ALLof storage under-havocAllByDefault— so the leg either proved in ~10 min or ran out the 7200s budget.Summarizes
_.price()asNONDETinNoDebtWithoutCollateral.spec:price()is a view (staticcall), so it can't mutate state or reenter, and the summary drops the spurious per-iteration havoc while keeping the return value fully adversarial.