| # PAX-Coder Package Manifest | |
| Package: `pax-coder` | |
| Version: `1.0.0` | |
| Release date: 2026-08-18 | |
| Repository: `SNAPKITTYWEST/pax-coder` | |
| ## Package Identity | |
| PAX-Coder is the institutional package for proof-carrying GPU kernel generation | |
| around the PAX axiom basis, Lean 4 proof modules, CUDA/PTX implementation | |
| surfaces, Futhark functional references, and training-data export. | |
| ## Contents | |
| | Path | Package role | | |
| | --- | --- | | |
| | `README.md` | Institutional entry point | | |
| | `ABOUT.md` | Short project overview | | |
| | `LICENSE.tri` | License structure | | |
| | `VERSION` | Version marker | | |
| | `CHANGELOG.md` | Release history | | |
| | `RELEASE_NOTES.md` | Current release notes | | |
| | `PAX/` | Lean 4 proof-module surfaces | | |
| | `src/` | CUDA/PTX/Futhark source surfaces | | |
| | `backends/` | License-policy backend | | |
| | `docs/` | Institutional, user, architecture, and GTM documentation | | |
| | `demo/` | Demonstration package | | |
| | `export_training_data.py` | Training-data exporter | | |
| | `train.py` | QLoRA training script | | |
| | `run_training.sh` | Training launcher | | |
| | `Modelfile` | Ollama packaging template | | |
| | `MODEL_CARD.md` | Model-card draft | | |
| | `DATASET_CARD.md` | Dataset-card draft | | |
| | `SOVEREIGN_NODE_KEY.md` | Node-key and seal policy | | |
| | `CONTRIBUTING.md` | Contribution guidance | | |
| ## Release Gates | |
| The package may be published as an institutional repository release when: | |
| - Version files and release notes are present. | |
| - README states the PAX axiom basis and governance rules. | |
| - License text matches `LICENSE.tri`. | |
| - GitHub About metadata and topics identify the institutional scope. | |
| - Release notes do not overclaim artifact-specific runtime verification. | |
| - `python export_training_data.py` completes in the release environment. | |
| Generated kernels require additional artifact-specific gates: | |
| - Lean/Lake proof check under the declared PAX axiom basis. | |
| - CUDA/PTX compiler output for the target architecture. | |
| - Runtime comparison against a functional reference on the target hardware. | |
| - License path selection and node-key/seal policy, when production use applies. | |
| ## GitHub Topics | |
| Recommended repository topics for v1.0.0: | |
| - `pax-coder` | |
| - `formal-verification` | |
| - `lean4` | |
| - `cuda` | |
| - `ptx` | |
| - `futhark` | |
| - `gpu-kernels` | |
| - `proof-carrying-code` | |
| - `tensor-cores` | |
| - `ampere` | |
| - `deepseek-coder` | |
| - `qlora` | |
| - `sovereign-compute` | |
| - `verified-kernels` | |
| - `model-training` | |
| ## Release Artifact | |
| The GitHub release should use tag `v1.0.0`. | |
| Release assets are the automatic source archives generated by GitHub unless a | |
| separate model artifact, GGUF file, dataset export, or signed binary package is | |
| explicitly attached later. | |
| ## v1.0.0 Packaging Evidence | |
| Observed on Windows: | |
| ```text | |
| Total unique examples: 10 | |
| train: 9 examples | |
| val: 0 examples | |
| test: 1 examples | |
| ``` | |
| Generated `build/` outputs are package build products and are not part of the | |
| source release unless explicitly attached as release assets. | |