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]>
85 lines
2.6 KiB
Lean4
85 lines
2.6 KiB
Lean4
/-
|
|
Decentralized AI Compute Swarm (HIP-0023)
|
|
|
|
Distributed GPU cluster for AI inference and training.
|
|
Nodes join/leave dynamically. Work is load-balanced.
|
|
|
|
Maps to:
|
|
- HIP-0023: Decentralized AI Compute Swarm Protocol
|
|
- HIP-0096: AI Compute Contribution Rewards
|
|
- hanzo/engine: inference provider nodes
|
|
|
|
Properties:
|
|
- Load balancing: work distributed proportional to capacity
|
|
- Fault tolerance: node failure doesn't lose work
|
|
- Accretive: rewards proportional to proven compute
|
|
- Dynamic: nodes can join/leave without disruption
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace Compute.Swarm
|
|
|
|
/-- A compute node in the swarm -/
|
|
structure Node where
|
|
id : Nat
|
|
capacity : Nat -- GPU-hours available
|
|
active : Bool
|
|
totalComputed : Nat -- lifetime compute contributed
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- Swarm state -/
|
|
structure SwarmState where
|
|
nodes : List Node
|
|
totalCapacity : Nat
|
|
pendingTasks : Nat
|
|
|
|
/-- Active nodes in the swarm -/
|
|
def activeNodes (s : SwarmState) : List Node :=
|
|
s.nodes.filter (·.active)
|
|
|
|
/-- Total active capacity -/
|
|
def activeCapacity (s : SwarmState) : Nat :=
|
|
(activeNodes s).foldl (fun acc n => acc + n.capacity) 0
|
|
|
|
/-- Add a node to the swarm -/
|
|
def joinSwarm (s : SwarmState) (n : Node) : SwarmState :=
|
|
{ s with nodes := n :: s.nodes
|
|
, totalCapacity := s.totalCapacity + n.capacity }
|
|
|
|
/-- Remove a node (mark inactive) -/
|
|
def leaveSwarm (s : SwarmState) (nodeId : Nat) : SwarmState :=
|
|
{ s with nodes := s.nodes.map (fun n =>
|
|
if n.id = nodeId then { n with active := false } else n) }
|
|
|
|
/-- JOINING INCREASES CAPACITY -/
|
|
theorem join_increases_capacity (s : SwarmState) (n : Node) :
|
|
(joinSwarm s n).totalCapacity = s.totalCapacity + n.capacity := by
|
|
simp [joinSwarm]
|
|
|
|
/-- LEAVING PRESERVES NODE COUNT -/
|
|
theorem leave_preserves_count (s : SwarmState) (nodeId : Nat) :
|
|
(leaveSwarm s nodeId).nodes.length = s.nodes.length := by
|
|
simp [leaveSwarm, List.length_map]
|
|
|
|
/-- FAULT TOLERANCE: One node leaving doesn't empty the swarm -/
|
|
theorem single_failure_survives (s : SwarmState) (nodeId : Nat)
|
|
(h : s.nodes.length ≥ 2) :
|
|
(leaveSwarm s nodeId).nodes.length ≥ 2 := by
|
|
simp [leaveSwarm, List.length_map]; exact h
|
|
|
|
/-- ACCRETIVE: Computed work only increases -/
|
|
def recordCompute (n : Node) (units : Nat) : Node :=
|
|
{ n with totalComputed := n.totalComputed + units }
|
|
|
|
theorem compute_monotone (n : Node) (units : Nat) :
|
|
(recordCompute n units).totalComputed ≥ n.totalComputed := by
|
|
simp [recordCompute]
|
|
|
|
/-- EMPTY SWARM HAS ZERO CAPACITY -/
|
|
theorem empty_zero : activeCapacity ⟨[], 0, 0⟩ = 0 := rfl
|
|
|
|
end Compute.Swarm
|