|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | += The Axiom.jl General Form — reference for PanLL coprocessor / backend organisation |
| 4 | +:toc: left |
| 5 | +:sectnums: |
| 6 | + |
| 7 | +Characterised 2026-05-17 from `hyperpolymath/Axiom.jl` @ HEAD (cloned to |
| 8 | +`~/dev/repos/Axiom.jl`). This is the *approach* PanLL's `panel-clades` |
| 9 | +coprocessor must follow (per ADR-0001) — the pattern, not Axiom.jl's code. |
| 10 | + |
| 11 | +NOTE: Axiom.jl is the single estate instance where the standard route |
| 12 | +reached completion. Treat **only** code resembling this form as reference; |
| 13 | +everything else (incl. `src-gossamer/src/coprocessor/`) is presumed mess. |
| 14 | + |
| 15 | +== The seven elements of the general form |
| 16 | + |
| 17 | +. **One abstract supertype.** `abstract type AbstractBackend end` |
| 18 | + (`src/backends/abstract.jl`). Every processor class is a concrete subtype. |
| 19 | + |
| 20 | +. **One concrete backend struct per processor class.** Observed taxonomy: |
| 21 | ++ |
| 22 | +[cols="1,3"] |
| 23 | +|=== |
| 24 | +| Reference / impl | `JuliaBackend` (default, debug/reference), `ZigBackend{lib_path}` (high-perf native) |
| 25 | +| GPU | `CUDABackend`, `MetalBackend`, `ROCmBackend` — each `{device::Int}` |
| 26 | +| Accelerators | `TPUBackend` (tensor), `NPUBackend` (neural), `DSPBackend`, `PPUBackend` (physics), `MathBackend`, `FPGABackend`, `VPUBackend` (vector/vision), `QPUBackend` (quantum), `CryptoBackend` — each `{device::Int}` |
| 27 | +|=== |
| 28 | ++ |
| 29 | +Maps to PanLL's 11-backend set: FPGA→FPGA, DSP→DSP, math→Math, physics→PPU, |
| 30 | +tensor→TPU, vector→VPU, neural→NPU, crypto→Crypto, quantum→QPU. *Gap to |
| 31 | +close:* Axiom.jl has no explicit `I/O` or `audio` backend — the form is |
| 32 | +extended by adding subtypes following the identical pattern. |
| 33 | + |
| 34 | +. **A `SmartBackend` per-operation dispatcher.** Routes each kernel to its |
| 35 | + fastest backend from *recorded benchmark data*, with **graceful fallback |
| 36 | + to the Julia/reference backend** when the preferred native backend is |
| 37 | + unavailable. Holds references to candidate backends; dispatch is |
| 38 | + per-operation (e.g. matmul→BLAS/Julia, gelu→Zig-SIMD), not global. |
| 39 | + |
| 40 | +. **Device selection delegated to `AcceleratorGate`.** Not inline: |
| 41 | + `select_backend`, `fits_on_device`, `estimate_cost`, `device_capabilities`, |
| 42 | + `detect_platform`, `DeviceCapabilities`, `PlatformInfo`. Capability- and |
| 43 | + cost-based selection + platform detection live in a separate registered |
| 44 | + package (`hyperpolymath/AcceleratorGate`, already in the Julia |
| 45 | + registration chain). PanLL should consume this, not reinvent it. |
| 46 | + |
| 47 | +. **ABI/FFI split = the estate language architecture.** |
| 48 | + * **Idris2 ABI = formal spec/scaffold:** `src/Abi/{Types,Layout,Foreign}.idr`, |
| 49 | + concrete `axiom_*` symbols (no template placeholders), typechecks via |
| 50 | + `idris2 --source-dir src --check`. |
| 51 | + * **Zig FFI = authoritative production runtime:** |
| 52 | + `ffi/zig/{src/main.zig,build.zig,include/axiom.h,test/integration_test.zig}`, |
| 53 | + exports concrete `axiom_*` C ABI symbols. *"For release/readiness |
| 54 | + decisions, treat the Zig FFI path as authoritative."* |
| 55 | + * **Host bridge:** `src/backends/zig_ffi.jl`. Bidirectional — |
| 56 | + host→runtime (`axiom_process`, `axiom_process_array`) and runtime→host |
| 57 | + callbacks (`axiom_register_callback`, `axiom_invoke_callback`). |
| 58 | + |
| 59 | +. **Concrete symbol naming.** C ABI symbols are `<project>_*` (here |
| 60 | + `axiom_*`) — concrete, no `{{placeholders}}`. PanLL clades use a concrete |
| 61 | + `panll_*` / clade-scoped scheme; placeholder-only files are not done. |
| 62 | + |
| 63 | +. **Honest status precedence.** Julia = reference/fallback; Idris2 ABI = |
| 64 | + formal scaffold (must typecheck); Zig FFI = authoritative for release. |
| 65 | + Plus CI: backend-parity + runtime-smoke checks gate readiness. |
| 66 | + |
| 67 | +== Re-validation status (the ADR-0001 gate) |
| 68 | + |
| 69 | +* **Characterised:** ✅ (this document, from the cloned repo). |
| 70 | +* **Self-attested validation (per `Axiom.jl/ABI-FFI-README.md`):** Idris2 |
| 71 | + ABI typechecks; `cd ffi/zig && zig build test` passes; Julia↔Zig path is |
| 72 | + CI-covered (backend parity + runtime smoke). The repo's `EXPLAINME.adoc` |
| 73 | + is explicit about caveats (e.g. `@axiom` shape-check is macro-expansion |
| 74 | + time, not dependent-type). |
| 75 | +* **Independent re-validation (done 2026-05-17):** |
| 76 | + ** **Idris2 ABI: ✅ PASSES.** `src/Abi/{Types,Layout,Foreign}.idr` all |
| 77 | + typecheck clean with Idris2 0.8.0 (`/dev/tools/provers/idris2/0.8.0`). |
| 78 | + The formal contract is sound. |
| 79 | + ** **Zig FFI: ❌ FAILS — mechanical bot corruption.** |
| 80 | + `ffi/zig/src/main.zig` has **17** invalid identifiers of the form |
| 81 | + `Axiom.jl_init`, `Axiom.jl_process`, … — a bad token substitution put |
| 82 | + the *repo name with the `.jl` extension* where the project token |
| 83 | + belongs (should be `axiom_init`, `axiom_process`, …). `.` is illegal |
| 84 | + in a Zig identifier, so `zig build test` (Zig 0.15.2) does not compile. |
| 85 | + ** **Damage is localised:** `ffi/zig/include/axiom.h`, the integration |
| 86 | + test, and `ABI-FFI-README.md` are **clean** and correctly use |
| 87 | + `axiom_*`. Only the implementation file `main.zig` was mangled. The |
| 88 | + *design* is intact; this is exactly the "bot/interference mess" class |
| 89 | + ADR-0001 warns about, and is a trivial `s/Axiom\.jl_/axiom_/` repair. |
| 90 | + ** **Estate spread:** the same corruption/placeholder class is present in |
| 91 | + `panll/panel-clades/ffi/zig/{build.zig,test/integration_test.zig}`. |
| 92 | + |
| 93 | +=== Gate verdict |
| 94 | + |
| 95 | +**PASSED with caveat.** The architectural general form is characterised and |
| 96 | +the formal Idris2 contract re-validates clean — this document is a |
| 97 | +trustworthy reference for P2 *design*. The reference *Zig implementation* |
| 98 | +needs a trivial de-corruption (Axiom.jl repo, separate from this work) |
| 99 | +before it is a runnable exemplar. P2 build (not design) is gated on that |
| 100 | +repair landing. |
| 101 | + |
| 102 | +== Implication for PanLL panel-clades |
| 103 | + |
| 104 | +`panel-clades/` already mirrors this skeleton (Idris2 `src/abi/*.idr`, Zig |
| 105 | +`ffi/zig/`, a2ml clade specs) but is an *uninstantiated template*. The work |
| 106 | +is to instantiate it *to this exact form*: AbstractBackend supertype + 11 |
| 107 | +backend subtypes + Smart dispatcher + AcceleratorGate consumption + concrete |
| 108 | +Idris2 ABI + authoritative Zig FFI + bidirectional host bridge + parity/smoke |
| 109 | +CI. No deviation from the Axiom.jl form. |
0 commit comments