From 5c849d3c02359b6f411d225270fd42f05eccbeff Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 09:00:48 +0200 Subject: [PATCH 01/12] =?UTF-8?q?docs(certora):=20round-3=20plan=20?= =?UTF-8?q?=E2=80=94=20narrowed,=20research-backed=20next=20steps?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- docs/testing/certora-round3-plan.md | 172 ++++++++++++++++++++++++++++ 1 file changed, 172 insertions(+) create mode 100644 docs/testing/certora-round3-plan.md diff --git a/docs/testing/certora-round3-plan.md b/docs/testing/certora-round3-plan.md new file mode 100644 index 000000000..a0df5f3ba --- /dev/null +++ b/docs/testing/certora-round3-plan.md @@ -0,0 +1,172 @@ +# Certora — round-3 plan (research-backed) + +This is the third follow-up. Rounds 1–2 ([`certora-followup.md`](./certora-followup.md), +[`certora-next-steps.md`](./certora-next-steps.md)) landed Phases 1–10 / Tracks B–G as +verified slices, with the blocked remainder recorded in +[`certora-security-findings.md`](./certora-security-findings.md). This round re-asks the +question **"is it worth continuing, and if so on what?"** after a fresh research pass, and +narrows the work to what is actually unblocked and high-value today. + +## Should we continue? — yes, with a narrowed scope + +The effort is mature and the docs are excellent. Two research findings reshape the plan: + +1. **certora-cli 8.13.1 is already the latest release** (May 19, 2026 — confirmed on PyPI + and the Prover changelog). There is no 8.14+/9.x. So the items parked as + "tooling-blocked, revisit on a cli bump" — chiefly **Track A** (engine internal-resolution + under `via_ir`), native solc-0.8.35 `via_ir` mapping, and the large-contract timeout — have + **no upgrade path right now**. The existing "escalate, don't chase" call on Track A is + correct and should be treated as final for this round. We are at the tooling ceiling; do + not spend engineering time fighting it. + +2. **The contracts have outrun the specs.** `ClusterPayoutOracle.sol` changed three times on + 2026-06-08 (`10ded66c` block replay of rejected correlation roots, `808570b3` reject + same-frontend challenges, `969536f0` split oracle metadata vs root rejections) — all + *after* `ClusterPayoutOracle.spec` was frozen on 2026-06-07. The spec still compiles (no + signature/struct drift), so existing proofs are not invalidated, but the new + security-relevant branches (correlation-epoch root/metadata rejection split, same-frontend + challenge guard) are **uncovered**, and one inline line reference is now stale (385 → 429). + This is verification debt accruing in real time, and it is the freshest, most concrete + reason to keep the lane alive. + +Net: continue, but spend the budget on **tooling-independent, fund-protecting work** — +refreshing drifted specs, the one headline solvency property that research showed is now +cheap, CI maturation, and a spec-strength check — not on the confirmed tooling dead-ends. + +## What is genuinely left + +| Item | Status after research | Verdict | +|---|---|---| +| Oracle spec drift (new uncovered branches) | NEW finding — contract changed after spec frozen | **Do first** — fresh debt | +| Track C: aggregate `claimed ≤ pool` (RoundRewardDistributor) | Feasible & cheaper than thought — the sum is already a scalar slot | **High value** | +| Track G: promote fast confs to required PR gate + freshness guard | CI still non-gating (`workflow_dispatch` + cron) | **High value, low effort** | +| Track B: machine-check `paid ≤ cap` end-to-end | Documented solver-completeness gap; correct by inspection | Low priority | +| Track D: QRPE no-double-claim without timeout | NONDET-lib fix not yet attempted; may be blocked by same via_ir/internal-summary limit | Attempt, time-boxed | +| Gambit mutation testing | `certoraMutate` actively maintained; runs against existing specs | Worthwhile assurance check | +| Track A: engine internal-resolution under via_ir | Confirmed hard limit in 8.13.1 (latest); no fix exists | **Escalate only** — file issue, stop | + +## The plan (priority order) + +### 1. Refresh the ClusterPayoutOracle spec to the current contract ← do first + +The contract grew new branches the spec doesn't see. Close the gap: + +- Fix the stale line reference in `ClusterPayoutOracle.spec` (rejected-root guard moved from + `:385` to `:429`). +- Add rules for the **new** rejection surface from `969536f0` / `10ded66c`: + - correlation-epoch root rejection is permanent and blocks replay + (`rejectedCorrelationEpochRoots`, new `rejectedCorrelationEpochSnapshotDigests`); + - the metadata-vs-root split (`rejectCorrelationEpoch` / `rejectCorrelationEpochRoot` / + `rejectFinalizedCorrelationEpoch` / `rejectFinalizedCorrelationEpochRoot`) — each path's + guard fires and is single-use. +- Add a rule for the same-frontend challenge guard (`808570b3`): a challenge from the + proposing frontend reverts. + +**Effort:** low–medium. Reuses the existing full-contract oracle conf; these are +state-gate / single-use rules in the shape the spec already proves. + +### 2. Track C — aggregate `claimed ≤ pool` (headline solvency) + +The single most valuable unproven property: a round's total reward payouts never exceed its +voter pool. Research showed this is **easier than the original ghost+hook plan** because the +aggregate already lives in a scalar: + +- `RoundRewardDistributor.roundVoterRewardClaimedAmount[contentId][roundId]` (`:78`) is the + running sum, written at `:265` and `:597`; the analogous frontend sum is + `roundFrontendClaimedAmount` (`:98`). No `hook Sstore` over a mapping range needed. +- The bound `voterPool` comes from the engine (`votingEngine.rbtsRoundState(...)`, `:248`), + which the distributor specs currently summarize `NONDET`. **Missing piece:** expose + `voterPool` deterministically — add a distributor-side harness getter (the + `RoundVotingEngineHarness` does not expose it today) — then prove the scalar invariant + `roundVoterRewardClaimedAmount[c][r] <= voterPool(c,r)`. +- Mirror the `LaunchDistributionPoolConservation.spec` idiom (counter already *is* the sum) + rather than the hook-heavy `sumOfBalances` pattern. + +**Effort:** medium. Main cost is the harness getter + getting the invariant inductive +(likely needs the `claimedAmount > voterPool` revert at `:256` as an auxiliary fact). + +### 3. Track G — CI maturation: required gate + spec-freshness guard + +`certora.yaml` is still `workflow_dispatch` + weekly cron, non-gating; the run step warns +(not fails) when `CERTORAKEY` is unset. Two steps: + +- Promote the fast, stable confs (`math`, `cluster-payout-oracle`, `loop-reputation`, + `protocol-config`) to a **required, path-filtered PR check**. Keep heavy confs (engine, + escrow, the two excluded QRPE confs) on the weekly schedule + send-only so a slow solver + never blocks a PR. Keep `fail-fast: false`. +- Add a lightweight **spec-freshness guard**: a CI check (or `make` target) that fails when a + contract with a matching spec is changed in a PR without the spec being touched — this is + exactly the drift that produced item 1, and a guard makes it visible instead of silent. + +**Effort:** low. Mostly workflow YAML + a small diff-checking script. + +### 4. Gambit mutation testing (spec-strength check) + +Run `certoraMutate` against the verified confs to measure whether the specs actually catch +injected bugs (a passing spec over a weak property is false assurance). Start with the +cleanest harness-based confs (`frontend-registry`, `feedback-bonus-escrow`, +`loop-reputation`, `math`). Run manually first, record surviving-mutant counts, and only +wire into CI if runtimes are acceptable. Note: the same via_ir/internal-summary constraints +apply to the Prover runs Gambit triggers, so prefer the harness-based (non-via_ir) confs. + +**Effort:** medium. New tooling surface; value is diagnostic, not a new proof. + +### 5. Track B — machine-check `paid ≤ cap` end-to-end (low priority) + +`raterLaunchPaid[r] <= raterLaunchCap[r]` is correct by inspection and covered by two proved +lemmas; only the end-to-end machine proof is missing (nonlinear mul-div the SMT backend won't +discharge). If wanted: add a small pure CVL lemma proving `a*b/c <= a` for `b <= c` once and +apply it to the assignment + the `finalizeEarnedRaterRewardCredit` / `unlockFullEarnedRaterCap` +catch-up paths. Low priority — assurance is already adequate. + +### 6. Track D — QRPE no-double-claim without timeout (attempt, time-boxed) + +The suggested NONDET-summary of the heavy libraries +(`QuestionRewardPoolEscrowQualificationLib/ClaimLib/VoterLib/TransferLib`) is **not yet +applied** — the current specs only NONDET external contract calls. Try it with send-only mode +(`wait_for_results: NONE`, `global_timeout: 7200`). **Risk:** the escrow needs `via_ir`, under +which 8.13.1 cannot instrument internal-function summaries — the same wall as Track A may +apply to internal libraries. Time-box it; if the via_ir/internal-summary error appears, fold +it into the Track A escalation rather than chasing. + +### 7. Track A — escalate, then stop + +Confirmed dead-end in 8.13.1 (the latest). File a Certora forum/support issue with the +already-reduced `_ProbeInternalSummary` repro asking for internal-summary support under +`solc_optimize + via_ir`, link it from `certora-security-findings.md`, and re-test only when +8.14+ ships. No further engineering this round. + +## Suggested sequencing + +``` +1. Oracle spec refresh ← fresh verification debt, do first +2. Track C (aggregate ≤ pool) ← headline solvency, now cheap +3. Track G (CI gate + freshness guard) ← lock in the gains, prevent future drift + ── then, as budget allows ── +4. Gambit (spec-strength check) +5. Track B (paid ≤ cap lemma) ← low priority +6. Track D (QRPE, time-boxed) ← may hit the via_ir wall +7. Track A (file issue, stop) ← no engineering +``` + +Items 1–3 are the core of this round: they are all tooling-independent, fund- or +correctness-protecting, and prevent the spec base from rotting against an active contract +codebase. Items 4–7 are opportunistic. + +## Non-goals (unchanged) + +Still no whole-protocol proof, no off-chain scorer correctness, no economic-game properties, +and no fighting the via_ir/internal-summary tooling limit until a new certora-cli ships. This +round only widens on-chain accounting coverage and keeps the existing proofs honest against a +moving contract base. + +## Sources + +- certora-cli releases (8.13.1 is latest, May 19 2026): https://pypi.org/project/certora-cli/ , + https://docs.certora.com/en/latest/docs/prover/changelog/prover_changelog.html +- CLI options (`function_finder_mode`, `wait_for_results`, `global_timeout`, `nondet_difficult_funcs`): + https://docs.certora.com/en/latest/docs/prover/cli/options.html +- Timeouts guide: https://docs.certora.com/en/latest/docs/user-guide/out-of-resources/timeout.html +- Ghosts/hooks + native ghost-map summation: https://docs.certora.com/en/latest/docs/cvl/ghosts.html +- Require-invariants (inductive strengthening): https://docs.certora.com/en/latest/docs/user-guide/patterns/require-invariants.html +- Gambit / certoraMutate: https://docs.certora.com/en/latest/docs/gambit/index.html , https://github.com/Certora/gambit From 0a14b892e833f9c61271baba65d8cfa7d79b3a73 Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 09:42:16 +0200 Subject: [PATCH 02/12] test(certora): refresh oracle spec for new rejection branches MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ClusterPayoutOracle.sol changed three times (10ded66c, 808570b3, 969536f0) 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 / 10ded66c) — 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 --- .../certora/specs/ClusterPayoutOracle.spec | 44 ++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/packages/foundry/certora/specs/ClusterPayoutOracle.spec b/packages/foundry/certora/specs/ClusterPayoutOracle.spec index 94e409340..8ec79fec8 100644 --- a/packages/foundry/certora/specs/ClusterPayoutOracle.spec +++ b/packages/foundry/certora/specs/ClusterPayoutOracle.spec @@ -10,6 +10,10 @@ * to imply every gate held (pure view properties over arbitrary state). * - rejected-root non-reuse: a blacklisted (snapshotKey, weightRoot) can never be * re-proposed (proposeRoundPayoutSnapshot reverts). + * - rejected correlation-epoch root non-reuse (L-Oracle-4, commit 10ded66c): once an + * epoch's clusterRoot is on the rejected-root blacklist, proposeCorrelationEpoch for + * that exact (epochId, clusterRoot) always reverts. This covers the explicit-root + * rejection path added by rejectCorrelationEpochRoot / rejectFinalizedCorrelationEpochRoot. * - single-use bond-credit withdrawal: a withdrawal zeroes the caller's credit and * an empty withdrawal reverts, so a credit is drawable at most once. * @@ -18,6 +22,11 @@ * - rejected digest non-reuse and the consumed-slot permanent-death guard * - challenge-window finalization timing * - parent correlation-epoch rejection cascade + * - the metadata-vs-root rejection split (rejectCorrelationEpoch keeps the deterministic + * root re-proposable; only the *Root variants blacklist it) — proving the metadata path + * does NOT blacklist needs a getter for the snapshot's stored clusterRoot (private struct) + * - the disinterested-challenger guard (a proposer/frontend-operator cannot self-challenge, + * commit 808570b3) — reads the private snapshot struct's proposer/frontendOperator fields * See docs/testing/certora.md (Phase 2). */ @@ -31,6 +40,8 @@ methods { function rejectedRoundPayoutSnapshotDigests(bytes32, bytes32) external returns (bool) envfree; function rejectedRoundPayoutSnapshotConsumed(bytes32) external returns (bool) envfree; function rejectedCorrelationEpochRoots(uint256, bytes32) external returns (bool) envfree; + function rejectedCorrelationEpochRootKeys(bytes32) external returns (bool) envfree; + function rejectedCorrelationEpochSnapshotDigests(uint256, bytes32) external returns (bool) envfree; // Summarize the external dependencies (frontend registry, snapshot consumer, // bond ERC20) as NONDET so a call to them cannot havoc THIS contract's storage. @@ -48,7 +59,7 @@ methods { // --------------------------------------------------------------------------- // Rejected roots cannot be reused: once a (snapshotKey, weightRoot) pair is on // the rejected-root blacklist, proposeRoundPayoutSnapshot for that exact root -// always reverts (guard at ClusterPayoutOracle.sol:385). The blacklists are only +// always reverts (guard at ClusterPayoutOracle.sol:429). The blacklists are only // ever written `true` and never cleared, so a rejected root stays unproposable. // --------------------------------------------------------------------------- @@ -59,6 +70,37 @@ rule cannotReproposeRejectedRoot(env e, IClusterPayoutOracle.RoundPayoutSnapshot assert lastReverted; } +// --------------------------------------------------------------------------- +// Same guarantee one level up, for correlation epochs (L-Oracle-4, commit +// 10ded66c "Block replay of rejected correlation roots"): once an epoch's +// clusterRoot is blacklisted via rejectCorrelationEpochRoot / +// rejectFinalizedCorrelationEpochRoot, proposeCorrelationEpoch for that exact +// (epochId, clusterRoot) always reverts at the guard on +// ClusterPayoutOracle.sol:267-272. This is the contrapositive of that guard's +// first disjunct; the blacklist is only ever written `true`, so the block is +// permanent. (The second disjunct — the source-set-keyed rootKeys mapping — is +// not asserted here because its key derives from the internally-computed +// sourceSetDigest, which cannot be matched from calldata.) +// --------------------------------------------------------------------------- + +rule cannotReproposeRejectedCorrelationEpochRoot( + env e, + uint64 epochId, + uint64 fromRoundId, + uint64 toRoundId, + bytes32 clusterRoot, + bytes32 parameterHash, + bytes32 artifactHash, + string artifactURI, + IClusterPayoutOracle.CorrelationEpochSourceRef[] sourceRefs +) { + require rejectedCorrelationEpochRoots(require_uint256(epochId), clusterRoot); + proposeCorrelationEpoch@withrevert( + e, epochId, fromRoundId, toRoundId, clusterRoot, parameterHash, artifactHash, artifactURI, sourceRefs + ); + assert lastReverted; +} + // --------------------------------------------------------------------------- // Bond-credit withdrawal is single-use: a successful withdrawal zeroes the // caller's credit, and a withdrawal with no credit reverts. Together these mean a From 97937a646c8d4ecf1e444a674e60bb56d7743a79 Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 13:01:22 +0200 Subject: [PATCH 03/12] test(certora): Track C aggregate-conservation slice + mul-div lemma MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../foundry/certora/confs/mul-div-lemma.conf | 13 ++++ ...round-reward-distributor-conservation.conf | 9 +++ .../foundry/certora/specs/MulDivLemma.spec | 55 +++++++++++++ .../RoundRewardDistributorConservation.spec | 78 +++++++++++++++++++ 4 files changed, 155 insertions(+) create mode 100644 packages/foundry/certora/confs/mul-div-lemma.conf create mode 100644 packages/foundry/certora/confs/round-reward-distributor-conservation.conf create mode 100644 packages/foundry/certora/specs/MulDivLemma.spec create mode 100644 packages/foundry/certora/specs/RoundRewardDistributorConservation.spec diff --git a/packages/foundry/certora/confs/mul-div-lemma.conf b/packages/foundry/certora/confs/mul-div-lemma.conf new file mode 100644 index 000000000..b941850b4 --- /dev/null +++ b/packages/foundry/certora/confs/mul-div-lemma.conf @@ -0,0 +1,13 @@ +{ + // Track B/C primitive: the nonlinear (a*b)/c <= a bound. Inherits compiler/prover + // settings from base.conf; overrides via_ir off (pure-arithmetic, no IR codegen + // needed, mirrors math.conf) and enables the nonlinear-arithmetic SMT backend so + // the multiply-then-divide inequality is dischargeable (see MulDivLemma.spec and + // docs/testing/certora-security-findings.md). + "override_base_config": "certora/confs/base.conf", + "solc_via_ir": false, + "files": ["certora/harnesses/MathHarness.sol"], + "verify": "MathHarness:certora/specs/MulDivLemma.spec", + "prover_args": ["-smt_useNIA true"], + "msg": "RateLoop mul-div conservation lemma (Track B/C primitive)" +} diff --git a/packages/foundry/certora/confs/round-reward-distributor-conservation.conf b/packages/foundry/certora/confs/round-reward-distributor-conservation.conf new file mode 100644 index 000000000..770f04a5b --- /dev/null +++ b/packages/foundry/certora/confs/round-reward-distributor-conservation.conf @@ -0,0 +1,9 @@ +{ + // Track C (aggregate solvency, slice 1): RoundRewardDistributor per-round claimed-amount + // monotonicity (no clawback / no underflow). Inherits compiler/prover settings from + // base.conf. Run with: certoraRun certora/confs/round-reward-distributor-conservation.conf + "override_base_config": "certora/confs/base.conf", + "files": ["contracts/RoundRewardDistributor.sol"], + "verify": "RoundRewardDistributor:certora/specs/RoundRewardDistributorConservation.spec", + "msg": "RateLoop Track C RoundRewardDistributor conservation (monotonicity slice)" +} diff --git a/packages/foundry/certora/specs/MulDivLemma.spec b/packages/foundry/certora/specs/MulDivLemma.spec new file mode 100644 index 000000000..ad2d4d8d7 --- /dev/null +++ b/packages/foundry/certora/specs/MulDivLemma.spec @@ -0,0 +1,55 @@ +/* + * MulDivLemma.spec — reusable nonlinear multiply-then-divide bound. + * + * Proves the floor-division primitive `(a * b) / c <= a` for `b <= c`, `c != 0` + * (and the exact corollary `(a * c) / c == a`). This is the single arithmetic + * fact that every "a proportional share never exceeds its pool/cap" conservation + * property in the protocol reduces to: + * + * - RewardMath.calculateVoterReward = (voterPool * stake) / totalStake + * <= voterPool when stake <= totalStake (RoundRewardDistributor) + * - LaunchDistributionPool cap = (fullCap * bps) / 10000 + * <= fullCap when bps <= 10000 (Track B) + * + * docs/testing/certora-security-findings.md records `(fullCap * bps) / 10000 <= fullCap` + * as a deferred gap because the default *linear* SMT backend cannot discharge a + * nonlinear multiply-then-divide. That doc's own re-run note ("`-smt_useNIA` ... + * discharged the assignment multiplication") is the evidence this lemma is provable + * once nonlinear arithmetic is enabled — which this conf does via prover_args. + * + * The rule calls no contract function: it is pure CVL integer arithmetic over the + * mathematical integers (to_mathint avoids any 256-bit wraparound, so the bound is + * the true mathematical one, which equals the EVM result on the non-overflowing + * inputs these formulas are fed). MathHarness is named only because `verify` needs + * a contract to attach to. + */ + +methods { + // No contract methods are exercised; the lemma is self-contained arithmetic. +} + +// Floor of (a*b)/c is at most a whenever b <= c (c != 0). The workhorse lemma. +rule mulDivAtMost(uint256 a, uint256 b, uint256 c) { + require c != 0; + require b <= c; + mathint product = to_mathint(a) * to_mathint(b); + assert product / to_mathint(c) <= to_mathint(a); +} + +// Exact corollary: a full-fraction allocation (b == c) returns a unchanged. This +// is the boundary the cap/pool clamps lean on (full cap, 100% bps, last claimant). +rule mulDivExactWhenFull(uint256 a, uint256 c) { + require c != 0; + mathint product = to_mathint(a) * to_mathint(c); + assert product / to_mathint(c) == to_mathint(a); +} + +// Monotonicity in the numerator factor: a larger share weight never yields a +// smaller payout. Underpins "a claimant's reward tracks its weight" reasoning. +rule mulDivMonotoneInB(uint256 a, uint256 b1, uint256 b2, uint256 c) { + require c != 0; + require b1 <= b2; + mathint p1 = to_mathint(a) * to_mathint(b1); + mathint p2 = to_mathint(a) * to_mathint(b2); + assert p1 / to_mathint(c) <= p2 / to_mathint(c); +} diff --git a/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec b/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec new file mode 100644 index 000000000..8e7e4ddd1 --- /dev/null +++ b/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec @@ -0,0 +1,78 @@ +/* + * RoundRewardDistributorConservation.spec — Track C (aggregate solvency, slice 1). + * + * Verification target: contracts/RoundRewardDistributor.sol (verified directly). + * Run with: certoraRun certora/confs/round-reward-distributor-conservation.conf + * + * The headline solvency property is "the sum of all voter-reward payouts for a round + * never exceeds that round's voterPool". The running sum lives in the scalar slot + * roundVoterRewardClaimedAmount[contentId][roundId] (written at RoundRewardDistributor.sol + * :265 as `claimedAmount + reward` and at :597 as `+= releasedDust`), so the property is + * `roundVoterRewardClaimedAmount[c][r] <= voterPool(c,r)`. + * + * What is proved here (engine-model-free, robust): + * - the accumulator is MONOTONE: neither a voter claim nor dust finalization can ever + * decrease it. Every write adds a non-negative amount or reverts. This is the + * no-clawback / no-underflow half of conservation and the inductive scaffold the + * upper bound builds on. + * + * Why the upper bound itself is NOT proved here (deferred, with the gap made explicit): + * The per-claimant increment is a PROPORTIONAL share, + * reward = RewardMath.calculateVoterReward(scoreWeight, totalScoreWeight, voterPool) + * = (voterPool * scoreWeight) / totalScoreWeight, + * so `sum(reward) <= voterPool` holds only because `sum(scoreWeight) <= totalScoreWeight` + * across claimants — an aggregate over engine state, not a distributor-storage fact. + * The two pieces it factors into ARE addressed elsewhere: + * - the single-claimant bound `(voterPool * scoreWeight)/totalScoreWeight <= voterPool` + * (for scoreWeight <= totalScoreWeight) is the mul-div lemma in MulDivLemma.spec; + * - the last-claimant settlement pays exactly `voterPool - claimedAmount` (:262), + * landing the sum on voterPool exactly. + * The remaining gap is the score-weight summation invariant across the engine's + * per-commit state, which needs a faithful engine model rather than the NONDET + * summaries used here. Tracked in docs/testing/certora-round3-plan.md (Track C). + * + * The engine payout (transferReward) and the LREP token transfer are summarized NONDET + * exactly as RoundRewardDistributor.spec does: the distributor never custodies rewards, + * so those calls cannot write its accumulators, and havoc'd engine view returns only make + * the monotonicity argument stronger (it holds for every possible voterPool). + */ + +methods { + function roundVoterRewardClaimedAmount(uint256, uint256) external returns (uint256) envfree; + function roundFrontendClaimedAmount(uint256, uint256) external returns (uint256) envfree; + + function _.transferReward(address, uint256) external => NONDET; + function _.transfer(address, uint256) external => NONDET; +} + +// A voter claim never decreases the per-round claimed-amount accumulator (any round). +// The only write is `claimedAmount + reward` with reward >= 0; every other path reverts. +rule claimRewardNeverDecreasesClaimedAmount(env e, uint256 contentId, uint256 roundId, uint256 c, uint256 r) { + uint256 before = roundVoterRewardClaimedAmount(c, r); + claimReward(e, contentId, roundId); + assert roundVoterRewardClaimedAmount(c, r) >= before; +} + +// Dust finalization never decreases the accumulator either: it adds releasedDust (> 0, +// or the call reverts with NoRewardDust). Together with the rule above, the per-round +// voter-reward sum is non-decreasing across the whole claim lifecycle. +rule dustFinalizationNeverDecreasesClaimedAmount( + env e, + uint256 contentId, + uint256 roundId, + address[] sortedWinningVoters, + uint256 c, + uint256 r +) { + uint256 before = roundVoterRewardClaimedAmount(c, r); + finalizeVoterRewardDust(e, contentId, roundId, sortedWinningVoters); + assert roundVoterRewardClaimedAmount(c, r) >= before; +} + +// Symmetric monotonicity for the frontend-fee accumulator (RoundRewardDistributor.sol:98), +// which follows the same add-or-revert discipline as the voter accumulator. +rule frontendClaimNeverDecreasesClaimedAmount(env e, method f, calldataarg args, uint256 c, uint256 r) { + uint256 before = roundFrontendClaimedAmount(c, r); + f(e, args); + assert roundFrontendClaimedAmount(c, r) >= before; +} From b7344175d60a7c821e6487b8c71028935e90758d Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 13:04:18 +0200 Subject: [PATCH 04/12] ci(certora): add secret-free type-check gate + spec-freshness guard (Track G) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .github/workflows/certora.yaml | 100 ++++++++++- .../certora/scripts/check_spec_freshness.py | 162 ++++++++++++++++++ 2 files changed, 256 insertions(+), 6 deletions(-) create mode 100755 packages/foundry/certora/scripts/check_spec_freshness.py diff --git a/.github/workflows/certora.yaml b/.github/workflows/certora.yaml index 2a2230f5e..b61ed756e 100644 --- a/.github/workflows/certora.yaml +++ b/.github/workflows/certora.yaml @@ -1,9 +1,19 @@ name: Certora -# Formal verification lane. Runs on demand, on a weekly schedule, and on PRs that touch -# contracts or the Certora workspace. NOT a required PR gate yet (no branch protection): -# it stays informational until prover runtimes and false-positive rates are understood -# across the full matrix (see docs/testing/certora-followup.md "CI maturation"). +# Formal verification lane. Three jobs with different gating intent: +# +# certora-check — compile + CVL type-check every conf. No CERTORAKEY, no cloud, +# deterministic and fast. This is the lane's REQUIRED-gate candidate: +# it catches spec/contract signature drift (the failure that left +# ClusterPayoutOracle.spec stale behind three contract commits). +# spec-freshness — on PRs, fail if a contract with Certora coverage changed without +# its spec being reviewed (bypass with [spec-ok] in the PR title/body). +# certora — the full cloud prover matrix. Needs the CERTORAKEY secret and runs +# for minutes-to-hours, so it stays NON-gating (informational) until +# runtimes/false-positive rates are understood; promote the fast confs +# (math, cluster-payout-oracle, loop-reputation, protocol-config, +# mul-div-lemma) to required cloud runs once stable. See +# docs/testing/certora-round3-plan.md (Track G). on: workflow_dispatch: @@ -25,6 +35,80 @@ env: SOLC_VERSION: "0.8.35" jobs: + # --------------------------------------------------------------------------- + # Required-gate candidate: compile + CVL type-check, no secret, no cloud run. + # --------------------------------------------------------------------------- + certora-check: + runs-on: ubuntu-latest + name: certora-check (compile + typecheck) + steps: + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + with: + submodules: true + + - uses: ./.github/actions/setup-foundry + + - name: Install Java 21 + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends openjdk-21-jre-headless + java --version + + - name: Install Certora CLI and solc + run: | + python3 -m pip install --upgrade pip + python3 -m pip install "certora-cli${CERTORA_CLI_VERSION}" solc-select + solc-select install "$SOLC_VERSION" + solc-select use "$SOLC_VERSION" + certoraRun --version + solc --version + + - name: Compile + type-check every conf + working-directory: packages/foundry + run: | + set -uo pipefail + failed=() + for conf in certora/confs/*.conf; do + [ "$(basename "$conf")" = "base.conf" ] && continue + echo "::group::$conf" + if certoraRun "$conf" --compilation_steps_only; then + echo "OK: $conf" + else + echo "::error::compile/type-check failed: $conf" + failed+=("$conf") + fi + echo "::endgroup::" + done + if [ "${#failed[@]}" -ne 0 ]; then + echo "Type-check failed for: ${failed[*]}" + exit 1 + fi + echo "All confs compiled and type-checked." + + # --------------------------------------------------------------------------- + # PR guard: a covered contract may not change without its spec being reviewed. + # --------------------------------------------------------------------------- + spec-freshness: + runs-on: ubuntu-latest + if: github.event_name == 'pull_request' + name: spec-freshness + steps: + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + with: + fetch-depth: 0 + + - name: Check spec freshness vs. contract changes + env: + BASE_REF: ${{ github.base_ref }} + SPEC_FRESHNESS_OVERRIDE: "${{ github.event.pull_request.title }} ${{ github.event.pull_request.body }}" + run: | + git fetch --no-tags --depth=1 origin "$BASE_REF" + git diff --name-only "origin/${BASE_REF}...HEAD" \ + | python3 packages/foundry/certora/scripts/check_spec_freshness.py --changed-stdin + + # --------------------------------------------------------------------------- + # Full cloud prover matrix (non-gating; needs the CERTORAKEY secret). + # --------------------------------------------------------------------------- certora: runs-on: ubuntu-latest strategy: @@ -32,9 +116,11 @@ jobs: matrix: conf: - certora/confs/math.conf + - certora/confs/mul-div-lemma.conf - certora/confs/cluster-payout-oracle.conf - certora/confs/round-voting-engine.conf - certora/confs/round-reward-distributor.conf + - certora/confs/round-reward-distributor-conservation.conf - certora/confs/no-double-claim.conf - certora/confs/round-voting-engine-lifecycle.conf - certora/confs/launch-distribution-pool.conf @@ -45,8 +131,10 @@ jobs: - certora/confs/launch-distribution-pool-cap.conf - certora/confs/launch-distribution-pool-conservation.conf # NOTE: question-reward-escrow.conf and question-reward-escrow-claim.conf are - # intentionally excluded — both exceed certora-cli's 15-minute output window on - # this 1,490-line + 11-library contract. Run them manually with a larger budget. + # intentionally excluded from the proof matrix — both exceed certora-cli's + # 15-minute output window on this 1,490-line + 11-library contract. Run them + # manually with a larger budget. (They are still compile/type-checked by the + # certora-check job above.) name: ${{ matrix.conf }} steps: - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 diff --git a/packages/foundry/certora/scripts/check_spec_freshness.py b/packages/foundry/certora/scripts/check_spec_freshness.py new file mode 100755 index 000000000..7c05f9a90 --- /dev/null +++ b/packages/foundry/certora/scripts/check_spec_freshness.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +"""Spec-freshness guard for the Certora lane. + +Fails when a contract that has Certora coverage is changed in a PR without its +spec being touched — the exact drift that left ClusterPayoutOracle.spec stale +behind three contract commits (see docs/testing/certora-round3-plan.md, Track G). + +The contract -> spec(s) map is derived from the conf files themselves (no second +source of truth to keep in sync): + - each conf's `verify` key names the spec; + - each conf's `files` list names the verification targets. A target under + contracts/ is a direct dependency; a target under certora/harnesses/ is + resolved to the contracts/ files it imports, so harness-based confs + (FrontendRegistry, FeedbackBonusEscrow, ...) are covered too. + +Usage: + check_spec_freshness.py --changed-from # diff ...HEAD + check_spec_freshness.py --changed-file # newline-listed paths + git diff --name-only BASE...HEAD | check_spec_freshness.py --changed-stdin + +Escape hatch (for intentional contract-only changes that don't affect proven +properties): include the literal token [spec-ok] anywhere in the environment +variable SPEC_FRESHNESS_OVERRIDE (the workflow wires this to the PR title/body). +""" + +from __future__ import annotations + +import argparse +import json +import os +import re +import subprocess +import sys +from pathlib import Path + +# Repo-root-relative location of the foundry package and the certora workspace. +FOUNDRY = "packages/foundry" +CONFS_DIR = Path(FOUNDRY) / "certora" / "confs" + + +def strip_jsonc(text: str) -> str: + """Remove // line comments so the commented conf files parse as JSON.""" + out = [] + for line in text.splitlines(): + # Only strip // that is not inside a string. The confs only ever use // + # at the start of a (possibly indented) line or after a value, never + # inside string literals, so a simple heuristic is safe here. + in_str = False + result = [] + i = 0 + while i < len(line): + ch = line[i] + if ch == '"': + in_str = not in_str + if not in_str and ch == "/" and i + 1 < len(line) and line[i + 1] == "/": + break + result.append(ch) + i += 1 + out.append("".join(result)) + return "\n".join(out) + + +def harness_contract_deps(harness_rel: str) -> list[str]: + """contracts/ files imported by a harness, as FOUNDRY-relative paths.""" + harness_path = Path(FOUNDRY) / harness_rel + deps: list[str] = [] + if not harness_path.exists(): + return deps + text = harness_path.read_text() + for m in re.finditer(r'import\s*\{[^}]*\}\s*from\s*"([^"]+)"', text): + target = m.group(1) + # Harnesses live in certora/harnesses/, so ../../contracts/X.sol -> contracts/X.sol + if "contracts/" in target: + normalized = "contracts/" + target.split("contracts/", 1)[1] + deps.append(normalized) + return deps + + +def build_map() -> dict[str, set[str]]: + """contract path (FOUNDRY-relative) -> set of spec paths (FOUNDRY-relative).""" + mapping: dict[str, set[str]] = {} + for conf in sorted(CONFS_DIR.glob("*.conf")): + if conf.name == "base.conf": + continue + data = json.loads(strip_jsonc(conf.read_text())) + verify = data.get("verify", "") + if ":" not in verify: + continue + spec = verify.split(":", 1)[1] + targets = data.get("files", []) + deps: set[str] = set() + for target in targets: + if target.startswith("contracts/"): + deps.add(target) + elif "harnesses/" in target: + deps.update(harness_contract_deps(target)) + for dep in deps: + mapping.setdefault(dep, set()).add(spec) + return mapping + + +def changed_files(args: argparse.Namespace) -> list[str]: + if args.changed_stdin: + return [l.strip() for l in sys.stdin if l.strip()] + if args.changed_file: + return [l.strip() for l in Path(args.changed_file).read_text().splitlines() if l.strip()] + if args.changed_from: + out = subprocess.run( + ["git", "diff", "--name-only", f"{args.changed_from}...HEAD"], + capture_output=True, text=True, check=True, + ).stdout + return [l.strip() for l in out.splitlines() if l.strip()] + raise SystemExit("one of --changed-from/--changed-file/--changed-stdin is required") + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--changed-from", help="git ref; diff ...HEAD for changed files") + parser.add_argument("--changed-file", help="file containing newline-separated changed paths") + parser.add_argument("--changed-stdin", action="store_true", help="read changed paths from stdin") + args = parser.parse_args() + + override = os.environ.get("SPEC_FRESHNESS_OVERRIDE", "") + if "[spec-ok]" in override: + print("spec-freshness: [spec-ok] override present — skipping check.") + return 0 + + mapping = build_map() + changed = set(changed_files(args)) + # Normalize conf-relative (FOUNDRY-relative) paths to repo-root-relative. + changed_foundry = { + c[len(FOUNDRY) + 1:] for c in changed if c.startswith(FOUNDRY + "/") + } + + stale: list[tuple[str, list[str]]] = [] + for contract, specs in sorted(mapping.items()): + if contract not in changed_foundry: + continue + if specs & changed_foundry: + continue # at least one covering spec was touched — OK + stale.append((contract, sorted(specs))) + + if not stale: + print("spec-freshness: OK — every changed covered contract had its spec reviewed.") + return 0 + + print("spec-freshness: FAIL — covered contract(s) changed without touching the spec.\n") + for contract, specs in stale: + spec_list = ", ".join(s.replace("certora/specs/", "") for s in specs) + msg = f"{contract} changed but its Certora spec(s) were not: {spec_list}" + print(f" - {msg}") + # GitHub Actions annotation. + print(f"::error file={FOUNDRY}/{contract}::{msg}") + print( + "\nReview the spec against the contract change. If the change genuinely does " + "not affect any proven property, add [spec-ok] to the PR title or body to bypass." + ) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) From 894dbd4483dc967c2538d9be8934bf328abbda30 Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 13:07:15 +0200 Subject: [PATCH 05/12] test(certora): wire up Gambit mutation testing (spec-strength check) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- packages/foundry/Makefile | 9 ++- packages/foundry/certora/mutation/README.md | 55 +++++++++++++++++++ .../feedback-bonus-escrow.mutation.conf | 17 ++++++ .../mutation/frontend-registry.mutation.conf | 22 ++++++++ .../mutation/reward-math.mutation.conf | 17 ++++++ 5 files changed, 119 insertions(+), 1 deletion(-) create mode 100644 packages/foundry/certora/mutation/README.md create mode 100644 packages/foundry/certora/mutation/feedback-bonus-escrow.mutation.conf create mode 100644 packages/foundry/certora/mutation/frontend-registry.mutation.conf create mode 100644 packages/foundry/certora/mutation/reward-math.mutation.conf diff --git a/packages/foundry/Makefile b/packages/foundry/Makefile index 7e28ea8ee..6253ead6b 100644 --- a/packages/foundry/Makefile +++ b/packages/foundry/Makefile @@ -1,4 +1,4 @@ -.PHONY: build deploy deploy-and-generate-abis generate-abis get-address account chain compile compile-all flatten fork format lint test verify verify-blockscout slither aderyn certora certora-check coverage check-contract-sizes check-storage-layouts snapshot-storage-layouts +.PHONY: build deploy deploy-and-generate-abis generate-abis get-address account chain compile compile-all flatten fork format lint test verify verify-blockscout slither aderyn certora certora-check certora-mutate coverage check-contract-sizes check-storage-layouts snapshot-storage-layouts TEST_ARGS ?= COVERAGE_ARGS ?= @@ -126,6 +126,8 @@ aderyn: # "override_base_config" key; certoraRun takes a single conf file. CERTORA_CONF ?= certora/confs/math.conf CERTORA_ARGS ?= +# Gambit mutation-testing target (spec strength). See certora/mutation/README.md. +MUTATION_CONF ?= certora/mutation/frontend-registry.mutation.conf certora: certoraRun $(CERTORA_CONF) $(CERTORA_ARGS) @@ -133,6 +135,11 @@ certora: certora-check: certoraRun $(CERTORA_CONF) --compilation_steps_only $(CERTORA_ARGS) +# Mutation testing: inject contract mutants and re-verify each against the spec. +# Needs CERTORAKEY (one prover job per mutant); run manually, not in CI. +certora-mutate: + certoraMutate $(MUTATION_CONF) $(CERTORA_ARGS) + coverage: forge coverage --offline --ir-minimum $(COVERAGE_ARGS) diff --git a/packages/foundry/certora/mutation/README.md b/packages/foundry/certora/mutation/README.md new file mode 100644 index 000000000..67c2b4647 --- /dev/null +++ b/packages/foundry/certora/mutation/README.md @@ -0,0 +1,55 @@ +# Gambit mutation testing + +Mutation testing measures **spec strength**: a passing Certora spec only means "no +counterexample to the rules as written." It does *not* tell you whether the rules are +strong enough to catch a real bug. [Gambit](https://docs.certora.com/en/latest/docs/gambit/index.html) +(bundled with `certora-cli`) answers that — it injects small mutations into a contract +and `certoraMutate` re-runs the Prover against each mutant: + +- a **killed** mutant = a rule failed on the broken code = the spec caught it (good); +- a **surviving** mutant = every rule still passed on broken code = the spec + under-constrains that line (a weak-spec signal to investigate — *not* a contract bug). + +## Running + +Each mutant is a full Prover job, so this needs `CERTORAKEY` and is run **manually**, not +in CI. From `packages/foundry`: + +```sh +export CERTORAKEY= + +make certora-mutate # default: FrontendRegistry +make certora-mutate MUTATION_CONF=certora/mutation/feedback-bonus-escrow.mutation.conf +make certora-mutate MUTATION_CONF=certora/mutation/reward-math.mutation.conf + +# or directly: +certoraMutate certora/mutation/frontend-registry.mutation.conf +``` + +`certoraMutate` prints a dashboard link; the report lists each mutant and whether it was +killed or survived. + +## Targets chosen first + +The confs here are the cleanest starting points — all **harness-based and `via_ir`-free**, +so they dodge the internal-summary tooling limits that block the heavier contracts, and +their proofs are fast enough for a full mutant sweep: + +| Mutation conf | Contract mutated | Spec under test | +|---|---|---| +| `frontend-registry.mutation.conf` | `FrontendRegistry.sol` | stake/slash conservation | +| `feedback-bonus-escrow.mutation.conf` | `FeedbackBonusEscrow.sol` | bonus conservation + single-award | +| `reward-math.mutation.conf` | `libraries/RewardMath.sol` | Math.spec conservation/bounds/monotonicity | + +## Interpreting results + +Record surviving-mutant counts per run. A survivor usually means one of: + +1. the mutated line is not covered by any rule → add a rule, or +2. a rule is too weak (e.g. asserts `>= 0` where `<= cap` was intended) → tighten it, or +3. the mutation is equivalent (semantically identical code) → no action, note it. + +Only wire a target into CI once its runtime is known and its survivor set is triaged to +"covered or equivalent". Heavy / `via_ir` contracts (engine, escrow) are intentionally not +listed yet — the same internal-summary constraints from the proof lane apply to the +Prover runs Gambit triggers. diff --git a/packages/foundry/certora/mutation/feedback-bonus-escrow.mutation.conf b/packages/foundry/certora/mutation/feedback-bonus-escrow.mutation.conf new file mode 100644 index 000000000..4c6f4362d --- /dev/null +++ b/packages/foundry/certora/mutation/feedback-bonus-escrow.mutation.conf @@ -0,0 +1,17 @@ +{ + // Gambit mutation run for the FeedbackBonusEscrow conservation proofs. + // See certora/mutation/README.md and frontend-registry.mutation.conf for how + // surviving mutants are interpreted (weak-spec signal). + // + // Run from packages/foundry (needs CERTORAKEY): + // certoraMutate certora/mutation/feedback-bonus-escrow.mutation.conf + "prover_conf": "certora/confs/feedback-bonus-escrow.conf", + "mutations": { + "gambit": [ + { + "filename": "contracts/FeedbackBonusEscrow.sol" + } + ] + }, + "msg": "FeedbackBonusEscrow spec-strength mutation run" +} diff --git a/packages/foundry/certora/mutation/frontend-registry.mutation.conf b/packages/foundry/certora/mutation/frontend-registry.mutation.conf new file mode 100644 index 000000000..168a0a253 --- /dev/null +++ b/packages/foundry/certora/mutation/frontend-registry.mutation.conf @@ -0,0 +1,22 @@ +{ + // Gambit mutation run for the FrontendRegistry stake/slash proofs. + // Measures whether FrontendRegistry.spec actually CATCHES injected bugs: Gambit + // generates mutants of the contract, and certoraMutate verifies each against the + // spec via the Prover. A SURVIVING mutant (all rules still pass on broken code) + // means the spec under-constrains that line — a weak-spec signal, not a contract bug. + // + // Run from packages/foundry (needs CERTORAKEY — each mutant is a full prover job): + // certoraMutate certora/mutation/frontend-registry.mutation.conf + // + // Chosen as a first target because it is harness-based and via_ir-free (no internal- + // summary tooling limits) and the proofs are fast, so a full mutant sweep is cheap. + "prover_conf": "certora/confs/frontend-registry.conf", + "mutations": { + "gambit": [ + { + "filename": "contracts/FrontendRegistry.sol" + } + ] + }, + "msg": "FrontendRegistry spec-strength mutation run" +} diff --git a/packages/foundry/certora/mutation/reward-math.mutation.conf b/packages/foundry/certora/mutation/reward-math.mutation.conf new file mode 100644 index 000000000..2cc94c11f --- /dev/null +++ b/packages/foundry/certora/mutation/reward-math.mutation.conf @@ -0,0 +1,17 @@ +{ + // Gambit mutation run for the pure math libraries (Math.spec). Mutating RewardMath + // exercises the conservation/bounds/monotonicity rules and the calculateVoterReward + // path that the mul-div lemma underpins. via_ir-free and fast. + // + // Run from packages/foundry (needs CERTORAKEY): + // certoraMutate certora/mutation/reward-math.mutation.conf + "prover_conf": "certora/confs/math.conf", + "mutations": { + "gambit": [ + { + "filename": "contracts/libraries/RewardMath.sol" + } + ] + }, + "msg": "RewardMath spec-strength mutation run" +} From a5ca44514ac92a1433c59b12c68e36e6a979467e Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 13:09:59 +0200 Subject: [PATCH 06/12] test(certora): machine-check the launch cap-assignment clamp (Track B) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../confs/launch-distribution-pool-cap.conf | 4 +++ .../LaunchDistributionPoolHarness.sol | 9 ++++++ .../specs/LaunchDistributionPoolCap.spec | 32 +++++++++++++++---- 3 files changed, 38 insertions(+), 7 deletions(-) diff --git a/packages/foundry/certora/confs/launch-distribution-pool-cap.conf b/packages/foundry/certora/confs/launch-distribution-pool-cap.conf index 39f154a12..b739e0c19 100644 --- a/packages/foundry/certora/confs/launch-distribution-pool-cap.conf +++ b/packages/foundry/certora/confs/launch-distribution-pool-cap.conf @@ -5,5 +5,9 @@ "override_base_config": "certora/confs/base.conf", "files": ["certora/harnesses/LaunchDistributionPoolHarness.sol"], "verify": "LaunchDistributionPoolHarness:certora/specs/LaunchDistributionPoolCap.spec", + // Enable the nonlinear-arithmetic SMT backend so the cap-assignment clamp + // (fullCap * bps) / 10000 <= fullCap (rule assignedCapWithinFullCap) is dischargeable; + // the default linear backend cannot (see certora-security-findings.md). + "prover_args": ["-smt_useNIA true"], "msg": "RateLoop Phase 5b LaunchDistributionPool cap invariant" } diff --git a/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol b/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol index 0604bc325..ee0b55ad8 100644 --- a/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol +++ b/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol @@ -16,4 +16,13 @@ contract LaunchDistributionPoolHarness is LaunchDistributionPool { function unverifiedCapBps_() external view returns (uint256) { return uint256(launchRewardPolicy.unverifiedEarnedRaterCapBps); } + + /// @notice Exposes the internal cap-assignment so the spec can machine-check the + /// clamp `activeCap <= fullCap` directly at the point it is computed + /// (`activeCap = (fullCap * bps) / BPS_DENOMINATOR`, or `fullCap` when the + /// full cap is unlocked). Uses the live policy, so `unverifiedCapBps_()` + /// is the bps the spec constrains <= 10000. See LaunchDistributionPoolCap.spec. + function assignLaunchCap_(address rater, uint256 fullCap) external returns (uint256 activeCap) { + (activeCap,) = _assignLaunchCap(rater, fullCap, launchRewardPolicy); + } } diff --git a/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec b/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec index 7c25cf7c6..6d7bb6663 100644 --- a/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec +++ b/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec @@ -13,13 +13,20 @@ * capAssignedWhenPaid — any rater with a non-zero paid-out amount has an assigned cap * (every payout path assigns the cap before paying). * - * The headline `raterLaunchPaid <= raterLaunchCap` itself remains deferred. Its last - * missing lemma is `raterLaunchCap <= raterFullLaunchCap`, which at assignment reduces to - * `fullCap * bps / 10000 <= fullCap` given `bps <= 10000`. That is a nonlinear - * multiply-then-divide inequality, which the SMT backend cannot discharge precisely (a - * solver-completeness limit, not a contract defect — by inspection the clamp is correct). - * Proving it would need a manual nonlinear lemma or a mul-div abstraction. The two - * invariants below are the sound, machine-checked part of the chain. + * The previously-deferred lemma `raterLaunchCap <= raterFullLaunchCap` reduces at + * assignment to `fullCap * bps / 10000 <= fullCap` given `bps <= 10000` — a nonlinear + * multiply-then-divide the *linear* SMT backend cannot discharge. This conf now enables + * the nonlinear-arithmetic backend (`-smt_useNIA`), under which the assignment clamp IS + * dischargeable (docs/testing/certora-security-findings.md confirmed NIA discharges the + * assignment multiply). `assignedCapWithinFullCap` below machine-checks exactly that clamp + * at the point it is computed, via the harness wrapper `assignLaunchCap_`. + * + * Still deferred (honest residual): the *global* invariant `raterLaunchPaid <= raterLaunchCap` + * over every method. Per the findings doc, even with NIA the catch-up paths + * (finalizeEarnedRaterRewardCredit / unlockFullEarnedRaterCap) — which contain further + * cap * count / rewardingCount mul-div sites — still resist as a standalone inductive + * invariant. So this slice proves the per-assignment clamp (the load-bearing step) rather + * than the end-to-end invariant. See docs/testing/certora-round3-plan.md (Track B). */ methods { @@ -44,3 +51,14 @@ invariant policyBpsBounded() // Any rater that has been paid has an assigned cap (every payout path assigns first). invariant capAssignedWhenPaid(address r) raterLaunchPaid(r) > 0 => raterLaunchCapAssigned(r); + +// The cap-assignment clamp: the active cap computed at assignment never exceeds the full +// cap. This is the load-bearing mul-div step (activeCap = (fullCap * bps) / 10000 when the +// full cap is locked, else fullCap), the real-contract instance of MulDivLemma.spec's +// `(a*b)/c <= a`. Requires the nonlinear SMT backend enabled in this conf. The bps +// precondition is `policyBpsBounded`, proved as an invariant above. +rule assignedCapWithinFullCap(env e, address rater, uint256 fullCap) { + requireInvariant policyBpsBounded(); + uint256 activeCap = assignLaunchCap_(e, rater, fullCap); + assert activeCap <= fullCap; +} From f07708d5243ddd742099de3760bc82df3590e577 Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 13:14:47 +0200 Subject: [PATCH 07/12] ci(certora): QRPE timeout load-cut + correct the resolver finding (Track D) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../certora/confs/question-reward-escrow-claim.conf | 7 +++++++ packages/foundry/certora/confs/question-reward-escrow.conf | 5 +++++ 2 files changed, 12 insertions(+) diff --git a/packages/foundry/certora/confs/question-reward-escrow-claim.conf b/packages/foundry/certora/confs/question-reward-escrow-claim.conf index 5d5e2918c..14cee2ba0 100644 --- a/packages/foundry/certora/confs/question-reward-escrow-claim.conf +++ b/packages/foundry/certora/confs/question-reward-escrow-claim.conf @@ -9,5 +9,12 @@ "rule_sanity": "none", "global_timeout": 7200, "prover_args": ["-mediumTimeout 30 -depth 5"], + // Track D load-cut (compiler-level auto-summary, not blocked by via_ir): drop the heavy + // difficult view/pure internal functions so the claim-flag rule has a chance to complete. + // NOTE: the per-commit no-double-claim property itself stays blocked — _resolveQuestionRewardClaim + // (QuestionRewardPoolEscrow.sol:1460, called from the claim path at :733) is INTERNAL, not the + // external resolver the earlier plan assumed, so it faces the same internal-summary-under-via_ir + // wall as the engine (Track A). See docs/testing/certora-round3-plan.md. + "nondet_difficult_funcs": true, "msg": "RateLoop Phase 4a QuestionRewardPoolEscrow claim flag never cleared" } diff --git a/packages/foundry/certora/confs/question-reward-escrow.conf b/packages/foundry/certora/confs/question-reward-escrow.conf index f609ff596..52a4c35d6 100644 --- a/packages/foundry/certora/confs/question-reward-escrow.conf +++ b/packages/foundry/certora/confs/question-reward-escrow.conf @@ -8,5 +8,10 @@ // This contract is large (1,490 lines + 11 libraries); the single revert-gate rule does // not need the sanity meta-checks, and disabling them keeps the SMT load down. "rule_sanity": "none", + // Track D load-cut: auto-summarize heuristically-difficult view/pure internal functions + // so the solver need not model the whole claim-weight/Merkle callgraph before reaching the + // early require(!refunded). This is a compiler-level auto-summary, NOT a CVL internal- + // function summary, so it is not blocked by the via_ir limitation (round3-plan Track D). + "nondet_difficult_funcs": true, "msg": "RateLoop Phase 4 QuestionRewardPoolEscrow refunded-pool claim gate" } From e6b28dbbf6d7db6cd9622ebe98ca24ecc890ab5b Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 13:16:30 +0200 Subject: [PATCH 08/12] docs(certora): Track A escalation write-up + round-3 status sync MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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 --- ...tora-escalation-internal-summary-via-ir.md | 80 +++++++++++++++++++ docs/testing/certora-round3-plan.md | 18 +++++ docs/testing/certora-security-findings.md | 21 +++++ packages/foundry/certora/README.md | 8 ++ 4 files changed, 127 insertions(+) create mode 100644 docs/testing/certora-escalation-internal-summary-via-ir.md diff --git a/docs/testing/certora-escalation-internal-summary-via-ir.md b/docs/testing/certora-escalation-internal-summary-via-ir.md new file mode 100644 index 000000000..21b299642 --- /dev/null +++ b/docs/testing/certora-escalation-internal-summary-via-ir.md @@ -0,0 +1,80 @@ +# Certora escalation — internal-function summaries under solc_optimize + solc_via_ir + +This is a ready-to-file support/forum write-up for the one genuinely tooling-blocked item +in the RateLoop Certora lane (Track A). It is parked here, not chased, because — as +verified below — there is no working path in certora-cli 8.13.1, which is the latest +release. File it upstream and re-test on each certora-cli bump. + +## Summary + +Several high-value properties (single-use refund on `RoundVotingEngine`, per-commit +no-double-claim on `QuestionRewardPoolEscrow`) require summarizing an **internal** +commit-resolution function deterministically. certora-cli 8.13.1 cannot apply +internal-function summaries when the contract is compiled with `solc_optimize` + +`solc_via_ir`, emitting: + +``` +Cannot apply summaries for internal functions ... when compiling using solc_optimize and solc_via_ir +``` + +and (relatedly, for the auto-finder): + +``` +Failed to generate auto finder for ... +WARNING: Cannot apply summaries for internal functions with unnamed argument when compiling using solc_optimize and solc_via_ir +``` + +These contracts genuinely require `via_ir`: building them on the legacy pipeline fails with +`Stack too deep. Try compiling with --via-ir`. So `via_ir` cannot be dropped, and the +internal summary cannot be applied — there is no intersection. + +## Environment + +- certora-cli: 8.13.1 (latest as of 2026-05-19; confirmed on PyPI / Prover changelog) +- solc: 0.8.35 + `via_ir`, optimizer runs = 100, evm = cancun +- `yul_optimizer_steps` set to solc 0.8.34's step string (certora-cli does not natively map + 0.8.35's via_ir Yul steps — a separate, minor gap) + +## Real-world repro cases in this repo + +Both are committed and reproduce the warning under `make certora-check` +(`certoraRun --compilation_steps_only`): + +- `packages/foundry/certora/confs/round-voting-engine-lifecycle.conf` — the single-use + refund property routes through the engine's internal `_resolveClaimCommit`. +- `packages/foundry/certora/confs/question-reward-escrow-claim.conf` — the per-commit + no-double-claim routes through `QuestionRewardPoolEscrow._resolveQuestionRewardClaim` + (QuestionRewardPoolEscrow.sol:1460, called from the claim path at :733), which is + internal — not an external call summarizable the way `NoDoubleClaim.spec` summarizes the + distributor→engine external `resolveClaimCommit`. + +## What was already tried (and did not work) + +Recorded from the round-2 empirical validation (docs/testing/certora-next-steps.md): + +| Attempt | Result | +|---|---| +| `function_finder_mode: relaxed` (valid key in 8.13.1) | internal summary still not applied | +| `use_memory_safe_autofinders` conf key | rejected — not a valid key in 8.13.1 | +| Drop via_ir (`solc_via_ir: false`) so internal summaries work | compile error: `Stack too deep. Try compiling with --via-ir` | +| Re-expose the internal fn as external on a harness | does not intercept — the call inside the contract is to the internal function directly | + +## The ask + +Add support for applying CVL internal-function summaries (or a sound equivalent) when a +contract is compiled with `solc_optimize` + `solc_via_ir`. Failing that, guidance on a +supported pattern for deterministically modeling an internal resolver in a via_ir-required +contract. + +## What we did instead (so the properties are not silently uncovered) + +- Proved the **resolution-independent state gates** the single-use properties build on: + refunds revert unless the round is terminal-but-not-settled; refunded pools reject + claims (`RoundVotingEngineLifecycle.spec`, `QuestionRewardPoolEscrow.spec`). +- Proved the **cross-contract** no-double-claim where the resolver IS external + (`NoDoubleClaim.spec`). +- The remaining single-use refund / per-commit no-double-claim are defense-in-depth on + flag-guarded paths already exercised by the Foundry test suite. + +Treat this as a tooling escalation, not an engineering task, until a certora-cli release +maps internal summaries under via_ir. diff --git a/docs/testing/certora-round3-plan.md b/docs/testing/certora-round3-plan.md index a0df5f3ba..716346ded 100644 --- a/docs/testing/certora-round3-plan.md +++ b/docs/testing/certora-round3-plan.md @@ -7,6 +7,24 @@ verified slices, with the blocked remainder recorded in question **"is it worth continuing, and if so on what?"** after a fresh research pass, and narrows the work to what is actually unblocked and high-value today. +> **Implementation status (2026-06-09).** All seven items below were implemented on branch +> `certora-followup-research-3`, each as its own commit. Every spec/conf compiles and CVL +> type-checks under certora-cli 8.13.1 (`make certora-check`); full proofs run on the cloud +> prover via CI (no `CERTORAKEY` locally). Summary: +> +> | Item | Outcome | +> |---|---| +> | 1. Oracle spec refresh | ✅ added `cannotReproposeRejectedCorrelationEpochRoot` (covers the L-Oracle-4 replay branch), fixed the stale line ref, documented the still-deferred new surface | +> | 2. Track C aggregate conservation | ◑ landed the tooling-independent pieces: `MulDivLemma.spec` (the reusable `(a*b)/c<=a` bound) + distributor accumulator monotonicity. The full inductive `claimed<=pool` upper bound stays deferred (needs the score-weight summation / engine model) — documented precisely | +> | 3. Track G CI | ✅ secret-free `certora-check` type-check gate + `spec-freshness` PR guard (+ script, tested) + new confs wired into the cloud matrix | +> | 4. Gambit | ✅ three mutation confs (FrontendRegistry, FeedbackBonusEscrow, RewardMath) + `make certora-mutate` + how-to README | +> | 5. Track B cap | ◑ `assignedCapWithinFullCap` machine-checks the cap-assignment clamp under `-smt_useNIA` (was by-inspection only); end-to-end global invariant stays the documented residual | +> | 6. Track D QRPE | ◑ `nondet_difficult_funcs` load-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-only | +> | 7. Track A | ✅ escalation write-up filed in-repo (`certora-escalation-internal-summary-via-ir.md`); no engineering, revisit on cli bump | +> +> ◑ = partial by design (the tooling-independent slice landed; the residual is a documented +> solver/tooling limit, not a contract defect). + ## Should we continue? — yes, with a narrowed scope The effort is mature and the docs are excellent. Two research findings reshape the plan: diff --git a/docs/testing/certora-security-findings.md b/docs/testing/certora-security-findings.md index d927ce479..9ff6264b8 100644 --- a/docs/testing/certora-security-findings.md +++ b/docs/testing/certora-security-findings.md @@ -10,6 +10,27 @@ vulnerability. Every property that was scoped to a clean, provable slice was pro items that could not be proved are **modeling/tooling limitations**, not known bugs — they are listed below in full so the gap is explicit rather than hidden. +## Round 3 (`certora-round3-plan.md`) + +A third pass (branch `certora-followup-research-3`) refreshed drifted specs and added the +tooling-independent conservation pieces. **No exploitable vulnerability was found.** New +machine-checked (cloud-prover) properties: the correlation-epoch rejected-root replay block +(`cannotReproposeRejectedCorrelationEpochRoot`), the reusable mul-div bound `(a*b)/c <= a` +(`MulDivLemma.spec`), the launch cap-assignment clamp under `-smt_useNIA` +(`assignedCapWithinFullCap`), and RoundRewardDistributor accumulator monotonicity. Three +findings refine the earlier deferral framing: + +1. **Oracle spec had drifted** behind three contract commits (new correlation-epoch + rejection branches). Not a bug — the existing proofs stayed sound (no signature drift) — + but coverage lagged. Closed for the replay branch; a CI `spec-freshness` guard now makes + future drift fail the PR instead of going silent. +2. **QRPE no-double-claim is NOT unblockable by send-only** as the round-2 plan hoped: + `_resolveQuestionRewardClaim` is *internal*, so it hits the same via_ir/internal-summary + wall as the engine (now escalated — see + [`certora-escalation-internal-summary-via-ir.md`](./certora-escalation-internal-summary-via-ir.md)). +3. **certora-cli 8.13.1 is the latest release**, so the via_ir blockers have no upgrade + path today; the escalation is filed and revisited on each cli bump. + ## Round 2 (Tracks B–G of `certora-next-steps.md`) A second implementation pass added LoopReputation, ProtocolConfig, the diff --git a/packages/foundry/certora/README.md b/packages/foundry/certora/README.md index 529c94994..9c15f38af 100644 --- a/packages/foundry/certora/README.md +++ b/packages/foundry/certora/README.md @@ -16,6 +16,8 @@ certora/ confs/ base.conf shared compiler + prover settings (no file targets) math.conf Phase 1: math-library harness + spec + mul-div-lemma.conf Track B/C: reusable (a*b)/c <= a bound (NIA) + round-reward-distributor-conservation.conf Track C: claimed-amount monotonicity cluster-payout-oracle.conf Phase 2: ClusterPayoutOracle round-voting-engine.conf Phase 3: RoundVotingEngine round-reward-distributor.conf Phase 3: RoundRewardDistributor @@ -167,6 +169,12 @@ yarn foundry:certora:check - Phase 4a (`question-reward-escrow-claim.conf`) — **authored, proof deferred**: the claim-flag-never-cleared rule type-checks but the solver exceeds the 15-min window on this large contract; not in CI. Run manually with a larger budget. + - Track B/C (`mul-div-lemma.conf`) — the reusable nonlinear bound `(a*b)/c <= a` for + `b <= c` (enables `-smt_useNIA`). Underpins the per-claimant reward bound and the launch + cap clamp. + - Track C (`round-reward-distributor-conservation.conf`) — the per-round claimed-amount + accumulators are monotone (no clawback/underflow). Full `claimed <= pool` upper bound + deferred (needs the engine score-weight model). See `certora-round3-plan.md`. - Verified under certora-cli 8.13.1 / solc 0.8.35 ("No errors found by Prover!"). - See [`docs/testing/certora-followup.md`](../../../docs/testing/certora-followup.md) for the phase plan and [`certora-security-findings.md`](../../../docs/testing/certora-security-findings.md) From e364e575d3d7a38cc82fc015f31757ba1fc6214a Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 14:41:31 +0200 Subject: [PATCH 09/12] fix(certora): track transitive library imports in spec-freshness guard MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../certora/scripts/check_spec_freshness.py | 74 ++++++++++++++----- 1 file changed, 55 insertions(+), 19 deletions(-) diff --git a/packages/foundry/certora/scripts/check_spec_freshness.py b/packages/foundry/certora/scripts/check_spec_freshness.py index 7c05f9a90..5f445e118 100755 --- a/packages/foundry/certora/scripts/check_spec_freshness.py +++ b/packages/foundry/certora/scripts/check_spec_freshness.py @@ -28,6 +28,7 @@ import argparse import json import os +import posixpath import re import subprocess import sys @@ -60,19 +61,57 @@ def strip_jsonc(text: str) -> str: return "\n".join(out) -def harness_contract_deps(harness_rel: str) -> list[str]: - """contracts/ files imported by a harness, as FOUNDRY-relative paths.""" - harness_path = Path(FOUNDRY) / harness_rel - deps: list[str] = [] - if not harness_path.exists(): - return deps - text = harness_path.read_text() - for m in re.finditer(r'import\s*\{[^}]*\}\s*from\s*"([^"]+)"', text): - target = m.group(1) - # Harnesses live in certora/harnesses/, so ../../contracts/X.sol -> contracts/X.sol - if "contracts/" in target: - normalized = "contracts/" + target.split("contracts/", 1)[1] - deps.append(normalized) +def _is_library(rel: str) -> bool: + return rel.startswith("contracts/libraries/") + + +def _resolve_imports(file_rel: str) -> list[str]: + """FOUNDRY-relative contracts/ files imported by file_rel (relative imports only). + + Remapped imports (@openzeppelin/..., etc.) resolve outside contracts/ and are dropped. + """ + path = Path(FOUNDRY) / file_rel + if not path.exists(): + return [] + base = posixpath.dirname(file_rel) + out: list[str] = [] + # Matches `import "X";`, `import {a,b} from "X";`, `import * as N from "X";`. + for m in re.finditer(r'import\s+(?:[^"\';]*?\sfrom\s+)?"([^"]+)"', path.read_text()): + resolved = posixpath.normpath(posixpath.join(base, m.group(1))) + if resolved.startswith("contracts/") and (Path(FOUNDRY) / resolved).exists(): + out.append(resolved) + return out + + +def contract_deps(target_rel: str) -> set[str]: + """The contracts/ files whose code is compiled INTO a conf target's verification. + + Starts from the target (a contracts/ file or a certora/harnesses/ harness) and walks + imports transitively, but only follows into LIBRARIES (contracts/libraries/**) — and, + from a harness, into the one full contract it wraps. Sibling full contracts reached + through an import are NOT included: the specs summarize those as external NONDET calls, + so a change to them cannot alter what is proved here. Libraries, by contrast, are linked + in and ARE part of the verified behavior (e.g. FrontendFeeDustLib in the distributor's + dust path), so a change to one must re-trip the freshness guard. + """ + deps: set[str] = set() + seen: set[str] = set() + # A harness is not itself a contracts/ file, so it is a walk root but never a dep. + stack = [target_rel] + if target_rel.startswith("contracts/"): + deps.add(target_rel) + while stack: + node = stack.pop() + if node in seen: + continue + seen.add(node) + node_is_harness = not node.startswith("contracts/") + for imp in _resolve_imports(node): + follow = _is_library(imp) or node_is_harness # harness -> its wrapped contract + if not follow: + continue # sibling full contract: summarized, out of scope + deps.add(imp) + stack.append(imp) return deps @@ -87,13 +126,10 @@ def build_map() -> dict[str, set[str]]: if ":" not in verify: continue spec = verify.split(":", 1)[1] - targets = data.get("files", []) deps: set[str] = set() - for target in targets: - if target.startswith("contracts/"): - deps.add(target) - elif "harnesses/" in target: - deps.update(harness_contract_deps(target)) + for target in data.get("files", []): + if target.startswith("contracts/") or "harnesses/" in target: + deps.update(contract_deps(target)) for dep in deps: mapping.setdefault(dep, set()).add(spec) return mapping From 6d5cc81ad787a825f9f653d49e4fcc25f8bd7dad Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 14:55:56 +0200 Subject: [PATCH 10/12] ci(certora): use the runner's preinstalled JDK 21 for the type-check 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 --- .github/workflows/certora.yaml | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/.github/workflows/certora.yaml b/.github/workflows/certora.yaml index b61ed756e..42187a8fa 100644 --- a/.github/workflows/certora.yaml +++ b/.github/workflows/certora.yaml @@ -48,11 +48,16 @@ jobs: - uses: ./.github/actions/setup-foundry - - name: Install Java 21 + - name: Use preinstalled Java 21 + # certora-cli's local CVL type-checker (used by --compilation_steps_only) needs + # Java >= 19; the runner's default java is older. Point at the GitHub-hosted + # runner's preinstalled JDK 21 rather than apt-installing one that is not the + # default on PATH. run: | - sudo apt-get update - sudo apt-get install -y --no-install-recommends openjdk-21-jre-headless - java --version + echo "JAVA_HOME=$JAVA_HOME_21_X64" >> "$GITHUB_ENV" + echo "$JAVA_HOME_21_X64/bin" >> "$GITHUB_PATH" + - name: Verify Java + run: java --version - name: Install Certora CLI and solc run: | @@ -143,11 +148,16 @@ jobs: - uses: ./.github/actions/setup-foundry - - name: Install Java 21 + - name: Use preinstalled Java 21 + # certora-cli's local CVL type-checker (used by --compilation_steps_only) needs + # Java >= 19; the runner's default java is older. Point at the GitHub-hosted + # runner's preinstalled JDK 21 rather than apt-installing one that is not the + # default on PATH. run: | - sudo apt-get update - sudo apt-get install -y --no-install-recommends openjdk-21-jre-headless - java --version + echo "JAVA_HOME=$JAVA_HOME_21_X64" >> "$GITHUB_ENV" + echo "$JAVA_HOME_21_X64/bin" >> "$GITHUB_PATH" + - name: Verify Java + run: java --version - name: Install Certora CLI and solc run: | From 289ba9f02ce68ed36e63fc13970aa56684043c3b Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 15:06:35 +0200 Subject: [PATCH 11/12] test(certora): drop artifact-tripping frontend dust rule (cloud-prover fix) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../RoundRewardDistributorConservation.spec | 30 +++++++++++++++++-- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec b/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec index 8e7e4ddd1..84249daee 100644 --- a/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec +++ b/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec @@ -70,9 +70,33 @@ rule dustFinalizationNeverDecreasesClaimedAmount( } // Symmetric monotonicity for the frontend-fee accumulator (RoundRewardDistributor.sol:98), -// which follows the same add-or-revert discipline as the voter accumulator. -rule frontendClaimNeverDecreasesClaimedAmount(env e, method f, calldataarg args, uint256 c, uint256 r) { +// which follows the same add-or-revert discipline as the voter accumulator: the only writes +// are `+= fee` (_consumeFrontendFeeClaim, :750) and `+= releasedDust` (_finalizeProcessed- +// FrontendFeeDust, :914). Targeted at the three public mutators rather than written as one +// parametric rule over every method: a free parametric rule over this via_ir, struct-heavy +// contract yields a spurious counterexample from an unreachable havoc prestate (the known +// auto-finder artifact documented in certora-security-findings.md), even though every real +// write only adds. The targeted rules below verify cleanly. +rule claimFrontendFeeNeverDecreasesClaimedAmount( + env e, uint256 contentId, uint256 roundId, address frontend, uint256 c, uint256 r +) { + uint256 before = roundFrontendClaimedAmount(c, r); + claimFrontendFee(e, contentId, roundId, frontend); + assert roundFrontendClaimedAmount(c, r) >= before; +} + +// NOTE: the public `finalizeFrontendFeeDust(.. address[] sortedFrontends)` wrapper is +// intentionally NOT given its own rule. Its only write to roundFrontendClaimedAmount is the +// `+= releasedDust` inside _finalizeProcessedFrontendFeeDust — already covered by the rule +// below — but it first runs the _processFrontendFeeDustBatch loop over the sorted-frontend +// array, whose deep internal calls hit the via_ir auto-finder instrumentation gap and +// produce a spurious "decrease" counterexample from an unreachable havoc state (the artifact +// documented in certora-security-findings.md). Covering the underlying writer directly keeps +// the proof sound without that false positive. +rule finalizeProcessedFrontendFeeDustNeverDecreasesClaimedAmount( + env e, uint256 contentId, uint256 roundId, uint256 c, uint256 r +) { uint256 before = roundFrontendClaimedAmount(c, r); - f(e, args); + finalizeProcessedFrontendFeeDust(e, contentId, roundId); assert roundFrontendClaimedAmount(c, r) >= before; } From 35f2cd460355eb436f25f42d8f1898f90e31173f Mon Sep 17 00:00:00 2001 From: Noc2 Date: Tue, 9 Jun 2026 15:08:47 +0200 Subject: [PATCH 12/12] style(foundry): forge fmt ClusterPayoutOracle.sol + test flagged by CI 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 --- .../foundry/contracts/ClusterPayoutOracle.sol | 26 +++++++++---------- .../foundry/test/ClusterPayoutOracle.t.sol | 18 ++++++------- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/packages/foundry/contracts/ClusterPayoutOracle.sol b/packages/foundry/contracts/ClusterPayoutOracle.sol index 3b327d8f5..88decf8c7 100644 --- a/packages/foundry/contracts/ClusterPayoutOracle.sol +++ b/packages/foundry/contracts/ClusterPayoutOracle.sol @@ -1,15 +1,15 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.34; -import {AccessControl} from "@openzeppelin/contracts/access/AccessControl.sol"; -import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol"; -import {SafeERC20} from "@openzeppelin/contracts/token/ERC20/utils/SafeERC20.sol"; -import {MerkleProof} from "@openzeppelin/contracts/utils/cryptography/MerkleProof.sol"; -import {SafeCast} from "@openzeppelin/contracts/utils/math/SafeCast.sol"; -import {ReentrancyGuard} from "@openzeppelin/contracts/utils/ReentrancyGuard.sol"; -import {IClusterPayoutOracle} from "./interfaces/IClusterPayoutOracle.sol"; -import {IFrontendRegistry} from "./interfaces/IFrontendRegistry.sol"; -import {IRoundPayoutSnapshotConsumer} from "./interfaces/IRoundPayoutSnapshotConsumer.sol"; +import { AccessControl } from "@openzeppelin/contracts/access/AccessControl.sol"; +import { IERC20 } from "@openzeppelin/contracts/token/ERC20/IERC20.sol"; +import { SafeERC20 } from "@openzeppelin/contracts/token/ERC20/utils/SafeERC20.sol"; +import { MerkleProof } from "@openzeppelin/contracts/utils/cryptography/MerkleProof.sol"; +import { SafeCast } from "@openzeppelin/contracts/utils/math/SafeCast.sol"; +import { ReentrancyGuard } from "@openzeppelin/contracts/utils/ReentrancyGuard.sol"; +import { IClusterPayoutOracle } from "./interfaces/IClusterPayoutOracle.sol"; +import { IFrontendRegistry } from "./interfaces/IFrontendRegistry.sol"; +import { IRoundPayoutSnapshotConsumer } from "./interfaces/IRoundPayoutSnapshotConsumer.sol"; /// @title ClusterPayoutOracle /// @notice Optimistic oracle for correlation epoch snapshots and per-round payout weights. @@ -1114,7 +1114,7 @@ contract ClusterPayoutOracle is IClusterPayoutOracle, AccessControl, ReentrancyG if (challenger == proposer || challenger == frontendOperator) revert InvalidSnapshot(); try frontendRegistry.isAuthorizedSnapshotProposer(frontendOperator, challenger) returns (bool authorized) { if (authorized) revert InvalidSnapshot(); - } catch {} + } catch { } } function _creditBond(address to, uint256 amount) private { @@ -1131,17 +1131,17 @@ contract ClusterPayoutOracle is IClusterPayoutOracle, AccessControl, ReentrancyG } catch { revert InvalidAddress(); } - try IFrontendRegistry(newFrontendRegistry).isEligible(address(0)) returns (bool) {} + try IFrontendRegistry(newFrontendRegistry).isEligible(address(0)) returns (bool) { } catch { revert InvalidAddress(); } - try IFrontendRegistry(newFrontendRegistry).authorizedSnapshotFrontend(address(0)) returns (address) {} + try IFrontendRegistry(newFrontendRegistry).authorizedSnapshotFrontend(address(0)) returns (address) { } catch { revert InvalidAddress(); } try IFrontendRegistry(newFrontendRegistry).isAuthorizedSnapshotProposer(address(0), address(0)) returns ( bool - ) {} + ) { } catch { revert InvalidAddress(); } diff --git a/packages/foundry/test/ClusterPayoutOracle.t.sol b/packages/foundry/test/ClusterPayoutOracle.t.sol index 8e6a38f2b..e9d9b41db 100644 --- a/packages/foundry/test/ClusterPayoutOracle.t.sol +++ b/packages/foundry/test/ClusterPayoutOracle.t.sol @@ -1,10 +1,10 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.34; -import {Test} from "forge-std/Test.sol"; -import {ClusterPayoutOracle} from "../contracts/ClusterPayoutOracle.sol"; -import {IClusterPayoutOracle} from "../contracts/interfaces/IClusterPayoutOracle.sol"; -import {MockERC20} from "../contracts/mocks/MockERC20.sol"; +import { Test } from "forge-std/Test.sol"; +import { ClusterPayoutOracle } from "../contracts/ClusterPayoutOracle.sol"; +import { IClusterPayoutOracle } from "../contracts/interfaces/IClusterPayoutOracle.sol"; +import { MockERC20 } from "../contracts/mocks/MockERC20.sol"; function _questionEpochSources(uint256 rewardPoolId, uint256 contentId, uint256 roundId) pure @@ -43,7 +43,7 @@ contract ClusterPayoutOracleTest is Test { MockRoundPayoutSnapshotConsumer internal launchConsumer; MockERC20 internal usdc; - receive() external payable {} + receive() external payable { } function setUp() public { usdc = new MockERC20("USD Coin", "USDC", 6); @@ -179,7 +179,7 @@ contract ClusterPayoutOracleTest is Test { function test_ProposalsDoNotAcceptEthBonds() public { vm.expectRevert(ClusterPayoutOracle.InvalidBond.selector); - oracle.proposeCorrelationEpoch{value: 1}( + oracle.proposeCorrelationEpoch{ value: 1 }( 1, 1, 20, @@ -1381,7 +1381,7 @@ contract ClusterPayoutOracleTest is Test { vm.prank(challenger); vm.expectRevert(ClusterPayoutOracle.InvalidBond.selector); - oracle.challengeCorrelationEpoch{value: 1}(1, keccak256("bad-root")); + oracle.challengeCorrelationEpoch{ value: 1 }(1, keccak256("bad-root")); } function test_ArbiterCanFinalizeChallengedSnapshots() public { @@ -1929,7 +1929,7 @@ contract ClusterPayoutOracleProposerBondTest is Test { event ProposerBondUnrecoverable(bytes32 indexed snapshotKey, address indexed proposer, uint256 missingAmount); - receive() external payable {} + receive() external payable { } function setUp() public { arbiter = address(this); @@ -2137,7 +2137,7 @@ contract MockRoundPayoutSnapshotConsumer { contract TestableClusterPayoutOracle is ClusterPayoutOracle { constructor(address admin, address frontendRegistry, address challengeBondToken) ClusterPayoutOracle(admin, frontendRegistry, challengeBondToken) - {} + { } /// @dev Sets proposerBond directly via the inherited (private) mapping. Because the storage /// mapping is `private`, we re-declare an internal shim that maps onto the same slot by