mirror of
https://github.com/hanzoai/proofs.git
synced 2026-10-30 18:23:34 +00:00
zeekayandHanzo Dev
abbe1c5aa3
Removed 31 files carrying Lux's consensus and cryptography — Consensus/, Crypto/, GPU/, Trust/, Warp/, Network/PeerDiscovery, Main — which the lakefile itself labelled "Infrastructure proofs (from Lux L1 foundation)" and "GPU acceleration proofs (from Zoo)". They were forks that had drifted. luxfi/proofs holds the maintained versions and they are consistently larger: Crypto/BLS 204 lines there against 114 here, FHE/TFHE 335 against 185, FROST 194 against 101, Consensus/Quasar 158 against 94. luxfi/proofs builds; 28 of those 31 files were the reason this one did not. Nothing in Agent/, Compute/, CRDT/, Gateway/, KMS/ or Platform/ imports them. Lux's consensus lives in luxfi/proofs. This repository proves Hanzo's: agents, compute, CRDT, gateway, KMS, platform. 19 files. Every library is now a default target, in all three proof repositories. With the attribute on one library, `lake build` compiles that library's import closure and reports success for everything else — here that was 6 of 50 files. The workflow is correspondingly a plain `lake build`, which makes the three workflows identical except for the runner label. Co-authored-by: Hanzo Dev <[email protected]>
70 lines
1.2 KiB
Lean4
70 lines
1.2 KiB
Lean4
import Lake
|
|
open Lake DSL
|
|
|
|
package hanzoFormal where
|
|
leanOptions := #[
|
|
⟨`autoImplicit, false⟩
|
|
]
|
|
|
|
-- Every library is a default target, so `lake build` builds the whole corpus.
|
|
-- With the attribute on one library, `lake build` compiles that library's
|
|
-- import closure and reports success for everything else.
|
|
|
|
@[default_target]
|
|
lean_lib Agent where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Agent.Safety,
|
|
`Agent.MCP,
|
|
`Agent.Delegation,
|
|
`Agent.Workflow,
|
|
`Agent.Identity,
|
|
`Agent.Memory
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Gateway where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Gateway.Auth,
|
|
`Gateway.RateLimit
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Platform where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Platform.Deploy,
|
|
`Platform.SBOM,
|
|
`Platform.Monitoring
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib KMS where
|
|
srcDir := "."
|
|
roots := #[
|
|
`KMS.Secrets
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Compute where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Compute.PoAI,
|
|
`Compute.ConfidentialCompute,
|
|
`Compute.Swarm,
|
|
`Compute.Billing
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib CRDT where
|
|
srcDir := "."
|
|
roots := #[
|
|
`CRDT.Privacy,
|
|
`CRDT.Commutativity,
|
|
`CRDT.Anchor
|
|
]
|
|
|
|
require mathlib from git
|
|
"https://github.com/leanprover-community/mathlib4" @ "v4.14.0"
|