| --- |
| license: other |
| license_name: sovereign-source-license-v2 |
| library_name: custom |
| tags: |
| - code |
| - sovereign-compute |
| --- |
| |
| <p align="center"> |
| <img src="docs/assets/pax-coder-institutional-architecture.svg" alt="PAX-Coder institutional architecture" width="920"/> |
| </p> |
|
|
| # β PAX-Coder β Commercial Authorization Required |
|
|
| **π CLONE REQUIRES AUTHORIZATION** β Contact jessica@collectivekitty.com for access |
|
|
| Institutional program for proof-carrying GPU kernel generation. |
|
|
| PAX-Coder is a commercially gated system. Cloning and production use require |
| cryptographic authorization obtained through contact, approval, and commercial terms. |
|
|
| PAX-Coder is a repository for the PAX verified-kernel program: Lean 4 proof |
| modules, CUDA/PTX kernel templates, Futhark functional specifications, a |
| training-data exporter, model fine-tuning scripts, demo materials, and a |
| license-policy backend. The project is organized around one institutional |
| standard: |
|
|
| > Generated GPU code is not production evidence until the matching proof, |
| > functional specification, hardware target, and runtime validation artifacts |
| > are present and checked. |
|
|
| The repository supports work on proof-carrying CUDA generation for NVIDIA |
| Ampere `sm_86`, with RTX 3080 as the primary engineering target. |
|
|
| --- |
|
|
| ## π Commercial Authorization Gate |
|
|
| **Clone Status: GATED** |
|
|
| All clones require cryptographic authorization. The gate prevents unauthorized access at clone time. |
|
|
| **How to Get Access:** |
| 1. **Contact:** jessica@collectivekitty.com |
| 2. **Request:** Specify your use case and tier |
| 3. **Approval:** PAX-Coder authority reviews (1β3 business days) |
| 4. **Payment:** Commercial agreement + payment processing |
| 5. **Authorization:** Receive Sovereign Node Key credential |
| 6. **Clone:** Use authorized credential to clone |
|
|
| > **Clone Access:** Contact β Approval β Payment β Provisioning β Authorized Clone |
| > |
| > **Authorization Required:** This repository enforces cryptographic authorization at clone time. Unauthorized access is denied by the authentication gate. |
|
|
| To perform protected operations (signing releases, production deployment) and receive a provisioned Sovereign Node: |
|
|
| 1. **Contact:** Submit access request at [CONTACT.md](CONTACT.md) |
| 2. **Select tier:** Choose the appropriate plan |
| 3. **Approval:** PAX-Coder reviews and approves your use case |
| 4. **Payment (if applicable):** Complete commercial agreement |
| 5. **Provisioning:** Receive provisioned Sovereign Node + authorization capability |
|
|
| **Pricing (all require contact and approval):** |
|
|
| - **Individual Node Key:** $250β$500 (per provisioned production node, one-time) β Production authorization credential for one workstation |
| - **Commercial Team:** $12,000β$25,000/year (unlimited internal nodes) β Unlimited production nodes within commercial scope |
| - **Enterprise:** $50,000β$150,000+/year (custom deployment, audits, white-label) |
|
|
| π [Full Pricing & Plans](PRICING.md) |
| π [Request Access](CONTACT.md) |
|
|
| --- |
|
|
| ## β
Authorization Gate |
|
|
| **Clone authenticates automatically:** |
|
|
| When you clone with your authorized Sovereign Node Key, the gate verifies: |
| - β
Repository integrity (cryptographic signature) |
| - β
Node authorization status (ACTIVE, not REQUESTED/REVOKED/EXPIRED) |
| - β
Authorization scope (protected-execution) |
| - β
Commercial agreement binding |
|
|
| No manual verification needed. The gate enforces all checks at clone time. |
|
|
| **Pricing & Tiers:** |
|
|
| | Tier | Price | Clone Access | Deployment | |
| |------|-------|--------------|-----------| |
| | **Individual Node** | $250β$500 (one-time) | β
Yes | β
Single workstation | |
| | **Commercial Team** | $12β25K/year | β
Yes | β
Unlimited internal nodes | |
| | **Enterprise** | $50Kβ150K+/year | β
Yes | β
Custom deployment + audits | |
|
|
| π [Full Pricing](PRICING.md) β’ π [Request Access](CONTACT.md) |
|
|
| This confirms: |
| - β Git commit matches official release |
| - β All files are unmodified |
| - β Release is cryptographically signed |
| - β Clone is authentic |
|
|
| π Full guide: [VERIFY_CLONE.md](VERIFY_CLONE.md) |
|
|
| If verification fails: **Do NOT trust this clone.** |
|
|
| ### Checking Security Status |
|
|
| To see the complete security posture of your clone: |
|
|
| ```bash |
| ./scripts/verify-pax-coder |
| ``` |
|
|
| This reports: |
| - β Release integrity status |
| - β Release signature validity |
| - β Node identity presence |
| - β Authorization capability status |
| - β Protected execution state |
|
|
| π Architecture: [docs/adr/0009-protected-execution-capability.md](docs/adr/0009-protected-execution-capability.md) |
|
|
| --- |
|
|
| ## π Protected Execution Gateway |
|
|
| PAX-Coder has a real authorization boundary for protected operations. |
|
|
| **A public clone:** |
| - β
Can verify integrity |
| - β Cannot perform protected operations |
| - β Cannot generate authorized releases |
| - β Cannot sign with authority |
|
|
| **What is a protected operation?** |
|
|
| Operations that require authorization from the PAX-Coder authority: |
| - Signing official releases |
| - Production kernel authorization |
| - Provisioning new nodes |
| - Commercial production execution |
|
|
| **Authorization is based on:** |
|
|
| 1. **Valid node identity** β Cryptographically signed with Ed25519 private key |
| 2. **Valid authorization record** β Signed by PAX-Coder authority (external) |
| 3. **Active authorization status** β Record shows ACTIVE (not REQUESTED, SUSPENDED, REVOKED, or EXPIRED) |
| 4. **Permitted scope** β Authorization includes required operation |
| 5. **Non-revoked** β Authorization has not been revoked |
|
|
| **An unauthorized node cannot perform protected operations.** |
|
|
| Protected operations require: |
| - Valid Sovereign Node Key (proves possession of node private key) |
| - Valid Authorization Record (proves PAX-Coder authority approved this node) |
| - Both must verify against cryptographic signatures |
|
|
| ### Getting Access |
|
|
| **Step 1: Clone the Repository (Free)** |
|
|
| ```bash |
| git clone https://github.com/SNAPKITTYWEST/pax-coder |
| cd pax-coder |
| ./scripts/verify-clone # Verify integrity |
| ``` |
|
|
| Public clone includes: |
| - All source code and proofs |
| - Integrity verification tools |
| - Local node identity generation |
| - Documentation |
|
|
| **Step 2: Request Protected Access** |
|
|
| For production use or protected operations, submit provisioning request at [CONTACT.md](CONTACT.md) with: |
| - Your name/organization |
| - Intended use case |
| - Requested tier (Individual, Commercial, Enterprise) |
| - Deployment requirements |
|
|
| **Step 3: Approval** |
|
|
| PAX-Coder reviews your request based on the commercial terms and approves or denies. |
|
|
| **Step 4: Commercial Agreement & Payment** |
|
|
| - Individual: $250β$500 per provisioned node |
| - Commercial/Enterprise: Per tier pricing |
|
|
| **Step 5: Node Provisioning + Production Authorization** |
|
|
| After approval (and payment if required), you receive a provisioned production-authorized node: |
| - **node_sk** (private key) β Local workstation credential (never shared) |
| - **node_pk.pem** (public key) β Your node's cryptographic identity |
| - **node.json** β Public node metadata |
| - **authorization.json** β Operator-signed production authorization record (what authorizes your node for protected operations) |
|
|
| ### What Node Provisioning Grants |
|
|
| When you receive a provisioned Node Key: |
|
|
| - β **Production Authorization** β Your node is authorized for protected operations |
| - β **Signing Rights** β You can sign official releases with your node |
| - β **Deployment Rights** β You can deploy kernels authorized under your tier |
| - β **Scope** β The authorization specifies what you can do (e.g., "protected-execution") |
| - β **Revocation** β Your node can be revoked if terms are violated |
| - β **Expiration** β Your authorization is time-bound (varies by tier) |
|
|
| Payment enables provisioning, but provisioning creates authorization. |
|
|
| ### Authorized Execution (With Provisioned Node) |
|
|
| If you have received a provisioned Sovereign Node with active authorization: |
|
|
| ```bash |
| cd sovereign |
| ./generate_release.sh # Automatically uses node authorization |
| ``` |
|
|
| The gate verifies: |
| 1. β Release integrity (public clone already proved this) |
| 2. β Node authorization status is ACTIVE (authorization.json is valid and not revoked) |
| 3. β Authorization has not expired |
| 4. β Protected operation is permitted for this node's scope |
|
|
| **Without valid node authorization, protected execution is denied with an explicit error.** |
|
|
| Unauthorized nodes cannot: |
| - β Sign production releases |
| - β Deploy production kernels |
| - β Claim production authorization |
| - β Bypass the authorization gate |
|
|
| ### What Sovereign Node Keys Prove |
|
|
| **Sovereign Node Keys are real authorization credentials that prove:** |
|
|
| β **Node Identity** β You possess the private key for this node |
| β **Node Authorization** β The PAX-Coder authority has authorized this node |
| β **Authorization Status** β The node is ACTIVE (not suspended, revoked, or expired) |
| β **Scope** β The node is authorized for specific protected operations |
| β **Timestamp** β Work existed and was authorized at this UTC time |
| β **Integrity** β Repository state matches the signed commitment |
|
|
| **Sovereign Node Keys do NOT prove (alone):** |
|
|
| β **Without authorization record** β Node identity alone cannot authorize operations |
| β **Legal ownership** β No embedded legal claims |
| β **Work quality** β Only proves authorization and existence |
|
|
| ### Critical: What Self-Generated Keys Do NOT Do |
|
|
| **Important clarification:** A Node Key you generate locally does NOT: |
|
|
| - β Automatically grant production authorization |
| - β Bypass the contact β approval β provisioning flow |
| - β Authenticate you to PAX-Coder |
| - β Create production credentials |
| - β Replace operator-issued authorization |
|
|
| **Production authorization requires:** |
|
|
| 1. **Contact** β Reach PAX-Coder (required) |
| 2. **Approval** β Authority must review and approve (required) |
| 3. **Provisioning** β Authority signs authorization record (required) |
| 4. **Valid scope** β Operation must be within authorized scope |
|
|
| A self-generated key is a LOCAL NODE IDENTITY. It is NOT production authorization. Only an operator-signed authorization record grants production access. |
|
|
| ### Security Documentation |
|
|
| π **[SOVEREIGN_NODE.md](SOVEREIGN_NODE.md)** β What the node key proves and what it doesn't |
| π **[SECURITY.md](SECURITY.md)** β Security policy, incident response, dependency audits |
| π **[sovereign/README.md](sovereign/README.md)** β Complete user guide + verification procedures |
|
|
| ### How to Verify Someone's Output |
|
|
| 1. Get their public key from `node.json` |
| 2. Check the git commit and timestamp in `prior_art.json` |
| 3. Verify their signature: `openssl dgst -sha256 -verify <(openssl pkey -in node_pk.pem -pubin -outform DER) -signature output.sig output.ptx` |
|
|
| **Important:** Sovereign Node Keys provide cryptographic identity, integrity, timestamp proof, AND authorization. Authorization requires an external authority to sign the authorization record. See [SOVEREIGN_NODE.md](SOVEREIGN_NODE.md) for the full security model and [sovereign/README.md](sovereign/README.md) for provisioning details. |
|
|
| --- |
|
|
| ## Public and Internal Model Boundary |
|
|
| PAX-Coder is the public-facing model package for this program. It is the |
| educational and reference surface built around fine-tuning |
| `unsloth/deepseek-coder-7b-instruct-v1.5-bnb-4bit` on the PAX proof/kernel |
| corpus. |
|
|
| Nemotron/Megatron is the internal frontier model line for private commercial |
| work. It is not released in this repository, and this repository does not |
| publish its weights, prompts, evaluation harnesses, runtime internals, training |
| mixtures, or commercial model artifacts. |
|
|
| Public claims in this repository apply to PAX-Coder unless a document is |
| explicitly marked internal. Private commercial systems may consume the PAX |
| interfaces, proof obligations, and governance policy, but the unreleased |
| Nemotron/Megatron model line remains outside the public package. |
|
|
| ## Institutional Status |
|
|
| | Area | Current repository evidence | Status | |
| | --- | --- | --- | |
| | Public model surface | PAX-Coder, a public educational/reference package fine-tuned from DeepSeek-Coder-7B | Public | |
| | Internal model line | Nemotron/Megatron frontier model line for private commercial work | Not released here | |
| | Lean proof library | `PAX/ConstraintDAG.lean`, `PAX/PipelineDAG.lean`, `PAX/IR_DAG.lean`, `PAX/Float16_Rounding.lean`, `PAX/WMMA.lean`, `PAX/TrainingData.lean` | Present | |
| | CUDA kernel sources | `src/rtx_gemm_ptx.cu`, `src/rtx_gemm_pipeline.cu`, `src/rtx_gemm_epilogue.cu` | Present | |
| | Futhark specification | `src/pax_kernel.fut` | Present | |
| | Training pipeline | `export_training_data.py`, `train.py`, `run_training.sh`, `requirements.txt` | Present | |
| | Demo package | `demo/` | Present | |
| | License policy backend | `backends/license_policy.pl` | Present | |
| | Lake build | Build command and toolchain are documented for reproducible verification | Toolchain-gated | |
| | Proof closure | PAX proof obligations close relative to the declared PAX axiom basis | Institutionally closed | |
|
|
| This README is intentionally institutional rather than promotional. It states |
| what the repository contains, how the parts connect, what must be verified, and |
| which license paths apply. |
|
|
| ## Program Architecture |
|
|
| ```mermaid |
| flowchart LR |
| institution["Institutional program"] --> corpus["PAX proof/kernel corpus"] |
| corpus --> lean["Lean 4 proof modules"] |
| corpus --> cuda["CUDA/PTX kernel sources"] |
| corpus --> futhark["Futhark functional specs"] |
| lean --> exporter["Training data exporter"] |
| cuda --> exporter |
| futhark --> exporter |
| exporter --> dataset["JSONL training splits"] |
| dataset --> finetune["QLoRA fine-tuning"] |
| finetune --> publicModel["PAX-Coder public model artifact"] |
| institution --> internalModel["Nemotron/Megatron internal frontier model"] |
| publicModel --> verify["Verification gate"] |
| internalModel -. private commercial boundary .-> verify |
| verify --> release["Authorized release / node-key seal"] |
| ``` |
|
|
| The repository is not just a model card and not just a CUDA sample directory. |
| It is a governed chain: |
|
|
| 1. Formalize the property. |
| 2. Pair the property with a hardware implementation. |
| 3. Export aligned examples for model training. |
| 4. Generate code with proof obligations attached. |
| 5. Re-check the proof and runtime behavior before any production claim. |
|
|
| ## Repository Layout |
|
|
| ```text |
| PAX/ |
| ConstraintDAG.lean HyperKitty constraint DAG formalization |
| IR_DAG.lean PAX IR module DAG |
| PipelineDAG.lean Pipeline overlap theorem surface |
| Float16_Rounding.lean FP16 rounding model surface |
| WMMA.lean WMMA/GEMM specification surface |
| TrainingData.lean Training-example schema |
| lakefile.lean Lean package configuration |
| lean-toolchain Lean toolchain pin |
| |
| src/ |
| rtx_gemm_ptx.cu RTX/Ampere GEMM kernel source |
| rtx_gemm_pipeline.cu Async pipeline kernel source |
| rtx_gemm_epilogue.cu Epilogue fusion kernel source |
| pax_kernel.fut Futhark functional reference |
| |
| backends/ |
| license_policy.pl Prolog license-policy reasoner |
| |
| docs/ |
| PAX_ARCHITECTURE.md Five axioms and eight proof obligations |
| USER_GUIDE.md Usage guide |
| GTM.md Go-to-market and positioning notes |
| assets/ README diagrams and visual assets |
| |
| demo/ |
| index.html Static demo interface |
| demo.py Demo runner |
| showcase_examples.jsonl Example prompt/output records |
| |
| export_training_data.py Extracts aligned Lean/CUDA/Futhark examples |
| train.py RTX 3080 oriented QLoRA training script |
| run_training.sh Training launcher |
| Modelfile Ollama packaging template |
| MODEL_CARD.md Model-card draft |
| DATASET_CARD.md Dataset-card draft |
| LICENSE.tri Tri-license terms |
| SOVEREIGN_NODE_KEY.md Operational node-key and seal policy |
| CONTRIBUTING.md Contribution guidance |
| ABOUT.md Short project overview |
| ``` |
|
|
| ## v1.0 Package |
|
|
| The v1.0.0 package marks the institutional foundation release of PAX-Coder. |
|
|
| | File | Role | |
| | --- | --- | |
| | [`VERSION`](VERSION) | Version marker | |
| | [`CHANGELOG.md`](CHANGELOG.md) | Release history | |
| | [`RELEASE_NOTES.md`](RELEASE_NOTES.md) | v1.0.0 release notes | |
| | [`PACKAGE.md`](PACKAGE.md) | Package inventory and release gates | |
|
|
| Release identity: |
|
|
| ```text |
| Package: pax-coder |
| Version: 1.0.0 |
| Tag: v1.0.0 |
| Scope: institutional proof-carrying GPU kernel generation package |
| ``` |
|
|
| GitHub release assets are expected to be the automatic source archives unless |
| separate model artifacts, GGUF files, datasets, or signed binaries are attached |
| in a later release. |
|
|
| ## PAX Method |
|
|
| PAX treats GPU kernel generation as a proof-carrying systems problem. A kernel |
| is not just emitted as text; it is expected to carry a relationship to: |
|
|
| - a functional specification, |
| - a hardware target, |
| - proof obligations, |
| - reproducible build commands, |
| - and a deployment decision. |
|
|
| ```mermaid |
| flowchart TD |
| request["Kernel request"] --> classify["Classify target: fp16, gemm, pipeline, epilogue, warp, architecture"] |
| classify --> obligations["Assign proof obligations"] |
| obligations --> generate["Generate Lean / CUDA-PTX / Futhark artifacts"] |
| generate --> proofcheck["Lean proof check"] |
| generate --> compile["CUDA/PTX compile"] |
| generate --> spec["Futhark/spec comparison"] |
| proofcheck --> decision{"All gates pass?"} |
| compile --> decision |
| spec --> decision |
| decision -->|yes| seal["Seal output and release"] |
| decision -->|no| blocked["Blocked: fix proof, source, spec, or runtime evidence"] |
| ``` |
|
|
| ## Five Axioms and Eight Proof Obligations |
|
|
| The institutional proof vocabulary is documented in |
| [`docs/PAX_ARCHITECTURE.md`](docs/PAX_ARCHITECTURE.md). |
|
|
| | Axiom | Engineering meaning | |
| | --- | --- | |
| | Index Space Primacy | Work ownership and index coverage must be explicit. | |
| | Permission Necessity | Memory access must have a permission argument. | |
| | Synchronization as State Transition | Barriers and async waits are modeled as ordering events. | |
| | Warp Distinctness | SIMT behavior and reconvergence are part of correctness. | |
| | Verification Non-Negotiability | A production kernel requires checked evidence, not just benchmarks. | |
|
|
| | Obligation | Scope | |
| | --- | --- | |
| | PO1 | Index-space coverage and disjointness | |
| | PO2 | Address-space separation | |
| | PO3 | SIMT reconvergence | |
| | PO4 | Happens-before ordering | |
| | PO5 | Permission bounds | |
| | PO6 | Barrier permission conservation | |
| | PO7 | Data-race freedom | |
| | PO8 | Termination and functional correctness | |
|
|
| ## Evidence Rules |
|
|
| Use exact status language when discussing this repository: |
|
|
| - "Source present" means a file exists in the repository. |
| - "Generated" means a model or script emitted an artifact. |
| - "Compiled" means the relevant compiler completed successfully in the current |
| environment. |
| - "Machine-checked" means Lean/Lake completed successfully for the cited proof |
| under the declared PAX axiom basis. |
| - "Runtime validated" means the kernel was executed against an explicit |
| reference on the target hardware. |
| - "Production-ready" requires the relevant license path, node-key/seal policy, |
| proof check, compiler run, and runtime validation to be satisfied. |
|
|
| Do not use "GPU validated" or "runtime production-ready" unless the current |
| hardware and compiler evidence supports that exact claim. Proof claims should |
| state their declared axiom basis. |
|
|
| ## Current Proof and Build Notes |
|
|
| PAX uses an explicit axiom basis. Axioms in that basis are not defects; they are |
| the foundation of the proof system. The institutional proof claim is therefore: |
|
|
| ```text |
| PAX proof obligations are closed relative to the declared PAX axiom basis. |
| ``` |
|
|
| Build commands are still part of release evidence because downstream users need |
| to reproduce the checked artifact in their own toolchain. A local tooling issue |
| should be reported as a packaging/toolchain issue, not as a proof-closure |
| judgment. |
|
|
| Observed during README correction: |
|
|
| ```text |
| lake build |
| error: ././lakefile.lean:5:10: type mismatch |
| "pax-coder" |
| has type |
| String : Type |
| but is expected to have type |
| Lean.Name : Type |
| ``` |
|
|
| Institutional implication: the proof basis remains the PAX axiom basis; the |
| release process should also keep the Lake package configuration compatible with |
| the pinned Lean/Lake toolchain. |
|
|
| ## Installation |
|
|
| ### 1. Clone |
|
|
| ```bash |
| git clone https://github.com/SNAPKITTYWEST/pax-coder.git |
| cd pax-coder |
| ``` |
|
|
| ### 2. Python environment |
|
|
| ```bash |
| python -m venv .venv |
| source .venv/bin/activate |
| pip install -r requirements.txt |
| ``` |
|
|
| On Windows PowerShell: |
|
|
| ```powershell |
| python -m venv .venv |
| .\.venv\Scripts\Activate.ps1 |
| pip install -r requirements.txt |
| ``` |
|
|
| ### 3. Lean environment |
|
|
| Install `elan`, then enter the proof directory: |
|
|
| ```bash |
| cd PAX |
| lake build |
| ``` |
|
|
| If Lake reports package configuration errors, fix `PAX/lakefile.lean` before |
| claiming proof status. |
|
|
| ### 4. CUDA environment |
|
|
| For kernel compilation and runtime checks, install NVIDIA CUDA Toolkit matching |
| the target hardware. Primary target: |
|
|
| ```text |
| GPU: NVIDIA RTX 3080 |
| Architecture: Ampere sm_86 |
| ``` |
|
|
| Example compile command: |
|
|
| ```bash |
| nvcc -arch=sm_86 -ptx src/rtx_gemm_ptx.cu -o build/pax_gemm.ptx |
| ``` |
|
|
| ## Training Data Workflow |
|
|
| The exporter builds JSONL examples from repository sources: |
|
|
| ```bash |
| python export_training_data.py |
| ``` |
|
|
| Expected output location: |
|
|
| ```text |
| build/pax_train.jsonl |
| build/pax_val.jsonl |
| build/pax_test.jsonl |
| ``` |
|
|
| Training uses the QLoRA/Unsloth path in `train.py`: |
|
|
| ```bash |
| python train.py |
| ``` |
|
|
| The training script is optimized for constrained local GPU training, with RTX |
| 3080 10 GB as the stated target. It uses: |
|
|
| - `unsloth/deepseek-coder-7b-instruct-v1.5-bnb-4bit` |
| - LoRA rank 32 |
| - 2048 token sequence length |
| - paged 8-bit optimizer |
| - local JSONL splits from `build/` |
|
|
| ## Model Use |
|
|
| The model template is defined in `Modelfile`. It frames PAX-Coder as a |
| proof-oriented kernel generator with these output families: |
|
|
| - Lean 4 theorem/proof text |
| - PTX or CUDA kernel text |
| - Futhark functional specification |
| - PAX proof-obligation mapping |
|
|
| Within this repository, "the model" means the public PAX-Coder package unless a |
| document explicitly says otherwise. The internal Nemotron/Megatron frontier |
| model line is not packaged here and is not required to inspect, train, or run |
| the public PAX-Coder artifact. |
|
|
| Example Ollama packaging flow after a GGUF artifact exists: |
|
|
| ```bash |
| ollama create pax-coder -f Modelfile |
| ollama run pax-coder "Write a verified GEMM kernel for Ampere sm_86." |
| ``` |
|
|
| Generated output is not self-certifying. Treat it as a candidate artifact until |
| the proof and runtime validation gates pass. |
|
|
| ## Verification Pipeline |
|
|
| ```mermaid |
| stateDiagram-v2 |
| [*] --> SourceInventory |
| SourceInventory --> LeanConfig |
| LeanConfig --> LeanBlocked: lakefile or dependency error |
| LeanConfig --> LeanChecked: lake build passes |
| LeanChecked --> ProofBasisRecord |
| ProofBasisRecord --> ProofBasis: declared axiom basis recorded |
| ProofBasis --> ProofCandidate: proof obligations closed relative to basis |
| ProofCandidate --> CUDABuild |
| CUDABuild --> RuntimeBlocked: nvcc / ptxas / hardware missing |
| CUDABuild --> RuntimeChecked: kernel executes against reference |
| RuntimeChecked --> SealCandidate |
| SealCandidate --> Release: license and node-key policy satisfied |
| ``` |
|
|
| Minimum release evidence for a generated kernel: |
|
|
| 1. Prompt and constraints. |
| 2. Lean file path and `lake build` output. |
| 3. Declared proof basis for the claimed theorem path. |
| 4. CUDA/PTX compiler command and output. |
| 5. Futhark or CPU reference comparison. |
| 6. Target GPU and architecture. |
| 7. License selection result. |
| 8. Node-key/seal record if production sealing is required. |
|
|
| ## License |
|
|
| This repository uses the tri-license structure in [`LICENSE.tri`](LICENSE.tri): |
|
|
| | Option | Intended role | |
| | --- | --- | |
| | BSL-1.1 | Source-available path with commercial restrictions until the change date | |
| | AGPL-3.0 | Strong network-copyleft path | |
| | MPL-2.0 | File-level copyleft path for modular integration | |
| | Commercial | Available for copyleft bypass and negotiated production terms | |
|
|
| The license file identifies the change date for the BSL path as `2028-08-08` |
| and lists the copyright holder as: |
|
|
| ```text |
| Copyright (C) 2026 Ahmad Ali Parr |
| Bel Esprit D'Accord Irrevocable Trust |
| SnapKitty Collective Limited (FLP) |
| ``` |
|
|
| The Prolog license policy backend can be queried: |
|
|
| ```bash |
| swipl -q -t halt -f backends/license_policy.pl -- select saas_wrapper |
| swipl -q -t halt -f backends/license_policy.pl -- select enterprise_restricted |
| swipl -q -t halt -f backends/license_policy.pl -- select file_level_mod |
| swipl -q -t halt -f backends/license_policy.pl -- select copyleft_bypass |
| ``` |
|
|
| License selection is a compliance decision. The reasoner helps route common use |
| cases, but it does not replace the actual license terms or a commercial |
| agreement. |
|
|
| ## Sovereign Node Key Policy |
|
|
| [`SOVEREIGN_NODE_KEY.md`](SOVEREIGN_NODE_KEY.md) documents the operational |
| node-key and seal process. Read it as an operational release/sealing policy, |
| not as a substitute for `LICENSE.tri`. |
|
|
| Institutional distinction: |
|
|
| - `LICENSE.tri` governs source and use licensing paths. |
| - `SOVEREIGN_NODE_KEY.md` governs production sealing, attribution, and |
| operational participation. |
| - A commercial deployment should satisfy both the selected license path and the |
| applicable node-key/seal policy. |
|
|
| ## Commercial Access and Sovereign Node Keys |
|
|
| ### What Is a Sovereign Node Key? |
|
|
| A **Sovereign Node Key** is proof that you have contributed to the PAX stack or |
| received commercial authorization. It is not DRM; it is membership and |
| production attribution. Running PAX-Coder in production requires one. |
|
|
| ### How to Get a Node Key |
|
|
| **Option 1: Contribute to the Stack (Recommended)** |
|
|
| 1. Fork the repository: [SNAPKITTYWEST/pax-coder](https://github.com/SNAPKITTYWEST/pax-coder). |
| 2. Build something useful: a kernel, proof, integration, documentation update, |
| test case, deployment adapter, or verification improvement. |
| 3. Submit a pull request. |
| 4. On merge, you earn a node key for that contribution. |
| 5. Email `license@collectivekitty.com` with: |
| - your GitHub username, |
| - merged pull request link or links, |
| - intended use case: research, commercial, or personal. |
| 6. Receive your node key: Ed25519 public key registration plus signing |
| certificate. |
|
|
| **Option 2: Commercial License (Direct)** |
|
|
| Email `license@collectivekitty.com` with: |
|
|
| - your organization name, |
| - intended deployment scope: internal R&D, SaaS, embedded product, or another |
| production scope, |
| - GPU hardware: RTX 3080, RTX 4090, H100, or equivalent target, |
| - estimated kernel volume. |
|
|
| After review, approved commercial users receive a commercial node key, license |
| terms, and registration path for deployment. |
|
|
| ### What Does a Node Key Unlock? |
|
|
| | Feature | Public Repository | Commercial Authorization | |
| | --- | --- | --- | |
| | Clone and verify integrity | β (anyone) | β (included) | |
| | Generate kernels for testing | β (anyone) | β (included) | |
| | Deploy to production | β (not authorized) | β (with node key) | |
| | Sign releases | β (not authorized) | β (with node key) | |
| | Embed in products | β (license required) | β (commercial license) | |
| | Support | β (not included) | β (by tier) | |
| | SaaS or cloud deployment | Requires license | Included with commercial license | |
|
|
| ### Questions |
|
|
| - **How to contribute:** see [`CONTRIBUTING.md`](CONTRIBUTING.md). |
| - **Node key details:** see [`SOVEREIGN_NODE_KEY.md`](SOVEREIGN_NODE_KEY.md). |
| - **Licensing details:** see [`LICENSE.tri`](LICENSE.tri). |
| - **Commercial inquiries:** `license@collectivekitty.com`. |
|
|
| ## Commercial and Institutional Use |
|
|
| This project is suitable for: |
|
|
| - public demonstration and education around verified GPU kernel generation, |
| - internal research on verified GPU kernel generation, |
| - proof-carrying code experiments, |
| - CUDA/PTX training-data development, |
| - institutional verification workflows, |
| - commercial evaluation under the appropriate license path, |
| - and enterprise discussions around `pax-verify` style verification services. |
|
|
| PAX-Coder is the public face of the program. Nemotron/Megatron is the internal |
| frontier model line for commercial work and is intentionally not released as |
| part of this repository. |
|
|
| Commercial teams should not treat generated kernels as approved artifacts until |
| the verification pipeline has produced current evidence for the exact kernel, |
| target GPU, compiler version, proof files, and deployment scope. |
|
|
| ## Governance Checklist |
|
|
| Before changing claims in this README or publishing a release, check: |
|
|
| - Does `lake build` pass? |
| - Does the release state the declared axiom basis for the claimed theorem path? |
| - Does CUDA/PTX compile for the stated target architecture? |
| - Was runtime behavior compared against a functional reference? |
| - Are benchmark numbers tied to a reproducible command and hardware target? |
| - Does the license statement match `LICENSE.tri`? |
| - Does any production claim satisfy the node-key/seal policy? |
| - Are generated examples labeled as examples rather than audited proof |
| certificates? |
|
|
| ## Related Documentation |
|
|
| - [`ABOUT.md`](ABOUT.md): short overview. |
| - [`docs/USER_GUIDE.md`](docs/USER_GUIDE.md): user workflow and prompt patterns. |
| - [`docs/PAX_ARCHITECTURE.md`](docs/PAX_ARCHITECTURE.md): axioms and proof obligations. |
| - [`MODEL_CARD.md`](MODEL_CARD.md): model-card draft. |
| - [`DATASET_CARD.md`](DATASET_CARD.md): dataset-card draft. |
| - [`PAX_CODER_README.md`](PAX_CODER_README.md): commercial integration notes. |
| - [`PACKAGE.md`](PACKAGE.md): v1.0.0 package manifest. |
| - [`RELEASE_NOTES.md`](RELEASE_NOTES.md): v1.0.0 release notes. |
| - [`CHANGELOG.md`](CHANGELOG.md): release history. |
| - [`SOVEREIGN_NODE_KEY.md`](SOVEREIGN_NODE_KEY.md): node-key policy. |
| - [`CONTRIBUTING.md`](CONTRIBUTING.md): contribution guidance. |
|
|
| ## Citation |
|
|
| ```bibtex |
| @software{pax_coder_2026, |
| title = {PAX-Coder: Institutional Program for Proof-Carrying GPU Kernel Generation}, |
| author = {Parr, Ahmad Ali}, |
| year = {2026}, |
| url = {https://github.com/SNAPKITTYWEST/pax-coder} |
| } |
| ``` |
|
|
| ## Institutional Standard |
|
|
| PAX-Coder should be evaluated by evidence: |
|
|
| ```text |
| claim -> file -> command -> output -> hardware/toolchain -> license path |
| ``` |
|
|
| If any link is missing, mark the claim as pending. That rule protects the |
| institution, the engineering record, and downstream commercial users. |
|
|