From ef7c98791c4c50cade1056fde8ee743e9ef953ce Mon Sep 17 00:00:00 2001 From: Fricoben Date: Thu, 16 Apr 2026 17:37:08 +0100 Subject: [PATCH] feat: add Kleros Sortition Tree case study Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/KlerosGuarantee.jsx | 86 ++++ components/research/SortitionDrawExample.jsx | 155 ++++++ components/research/SortitionTreeDiagram.jsx | 107 ++++ data/research.js | 10 + pages/research/index.jsx | 3 +- pages/research/kleros-sortition-tree.jsx | 505 +++++++++++++++++++ 6 files changed, 865 insertions(+), 1 deletion(-) create mode 100644 components/research/KlerosGuarantee.jsx create mode 100644 components/research/SortitionDrawExample.jsx create mode 100644 components/research/SortitionTreeDiagram.jsx create mode 100644 pages/research/kleros-sortition-tree.jsx diff --git a/components/research/KlerosGuarantee.jsx b/components/research/KlerosGuarantee.jsx new file mode 100644 index 0000000..fd9df5c --- /dev/null +++ b/components/research/KlerosGuarantee.jsx @@ -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 ( +
+ + +
+
+ {FORMAL_INVARIANTS.map((formal, i) => ( + + {formal} + + ))} +
+
+

+ The sortition tree always conserves total stake, and the draw + mechanism selects jurors with probability exactly proportional to + their stake. +

+
+
+
+ ) +} diff --git a/components/research/SortitionDrawExample.jsx b/components/research/SortitionDrawExample.jsx new file mode 100644 index 0000000..9be56f1 --- /dev/null +++ b/components/research/SortitionDrawExample.jsx @@ -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 ( +
+ + {/* ── Level 0: Root (active) ── */} + + + root = 800 + + {/* ticket label at root */} + + ticket = 200 + + + {/* ── Level 1 ── */} + {/* node1 (active, go left) */} + + + node1 = 350 + + + {/* node2 (inactive) */} + + + node2 = 450 + + + {/* Lines: root to level 1 */} + + + + {/* Decision label: 200 < 350, go left */} + + 200 {'<'} 350 + + + go left + + + {/* ── Level 2 ── */} + {/* node3 (inactive) */} + + + node3 = 150 + + + {/* node4 (active, go right) */} + + + node4 = 200 + + + {/* node5 (inactive) */} + + + node5 = 250 + + + {/* node6 (inactive) */} + + + node6 = 200 + + + {/* Lines: level 1 to level 2 */} + + + + + + {/* Decision label: 200 >= 150, go right, ticket = 50 */} + + 200 {'≥'} 150 + + + go right, ticket = 50 + + + {/* ── 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) => ( + + + + {leaf.label} + + + {leaf.val} + + + ))} + + {/* Lines: level 2 to leaves */} + + + + + + + + + + {/* Decision label: 50 < 100, go left */} + + 50 {'<'} 100 + + + go left + + + {/* Selected juror callout */} + + Selected + + + {/* Result annotation */} + + L2 owns tickets 150 to 249 (100 out of 800 = 12.5% chance) + + +
+ ) +} diff --git a/components/research/SortitionTreeDiagram.jsx b/components/research/SortitionTreeDiagram.jsx new file mode 100644 index 0000000..80b8d64 --- /dev/null +++ b/components/research/SortitionTreeDiagram.jsx @@ -0,0 +1,107 @@ +export default function SortitionTreeDiagram({ className = '' }) { + return ( +
+ + {/* ── Level 0: Root ── */} + + + root = 800 + + + {/* ── Level 1: Two subtree roots ── */} + + + node1 = 350 + + + + + node2 = 450 + + + {/* Lines: root → level 1 */} + + + + {/* ── Level 2: Four nodes ── */} + + + node3 = 150 + + + + + node4 = 200 + + + + + node5 = 250 + + + + + node6 = 200 + + + {/* Lines: level 1 → level 2 */} + + + + + + {/* ── 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) => ( + + + + {leaf.label} + + + {leaf.val} + + + ))} + + {/* Lines: level 2 → leaves */} + + + + + + + + + + {/* ── Draw traversal annotation ── */} + + draw(ticket): ticket {'<'} nodeSum {'→'} go left, else go right + + + {/* ── setLeaf annotation ── */} + + setLeaf: update leaf, propagate sum upward through all 3 levels + + + {/* ── Conservation annotation ── */} + + root = 80 + 70 + 100 + 100 + 120 + 130 + 90 + 110 = 800 (conserved) + + +
+ ) +} diff --git a/data/research.js b/data/research.js index 468b89d..4f5c7e2 100644 --- a/data/research.js +++ b/data/research.js @@ -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', diff --git a/pages/research/index.jsx b/pages/research/index.jsx index 87159e4..245ee58 100644 --- a/pages/research/index.jsx +++ b/pages/research/index.jsx @@ -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() { diff --git a/pages/research/kleros-sortition-tree.jsx b/pages/research/kleros-sortition-tree.jsx new file mode 100644 index 0000000..fe6e8bf --- /dev/null +++ b/pages/research/kleros-sortition-tree.jsx @@ -0,0 +1,505 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import KlerosGuarantee from '../../components/research/KlerosGuarantee' +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 SortitionTreeDiagram from '../../components/research/SortitionTreeDiagram' +import SortitionDrawExample from '../../components/research/SortitionDrawExample' +import { getSortedResearch } from '../../lib/getSortedResearch' + +const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark +cd verity-benchmark +lake build Benchmark.Cases.Kleros.SortitionTrees.Compile` + +const UPSTREAM_CONTRACT = + 'https://github.com/kleros/kleros-v2/blob/75125dfa/contracts/src/libraries/SortitionTrees.sol' + +const VERITY_CONTRACT = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Kleros/SortitionTrees/Contract.lean' + +const SPECS_URL = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Kleros/SortitionTrees/Specs.lean' + +const PROOFS_URL = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Kleros/SortitionTrees/Proofs.lean' + +export default function KlerosSortitionTreePage() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'kleros-sortition-tree' + ) + + return ( + <> + + + Kleros Sortition Tree Conservation & Draw Invariants | Research | LFG + Labs + + + + +
+ + +
+

