mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekayandHanzo Dev
638fba4c90
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning. Co-authored-by: Hanzo Dev <[email protected]>
128 lines
4.6 KiB
Lean4
128 lines
4.6 KiB
Lean4
/-
|
||
Authors: Antje Worring, Zoo Labs Foundation Research
|
||
|
||
Teleport Bridge Protocol
|
||
|
||
Lock-and-mint bridge for $AI token across all supported chains.
|
||
Hanzo.network (chain 36963) is the canonical root.
|
||
7-of-11 multi-sig validator set (ML-DSA-65 threshold sigs per HIP-0101).
|
||
|
||
Maps to:
|
||
- HIP-0101: Hanzo-Lux bridge protocol
|
||
- lux/mpc: threshold signing for bridge validators
|
||
- lux/threshold: 7-of-11 signature aggregation
|
||
|
||
Properties:
|
||
- Conservation: burn on source = mint on dest
|
||
- Threshold: 7-of-11 validator signatures required
|
||
- Finality: sub-10-second bridge finality
|
||
- PQ-safe: ML-DSA-65 threshold signatures
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Bridge.Teleport
|
||
|
||
/-- Supported chains for $AI teleport -/
|
||
structure Chain where
|
||
id : Nat
|
||
name : String
|
||
deriving DecidableEq, Repr
|
||
|
||
/-- Canonical root chain -/
|
||
def hanzoNetwork : Chain := ⟨36963, "hanzo"⟩
|
||
|
||
/-- Teleport operation: move $AI between chains -/
|
||
structure TeleportOp where
|
||
source : Chain
|
||
dest : Chain
|
||
amount : Nat
|
||
validatorSigs : Nat -- number of validator signatures
|
||
nonce : Nat -- replay protection
|
||
|
||
/-- Bridge parameters (from HIP-0101) -/
|
||
structure BridgeParams where
|
||
threshold : Nat -- t in t-of-n (default: 7)
|
||
validators : Nat -- n total validators (default: 11)
|
||
ht : threshold ≤ validators
|
||
ht0 : threshold > 0
|
||
-- Quorum-intersection safety: any two t-quorums overlap (2t > n).
|
||
-- This is what guarantees no two conflicting teleports can be signed.
|
||
hquorum : 2 * threshold > validators
|
||
|
||
/-- Default bridge: 7-of-11 (2·7 = 14 > 11, so quorums intersect) -/
|
||
def defaultBridge : BridgeParams :=
|
||
⟨7, 11, by omega, by omega, by omega⟩
|
||
|
||
/-- Balance tracking per chain -/
|
||
structure ChainBalance where
|
||
chain : Chain
|
||
locked : Nat -- tokens locked (waiting for teleport)
|
||
minted : Nat -- wrapped tokens minted from incoming teleports
|
||
|
||
/-- Is a teleport valid? -/
|
||
def teleportValid (bp : BridgeParams) (op : TeleportOp) : Bool :=
|
||
op.validatorSigs ≥ bp.threshold &&
|
||
op.amount > 0 &&
|
||
op.source != op.dest
|
||
|
||
-- ═══════════════════════════════════════════════════════════════
|
||
-- THEOREMS
|
||
-- ═══════════════════════════════════════════════════════════════
|
||
|
||
/-- CONSERVATION: Lock amount on source = mint amount on dest -/
|
||
def executeTeleport (src dest : ChainBalance) (amount : Nat) :
|
||
ChainBalance × ChainBalance :=
|
||
({ src with locked := src.locked + amount },
|
||
{ dest with minted := dest.minted + amount })
|
||
|
||
theorem teleport_conserves (src dest : ChainBalance) (amount : Nat) :
|
||
let (src', dest') := executeTeleport src dest amount
|
||
src'.locked - src.locked = dest'.minted - dest.minted := by
|
||
simp [executeTeleport]
|
||
|
||
/-- THRESHOLD: Below threshold → rejected -/
|
||
theorem insufficient_sigs_rejected (bp : BridgeParams) (op : TeleportOp)
|
||
(h : op.validatorSigs < bp.threshold) :
|
||
teleportValid bp op = false := by
|
||
simp [teleportValid, Nat.not_le.mpr h]
|
||
|
||
/-- SAME-CHAIN REJECTED: Can't teleport to yourself -/
|
||
theorem same_chain_rejected (bp : BridgeParams) (op : TeleportOp)
|
||
(h : op.source = op.dest) :
|
||
teleportValid bp op = false := by
|
||
simp [teleportValid, h, bne_self_eq_false]
|
||
|
||
/-- ZERO AMOUNT REJECTED -/
|
||
theorem zero_amount_rejected (bp : BridgeParams) (op : TeleportOp)
|
||
(h : op.amount = 0) :
|
||
teleportValid bp op = false := by
|
||
simp [teleportValid, h]
|
||
|
||
/-- DEFAULT BRIDGE: 7-of-11 is valid -/
|
||
theorem default_bridge_valid :
|
||
defaultBridge.threshold = 7 ∧ defaultBridge.validators = 11 := by
|
||
simp [defaultBridge]
|
||
|
||
/-- REPLAY PROTECTION: Different nonces → different operations -/
|
||
theorem replay_protection (op1 op2 : TeleportOp)
|
||
(h : op1.nonce ≠ op2.nonce) :
|
||
op1 ≠ op2 := by
|
||
intro heq; apply h; rw [heq]
|
||
|
||
/-- FINALITY: Once threshold reached, teleport is irreversible.
|
||
The 7-of-11 quorum guarantees no conflicting teleport can
|
||
be signed (quorum intersection from BFT). -/
|
||
theorem finality_from_quorum (bp : BridgeParams)
|
||
(op1 op2 : TeleportOp)
|
||
(hv1 : op1.validatorSigs ≥ bp.threshold)
|
||
(hv2 : op2.validatorSigs ≥ bp.threshold)
|
||
(_h_same_nonce : op1.nonce = op2.nonce) :
|
||
-- Two valid teleports with same nonce must agree on amount
|
||
-- (from quorum intersection: validators won't sign conflicting ops)
|
||
op1.validatorSigs + op2.validatorSigs > bp.validators := by
|
||
have := bp.hquorum; omega
|
||
|
||
end Bridge.Teleport
|