custom
code
sovereign-compute
File size: 30,426 Bytes
128a6ea
 
 
41d5c39
128a6ea
 
 
 
 
41d5c39
 
 
128a6ea
41d5c39
128a6ea
41d5c39
128a6ea
41d5c39
128a6ea
41d5c39
 
128a6ea
41d5c39
 
 
 
 
128a6ea
41d5c39
 
 
128a6ea
41d5c39
 
128a6ea
41d5c39
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
128a6ea
41d5c39
128a6ea
41d5c39
 
 
 
 
 
128a6ea
41d5c39
128a6ea
41d5c39
 
 
128a6ea
 
41d5c39
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
128a6ea
41d5c39
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
128a6ea
 
41d5c39
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
128a6ea
41d5c39
128a6ea
41d5c39
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
128a6ea
41d5c39
 
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
---
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.