+ Kleros Sortition Tree Conservation & Draw Invariants +

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

+ Kleros is a + decentralized dispute resolution protocol, an on-chain + court system. When two parties disagree (over an escrow payment, a + content moderation decision, an insurance claim), they submit the + dispute to Kleros. The protocol randomly selects a panel of jurors + from a pool of PNK token stakers, the jurors vote, and the + majority ruling is enforced on-chain. +

+

+ For this to be fair, juror selection must be both random and + stake-weighted: a juror who staked twice as much PNK should be + twice as likely to be drawn. The{' '} + + sortition tree + {' '} + is the data structure that makes this possible. It is a + sum-tree where each leaf holds one juror's staked weight, and + each internal node holds the sum of its children. The root always + equals the total staked amount. +

+ +

+ To select a juror, the protocol picks a random number + (the “ticket”) between 0 and the root. Think of it + as a number line of length 800, split into segments, one per + juror, sized by their stake. The tree turns this lookup into a + three-step walk from root to leaf. +

+

+ Example with{' '} + ticket = 200: +

+
    +
  1. + Root (800): left subtree = 350. + 200 < 350, so go left. +
    2. +
  2. + Node1 (350): left child = 150. + 200 ≥ 150, so subtract 150 and go right. + Remaining ticket = 50. +
    3. +
  3. + Node4 (200): left child (L2) = 100. + 50 < 100, so go left. The draw lands + on L2. +
    4. +
+ +

+ Any ticket from 150 to 249 follows the same path and lands on + L2. The ticket is drawn uniformly at random from 0 to 799, + so L2 owns 100 out of 800 possible values: its selection + probability is exactly 100/800. The same applies to every leaf. +

+

+

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

+ Why this matters +

+

+ Kleros handles real arbitration with real money at stake. If a + propagation bug means the root does not reflect actual total + stake, draw intervals shift and some jurors are systematically + over- or under-selected. Every dispute resolved by a biased + jury is compromised. +

+ +

+ In scope (12 proven theorems): +

+
    +
  • + level2_parent_equals_sum_of_children: Each + grandparent-of-leaves node equals the sum of its two leaf + children (4 nodes verified) +
    • +
  • + level1_parent_equals_sum_of_children: Each + subtree-root node equals the sum of its two level-2 children (2 + nodes verified) +
    • +
  • + root_equals_sum_of_leaves: Root = sum of all 8 + leaf weights (total stake conservation) +
    • +
  • + root_minus_left_equals_right_subtree: Root + partitions cleanly into left and right subtrees +
    • +
  • + draw_selects_valid_leaf: Every draw lands on a + valid leaf index (7..14) +
    • +
  • + draw_interval_matches_weights: Draw intervals + match leaf weights across all 3 traversal levels (8-way + coverage) +
    • +
  • + node_id_bijection: Forward and reverse ID + mappings are consistent +
    • +
  • + sequential_setLeaf_root_conservation: + Conservation holds inductively after multiple operations +
    • +
