Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
116 changes: 116 additions & 0 deletions components/research/ConfidentialTransferDiagram.jsx
Original file line number Diff line number Diff line change
@@ -0,0 +1,116 @@
export default function ConfidentialTransferDiagram({ className = '' }) {
return (
<div className={className}>
<div className="grid grid-cols-1 md:grid-cols-2 gap-4">
{/* ERC-20 */}
<div className="border border-gray-200 rounded-lg p-5">
<p className="text-[12px] font-semibold text-muted uppercase tracking-wider mb-5">
ERC-20 transfer
</p>

{/* Scenario: enough funds */}
<div className="mb-5">
<p className="text-[11px] font-medium text-emerald-600 mb-2 flex items-center gap-1.5">
<span className="inline-block w-1.5 h-1.5 rounded-full bg-emerald-500" />
Alice has 100, sends 50 to Bob
</p>
<div className="flex items-center gap-3 text-[13px]">
<div className="flex-1 rounded bg-gray-50 border border-gray-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Alice</span>
<span className="font-mono">100 → 50</span>
</div>
<span className="text-muted text-[16px]">→</span>
<div className="flex-1 rounded bg-gray-50 border border-gray-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Bob</span>
<span className="font-mono">0 → 50</span>
</div>
</div>
<p className="text-[11px] text-emerald-600 mt-1.5 font-medium">
✓ Transfer succeeds
</p>
</div>

{/* Scenario: not enough funds */}
<div>
<p className="text-[11px] font-medium text-red-500 mb-2 flex items-center gap-1.5">
<span className="inline-block w-1.5 h-1.5 rounded-full bg-red-400" />
Alice has 30, sends 50 to Bob
</p>
<div className="flex items-center gap-3 text-[13px]">
<div className="flex-1 rounded bg-red-50 border border-red-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Alice</span>
<span className="font-mono line-through text-red-400">
30
</span>
</div>
<span className="text-red-300 text-[16px]">✕</span>
<div className="flex-1 rounded bg-red-50 border border-red-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Bob</span>
<span className="font-mono line-through text-red-400">0</span>
</div>
</div>
<p className="text-[11px] text-red-500 mt-1.5 font-medium">
✕ Transaction reverts. Everyone sees it failed.
</p>
</div>
</div>

{/* ERC-7984 */}
<div className="border border-gray-200 rounded-lg p-5 bg-[#fafafa]">
<p className="text-[12px] font-semibold text-muted uppercase tracking-wider mb-5">
ERC-7984 transfer (encrypted)
</p>

{/* Scenario: enough funds */}
<div className="mb-5">
<p className="text-[11px] font-medium text-emerald-600 mb-2 flex items-center gap-1.5">
<span className="inline-block w-1.5 h-1.5 rounded-full bg-emerald-500" />
Alice has 100, sends 50 to Bob
</p>
<div className="flex items-center gap-3 text-[13px]">
<div className="flex-1 rounded bg-gray-50 border border-gray-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Alice</span>
<span className="font-mono">🔒 → 🔒</span>
</div>
<span className="text-muted text-[16px]">→</span>
<div className="flex-1 rounded bg-gray-50 border border-gray-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Bob</span>
<span className="font-mono">🔒 → 🔒</span>
</div>
</div>
<p className="text-[11px] text-emerald-600 mt-1.5 font-medium">
✓ 50 moved, but amounts stay hidden
</p>
</div>

{/* Scenario: not enough funds */}
<div>
<p className="text-[11px] font-medium text-amber-600 mb-2 flex items-center gap-1.5">
<span className="inline-block w-1.5 h-1.5 rounded-full bg-amber-500" />
Alice has 30, sends 50 to Bob
</p>
<div className="flex items-center gap-3 text-[13px]">
<div className="flex-1 rounded bg-amber-50 border border-amber-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Alice</span>
<span className="font-mono">🔒 → 🔒</span>
</div>
<span className="text-amber-400 text-[16px]">→</span>
<div className="flex-1 rounded bg-amber-50 border border-amber-200 px-3 py-2 text-center">
<span className="text-muted text-[11px] block">Bob</span>
<span className="font-mono">🔒 → 🔒</span>
</div>
</div>
<p className="text-[11px] text-amber-600 mt-1.5 font-medium">
✓ Tx succeeds, but 0 moved. No one can tell it failed.
</p>
</div>
</div>
</div>

<p className="mt-3 text-center text-[11px] text-muted/70">
ERC-7984 never reverts on insufficient balance. Reverting would reveal
that the sender doesn&apos;t have enough funds.
</p>
</div>
)
}
107 changes: 107 additions & 0 deletions components/research/ZamaGuarantee.jsx
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
import { useState, useEffect, useRef } from 'react'
import { ExternalLinkIcon } from './ExternalLink'

const FORMAL_INVARIANTS = [
'balances\u2032[from] + balances\u2032[to] = balances[from] + balances[to]',
'balance \u2265 amount \u2192 balances\u2032[from] = balances[from] \u2212 amount \u2227 balances\u2032[to] = balances[to] + amount',
'balance < amount \u2192 balances\u2032[from] = balances[from] \u2227 balances\u2032[to] = balances[to]',
'balance < amount \u2192 \u00ACreverts',
'\u2200 transfer, totalSupply\u2032 = totalSupply'
]

export default function ZamaGuarantee() {
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}
>
<div className="flex flex-col items-center gap-3 md:gap-4 max-w-prose mx-auto px-1">
<p className="text-xl md:text-2xl leading-snug font-serif">
Tokens are never created or destroyed by a transfer.
</p>
<p className="text-xl md:text-2xl leading-snug font-serif">
Sufficient transfers move exactly the requested amount.
</p>
<p className="text-xl md:text-2xl leading-snug font-serif">
Insufficient transfers change nothing and never revert.
</p>
</div>
</div>
</div>

<div className="text-right mt-4">
<a
href="https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Zama/ERC7984ConfidentialToken/Specs.lean"
target="_blank"
rel="noopener noreferrer"
className="inline-flex items-center gap-1.5 text-[12px] font-semibold text-accent hover:text-heading transition-colors cursor-pointer"
>
View Lean
<ExternalLinkIcon />
</a>
</div>
</div>
)
}
10 changes: 10 additions & 0 deletions data/research.js
Original file line number Diff line number Diff line change
@@ -1,4 +1,14 @@
export const research = [
{
slug: 'zama-erc7984-confidential-token',
title: 'ERC-7984 Confidential Token Invariants',
subtitle:
'Formally verified accounting properties of the Confidential Token Standard.',
description:
'How we proved transfer conservation, mint/burn correctness, and overflow protection for ERC-7984 (Zama fhEVM + OpenZeppelin) using Verity and Lean 4.',
date: '2026-04-16',
tag: 'Case study'
},
{
slug: 'stream-recovery-claim',
title: 'StreamRecoveryClaim Accounting Invariants',
Expand Down
Loading