Skip to content

Add Kleros Sortition Tree case study #25

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

Open
fricoben wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add Kleros Sortition Tree case study #25

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
86 changes: 86 additions & 0 deletions components/research/KlerosGuarantee.jsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
import { useState, useEffect, useRef } from 'react'

const FORMAL_INVARIANTS = [
'root = \u2211\u1d62 leaf(i), i \u2208 {7..14}',
'\u2200 ticket < root, draw(ticket) \u2208 {7..14}',
'\u2200 leaf i, draw\u207b\u00b9(i) = [offset(i), offset(i) + weight(i))'
]

export default function KlerosGuarantee() {
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">
The sortition tree always conserves total stake, and the draw
mechanism selects jurors with probability exactly proportional to
their stake.
</p>
</div>
</div>
</div>
)
}
155 changes: 155 additions & 0 deletions components/research/SortitionDrawExample.jsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,155 @@
export default function SortitionDrawExample({ className = '' }) {
const active = '#059669'
const activeBg = '#ecfdf5'
const inactive = '#d1d5db'
const inactiveBg = '#f9fafb'
const inactiveText = '#c4c8cd'

return (
<div className={className}>
<svg
viewBox="0 0 560 370"
className="w-full max-w-[560px] mx-auto"
fill="none"
xmlns="http://www.w3.org/2000/svg"
>
{/* ── Level 0: Root (active) ── */}
<rect x="230" y="10" width="100" height="36" rx="6" stroke={active} strokeWidth="1.5" fill={activeBg} />
<text x="280" y="33" textAnchor="middle" fill={active} fontSize="12" fontWeight="600" fontFamily="monospace">
root = 800
</text>
{/* ticket label at root */}
<text x="340" y="22" fill={active} fontSize="9" fontWeight="600" fontFamily="sans-serif">
ticket = 200
</text>

{/* ── Level 1 ── */}
{/* node1 (active, go left) */}
<rect x="100" y="90" width="100" height="36" rx="6" stroke={active} strokeWidth="1.5" fill={activeBg} />
<text x="150" y="113" textAnchor="middle" fill={active} fontSize="11" fontWeight="600" fontFamily="monospace">
node1 = 350
</text>

{/* node2 (inactive) */}
<rect x="360" y="90" width="100" height="36" rx="6" stroke={inactive} strokeWidth="1" fill={inactiveBg} />
<text x="410" y="113" textAnchor="middle" fill={inactiveText} fontSize="11" fontFamily="monospace">
node2 = 450
</text>

{/* Lines: root to level 1 */}
<line x1="255" y1="46" x2="175" y2="90" stroke={active} strokeWidth="2" />
<line x1="305" y1="46" x2="385" y2="90" stroke={inactive} strokeWidth="1" />

{/* Decision label: 200 < 350, go left */}
<text x="196" y="64" textAnchor="middle" fill={active} fontSize="9" fontFamily="sans-serif" fontWeight="600">
200 {'<'} 350
</text>
<text x="196" y="74" textAnchor="middle" fill={active} fontSize="8" fontFamily="sans-serif">
go left
</text>

{/* ── Level 2 ── */}
{/* node3 (inactive) */}
<rect x="30" y="170" width="90" height="36" rx="6" stroke={inactive} strokeWidth="1" fill={inactiveBg} />
<text x="75" y="193" textAnchor="middle" fill={inactiveText} fontSize="10" fontFamily="monospace">
node3 = 150
</text>

{/* node4 (active, go right) */}
<rect x="160" y="170" width="90" height="36" rx="6" stroke={active} strokeWidth="1.5" fill={activeBg} />
<text x="205" y="193" textAnchor="middle" fill={active} fontSize="10" fontWeight="600" fontFamily="monospace">
node4 = 200
</text>

{/* node5 (inactive) */}
<rect x="310" y="170" width="90" height="36" rx="6" stroke={inactive} strokeWidth="1" fill={inactiveBg} />
<text x="355" y="193" textAnchor="middle" fill={inactiveText} fontSize="10" fontFamily="monospace">
node5 = 250
</text>

{/* node6 (inactive) */}
<rect x="440" y="170" width="90" height="36" rx="6" stroke={inactive} strokeWidth="1" fill={inactiveBg} />
<text x="485" y="193" textAnchor="middle" fill={inactiveText} fontSize="10" fontFamily="monospace">
node6 = 200
</text>

{/* Lines: level 1 to level 2 */}
<line x1="125" y1="126" x2="90" y2="170" stroke={inactive} strokeWidth="1" />
<line x1="175" y1="126" x2="195" y2="170" stroke={active} strokeWidth="2" />
<line x1="385" y1="126" x2="345" y2="170" stroke={inactive} strokeWidth="1" />
<line x1="435" y1="126" x2="475" y2="170" stroke={inactive} strokeWidth="1" />

{/* Decision label: 200 >= 150, go right, ticket = 50 */}
<text x="198" y="144" textAnchor="middle" fill={active} fontSize="9" fontFamily="sans-serif" fontWeight="600">
200 {'≥'} 150
</text>
<text x="198" y="154" textAnchor="middle" fill={active} fontSize="8" fontFamily="sans-serif">
go right, ticket = 50
</text>

{/* ── Level 3: Leaves ── */}
{[
{ x: 10, label: 'L0', val: '80', on: false },
{ x: 75, label: 'L1', val: '70', on: false },
{ x: 140, label: 'L2', val: '100', on: true },
{ x: 205, label: 'L3', val: '100', on: false },
{ x: 290, label: 'L4', val: '120', on: false },
{ x: 355, label: 'L5', val: '130', on: false },
{ x: 420, label: 'L6', val: '90', on: false },
{ x: 485, label: 'L7', val: '110', on: false }
].map((leaf, i) => (
<g key={i}>
<rect
x={leaf.x} y={260} width="60" height="36" rx="6"
stroke={leaf.on ? active : inactive}
strokeWidth={leaf.on ? 2 : 1}
fill={leaf.on ? activeBg : inactiveBg}
/>
<text
x={leaf.x + 30} y={275} textAnchor="middle"
fill={leaf.on ? active : inactiveText}
fontSize="10" fontWeight="600" fontFamily="sans-serif"
>
{leaf.label}
</text>
<text
x={leaf.x + 30} y={289} textAnchor="middle"
fill={leaf.on ? active : inactiveText}
fontSize="9" fontFamily="monospace"
>
{leaf.val}
</text>
</g>
))}

{/* Lines: level 2 to leaves */}
<line x1="52" y1="206" x2="40" y2="260" stroke={inactive} strokeWidth="1" />
<line x1="98" y1="206" x2="105" y2="260" stroke={inactive} strokeWidth="1" />
<line x1="185" y1="206" x2="170" y2="260" stroke={active} strokeWidth="2" />
<line x1="225" y1="206" x2="235" y2="260" stroke={inactive} strokeWidth="1" />
<line x1="335" y1="206" x2="320" y2="260" stroke={inactive} strokeWidth="1" />
<line x1="375" y1="206" x2="385" y2="260" stroke={inactive} strokeWidth="1" />
<line x1="465" y1="206" x2="450" y2="260" stroke={inactive} strokeWidth="1" />
<line x1="505" y1="206" x2="515" y2="260" stroke={inactive} strokeWidth="1" />

{/* Decision label: 50 < 100, go left */}
<text x="160" y="234" textAnchor="middle" fill={active} fontSize="9" fontFamily="sans-serif" fontWeight="600">
50 {'<'} 100
</text>
<text x="160" y="244" textAnchor="middle" fill={active} fontSize="8" fontFamily="sans-serif">
go left
</text>

{/* Selected juror callout */}
<text x="170" y="312" textAnchor="middle" fill={active} fontSize="10" fontWeight="700" fontFamily="sans-serif">
Selected
</text>

{/* Result annotation */}
<text x="280" y="350" textAnchor="middle" fill="#6b7280" fontSize="10" fontFamily="sans-serif">
L2 owns tickets 150 to 249 (100 out of 800 = 12.5% chance)
</text>
</svg>
</div>
)
}
107 changes: 107 additions & 0 deletions components/research/SortitionTreeDiagram.jsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
export default function SortitionTreeDiagram({ className = '' }) {
return (
<div className={className}>
<svg
viewBox="0 0 560 400"
className="w-full max-w-[560px] mx-auto"
fill="none"
xmlns="http://www.w3.org/2000/svg"
>
{/* ── Level 0: Root ── */}
<rect x="230" y="10" width="100" height="36" rx="6" stroke="#374151" strokeWidth="1.5" fill="#f3f4f6" />
<text x="280" y="33" textAnchor="middle" className="fill-[#374151]" fontSize="12" fontWeight="600" fontFamily="monospace">
root = 800
</text>

{/* ── Level 1: Two subtree roots ── */}
<rect x="100" y="90" width="100" height="36" rx="6" stroke="#374151" strokeWidth="1.2" fill="#f9fafb" />
<text x="150" y="113" textAnchor="middle" className="fill-[#6b7280]" fontSize="11" fontFamily="monospace">
node1 = 350
</text>

<rect x="360" y="90" width="100" height="36" rx="6" stroke="#374151" strokeWidth="1.2" fill="#f9fafb" />
<text x="410" y="113" textAnchor="middle" className="fill-[#6b7280]" fontSize="11" fontFamily="monospace">
node2 = 450
</text>

{/* Lines: root → level 1 */}
<line x1="255" y1="46" x2="175" y2="90" stroke="#9ca3af" strokeWidth="1.2" />
<line x1="305" y1="46" x2="385" y2="90" stroke="#9ca3af" strokeWidth="1.2" />

{/* ── Level 2: Four nodes ── */}
<rect x="30" y="170" width="90" height="36" rx="6" stroke="#374151" strokeWidth="1" fill="#f9fafb" />
<text x="75" y="193" textAnchor="middle" className="fill-[#6b7280]" fontSize="10" fontFamily="monospace">
node3 = 150
</text>

<rect x="160" y="170" width="90" height="36" rx="6" stroke="#374151" strokeWidth="1" fill="#f9fafb" />
<text x="205" y="193" textAnchor="middle" className="fill-[#6b7280]" fontSize="10" fontFamily="monospace">
node4 = 200
</text>

<rect x="310" y="170" width="90" height="36" rx="6" stroke="#374151" strokeWidth="1" fill="#f9fafb" />
<text x="355" y="193" textAnchor="middle" className="fill-[#6b7280]" fontSize="10" fontFamily="monospace">
node5 = 250
</text>

<rect x="440" y="170" width="90" height="36" rx="6" stroke="#374151" strokeWidth="1" fill="#f9fafb" />
<text x="485" y="193" textAnchor="middle" className="fill-[#6b7280]" fontSize="10" fontFamily="monospace">
node6 = 200
</text>

{/* Lines: level 1 → level 2 */}
<line x1="125" y1="126" x2="90" y2="170" stroke="#9ca3af" strokeWidth="1" />
<line x1="175" y1="126" x2="195" y2="170" stroke="#9ca3af" strokeWidth="1" />
<line x1="385" y1="126" x2="345" y2="170" stroke="#9ca3af" strokeWidth="1" />
<line x1="435" y1="126" x2="475" y2="170" stroke="#9ca3af" strokeWidth="1" />

{/* ── Level 3: Eight leaves ── */}
{[
{ x: 10, label: 'L0', val: '80' },
{ x: 75, label: 'L1', val: '70' },
{ x: 140, label: 'L2', val: '100' },
{ x: 205, label: 'L3', val: '100' },
{ x: 290, label: 'L4', val: '120' },
{ x: 355, label: 'L5', val: '130' },
{ x: 420, label: 'L6', val: '90' },
{ x: 485, label: 'L7', val: '110' }
].map((leaf, i) => (
<g key={i}>
<rect x={leaf.x} y={260} width="60" height="36" rx="6" stroke="#059669" strokeWidth="1.2" fill="#ecfdf5" />
<text x={leaf.x + 30} y={275} textAnchor="middle" className="fill-[#059669]" fontSize="10" fontWeight="600" fontFamily="sans-serif">
{leaf.label}
</text>
<text x={leaf.x + 30} y={289} textAnchor="middle" className="fill-[#6b7280]" fontSize="9" fontFamily="monospace">
{leaf.val}
</text>
</g>
))}

{/* Lines: level 2 → leaves */}
<line x1="52" y1="206" x2="40" y2="260" stroke="#9ca3af" strokeWidth="1" />
<line x1="98" y1="206" x2="105" y2="260" stroke="#9ca3af" strokeWidth="1" />
<line x1="185" y1="206" x2="170" y2="260" stroke="#9ca3af" strokeWidth="1" />
<line x1="225" y1="206" x2="235" y2="260" stroke="#9ca3af" strokeWidth="1" />
<line x1="335" y1="206" x2="320" y2="260" stroke="#9ca3af" strokeWidth="1" />
<line x1="375" y1="206" x2="385" y2="260" stroke="#9ca3af" strokeWidth="1" />
<line x1="465" y1="206" x2="450" y2="260" stroke="#9ca3af" strokeWidth="1" />
<line x1="505" y1="206" x2="515" y2="260" stroke="#9ca3af" strokeWidth="1" />

{/* ── Draw traversal annotation ── */}
<text x="280" y="330" textAnchor="middle" className="fill-[#9ca3af]" fontSize="10" fontFamily="sans-serif" fontStyle="italic">
draw(ticket): ticket {'<'} nodeSum {'→'} go left, else go right
</text>

{/* ── setLeaf annotation ── */}
<text x="280" y="350" textAnchor="middle" className="fill-[#9ca3af]" fontSize="10" fontFamily="sans-serif" fontStyle="italic">
setLeaf: update leaf, propagate sum upward through all 3 levels
</text>

{/* ── Conservation annotation ── */}
<text x="280" y="385" textAnchor="middle" className="fill-[#9ca3af]" fontSize="10" fontFamily="sans-serif">
root = 80 + 70 + 100 + 100 + 120 + 130 + 90 + 110 = 800 (conserved)
</text>
</svg>
</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: 'kleros-sortition-tree',
title: 'Kleros Sortition Tree Conservation & Draw Invariants',
subtitle:
'Formally verified stake conservation and fair juror selection for the Kleros dispute resolution protocol.',
description:
'How we proved total stake conservation and draw fairness across the Kleros sortition tree using Verity and Lean 4.',
date: '2026-04-16',
tag: 'Case study'
},
{
slug: 'stream-recovery-claim',
title: 'StreamRecoveryClaim Accounting Invariants',
Expand Down
3 changes: 2 additions & 1 deletion pages/research/index.jsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,8 @@ const caseStudyOrder = [
'safe-owner-reachability',
'lido-vault-solvency',
'nexus-mutual-book-value',
'stream-recovery-claim'
'stream-recovery-claim',
'kleros-sortition-tree'
]

export default function ResearchPage() {
Expand Down
Loading