| # About PAX-Coder | |
| ## What PAX-Coder Does | |
| PAX-Coder is a fine-tuned AI model (based on DeepSeek-Coder-7B) that generates GPU kernels paired with formal proofs. You ask it to write a kernel, and it gives you: | |
| 1. **Lean 4 proof** — A mathematical proof that your kernel is correct | |
| 2. **PTX assembly** — The actual GPU code that runs on NVIDIA sm_86 hardware (RTX 3080, RTX 4090) | |
| 3. **Futhark reference** — A high-level functional specification to verify against | |
| 4. **PAX certificate** — Which safety guarantees this kernel provides | |
| ## For Whom | |
| - **GPU engineers** who want to ship kernels with formal guarantees | |
| - **CUDA developers** who want to skip manual proof-writing | |
| - **Research labs** building verified AI infrastructure | |
| - **Companies** shipping safety-critical ML models where "trust me bro" is not acceptable | |
| ## What Makes It Different | |
| Most GPU kernel generators output code you hope is correct. PAX-Coder outputs code + a machine-checked proof that it IS correct. The proof can be read by any Lean 4 compiler and verified independently—no human judgment required. | |
| ## Key Topics | |
| ### 🎯 Getting Started | |
| - **No prerequisites needed** — Read [User Guide](#user-guide) in the README | |
| - **30 seconds**: Run via Ollama (pre-installed model) | |
| - **3 minutes**: Run via Python (HuggingFace transformers) | |
| - **30 minutes**: Train your own version locally | |
| ### 🔧 What You Can Ask For | |
| - IEEE-754 floating-point proofs (rounding error bounds) | |
| - GEMM kernels (matrix multiply) | |
| - Async copy pipelines (3-stage, double-buffer) | |
| - Epilogue fusion (Bias+GeLU, Residual+GeLU) | |
| - Warp reductions (shfl.sync) | |
| - Architecture mappings (axioms → proof obligations) | |
| ### 📋 What You Get | |
| Every output includes: | |
| - **Lean 4**: Machine-checked theorem (zero `sorry` placeholders) | |
| - **PTX**: sm_86 assembly for RTX 3080 / RTX 4090 | |
| - **Futhark**: Functional spec (compiler-verified semantics) | |
| - **Certificate**: Which of 8 proof obligations this satisfies | |
| ### 🏗️ The Five Axioms (Math Foundation) | |
| 1. **Index Space Primacy** — Each thread owns one element; proven partition | |
| 2. **Permission Necessity** — Every memory access has a fractional permission; sum ≤ 1 | |
| 3. **Synchronization as State** — Barriers are happens-before edges | |
| 4. **Warp Distinctness** — SIMT reconvergence proven before barriers | |
| 5. **Verification Non-Negotiability** — No kernel ships without proof | |
| These map to 8 proof obligations (PO1–PO8) that codify GPU safety. | |
| ### 🎓 Training | |
| You can train your own version: | |
| ```bash | |
| python3 export_training_data.py # Extract proofs + code | |
| ./run_training.sh # QLoRA fine-tune (4-6h on RTX 3080) | |
| ollama create pax-coder -f Modelfile | |
| ``` | |
| ### 📜 License | |
| Tri-licensed (BSL-1.1, AGPL-3.0, MPL-2.0). Use the Prolog reasoner to determine which license applies to your use case. | |
| ### 🔑 Sovereign Node Key | |
| Production use requires a Sovereign Node Key — proof you've contributed to the stack. Not DRM; community membership. See [`SOVEREIGN_NODE_KEY.md`](SOVEREIGN_NODE_KEY.md). | |
| ## The Repository | |
| | Folder | Purpose | | |
| |--------|---------| | |
| | `PAX/` | Lean 4 formal proofs (ConstraintDAG, PipelineDAG, Float16_Rounding, WMMA, IR_DAG) | | |
| | `src/` | GPU kernel templates (PTX + Futhark specs) | | |
| | `backends/` | License policy reasoner (Prolog) | | |
| | `docs/` | Documentation (architecture, user guide, GTM) | | |
| | `demo/` | Interactive examples | | |
| ## Key Files | |
| - **[README.md](README.md)** — This document + quickstart + user guide | |
| - **[USER_GUIDE.md](docs/USER_GUIDE.md)** — Step-by-step usage examples | |
| - **[PAX_ARCHITECTURE.md](docs/PAX_ARCHITECTURE.md)** — 5 axioms → 8 proof obligations | |
| - **[PAX_CODER_README.md](PAX_CODER_README.md)** — Commercial integration (GGUF, CUDA, PTX, GEMM bridge) | |
| - **[SOVEREIGN_NODE_KEY.md](SOVEREIGN_NODE_KEY.md)** — How to get a node key | |
| - **[LICENSE.tri](LICENSE.tri)** — Full tri-license text | |
| ## Hardware Support | |
| | GPU | Architecture | Status | | |
| |-----|--------------|--------| | |
| | RTX 3080 | Ampere (sm_86) | Primary target ✅ | | |
| | RTX 4090 | Ada (sm_90) | Secondary (TMA support planned) | | |
| ## Quick Links | |
| - **Use it now**: [User Guide](#user-guide) in README | |
| - **Examples**: `demo/` folder | |
| - **Architecture details**: [PAX_ARCHITECTURE.md](docs/PAX_ARCHITECTURE.md) | |
| - **Commercial integration**: [PAX_CODER_README.md](PAX_CODER_README.md) | |
| - **Contribute**: [CONTRIBUTING.md](CONTRIBUTING.md) | |
| --- | |
| **TL;DR**: Write English prose asking for a GPU kernel. PAX-Coder generates proof + code. Ship with confidence. | |