mirror of
https://github.com/hanzoai/proofs.git
synced 2026-10-30 18:23:34 +00:00
zeekayandHanzo Dev
3626b96b68
Every library is a default target, so any one of these failing takes the whole build down. What each was: Compute/Billing.lean, Gateway/RateLimit.lean, CRDT/Anchor.lean — `simp [f] at h` already turns the guard into a conjunction, so the `split at h` after it had nothing left to split. Destructure the conjunction and state the reduced goal for omega. In `rate_limited` the simp closed the goal, so the line after it ran on none. Compute/ConfidentialCompute.lean — `a == b = true` does not parse: `==` and `=` are both precedence 50 and non-associative. State the propositional equality, which is the stronger claim anyway. Compute/PoAI.lean — `reward_bounded` was false as stated. qualityScore is unbounded in the type, so `rate ≤ 1000` alone does not bound computeUnits * rate * quality / 1000000 by computeUnits; quality = 10^9 breaks it. Added the range hypothesis on qualityScore that the 1000000 divisor normalizes against, and proved it. `canonical_root` was false of an arbitrary AISupply — nothing stops a record from teleporting more than was minted — so the bridge invariant it needs is now stated as `wellFormed`. `low_quality_no_mining` closed at the simp. Compute/Swarm.lean, KMS/Secrets.lean — trailing `omega` after a simp that had already closed the goal. AccessPolicy also needed `deriving Repr`, which SecretMeta's own Repr derivation requires of it. CRDT/Privacy.lean — `seal ` is a Lean command token, so a structure field named `seal` cannot parse. Backend fields take the names the Go interface uses (encrypt / decrypt) and the envelope layer is wrap / unwrap. `wrong_tag` needed the tag inequality in the direction the guard tests it, and both message theorems needed mapM' so the goal did not unfold into List.mapM.loop. Gateway/Auth.lean — checkAuth calls the axiomatized verifyToken, so it has no code to compile: noncomputable. Platform/SBOM.lean — simp had already pushed the negation inward, leaving push_neg nothing to do, and `List.all_cons` left a goal in ∀-form that the Bool-form hypothesis does not close. Three statements compiled while asserting nothing, and now carry a claim: enclave_isolation and attestation_constant_size stated `True`, and derived_key_isolation returned its own hypothesis. Isolation is now non-interference over a host view — two attested tasks differing only in enclave payload look identical from outside — and derived_key_isolation derives the master's confinement from hsm_boundary, which until now no theorem used. lake build exits 0. vacuity.py: 0 vacuous declarations, down from 2, and no theorem rests on sorryAx. Co-authored-by: Hanzo Dev <[email protected]>
162 lines
6.7 KiB
Lean4
162 lines
6.7 KiB
Lean4
/-
|
|
Proof of AI (PoAI) — Hanzo Native Consensus
|
|
|
|
$AI is the native currency on hanzo.network (chain ID 36963).
|
|
Minted via Proof of Compute mining on the sovereign L1.
|
|
Teleportable to any supported chain via lock-and-mint bridge (HIP-0101).
|
|
|
|
Maps to:
|
|
- HIP-0001: $AI token specification
|
|
- HIP-0024: Hanzo sovereign L1 architecture
|
|
- HIP-0096: AI compute contribution rewards
|
|
- HIP-0101: Hanzo-Lux bridge protocol
|
|
- hanzo/engine: inference provider (compute source)
|
|
|
|
Properties:
|
|
- Mining: $AI minted only for TEE-attested proven compute
|
|
- Accretive: rewards are purely additive (no slashing of compute rewards)
|
|
- Teleport: burn on source chain, mint on dest chain (conservation)
|
|
- Canonical: hanzo.network is the root chain for all $AI
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace Compute.PoAI
|
|
|
|
/-- Chain identifier -/
|
|
structure ChainId where
|
|
id : Nat
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- Hanzo canonical chain (chain ID 36963) -/
|
|
def hanzoChain : ChainId := ⟨36963⟩
|
|
|
|
/-- Compute attestation from TEE (SGX/SEV/Blackwell CC) -/
|
|
structure ComputeProof where
|
|
provider : Nat -- validator/miner public key
|
|
computeUnits : Nat -- normalized GPU-hours
|
|
taskHash : Nat -- task specification hash
|
|
resultHash : Nat -- Merkle root of outputs
|
|
teeAttestation : Bool -- hardware attestation (NVIDIA CC, Intel SGX, AMD SEV)
|
|
qualityScore : Nat -- 0-1000 basis points
|
|
chain : ChainId -- which chain this was computed on
|
|
|
|
/-- Quality threshold for mining reward -/
|
|
def miningThreshold : Nat := 500
|
|
|
|
/-- Is compute proof eligible for $AI mining? -/
|
|
def isMineable (p : ComputeProof) : Bool :=
|
|
p.teeAttestation && p.qualityScore ≥ miningThreshold
|
|
|
|
/-- Mining reward calculation (purely accretive) -/
|
|
def miningReward (p : ComputeProof) (rewardRate : Nat) : Nat :=
|
|
if isMineable p then p.computeUnits * rewardRate * p.qualityScore / 1000000
|
|
else 0
|
|
|
|
/-- $AI supply state across all chains -/
|
|
structure AISupply where
|
|
hanzoMinted : Nat -- total minted on canonical chain
|
|
totalTeleported : Nat -- total teleported to other chains
|
|
burned : Nat -- burned during teleport-back
|
|
|
|
-- ═══════════════════════════════════════════════════════════════
|
|
-- MINING THEOREMS
|
|
-- ═══════════════════════════════════════════════════════════════
|
|
|
|
/-- TEE REQUIRED: No attestation → no mining reward -/
|
|
theorem no_tee_no_mining (p : ComputeProof) (rate : Nat)
|
|
(h : p.teeAttestation = false) :
|
|
miningReward p rate = 0 := by
|
|
simp [miningReward, isMineable, h]
|
|
|
|
/-- LOW QUALITY REJECTED: Below threshold → no mining reward -/
|
|
theorem low_quality_no_mining (p : ComputeProof) (rate : Nat)
|
|
(h : p.qualityScore < miningThreshold) :
|
|
miningReward p rate = 0 := by
|
|
simp [miningReward, isMineable, Nat.not_le.mpr h]
|
|
|
|
/-- ACCRETIVE: Mining rewards are non-negative -/
|
|
theorem mining_nonneg (p : ComputeProof) (rate : Nat) :
|
|
miningReward p rate ≥ 0 := Nat.zero_le _
|
|
|
|
/-- REWARD BOUNDED: Reward scales with compute, never exceeds it.
|
|
Requires both scaling factors to be in range: the reward rate at or
|
|
below 1000 and the quality score at or below its 1000-basis-point
|
|
maximum, which is what the 1000000 divisor in `miningReward`
|
|
normalizes against. -/
|
|
theorem reward_bounded (p : ComputeProof) (rate : Nat)
|
|
(h : rate ≤ 1000) (hq : p.qualityScore ≤ 1000) :
|
|
miningReward p rate ≤ p.computeUnits := by
|
|
unfold miningReward
|
|
split
|
|
· have hrq : rate * p.qualityScore ≤ 1000000 :=
|
|
le_trans (Nat.mul_le_mul h hq) (by norm_num)
|
|
have hbound : p.computeUnits * rate * p.qualityScore ≤ p.computeUnits * 1000000 := by
|
|
rw [mul_assoc]
|
|
exact Nat.mul_le_mul (le_refl _) hrq
|
|
calc p.computeUnits * rate * p.qualityScore / 1000000
|
|
≤ p.computeUnits * 1000000 / 1000000 := Nat.div_le_div_right hbound
|
|
_ = p.computeUnits := by omega
|
|
· exact Nat.zero_le _
|
|
|
|
-- ═══════════════════════════════════════════════════════════════
|
|
-- TELEPORT (CROSS-CHAIN) THEOREMS
|
|
-- ═══════════════════════════════════════════════════════════════
|
|
|
|
/-- Teleport state: burn on source, mint on dest -/
|
|
structure TeleportOp where
|
|
sourceChain : ChainId
|
|
destChain : ChainId
|
|
amount : Nat
|
|
bridgeSigs : Nat -- threshold signatures (7-of-11 per HIP-0101)
|
|
bridgeThreshold : Nat -- required threshold
|
|
|
|
/-- Teleport is valid iff threshold signatures present -/
|
|
def teleportValid (t : TeleportOp) : Bool :=
|
|
t.bridgeSigs ≥ t.bridgeThreshold && t.amount > 0
|
|
|
|
/-- Apply a teleport to the supply: a valid teleport moves `amount` into
|
|
the wrapped representation held on other chains. An invalid one is a
|
|
no-op. Neither branch touches `hanzoMinted`. -/
|
|
def applyTeleport (supply : AISupply) (t : TeleportOp) : AISupply :=
|
|
if teleportValid t then
|
|
{ supply with totalTeleported := supply.totalTeleported + t.amount }
|
|
else supply
|
|
|
|
/-- CONSERVATION: Teleport preserves total supply.
|
|
Burn on source = mint on dest, so the canonical mint count is
|
|
untouched by any teleport, valid or not. -/
|
|
theorem teleport_conservation (supply : AISupply) (t : TeleportOp) :
|
|
(applyTeleport supply t).hanzoMinted = supply.hanzoMinted := by
|
|
unfold applyTeleport
|
|
split <;> rfl
|
|
|
|
/-- THRESHOLD: Teleport requires bridge signatures -/
|
|
theorem teleport_needs_threshold (t : TeleportOp)
|
|
(h : t.bridgeSigs < t.bridgeThreshold) :
|
|
teleportValid t = false := by
|
|
simp [teleportValid, Nat.not_le.mpr h]
|
|
|
|
/-- A supply is well formed when everything teleported out and everything
|
|
burned was minted on the canonical chain first. This is the invariant
|
|
the bridge maintains; it does not hold of an arbitrary record. -/
|
|
def wellFormed (supply : AISupply) : Prop :=
|
|
supply.totalTeleported + supply.burned ≤ supply.hanzoMinted
|
|
|
|
/-- CANONICAL ROOT: All $AI originates from hanzo.network.
|
|
Teleported $AI is a wrapped representation on other chains, so it is
|
|
bounded by what the canonical chain minted and still holds. -/
|
|
theorem canonical_root (supply : AISupply) (wf : wellFormed supply) :
|
|
supply.totalTeleported ≤ supply.hanzoMinted - supply.burned := by
|
|
unfold wellFormed at wf
|
|
omega
|
|
|
|
/-- ZERO AMOUNT REJECTED -/
|
|
theorem zero_teleport_invalid (t : TeleportOp) (h : t.amount = 0) :
|
|
teleportValid t = false := by
|
|
simp [teleportValid, h]
|
|
|
|
end Compute.PoAI
|