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]>
93 lines
3.0 KiB
Lean4
93 lines
3.0 KiB
Lean4
/-
|
|
Compute Billing Protocol (HIP-0025)
|
|
|
|
Agent wallet RPC billing. Every API call costs $AI.
|
|
Pre-paid balance, per-call deduction, rate limiting.
|
|
|
|
Maps to:
|
|
- HIP-0025: Bot/Agent Wallet RPC Billing Protocol
|
|
- HIP-0096: AI Compute Contribution Rewards
|
|
- hanzo/gateway: billing middleware
|
|
- hanzo/formal/lean/Agent/Identity.lean: session budgets
|
|
|
|
Properties:
|
|
- Prepaid: balance checked before execution
|
|
- Metered: each call has a known cost
|
|
- Rate limited: max calls per second
|
|
- Accretive rewards: compute providers earn $AI
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Compute.Billing
|
|
|
|
/-- Billing account state -/
|
|
structure Account where
|
|
balance : Nat -- $AI balance (in smallest unit)
|
|
totalSpent : Nat -- lifetime spend
|
|
callsThisSecond : Nat -- rate limit counter
|
|
rateLimit : Nat -- max calls per second
|
|
|
|
/-- API call with cost -/
|
|
structure APICall where
|
|
method : String
|
|
cost : Nat -- cost in $AI
|
|
computeUnits : Nat -- compute consumed
|
|
|
|
/-- Execute a billed API call -/
|
|
def executeCall (a : Account) (c : APICall) : Option Account :=
|
|
if c.cost ≤ a.balance && a.callsThisSecond < a.rateLimit then
|
|
some { a with
|
|
balance := a.balance - c.cost
|
|
totalSpent := a.totalSpent + c.cost
|
|
callsThisSecond := a.callsThisSecond + 1 }
|
|
else none
|
|
|
|
/-- PREPAID: Insufficient balance → rejected -/
|
|
theorem insufficient_balance_rejected (a : Account) (c : APICall)
|
|
(h : c.cost > a.balance) :
|
|
executeCall a c = none := by
|
|
simp [executeCall, Nat.not_le.mpr h]
|
|
|
|
/-- RATE LIMITED: Exceeded rate → rejected -/
|
|
theorem rate_limited (a : Account) (c : APICall)
|
|
(h : a.callsThisSecond ≥ a.rateLimit) :
|
|
executeCall a c = none := by
|
|
simp [executeCall, Nat.not_lt.mpr h]
|
|
|
|
/-- BALANCE CONSERVATION: balance + totalSpent is constant -/
|
|
theorem balance_conservation (a a' : Account) (c : APICall)
|
|
(h : executeCall a c = some a') :
|
|
a'.balance + a'.totalSpent = a.balance + a.totalSpent := by
|
|
simp [executeCall] at h
|
|
obtain ⟨⟨hcost, -⟩, rfl⟩ := h
|
|
show a.balance - c.cost + (a.totalSpent + c.cost) = a.balance + a.totalSpent
|
|
omega
|
|
|
|
/-- BALANCE DECREASES: Each call reduces balance -/
|
|
theorem balance_decreases (a a' : Account) (c : APICall)
|
|
(h : executeCall a c = some a') (hc : c.cost > 0) :
|
|
a'.balance < a.balance := by
|
|
simp [executeCall] at h
|
|
obtain ⟨⟨hcost, -⟩, rfl⟩ := h
|
|
show a.balance - c.cost < a.balance
|
|
omega
|
|
|
|
/-- SPEND MONOTONE: totalSpent only increases -/
|
|
theorem spend_monotone (a a' : Account) (c : APICall)
|
|
(h : executeCall a c = some a') :
|
|
a'.totalSpent ≥ a.totalSpent := by
|
|
simp [executeCall] at h
|
|
obtain ⟨-, rfl⟩ := h
|
|
show a.totalSpent + c.cost ≥ a.totalSpent
|
|
omega
|
|
|
|
/-- FREE CALLS: Zero-cost calls don't reduce balance -/
|
|
theorem free_call_preserves (a : Account) (c : APICall)
|
|
(hc : c.cost = 0) (hr : a.callsThisSecond < a.rateLimit) :
|
|
∃ a', executeCall a c = some a' ∧ a'.balance = a.balance := by
|
|
simp [executeCall, hc, hr]
|
|
|
|
end Compute.Billing
|