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]>
149 lines
5.2 KiB
Lean4
149 lines
5.2 KiB
Lean4
/-
|
||
KMS Secret Access Model
|
||
|
||
Secrets are the root of trust. Build signing keys, attestation
|
||
credentials, and validator keys all come from KMS.
|
||
|
||
Maps to:
|
||
- hanzo/kms: secrets management with AI access control
|
||
- hanzo/kms-operator: K8s secret sync (KMSSecret CRDs)
|
||
- lux/kms: MPC-backed validator key management
|
||
|
||
Properties:
|
||
- Access requires authentication + authorization
|
||
- Secret access is audited (every read logged)
|
||
- Rotation preserves availability
|
||
- AI agents require explicit per-secret approval
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Data.List.Basic
|
||
import Mathlib.Tactic
|
||
|
||
namespace KMS.Secrets
|
||
|
||
/-- Secret classification -/
|
||
inductive Classification where
|
||
| signing -- Build attestation signing keys
|
||
| validator -- Blockchain validator keys
|
||
| api -- API keys and tokens
|
||
| encryption -- Data encryption keys
|
||
| certificate -- TLS certificates
|
||
deriving DecidableEq, Repr
|
||
|
||
/-- Access policy for a secret -/
|
||
structure AccessPolicy where
|
||
requiredRole : Nat -- minimum IAM role level
|
||
aiApproval : Bool -- requires human approval for AI access
|
||
rotationDays : Nat -- auto-rotation interval
|
||
auditRequired : Bool -- must log every access
|
||
deriving Repr
|
||
|
||
/-- Secret metadata (not the value itself!) -/
|
||
structure SecretMeta where
|
||
id : Nat
|
||
classification : Classification
|
||
policy : AccessPolicy
|
||
version : Nat -- increments on rotation
|
||
deriving Repr
|
||
|
||
/-- Access request -/
|
||
structure AccessRequest where
|
||
requester : Nat -- identity
|
||
roleLevel : Nat -- their IAM role level
|
||
isAI : Bool -- is this an AI agent?
|
||
humanApproved : Bool -- has a human approved this access?
|
||
secret : SecretMeta
|
||
|
||
/-- Access check -/
|
||
def isAccessAllowed (req : AccessRequest) : Bool :=
|
||
req.roleLevel ≥ req.secret.policy.requiredRole &&
|
||
(!req.isAI || !req.secret.policy.aiApproval || req.humanApproved)
|
||
|
||
/-- Insufficient role → denied -/
|
||
theorem insufficient_role_denied (req : AccessRequest)
|
||
(h : req.roleLevel < req.secret.policy.requiredRole) :
|
||
isAccessAllowed req = false := by
|
||
simp [isAccessAllowed, Nat.not_le.mpr h]
|
||
|
||
/-- AI without human approval → denied (when policy requires it) -/
|
||
theorem ai_needs_approval (req : AccessRequest)
|
||
(h_ai : req.isAI = true)
|
||
(h_policy : req.secret.policy.aiApproval = true)
|
||
(h_no_approval : req.humanApproved = false) :
|
||
isAccessAllowed req = false := by
|
||
simp [isAccessAllowed, h_ai, h_policy, h_no_approval]
|
||
|
||
/-- Human access doesn't need AI approval flag -/
|
||
theorem human_no_ai_check (req : AccessRequest)
|
||
(h_human : req.isAI = false)
|
||
(h_role : req.roleLevel ≥ req.secret.policy.requiredRole) :
|
||
isAccessAllowed req = true := by
|
||
simp [isAccessAllowed, h_human, h_role]
|
||
|
||
/-- AI with approval and sufficient role → allowed -/
|
||
theorem ai_with_approval (req : AccessRequest)
|
||
(h_ai : req.isAI = true)
|
||
(h_approved : req.humanApproved = true)
|
||
(h_role : req.roleLevel ≥ req.secret.policy.requiredRole) :
|
||
isAccessAllowed req = true := by
|
||
simp [isAccessAllowed, h_ai, h_approved, h_role]
|
||
|
||
/-- Rotation increments version -/
|
||
def rotate (s : SecretMeta) : SecretMeta :=
|
||
{ s with version := s.version + 1 }
|
||
|
||
/-- Rotation preserves classification -/
|
||
theorem rotation_preserves_class (s : SecretMeta) :
|
||
(rotate s).classification = s.classification := rfl
|
||
|
||
/-- Rotation preserves policy -/
|
||
theorem rotation_preserves_policy (s : SecretMeta) :
|
||
(rotate s).policy = s.policy := rfl
|
||
|
||
/-- Version strictly increases on rotation -/
|
||
theorem rotation_version_increases (s : SecretMeta) :
|
||
(rotate s).version > s.version := by
|
||
simp [rotate]
|
||
|
||
/-- KEY HIERARCHY: Master key → derived keys.
|
||
Compromising a derived key doesn't compromise the master. -/
|
||
structure KeyHierarchy where
|
||
masterKeyId : Nat
|
||
derivedKeys : List Nat
|
||
derivationPath : Nat → String
|
||
|
||
/-- Whether a key has been exported outside the HSM boundary -/
|
||
axiom exported : Nat → Prop
|
||
|
||
/-- HSM BACKING: Hardware security modules for master keys.
|
||
Master key never leaves the HSM boundary. -/
|
||
axiom hsm_boundary :
|
||
∀ (h : KeyHierarchy), ¬ exported h.masterKeyId
|
||
|
||
/-- DERIVED KEY ISOLATION: a leaked derived key does not breach the
|
||
master. Confinement of the master is an HSM property and takes no
|
||
argument from the state of any derived key — which is what the
|
||
unused hypotheses record. -/
|
||
theorem derived_key_isolation (h : KeyHierarchy) (k : Nat)
|
||
(_derived : k ∈ h.derivedKeys) (_leaked : exported k) :
|
||
¬ exported h.masterKeyId := hsm_boundary h
|
||
|
||
/-- ZERO TRUST: Every access is authenticated + authorized + logged.
|
||
No implicit trust based on network position. -/
|
||
def zeroTrustCheck (req : AccessRequest) : Bool :=
|
||
isAccessAllowed req -- same check regardless of network origin
|
||
|
||
theorem zero_trust_applies (req : AccessRequest) :
|
||
zeroTrustCheck req = isAccessAllowed req := rfl
|
||
|
||
/-- AUDIT COMPLETENESS: Every access attempt is logged,
|
||
including denied attempts. -/
|
||
theorem audit_all_attempts (req : AccessRequest) :
|
||
-- Both allowed and denied attempts produce an audit entry
|
||
-- (the function always returns a Bool, never throws)
|
||
isAccessAllowed req = true ∨ isAccessAllowed req = false := by
|
||
cases isAccessAllowed req <;> simp
|
||
|
||
end KMS.Secrets
|