certora: fix prover timeouts and spec cleanup - #46
Open
avniculae wants to merge 20 commits into
Open
Conversation
Remove the representative-constant pins on price ratio and sell fee from R4_buyGhoUpdatesGhoBalanceCorrectly: route the conf's mulDiv summaries to a nondeterministic (multiplicative) encoding, where the quotient is a fresh variable pinned by its floor/ceil bounds plus implied product-free hints.
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
![certora-run[bot]](https://avatars.githubusercontent.com/in/1083145?s=60&v=4){kind=small}
There was a problem hiding this comment.
Certora Prover Run
- Group ID: bf503479-bdc2-4dad-9108-0dacc6b8c081
- Commit: 9a0e396
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Certora Prover Run
- Group ID: 88126f38-e174-4280-a1c5-bcf4473d6ed2
- Commit: 9a0e396
There was a problem hiding this comment.
Certora Prover Run
- Group ID: 7bd15000-aa4d-4fe5-bcc2-77c74237a212
- Commit: d63123f
| Job | Result | VERIFIED |
|---|---|---|
| GhoGsmStewar… | ✅ | 12 |
| GhoCcipStewa… | ✅ | 11 |
| GhoBucketSte… | ✅ | 8 |
| GhoAaveStewa… | ✅ | 17 |
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Certora Prover Run
- Group ID: 989119a6-410f-45e4-b71a-546a520f721b
- Commit: d63123f
| Job | Result | VERIFIED |
|---|---|---|
| verifyUpgrad… | ✅ | 28 |
| verifyGhoTok… | ✅ | 28 |
| verifyFlashM… | ✅ | 7 |
The summaries decided rounding with `rounding == Ceil`, but OZ v5 rounds up whenever `uint8(rounding) % 2 == 1`, i.e. for Ceil and Expand. An Expand call would silently have been modelled as a floor division. Nothing in scene passes Expand today, so this is a no-op on the current proofs, but it removes a footgun that was replicated across all eight call sites.
The confs pick between the exact, nondeterministic and closed-form mulDiv encodings purely for solver tractability, so they must all denote the same value. Nothing enforced that: loosening one of the nondet bounds would weaken every proof routed through it while leaving CI green. Verified, and rule_sanity confirms the rules are not vacuous.
optimality.spec routes to the closed-form Ceil because the optimality proofs reason about (x*y + d - 1)/d far better than about a floor plus a remainder bump; the 4626 twin was still on the reuse-floor form. Also drops the unused env binding from the constructor preserved blocks.
gho-fixedPriceStrategy4626.conf pointed at FixedPriceStrategy4626.spec, which does not exist in the tree, so it could never run; point it at the spec that does. gho-assetToGhoInvertibility-4626.conf failed typechecking outright - methods4626_base.spec declares `using GhoReserve as _ghoReserve` but the conf's files list had never been updated - so add GhoReserve plus the missing links and remapping to match its working siblings. Both had drifted precisely because nothing exercised them.
…ces-sell timeout - Both remaining unchecked `-destructiveOptimizations twostage` uses become twostage-checked, matching the decision already applied to the six confs. Plain twostage only warns when a violation cannot be confirmed without the optimizations; the checked variant fails. - balances-sell-4626 R1/R1a/R2 was only going green via auto-rerun-timeouts: the committed conf timed out and a rerun with different settings passed. The conf's nonlinear solver tuning is there for R4, so give these three their own args instead of relying on the rerun ladder. - Wire in the two previously unrun 4626 confs and the mulDiv equivalence conf. - Note that a --prover_args here replaces the conf's array rather than appending to it, which is easy to miss: the optimality R2 line therefore runs without the conf's -copyLoopUnroll 6 -depth 20.
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Certora Prover Run
- Group ID: 360494a4-ae11-4d6d-b4a8-c6e70c433833
- Commit: d0ca89b
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Certora Prover Run
- Group ID: 28ae0c1e-8555-4342-9f38-3ad7e1c08ed1
- Commit: d63123f
I would try to add back |
A --prover_args on a workflow line replaces the conf's array, so overriding it for R2 silently dropped the conf's -copyLoopUnroll 6 and fell back to the default of 4. With optimistic_loop the shortfall paths are assumed away rather than reported, so the unroll bound is a coverage setting and not just a timing one. -depth is left off, it only affects performance. Per #46 (comment)
Running both rules in one job took 67 minutes and only passed via the rerun ladder (2 of 11 strategies succeeded), which is the same masking this PR removes from balances-sell-4626. Splitting matches how every other heavy conf here is handled. buyAssetInverse_all verifies on its own with timed_out=False.
Collaborator
Author
|
Thanks — added The other override, on Two other things while I was in here:
On (Edited: originally said the invertibility conf "needed splitting per rule" and did not say where the 11-rerun observation came from.) |
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Certora Prover Run
- Group ID: 7f157de4-037e-48db-b45f-217cd14b6dc8
- Commit: d63123f
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Certora Prover Run
- Group ID: afafce4b-dc5b-4df0-81db-6f45dce67139
- Commit: 49bf400
shellygr
reviewed
Aug 3, 2026
| certora/gsm/conf/gsm4626/gho-assetToGhoInvertibility-4626.conf | ||
| # One rule per line: both are heavy enough that running them together times out. | ||
| certora/gsm/conf/gsm4626/gho-assetToGhoInvertibility-4626.conf --rule buyAssetInverse_all | ||
| certora/gsm/conf/gsm4626/gho-assetToGhoInvertibility-4626.conf --rule sellAssetInverse_all |
There was a problem hiding this comment.
are you sure we cover everything in the spec file for this conf? that's why we sometimes do --rule R and then --exclude_rule R
Collaborator
Author
There was a problem hiding this comment.
Good catch — you were right that enumerating rules with --rule is fragile: add a third rule to that spec and it would silently never run with CI still green.
In the end the split went away entirely rather than being converted to --exclude_rule. The timeout that made me split it was fixable with the z3 seed race (see follow-up below), so the workflow is back to a single bare gho-assetToGhoInvertibility-4626.conf line with no rule enumeration at all.
Worth knowing this conf had never run in any workflow: its files list was missing GhoReserve.sol that methods4626_base.spec needs, so it failed typechecking.
(Edited: originally said I had excluded sellAssetInverse_all and asked for a ticket number to reference it. Both no longer apply — nothing is excluded and no ticket is needed.)
Collaborator
Author
There was a problem hiding this comment.
Update — I was wrong to exclude sellAssetInverse_all, and the fix was your own trick sitting in four sibling confs.
The assert is provable; it was just landing near the timeout. Adding the z3 random-seed race that balances-buy, fees-buy, fees-buy-4626 and optimality4626 already use:
| before | after | |
|---|---|---|
sellAssetInverse_all alone |
TIMEOUT at 119m (5 of 6 asserts) | verified, 3m, 6 asserts |
| whole conf, both rules | 67m | verified, 5m, 11 asserts |
So no rule is dropped, no ticket needed, and I've put the flag in the conf's prover_args rather than on the workflow line — both because that's where the other four keep it, and because a --prover_args on the line would replace the conf's array rather than add to it.
That also removes the thing you flagged: with the conf fast again there's no reason to split at all, so the workflow is back to a single bare gho-assetToGhoInvertibility-4626.conf line with no rule enumeration to go stale.
What led me astray was treating one unlucky 119m run as evidence the rule couldn't converge. Ignore the earlier ticket-number request.
…the timing-out rule Two --rule lines enumerate the spec's rules, so a rule added later would silently never run while CI stayed green. --exclude_rule is a partition and picks new rules up automatically, matching how gho-gsm-2.conf and fees-sell.conf are split here. sellAssetInverse_all times out on Assert_asset_amount (119m locally, one assert of six) and only reported green through the rerun ladder, with a different winning strategy each run. Commented out pending a ticket rather than left masked.
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Certora Prover Run
- Group ID: 0e19bf8b-95b3-4920-ac2d-5ff6794d3d56
- Commit: 393c4f0
Collaborator
Author
|
@shellygr one more thing on
Same flavour as Is that expected variance, or are these confs close enough to the timeout that the ladder is doing real work? It matters because when the rerun fires, the configuration that verified isn't the one in the repo, and the winning strategy has differed every time I've looked. For what it's worth, the z3 seed race fixed exactly this shape of problem on |
…ad of dropping a rule sellAssetInverse_all was timing out on its asset_amount assert and only reaching green through the rerun ladder, and I had excluded it. That was wrong: the assert is provable, it was just landing near the timeout. Adding the same z3 random-seed race already used by balances-buy, fees-buy, fees-buy-4626 and optimality4626 takes the rule from a 119m timeout to 3m, and the whole conf from 67m to 5m for all 11 asserts. With the conf fast again the workflow needs no rule splitting at all, so the --rule/--exclude_rule enumeration goes away entirely. Keeping the flag in the conf rather than on the workflow line also avoids the CLI prover_args override replacing the conf's array.
avniculae
marked this pull request as ready for review
August 4, 2026 12:37
avniculae
changed the title
Kogaroshi
approved these changes
Aug 5, 2026
DhairyaSethi
approved these changes
Aug 10, 2026
Comment on lines
+35
to
+36
| # NB: a `--prover_args` here REPLACES the conf's `prover_args` array, it does not | ||
| # append to it. Restate every flag the run needs, not just the one being added. |
Member
There was a problem hiding this comment.
do we need this comment here?
Collaborator
Author
There was a problem hiding this comment.
Dropped in d63123f, from both workflows that had it.
| submodules: recursive | ||
|
|
||
| - uses: Certora/certora-run-action@v2 | ||
| - uses: Certora/certora-run-action@v2.10.0 |
Member
There was a problem hiding this comment.
we've been pinning by hash usually bc this can be updated as well but nbd this is fine also
Collaborator
Author
There was a problem hiding this comment.
Pinned by SHA across all four workflows in d63123f.
| is_in_facilitator_set_array(facilitator) <=> is_in_facilitator_set_map(facilitator) | ||
| {preserved{ | ||
| requireInvariant addressSetInvariant_2(); | ||
| requireInvariant length_leq_max_uint160(); |
Member
There was a problem hiding this comment.
why do we not need this anymore?
Collaborator
Author
There was a problem hiding this comment.
set.spec:109 has axiom to_mathint(mirrorArrayLen) < TWO_TO_160() - 1 unconditionally, and the array-length Sload hook forces mirrorArrayLen == len, so the bound already holds without the requireInvariant.
The invariant itself was vacuous — its own docstring said so, "the proof of the assumption is vacuous because length > loop_iter" — so it went along with its five uses. verifyGhoToken went 29 -> 28 rules, just that one.
Comment on lines
+44
to
+45
| // Same value as mulDivRounding, written as the single closed form (x*y+d-1)/d for Ceil. | ||
| // The optimality proofs reason about this closed form far better than the reuse-floor form. |
Member
There was a problem hiding this comment.
very interesting, curious if it's bc of the consecutive random number gen (seed)
need to look into how that z3 rand works bc if it's deterministic then symbolically we're not checking all cases and instead adding a restriction correlation
Collaborator
Author
There was a problem hiding this comment.
what do you mean here? what cases are we leaving out here?
Tags are mutable, so pin the action by SHA across all four workflows.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Ports Certora#9, which supersedes #6 and #8 — all three can be closed once this lands. Commits and authorship retained;
mainis a direct ancestor, so the diff is only the Certora spec/conf/CI changes.All 48 prover jobs verify.
On top of the ported work:
Rounding.Expandwas modelled as a floor division; the summaries now mirror OZ'sunsignedRoundsUpmulDiv_equivalence.specproves the exact, nondeterministic and closed-form mulDiv encodings denote the same value-copyLoopUnroll 6was silently dropped on theoptimality.conf R2line, since a line-level--prover_argsreplaces the conf's arraygho-fixedPriceStrategy4626.confpointed at a spec that isn't in the tree, andgho-assetToGhoInvertibility-4626.conffailed typechecking on a missingGhoReserve.sol; both fixed and wired into CIbalances-sell-4626 R1/R1a/R2andgho-assetToGhoInvertibility-4626were green only via timeout reruns; both now verify on the committed config, the latter via a z3 seed race (119m timeout → 3m)twostage→twostage-checked;optimality4626.specmoved to the closed-form Ceil encoding to match its non-4626 twinOne pre-existing item left open:
getAmount-properties-4626.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcPropertyhas gone green via rerun on two of five runs (#issuecomment-5177477733).