diff --git a/components/research/ClaimFlowDiagram.jsx b/components/research/ClaimFlowDiagram.jsx new file mode 100644 index 0000000..3308419 --- /dev/null +++ b/components/research/ClaimFlowDiagram.jsx @@ -0,0 +1,100 @@ +export default function ClaimFlowDiagram({ className = '' }) { + return ( +
+ + {/* ── User ── */} + + + User + + + {/* ── Before state box ── */} + + + Contract State (before) + + + roundUsdcTotal: 10000 + + + roundUsdcClaimed: 2000 + + + totalUsdcAllocated: 8000 + + + hasClaimedUsdc[Alice]: 0 + + + {/* Arrow: User → Before (call) */} + + + + claimUsdc(shareWad, proof) + + + {/* ── Checks ── */} + + + ✓ waiver signed + + + ✓ round active + + + ✓ not already claimed + + + ✓ proof accepted + + + ✓ 2000 + 1500 ≤ 10000 + + + {/* Arrow: Before → Checks */} + + + + {/* ── After state box ── */} + + + Contract State (after) + + + roundUsdcTotal: 10000 + + + roundUsdcClaimed: 3500 + + + totalUsdcAllocated: 6500 + + + hasClaimedUsdc[Alice]: 1 + + + {/* Arrow: Checks → After */} + + + + {/* Arrow: After → User (payout) */} + + + + + amount = 1500 + + + {/* Conservation annotation */} + + claimed + allocated = 2000 + 8000 = 3500 + 6500 = 10000 (conserved) + + +
+ ) +} diff --git a/components/research/StreamRecoveryGuarantee.jsx b/components/research/StreamRecoveryGuarantee.jsx new file mode 100644 index 0000000..703cf14 --- /dev/null +++ b/components/research/StreamRecoveryGuarantee.jsx @@ -0,0 +1,85 @@ +import { useState, useEffect, useRef } from 'react' + +const FORMAL_INVARIANTS = [ + '\u2200 user token, claimed(user, token) \u2192 payout(user, token) = shareWad(user) \u00d7 roundTotal(token) / 1e18', + '\u2200 token, roundClaimed\u2032(token) + totalAllocated\u2032(token) = roundClaimed(token) + totalAllocated(token)', + '\u2200 token, roundClaimed(token) \u2264 roundTotal(token)' +] + +export default function StreamRecoveryGuarantee() { + const [showEnglish, setShowEnglish] = useState(true) + const timerRef = useRef(null) + + useEffect(() => { + timerRef.current = setTimeout(() => setShowEnglish(false), 5000) + return () => clearTimeout(timerRef.current) + }, []) + + const handleToggle = () => { + if (timerRef.current) { + clearTimeout(timerRef.current) + timerRef.current = null + } + setShowEnglish((prev) => !prev) + } + + return ( +
+ + +
+
+ {FORMAL_INVARIANTS.map((formal, i) => ( + + {formal} + + ))} +
+
+

+ No user can claim more than their share. The round pool stays + solvent. The two token flows don't interfere. +

+
+
+
+ ) +} diff --git a/data/research.js b/data/research.js index 622c10c..468b89d 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'stream-recovery-claim', + title: 'StreamRecoveryClaim Accounting Invariants', + subtitle: + 'Formally verified claim accounting for the Sonic Earn Recovery System.', + description: + 'How we proved payout correctness, solvency, and cross-token independence across all claim functions in StreamRecoveryClaim using Verity and Lean 4.', + date: '2026-04-14', + tag: 'Case study' + }, { slug: 'safe-owner-reachability', title: 'Safe Owner List Invariants', diff --git a/pages/research/stream-recovery-claim.jsx b/pages/research/stream-recovery-claim.jsx new file mode 100644 index 0000000..f965ac8 --- /dev/null +++ b/pages/research/stream-recovery-claim.jsx @@ -0,0 +1,449 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import StreamRecoveryGuarantee from '../../components/research/StreamRecoveryGuarantee' +import Disclosure from '../../components/research/Disclosure' +import CodeBlock from '../../components/research/CodeBlock' +import ExternalLink from '../../components/research/ExternalLink' +import Hypothesis from '../../components/research/Hypothesis' +import ClaimFlowDiagram from '../../components/research/ClaimFlowDiagram' +import { getSortedResearch } from '../../lib/getSortedResearch' + +const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark +cd verity-benchmark +lake build Benchmark.Cases.PaladinVotes.StreamRecoveryClaimFull.Compile` + +const UPSTREAM_CONTRACT = + 'https://github.com/Figu3/sonic-earn-recovery-system/blob/699cbbc79def374cab9739e451acbbf866293d12/src/StreamRecoveryClaim.sol' + +const VERITY_CONTRACT = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/PaladinVotes/StreamRecoveryClaimFull/Contract.lean' + +export default function StreamRecoveryClaimPage() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'stream-recovery-claim' + ) + + return ( + <> + + + StreamRecoveryClaim Accounting Invariants | Research | LFG Labs + + + + +
+ + +
+

+ StreamRecoveryClaim Accounting Invariants +

+
+ + {/* The Guarantee */} +
+ +

+ The{' '} + + StreamRecoveryClaim + {' '} + contract is a Merkle-proof-based distribution system for recovering + USDC and WETH to ~40 users affected by the Stream Trading incident + on Trevee Earn's vaults on Sonic chain. An admin snapshots + affected users' vault balances, computes each user's + pro-rata share, builds a Merkle tree with leaves{' '} + + (address, shareWad) + + , and stores only the root onchain. +

+ +

+ Users sign an EIP-712 liability waiver, then call{' '} + claimUsdc or{' '} + claimWeth. The + contract verifies the Merkle proof against the stored root, computes{' '} + + amount = shareWad × roundTotal / 1e18 + + , checks accounting bounds, and pays out.{' '} + claimBoth calls + both sequentially. +

+
+ + {/* Why this matters */} +
+

+ Why this matters +

+

+ This contract distributes recovery funds to victims of an exploit. + A bug in the claim logic could let someone extract more than their + entitlement, claim twice, or drain the round pool, taking funds + that belong to other victims. The stakes are not abstract: every + dollar overclaimed is a dollar another affected user does not + receive. +

+ +

+ The proofs cover six property families across all three claim + functions: +

+
    +
  • + Correct payout: claimed counter increases and + allocated counter decreases by exactly{' '} + + shareWad × roundTotal / 1e18 + +
    • +
  • + Books balanced:{' '} + + roundClaimed + totalAllocated + {' '} + is conserved per token +
    • +
  • + Pool solvent:{' '} + + roundClaimed ≤ roundTotal + {' '} + per token +
    • +
  • + No double-dip: if user already claimed, + function reverts, state unchanged +
    • +
  • + No overclaim: if payout would exceed round + budget, function reverts, state unchanged +
    • +
  • + Cross-token independence:{' '} + claimBoth{' '} + produces identical state to calling each claim separately +
    • +
+

+ The model covers a single-round protocol slice. Multi-round + batching ( + + claimMultipleUsdc + + ) is out of scope. The per-round accounting properties hold + identically for each round. +

+ +
+ + {/* How this was proven */} +
+

+ How this was proven +

+

+ The claim functions were modeled in{' '} + Verity from + the Solidity{' '} + + StreamRecoveryClaim.sol + {' '} + implementation. Merkle verification is abstracted as a boolean + witness and token transfers are elided; the proofs focus on + accounting correctness. +

+

+ The Lean model maps ten storage slots: round totals, claimed + counters, allocated counters, round-active flag, per-user waiver + and claim flags, split across USDC and WETH. Each function mutates + this state differently: +

+
    +
  • + claimUsdc: verifies the Merkle proof, computes + the payout, increments{' '} + roundUsdcClaimed, + decrements{' '} + + totalUsdcAllocated + + , marks the user as claimed +
    • +
  • + claimWeth: symmetric to{' '} + claimUsdc on the + WETH slots +
    • +
  • + claimBoth: calls{' '} + claimUsdc then{' '} + claimWeth{' '} + sequentially. The cross-token independence proof shows this + composition is safe: USDC accounting does not interfere with WETH + accounting +
    • +
+

+ How do you prove the books stay balanced? You show that every + successful claim increases{' '} + roundClaimed and + decreases{' '} + totalAllocated by + exactly the same amount, so their sum is conserved. Combined with + the solvency bound ( + + roundClaimed ≤ roundTotal + + ), this guarantees no value is created or destroyed and the round + pot is never overdrawn. +

+

+ All proofs are verified by Lean 4's kernel and are provided + in{' '} + + Proofs.lean + + . If any step were wrong, the code would not compile. +

+ + {VERIFY_COMMAND} +

+ If the build succeeds, the proofs are correct.{' '} + + Source repository + +

+ +
+ + {/* Proof status */} +
+

+ Proof status +

+

+ All 18 theorems are proven.{' '} + + Proofs.lean + {' '} + is sorry-free. +

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ Function + + Correct payout + + Books balanced + + Pool solvent + + No double-dip + + No overclaim + + Cross-token +
claimUsdc + proven + + proven + + proven + + proven + + proven + + — +
claimWeth + proven + + proven + + proven + + proven + + proven + + — +
claimBoth + proven + + proven + + proven + + proven + + proven + + proven +
+
+
+ + {/* Assumptions */} +
+

+ Assumptions +

+

+ The proofs use zero axioms. The only trust assumption is the + Merkle proof abstraction. All other conditions are consumed in + exactly the form the contract enforces them. +

+
    + + Merkle verification is modeled as a boolean witness{' '} + proofAccepted. + This is the one real trust assumption: we assume the Merkle tree + correctly binds{' '} + + (msg.sender, shareWad) + {' '} + to the stored root. This is a cryptographic guarantee from + OpenZeppelin's MerkleProof library, not a contract-level + concern. + + + The model covers one round. Multi-round batching ( + + claimMultipleUsdc + + ) is out of scope. The per-round accounting properties hold + identically for each round. + + + The model verifies state accounting, not ERC20 transfer + execution. SafeERC20 correctness is trusted from OpenZeppelin. + + + msg.sender is + authentic. This is an EVM-level guarantee, not a contract-level + concern. + +
+

+ + View specs in Lean + + + View proofs in Lean + +

+
+ + {/* Learn more */} +
+

+ Learn more +

+

+ + Sonic Earn Recovery System + + {', the upstream contract repository.'} +

+

+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +

+
+ + {otherResearch.length > 0 && ( +
+

+ More research +

+
+ {otherResearch.map((r) => ( + + ))} +
+
+ )} +
+ + + ) +}