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
/-
|
|
SBOM (Software Bill of Materials) Generation Correctness
|
|
|
|
Every deployed artifact has an SBOM listing all dependencies,
|
|
contributors, and attestations. Extends CycloneDX/SPDX with
|
|
role-aware contribution tracking.
|
|
|
|
Maps to:
|
|
- hanzo/platform: deployment with SBOM
|
|
- hanzo/attest: attestation generation
|
|
- zoo/formal/lean/Governance/Contribution.lean: SBOM+ model
|
|
|
|
Properties:
|
|
- Completeness: all transitive deps are included
|
|
- Accuracy: dep versions match actual build inputs
|
|
- Attestation: every dep has a content hash
|
|
- No phantom deps: only actually-used deps are listed
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace Platform.SBOM
|
|
|
|
/-- A dependency entry -/
|
|
structure DepEntry where
|
|
name : String
|
|
version : String
|
|
hash : Nat -- content hash of the dependency
|
|
attested : Bool -- has build attestation
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- SBOM document -/
|
|
structure SBOMDoc where
|
|
artifact : Nat -- hash of the built artifact
|
|
deps : List DepEntry
|
|
contributors : List Nat -- contributor public keys
|
|
buildTime : Nat
|
|
deriving Repr
|
|
|
|
/-- All deps are attested -/
|
|
def fullyAttested (s : SBOMDoc) : Bool :=
|
|
s.deps.all (·.attested)
|
|
|
|
/-- Dep count -/
|
|
def depCount (s : SBOMDoc) : Nat := s.deps.length
|
|
|
|
/-- Contributor count -/
|
|
def contributorCount (s : SBOMDoc) : Nat := s.contributors.length
|
|
|
|
/-- Empty SBOM is trivially attested -/
|
|
theorem empty_attested : fullyAttested ⟨0, [], [], 0⟩ = true := rfl
|
|
|
|
/-- Unattested dep breaks full attestation -/
|
|
theorem unattested_breaks (s : SBOMDoc) (d : DepEntry)
|
|
(h_mem : d ∈ s.deps) (h_bad : d.attested = false) :
|
|
fullyAttested s = false := by
|
|
simp [fullyAttested, List.all_eq_true]
|
|
exact ⟨d, h_mem, by simp [h_bad]⟩
|
|
|
|
/-- Adding an attested dep preserves full attestation -/
|
|
theorem add_attested_preserves (s : SBOMDoc) (d : DepEntry)
|
|
(h_full : fullyAttested s = true) (h_att : d.attested = true) :
|
|
fullyAttested { s with deps := d :: s.deps } = true := by
|
|
simp only [fullyAttested, List.all_eq_true] at h_full ⊢
|
|
intro x hx
|
|
rcases List.mem_cons.mp hx with rfl | hx'
|
|
· exact h_att
|
|
· exact h_full x hx'
|
|
|
|
/-- Dep count is monotone under addition -/
|
|
theorem add_dep_increases (s : SBOMDoc) (d : DepEntry) :
|
|
depCount { s with deps := d :: s.deps } = depCount s + 1 := by
|
|
simp [depCount, List.length_cons]
|
|
|
|
/-- All contributors are listed -/
|
|
def hasContributor (s : SBOMDoc) (pk : Nat) : Bool :=
|
|
s.contributors.contains pk
|
|
|
|
/-- SBOM with no deps has zero dep count -/
|
|
theorem no_deps_zero : depCount ⟨0, [], [], 0⟩ = 0 := rfl
|
|
|
|
end Platform.SBOM
|