Skip to content

feat: add StreamRecoveryClaim research article #21

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fricoben merged 1 commit into from
Apr 14, 2026
Merged

feat: add StreamRecoveryClaim research article #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 100 additions & 0 deletions components/research/ClaimFlowDiagram.jsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
export default function ClaimFlowDiagram({ className = '' }) {
return (
<div className={className}>
<svg
viewBox="0 0 520 420"
className="w-full max-w-[520px] mx-auto"
fill="none"
xmlns="http://www.w3.org/2000/svg"
>
{/* ── User ── */}
<rect x="20" y="60" width="90" height="40" rx="6" stroke="#9ca3af" strokeWidth="1.2" fill="#f9fafb" />
<text x="65" y="84" textAnchor="middle" className="fill-[#374151]" fontSize="13" fontFamily="sans-serif">
User
</text>

{/* ── Before state box ── */}
<rect x="200" y="20" width="300" height="110" rx="6" stroke="#374151" strokeWidth="1.5" fill="#f3f4f6" />
<text x="350" y="42" textAnchor="middle" className="fill-[#374151]" fontSize="12" fontWeight="600" fontFamily="sans-serif">
Contract State (before)
</text>
<text x="220" y="62" className="fill-[#6b7280]" fontSize="11" fontFamily="monospace">
roundUsdcTotal: 10000
</text>
<text x="220" y="78" className="fill-[#6b7280]" fontSize="11" fontFamily="monospace">
roundUsdcClaimed: 2000
</text>
<text x="220" y="94" className="fill-[#6b7280]" fontSize="11" fontFamily="monospace">
totalUsdcAllocated: 8000
</text>
<text x="220" y="110" className="fill-[#6b7280]" fontSize="11" fontFamily="monospace">
hasClaimedUsdc[Alice]: 0
</text>

{/* Arrow: User → Before (call) */}
<line x1="110" y1="80" x2="196" y2="80" stroke="#9ca3af" strokeWidth="1.2" />
<polygon points="196,77 204,80 196,83" fill="#9ca3af" />
<text x="153" y="72" textAnchor="middle" className="fill-[#9ca3af]" fontSize="9" fontFamily="monospace">
claimUsdc(shareWad, proof)
</text>

{/* ── Checks ── */}
<rect x="200" y="160" width="300" height="100" rx="6" stroke="#d1d5db" strokeWidth="1" fill="#ffffff" />
<text x="230" y="182" className="fill-[#059669]" fontSize="11" fontFamily="sans-serif">
&#x2713; waiver signed
</text>
<text x="230" y="198" className="fill-[#059669]" fontSize="11" fontFamily="sans-serif">
&#x2713; round active
</text>
<text x="230" y="214" className="fill-[#059669]" fontSize="11" fontFamily="sans-serif">
&#x2713; not already claimed
</text>
<text x="230" y="230" className="fill-[#059669]" fontSize="11" fontFamily="sans-serif">
&#x2713; proof accepted
</text>
<text x="230" y="246" className="fill-[#059669]" fontSize="11" fontFamily="sans-serif">
&#x2713; 2000 + 1500 &le; 10000
</text>

{/* Arrow: Before → Checks */}
<line x1="350" y1="130" x2="350" y2="156" stroke="#9ca3af" strokeWidth="1.2" />
<polygon points="347,156 350,164 353,156" fill="#9ca3af" />

{/* ── After state box ── */}
<rect x="200" y="290" width="300" height="110" rx="6" stroke="#374151" strokeWidth="1.5" fill="#f3f4f6" />
<text x="350" y="312" textAnchor="middle" className="fill-[#374151]" fontSize="12" fontWeight="600" fontFamily="sans-serif">
Contract State (after)
</text>
<text x="220" y="332" className="fill-[#6b7280]" fontSize="11" fontFamily="monospace">
roundUsdcTotal: 10000
</text>
<text x="220" y="348" className="fill-[#374151]" fontSize="11" fontWeight="600" fontFamily="monospace">
roundUsdcClaimed: 3500
</text>
<text x="220" y="364" className="fill-[#374151]" fontSize="11" fontWeight="600" fontFamily="monospace">
totalUsdcAllocated: 6500
</text>
<text x="220" y="380" className="fill-[#374151]" fontSize="11" fontWeight="600" fontFamily="monospace">
hasClaimedUsdc[Alice]: 1
</text>

{/* Arrow: Checks → After */}
<line x1="350" y1="260" x2="350" y2="286" stroke="#9ca3af" strokeWidth="1.2" />
<polygon points="347,286 350,294 353,286" fill="#9ca3af" />

{/* Arrow: After → User (payout) */}
<line x1="200" y1="345" x2="65" y2="345" stroke="#9ca3af" strokeWidth="1.2" />
<line x1="65" y1="345" x2="65" y2="104" stroke="#9ca3af" strokeWidth="1.2" />
<polygon points="62,104 65,96 68,104" fill="#9ca3af" />
<text x="133" y="338" textAnchor="middle" className="fill-[#9ca3af]" fontSize="9" fontFamily="monospace">
amount = 1500
</text>

{/* Conservation annotation */}
<text x="350" y="415" textAnchor="middle" className="fill-[#9ca3af]" fontSize="10" fontFamily="sans-serif">
claimed + allocated = 2000 + 8000 = 3500 + 6500 = 10000 (conserved)
</text>
</svg>
</div>
)
}
85 changes: 85 additions & 0 deletions components/research/StreamRecoveryGuarantee.jsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 (
<div className="py-6">
<button
onClick={handleToggle}
className="inline-flex items-center gap-1.5 text-[12px] font-semibold text-muted hover:text-heading transition-colors cursor-pointer mb-4"
>
<svg
viewBox="0 0 24 24"
className="w-[13px] h-[13px]"
fill="none"
stroke="currentColor"
strokeWidth="1.5"
strokeLinecap="round"
strokeLinejoin="round"
>
<path d="m5 8 6 6" />
<path d="m4 14 6-6 2-3" />
<path d="M2 5h12" />
<path d="M7 2h1" />
<path d="m22 22-5-10-5 10" />
<path d="M14 18h6" />
</svg>
{showEnglish ? 'Switch to formal' : 'Switch to English'}
</button>

<div className="grid text-center [&>*]:col-start-1 [&>*]:row-start-1">
<div
className="flex flex-col items-center justify-center gap-4 md:gap-5 transition-opacity duration-200 text-[0.84rem] md:text-[1.05rem] font-mono text-primary leading-snug"
style={{
opacity: showEnglish ? 0 : 1,
pointerEvents: showEnglish ? 'none' : 'auto'
}}
aria-hidden={showEnglish}
>
{FORMAL_INVARIANTS.map((formal, i) => (
<code
key={i}
className="block w-full max-w-full overflow-x-auto px-1"
>
{formal}
</code>
))}
</div>
<div
className="flex items-center justify-center transition-opacity duration-200"
style={{
opacity: showEnglish ? 1 : 0,
pointerEvents: showEnglish ? 'auto' : 'none'
}}
aria-hidden={!showEnglish}
>
<p className="text-xl md:text-2xl leading-snug font-serif max-w-prose mx-auto px-1">
No user can claim more than their share. The round pool stays
solvent. The two token flows don&apos;t interfere.
</p>
</div>
</div>
</div>
)
}
10 changes: 10 additions & 0 deletions data/research.js
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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',
Expand Down
Loading