+
    +
  • + overflow_safety_of_no_wrap /{' '} + level1_overflow_safety_of_no_wrap: node sums + never exceed 2256 - 1 and wrap around + to zero, proven under explicit no-wrap assumptions +
    • +
  • + remove_leaf_zeroed /{' '} + remove_leaf_clears_associated_id: removing a + juror sets their leaf weight to zero and clears all associated + mappings +
    • +
+

+ No ghost draws (not proven as a separate + theorem): we originally wanted to prove that a draw can never + select a juror whose stake is zero. When we tried to formalize + this as its own statement, a counterexample showed the naive + formulation was wrong. However, the guarantee still holds: it + follows directly from two theorems that are already proven. If + the root equals the sum of all leaves ( + + root_equals_sum_of_leaves + + ) and each leaf's draw interval equals its weight ( + + draw_interval_matches_weights + + ), then a leaf with weight 0 has an interval of size 0, so no + ticket can ever land on it. +

+

+ Simplifications (the benchmark works on a + simplified version of the production contract): +

+
    +
  • + The production tree supports a variable number of children per + node (K-ary). The benchmark fixes K=2 (binary tree) to isolate + the core logic. +
    • +
  • + Low-level encoding details (bytes32 stake-path packing, vacancy + stack) are abstracted. +
    • +
  • + Ticket generation uses keccak256 in production. The benchmark + treats the ticket as an opaque number, proving fairness for any + ticket value, not just hash-derived ones. +
    • +
+

+ The benchmark specializes the production sortition tree to a + balanced binary tree with eight leaves (three levels). This + preserves the core algorithmic logic (parent-sum propagation and + weighted-interval draw traversal) while abstracting encoding and + randomness details that Verity does not yet support. +

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

+ How this was proven +

+

+ We translated the Solidity{' '} + + SortitionTrees.sol + {' '} + into{' '} + Verity, our + Lean 4 framework for writing smart contract logic as + mathematical definitions. Once the contract is expressed in Lean, + we can state properties about it and prove them. +

+

+ Two kinds of properties were proven: +

+
    +
  • + Conservation: after any{' '} + setLeaf call, + every parent still equals the sum of its children, all the way + up to the root. We proved this level by level (leaves → + mid-nodes → root), then composed those results to show + that the root always equals the sum of all 8 leaves. +
    • +
  • + Draw fairness: for any valid ticket, the draw + function lands on a real leaf, and each leaf's draw + interval matches its weight exactly. The proof considers each + of the 8 leaf positions separately, but within each position + it covers every possible combination of weights and ticket + values, not just specific examples. Eight universal proofs, + not eight test cases. +
    • +
+

+ All proofs are checked by Lean 4's type-checking kernel. + This is not testing or simulation: if any proof 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 12 theorems are proven.{' '} + Proofs.lean{' '} + contains no unfinished proofs. +

+

+ The table below shows which properties have been proven for each + function. “Conservation” means the tree sums stay + correct. “Draw correctness” means the draw always + picks a valid leaf with the right probability. + “Composition” means the property still holds after + multiple operations in sequence. +

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ Function + + Conservation + + Draw correctness + + ID mapping + + Composition +
setLeaf + proven + + – + + proven + + proven +
draw + – + + proven + + – + + – +
removeLeaf + – + + – + + proven + + – +
+
+
+ + {/* Assumptions */} +
+

+ Assumptions +

+

+ The proofs use zero axioms. Most hypotheses correspond directly + to Solidity{' '} + require statements + that revert the transaction if violated. The overflow and removal + proofs carry additional assumptions noted below. +

+
    + + The caller passes a valid leaf index. Enforced by{' '} + require guards in + the contract. Matches the Solidity implementation's bounds + check for the 8-leaf tree. + + + The tree is non-empty. Enforced by{' '} + + require(root != 0) + {' '} + in the draw function. A draw on an empty tree would be + meaningless. + + + The ticket is within the valid range. Enforced by{' '} + + require(ticket {'<'} root) + {' '} + in the draw function. Ensures the ticket falls within the total + stake interval. + + + The mathematical sum of leaf weights does not exceed + 2256 - 1. This assumption is only used by + the overflow safety theorems. The core conservation and draw + proofs do not depend on it. + + + The caller knows which juror ID was associated with the leaf + being removed. Used only by the removal cleanup proofs. + +
+

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

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

+ Learn more +

+

+ + Kleros V2 repository + + {', the upstream protocol.'} +

+

+ + Verity Benchmark + + {', the open-source benchmark suite.'} +

+

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

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

+ More research +

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