SentinelOps-CI/lean-toolchain
GitHub: SentinelOps-CI/lean-toolchain
基于 Lean 4 形式化验证的密码学与数学运算库，可将经过证明的算法规格说明提取为高性能 Rust 代码。
Stars: 3 | Forks: 0
##############################################################################################
# #
# _ _____ _ _ _ #
# | | ___ __ _ _ __|_ _|__ ___ | | ___| |__ __ _(_)_ __ #
# | | / _ \/ _` | '_ \ | |/ _ \ / _ \| |/ __| '_ \ / _` | | '_ \ #
# | |__| __/ (_| | | | || | (_) | (_) | | (__| | | | (_| | | | | | #
# |_____\___|\__,_|_| |_||_|\___/ \___/|_|\___|_| |_|\__,_|_|_| |_| #
# #
# #
##############################################################################################
[](https://opensource.org/licenses/MIT)
[](https://leanprover.github.io/lean4/)
[](https://github.com/SentinelOps-CI/lean-toolchain/actions/workflows/local-ci.yml)
## 本仓库是什么
Lean Toolchain 是一个小型的、带有特定理念的库，用于教学和实验：包含你可以阅读并据此进行证明的密码学原语、感知维度的向量和矩阵，以及一条从 Lean 规格说明到 `rust/` crate 的可重现路径。它不是一个经过认证的产品，也不是已审计密码库的直接替代品；在敏感环境中依赖它之前，请参阅 [SECURITY.md](SECURITY.md)。
## 功能特性
| 领域 | 内容 |
| --- | --- |
| **密码学** | 基于 `ByteArray` 的 SHA-256 和 HMAC-SHA256，字节与十六进制辅助工具，位于 `LeanToolchain/Crypto/Tests` 的 NIST 和 RFC 4231 向量。 |
| **离散数学** | 长度索引的 `Vec`，具有 Bareiss 行列式、高斯秩、Gauss–Jordan 逆矩阵的行列 `Matrix`；位于 `Norm.lean` 中通过 mathlib 实现的实值范数（`ℝ`, `sqrt`）与算子 2-范数。 |
| **Rust 产物** | `lake exe extract` 从 `LeanToolchain/Extraction` 写入 `rust/`（模板生成，而非 Lean 项提取）。集成测试位于 `rust/tests/`。 |
| **质量标准** | 依据策略，`LeanToolchain/` 下严禁使用 `sorry`（`scripts/check_sorry.sh`）；本地 CI 会运行 Lean 和 Rust 质量门禁（详见 [docs/development/ci.md](docs/development/ci.md)）。 |
## 各组件如何协同工作
```
flowchart LR
subgraph lean [Lean 4]
Lib[LeanToolchain library]
Tests[Tests and benchmarks]
end
subgraph rust [Rust]
Gen[Generated src and Cargo.toml]
Cargo[cargo test and clippy]
end
Lib --> Tests
Lib --> Extract[lake exe extract]
Extract --> Gen
Gen --> Cargo
```
## 快速开始
**前置条件：** [Lean 4](https://leanprover.github.io/lean4/doc/quickstart.html)（在 [`lean-toolchain`](lean-toolchain) 中锁定版本），以及用于 Rust 相关工作的 [Rust stable](https://rustup.rs/)。
克隆仓库并验证默认构建与冒烟测试：
```
git clone https://github.com/SentinelOps-CI/lean-toolchain.git
cd lean-toolchain
lake build
lake test
```
重新生成 Rust 目录树并验证它（与 CI 流程保持一致）：
```
lake exe extract
cd rust
cargo test
cargo clippy --all-targets -- -D warnings
```
可选：运行 `lake exe cryptoTests`、`lake exe mathTests` 或 `lake exe benchmarks` 进行针对性测试。
## 仓库结构
```
lean-toolchain/
├── LeanToolchain/ # Crypto, Math, Extraction; Tests/; Benchmarks/
├── rust/ # Generated crate (regenerate with lake exe extract)
├── docs/ # MkDocs site source (mkdocs.yml)
├── scripts/ # e.g. check_sorry.sh and sorry_allowlist.txt
├── lakefile.lean # Lake config and mathlib require
└── lean-toolchain # Lean release pin
```
## 工具链策略
Lean 版本在 `lean-toolchain` 中锁定；根据 `lakefile.lean` 的要求，**mathlib** 必须使用与该 Lean 版本匹配的 tag 或 revision。当你升级 Lean 时，必须同步升级 mathlib 并运行 `lake update`。详情请参阅：[CONTRIBUTING.md](CONTRIBUTING.md)。
## 文档
| 文档 | 用途 |
| --- | --- |
| [docs/index.md](docs/index.md) | 导航中心及如何构建 MkDocs 站点 |
| [CONTRIBUTING.md](CONTRIBUTING.md) | 贡献指南、`sorry` 策略、PR 检查清单 |
| [docs/development/ci.md](docs/development/ci.md) | SentinelOps 与 GitHub Actions 对比，Dependabot |
| [docs/development/extraction.md](docs/development/extraction.md) | `lake exe extract` 的功能与限制 |
| [docs/api/crypto.md](docs/api/crypto.md) | 密码学 API 及 HMAC 互操作性说明 |
| [docs/api/math.md](docs/api/math.md) | 向量、矩阵、范数 |
| [docs/vector-implementation.md](docs/vector-implementation.md) | `Vec` 设计说明 |
在仓库根目录下构建静态站点（需先执行 `pip install mkdocs-material`）：
```
mkdocs build -f docs/mkdocs.yml
```
## 安全性
这是一个用于**研究与教学**的代码库。请阅读 [SECURITY.md](SECURITY.md) 以了解威胁模型、漏洞报告方式，以及 Lean 定理与生成的 Rust 代码之间的关系。
## 许可证
基于 MIT 许可证分发。详见 [LICENSE](LICENSE)。
## 致谢
[Lean 4](https://leanprover.github.io/lean4/)、[mathlib4](https://github.com/leanprover-community/mathlib4)，以及来自 [NIST](https://www.nist.gov/) 和相关 RFC 的公开测试材料。
标签：Lean 4, Rust, 代码生成, 可视化界面, 密码学库, 形式化验证, 数学运算, 渗透测试工具, 网络流量审计