docs(certora): research-backed next-steps recommendation#35
Merged
Conversation
Second follow-up. Researched (multi-agent + web) the tooling/methodology around the properties parked as 'via_ir-limited' and EMPIRICALLY validated the leads: - function_finder_mode: relaxed does NOT apply the engine's internal-function summary under via_ir (re-ran the Phase 3b single-use refund rule -> still FAILS); use_memory_safe_autofinders is not a valid key in 8.13.1; via_ir cannot be dropped for the engine (stack-too-deep). So engine internal-resolution proofs are a confirmed hard limit -> escalate to Certora (Track A). - Actionable instead: strengthen the cap invariant via requireInvariant (B), aggregate-conservation ghosts+hooks (C), LoopReputation + ProtocolConfig (E), QRPE no-double-claim via external-resolver summarization + send-only (D), port the Foundry solvency/rating invariants (F), CI gate (G). Includes CVL snippets and cited sources. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7fb3f38485
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+172
to
+175
| 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). |
There was a problem hiding this comment.
When following Track D to implement the QRPE no-double-claim proof, this premise points engineers at the wrong summary: the plain claim path calls the escrow's internal _resolveQuestionRewardClaim from QuestionRewardPoolEscrow.sol:732, which delegates through internal _resolveRoundRewardClaim and QuestionRewardPoolEscrowVoterLib.resolveRoundRewardClaim; a repo search shows votingEngine.resolveClaimCommit is not called by the escrow at all. Summarizing that external method therefore will not control the commitKey used by rewardClaimed, so the proposed path is still subject to the internal/via_ir modeling blocker and can lead to a failed or vacuous no-double-claim proof.
Useful? React with 👍 / 👎.
Verified (certora-cli 8.13.1 / solc 0.8.35): the address-book setters cannot be called without the required role - setRewardDistributor / revokeRewardDistributor / setRaterRegistry / setFrontendRegistry require CONFIG_ROLE, setTreasury requires TREASURY_ROLE, and replaceRevokedRewardDistributor requires DEFAULT_ADMIN_ROLE. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Verified (solc 0.8.35, legacy pipeline): totalSupply never exceeds MAX_SUPPLY (self-inductive; mint is the only supply increase and is guarded, no burn path), mint is MINTER_ROLE-gated, governance locking is governor-only, and a transfer never moves more than the sender's non-locked transferable balance. Conf pins solc_via_ir=false: the ERC20Votes checkpoint helpers take a function-type parameter that the prover's auto-finder cannot instrument under via_ir, which crashed the cloud job; the contract compiles fine on the legacy pipeline and needs no IR. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Verified: policyBpsBounded (unverified-cap bps <= 10000, setter-enforced) and capAssignedWhenPaid (any rater with paid>0 has an assigned cap - every payout path assigns before paying). These are the sound, machine-checked part of the chain toward raterLaunchPaid<=raterLaunchCap. The headline paid<=cap remains deferred: its last lemma reduces to fullCap*bps/10000<=fullCap, a nonlinear multiply-then-divide inequality the SMT backend cannot discharge (solver-completeness limit, not a defect - the clamp is correct by inspection). Noted in certora-security-findings.md for manual review. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Verified: aggregate payout conservation for two of the three launch sub-pools - earnedRaterDistributed <= EARNED_RATER_POOL_AMOUNT and verifiedReferralDistributed <= VERIFIED_REFERRAL_POOL_AMOUNT. Each *Distributed counter is the running sum of all payouts and is clamped to the remaining pool at every payout, so the bound is self-inductive. The legacy pool's combined distributed+treasuryRecovered<=pool bound resisted on the expired-allocation sweep (needs an auxiliary invariant); deferred and noted in certora-security-findings.md. A ghost+hook Sum(raterLaunchPaid)==distributed equality was also tried but is fragile under SafeERC20 havoc and unnecessary - the counter already is the aggregate sum. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…of deferred) Resolution-free no-double-claim backbone: a storage hook mirrors the private rewardClaimed mapping and the rule asserts no method ever clears a set flag (the same shape proved for RoundRewardDistributor). Compiles and type-checks; engine getters are summarized NONDET to cut load. Even with rule_sanity off, global_timeout 7200, and -mediumTimeout/-depth splitting, the solver still exceeds the 15-min output window on this 1,490-line + 11-library contract, so the lane is excluded from CI and marked proof-deferred. Run manually with a larger prover budget. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add loop-reputation, protocol-config, launch-distribution-pool-cap, and launch-distribution-pool-conservation to the CI matrix (all verified). The two QuestionRewardPoolEscrow confs stay excluded (exceed the 15-min prover window). Record round-2 implementation status in certora-next-steps.md (incl. Track F: the InvariantRating bounds are already proved in Math.spec) and update the workspace README phase list. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
No exploitable vulnerability found across Tracks B-G. Records two low-confidence items for manual review: the LaunchDistributionPool paid<=cap nonlinear-division gap and the legacy-pool sweep conservation gap - both most likely solver/modeling limits, neither a confirmed defect. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Investigation of the low-confidence legacy-sweep item: it is a proof gap, not a contract bug. The sweep and claim both bound against legacyContributorAllocationTotal, which setLegacyContributorRoot pins to exactly LEGACY_CONTRIBUTOR_POOL_AMOUNT (reverts otherwise, write-once). The original invariant compared to the wrong bound. Now verified: legacyAllocationTotalBounded (allocationTotal <= 9M pool), legacyDistributedWithinAllocation, legacyRecoveredWithinAllocation, and legacyDistributedWithinPool. The tight distributed+recovered<=pool bound holds in the contract (claims need an open window, the sweep a closed one - never overlapping) but is not a storage-only invariant; left documented-deferred (needs temporal modeling). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Both flagged items investigated and resolved as proof gaps, not contract bugs: - Legacy-pool conservation: spec corrected (bound against allocationTotal, which is pinned to the 9M pool); now verified. Tight sum bound needs temporal modeling. - Cap paid<=cap: nonlinear solver (-smt_useNIA) closes the assignment multiplication but finalize/unlock catch-up mul-div sites still resist; contract correct by inspection; documented fix plan (CVL mul-div lemma) if a full proof is wanted. No contract changes required. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Pre-existing forge-fmt violations on main (multi-line constants / call args the formatter collapses to a single line) surfaced in this PR via the pull_request merge commit. Ran forge fmt 1.5.1 to collapse them; fixes the Lint CI job. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
A second Certora follow-up: a research-backed recommendation for what to do next, in
docs/testing/certora-next-steps.md. Written after Phases 3b–7 landed, and grounded in empirical validation rather than docs alone.Researched (multi-agent + web) the tooling/methodology around the properties parked last round as "via_ir-limited", then tested the central lead on our installed certora-cli 8.13.1.
Key finding — validated, not assumed
The research suggested
--function_finder_mode relaxedwould unblock the engine's internal-function summaries (single-use refund, no-double-claim). I re-ran the exact rule that failed in Phase 3b and tested the alternatives:function_finder_mode: relaxed+ full re-runnoDoubleRefundSameCallerFAILS — internal summary still not applieduse_memory_safe_autofindersconf key→ The engine's internal-resolution properties are a confirmed hard limit in 8.13.1 (escalate to Certora, don't chase). This corrects the over-optimistic research lead before any time is spent on it.
Recommendation (prioritized, all actionable today)
requireInvariant+ auxiliary invariants)totalSupply ≤ MAX_SUPPLY, self-inductive) and ProtocolConfig (single-distributor bijection)sum(payouts) ≤ pool) via ghost+hook / native ghost-map summation — the headline solvency property still missingNONDETsummaries + send-only modeEach track includes concrete CVL snippets and cited sources. Docs-only change.
🤖 Generated with Claude Code