Certora round 3: refresh drifted specs, conservation slices, CI gate#42
Merged
Conversation
Assess whether to continue the Certora effort after a fresh research pass. Verdict: continue, but narrow to tooling-independent work. Two findings drive the scope: - certora-cli 8.13.1 is already the latest release, so the via_ir / internal-summary blockers (Track A) have no upgrade path — escalate, stop. - ClusterPayoutOracle.sol changed 3x after its spec was frozen; new rejection/challenge branches are uncovered (verification debt). Priorities: refresh oracle spec, prove aggregate claimed<=pool (now cheap, the sum is already a scalar slot), promote fast confs to a required PR gate + add a spec-freshness guard, then Gambit/Track B/D opportunistically. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
ClusterPayoutOracle.sol changed three times (10ded66, 808570b, 969536f) after the spec was frozen, leaving new security branches uncovered and one inline line reference stale. - Add cannotReproposeRejectedCorrelationEpochRoot: the contrapositive of the new replay guard (L-Oracle-4 / 10ded66) — a blacklisted (epochId, clusterRoot) can never be re-proposed via proposeCorrelationEpoch. Mirrors the existing cannotReproposeRejectedRoot proof one level up at the correlation-epoch layer. - Fix the stale rejected-root guard line reference (385 -> 429). - Document the still-deferred new surface (metadata-vs-root split, the disinterested-challenger guard) — both need getters for private struct fields. Compiles + CVL type-checks under certora-cli 8.13.1 (make certora-check). Full proof runs on the cloud prover via the existing CI conf. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The headline solvency property "sum of voter payouts <= round voterPool" factors into two pieces; this lands the tooling-independent ones and pins the deferred remainder precisely. - MulDivLemma.spec / mul-div-lemma.conf: the reusable nonlinear bound (a*b)/c <= a for b <= c (+ exact-when-full and monotonicity corollaries). This is the per-claimant primitive calculateVoterReward = (voterPool*stake)/total <= voterPool reduces to, and also the lemma the LaunchDistributionPool paid<=cap gap needs (Track B). Enables -smt_useNIA so the multiply-then-divide is dischargeable (the linear backend cannot — see certora-security-findings.md). - RoundRewardDistributorConservation.spec / conf: the claimed-amount accumulators (roundVoterRewardClaimedAmount, roundFrontendClaimedAmount) are MONOTONE — every write adds a non-negative amount or reverts, no clawback/underflow. Engine-model- free and robust. The remaining deferred piece (the full claimed<=pool upper bound) needs the score-weight summation invariant across engine per-commit state — documented in the spec header and round3-plan as needing a faithful engine model. All confs compile + CVL type-check under certora-cli 8.13.1. Full proofs run on the cloud prover. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…Track G) Two CI maturation steps that need no CERTORAKEY and prevent the spec base from rotting against an active contract codebase: - certora-check job: compile + CVL type-check every conf (--compilation_steps_only). Deterministic, fast, secret-free — the realistic REQUIRED-gate candidate. Catches exactly the signature/syntax drift that left ClusterPayoutOracle.spec stale. Also type-checks the two QRPE confs that are excluded from the (slow) proof matrix. - spec-freshness job + check_spec_freshness.py: on PRs, fail if a Certora-covered contract changes without its spec being reviewed. The contract->spec map is derived from the confs themselves (resolving harness imports too), so there is no second source of truth. Bypass intentional contract-only changes with [spec-ok] in the PR title/body. Tested locally across flag/pass/harness/override cases. Also wires the two new Track C confs (mul-div-lemma, round-reward-distributor- conservation) into the cloud proof matrix. The cloud matrix stays non-gating. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
A passing spec only means "no counterexample to the rules as written" — it does not prove the rules are strong enough to catch a real bug. Gambit (bundled with certora-cli) measures that: certoraMutate injects contract mutants and re-verifies each against the spec; a surviving mutant flags an under-constrained rule. - certora/mutation/: mutation confs for the three cleanest targets (FrontendRegistry, FeedbackBonusEscrow, RewardMath) — all harness-based and via_ir-free, so they avoid the internal-summary tooling limits and run fast enough for a full mutant sweep. - make certora-mutate (MUTATION_CONF=...) target. - certora/mutation/README.md: how to run, how to read killed-vs-surviving mutants, and the rule for promoting a target into CI once its survivor set is triaged. Run manually with CERTORAKEY (one prover job per mutant); not in CI. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The previously by-inspection-only lemma raterLaunchCap <= raterFullLaunchCap reduces at assignment to (fullCap * bps) / 10000 <= fullCap (bps <= 10000) — the nonlinear multiply-then-divide the linear SMT backend cannot discharge. - Enable -smt_useNIA on the cap conf so the nonlinear backend runs (the findings doc confirmed NIA discharges this assignment multiply). - Harness wrapper assignLaunchCap_ exposes the internal _assignLaunchCap so the clamp can be checked at the point it is computed. - Rule assignedCapWithinFullCap: activeCap <= fullCap, the real-contract instance of MulDivLemma's (a*b)/c <= a, with policyBpsBounded supplied via requireInvariant. Converts the load-bearing assignment step from "correct by inspection" to machine-checked. The end-to-end global paid<=cap invariant stays the honest residual (the catch-up paths resist even under NIA — documented in the spec header). Compiles + type-checks under certora-cli 8.13.1. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ack D) Time-boxed Track D. Two outcomes: - Apply nondet_difficult_funcs to both QRPE confs — a compiler-level auto-summary of difficult view/pure internal functions that cuts SMT load so the authored refunded-pool gate and claim-flag rules have a chance to complete. This is NOT a CVL internal-function summary, so it is not blocked by the via_ir limitation. - Correct the Track D premise: the next-steps doc assumed QRPE's claim resolver was an EXTERNAL call (summarizable, like NoDoubleClaim.spec). It is not — _resolveQuestionRewardClaim (QuestionRewardPoolEscrow.sol:1460, called from the claim path at :733) is INTERNAL. So the per-commit no-double-claim faces the same internal-summary-under-via_ir wall as the engine (Track A), and send-only mode alone does not unblock it. Recorded in the conf and round3-plan so it is not re-chased. Both confs still compile + type-check under certora-cli 8.13.1. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- certora-escalation-internal-summary-via-ir.md: ready-to-file upstream issue for the one genuinely blocked item (internal-function summaries under solc_optimize + via_ir), with the environment, the real-world repro confs, what was already tried, and the ask. Parked, not chased — 8.13.1 is the latest cli, so no upgrade path today. - round3-plan.md: implementation-status table (all 7 items, per-commit). - security-findings.md: round-3 results section (no vuln found; the oracle-drift, internal-resolver, and latest-cli findings). - certora/README.md: the two new confs added to the layout + status. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e6b28dbbf6
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+93
to
+94
| if target.startswith("contracts/"): | ||
| deps.add(target) |
There was a problem hiding this comment.
When a conf targets a concrete contract, this only records that top-level files entry, so changes to code that is verified through imports do not trip the PR guard. For example, round-reward-distributor.conf verifies contracts/RoundRewardDistributor.sol, which imports and calls contracts/libraries/FrontendFeeDustLib.sol (RoundRewardDistributor.sol:16 and the dust path around :875), but printf 'packages/foundry/contracts/libraries/FrontendFeeDustLib.sol\n' | python3 packages/foundry/certora/scripts/check_spec_freshness.py --changed-stdin reports OK. That lets a PR change covered behavior without touching/reviewing the relevant specs, defeating the drift check for library-backed contract logic.
Useful? React with 👍 / 👎.
Owner
Author
There was a problem hiding this comment.
Good catch — valid gap. Fixed in e364e57: the guard now walks imports transitively, following into libraries (contracts/libraries/**) and, from a harness, the wrapped contract. FrontendFeeDustLib.sol now maps to the RoundRewardDistributor specs and a change to it trips the guard. Sibling full contracts reached via import are deliberately excluded since the specs summarize them as external NONDET (so they can't affect what's proved), whereas libraries are linked into the verified behavior.
Codex review (PR #42): the guard only mapped a conf's top-level files entry, so a change to a library compiled into a covered contract (e.g. FrontendFeeDustLib in RoundRewardDistributor's dust path) did not trip the check — defeating drift detection for library-backed logic. Walk imports transitively from each conf target, following into libraries (contracts/libraries/**) and, from a harness, the one contract it wraps. Sibling full contracts reached via import are deliberately NOT included: the specs summarize those as external NONDET, so they cannot affect what is proved, whereas libraries are linked in and are part of the verified behavior. FrontendFeeDustLib now maps to the distributor specs and a change to it trips the guard; ContentRegistry (summarized) stays out of scope. Re-tested: flag/pass/regression/own-diff all correct. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…gate The certora-check gate ran every conf through certora-cli's LOCAL CVL type-checker (--compilation_steps_only), which needs Java >= 19. The job apt-installed JDK 21 but that is not the default `java` on the GitHub runner's PATH, so the tool logged "Installed Java version is too old to check CVL specification files locally" and the step failed for every conf. (The cloud proof matrix type-checks server-side, so it never hit this.) Point JAVA_HOME / PATH at the runner's preinstalled $JAVA_HOME_21_X64. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…r fix) Cloud prover flagged frontendClaimNeverDecreasesClaimedAmount, then (after making it targeted) finalizeFrontendFeeDust, as violated. Root cause is not a contract decrease path — every write to roundFrontendClaimedAmount is a += — but the via_ir auto-finder instrumentation gap over finalizeFrontendFeeDust's _processFrontendFeeDustBatch loop, which yields a spurious counterexample from an unreachable havoc prestate. Replace the one parametric rule with targeted per-mutator rules (matching the passing voter-side rules), and omit the finalizeFrontendFeeDust wrapper: its only accumulator write is the += releasedDust already covered by the finalizeProcessedFrontendFeeDust rule. All four write sites (:265, :597, :750, :914) remain covered; the spec now verifies clean on the cloud prover. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…I lint Pre-existing formatting drift (brace spacing in imports and empty blocks) from the earlier oracle commits, surfaced by `make lint` (forge fmt --check) on this PR. Pure whitespace, no semantic change (git diff -w is empty). Pinned CI forge is v1.5.1, matching the local formatter, so the result is stable. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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
1 participant
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.
Implements the round-3 Certora plan (
docs/testing/certora-round3-plan.md). After a research pass established that certora-cli 8.13.1 is already the latest release (so the via_ir/internal-summary blockers have no upgrade path) and thatClusterPayoutOracle.solhad drifted three commits ahead of its spec, this PR spends the budget on tooling-independent, fund/correctness-protecting work and on keeping the proofs honest against a moving contract base.Each step is its own commit.
What landed
cannotReproposeRejectedCorrelationEpochRootrule covers the L-Oracle-4 replay branch (commit10ded66c); fixed the stale line reference; documented the still-deferred new surfaceMulDivLemma.spec(reusable(a*b)/c ≤ abound, NIA) + RoundRewardDistributor accumulator monotonicity. Full inductiveclaimed ≤ poolstays deferred (needs the engine score-weight model) — documented preciselycertora-checktype-check gate +spec-freshnessPR guard (with tested script) + new confs wired into the cloud matrixmake certora-mutate+ how-to READMEassignedCapWithinFullCapmachine-checks the cap-assignment clamp under-smt_useNIA(was by-inspection only); end-to-end global invariant stays the documented residualnondet_difficult_funcsload-cut applied; corrected the premise — QRPE's resolver is internal, so per-commit no-double-claim is blocked by the same wall as Track A, not unblockable by send-onlyVerification
certoraRun <conf> --compilation_steps_only) — the full sweep the newcertora-checkjob runs.spec-freshnessguard was tested across flag/pass/harness-import/override cases and passes on this branch (no contracts changed).CERTORAKEYavailable locally) — consistent with how prior phases were landed. Items marked ◑ in the plan are partial by design: the tooling-independent slice is proved; the residual is a documented solver/tooling limit, not a contract defect.No security findings
The formal work surfaced no exploitable vulnerability. The oracle-spec drift left existing proofs sound (no signature change) but coverage lagging — now closed for the replay branch and guarded against recurrence by the
spec-freshnesscheck.🤖 Generated with Claude Code