File size: 2,978 Bytes
ef6eb55 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 | # 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.
|