Skip to content

docs: clarify formal invariants #28

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 21, 2026
Merged

docs: clarify formal invariants #28

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
15 changes: 10 additions & 5 deletions components/research/ZamaGuarantee.jsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,11 @@ 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'
'\u2200 sender recipient amount s s\u2032, balances\u2032[sender] + balances\u2032[recipient] = balances[sender] + balances[recipient]',
'\u2200 sender recipient amount s s\u2032, balances[sender] \u2265 amount \u2192 balances\u2032[sender] = balances[sender] \u2212 amount \u2227 balances\u2032[recipient] = balances[recipient] + amount',
'\u2200 sender recipient amount s s\u2032, balances[sender] < amount \u2192 balances\u2032[sender] = balances[sender] \u2227 balances\u2032[recipient] = balances[recipient]',
'\u2200 sender recipient amount s, \u00ACreverts',
'\u2200 sender recipient amount s s\u2032, totalSupply\u2032 = totalSupply'
]

export default function ZamaGuarantee() {
Expand Down Expand Up @@ -91,6 +91,11 @@ export default function ZamaGuarantee() {
</div>
</div>

<p className="mt-4 text-[12px] leading-relaxed text-muted">
In the formal view, each statement ranges over all transfer inputs and
states satisfying the assumptions listed below.
</p>

<div className="text-right mt-4">
<a
href="https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Zama/ERC7984ConfidentialToken/Specs.lean"
Expand Down