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]>
73 lines
2.2 KiB
Lean4
73 lines
2.2 KiB
Lean4
/-
|
|
Rate Limiting Fairness
|
|
|
|
Token bucket rate limiting. Fair across tenants.
|
|
No single tenant can starve others.
|
|
|
|
Maps to:
|
|
- hanzo/gateway: rate limiting middleware
|
|
- hanzo/iam: tenant-level quotas
|
|
|
|
Properties:
|
|
- Fairness: each tenant gets their quota
|
|
- No starvation: below-quota requests always pass
|
|
- Burst: allows short bursts up to bucket size
|
|
- Recovery: bucket refills over time
|
|
|
|
Author: Woo Bin
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Gateway.RateLimit
|
|
|
|
structure TokenBucket where
|
|
tokens : Nat -- current tokens
|
|
capacity : Nat -- max tokens (burst size)
|
|
refillRate : Nat -- tokens per second
|
|
|
|
def tryConsume (b : TokenBucket) (cost : Nat) : Option TokenBucket :=
|
|
if cost ≤ b.tokens then some { b with tokens := b.tokens - cost }
|
|
else none
|
|
|
|
def refill (b : TokenBucket) (seconds : Nat) : TokenBucket :=
|
|
{ b with tokens := min (b.tokens + seconds * b.refillRate) b.capacity }
|
|
|
|
/-- FAIRNESS: If you have tokens, request passes -/
|
|
theorem has_tokens_passes (b : TokenBucket) (cost : Nat)
|
|
(h : cost ≤ b.tokens) :
|
|
(tryConsume b cost).isSome = true := by
|
|
simp [tryConsume, h]
|
|
|
|
/-- RATE LIMITED: No tokens → blocked -/
|
|
theorem no_tokens_blocked (b : TokenBucket) (cost : Nat)
|
|
(h : cost > b.tokens) :
|
|
tryConsume b cost = none := by
|
|
simp [tryConsume, Nat.not_le.mpr h]
|
|
|
|
/-- BURST: Bucket never exceeds capacity -/
|
|
theorem refill_capped (b : TokenBucket) (seconds : Nat) :
|
|
(refill b seconds).tokens ≤ b.capacity := by
|
|
simp [refill]
|
|
|
|
/-- RECOVERY: Refill never loses tokens, for any bucket at or under
|
|
capacity. The cap is what makes the bound need `hb`: a bucket already
|
|
over capacity would be clamped down by a refill. -/
|
|
theorem refill_increases (b : TokenBucket) (seconds : Nat)
|
|
(hb : b.tokens ≤ b.capacity) :
|
|
(refill b seconds).tokens ≥ b.tokens := by
|
|
simp only [refill]
|
|
exact le_min (Nat.le_add_right _ _) hb
|
|
|
|
/-- CONSUMPTION DECREASES: Using tokens reduces count -/
|
|
theorem consume_decreases (b b' : TokenBucket) (cost : Nat)
|
|
(h : tryConsume b cost = some b') (hc : cost > 0) :
|
|
b'.tokens < b.tokens := by
|
|
simp [tryConsume] at h
|
|
obtain ⟨hcost, rfl⟩ := h
|
|
show b.tokens - cost < b.tokens
|
|
omega
|
|
|
|
end Gateway.RateLimit
|