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]>
74 lines
2.2 KiB
Lean4
74 lines
2.2 KiB
Lean4
/-
|
|
Gateway Auth Correctness
|
|
|
|
Models the Hanzo API gateway authentication check.
|
|
Unauthorized requests cannot access protected resources.
|
|
|
|
Maps to:
|
|
- hanzo/gateway: 147 endpoints with auth forwarding
|
|
- hanzo/iam: OAuth 2.1 / OIDC identity
|
|
|
|
Properties:
|
|
- Unauthorized ⟹ no access
|
|
- Auth check is deterministic
|
|
- Scoped access is bounded by token claims
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Gateway.Auth
|
|
|
|
/-- Auth result -/
|
|
inductive AuthResult where
|
|
| authorized (scopes : List String)
|
|
| unauthorized (reason : String)
|
|
deriving Repr
|
|
|
|
/-- A request with identity context -/
|
|
structure Request where
|
|
token : Option Nat -- OIDC token (None = anonymous)
|
|
path : String
|
|
method : String
|
|
|
|
/-- Route protection level -/
|
|
inductive Protection where
|
|
| public_ -- No auth required
|
|
| authenticated -- Any valid token
|
|
| scoped (required : List String) -- Specific scopes needed
|
|
|
|
/-- Auth check (axiomatized — real impl is in hanzo/gateway) -/
|
|
axiom verifyToken : Nat → AuthResult
|
|
|
|
/-- Check if a request is authorized for a route.
|
|
Noncomputable: `verifyToken` is axiomatized, so this has no code to run. -/
|
|
noncomputable def checkAuth (req : Request) (prot : Protection) : AuthResult :=
|
|
match prot with
|
|
| .public_ => .authorized []
|
|
| .authenticated =>
|
|
match req.token with
|
|
| none => .unauthorized "No token provided"
|
|
| some t => verifyToken t
|
|
| .scoped _ =>
|
|
match req.token with
|
|
| none => .unauthorized "No token provided"
|
|
| some t => verifyToken t
|
|
|
|
/-- Public routes always authorize -/
|
|
theorem public_always_authorized (req : Request) :
|
|
checkAuth req .public_ = .authorized [] := by
|
|
simp [checkAuth]
|
|
|
|
/-- No token ⟹ unauthorized for authenticated routes -/
|
|
theorem no_token_unauthorized (req : Request) (h : req.token = none) :
|
|
checkAuth req .authenticated = .unauthorized "No token provided" := by
|
|
simp [checkAuth, h]
|
|
|
|
/-- No token ⟹ unauthorized for scoped routes -/
|
|
theorem no_token_unauthorized_scoped (req : Request) (scopes : List String)
|
|
(h : req.token = none) :
|
|
checkAuth req (.scoped scopes) = .unauthorized "No token provided" := by
|
|
simp [checkAuth, h]
|
|
|
|
end Gateway.Auth
|