Verified crypto and discrete linear algebra in Lean 4, with mathlib-backed real norms where needed, and a maintained Rust surface produced by a template generator and checked against the same vectors as the Lean test suite.
Lean Toolchain is a small, opinionated library for teaching and experimentation: cryptographic primitives you can read and prove against, dimension-aware vectors and matrices, and a reproducible path from Lean specifications to a rust/ crate. It is not a certified product or a drop-in replacement for audited cryptography libraries; see SECURITY.md before relying on it in sensitive contexts.
| Area | Contents |
|---|---|
| Cryptography | SHA-256 and HMAC-SHA256 on ByteArray, byte and hex helpers, NIST and RFC 4231 vectors in LeanToolchain/Crypto/Tests. |
| Discrete math | Length-indexed Vec, row–column Matrix, structural lemmas; real-valued norms (ℝ, sqrt) in Norm.lean via mathlib. |
| Rust artifacts | lake exe extract writes rust/ from LeanToolchain/Extraction (template emission, not Lean term extraction). Integration tests live in rust/tests/. |
| Quality bar | No sorry under LeanToolchain/ by policy (scripts/check_sorry.sh); local CI runs Lean and Rust gates (see 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
Prerequisites: Lean 4 (pin in lean-toolchain) and, for Rust work, Rust stable.
Clone and verify the default build and smoke tests:
git clone https://github.com/SentinelOps-CI/lean-toolchain.git
cd lean-toolchain
lake build
lake testRegenerate the Rust tree and validate it (mirrors CI):
lake exe extract
cd rust
cargo test
cargo clippy --all-targets -- -D warningsOptional: lake exe cryptoTests, lake exe mathTests, or lake exe benchmarks for focused runs.
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 is pinned in lean-toolchain; mathlib is required from lakefile.lean on a tag or revision that matches that Lean version. When you bump Lean, bump mathlib in lockstep and run lake update. Details: CONTRIBUTING.md.
| Document | Purpose |
|---|---|
| docs/index.md | Hub and how to build the MkDocs site |
| CONTRIBUTING.md | Contributions, sorry policy, PR checklist |
| docs/development/ci.md | SentinelOps vs GitHub Actions, Dependabot |
| docs/development/extraction.md | What lake exe extract does and does not do |
| docs/api/crypto.md | Crypto API and HMAC interoperability notes |
| docs/api/math.md | Vectors, matrices, norms |
| docs/vector-implementation.md | Vec design notes |
Build the static site from the repository root (after pip install mkdocs-material):
mkdocs build -f docs/mkdocs.ymlThis is a research and teaching codebase. Read SECURITY.md for threat model, reporting, and how Lean theorems relate to generated Rust.
Distributed under the MIT License. See LICENSE.
Lean 4, mathlib4, and public test material from NIST and relevant RFCs.