demo/README.md

PAX-Coder Demo

Verified GPU kernel generation demonstration with realistic Lean 4 proofs, PTX kernels, and Futhark specs.

Quick Start

# Mock mode (no model download required)
python3 demo.py

# Non-interactive mode (useful for CI/scripting)
python3 demo.py --no-pause

# Use actual Ollama model (if running locally)
python3 demo.py --live

# Target H100 (Hopper, sm_90) instead of RTX 3080 (Ampere, sm_86)
python3 demo.py --arch sm_90

What It Shows

The demo demonstrates PAX-Coder end-to-end with 5 kernel categories:

Category	What's Proven	Example Output
FP16	IEEE-754 binary16 rounding error bound	Lean 4 proof + PTX cvt.rn.f16.f32
GEMM	128×128 matrix multiply correctness	mma.sync kernel + index partition proof
Pipeline	3-stage async GEMM throughput bound	cp.async + happens-before proof
Epilogue	Bias+GeLU fusion numerical stability	In-register computation proof
Warp	Tree-reduction warp shuffle correctness	shfl.sync.xor + divergence-free guarantee

For each category, you see:

• Prompt: What was asked
• Lean 4 Proof: Machine-checked correctness (zero sorry)
• PTX Kernel: Hand-rolled mma.sync, ldmatrix, cp.async code
• Futhark Spec: Functional reference implementation
• PAX Certificate: Which proof obligations (PO1–PO8) are satisfied

Command-Line Options

--live              Use actual Ollama instance (localhost:11434)
--arch {sm_86,sm_90}
                    Target GPU (default: sm_86 / RTX 3080)
--no-rich           Disable colored terminal output (plain text)
--speed SPEED       Streaming animation speed multiplier (default: 1.0)
--no-pause          Skip pauses between demos (for CI/automation)
--help              Show this help message

Requirements

Minimal (Mock Mode)

• Python 3.10+
• Standard library only

Optional (Live Mode + Rich Output)

• Ollama running at localhost:11434 with Snapkitty/pax-coder-7b model
• rich library: pip install rich

# Install rich for prettier output
pip install rich

# Run Ollama locally for --live mode
ollama run Snapkitty/pax-coder-7b

Example Output

Running python3 demo.py --no-pause will generate ~680 lines showing:

1. PAX-Coder banner with legal information
2. 5 kernel demos (fp16, gemm, pipeline, epilogue, warp)
3. VRAM usage breakdown (~8.1 GB on RTX 3080)
4. Call-to-action for Sovereign Node Key
5. Links to GitHub, HuggingFace, documentation

Sample Output Structure

================================================================================
DEMO 1/5: FP16
================================================================================

📋 PROMPT:
Prove that IEEE-754 binary16 rounding error is bounded by 0.5 ulp...

🔍 LEAN 4 PROOF:
theorem fp16_rounding_bound (x : Float)...
  nlinarith [ulp_nonneg (roundToFP16 x), ...]

⚙️  PTX KERNEL:
// IEEE-754 binary16 RNE conversion
.target sm_86
cvt.rn.f16.f32 h_out, f_in;

🌐 FUTHARK SPEC:
def round_fp16 (x : f32) : f16 = f16.from_f32 x

✓ PAX CERTIFICATE: [PO4 | PO5 | PO7]

Proof Obligations (PO1–PO8)

PO	Invariant	Example
PO1	Index space partition	Coverage + disjointness proven
PO2	Address space separation	shared ∩ global = ∅
PO3	SIMT reconvergence	Before every barrier
PO4	Happens-before SPO	Strict partial order proven
PO5	Permission sum ≤ 1	Fractional permissions at every address
PO6	Barrier permission conservation	Preserved across __syncthreads
PO7	Data-race freedom	No concurrent writes to same address
PO8	Termination + correctness	Kernel always terminates correctly

Each PAX-Coder output lists which POs are satisfied by that kernel.

Architecture Targets

Ampere (sm_86) — RTX 3080 — Default

• mma.sync.aligned.m16n8k8.f32 (FP32 accumulate)
• mma.sync.aligned.m16n8k16.f32 (FP16 input)
• ldmatrix.sync.aligned.m8n8.x4.b16
• cp.async.ca.shared.global + cp.async.wait_group
• Shared memory: 48 KB (or 100 KB dynamic)

Hopper (sm_90) — H100 — --arch sm_90

• TMA (Tensor Memory Accelerator) multicast
• cp.async.bulk (pipelined async copy)
• Cluster sync primitives
• Thread blocks per cluster

Running on Different GPUs

# Default: RTX 3080 Ampere (sm_86)
python3 demo.py

# H100 Hopper (sm_90)
python3 demo.py --arch sm_90

# With actual model (requires Ollama)
ollama run Snapkitty/pax-coder-7b "Write verified GEMM for sm_90"
python3 demo.py --live --arch sm_90

For CI/Automation

# Non-interactive, plain text, full output to file
python3 demo.py --no-pause --no-rich > pax_demo.log 2>&1

# Check all POs are satisfied
python3 demo.py --no-pause 2>&1 | grep "PAX CERTIFICATE"

Troubleshooting

ModuleNotFoundError: No module named 'rich'

Rich is optional. Run pip install rich or use --no-rich for plain output.

ModuleNotFoundError: No module named 'requests'

Only needed for --live mode. Install with pip install requests.

Ollama connection refused

Ensure Ollama is running: ollama serve Then in another terminal: ollama run Snapkitty/pax-coder-7b

Unicode/Encoding errors on Windows

The script handles UTF-8 automatically. If issues persist, try --no-rich.

---

Learn More

• GitHub: https://github.com/SNAPKITTYWEST/pax-coder
• HuggingFace: https://huggingface.co/Snapkitty/pax-coder-7b
• Architecture Doc: https://github.com/SNAPKITTYWEST/pax-coder/tree/main/PAX
• User Guide: https://github.com/SNAPKITTYWEST/pax-coder/tree/main/docs

License

PAX-Coder is tri-licensed:

• BSL-1.1 (Business Source License 1.1) — restricts until 2028-08-08
• AGPL-3.0 (GNU Affero General Public License 3.0) — starting 2028-08-08
• MPL-2.0 (Mozilla Public License 2.0) — alternative terms

Copyright: Ahmad Ali Parr, Bel Esprit D'Accord Irrevocable Trust

---

Evidence or Silence — 2026