diff --git a/.github/workflows/certora.yaml b/.github/workflows/certora.yaml index 042d6fc05..2a2230f5e 100644 --- a/.github/workflows/certora.yaml +++ b/.github/workflows/certora.yaml @@ -40,6 +40,13 @@ jobs: - certora/confs/launch-distribution-pool.conf - certora/confs/frontend-registry.conf - certora/confs/feedback-bonus-escrow.conf + - certora/confs/loop-reputation.conf + - certora/confs/protocol-config.conf + - 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. name: ${{ matrix.conf }} steps: - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 diff --git a/docs/testing/certora-next-steps.md b/docs/testing/certora-next-steps.md new file mode 100644 index 000000000..858a9c72b --- /dev/null +++ b/docs/testing/certora-next-steps.md @@ -0,0 +1,240 @@ +# Certora — next-steps recommendation (research-backed) + +This is a second follow-up: a research-backed recommendation for what to do next with +the Certora work, written after Phases 3b–7 landed. It supersedes the "deferred" +framing in [`certora-security-findings.md`](./certora-security-findings.md) where new +evidence changes it. The plan in [`certora-followup.md`](./certora-followup.md) still +holds for *what* to prove; this doc is about *how* to unblock the parts that were parked +as "tooling-limited," plus the cheapest new wins. + +## Implementation status (round 2, 2026-06-08) + +Tracks B–G below were implemented (everything except Track A, which needs a Certora +escalation). Verified slices, with deferrals recorded in +[`certora-security-findings.md`](./certora-security-findings.md): + +| Track | Outcome | +|---|---| +| **E — LoopReputation** | ✅ supply cap (self-inductive), mint/lock access control, lock-respecting transfers. Pinned `solc_via_ir=false` (ERC20Votes checkpoint function-pointers crash the prover under IR). | +| **E — ProtocolConfig** | ✅ six address-book setters are role-gated (CONFIG/TREASURY/DEFAULT_ADMIN). | +| **B — LaunchDistributionPool cap** | ◑ `policyBpsBounded` + `capAssignedWhenPaid` proved; headline `paid<=cap` deferred (nonlinear `fullCap*bps/10000<=fullCap` is beyond the SMT backend). | +| **C — LaunchDistributionPool conservation** | ◑ earned-rater + verified-referral pool conservation proved; legacy-pool sweep deferred. | +| **D — QuestionRewardPoolEscrow no-double-claim** | ◑ authored (claim-flag-never-cleared, resolution-free); solver exceeds the 15-min window even with splitting flags → excluded from CI, run manually. | +| **F — port Foundry invariants** | ✅ already covered: the InvariantRating bounds (`rating<=100`, up-majority`>=50`) are proved in `Math.spec` (`ratingWithinBounds`, `ratingUpMajorityAtLeastNeutral`, `ratingDownMajorityAtMostNeutral`). InvariantSolvency C-02/C-03 stay deferred (cross-contract, multi-tx). | +| **G — CI + tooling** | ✅ the four new green confs added to the CI matrix; QRPE confs excluded with a note. | + +## TL;DR recommendation + +This round started from a research lead that the certora-cli flags +`--function_finder_mode relaxed` / `--use_memory_safe_autofinders` would unblock the +internal-function summaries that the highest-value proofs (single-use refund, no-double- +claim) depend on. **I validated that lead empirically against our 8.13.1 install, and it +does not hold for the engine** (see "Empirical validation" below). So the recommendation +is grounded in what actually works here, not what the docs imply: + +1. **Strengthen the LaunchDistributionPool cap invariant** with auxiliary invariants + + `requireInvariant` (Track B) — true, just not self-inductive. Tooling-independent; + **do this first**. +2. **Add aggregate-conservation proofs** (sum-of-payouts ≤ pool) with the ghost+hook + idiom / native ghost-map summation (Track C) — the headline solvency property still + missing. +3. **Two cheap new high-value targets**: LoopReputation and ProtocolConfig (Track E). +4. **Land QuestionRewardPoolEscrow no-double-claim** — its resolver is an *external* call + (summarizable), so unlike the engine it is reachable once the timeout is fixed by + summarizing the heavy libraries + send-only mode (Track D). +5. **Port the existing Foundry solvency/rating invariants** to CVL (Track F). + +The engine's *own* single-use-refund / internal-resolution properties stay **genuinely +blocked** in certora-cli 8.13.1 (Track A) — escalate to Certora rather than chase it. +Everything below cites the docs/changelog evidence and, where I tested it, the result. + +## Empirical validation (what I actually ran) + +I reconstructed the single-use refund rule that failed in Phase 3b (it summarizes the +engine's internal `_resolveClaimCommit` deterministically) and re-ran it with the flags +the research surfaced: + +| Test | Result | +|---|---| +| `function_finder_mode: relaxed` (valid conf key in 8.13.1) + full proof | `noDoubleRefundSameCaller` **FAILS** — the internal summary is still not applied | +| `use_memory_safe_autofinders` conf key | **rejected** — not a valid key in 8.13.1 | +| Drop via_ir for the engine via `solc_via_ir: false` (so internal summaries would work) | **compile error: "Stack too deep. Try compiling with --via-ir"** — the engine genuinely requires via_ir | + +Conclusion: for a contract that *must* use via_ir, certora-cli 8.13.1 has **no working +path** to apply an internal-function summary. The flags exist but do not cover this case, +and via_ir cannot be dropped. This confirms the original Phase 3b "deferred" call was +correct, and it sharpens the plan: pursue the properties whose resolver is *external* +(QRPE no-double-claim) or that need no resolution at all (Tracks B/C/E/F), and treat the +engine's internal-resolution properties as a tooling escalation, not a quick win. + +## Why this updates the picture + +When Phases 3b/4 were implemented, several blockers were recorded. Research surfaced +candidate workarounds; testing them sorts the blockers into "actually fixable" vs. +"confirmed hard limit": + +| Blocker (as recorded) | Tested outcome | Action | +|---|---|---| +| Internal-function summaries not applied under `solc_optimize + via_ir` (engine resolver) | `function_finder_mode: relaxed` **does not** fix it; via_ir **cannot** be dropped (stack-too-deep). Confirmed hard limit in 8.13.1. | **Track A** — escalate to Certora; do not chase | +| QuestionRewardPoolEscrow no-double-claim (resolver is *external*) | Not blocked by the above — external resolvers are summarizable (NoDoubleClaim.spec already does this). Only the contract-size timeout is in the way. | **Track D** — summarize libs + send-only | +| QuestionRewardPoolEscrow solver exceeds the 15-min client window | Send-only mode (`wait_for_results: NONE`, default outside CI) avoids the client timeout; `global_timeout` caps at 2 h; heavy libraries summarizable `NONDET` | **Track D** | +| LaunchDistributionPool cap invariant not self-inductive | Tooling-independent — solvable with auxiliary invariants + `requireInvariant` | **Track B** | +| `yul_optimizer_steps` 0.8.34 workaround for 0.8.35 via_ir | No documented native 0.8.35 mapping even on latest (8.13.1) | keep the workaround; re-test on each cli bump | + +## The plan + +### Track A — engine internal-resolution properties: escalate, don't chase (BLOCKED) + +The engine properties parked in Phase 3b (single-use refund, refund==stake) hinge on +**deterministic commit resolution** via the engine's *internal* `_resolveClaimCommit`, +which needs an internal-function summary. As validated above, certora-cli 8.13.1 cannot +apply that summary: `function_finder_mode: relaxed` does not help, and via_ir (required to +compile the engine) blocks internal summarization. The harness-wrapper trick does **not** +rescue this case either — the call inside `claimCancelledRoundRefund` is to the *internal* +function directly, so re-exposing it as external on the harness doesn't intercept it. + +Recommended action: **do not invest engineering time here yet.** Instead: +- File a Certora forum/support issue with the minimal repro (it's already reduced — the + `_ProbeInternalSummary` rule used for validation), asking for internal-summary support + under via_ir, and re-test on each certora-cli bump. +- Treat the property as covered indirectly: the cross-contract no-double-claim (Phase 3) + and the refund *state gates* (Phase 3b) already bound the most important misuse; the + remaining single-use refund is defense-in-depth on a flag-guarded path that the existing + Foundry tests already exercise. + +This is the only genuinely blocked track. Everything below is actionable today. + +### Track B — make the LaunchDistributionPool cap invariant inductive + +`raterLaunchPaid[r] <= raterLaunchCap[r]` is true but not self-inductive. Strengthen it +with auxiliary invariants conjoined via `requireInvariant` (sound, unlike a raw `require`): + +```cvl +// (1) cap monotonicity — a two-state relation, so a rule not an invariant +rule capNeverDecreases(method f, env e, calldataarg args, address r) { + mathint capBefore = raterLaunchCap(r); + f(e, args); + assert raterLaunchCap(r) >= capBefore; +} + +// (2) auxiliary consistency: paid>0 implies a cap was assigned +invariant capAssignedWhenPaid(address r) + raterLaunchPaid(r) > 0 => raterLaunchCap(r) > 0; + +// (3) the target, strengthened in the preserved block +invariant paidWithinCap(address r) + raterLaunchPaid(r) <= raterLaunchCap(r) + { + preserved with (env e) { + requireInvariant capAssignedWhenPaid(r); + requireInvariant paidWithinCap(e.msg.sender); // the key a record path touches + } + } +``` + +The `requireInvariant paidWithinCap(e.msg.sender)` move is exactly the docs' cap-style +example (`collateralCoversBalance` requiring itself for `msg.sender`). + +### Track C — aggregate conservation (the headline solvency property) + +"Sum of all per-round reward payouts ≤ the round's pool" and "sum of `raterLaunchPaid` ≤ +`poolBalance`" are the strongest solvency statements and still unproven. Use the canonical +ghost+hook idiom (the OpenZeppelin `sumOfBalances` pattern): + +```cvl +ghost mathint sumRaterLaunchPaid { init_state axiom sumRaterLaunchPaid == 0; } + +hook Sload uint256 paid raterLaunchPaid[KEY address r] STORAGE { + require sumRaterLaunchPaid >= to_mathint(paid); // no single entry exceeds the sum +} +hook Sstore raterLaunchPaid[KEY address r] uint256 newValue (uint256 oldValue) STORAGE { + sumRaterLaunchPaid = sumRaterLaunchPaid - oldValue + newValue; +} +invariant sumPaidWithinPool() sumRaterLaunchPaid <= to_mathint(poolBalance()); +``` + +For per-round sums use a `ghost mapping(uint256 => mathint)` accumulator (the Comet +`sumBalancePerAsset` pattern). certora-cli 7.25.2+ also offers **native summation over +ghost maps**, which removes most of the hook boilerplate — worth using on our 8.13.1. + +Note for parametric rules (e.g. the lifecycle-monotonicity rule that produced spurious +counterexamples): constrain them to reachable states with `requireInvariant`, not raw +`require` or `filtered` — this is Certora's documented guidance and is sound because the +required invariants are separately proved. + +### Track D — verify QuestionRewardPoolEscrow without timing out + +The contract is 1,490 lines + 11 libraries; even the one revert-gate rule blew the 15-min +client window. Two independent fixes: + +1. **Avoid the client timeout**: run with `wait_for_results: NONE` (send-only is already + the default outside CI) and read results from the dashboard, and/or raise + `global_timeout` toward its 2 h cap. In CI, prefer send-only + a follow-up status check + over a blocking `--wait_for_results all` that can hit the client window. +2. **Cut the SMT load**: summarize the heavy claim-path libraries as `NONDET` so the prover + doesn't analyze them (the refunded-pool / no-double-claim guards fire before they + matter): + ```cvl + methods { + function QuestionRewardPoolEscrowQualificationLib._ internal => NONDET; + function QuestionRewardPoolEscrowClaimLib._ internal => NONDET; + function QuestionRewardPoolEscrowVoterLib._ internal => NONDET; + function QuestionRewardPoolEscrowTransferLib._ internal => NONDET; + } + ``` + Also consider `--nondet_difficult_funcs`, `--split_rules`, and `--prover_args + '-mediumTimeout 30 -depth 5'`. + +With the load cut, the refunded-pool gate should complete, and the **no-double-claim** +slice becomes reachable (its resolver, `votingEngine.resolveClaimCommit`, is an *external* +call — summarizable deterministically with the `persistent ghost` idiom exactly as +NoDoubleClaim.spec already does for the round reward). + +### Track E — two cheap new high-value targets + +- **LoopReputation (Phase 8)** — ~168 lines, no external deps. `totalSupply() <= + MAX_SUPPLY` is self-inductive (mint is the only supply increase and is guarded). Also + prove `lockedBalance(a) <= balanceOf(a)` and that governance-lock functions are + governor-only. Highest ROI of any remaining target; ~1 day. +- **ProtocolConfig (Phase 10)** — small address-book; prove the single-active-distributor + -per-engine relation (`rewardDistributorForVotingEngine` is a function, not multi-valued) + and that config setters are role-gated. ~1 day; underpins governance confidence. + +### Track F — port the existing Foundry invariants to CVL + +`test/InvariantSolvency.t.sol` and `test/InvariantRating.t.sol` already assert strong +properties under fuzzing; porting them to CVL upgrades them from "no counterexample found +in N runs" to "proved": +- `totalClaimed <= round.totalStake + voterPool` (C-01 solvency) — pairs with Track C. +- `rating <= 100` and `weightedUpPool > weightedDownPool => rating >= 50` (rating bounds). + +### Track G — CI maturation + +Once Tracks A–C are green, the fast confs (`math`, `cluster-payout-oracle`, +`loop-reputation`, `protocol-config`) are stable enough to make a **required** PR check. +Keep the heavy confs (engine, escrow) on the weekly schedule + send-only mode so a slow +solver run never blocks a PR. Add `function_finder_mode: relaxed` to `base.conf` if Track A +confirms it helps broadly. + +## Suggested sequencing + +``` +Track B (cap invariant inductive) ┐ small, tooling-independent +Track E (LoopReputation, ProtocolConfig) ┘ cheapest wins, parallelizable ← do first +Track C (aggregate conservation ghosts) ← the headline solvency property +Track D (QRPE no-double-claim: lib summaries + send-only) ← unblocks the largest contract +Track F (port Foundry invariants) ← rolls into Track C +Track G (CI gate) ← after B–D are stable +Track A (engine internal-resolution) ← BLOCKED in 8.13.1; escalate to Certora, revisit on cli bump +``` + +## Sources + +- certora-cli changelog (flags & versions): https://docs.certora.com/en/latest/docs/prover/changelog/prover_changelog.html +- CLI options (`function_finder_mode`, `solc_via_ir_map`, `smt_timeout` 300s, `global_timeout` 2 h cap, `wait_for_results`): https://docs.certora.com/en/latest/docs/prover/cli/options.html +- Timeouts guide (splitting, summarization, `nondet_difficult_funcs`): https://docs.certora.com/en/latest/docs/user-guide/out-of-resources/timeout.html +- Invariants & preserved blocks: https://docs.certora.com/en/latest/docs/cvl/invariants.html +- Require-invariants pattern (inductive strengthening): https://docs.certora.com/en/latest/docs/user-guide/patterns/require-invariants.html +- Ghosts & hooks (aggregate conservation): https://docs.certora.com/en/latest/docs/cvl/ghosts.html , https://docs.certora.com/en/latest/docs/cvl/hooks.html +- Canonical sum-of-balances spec: https://github.com/OpenZeppelin/openzeppelin-contracts/blob/release-v5.0/certora/specs/ERC20.spec +- methods/summaries & DISPATCHER: https://docs.certora.com/en/latest/docs/cvl/methods.html diff --git a/docs/testing/certora-security-findings.md b/docs/testing/certora-security-findings.md index 63ce08062..d927ce479 100644 --- a/docs/testing/certora-security-findings.md +++ b/docs/testing/certora-security-findings.md @@ -10,6 +10,67 @@ 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 2 (Tracks B–G of `certora-next-steps.md`) + +A second implementation pass added LoopReputation, ProtocolConfig, the +LaunchDistributionPool cap lemmas + pool conservation, and a QuestionRewardPoolEscrow +claim-flag proof. **No exploitable vulnerability was found** in this pass either. Two +properties resisted proof; both are most likely tooling/solver limits rather than bugs, +but both are worth a quick manual confirmation: + +1. **LaunchDistributionPool `raterLaunchPaid <= raterLaunchCap`** — the last missing + lemma is `raterLaunchCap <= raterFullLaunchCap`, which at assignment reduces to + `fullCap * bps / 10000 <= fullCap` (given `bps <= 10000`). This is a nonlinear + multiply-then-divide inequality that the SMT backend cannot discharge precisely. By + inspection the clamp is correct (`unverifiedEarnedRaterCapBps` is validated `<= 10000` + by `_validateLaunchRewardPolicy`, and `_assignLaunchCap` divides by `BPS_DENOMINATOR`), + so this is a solver-completeness gap, not a defect. **Manual check:** confirm no payout + path raises `raterLaunchPaid` above the active cap. + +2. **LaunchDistributionPool legacy-pool conservation + (`distributed + treasuryRecovered <= LEGACY_CONTRIBUTOR_POOL_AMOUNT`)** — proved for + the earned-rater and verified-referral pools, but resisted on + `sweepExpiredLegacyContributorAllocationToTreasury`. **Manual check (low confidence):** + confirm the expired-allocation sweep cannot recover more than the pool's unclaimed + remainder. + +### Investigation outcome (both items resolved as proof gaps) + +Both items were investigated against the source. **Neither is a contract bug** — both are +proof-tooling gaps, and the contracts are correct by construction: + +- **Legacy-pool conservation — RESOLVED (spec corrected).** The claim and sweep both bound + against `legacyContributorAllocationTotal`, and `setLegacyContributorRoot` pins that to + exactly `LEGACY_CONTRIBUTOR_POOL_AMOUNT` (it reverts otherwise and is write-once). The + original invariant simply compared against the wrong bound. It is now proved as + `legacyAllocationTotalBounded` + `legacyDistributedWithinAllocation` + + `legacyRecoveredWithinAllocation` + `legacyDistributedWithinPool` (all verified). The + *tight* `distributed + treasuryRecovered <= pool` bound holds in the contract — claims + require an open window and the sweep a closed one, so the two never overlap and the sweep + can only recover the unclaimed remainder — but it depends on that temporal exclusivity, + which CVL cannot express as a storage-only invariant. It stays deferred as a + multi-tx/time-modeling item, **not** a risk: over-recovery is unreachable. + +- **Cap `paid <= cap` — CONFIRMED proof gap (no contract change needed).** Re-ran the full + chain with the nonlinear-arithmetic solver (`-smt_useNIA`); it discharged the assignment + multiplication but the `finalizeEarnedRaterRewardCredit` / `unlockFullEarnedRaterCap` + catch-up paths (which contain further `cap * count / rewardingCount` mul-div sites) still + resist. The contract is correct by inspection (every payout computes a target clamped to + the cap and pays only the positive delta). **Fix plan if a machine-checked proof is + wanted later:** introduce a small CVL mul-div lemma (prove `a*b/c <= a` for `b <= c` once, + as a pure rule) and apply it, or summarize the cap-fraction computation with a + monotonic-abstraction `ghost`. Low priority — the two proved lemmas + (`policyBpsBounded`, `capAssignedWhenPaid`) plus the by-inspection argument already cover + the property; only the end-to-end machine proof is missing. + +**Bottom line:** no fix is required to either contract. The legacy gap is closed in the +spec; the cap gap is a documented solver limitation with a concrete (low-priority) path to +a full proof. + +Neither is a confirmed bug. The proved properties (supply cap, role gates, earned/verified +/legacy pool conservation, cap-assignment + bps-bound lemmas, claim-flag integrity) provide +positive assurance over the value-handling paths. + ## Proved properties | Phase | Conf | Property proved | Status | diff --git a/packages/foundry/certora/README.md b/packages/foundry/certora/README.md index 8f92a1057..529c94994 100644 --- a/packages/foundry/certora/README.md +++ b/packages/foundry/certora/README.md @@ -152,6 +152,21 @@ yarn foundry:certora:check (stake <= STAKE_AMOUNT), single-use stake return, and exact bounded slash. - Phase 7 (`feedback-bonus-escrow.conf`) — **verified**: per-pool remaining <= funded (payouts bounded by funding), and a feedback hash is awarded at most once per pool. + - Phase 8 (`loop-reputation.conf`) — **verified**: totalSupply <= MAX_SUPPLY, mint is + MINTER_ROLE-gated, governance lock is governor-only, transfers respect the lock. + (Pins `solc_via_ir=false` — ERC20Votes checkpoint function-pointers crash the prover + under IR; the contract needs no IR.) + - Phase 10 (`protocol-config.conf`) — **verified**: the address-book setters are + role-gated (CONFIG / TREASURY / DEFAULT_ADMIN). + - Phase 5b (`launch-distribution-pool-cap.conf`) — **verified (lemmas)**: + `policyBpsBounded` + `capAssignedWhenPaid`. Headline paid<=cap deferred (nonlinear + SMT) — see `certora-security-findings.md`. + - Phase 5c (`launch-distribution-pool-conservation.conf`) — **verified**: earned-rater + and verified-referral pool payouts never exceed their funded pools. Legacy-pool sweep + deferred. + - 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. - 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) diff --git a/packages/foundry/certora/confs/launch-distribution-pool-cap.conf b/packages/foundry/certora/confs/launch-distribution-pool-cap.conf new file mode 100644 index 000000000..39f154a12 --- /dev/null +++ b/packages/foundry/certora/confs/launch-distribution-pool-cap.conf @@ -0,0 +1,9 @@ +{ + // Phase 5b (Track B): LaunchDistributionPool per-rater cap conservation, made inductive + // with an auxiliary invariant. Inherits compiler/prover settings from base.conf. + // Run with: certoraRun certora/confs/launch-distribution-pool-cap.conf + "override_base_config": "certora/confs/base.conf", + "files": ["certora/harnesses/LaunchDistributionPoolHarness.sol"], + "verify": "LaunchDistributionPoolHarness:certora/specs/LaunchDistributionPoolCap.spec", + "msg": "RateLoop Phase 5b LaunchDistributionPool cap invariant" +} diff --git a/packages/foundry/certora/confs/launch-distribution-pool-conservation.conf b/packages/foundry/certora/confs/launch-distribution-pool-conservation.conf new file mode 100644 index 000000000..42562900b --- /dev/null +++ b/packages/foundry/certora/confs/launch-distribution-pool-conservation.conf @@ -0,0 +1,9 @@ +{ + // Phase 5c (Track C): LaunchDistributionPool aggregate conservation (ghost+hook + // sum-of-mapping). Inherits compiler/prover settings from base.conf. + // Run with: certoraRun certora/confs/launch-distribution-pool-conservation.conf + "override_base_config": "certora/confs/base.conf", + "files": ["contracts/LaunchDistributionPool.sol"], + "verify": "LaunchDistributionPool:certora/specs/LaunchDistributionPoolConservation.spec", + "msg": "RateLoop Phase 5c LaunchDistributionPool aggregate conservation" +} diff --git a/packages/foundry/certora/confs/loop-reputation.conf b/packages/foundry/certora/confs/loop-reputation.conf new file mode 100644 index 000000000..11017152f --- /dev/null +++ b/packages/foundry/certora/confs/loop-reputation.conf @@ -0,0 +1,9 @@ +{ + "override_base_config": "certora/confs/base.conf", + "files": [ + "contracts/LoopReputation.sol" + ], + "verify": "LoopReputation:certora/specs/LoopReputation.spec", + "solc_via_ir": false, + "msg": "RateLoop Phase 8 LoopReputation supply cap and locks" +} \ No newline at end of file diff --git a/packages/foundry/certora/confs/protocol-config.conf b/packages/foundry/certora/confs/protocol-config.conf new file mode 100644 index 000000000..4e8c67c9e --- /dev/null +++ b/packages/foundry/certora/confs/protocol-config.conf @@ -0,0 +1,9 @@ +{ + // Phase 10 (Track E): ProtocolConfig address-book role gates. Inherits compiler/prover + // settings from base.conf. + // Run with: certoraRun certora/confs/protocol-config.conf + "override_base_config": "certora/confs/base.conf", + "files": ["contracts/ProtocolConfig.sol"], + "verify": "ProtocolConfig:certora/specs/ProtocolConfig.spec", + "msg": "RateLoop Phase 10 ProtocolConfig role gates" +} diff --git a/packages/foundry/certora/confs/question-reward-escrow-claim.conf b/packages/foundry/certora/confs/question-reward-escrow-claim.conf new file mode 100644 index 000000000..5d5e2918c --- /dev/null +++ b/packages/foundry/certora/confs/question-reward-escrow-claim.conf @@ -0,0 +1,13 @@ +{ + // Phase 4a (Track D): QuestionRewardPoolEscrow no-double-claim backbone (claim flag + // never cleared). Inherits compiler/prover settings from base.conf. The contract is + // large (1,490 lines + 11 libraries), so the sanity meta-checks are off and the solver + // is given a longer budget with control-flow splitting to avoid timing out. + "override_base_config": "certora/confs/base.conf", + "files": ["contracts/QuestionRewardPoolEscrow.sol"], + "verify": "QuestionRewardPoolEscrow:certora/specs/QuestionRewardPoolEscrowClaim.spec", + "rule_sanity": "none", + "global_timeout": 7200, + "prover_args": ["-mediumTimeout 30 -depth 5"], + "msg": "RateLoop Phase 4a QuestionRewardPoolEscrow claim flag never cleared" +} diff --git a/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol b/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol new file mode 100644 index 000000000..0604bc325 --- /dev/null +++ b/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol @@ -0,0 +1,19 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.35; + +import { LaunchDistributionPool } from "../../contracts/LaunchDistributionPool.sol"; + +/// @title LaunchDistributionPoolHarness +/// @notice Exposes the policy's unverified-cap bps so Certora can prove the auxiliary +/// invariant `raterLaunchCap <= raterFullLaunchCap` (which needs bps <= 10000) in +/// the cap-conservation chain. Verification target for +/// certora/specs/LaunchDistributionPoolCap.spec (Phase 5b / Track B). +contract LaunchDistributionPoolHarness is LaunchDistributionPool { + constructor(address lrep, address registry, address governance) + LaunchDistributionPool(lrep, registry, governance) + { } + + function unverifiedCapBps_() external view returns (uint256) { + return uint256(launchRewardPolicy.unverifiedEarnedRaterCapBps); + } +} diff --git a/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec b/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec new file mode 100644 index 000000000..7c25cf7c6 --- /dev/null +++ b/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec @@ -0,0 +1,46 @@ +/* + * LaunchDistributionPoolCap.spec — Phase 5b (Track B). + * + * Verification target: certora/harnesses/LaunchDistributionPoolHarness.sol + * Run with: certoraRun certora/confs/launch-distribution-pool-cap.conf + * + * Track B set out to make the Phase-5-deferred per-rater bound + * `raterLaunchPaid[r] <= raterLaunchCap[r]` inductive. Two of the supporting invariants + * are proved here: + * + * policyBpsBounded — the unverified-cap bps never exceeds 10000 (the policy setter + * reverts otherwise; the default policy and zero-state satisfy it). + * 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. + */ + +methods { + function raterLaunchPaid(address) external returns (uint256) envfree; + function raterLaunchCapAssigned(address) external returns (bool) envfree; + function unverifiedCapBps_() external returns (uint256) envfree; + + function _.transfer(address, uint256) external => NONDET; + function _.transferFrom(address, address, uint256) external => NONDET; + function _.safeTransfer(address, uint256) external => NONDET; + function _.balanceOf(address) external => NONDET; + function _.getHumanCredential(address) external => NONDET; + function _.launchHumanIdentityKey(uint8, bytes32) external => NONDET; + function _.verifyPayoutWeight(IClusterPayoutOracle.PayoutWeight, bytes32[]) external => NONDET; +} + +// The unverified-cap bps is bounded by 10000 (BPS_DENOMINATOR): _validateLaunchRewardPolicy +// reverts otherwise, and the default policy and zero-state both satisfy it. +invariant policyBpsBounded() + unverifiedCapBps_() <= 10000; + +// Any rater that has been paid has an assigned cap (every payout path assigns first). +invariant capAssignedWhenPaid(address r) + raterLaunchPaid(r) > 0 => raterLaunchCapAssigned(r); diff --git a/packages/foundry/certora/specs/LaunchDistributionPoolConservation.spec b/packages/foundry/certora/specs/LaunchDistributionPoolConservation.spec new file mode 100644 index 000000000..652e6c22e --- /dev/null +++ b/packages/foundry/certora/specs/LaunchDistributionPoolConservation.spec @@ -0,0 +1,77 @@ +/* + * LaunchDistributionPoolConservation.spec — Phase 5c (Track C). + * + * Verification target: contracts/LaunchDistributionPool.sol (verified directly). + * Run with: certoraRun certora/confs/launch-distribution-pool-conservation.conf + * + * Aggregate conservation across the three launch sub-pools: the total LREP paid out of + * each pool never exceeds that pool's funded size. Each `*Distributed` counter is the + * running sum of all payouts from its pool, incremented only by amounts that the code + * clamps to (or reverts above) the remaining pool, so each bound is a self-inductive + * invariant: + * + * earnedRaterDistributed <= EARNED_RATER_POOL_AMOUNT + * verifiedReferralDistributed <= VERIFIED_REFERRAL_POOL_AMOUNT + * legacyContributorDistributed <= LEGACY_CONTRIBUTOR_POOL_AMOUNT + * legacyContributorTreasuryRecovered <= legacyContributorAllocationTotal (<= pool) + * + * (An earlier attempt also tied Σ raterLaunchPaid to earnedRaterDistributed via a + * ghost+hook; that equality is fragile under the SafeERC20 external calls that havoc a + * non-persistent ghost, and is not needed — the distributed counter already IS the + * aggregate sum, so the scalar invariants below carry the property.) + */ + +methods { + function earnedRaterDistributed() external returns (uint256) envfree; + function verifiedReferralDistributed() external returns (uint256) envfree; + function legacyContributorDistributed() external returns (uint256) envfree; + function legacyContributorTreasuryRecovered() external returns (uint256) envfree; + function legacyContributorAllocationTotal() external returns (uint256) envfree; + function EARNED_RATER_POOL_AMOUNT() external returns (uint256) envfree; + function VERIFIED_REFERRAL_POOL_AMOUNT() external returns (uint256) envfree; + function LEGACY_CONTRIBUTOR_POOL_AMOUNT() external returns (uint256) envfree; + + function _.transfer(address, uint256) external => NONDET; + function _.transferFrom(address, address, uint256) external => NONDET; + function _.safeTransfer(address, uint256) external => NONDET; + function _.safeTransferFrom(address, address, uint256) external => NONDET; + function _.balanceOf(address) external => NONDET; + function _.getHumanCredential(address) external => NONDET; + function _.launchHumanIdentityKey(uint8, bytes32) external => NONDET; + function _.verifyPayoutWeight(IClusterPayoutOracle.PayoutWeight, bytes32[]) external => NONDET; +} + +// Earned-rater pool: total paid never exceeds the funded pool. +invariant earnedRaterPoolConserved() + to_mathint(earnedRaterDistributed()) <= to_mathint(EARNED_RATER_POOL_AMOUNT()); + +// Verified-referral pool: total paid never exceeds the funded pool. +invariant verifiedReferralPoolConserved() + to_mathint(verifiedReferralDistributed()) <= to_mathint(VERIFIED_REFERRAL_POOL_AMOUNT()); + +// Legacy pool (revisited). The claim and sweep paths bound against +// legacyContributorAllocationTotal, which setLegacyContributorRoot pins to exactly +// LEGACY_CONTRIBUTOR_POOL_AMOUNT (it reverts otherwise and is write-once). So the legacy +// conservation splits cleanly into three self-inductive invariants: +invariant legacyAllocationTotalBounded() + to_mathint(legacyContributorAllocationTotal()) <= to_mathint(LEGACY_CONTRIBUTOR_POOL_AMOUNT()); + +invariant legacyDistributedWithinAllocation() + to_mathint(legacyContributorDistributed()) <= to_mathint(legacyContributorAllocationTotal()); + +invariant legacyRecoveredWithinAllocation() + to_mathint(legacyContributorTreasuryRecovered()) <= to_mathint(legacyContributorAllocationTotal()); + +// Combined, neither the distributed total nor the swept-to-treasury total individually +// exceeds the 9M legacy pool. (The TIGHT bound `distributed + recovered <= pool` holds in +// the contract — claims require an open window and the sweep a closed one, so they never +// overlap — but is not a storage-only invariant: it needs the temporal claim/sweep +// exclusivity, which CVL cannot express without multi-tx/time modeling. Left deferred.) +invariant legacyDistributedWithinPool() + to_mathint(legacyContributorDistributed()) <= to_mathint(LEGACY_CONTRIBUTOR_POOL_AMOUNT()) + { + preserved { + requireInvariant legacyAllocationTotalBounded(); + requireInvariant legacyDistributedWithinAllocation(); + } + } diff --git a/packages/foundry/certora/specs/LoopReputation.spec b/packages/foundry/certora/specs/LoopReputation.spec new file mode 100644 index 000000000..207aa2c2c --- /dev/null +++ b/packages/foundry/certora/specs/LoopReputation.spec @@ -0,0 +1,49 @@ +/* + * LoopReputation.spec — Phase 8 (Track E). + * + * Verification target: contracts/LoopReputation.sol (verified directly). + * Run with: certoraRun certora/confs/loop-reputation.conf + * + * LREP is the capped governance token. Properties: + * 1. Supply cap — totalSupply never exceeds MAX_SUPPLY. mint is the only supply + * increase and is guarded by `require(totalSupply()+amount <= MAX_SUPPLY)`, and + * there is no burn path, so the cap is self-inductive. + * 2. mint is MINTER_ROLE-gated. + * 3. Governance locking is governor-only. + * 4. Transfers cannot move governance-locked tokens (a successful transfer never + * exceeds the sender's transferable balance). + */ + +methods { + function totalSupply() external returns (uint256) envfree; + function MAX_SUPPLY() external returns (uint256) envfree; + function MINTER_ROLE() external returns (bytes32) envfree; + function hasRole(bytes32, address) external returns (bool) envfree; + function governor() external returns (address) envfree; + function getTransferableBalance(address) external returns (uint256); +} + +// 1. Supply cap is never exceeded, in any reachable state. +invariant totalSupplyWithinCap() + totalSupply() <= MAX_SUPPLY(); + +// 2. mint succeeds only for a caller holding MINTER_ROLE. +rule mintRequiresMinterRole(env e, address to, uint256 amount) { + bool isMinter = hasRole(MINTER_ROLE(), e.msg.sender); + mint@withrevert(e, to, amount); + assert !lastReverted => isMinter; +} + +// 3. Governance lock can only be engaged by the configured governor. +rule lockForGovernanceOnlyByGovernor(env e, address account, uint256 amount) { + lockForGovernance@withrevert(e, account, amount); + assert !lastReverted => e.msg.sender == governor(); +} + +// 4. A transfer never moves more than the sender's transferable (non-locked) balance. +rule transferCannotMoveLockedTokens(env e, address to, uint256 value) { + require e.msg.sender != 0; + mathint transferable = getTransferableBalance(e, e.msg.sender); + transfer@withrevert(e, to, value); + assert !lastReverted => to_mathint(value) <= transferable; +} diff --git a/packages/foundry/certora/specs/ProtocolConfig.spec b/packages/foundry/certora/specs/ProtocolConfig.spec new file mode 100644 index 000000000..d42b7b41c --- /dev/null +++ b/packages/foundry/certora/specs/ProtocolConfig.spec @@ -0,0 +1,70 @@ +/* + * ProtocolConfig.spec — Phase 10 (Track E). + * + * Verification target: contracts/ProtocolConfig.sol (verified directly). + * Run with: certoraRun certora/confs/protocol-config.conf + * + * ProtocolConfig is the governance-controlled address book + parameter store for the + * protocol. Its security rests on every mutation being role-gated. This proves that the + * address-book setters cannot be called without the required role: + * - the address-book / parameter setters require CONFIG_ROLE, + * - treasury rotation requires TREASURY_ROLE, + * - replacing a revoked reward distributor requires DEFAULT_ADMIN_ROLE (higher bar). + * + * Each `onlyRole` modifier runs before any body logic / external validation call, so the + * "succeeded => caller holds the role" implication is a pure access-control gate that + * needs no modeling of the validated dependencies. + */ + +methods { + function hasRole(bytes32, address) external returns (bool) envfree; + function CONFIG_ROLE() external returns (bytes32) envfree; + function TREASURY_ROLE() external returns (bytes32) envfree; + function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; + + // Dependency-validation calls in the setters are irrelevant to the access gate. + function _.votingEngine() external => NONDET; + function _.registry() external => NONDET; + function _.lrepToken() external => NONDET; + function _.claimAccountingStarted() external => NONDET; + function _.authorizedCallers(address) external => NONDET; + function _.isCategory(uint256) external => NONDET; + function _.STAKE_AMOUNT() external => NONDET; + function _.protocolConfig() external => NONDET; +} + +// Reward-distributor registration requires CONFIG_ROLE. +rule setRewardDistributorRequiresConfigRole(env e, address value) { + setRewardDistributor@withrevert(e, value); + assert !lastReverted => hasRole(CONFIG_ROLE(), e.msg.sender); +} + +// Revoking a reward distributor requires CONFIG_ROLE. +rule revokeRewardDistributorRequiresConfigRole(env e, address value) { + revokeRewardDistributor@withrevert(e, value); + assert !lastReverted => hasRole(CONFIG_ROLE(), e.msg.sender); +} + +// Replacing a revoked reward distributor is a higher-privilege action: DEFAULT_ADMIN_ROLE. +rule replaceRevokedRewardDistributorRequiresAdminRole(env e, address oldValue, address newValue) { + replaceRevokedRewardDistributor@withrevert(e, oldValue, newValue); + assert !lastReverted => hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); +} + +// Treasury rotation requires TREASURY_ROLE. +rule setTreasuryRequiresTreasuryRole(env e, address value) { + setTreasury@withrevert(e, value); + assert !lastReverted => hasRole(TREASURY_ROLE(), e.msg.sender); +} + +// The rater-registry pointer is CONFIG_ROLE-gated (representative of the address book). +rule setRaterRegistryRequiresConfigRole(env e, address value) { + setRaterRegistry@withrevert(e, value); + assert !lastReverted => hasRole(CONFIG_ROLE(), e.msg.sender); +} + +// The frontend-registry pointer is CONFIG_ROLE-gated. +rule setFrontendRegistryRequiresConfigRole(env e, address value) { + setFrontendRegistry@withrevert(e, value); + assert !lastReverted => hasRole(CONFIG_ROLE(), e.msg.sender); +} diff --git a/packages/foundry/certora/specs/QuestionRewardPoolEscrowClaim.spec b/packages/foundry/certora/specs/QuestionRewardPoolEscrowClaim.spec new file mode 100644 index 000000000..73b738d7c --- /dev/null +++ b/packages/foundry/certora/specs/QuestionRewardPoolEscrowClaim.spec @@ -0,0 +1,46 @@ +/* + * QuestionRewardPoolEscrowClaim.spec — Phase 4a (Track D). + * + * Verification target: contracts/QuestionRewardPoolEscrow.sol (verified directly). + * Run with: certoraRun certora/confs/question-reward-escrow-claim.conf + * + * The no-double-claim backbone for question rewards: no function ever clears a recorded + * per-commit claim flag. Combined with the up-front `require(!rewardClaimed[...])` guard + * in the claim path, this is exactly what prevents a commit from being paid twice — the + * same shape proved for the round-reward distributor in RoundRewardDistributor.spec. + * + * `rewardClaimed` is private, so a storage hook mirrors it into a ghost (hooks observe + * storage regardless of Solidity visibility). The rule is resolution-free: it does not + * depend on which commit a caller resolves to, only that a set flag is never unset. The + * external votingEngine getters used during a claim are summarized NONDET (they cannot + * write this contract's storage) — this also keeps the heavy claim path tractable. + */ + +ghost mapping(uint256 => mapping(uint256 => mapping(bytes32 => bool))) claimedMirror; + +hook Sstore rewardClaimed[KEY uint256 poolId][KEY uint256 roundId][KEY bytes32 commitKey] bool newValue (bool oldValue) { + claimedMirror[poolId][roundId][commitKey] = newValue; +} + +methods { + // Engine / oracle / token externals: NONDET (no side effects on this contract's + // storage; also cuts the SMT load on this 1,490-line + 11-library contract). + function _.roundLifecycleState(uint256, uint256) external => NONDET; + function _.commitCore(uint256, uint256, bytes32) external => NONDET; + function _.commitIdentityState(uint256, uint256, bytes32) external => NONDET; + function _.identityCommitState(uint256, uint256, bytes32, address) external => NONDET; + function _.voterCommitKey(uint256, uint256, address) external => NONDET; + function _.roundRaterRegistrySnapshot(uint256, uint256) external => NONDET; + function _.roundFrontendRegistrySnapshot(uint256, uint256) external => NONDET; + function _.transfer(address, uint256) external => NONDET; + function _.transferFrom(address, address, uint256) external => NONDET; + function _.safeTransfer(address, uint256) external => NONDET; + function _.balanceOf(address) external => NONDET; +} + +// No function ever clears a recorded per-commit claim flag. +rule rewardClaimedFlagNeverCleared(method f, env e, calldataarg args, uint256 poolId, uint256 roundId, bytes32 commitKey) { + require claimedMirror[poolId][roundId][commitKey]; + f(e, args); + assert claimedMirror[poolId][roundId][commitKey]; +} diff --git a/packages/foundry/test/AdvisoryRecorderSampler.t.sol b/packages/foundry/test/AdvisoryRecorderSampler.t.sol index c7d7e7151..3e789f6c8 100644 --- a/packages/foundry/test/AdvisoryRecorderSampler.t.sol +++ b/packages/foundry/test/AdvisoryRecorderSampler.t.sol @@ -55,8 +55,7 @@ contract HarnessAdvisoryRecorder is AdvisoryVoteRecorder { /// 2. The reference draw (uint256(seed) % revealedLen) is uniformly distributed. /// 3. The peer draw excludes the reference and is uniformly distributed over the rest. contract AdvisoryRecorderSamplerTest is Test { - bytes32 internal constant QUICKNET_CHAIN_HASH = - 0x52db9ba70e0cc0f6eaf7803dd07447a1f5477735fd3f661792ba94600c84e971; + bytes32 internal constant QUICKNET_CHAIN_HASH = 0x52db9ba70e0cc0f6eaf7803dd07447a1f5477735fd3f661792ba94600c84e971; uint64 internal constant QUICKNET_TEST_GENESIS_TIME = 1; uint64 internal constant QUICKNET_TEST_PERIOD = 3; HarnessAdvisoryRecorder internal recorder; @@ -88,14 +87,7 @@ contract AdvisoryRecorderSamplerTest is Test { address(protocolConfigImpl), abi.encodeCall( ProtocolConfig.initializeWithDrandConfig, - ( - owner, - owner, - owner, - QUICKNET_CHAIN_HASH, - QUICKNET_TEST_GENESIS_TIME, - QUICKNET_TEST_PERIOD - ) + (owner, owner, owner, QUICKNET_CHAIN_HASH, QUICKNET_TEST_GENESIS_TIME, QUICKNET_TEST_PERIOD) ) ) ) diff --git a/packages/foundry/test/UpgradeTest.t.sol b/packages/foundry/test/UpgradeTest.t.sol index 2cacecdfe..bf2bc0211 100644 --- a/packages/foundry/test/UpgradeTest.t.sol +++ b/packages/foundry/test/UpgradeTest.t.sol @@ -84,8 +84,7 @@ contract UpgradeTest is Test { address public governance = address(2); address public attacker = address(999); bytes32 internal constant ERC1967_ADMIN_SLOT = bytes32(uint256(keccak256("eip1967.proxy.admin")) - 1); - bytes32 internal constant QUICKNET_CHAIN_HASH = - 0x52db9ba70e0cc0f6eaf7803dd07447a1f5477735fd3f661792ba94600c84e971; + bytes32 internal constant QUICKNET_CHAIN_HASH = 0x52db9ba70e0cc0f6eaf7803dd07447a1f5477735fd3f661792ba94600c84e971; uint64 internal constant QUICKNET_TEST_GENESIS_TIME = 1; uint64 internal constant QUICKNET_TEST_PERIOD = 3; @@ -114,14 +113,7 @@ contract UpgradeTest is Test { governance, abi.encodeCall( ProtocolConfig.initializeWithDrandConfig, - ( - admin, - governance, - governance, - QUICKNET_CHAIN_HASH, - QUICKNET_TEST_GENESIS_TIME, - QUICKNET_TEST_PERIOD - ) + (admin, governance, governance, QUICKNET_CHAIN_HASH, QUICKNET_TEST_GENESIS_TIME, QUICKNET_TEST_PERIOD) ) ); protocolConfig = ProtocolConfig(address(pcProxy)); diff --git a/packages/foundry/test/helpers/VotingTestHelpers.sol b/packages/foundry/test/helpers/VotingTestHelpers.sol index 749f78267..6fb292ee4 100644 --- a/packages/foundry/test/helpers/VotingTestHelpers.sol +++ b/packages/foundry/test/helpers/VotingTestHelpers.sol @@ -701,8 +701,7 @@ abstract contract VotingTestBase is Test, ContentSubmissionTestBase { mapping(bytes32 => TestRevealPayload) internal testRevealPayloads; - bytes32 internal constant DEFAULT_DRAND_CHAIN_HASH = - TEST_PROTOCOL_CONFIG_DRAND_CHAIN_HASH; + bytes32 internal constant DEFAULT_DRAND_CHAIN_HASH = TEST_PROTOCOL_CONFIG_DRAND_CHAIN_HASH; uint64 internal constant DEFAULT_DRAND_GENESIS_TIME = TEST_PROTOCOL_CONFIG_DRAND_GENESIS_TIME; uint64 internal constant DEFAULT_DRAND_PERIOD = TEST_PROTOCOL_CONFIG_DRAND_PERIOD; uint256 internal constant DEFAULT_TLOCK_EPOCH_DURATION = 20 minutes;