From 5f2f8cbc7d1a04e730bbdb55564e850f44043c57 Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sat, 26 Sep 2026 15:31:25 +0000 Subject: [PATCH 1/2] =?UTF-8?q?docs:=20silicon-core=20reconnaissance=20rep?= =?UTF-8?q?ort=20(deliverables=20A=E2=80=93J=20+=20reproductions)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Read-only investigation of backend/native/GPU/coprocessor responsibilities in Axiom.jl. No source, dependency or structure changes. Adds: - docs/investigation/2026-09-26-silicon-core-recon/{README,A..J}.adoc - repro/: Zig test files and ctypes probes against the CI-built libaxiom_zig.so Empirically confirmed (Zig 0.15.2, ReleaseFast .so): batchnorm wrong >4096 features and SIGSEGV from 8192; pooling wrappers pass column-major memory to row-major kernels; tanh NaN for x >= 44.5; chunking underflow at batch=5 (UB); axiom_matmul_checked 9-16x slower than the benchmarked kernel; 44 exports vs documented 32/36; ffi/zig does not compile. Recommendation: defer extraction (Option D), build the runtime seam in-tree, then supersede AcceleratorGate.jl rather than create a third package. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .../A-component-map.adoc | 169 ++++++++++++ .../B-backend-status.adoc | 107 ++++++++ .../C-abi-ffi-discrepancies.adoc | 83 ++++++ .../D-numerical-parity-risks.adoc | 225 ++++++++++++++++ .../E-memory-performance.adoc | 138 ++++++++++ .../F-extraction-recommendation.adoc | 130 +++++++++ .../G-api-boundary.adoc | 166 ++++++++++++ .../H-staged-plan.adoc | 130 +++++++++ .../I-not-recommended.adoc | 49 ++++ .../J-upstream-issues.adoc | 255 ++++++++++++++++++ .../2026-09-26-silicon-core-recon/README.adoc | 91 +++++++ .../repro/README.adoc | 35 +++ .../repro/activation_probe.py | 34 +++ .../repro/batchnorm_probe.py | 22 ++ .../repro/canary_probe.py | 17 ++ .../repro/chunking_probe.py | 29 ++ .../repro/layout_probe.py | 79 ++++++ .../repro/matmul_cost.py | 32 +++ .../repro/repro_batchnorm.zig | 33 +++ .../repro/repro_underflow.zig | 45 ++++ .../repro/repro_underflow_canary.zig | 53 ++++ 21 files changed, 1922 insertions(+) create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/A-component-map.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/B-backend-status.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/C-abi-ffi-discrepancies.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/D-numerical-parity-risks.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/E-memory-performance.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/F-extraction-recommendation.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/G-api-boundary.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/H-staged-plan.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/I-not-recommended.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/J-upstream-issues.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/README.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/README.adoc create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/batchnorm_probe.py create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/chunking_probe.py create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/layout_probe.py create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/repro_batchnorm.zig create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow.zig create mode 100644 docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow_canary.zig diff --git a/docs/investigation/2026-09-26-silicon-core-recon/A-component-map.adoc b/docs/investigation/2026-09-26-silicon-core-recon/A-component-map.adoc new file mode 100644 index 0000000..4cc0266 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/A-component-map.adoc @@ -0,0 +1,169 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += A. Component map +:toc: + +Classification key: + +* *production-tested* — exercised by `Pkg.test()` or a CI script that would fail if the component broke. +* *experimental* — real code, self-described or evidently heuristic/simplified. +* *stub / capability-only* — types, env-var detection and dispatch plumbing with no execution path of its own. +* *disconnected* — present in the tree but not reachable from any public entry point, or does not build. +* *documentation-only* — described in docs with no corresponding code. + +Line counts are `wc -l` at `79e6f48` (27,093 lines of `.jl`/`.zig`/`.h` total). + +== A.1 Julia package (`src/`, `ext/`) + +[cols="2,1,1,4"] +|=== +| Component | LOC | Class | Evidence / notes + +| `types/` — `Tensor{T,N,Shape}`, `DynamicTensor`, arithmetic +| 1,179 | production-tested +| `test/runtests.jl` "Tensor Types", "Tensor Arithmetic", "Compile-Time Shape Verification". Design note: `Tensor(data) = Tensor{T,N,Tuple(size(data))}(data)` (`tensor.jl:161`) puts the *runtime* size into the type → see E.5. + +| `layers/` — Dense, Conv{1,2,3}d, ConvTranspose2d, activations, normalisation, pooling, invertible +| 3,505 | production-tested (Julia path only) +| Tested on `JuliaBackend` only. Backend-aware `forward` for Dense/Conv2d/BatchNorm/LayerNorm/RMSNorm/Dropout lives in `backends/abstract.jl`, not in `layers/` (`normalization.jl:51` comment). Activations, pooling and LogSoftmax never dispatch to a backend (see B.3). `conv.jl:245` "Simplified 1D conv", `normalization.jl:296,320` "Simplified implementation". + +| `dsl/` — `@axiom`, `@prove`, `Pipeline`/`Sequential`/`Chain`, `@ensure` +| 1,738 | production-tested (structure) / experimental (`@prove`) +| `prove.jl:10,18,244,258,274,316` label strategies 1 and 3 "experimental heuristic — not symbolic execution, not a theorem prover". Strategy 2 = SMT extension (below). + +| `autograd/`, `training/` (Zygote-based) +| 1,407 | production-tested +| "Optimizers", "Loss Functions", "Data Utilities" test sets. Zygote is a hard dependency used only here and in `layers/invertible.jl`. + +| `verification/` — `verify()`, properties, certificates, Ed448+Dilithium signing +| 2,024 | production-tested (structural checks) / experimental (proof semantics) +| `checker.jl:295`: `ValidProbabilities` is `:proven` iff `last_layer isa Softmax`. Empirical `check()` runs on `current_backend()` and records no backend provenance. Signing calls a Rust cdylib in `crypto/` (837 LOC, separate build) — `test/verification/hybrid_signing_tests.jl`. + +| `proof_export.jl` — Lean/Coq/Isabelle/Agda export +| 1,115 | experimental +| Emits theorem *skeletons*; `proof_export.jl:185–246` counts unresolved placeholders in the emitted file ("vacuous placeholder", "`theorem foo : True := trivial`-style"). + +| `backends/abstract.jl` +| 3,069 | mixed — see B +| One file holds: 15 backend types, `SmartBackend`, `current_backend()` global, Float32 reference kernels, backend-aware layer forwards, `compile()` + optimisation passes, `MixedPrecisionWrapper`, GPU/coprocessor compiled-model wrappers, self-healing wrappers, diagnostics, capability reports. This is the seam a runtime package would need, and it is not separable today. + +| `backends/julia_backend.jl` +| — (part of 4,573) | production-tested +| Generic-`T` reference kernels that *duplicate* the Float32 kernels in `abstract.jl` with different summation order (D.6). + +| `backends/zig_ffi.jl` +| 651 | production-tested (7 ops via `test/ci/backend_parity.jl`, only when `AXIOM_ZIG_LIB` is set) +| 29 `ccall`s; `dlsym` per call (`zig_ffi.jl:49–55`); every wrapper silently returns the Julia result when `!zig_available()` (`zig_ffi.jl:51,102`). + +| `backends/gpu_hooks.jl` +| — | stub / capability-only (in-tree) — real hooks arrive via extensions +| `backend_gpu_*` default methods are CPU implementations. `cuda_available()` honours `AXIOM_CUDA_AVAILABLE` before any device probe — in the base definition (`abstract.jl:1700–1704`, returns `false` otherwise) *and* in the extension override (`ext/AxiomCUDAExt.jl:16–20`, `forced !== nothing && return forced` precedes `CUDA.functional()`); `gpu_hooks.jl:454` is a docstring example of the override. `gpu_capability_report()["kernel_hooks_loaded"]` (`:125–143`) is the only genuine "is an accelerator really wired" signal in the package. + +| Coprocessor backends (TPU, NPU, PPU, MATH, FPGA, DSP, VPU, QPU, CRYPTO) in `abstract.jl` +| ≈900 | stub / capability-only +| Availability = env var (`AXIOM__AVAILABLE`); execution = Julia path with a one-time warning unless `AXIOM__REQUIRED` makes it error. `REGISTRY-READINESS.adoc:51` says so itself: "type stubs, not working hardware backends". "MATH" = AVX-512 and "CRYPTO" = AES-NI are CPU ISA features presented as coprocessors. Tested only as env-var plumbing (`test/runtests.jl:211–255`, `test/ci/*_required_mode.jl`). + +| `vendored/AcceleratorGateVendored.jl` +| 494 | disconnected +| Imported at `abstract.jl:8–10`; the only call site is `abstract.jl:2277`, guarded by `applicable(device_capabilities, backend)` which is false for every Axiom backend (disjoint type hierarchy). Upstream `hyperpolymath/AcceleratorGate.jl` exists (v0.1.0, unregistered, deps Dates+Libdl) and its README states it was "extracted from Axiom.jl's backend module". See F. + +| `ext/AxiomCUDAExt.jl`, `AxiomAMDGPUExt.jl`, `AxiomMetalExt.jl` +| ≈700 | experimental — no hardware evidence +| Real vendor-array code. Hardware CI gated on `vars.AXIOM_ENABLE_GPU_HARDWARE_CI` + self-hosted runners (`ci.yml`); `benchmark/gpu_performance_baseline.json` is an empty template ("Populate … from dedicated CUDA/ROCm/Metal hardware runners"). AMDGPU/Metal are copy-edits of the CUDA file. + +| `ext/AxiomSMTExt.jl` + `packages/SMTLib.jl` (2,329 LOC, unregistered path dep) +| ≈2,700 | experimental +| Sound sat/unsat mapping (`AxiomSMTExt.jl:125–150`), but variables are declared `Real` (`SMTLib.jl:734–736`), `≈` becomes `==`, and the model is never encoded (no reference to weights/layers in the extension). Tests skip when no solver is installed (`runtests.jl:785–812`). + +| `ext/AxiomPyTorchExt.jl` +| 291 | experimental +| Defines `Axiom.from_pytorch(::String)`; core `integrations/interop.jl:348` defines `from_pytorch(::AbstractString; strict)` for a JSON descriptor format. Loading PyCall+torch therefore changes which method a `String` path hits `[static]` (J-27). + +| `integrations/` — HuggingFace, interop (PyTorch descriptor, ONNX export) +| 1,887 | experimental +| `huggingface.jl:26–29` "NOT implemented (honest gaps)"; architectures are "simplified" (`:362,453,548`); tokenizer is a documented stub (`:809–812`). + +| `serving/` +| 549 | production-tested (HTTP handlers unit-tested) +| Only consumer of the `HTTP` hard dependency besides HuggingFace download. + +| `model_metadata.jl`, `model_packaging.jl` +| 823 | production-tested +| `backend_compatibility::Vector{String}` is the only backend-related metadata anywhere; it is declarative, not measured. +|=== + +== A.2 Native and specification trees + +[cols="2,1,1,4"] +|=== +| Component | LOC | Class | Evidence / notes + +| `zig/` — `libaxiom_zig` (matmul, activations, conv, pool, norm, attention, threading) +| 3,410 | production-tested (Zig unit tests; 7 ops parity-tested from Julia) +| Builds with Zig 0.15.2 (the CI version); `build.zig` uses the `b.addLibrary` API (Zig ≥ 0.14) and declares no minimum; Zig 0.13 fails. 44 exports; 29 wrapped from Julia; 15 exported-but-unwrapped (`add`, `mul`, `bmm`, `fill`, `avgpool2d`, `relu`, `relu6`, `rotary_embedding`, `scaled_dot_product_attention`, `flash_attention`, and their `_checked` twins). Four confirmed defects (B.2, D, J). + +| `ffi/zig/` — second Zig tree + `include/axiom.h` + `test/integration_test.zig` +| 392 | disconnected (does not compile) +| `src/main.zig:55` `export fn Axiom.jl_init()` — a project-name template placeholder was expanded to `Axiom.jl`, which is not a valid identifier; same at `:74,90,114,136,149,185,199,204,216,247`. Fails to parse under Zig 0.13/0.14/0.15. `ABI-FFI-README.adoc:108` claims it is "concrete (non-template) and internally self-consistent" and that `cd ffi/zig && zig build test` works. + +| `src/Abi/*.idr`, `axiom-abi.ipkg` — Idris2 ABI/layout specification +| 568 | documentation-only (as a check) +| `Foreign.idr` declares the generic lifecycle symbols of `ffi/zig` plus `axiom_matmul/relu/conv2d` — 3 of the 44 real exports. `ABI-FFI-README.adoc` itself notes the `Verify.*` functions are `putStrLn` stubs. Nothing in CI compares the Idris declarations to `nm -D` output. + +| `crypto/` — Rust cdylib (Ed448 + ML-DSA-87) +| 837 | production-tested when built +| Loaded via `AXIOM_CRYPTO_LIB`; tests fall back when absent. + +| `benchmark/` +| — | documentation-only (stale) +| `results_2026-02-20_julia-rust-zig.adoc` reports Zig matmul 512² = 25.6 ms; the current wrapper's `axiom_matmul_checked` measures 284.6 ms on this machine (unchecked: 21.7 ms) — the published numbers were produced by a kernel the Julia wrapper no longer calls (E.1). Also references a Rust backend that no longer exists in the tree. +|=== + +== A.3 Documentation surfaces (claims audited in C, D, J) + +`README.adoc`, `ROADMAP.adoc`, `PROOF-PROGRESS.adoc`, `TOPOLOGY.adoc`, +`ABI-FFI-README.adoc`, `REGISTRY-READINESS.adoc`, `TEST-NEEDS.adoc`, +`docs/wiki/Verification.md`, `docs/design-diary/ULTRAPLAN.adoc`, `CHANGELOG.adoc`. +They disagree with each other on the same facts: `PROOF-PROGRESS.adoc:55,224` +still says the Zig backend is "PLANNED / not yet wired", `ROADMAP.adoc:19,31,93` +ticks backend parity and "production-hardened GPU paths" as done, and +`REGISTRY-READINESS.adoc:47–54` says there is "no native GPU acceleration of +Axiom's own" and that accelerator backends are "type stubs". The last one is +the accurate description. + +== A.4 Dependency boundary facts (Project.toml) + +* Hard deps: `Dates, HTTP, JSON, Libdl, LinearAlgebra, Random, SHA, Serialization, Statistics, Zygote`. + `HTTP` is used only by `serving/` and HuggingFace download; `Zygote` only by + autograd/training/invertible; `Random` only by `DataLoader`. None is unused, + but `HTTP`/`Zygote` are heavy for an inference-only consumer. +* Weak deps: `AMDGPU, CUDA, KernelAbstractions, Metal, PyCall, SMTLib`. + *`KernelAbstractions` is an orphan*: no extension and no source reference. +* Extensions: 5 (no `AxiomKernelAbstractionsExt`). +* Toolchain pins disagree: `Justfile:128` checks Zig "0.13"; `mise.toml:7` + `zig = "latest"`; `ci.yml:75,105` `0.15.2`; `zig/build.zig` needs ≥ 0.14 (`b.addLibrary` API) and declares no minimum. + Zig 0.13 cannot build the tree (`b.addLibrary` API). +* De-facto configuration surface: *62 distinct `AXIOM_*` environment + variables* read by `src/` + `ext/` (`grep -rhoE 'AXIOM_[A-Z0-9_]+' src ext | sort -u`). + There is no single documented list and no schema; the same concept (strict + mode) is spelt `AXIOM__REQUIRED` for coprocessors, `AXIOM_GPU_SELF_HEAL=0` + for GPUs, and does not exist for Zig. + +== A.5 Where responsibilities are entangled (the actual problem) + +. `current_backend()` is a process-global read inside layer `forward` + (`dense.jl`, `abstract.jl:1073`, `normalization.jl:123`). A model has no + backend identity; `compile(model, backend=…)` for Julia/Zig returns a + wrapper that still consults the global. +. Reference kernels exist twice in Julia (`abstract.jl` Float32 specialisations + vs `julia_backend.jl` generic) and once in Zig; which Julia copy runs depends + on the element type (D.6). +. Proofs (`verify`, `@prove`, certificates) are backend-blind; execution + (`compile`, `SmartBackend`, GPU/coprocessor wrappers) is proof-blind. + Nothing links a certificate hash to a kernel/ABI version. +. Fallback policy is implemented six different ways (bare `try … catch end` + in layer forwards; `zig_available()` early-returns; GPU self-heal; + coprocessor self-heal + required; `compile_to_backend` returning the + original model; SmartBackend heuristics) with no shared record of what ran. + +These four entanglements — not the number of directories — are what +G/H address. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/B-backend-status.adoc b/docs/investigation/2026-09-26-silicon-core-recon/B-backend-status.adoc new file mode 100644 index 0000000..067394e --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/B-backend-status.adoc @@ -0,0 +1,107 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += B. Backend status table +:toc: + +"Verified" below means: a test exists that compares numerical output against +the reference on that backend *and* would fail if the backend silently fell +back. Compiling, loading, or returning the right shape does not count. + +== B.1 Status by backend type + +[cols="1,1,1,1,2,3"] +|=== +| Backend type | Kernels exist | Reachable from a layer `forward` | Strict mode | Tested how | Status + +| `JuliaBackend` | yes (two copies) | yes (default) | n/a | `Pkg.test()`; parity *baseline* | *Reference.* Float32 and generic-`T` copies use different summation orders (D.6). +| `ZigBackend` | yes, 44 exports (29 wrapped) | yes, for Dense/Conv2d/BatchNorm/LayerNorm/RMSNorm/Dropout — only after `set_backend!` | *none* — every wrapper returns the Julia result when `!zig_available()` (`zig_ffi.jl:51,102`) | `test/ci/backend_parity.jl` (7 ops, tiny random shapes, one NaN case); `test/ci/zig_checked_ffi.jl` | *Partially verified; 4 confirmed defects* (B.2). The documented `compile(model, backend=ZigBackend(path))` on a `Sequential` runs pure Julia (B.3). +| `SmartBackend` | delegates | yes | none | none directly | `SmartBackend(; zig_path=nothing)` (`abstract.jl:166`) silently means "no Zig"; layernorm delegation drops `normalized_shape` (`abstract.jl:215`). Activation routing is inert for `Pipeline` inference (B.3). +| `CUDABackend` | in `ext/AxiomCUDAExt.jl` | via `GPUCompiledModel` only (`compile(..., backend=CUDABackend())`), not via `set_backend!` layer path | none; `AXIOM_GPU_SELF_HEAL=0` only stops *runtime* self-healing | `test/ci/gpu_fallback.jl` (no GPU: asserts CPU fallback works); `gpu_hardware_smoke.jl` behind `vars.AXIOM_ENABLE_GPU_HARDWARE_CI` | *Unverified on hardware.* Empty baseline file; smoke test compares `acc ≈ cpu`, which passes trivially on fallback; `AXIOM_GPU_REQUIRED` is read by the test only, not by the library. +| `ROCmBackend` | `ext/AxiomAMDGPUExt.jl` (copy-edit of CUDA) | as above | none | as above | *Unverified on hardware.* +| `MetalBackend` | `ext/AxiomMetalExt.jl` | as above | none | as above | *Unverified on hardware.* Accepts `Float64` arrays that Metal cannot execute natively `[static]`. +| `TPUBackend`, `NPUBackend`, `PPUBackend`, `MATHBackend`, `FPGABackend`, `DSPBackend`, `VPUBackend`, `QPUBackend`, `CRYPTOBackend` | *no* | via `CoprocessorCompiledModel` → Julia path | `AXIOM__REQUIRED=1` → error when env says unavailable | `runtests.jl:211–255`, `test/ci/{coprocessor_strategy,coprocessor_resilience,*_required_mode}.jl` | *Capability-only stubs.* Tests assert the plumbing (env var → `tpu_available()` → wrapper type), never a computation on a device. "MATH" (AVX-512) and "CRYPTO" (AES-NI) are CPU features. +|=== + +== B.2 Native (Zig) backend — per-kernel status + +Built with Zig 0.15.2, `-Doptimize=ReleaseFast` (as CI). `[empirical]` unless noted. + +[cols="2,1,1,3"] +|=== +| Kernel (Julia wrapper → export) | Parity-tested | Result | Notes + +| `backend_matmul` → `axiom_matmul_checked` | yes (16×12·12×7) | correct | 9–16× slower than `axiom_matmul` (E.1). Rejects NaN/Inf with an error — different contract from the Julia reference (D.4). +| `backend_relu` → `axiom_relu_checked` | yes (128; NaN → error) | correct | In-place `backend_relu!` uses the *unchecked* `axiom_relu_inplace` — same op, different NaN contract. +| `backend_gelu`, `backend_sigmoid` → `axiom_gelu/sigmoid` | yes | correct | GELU uses the overflow-safe `1 − 2/(e+1)` form. +| `backend_tanh` / `backend_tanh!` → `axiom_tanh(_inplace)` | *no* | *NaN for x ≥ 44.5 and +Inf* (Julia: 1.0); rel. error 1.3e-3 at x=1e-5, 100 % at 1e-8 | `activations.zig:103–119` uses `(e^{2x}−1)/(e^{2x}+1)`; `repro/activation_probe.py`. +| `backend_softmax`, `backend_log_softmax` → `axiom_softmax/log_softmax` | softmax yes (8×5) | correct for `dim == ndims` | `dim` argument ignored (`zig_ffi.jl:329,351`) `[static]`. `[empirical]` B=4…17 × 2048 correct through the `.so`. +| `backend_conv2d` → `axiom_conv2d` | yes (2×10×10×3, 3×3×3×4) | correct at that shape | Wrapper does full `permutedims` copies both ways (E.3). Stride/padding/dilation/groups other than the tested defaults: untested. +| `backend_batchnorm` → `axiom_batchnorm` | yes (6×8) | *wrong for `num_features` 4097–8191; SIGSEGV from 8192* | Fixed `[4096]f32` stack scratch (`norm.zig:143`); `repro/batchnorm_probe.py`. Reachable from `forward(bn::BatchNorm)` (`abstract.jl:1072–1086`) with the Zig backend set. `training` flag ignored `[static]`. +| `backend_layernorm`, `backend_rmsnorm` → `axiom_layernorm/rmsnorm` | *no* | correct through the shipped `.so` for B=4…17 × 2048/4096/65536, canary intact | `threading.zig:392,469,523` `batch_size − last_start` underflows at `batch_size = 5` (with `MAX_WORKERS = 3`, `total ≥ 8192`): panics in Debug/ReleaseSafe; the same function compiled ReleaseFast in a `zig test` binary segfaults; in the shipped `.so` LLVM happened to make it benign. Undefined behaviour either way. `repro/repro_underflow*.zig`, `repro/canary_probe.py`. 3-D inputs: wrapper treats `size(x,2)` as hidden `[static]`. +| `backend_maxpool2d`, `backend_global_avgpool2d` → `axiom_maxpool2d`, `axiom_global_avgpool2d` (no Zig wrapper exists for `avgpool2d`) | *no* | *wrong values whenever N>1 or C>1 (and for non-square N=1,C=1)* | Wrapper passes column-major bytes to row-major NHWC kernels without `_to_row_major_vec` (`zig_ffi.jl:479–507`, `:513`). `repro/layout_probe.py`: maxpool wrong 5/8, 5/8, 49/54, 7/8 elements in four cases; global-avgpool wrong for every N>1 or C>1. Edge contracts: all-`−Inf` window → `−3.4028235e38` (Julia `−Inf`); NaN in window → `1.0` (Julia `NaN`). Not reachable from `MaxPool2d.forward` (pure Julia) — reachable from direct calls, `SmartBackend`, and benchmarks. +| `backend_dense` (fused) → `axiom_dense`? | no | not probed | `zig_forward(model::Dense)` (`abstract.jl:2495–2502`) drops bias and activation `[static]`. +| attention (`axiom_scaled_dot_product_attention`, `axiom_flash_attention`) | no Julia wrapper | silent no-op for `seq_len > 64` (`attention.zig:29`), `> 4096` for flash | Output buffer left untouched, no error code. +| 15 unwrapped exports | — | unreachable from Julia | `add(_checked)`, `mul(_checked)`, `bmm`, `fill`, `avgpool2d`, `relu`, `relu6(_checked)`, `rotary_embedding`, `scaled_dot_product_attention(_checked)`, `flash_attention(_checked)`. +|=== + +Threading: every `axiom_*` call above the element threshold spawns OS threads +(`std.Thread.spawn`, `threading.zig:220,262,387`) and *ignores spawn failure* +(`catch null`) — the chunk assigned to a thread that failed to start is never +computed and the output buffer keeps its previous contents `[static; not +forced in this environment]`. + +== B.3 Reachability: what the "production path" actually executes `[static]` + +. `compile(model, backend=ZigBackend(path), …)` → `compile_to_backend(model, ::ZigBackend)` + (`abstract.jl:1584`) → `ZigCompiledModel` (`:2460`). +. `forward(::ZigCompiledModel, x)` → `zig_forward(model::Pipeline, …)` → + `forward(pipeline, x)` → each layer calls `current_backend()` — the global, + which is still `JuliaBackend()` unless the user also called + `set_backend!(ZigBackend(path))`. +. Therefore README's "Production path" and CI's "Runtime smoke (accelerated)" + (`test/ci/runtime_smoke.jl:67–79`, which calls `compile(model, + backend=accelerator, verify=false, optimize=:none)` and never + `set_backend!`) execute pure Julia. The smoke test cannot detect this. +. Even with `set_backend!(ZigBackend(path))`: only Dense (matmul), Conv2d, + BatchNorm (inference, affine), LayerNorm/RMSNorm (2-D, affine, cast to + Float32) and Dropout dispatch. `ReLU`, `GELU`, `Tanh`, `Softmax`, + `MaxPool2d`, `AvgPool2d`, `LogSoftmax` layers run pure Julia on every + backend (`activations.jl:275–312`, `pooling.jl:30–60`). The `SmartBackend` + rule "activations → Zig" therefore never fires during `Pipeline` inference. +. GPU: `compile(model, backend=CUDABackend())` produces a `GPUCompiledModel` + whose forward moves data host→device→host *per layer op* (Dense + activation + = 4 transfers). `set_backend!(CUDABackend())` on the layer path: *with* the + extension loaded, Dense/Conv2d/BatchNorm hit the extension's + `backend_matmul/conv2d/batchnorm(::CUDABackend, …)` (`ext/AxiomCUDAExt.jl:168` + ff.) and LayerNorm/RMSNorm raise `MethodError` inside their bare `try/catch` + → silent CPU; *without* the extension, Dense raises `MethodError` (no + fallback method, no `try/catch`) while Conv2d/BatchNorm silently run on + CPU. Only the five `backend_gpu_*` hooks have in-tree CPU fallbacks + (`gpu_hooks.jl:299–313`, `@warn maxlog=1`). + +== B.4 Fallback inventory (where "requested ≠ executed" can happen silently) + +[cols="3,2,2"] +|=== +| Site | Trigger | Observable? + +| `zig_ffi.jl` every wrapper (`:51`, `:102`, …) | `!zig_available()` (env `AXIOM_ZIG_LIB` unset, load failure, `ZigBackend("")`) | No. Returns Julia result, no counter, no warning. +| `abstract.jl:1584–1595` `compile_to_backend(::ZigBackend)` | `!isfile(lib_path)` | `@warn` and returns the *unwrapped* model (no strict option). +| Layer forwards: `abstract.jl:1078–1085` (BatchNorm), `normalization.jl:128–138` (LayerNorm), `:364–372` (RMSNorm), `conv.jl:137` (Conv2d) | *any* exception from the backend | No. Bare `catch end`, diagnostics not incremented. (A segfault is not an exception — the process dies.) +| `abstract.jl:407` `_gpu_forward_with_recovery` | any exception | `@warn` unless suppressed; falls back to CPU unless `AXIOM_GPU_SELF_HEAL=0`. +| `abstract.jl:2754` `_coprocessor_forward_with_recovery` | any exception | as above with `AXIOM_COPROCESSOR_SELF_HEAL`. +| `cuda_available()` (`abstract.jl:1700–1704`; `ext/AxiomCUDAExt.jl:16–20`) | `AXIOM_CUDA_AVAILABLE=1` | Claims availability without a device; `kernel_hooks_loaded` in `gpu_capability_report()` stays `false` — the only tell. +| `SmartBackend` constructor `abstract.jl:166` | `zig_path === nothing` | No. `sb.zig === nothing` silently. +| `MixedPrecisionWrapper` / `precision=:float16` (`abstract.jl:1398–1408`, `1476–1500`) | `setfield!` of a `Matrix{Float16}` into a `Matrix{Float32}` field | `[static]` `setfield!` does not convert → `TypeError` for any parameterised layer; for a `Pipeline`, `parameters()` is empty, so `:mixed` only rounds the *input* to Float16 and computes in Float32 (J-19). +|=== + +== B.5 Verification-status summary + +[cols="2,1,1,1,1"] +|=== +| Backend | Compiles / loads | Correct on tested cases | Correct in general | Claimed status in docs + +| Julia | ✓ | ✓ | ✓ (with two summation orders) | reference +| Zig | ✓ | ✓ for 7 ops at 1 shape each | ✗ (pooling, tanh, batchnorm > 4096, dim, seq_len > 64) | "high-performance … production" (README), "PLANNED" (PROOF-PROGRESS) +| CUDA/ROCm/Metal | ✓ (no hardware here) | unknown | unknown | "production-hardened" (ROADMAP:93) vs "no native GPU acceleration" (REGISTRY-READINESS:47) +| 9 coprocessors | n/a | n/a | n/a | "15 backends" (README:309) vs "type stubs" (REGISTRY-READINESS:51) +|=== diff --git a/docs/investigation/2026-09-26-silicon-core-recon/C-abi-ffi-discrepancies.adoc b/docs/investigation/2026-09-26-silicon-core-recon/C-abi-ffi-discrepancies.adoc new file mode 100644 index 0000000..56e0e94 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/C-abi-ffi-discrepancies.adoc @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += C. ABI / FFI discrepancy report +:toc: + +Method: `nm -D --defined-only zig/zig-out/lib/libaxiom_zig.so | grep ' T axiom_'` +against (a) `@zig_call`/`dlsym` names in `src/backends/zig_ffi.jl` and +`src/backends/abstract.jl`, (b) `ffi/zig/include/axiom.h`, (c) `export fn` in +`ffi/zig/src/main.zig`, (d) `%foreign` declarations in `src/Abi/Foreign.idr`, +(e) numeric claims in the prose documents. `readelf -d` for link dependencies. + +== C.1 Symbol inventory `[empirical]` + +[cols="3,1,4"] +|=== +| Set | Count | Members / notes + +| Exported by the built library | *44* | all `axiom_*` (42 kernels + `axiom_zig_init` + `axiom_zig_version`). +| Called from Julia | 29 | all 29 resolve — *no missing symbol*. +| Exported but never wrapped | 15 | `axiom_add`, `axiom_add_checked`, `axiom_avgpool2d`, `axiom_bmm`, `axiom_fill`, `axiom_flash_attention`, `axiom_flash_attention_checked`, `axiom_mul`, `axiom_mul_checked`, `axiom_relu`, `axiom_relu6`, `axiom_relu6_checked`, `axiom_rotary_embedding`, `axiom_scaled_dot_product_attention`, `axiom_scaled_dot_product_attention_checked`. +| `_checked` variants used by Julia | 2 of 29 | `axiom_matmul_checked`, `axiom_relu_checked` (`zig_ffi.jl:114,138`). All other calls use unchecked kernels — the "checked FFI" guarantee (`test/ci/zig_checked_ffi.jl`) covers two operations. +| Dynamic link dependencies (`NEEDED`) | 0 | The "libc-free" claim is *true*. +| Artifact size | 1,101,096 B | vs "~400KB" (`zig/src/axiom.zig:13`), "320KB" (`TOPOLOGY.adoc:145,158`), "395KB" (`TOPOLOGY.adoc:273`). +|=== + +== C.2 Document vs. reality + +[cols="2,2,3"] +|=== +| Document says | Reality | Location + +| "36 FFI exports, ~400KB compiled .so" | 44 exports, 1.1 MB (ReleaseFast, Zig 0.15.2) | `zig/src/axiom.zig:13` +| "FFI exports (32 syms) … 320KB .so" | as above | `TOPOLOGY.adoc:145–159` +| "36 exports, 395KB .so, SIMD + 4-thread dispatch" | as above (4-thread dispatch is accurate: `MAX_WORKERS = 3` + main) | `TOPOLOGY.adoc:273` +| "`zig/src/axiom.zig` exports the ~36 real `axiom_*` kernels" | 44 | `ABI-FFI-README.adoc:73,100` +| `ffi/zig` "is also concrete (non-template) and internally self-consistent"; "`cd ffi/zig && zig build test`" | `ffi/zig/src/main.zig:55` `export fn Axiom.jl_init()` is a syntax error (`.` in an identifier). The file does not parse under Zig 0.13, 0.14.1 or 0.15.2. Same placeholder at `:74,90,114,136,149,185,199,204,216,247`. `ffi/zig/include/axiom.h` declares 13 generic symbols (`axiom_init`, `axiom_version`, `axiom_create`, …) — none is exported by any buildable artifact. | `ABI-FFI-README.adoc:108–112` +| `src/Abi/Foreign.idr` "specifies the ABI" | It declares the 13 generic lifecycle symbols of the non-compiling tree *plus* `axiom_matmul`, `axiom_relu`, `axiom_conv2d` — 3 of 44 real exports; signatures are not compared with anything in CI. `ABI-FFI-README.adoc` concedes `Verify.*` are `putStrLn` stubs. | `src/Abi/Foreign.idr`, `axiom-abi.ipkg` +| README: "`AXIOM_SMT_RUNNER=zig`" enables a Zig SMT runner | Zero references to `AXIOM_SMT_RUNNER` in `src/`, `ext/`, `zig/`. | `README.adoc:353`, `PROOF-PROGRESS.adoc:57,234` +| README tree: "backends/ — Backend abstraction (15 backends)" | 1 reference + 1 native + 3 extension + 9 stubs + `SmartBackend` | `README.adoc:309` +| Justfile toolchain check: Zig "0.13" | Tree needs ≥ 0.14 (`b.addLibrary` API in `build.zig`; 0.13 fails to build); CI uses 0.15.2; `mise.toml` says `latest` | `Justfile:128`, `mise.toml:7`, `ci.yml:75,105` +| Benchmarks: Zig matmul 512² = 25.6 ms | Wrapper now calls `axiom_matmul_checked`: 284.6 ms here (unchecked kernel: 21.7 ms) | `benchmark/results_2026-02-20_julia-rust-zig.adoc` vs `zig_ffi.jl:114` +|=== + +== C.3 Interface contract gaps (not documentation errors — missing mechanisms) + +. *No ABI version negotiation.* Julia calls `axiom_zig_init` and can read + `axiom_zig_version`, but nothing compares it with an expected value or with + the wrapper's assumptions about argument order/layout. A `.so` from a + different commit with a changed signature would be `ccall`ed with the wrong + arguments. `ZigBackend.lib_path` (`abstract.jl:32`) is never used to load + anything — the global `_zig_lib` from `AXIOM_ZIG_LIB` is (`abstract.jl:2502` + literally passes `ZigBackend("")` as a "dummy path"). +. *Layout contract is implicit.* Some wrappers convert column-major → row-major + (`_to_row_major_vec`, `zig_ffi.jl:79–95`) and some do not (pooling). The Zig + side documents NHWC row-major in comments only. Nothing on either side names + the layout in the symbol, signature, or a descriptor. +. *Error contract is split.* `_checked` kernels return a status code; unchecked + kernels return `void` and cannot report an error — attention kernels + silently return without writing the output for unsupported `seq_len` + (`attention.zig:29,268`). +. *Symbol resolution per call.* `@zig_call` performs `Libdl.dlsym` on every + invocation (`zig_ffi.jl:49–55`). Cheap relative to a kernel, but it means + there is no single place where the set of required symbols is validated at + load time (a missing symbol is discovered on first use). +. *Two FFI trees, one name.* `zig/` (real) and `ffi/zig/` (non-compiling + template) are both described as the Axiom FFI. `ffi/zig/include/axiom.h` + is the only C header in the repository and it describes the wrong tree. +. *No CI check that would have caught any of the above.* `ci.yml` builds and + unit-tests `zig/`, then runs parity for 7 symbols. There is no `nm` + diff against a checked-in symbol list, no header/Idris cross-check, and no + build of `ffi/zig`. + +== C.4 Recommended contract (input to G and H) — minimal + +* One checked-in `zig/ABI.txt` (or JSON) listing `symbol, argument layout, + row/column-major, error contract, since-version`; CI diffs it against + `nm -D`. The Julia side validates all 29 required symbols at load and + records the library's `axiom_zig_version` in the execution report (G). +* Either build `ffi/zig` in CI or delete it and rewrite + `ABI-FFI-README.adoc` and `Foreign.idr` to describe `zig/`. Keeping a + non-compiling tree that documentation calls "self-consistent" is the + highest-leverage documentation fix available. +* Make the layout explicit in wrapper names or a descriptor argument; add + parity tests for every wrapper that touches ≥ 3-D arrays with N>1 and C>1. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/D-numerical-parity-risks.adoc b/docs/investigation/2026-09-26-silicon-core-recon/D-numerical-parity-risks.adoc new file mode 100644 index 0000000..b256048 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/D-numerical-parity-risks.adoc @@ -0,0 +1,225 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += D. Numerical parity risk report +:toc: + +Ordered by (reachability from ordinary use) × (severity). Every item states +whether it was executed (`[empirical]`, script in `repro/`) or read from source +(`[static]`, with a maintainer-runnable Julia check). + +== D.1 Pooling wrappers pass the wrong memory layout `[empirical]` + +*What.* `backend_maxpool2d(::ZigBackend, …)` (`zig_ffi.jl:479–507`) and +`backend_global_avgpool2d(::ZigBackend, …)` (`:513`) hand Julia's +column-major `(N,H,W,C)` buffer straight to `axiom_maxpool2d` / +`axiom_global_avgpool2d`, which index row-major NHWC (`zig/src/pool.zig`). +Every other array wrapper in the file converts with `_to_row_major_vec` +(`:79`); these two do not. + +*Measured* (`repro/layout_probe.py`, simulates exactly what the Julia wrapper +does, compares with correct pooling): + +[cols="2,1,1"] +|=== +| Case | maxpool wrong elements | global-avgpool wrong + +| N=1, 4×4, C=2, k=2 s=2 | 5 / 8 | 2 / 2 +| N=2, 4×4, C=1 | 5 / 8 | 2 / 2 +| N=2, 6×6, C=3 | 49 / 54 | 8 / 8 (any N>1 or C>1) +| N=1, 5×3, C=1, k=2 s=1 | 7 / 8 | — +| N=1, C=1, square | 0 | 0 (the only correct case) +|=== + +Also `[static]`: the maxpool wrapper sizes the output with `padding` but the +export has no padding parameters (`N H_in W_in C kH kW sH sW`), so any +`padding ≠ (0,0)` leaves part of the output buffer uninitialised. + +*Reachability.* `MaxPool2d`/`AvgPool2d` layer `forward` never dispatches to a +backend (`pooling.jl:30–60`), so `Pipeline` inference is unaffected. Direct +`backend_*` calls, `SmartBackend`, `benchmark/benchmarks.jl` and any future +"route pooling to Zig" change are affected. Not covered by +`test/ci/backend_parity.jl`. + +*Maintainer check (Julia):* +[source,julia] +---- +using Axiom; zig = ZigBackend(ENV["AXIOM_ZIG_LIB"]) +x = randn(Float32, 2, 6, 6, 3) +a = Axiom.backend_maxpool2d(zig, x, (2,2), (2,2), (0,0)) +b = Axiom.backend_maxpool2d(JuliaBackend(), x, (2,2), (2,2), (0,0)) +count(a .!= b), maximum(abs.(a .- b)) # expect (≈49, large), not (0, 0) +---- + +== D.2 `tanh` overflows to NaN `[empirical]` + +`activations.zig:103–119` computes `tanh(x) = (e^{2x}−1)/(e^{2x}+1)` in f32. +For `x ≥ 44.5` (and `+Inf`) `e^{2x} = Inf` and the result is `Inf/Inf = NaN`; +Julia's `tanh` returns `1.0`. `gelu` in the same file already uses the +overflow-safe `1 − 2/(e^{2x}+1)` (`:135,144`) — the fix is to use the same +form in `tanh_inplace`/`tanh`. Near zero the formula cancels: relative error +1.3e-3 at `x = 1e-5`, 100 % at `x = 1e-8` (absolute error negligible). +Measured with `repro/activation_probe.py`; `axiom_tanh_inplace` behaves the +same. `gelu`, `sigmoid`, `silu` are fine over the probed range (sigmoid(−100) +flushes a denormal to 0 — harmless). + +*Reachability.* `backend_tanh(::ZigBackend)`, `backend_tanh!`, `SmartBackend` +routing. `Tanh()` layer forward is pure Julia. Not parity-tested (`tanh` is +absent from `backend_parity.jl`). + +== D.3 BatchNorm above 4096 features: wrong values, then SIGSEGV `[empirical]` + +`norm.zig:143` `var inv_std: [4096]f32 = undefined;` indexed by +`num_features` with no bound check. Through the shipped ReleaseFast `.so` +(`repro/batchnorm_probe.py`, B=2): + +[cols="1,2"] +|=== +| `num_features` | result +| 4096 | correct +| 4097 | 2 wrong values (silent) +| 4100 | 8 wrong values (silent) +| 8192, 65536, 1,000,000 | *process killed by SIGSEGV* +|=== + +In Debug/ReleaseSafe it is an index-out-of-bounds panic +(`repro/repro_batchnorm.zig`). + +*Reachability: high.* `forward(bn::BatchNorm, x)` (`abstract.jl:1072–1086`) +calls `backend_batchnorm(backend, …)` for any non-Julia backend in inference +mode with affine parameters — i.e. `set_backend!(ZigBackend(path))` followed +by a `BatchNorm(8192)` in a model *terminates the Julia process*; the +surrounding `try … catch` cannot intercept a segfault. `BatchNorm(4097…8191)` +returns silently wrong numbers for the trailing features. + +== D.4 Different NaN/Inf/edge contracts per backend and per variant `[empirical + static]` + +[cols="2,2,2"] +|=== +| Operation | Julia reference | Zig + +| `matmul` with NaN/Inf input | propagates (BLAS) | `axiom_matmul_checked` → Julia `error(...)` (`zig_ffi.jl:114–130`) +| `relu` with NaN | NaN | `backend_relu` errors (`_checked`); `backend_relu!` (`axiom_relu_inplace`, unchecked) returns NaN — *same op, two contracts on one backend* +| `maxpool2d`, all-`−Inf` window | `−Inf` | `−3.4028235e38` (`floatmax` sentinel) `[empirical]` +| `maxpool2d`, NaN in window | `NaN` (`maximum`/`max` propagate) | `1.0` `[empirical]` (comparison-based max ignores NaN) +| `tanh(x ≥ 44.5)`, `tanh(+Inf)` | `1.0` | `NaN` +| `softmax(dim=1)` on a matrix | normalises along dim 1 | normalises along the last dim regardless (`dim` unused, `zig_ffi.jl:329,351`) `[static]` +| `layernorm` on 3-D input | any `normalized_shape` | wrapper assumes `(batch, hidden)`; `SmartBackend` drops `normalized_shape` (`abstract.jl:215`) `[static]` +| `batchnorm(training=true)` | batch statistics | `training` ignored, running stats used `[static]` +| attention `seq_len > 64` (SDPA) / `> 4096` (flash) | n/a (no Julia wrapper) | silent no-op, output untouched (`attention.zig:29,268`) +| thread spawn failure | n/a | chunk skipped, output stale (`threading.zig:225,268,387` `catch null`) `[static]` +|=== + +A parity test that only feeds `randn` never sees any of these. The +"documented tolerance budgets" (`backend_parity.jl:11–15`) are fine as +tolerances; they are not a contract for edge values. + +== D.5 Precision changes silently on non-reference backends `[static]` + +* Every backend-aware layer forward casts to Float32 before dispatch + (`Float32.(x.data)`, `Float32.(bn.γ)`, … at `abstract.jl:1079`, + `normalization.jl:129–132`, `dense.jl` forward). A `Float64` model on + `ZigBackend`/GPU is computed in Float32 and the result is returned as Float32 + — no warning, no record. +* `precision=:float16` → `convert_precision(::AbstractLayer, Float16)` + (`abstract.jl:1398–1408`) does `setfield!(model, name, Float16.(param))` + into a field typed `Matrix{Float32}` (`Dense{T}` is `mutable struct` with + `weight::Matrix{T}`). `setfield!` does not convert, so this throws + `TypeError` for every parameterised layer. Not covered by + `test/ci/optimization_passes.jl` (which tests `:float32` and `:mixed` only). +* `precision=:mixed` → `MixedPrecisionWrapper` (`:1476–1500`). For a + `Pipeline`, `parameters(::Pipeline)` is the generic `NamedTuple()` + (`layers/abstract.jl:136`) so no weights are converted; the input is + rounded to Float16, then multiplied with Float32 weights → Float32 + arithmetic. The CI drift bound `≤ 5e-2` passes because only the *input* + was rounded. For a single `Dense`, the first `setfield!` throws. There is + also no `try/finally`, so an exception mid-forward would leave a model + permanently converted. + +*Maintainer check:* +[source,julia] +---- +using Axiom +m = Dense(4, 3) +compile(m; backend=JuliaBackend(), precision=:float16, verify=false) # expect TypeError [static prediction] +p = Sequential(Dense(4, 3), ReLU()) +mp = compile(p; backend=JuliaBackend(), precision=:mixed, verify=false) +eltype(mp.model.layers[1].weight) # expect Float32 (never Float16) +---- + +== D.6 The reference backend is not one implementation `[static]` + +`abstract.jl` defines Float32-specialised reference kernels +(`backend_conv2d(::JuliaBackend, ::Array{Float32,4}, …)`, +`backend_avgpool2d` at `:598`, …) and `julia_backend.jl` defines generic-`T` +versions of the same functions. Julia's dispatch picks the Float32 copy for +`Array{Float32}` inputs and the generic copy for everything else. The two +copies accumulate in different orders (e.g. `sum(patch .* kernel)` pairwise vs +an explicit sequential loop; `mean(window)` vs manual accumulation), and the +Float32 `avgpool2d` lacks `count_include_pad`. Consequences: + +* "Parity with the reference" means parity with *whichever* copy dispatch + selected; a Float64 parity test and a Float32 parity test compare against + different code. +* Bit-for-bit reproducibility across dtypes is impossible to promise. + +Recommendation (H, Phase 0): keep *one* generic reference kernel per op with +a documented summation order, and make the Float32 fast paths call it or be +tested against it explicitly. + +== D.7 Aliasing and mutation `[static]` + +* `Base.Array(t::Tensor) = t.data` (`tensor.jl:310`) returns the buffer, not a + copy; `forward(::Dropout)` in inference returns the input tensor itself; + `backend_dropout(…, training=false)` returns `x`. Callers that mutate the + output mutate the input. Document or copy. +* In-place `backend_*!` Zig wrappers mutate Julia arrays through raw pointers; + they are correctly restricted to `Array{Float32}` (contiguous), but the + matching out-of-place wrappers may return the *same* array when Zig is + unavailable (e.g. `backend_dropout`), so "in-place vs out-of-place" is not a + stable distinction across availability states. +* `convert_precision` and `MixedPrecisionWrapper.forward` mutate the user's + model object (see D.5). `compile()` is documented as returning a compiled + model, not as mutating its argument. + +== D.8 GPU extensions `[static]` + +* Availability can be asserted by environment (`AXIOM_CUDA_AVAILABLE=1`, + `abstract.jl:1700–1704` and `ext/AxiomCUDAExt.jl:16–20`) with no device present; nothing later re-checks + `CUDA.functional()` before claiming acceleration. No strict mode exists; + `AXIOM_GPU_REQUIRED` is read only by the test script. +* Host↔device transfer per op (`GPUCompiledModel`): Dense + activation = 4 + transfers per layer; conv2d builds im2col per patch with kernel launches in + a loop. +* `backend_gpu_maxpool2d/avgpool2d` use scalar indexing on device arrays and + are never called from a layer path. +* `batchnorm` ignores `training` (same as Zig). Metal extension accepts + `Float64` (unsupported natively on Metal). +* `test/ci/gpu_hardware_smoke.jl` asserts `acc ≈ cpu`; with self-healing on + (default), a failed GPU op silently falls back and the assertion still + passes. The test cannot prove GPU execution. `gpu_capability_report() + ["kernel_hooks_loaded"]` and the hook-counter override pattern used in + `test/ci/gpu_fallback.jl` are the right building blocks for a real check + (see the verification plan in H). + +== D.9 Edge-shape coverage that does not exist today + +* `batch_size = 5` (chunking underflow, D.4/threading) — never tested. +* `num_features > 4096` — never tested. +* `N > 1` and `C > 1` for pooling — never tested. +* `dim ≠ ndims` for softmax — never tested. +* Zero-size dimensions (`0×n` matmul, empty batch): `axiom_matmul_checked` + pre-pass and the threading thresholds have not been exercised with `n = 0` + `[not verified]`. +* Non-finite inputs for anything but `relu` — never tested. +* Non-default `stride/padding/dilation/groups` for conv2d on Zig — never tested. + +== D.10 Proof layer vs. numerical execution + +Nothing in `verification/`, `dsl/prove.jl`, `proof_export.jl` or the SMT +extension refers to a backend, a kernel, a dtype, or a summation order. The +SMT encoding uses `Real` (`SMTLib.jl:734–736`), so even a genuinely proven +property is a statement about real arithmetic, not about the Float32 kernel +that runs. `verify()`'s structural checks are backend-agnostic by design +(`checker.jl:295`). Empirical `check()` runs on the global backend and stores +no provenance. Conclusion: the proof layer *does not* prove the runtime +implementation, and any certificate produced today is valid for every backend +only because it says nothing about any of them. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/E-memory-performance.adoc b/docs/investigation/2026-09-26-silicon-core-recon/E-memory-performance.adoc new file mode 100644 index 0000000..9ff15aa --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/E-memory-performance.adoc @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += E. Memory / performance report +:toc: + +Time is separated into: *compile/JIT*, *dispatch/wrapper overhead*, +*allocation/copies*, *transfers/sync*, *kernel*. Measurements are +`[empirical]` on a 2-vCPU sandbox (numbers are for ratios, not absolute +performance claims); Julia-side items are `[static]` with the measurement +that would settle them. + +== E.1 Kernel time: the Julia wrapper calls a kernel 9–16× slower than the one that was benchmarked `[empirical]` + +`backend_matmul(::ZigBackend)` always calls `axiom_matmul_checked` +(`zig_ffi.jl:114`), which runs a scalar `O(m·n·k)` finiteness pre-pass before +the tiled SIMD kernel. `repro/matmul_cost.py`, same `.so`, same inputs +(median of repeats): + +[cols="1,1,1,1,1"] +|=== +| size | `axiom_matmul_checked` | `axiom_matmul` | ratio | single-thread numpy/OpenBLAS + +| 64² | 0.311 ms | 0.035 ms | 8.9× | — +| 128² | 2.82 ms | 0.18 ms | 15.7× | — +| 256² | 24.8 ms | 2.17 ms | 11.4× | — +| 512² | 284.6 ms | 21.7 ms | 13.1× | 2.3 ms +|=== + +`benchmark/results_2026-02-20_julia-rust-zig.adoc` reports Zig 512² = +25.6 ms — consistent with the *unchecked* kernel. The published "Zig backend +performance" therefore describes a code path the Julia wrapper no longer +uses. Even unchecked, the kernel is ~10× slower than OpenBLAS at 512², so the +honest positioning of the Zig matmul is "dependency-free", not "fast". + +Algorithmic fix (preferred over any offload): make the finiteness check +`O(m·k + k·n)` on the *inputs* (one vectorised pass each) instead of +`O(m·n·k)` over products, or check the output once. Then the checked and +unchecked kernels cost the same to within noise. + +== E.2 Dispatch overhead per FFI call `[static, cheap to measure]` + +* `@zig_call` does `Libdl.dlsym(_zig_lib[], :sym)` on *every* invocation + (`zig_ffi.jl:49–55`). Cost is ~100 ns–1 µs; it matters for small tensors + (activation of a 128-vector) and it hides missing symbols until first use. + Fix: resolve all 29 symbols once at load into a `NamedTuple` of `Ptr{Cvoid}`. +* Every threaded kernel spawns and joins fresh OS threads per call + (`std.Thread.spawn`, `threading.zig`). Thread creation is ~10–50 µs per + thread; for an op that takes 100 µs this is the dominant cost. The + thresholds (`THREAD_THRESHOLD = 65536` elements, `BATCH_THREAD_THRESHOLD = + 8192`) partly mask it. A persistent pool or single-threaded default with + opt-in threading would be the algorithmic fix; not a priority until + correctness items land. +* Julia layer forward: `current_backend()` global read + `isa` checks per + layer per call — negligible, but see E.5. + +== E.3 Allocations and copies `[static]` + +[cols="3,2"] +|=== +| Site | Copies per call + +| Layer forward on non-Julia backend: `Float32.(x.data)`, `Float32.(bn.γ)`, `Float32.(bn.running_mean)`, … (`abstract.jl:1079–1082`, `normalization.jl:129–132`) | 1 full input copy + 4 parameter copies *even when already Float32* (`Float32.(::Array{Float32})` allocates a new array). +| `_to_row_major_vec` / `_from_row_major_vec` (`zig_ffi.jl:79–95`) | 2 full `permutedims` copies per conv2d/layernorm/softmax call. +| `zig_forward(model::Dense)` etc. `Tensor(y)` re-wraps | 0 extra (wraps), but see E.5 for the type cost. +| `MixedPrecisionWrapper.forward` | converts every parameter to Float16 and back on *every* forward (`abstract.jl:1476–1500`) — allocation proportional to model size per inference (when it does not throw, D.5). +| GPU `GPUCompiledModel` | host→device→host per op: Dense + activation = 4 transfers/layer; `CuArray(x)` + `Array(y)` allocate on both sides. +| Reference `conv2d` Float32 path (`abstract.jl`) | allocates a `patch .* kernel` temporary per output element — `O(N·H_out·W_out·C_out)` small allocations; the generic loop version does not. The *faster* reference path is selected only for non-Float32 inputs (D.6). +| `Dense` forward | `y .+ d.bias'` materialises; fine. +|=== + +Fixes are local and cheap: `convert(Array{Float32}, x)` (no-op if already +Float32) instead of broadcasting; cache row-major weight copies for conv +layers; pre-allocate output buffers for in-place FFI variants. + +== E.4 Transfers and synchronisation + +* Zig path: none (in-process), but all threaded kernels join before return — + no asynchrony, no overlap. Fine. +* GPU path: synchronous `Array(y)` after every op; no streams, no batching of + layers on-device. The design is "call one kernel, come back" rather than + "keep the activation on device". An `on_device` compiled pipeline would + remove 2·(L−1) transfers for an L-layer model. Not recommended before + correctness/provenance work (I). + +== E.5 Compile/JIT time: shape-in-type `[static; measurable in one session]` + +`Tensor(data::Array{T,N}) = Tensor{T,N,Tuple(size(data))}(data)` +(`types/tensor.jl:161`) embeds the *runtime* size in the type parameter. +Every layer `forward` returns `Tensor(y)`, whose type depends on a runtime +value → return types are not inferable → dynamic dispatch at every layer +boundary, and every distinct input shape (batch size, sequence length, +image size) triggers fresh specialisation of every `forward` method it +flows through. Symptoms a user will see: the "first call" penalty recurs for +each new batch size (e.g. the last partial batch of a `DataLoader`), and +`@code_warntype forward(model, x)` is red at each layer. + +Measurement plan (Julia, ~2 minutes): +[source,julia] +---- +using Axiom +m = Sequential(Dense(784,128,relu), Dense(128,10), Softmax()) +for b in (32, 32, 33, 64, 65) # repeated 32 shows warm cost; new sizes show recompile + x = Tensor(randn(Float32, b, 784)) + @time m(x) +end +# and: using SnoopCompileCore; tinf = @snoopi_deep m(Tensor(randn(Float32, 17, 784))) +---- +Expected: each *new* `b` costs tens to hundreds of ms of compilation; repeats +cost microseconds. If confirmed, the design choice needs a documented +"static shape only where declared" policy (`:dynamic` batch dimension by +default in layer outputs) — a core-type decision, *not* a runtime-package +concern. + +== E.6 Where the time actually goes (qualitative budget for a small MLP on Zig backend) + +For `Dense(784,128) → ReLU → Dense(128,10) → Softmax`, batch 32, with +`set_backend!(ZigBackend(path))`: + +. JIT for a new shape (E.5): dominates the first call. +. Two `axiom_matmul_checked` calls: kernel time inflated ~10× by the + pre-pass (E.1). +. `Float32.(x.data)` copy + `dlsym` ×2 + thread spawn (784·32·128 ≈ 3.2 M + products, above the threshold → spawns). +. ReLU and Softmax run in Julia (never dispatched, B.3). + +Without `set_backend!` (the documented `compile(...)` path) the whole model +runs in Julia and the Zig library is loaded but idle. + +== E.7 Recommendations (algorithmic first, in this order) + +. Replace the `O(m·n·k)` finiteness pre-pass with `O(m·k + k·n)` input scans + (or a single output scan) → restores the benchmarked performance without + removing the safety contract. +. Resolve symbols once at load; validate the required set; expose the + library version in the execution report (G). +. Remove redundant `Float32.(…)` copies; cache row-major parameter layouts. +. Decide the `Tensor` shape-in-type policy after measuring E.5. +. Only then consider persistent threads, on-device pipelines, or any + accelerator work. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/F-extraction-recommendation.adoc b/docs/investigation/2026-09-26-silicon-core-recon/F-extraction-recommendation.adoc new file mode 100644 index 0000000..2922ad5 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/F-extraction-recommendation.adoc @@ -0,0 +1,130 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += F. Standalone package decision (SiliconCore.jl / CoprocessorRuntime.jl) +:toc: + +== F.1 What would be extracted, and what must not be + +The candidate runtime package would own: capability detection, device +description, backend selection, strict-vs-fallback policy, diagnostics, +execution provenance, and a small execution protocol. It must *not* contain +models, proof logic, domain science, speculative hardware types without an +execution path, or application policy. + +Applying that filter to Axiom today: + +[cols="3,1,3"] +|=== +| Axiom component | Extractable? | Why + +| Backend type hierarchy (`AbstractBackend`, `JuliaBackend`, `ZigBackend`, GPU types) | yes, *after* redesign | Currently 15 types incl. 9 stubs; the stubs fail the "no speculative hardware types" rule. +| Availability detection (`*_available()`, env overrides) | yes | but env-forced availability must become "requested/forced" state, not "available". +| `SmartBackend` heuristics | no (policy) | Cost model constants are Axiom-specific policy. +| `compile()` + optimisation passes + `MixedPrecisionWrapper` | no | Model-level; belongs with layers. +| GPU/coprocessor compiled-model wrappers, self-healing | partly | The *policy* (strict/fallback) is runtime; the *wrappers* know about `Pipeline` and layers. +| `backend_*` kernel functions (Julia reference + Zig FFI) | not in a "runtime" package | Kernels are a separate concern (Option C). +| Diagnostics counters, capability reports | yes | Already close to standalone. +| Vendored AcceleratorGate | it *is* the previous extraction | See F.2. +|=== + +The honest size of the extractable core, once stubs and policy are removed, is +a few hundred lines (G). That is the same size as `AcceleratorGate.jl`. + +== F.2 The extraction has already been attempted once — and it did not take + +`hyperpolymath/AcceleratorGate.jl` (v0.1.0, MPL-2.0, deps `Dates`+`Libdl`, +unregistered) describes itself as "a small, dependency-light backend-selection +layer … extracted from Axiom.jl's backend module". Axiom carries a copy at +`src/vendored/AcceleratorGateVendored.jl` (494 lines), imports seven symbols +(`abstract.jl:8–10`) and uses exactly one, at `abstract.jl:2277`, behind +`applicable(device_capabilities, backend)` — which is `false` for every Axiom +backend because the two packages define *disjoint* type hierarchies. The +vendored copy is therefore dead code, and Axiom's own selection logic was +never replaced by it. + +This is direct evidence for the failure mode of extracting before the seam +exists: the package was created around *types*, not around an *execution +protocol* that Axiom's layers actually call. Repeating this with a new name +would produce a third hierarchy. + +== F.3 Options compared + +[cols="1,2,2,2"] +|=== +| Option | What it means | For | Against + +| *A — keep everything in Axiom, as is* +| Fix bugs in place; no new interface. +| Zero coordination cost; no external consumers exist (0 open issues; both packages unregistered). +| Leaves the four entanglements (A.5) in place; docs will keep drifting because nothing forces requested/executed backend to be recorded; every fallback stays silent. + +| *B — extract a small runtime package now* +| New `SiliconCore.jl` (or `AcceleratorGate.jl` 0.2) owning types, detection, selection policy, provenance; Axiom depends on it. +| Clean dependency story for a future second consumer; forces the protocol to be written down. +| The protocol does not exist in Axiom yet, so the package would be designed in the abstract — exactly how F.2 happened. Adds registry/versioning/CI overhead for one consumer. Would ship with today's semantics (env-forced availability = "available", silent fallbacks) unless those are fixed first, and fixing them is in-tree work anyway. + +| *C — B plus a separate kernel/FFI package* +| `AxiomKernels.jl` (Zig `.so` + Julia wrappers) and/or a JLL-style artifact. +| Kernel release cadence decoupled from the framework; ABI becomes a versioned contract. +| The ABI is unversioned and undocumented (C.3); 15 exports unused; 4 kernel defects open; a second FFI tree does not compile. Packaging this now would freeze the wrong contract. Artifact building for Zig across platforms is real work with no current user demand. + +| *D — defer; stabilise internal interfaces first* +| Create the runtime seam *inside* Axiom as a submodule with the minimal API (G); route every existing path through it; add strict mode and provenance; fix the confirmed defects with parity tests; measure. Re-evaluate extraction against an explicit exit criterion. +| Does the necessary work either way; produces the evidence the extraction decision needs; no new packages, deps or repos; every step is independently shippable and testable in existing CI. +| Slower to a "clean package boundary" headline; requires discipline to keep the submodule free of model/proof imports (enforce with a test). +|=== + +== F.4 Recommendation + +*Option D now, with a pre-committed exit to Option B.* + +Reasons, in order of weight: + +. *The boundary must be discovered in-tree.* Today layers read a global, + fallbacks happen in six places, and provenance is not recorded anywhere. + Until a single `execute(op, backend; strict)` seam exists and everything + goes through it, there is nothing to extract except types — and F.2 shows + what extracting types alone yields. +. *Correctness debt precedes packaging.* A runtime package's value is the + promise "what it reports is what ran". Shipping that promise on top of + D.1–D.5 (wrong pooling, tanh NaN, segfaulting BatchNorm, env-forced GPU + availability, broken precision paths) would make the promise false on day + one. +. *No consumer pressure.* One consumer, unregistered packages, no issues. + Extraction cost is pure overhead until a second consumer or a release + cadence conflict exists. +. *Evidence is cheap in-tree.* The parity, strict-mode, provenance and ABI + tests (H, Phase 0–1) run in the existing CI with the existing Zig build. + After they exist, the extraction is a mechanical move of one submodule. + +*Exit criterion to Option B* (all must hold): + +* The `Runtime` submodule has had no import from `layers/`, `dsl/`, + `verification/`, `integrations/`, `serving/` for two releases (enforced by + test). +* Every `backend_*` call site in Axiom goes through it (grep-enforced). +* Strict mode, provenance and ABI-version checks are tested in CI, including + a "fallback must be visible" test. +* A second consumer exists *or* the Zig artifact needs a release cadence + different from Axiom's. + +When the exit is taken: publish the submodule as the successor of +`AcceleratorGate.jl` (same author, same purpose) rather than a third name, and +delete `src/vendored/AcceleratorGateVendored.jl`. Kernels (Option C) stay in +Axiom until `zig/ABI.txt` has been stable for two releases. + +== F.5 Answer to "is Axiom.jl doing too much?" + +Yes in inventory (A), but the cost centres are: + +* One 3,069-line file mixing runtime policy, kernels, layer forwards and + compile passes. +* Two Julia reference kernel sets plus Zig, with no single source of truth. +* A verification layer and an execution layer that never mention each other. +* Nine capability stubs presented as backends, which inflate the surface the + runtime must "support". + +Each is fixable by in-tree modularisation (`src/runtime/`, one reference +kernel set, an execution report that certificates can embed, stubs moved +behind an explicit `experimental` flag or removed). None requires a new +repository, and doing them first is what makes an eventual extraction +trivial instead of a rewrite. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/G-api-boundary.adoc b/docs/investigation/2026-09-26-silicon-core-recon/G-api-boundary.adoc new file mode 100644 index 0000000..87ba467 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/G-api-boundary.adoc @@ -0,0 +1,166 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += G. Proposed package / API boundary (design only — not implemented) +:toc: + +Goal: the smallest interface that (1) makes "requested vs. executed" a +first-class, recorded fact, (2) is safe and reproducible by default, (3) can +live as `Axiom.Runtime` today and be moved verbatim into a standalone package +later. Names are proposals. + +== G.1 Design rules + +. *Default is the reference backend.* Nothing accelerates unless asked. +. *Availability is measured, never asserted.* Environment variables may + *request* or *forbid* a backend; they cannot make it available. +. *Strict mode fails; permissive mode records.* `strict=true` throws when the + requested backend cannot execute the op. `strict=false` may fall back — but + the report says so. There is no third mode that falls back silently. +. *One report per execution.* Every call returns (or attaches) an + `ExecutionReport`; `Pipeline` execution aggregates them. +. *No model, proof, or domain types in the module.* Enforced by a test that + the module's transitive `using`/`import` set is `{Base, Libdl, Dates}`. +. *No speculative hardware.* A backend type may exist only if the module can + execute at least one op on it or *detect* it via a real probe (not an env + var). Today that admits `Reference`, `Zig`, `CUDA`, `ROCm`, `Metal`. + +== G.2 Types + +[source,julia] +---- +module Runtime + +abstract type Backend end +struct ReferenceBackend <: Backend end # pure Julia, deterministic order +struct NativeBackend <: Backend; lib::String; end # Zig .so (path is *used*) +struct CUDABackend <: Backend; device::Int; end # provided by extension +struct ROCmBackend <: Backend; device::Int; end +struct MetalBackend <: Backend; device::Int; end + +"Why an op could not run where it was asked to." +@enum Unavailability NotBuilt NotLoaded NoDevice DriverError UnsupportedOp UnsupportedShape UnsupportedDType Forbidden + +struct Capability + backend::Backend + available::Bool + reason::Union{Nothing,Unavailability} + device::Union{Nothing,DeviceIdentity} + kernel_version::Union{Nothing,VersionNumber} # e.g. axiom_zig_version + abi_version::Union{Nothing,VersionNumber} # checked-in ABI contract the wrapper expects + ops::Set{Symbol} # ops this backend can execute here +end + +struct DeviceIdentity + vendor::String; name::String; id::String # e.g. ("NVIDIA","A10G","GPU-uuid"), ("cpu","x86_64","host") + memory_bytes::Union{Nothing,Int} +end + +struct ExecutionReport + op::Symbol + requested::Backend + selected::Backend # after policy + executed::Backend # what actually ran + fallback_used::Bool # executed !== requested + fallback_reason::Union{Nothing,Unavailability} + precision::DataType # element type the kernel computed in + input_precision::DataType # element type the caller supplied + device::DeviceIdentity + kernel_version::Union{Nothing,VersionNumber} + abi_version::Union{Nothing,VersionNumber} + strict::Bool + elapsed_ns::Int + diagnostics::Vector{Diagnostic} # warnings that were *recorded*, never printed by default +end + +struct Diagnostic; level::Symbol; code::Symbol; message::String; end + +end # module +---- + +== G.3 Functions (the whole public surface) + +[source,julia] +---- +# --- discovery ------------------------------------------------------------- +capabilities()::Vector{Capability} # probes; cached; never consults AXIOM_*_AVAILABLE +capability(::Backend)::Capability +reference()::ReferenceBackend + +# --- policy ---------------------------------------------------------------- +struct Policy + requested::Backend + strict::Bool # default: false for ReferenceBackend, true otherwise? -> see G.4 + allow_precision_change::Bool # default false: Float64 in => Float64 out or Unavailable(UnsupportedDType) + forbidden::Set{Type{<:Backend}} +end +Policy(; backend=reference(), strict=..., kwargs...) + +# --- execution ------------------------------------------------------------- +# `f` is a kernel function `f(::Backend, args...)` provided by the host (Axiom's backend_*). +execute(f, policy::Policy, args...)::Tuple{Any, ExecutionReport} + +# The host registers which ops each backend implements; Runtime never defines kernels. +register_op!(::Type{<:Backend}, op::Symbol; dtypes, ndims_range, constraints=nothing) + +# --- provenance ------------------------------------------------------------ +aggregate(reports::Vector{ExecutionReport})::ExecutionSummary # per-op counts, any_fallback, backends_used +fingerprint(summary)::String # stable hash for certificates/metadata +---- + +`ExecutionSummary` is what `compile`/`verify`/certificates embed. It answers +"did anything fall back?", "which kernel versions ran?", "what precision?" +without the caller reconstructing it from logs. + +== G.4 Semantics that resolve today's ambiguities + +[cols="2,3"] +|=== +| Situation | Behaviour + +| `Policy(backend=NativeBackend(path))`, library missing | `strict` defaults to `true` for any non-reference request → `execute` throws `BackendUnavailable(NotLoaded, path)`. With `strict=false`: runs on reference, report has `fallback_used=true`, `fallback_reason=NotLoaded`. +| Env var `AXIOM_CUDA_AVAILABLE=1`, no device | `capability(CUDABackend(0)).available == false` (probe result). The env var is read only by `Policy` defaults as a *request*, never by `capabilities()`. +| Float64 input, backend kernel is Float32-only | Default: `UnsupportedDType` → strict throws / permissive falls back to reference in Float64. With `allow_precision_change=true`: runs in Float32, `report.precision=Float32`, `input_precision=Float64`. +| Op not implemented on backend (e.g. pooling on Zig) | `UnsupportedOp` — reference executes; report says so. Never a bare `try … catch end`. +| Shape outside kernel contract (`num_features > 4096`, `seq_len > 64`, `batch_size == 5` until fixed) | `UnsupportedShape` from `register_op!` constraints *before* the `ccall` — the runtime is where such limits live, not in Zig comments. +| Kernel returns an error code (`_checked`) | Converted to a typed exception with the report attached; not swallowed. +| Requested backend is `ReferenceBackend` | `strict` irrelevant; report still produced (precision, order id). +| Diagnostics | Recorded in the report. Printing is a host decision (`Axiom` may `@warn` once per process for `fallback_used` in permissive mode). No global suppression switch. +|=== + +== G.5 How Axiom would consume it (Phase 1 in H) + +* `set_backend!(b)` becomes `set_policy!(Policy(backend=b, strict=…))`; + `current_backend()` becomes `current_policy()`. Layer forwards call + `execute(backend_matmul, policy, A, B)` instead of `backend_matmul(current_backend(), A, B)` + inside `try … catch`. +* `compile(model; backend, strict=true)` returns a model *bound to a policy* + (no global consulted at forward time). A `compile` on an unavailable strict + backend throws at compile time — which is what the current CI smoke test + believes already happens. +* `Pipeline` forward collects reports; `model(x; report=true)` returns + `(y, summary)`. +* `verify()` / `check()` / `sign_certificate` embed `fingerprint(summary)` + and the summary's `kernel_version`/`abi_version`. A certificate then + states *which* execution it is about. +* `gpu_capability_report()` and the coprocessor `*_capability_report()` + functions become thin views over `capabilities()`. +* `SmartBackend` becomes a `Policy` with a selection function; its cost + heuristics stay in Axiom. + +== G.6 What stays out + +* Coprocessor stubs (TPU/NPU/PPU/MATH/FPGA/DSP/VPU/QPU/CRYPTO): no probe, no + op → not admissible as `Backend` subtypes. If the project wants to keep the + names for roadmap reasons, keep them in Axiom behind + `Axiom.Experimental` with the existing env-var behaviour, clearly outside + the runtime contract. +* Kernel implementations (Julia reference, Zig wrappers, GPU extension + methods) remain in Axiom (Option C deferred). +* `SmartBackend` cost model, `compile` optimisation passes, mixed precision. +* Anything that imports `Tensor`, `AbstractLayer`, `Pipeline`, proof types. + +== G.7 Size estimate + +Types + policy + execute + aggregate + tests: roughly 400–600 lines of Julia, +zero new dependencies (`Libdl` for the native probe, `Dates` for timestamps). +Comparable to `AcceleratorGate.jl`'s current size — which is the point: this +is what that package should have been, defined from the call sites outward. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/H-staged-plan.adoc b/docs/investigation/2026-09-26-silicon-core-recon/H-staged-plan.adoc new file mode 100644 index 0000000..4712e3d --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/H-staged-plan.adoc @@ -0,0 +1,130 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += H. Staged plan (with the verification plan embedded) +:toc: + +Each phase is independently shippable, uses only existing dependencies and +the existing CI Zig build, and has an exit test. Nothing in Phase 0–2 changes +the repository layout beyond adding `src/runtime/` and test files. + +== Phase 0 — Stop the bleeding (correctness, in Axiom) — 1–2 weeks + +Fix the confirmed defects with a parity test for each *before* the fix (red +→ green), so the test suite documents the contract: + +. Zig `norm.zig:143` fixed `[4096]f32` scratch → heap/arena or chunked + computation; add `num_features ∈ {4096, 4097, 8192, 65536}` to + `test/ci/backend_parity.jl` and to `zig build test`. (D.3) +. Zig `activations.zig:103–119` `tanh` → overflow-safe form already used by + `gelu`; add `x ∈ {±1e-8, ±1e-5, ±10, ±44.3, ±44.5, ±50, ±Inf}` for *all* + activations, both in-place and out-of-place. (D.2) +. Zig `threading.zig:392,469,523` chunking → `last_count = batch_size - + min(last_start, batch_size)` or compute chunk bounds with `@min`; add + `batch_size ∈ {1,2,3,4,5,6,7,9,13}` × `hidden ∈ {2048, 65536}` for + layernorm/rmsnorm/softmax in `zig build test` (runs in Debug → would have + panicked). (B.2) +. Julia `zig_ffi.jl` pooling wrappers → `_to_row_major_vec` in/out (or Zig + kernels that accept a layout flag); pass padding or reject `padding ≠ 0`; + add pooling to parity with `N ∈ {1,2}`, `C ∈ {1,3}`, non-square, and the + `−Inf`/NaN window cases with an explicit decision on the contract. (D.1) +. `axiom_matmul_checked` pre-pass → `O(m·k + k·n)` input scans; add a perf + *guard* (not a correctness test) asserting checked/unchecked ratio < 1.5 on + a 512² case. (E.1) +. `backend_softmax/log_softmax(::ZigBackend)` → honour `dim` (permute or + reject with an error). (D.4) +. `precision=:float16` → construct new layers (`Dense{Float16}`) instead of + `setfield!`; `MixedPrecisionWrapper` → `try/finally` or, better, + non-mutating; add a test that asserts the weight `eltype` actually changes. + (D.5) +. `zig_forward(model::Dense)` → apply bias and activation, or delete the + special case. (B.2) +. Delete or build `ffi/zig`; correct `ABI-FFI-README.adoc`, `TOPOLOGY.adoc`, + `zig/src/axiom.zig:13`, `PROOF-PROGRESS.adoc:55,224`, `README.adoc:353` + (`AXIOM_SMT_RUNNER`), `Justfile:128` (Zig version). (C.2) + +*Exit test:* parity job covers every wrapped op (29 symbols) at ≥ 2 shapes, +both dtypes' reference copies, and the edge-value table in D.4; `zig build +test` includes the shapes above; `nm -D` of the built `.so` is diffed against +a checked-in `zig/ABI.txt`. + +== Phase 1 — Build the seam in-tree (`src/runtime/`) — 2–3 weeks + +. Add `Axiom.Runtime` with the types/functions in G (no kernels, no model + types; enforce with a test on the module's import set). +. Implement `capabilities()` from real probes: `Libdl.dlopen` + symbol set + + `axiom_zig_version` for native; extension-provided `CUDA.functional()` etc. + for GPUs; env vars only as *requests*/*forbids*. +. Route the existing call sites through `execute`: Dense, Conv2d, BatchNorm, + LayerNorm, RMSNorm, Dropout forwards; `GPUCompiledModel`; + `CoprocessorCompiledModel` (as `Experimental`, permissive only, report + `fallback_used=true` always). +. Replace the six fallback mechanisms (B.4) with `Policy.strict`; remove the + bare `try … catch end` blocks. +. `compile(model; backend, strict=true)` binds a `Policy` to the returned + model; `compile` on an unavailable strict backend throws. +. `verify`/`check`/certificates/`model_metadata` embed `ExecutionSummary` + fingerprint + kernel/ABI versions. +. Keep `set_backend!`/`current_backend()` as deprecated shims for one + release. + +*Exit tests (all CPU-only, run in ordinary CI):* + +* *Provenance:* `compile(m, backend=ZigBackend(path), strict=false)` without + the library → `summary.any_fallback == true`; with the library → + `false` and `kernel_version` non-`nothing`. Use the hook-counter pattern + from `test/ci/gpu_fallback.jl` to assert the native symbol was called. +* *Strict:* same request with `strict=true` and no library → throws + `BackendUnavailable(NotLoaded)`; never returns a model. +* *No false acceleration:* `AXIOM_CUDA_AVAILABLE=1` without CUDA → + `capability(CUDABackend(0)).available == false`; `compile(m, + backend=CUDABackend(0), strict=true)` throws. +* *Precision:* Float64 input on native backend → `UnsupportedDType` unless + `allow_precision_change=true`, and then `report.precision == Float32`. +* *Runtime smoke honesty:* `test/ci/runtime_smoke.jl` "accelerated" case + asserts `summary.backends_used == {NativeBackend}` — the test that today + cannot fail becomes one that can. + +== Phase 2 — Evidence gate — 1 week, then ongoing + +. Measure E.5 (shape-in-type recompilation) and decide the `Tensor` policy; + this is core-type work and is *not* blocked on the runtime. +. Publish a corrected benchmark table (checked kernel, current wrapper, + OpenBLAS baseline) and mark the 2026-02-20 results superseded. +. Hardware CI (unchanged infrastructure): make `gpu_hardware_smoke.jl` + assert `summary.backends_used == {CUDABackend}` and + `kernel_hooks_loaded == true`; populate + `benchmark/gpu_performance_baseline.json` from a real run or delete the + file. Hardware tests stay behind `AXIOM_ENABLE_GPU_HARDWARE_CI`, separate + from correctness CI. +. Re-read every doc claim in C.2 against `capabilities()` output; where docs + describe a backend, link the parity job that proves it. + +*Exit:* two consecutive releases with the Phase 1 tests green and no new +`backend_*` call outside `Runtime.execute` (grep test). + +== Phase 3 — Conditional extraction (only if F.4's exit criterion holds) + +. Move `src/runtime/` to a package that *supersedes* `AcceleratorGate.jl` + (same author, same purpose; bump to 0.2 or rename once — not a third + package). Axiom adds it as a dependency; delete + `src/vendored/AcceleratorGateVendored.jl`. +. Kernels stay in Axiom until `zig/ABI.txt` has been unchanged for two + releases; then Option C can be evaluated with an artifact build plan. + +== Verification plan summary (what proves what) + +[cols="2,3,1"] +|=== +| Property | Test | Runs where + +| Exact small-case parity | Hand-computed 2×2/3×3 expected values per op, per backend (not only reference-vs-backend `isapprox`) | CI +| Tolerance parity | Existing `backend_parity.jl` budgets, extended to all 29 wrapped ops, ≥ 2 shapes, both dtypes | CI +| Shape/order | `dim ∈ {1,2}` softmax; `N,C > 1` pooling; non-square; odd batch (5); `stride/padding/dilation/groups ≠ default` conv | CI +| Zero/NaN/Inf/overflow | D.4 table as a data-driven test; each cell has a decided contract | CI +| Aliasing/mutation | `x_before == x_after` for every out-of-place op; `compile` does not mutate its argument; `Array(t)` documented | CI +| CPU fallback | Permissive policy without library → `fallback_used`; strict → throws | CI +| No false acceleration | Env-forced availability never yields `available=true` | CI +| ABI symbols | `nm -D` vs `zig/ABI.txt`; Julia load validates all required symbols and version | CI +| Provenance | `ExecutionSummary` fingerprint present in certificate/metadata; changes when backend changes | CI +| Hardware | `gpu_hardware_smoke.jl` with `backends_used` assertion | self-hosted, opt-in +| Performance | Ratio guards (checked/unchecked < 1.5; wrapper overhead < X µs) marked `@test_broken`-tolerant to noise; never mixed with correctness assertions | nightly / opt-in +|=== diff --git a/docs/investigation/2026-09-26-silicon-core-recon/I-not-recommended.adoc b/docs/investigation/2026-09-26-silicon-core-recon/I-not-recommended.adoc new file mode 100644 index 0000000..fd37d4f --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/I-not-recommended.adoc @@ -0,0 +1,49 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += I. Changes explicitly NOT recommended (and why) + +[cols="2,4"] +|=== +| Not recommended | Reason grounded in this investigation + +| *Splitting the repository or creating `SiliconCore.jl` / `CoprocessorRuntime.jl` now* +| The runtime seam does not exist inside Axiom yet (A.5, F.4). The one previous extraction (`AcceleratorGate.jl`) is vendored back as dead code with a disjoint type hierarchy (F.2). Extract after Phase 1–2, as a successor of that package. + +| *A separate kernel/FFI package (Option C)* +| ABI is unversioned, 15 of 44 exports unused, four kernel defects open, second FFI tree does not compile (C). Packaging freezes the wrong contract. + +| *Adding GPU, KernelAbstractions, TPU/NPU or any accelerator dependency* +| No hardware evidence exists for the GPU paths that are already present; adding more surface increases the claim/reality gap. `KernelAbstractions` is already an unused weak dependency — remove it or use it, do not add more. + +| *Promoting the nine coprocessor types into a runtime package or its documentation as "supported"* +| They have no execution path and no real probe (B.1). Keep in `Axiom.Experimental` or delete. Naming AVX-512 and AES-NI "coprocessors" should be dropped. + +| *Replacing the Julia reference kernels with Zig/GPU implementations, or making a non-reference backend the default* +| Parity coverage is 7 ops at one shape; three of the untested ops are wrong (D). The reference must stay the default until the Phase 0 exit test passes — and even then, "default = reference" is a design rule (G.1). + +| *Merging the two Julia reference copies by deleting one without tests* +| Which copy runs depends on dtype (D.6). First pin the summation order with tests, then unify. + +| *Removing the `_checked` matmul to recover performance* +| The finiteness contract is a documented feature (`test/ci/zig_checked_ffi.jl`). Fix the algorithmic cost of the check (E.1) instead. + +| *Suppressing warnings globally (e.g. a `AXIOM_QUIET` switch) to make fallback noise go away* +| Fallbacks must become *recorded* (G.4), not silent. A global suppressor would make the current silent-downgrade problem permanent. + +| *Adding a "soft strict" mode that downgrades with a warning* +| That is today's behaviour. Two modes only: strict throws; permissive records. + +| *Rewriting `backends/abstract.jl` wholesale in the first phase* +| 3,069 lines with the only tests being the ones that exist; a rewrite would invalidate them. Phase 1 routes call sites through the seam incrementally. + +| *On-device pipelines, persistent thread pools, async transfers* +| Real improvements (E.4, E.2), but they optimise paths whose correctness and provenance are not yet established. Sequence after Phase 1. + +| *Opening PRs from documentation review alone* +| Every issue in J that is `[static]` carries a maintainer-runnable check; open issues (not PRs) for those until the check has been run in Julia. + +| *Trusting `test/ci/runtime_smoke.jl` "accelerated" or `gpu_hardware_smoke.jl` as evidence of acceleration* +| Both pass on CPU fallback by construction (B.3, D.8). Fix the tests in Phase 1/2 before citing them. + +| *Changing the `Tensor{T,N,Shape}` design in the runtime work* +| Shape-in-type (E.5) is a core-type decision with wide blast radius; measure first, decide separately. +|=== diff --git a/docs/investigation/2026-09-26-silicon-core-recon/J-upstream-issues.adoc b/docs/investigation/2026-09-26-silicon-core-recon/J-upstream-issues.adoc new file mode 100644 index 0000000..c2e6ec0 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/J-upstream-issues.adoc @@ -0,0 +1,255 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += J. Upstream issues with evidence and minimal reproductions +:toc: +:toclevels: 2 + +Buckets: *FIX-IN-AXIOM* (in-tree, now), *FUTURE-STANDALONE* (belongs to the +runtime seam of G; implement in-tree in Phase 1, extract later), +*NOT-YET-VERIFIED* (static reading of Julia source; check provided — open as +an issue, not a PR, until run). Evidence: `[E]` empirical here, `[S]` static. + +Severity: *Critical* = crash or wrong results on an ordinary path; *High* = +wrong results / false claim on a documented path or major perf regression; +*Medium* = wrong results on a direct-API path, or a broken documented feature; +*Low* = doc/hygiene. + +== J.1 Index + +[cols="1,4,1,1,2"] +|=== +| ID | Title | Sev | Ev | Bucket + +| J-01 | Zig `batchnorm` wrong above 4096 features, SIGSEGV from 8192 — reachable from `BatchNorm.forward` | Critical | E | FIX-IN-AXIOM +| J-02 | Zig pooling wrappers pass column-major memory to row-major kernels → wrong values | High | E | FIX-IN-AXIOM +| J-03 | Zig `tanh`/`tanh_inplace` return NaN for x ≥ 44.5 and +Inf | High | E | FIX-IN-AXIOM +| J-04 | Chunking underflow at `batch_size = 5` in `parallel_layernorm/rmsnorm/batch` (UB; panics in safe builds) | Medium | E | FIX-IN-AXIOM +| J-05 | `axiom_matmul_checked` pre-pass is O(m·n·k): 9–16× slower than the benchmarked kernel | High | E | FIX-IN-AXIOM +| J-06 | Zig `maxpool2d` wrapper sizes output with padding but the export has no padding args | Medium | S | FIX-IN-AXIOM +| J-07 | Pooling edge contracts differ: all-`−Inf` → `−floatmax`, NaN window → `1.0` | Low | E | FIX-IN-AXIOM +| J-08 | Documented production path `compile(model, backend=ZigBackend(path))` runs pure Julia; CI "accelerated" smoke cannot detect it | High | S | FIX-IN-AXIOM +| J-09 | Every Zig wrapper silently returns the Julia result when the library is unavailable; no strict mode for Zig | High | S | FUTURE-STANDALONE +| J-10 | `AXIOM_CUDA_AVAILABLE=1` asserts GPU availability without a device; no GPU strict mode; `AXIOM_GPU_REQUIRED` unread by the library | High | S | FUTURE-STANDALONE +| J-11 | `gpu_hardware_smoke.jl` passes on CPU fallback (`acc ≈ cpu`), so it cannot evidence GPU execution | Medium | S | FIX-IN-AXIOM +| J-12 | `backend_softmax/log_softmax(::ZigBackend)` ignore `dim` | Medium | S | FIX-IN-AXIOM +| J-13 | `SmartBackend` layernorm drops `normalized_shape`; Zig layernorm wrapper assumes 2-D `(batch, hidden)` | Medium | S | FIX-IN-AXIOM +| J-14 | `training` flag ignored by Zig and GPU `batchnorm` | Medium | S | FIX-IN-AXIOM +| J-15 | Attention kernels silently no-op for `seq_len > 64` (SDPA) / `> 4096` (flash) | Medium | S | FIX-IN-AXIOM +| J-16 | `std.Thread.spawn … catch null` — a failed spawn leaves that chunk uncomputed | Medium | S | NOT-YET-VERIFIED +| J-17 | `zig_forward(model::Dense)` drops bias and activation | Medium | S | FIX-IN-AXIOM +| J-18 | `precision=:float16` → `setfield!` `TypeError` on any parameterised layer | High | S | NOT-YET-VERIFIED +| J-19 | `precision=:mixed` never computes in Float16 for a `Pipeline`; wrapper mutates the model without `try/finally` | Medium | S | NOT-YET-VERIFIED +| J-20 | Two Julia reference kernel sets with different summation order, selected by dtype; Float32 `avgpool2d` lacks `count_include_pad` | Medium | S | FIX-IN-AXIOM +| J-21 | Bare `try … catch end` fallbacks in layer forwards; diagnostics not incremented | Medium | S | FIX-IN-AXIOM +| J-22 | `ZigBackend.lib_path` unused; global library from `AXIOM_ZIG_LIB`; `ZigBackend("")` "dummy path" | Low | S | FIX-IN-AXIOM +| J-23 | `dlsym` per call; no load-time symbol/ABI-version validation | Medium | S | FUTURE-STANDALONE +| J-24 | Redundant `Float32.(…)` copies of inputs and parameters on every backend-aware forward | Low | S | FIX-IN-AXIOM +| J-25 | Vendored `AcceleratorGate` is dead code (disjoint type hierarchy; one guarded call site) | Low | S | FUTURE-STANDALONE +| J-26 | `KernelAbstractions` is a weak dependency with no extension and no reference | Low | S | FIX-IN-AXIOM +| J-27 | `AxiomPyTorchExt` defines `from_pytorch(::String)` which shadows core `from_pytorch(::AbstractString; strict)` when PyCall+torch load | Medium | S | NOT-YET-VERIFIED +| J-28 | `Tensor(data)` embeds runtime size in the type → per-shape recompilation and type-unstable forwards | Medium | S | NOT-YET-VERIFIED +| J-29 | `backend_flatten` is only correct for `start_dim == 2` (`reshape(x, size(x,1), prod(size(x)[start_dim:end]))`); `backend_dropout(training=false)` returns the input array itself | Low | S | FIX-IN-AXIOM +| J-30 | In-place `backend_relu!` uses the unchecked `axiom_relu_inplace` while `backend_relu` uses `axiom_relu_checked` — one op, two NaN contracts on one backend | Low | S | FIX-IN-AXIOM +| J-31 | Export count/size claims wrong everywhere (32/36 vs 44; 320/395/400 KB vs 1.1 MB) | Low | E | FIX-IN-AXIOM +| J-32 | `ABI-FFI-README.adoc` says `ffi/zig` is "concrete … internally self-consistent" and `zig build test` works; it does not parse | Medium | E | FIX-IN-AXIOM +| J-33 | `AXIOM_SMT_RUNNER=zig` documented; zero code references | Low | S | FIX-IN-AXIOM +| J-34 | Docs contradict each other on backend status (PROOF-PROGRESS "planned" vs ROADMAP "production-hardened" vs REGISTRY-READINESS "type stubs") | Low | S | FIX-IN-AXIOM +| J-35 | Published benchmarks measured the unchecked kernel and cite a Rust backend that is not in the tree | Medium | E | FIX-IN-AXIOM +| J-36 | Toolchain pins disagree (Justfile Zig 0.13 / mise latest / CI 0.15.2 / build.zig needs ≥ 0.14, no minimum declared) | Low | S | FIX-IN-AXIOM +| J-37 | README "15 backends" | Low | S | FIX-IN-AXIOM +| J-38 | Proof/certificate layer records no backend, kernel or ABI provenance; SMT proves over `Real` and never encodes the model | Medium | S | FUTURE-STANDALONE +| J-39 | `src/Abi/Foreign.idr` covers 3 of 44 real exports plus 13 symbols of the non-compiling tree; nothing checks it | Low | S | FIX-IN-AXIOM +| J-40 | 62 `AXIOM_*` env vars with no schema; strict mode spelt three different ways | Low | S | FUTURE-STANDALONE +|=== + +== J.2 Detailed entries (evidence + reproduction) + +All commands assume the library was built as CI does: +`cd zig && zig build -Doptimize=ReleaseFast` (Zig 0.15.2) and that `numpy` +is importable. Zig test reproductions compile against the repository's +`zig/src` tree directly. Paths are relative to `docs/investigation/2026-09-26-silicon-core-recon/repro/`. + +=== J-01 Zig `batchnorm` above 4096 features `[E]` — Critical + +* *Where:* `zig/src/norm.zig:143` `var inv_std: [4096]f32 = undefined;` indexed by `num_features`. +* *Reach:* `abstract.jl:1072–1086` `forward(bn::BatchNorm, x)` → `backend_batchnorm(::ZigBackend, …)` (`zig_ffi.jl:536`) whenever the current backend is not `JuliaBackend`, `!bn.training`, `bn.affine`. +* *Observed (shipped `.so`):* 4096 correct; 4097 → 2 wrong; 4100 → 8 wrong; 8192 / 65536 / 1e6 → SIGSEGV. +* *Repro:* `python3 batchnorm_probe.py ../../../../zig/zig-out/lib/libaxiom_zig.so`; Zig-level: `zig test --dep axiom -Mroot=repro_batchnorm.zig -Maxiom=../../../../zig/src/axiom.zig -OReleaseSafe` → index out of bounds panic. +* *Julia confirmation:* `set_backend!(ZigBackend(lib)); m = Sequential(Dense(4, 8192), BatchNorm(8192)); m(Tensor(randn(Float32, 2, 4)))` — expected: process terminates. +* *Fix:* allocate `inv_std` per call (arena/heap) or compute per feature without the scratch; add `num_features ∈ {4096, 4097, 8192, 65536}` to `zig build test` and `backend_parity.jl`. + +=== J-02 Pooling wrappers: wrong layout `[E]` — High + +* *Where:* `src/backends/zig_ffi.jl:479–507` (`backend_maxpool2d`), `:513` (`backend_global_avgpool2d`) pass `input` directly; compare `_to_row_major_vec` use in conv/layernorm/softmax wrappers (`:79–95`). Kernels index row-major NHWC (`zig/src/pool.zig`). +* *Observed:* maxpool wrong 5/8 (N=1,4×4,C=2), 5/8 (N=2,C=1), 49/54 (N=2,6×6,C=3), 7/8 (N=1,5×3,C=1,k=2,s=1); global-avgpool wrong for any N>1 or C>1; only N=1,C=1,square is correct. +* *Repro:* `python3 layout_probe.py ../../../../zig/zig-out/lib/libaxiom_zig.so`. +* *Julia confirmation:* see D.1. +* *Reach:* direct API, `SmartBackend`, `benchmark/benchmarks.jl`; not `MaxPool2d.forward` (pure Julia). Not parity-tested. + +=== J-03 Zig `tanh` NaN overflow `[E]` — High + +* *Where:* `zig/src/activations.zig:103–119` `(e^{2x}−1)/(e^{2x}+1)`; `gelu` at `:135,144` already uses `1 − 2/(e^{2x}+1)`. +* *Observed:* `axiom_tanh(44.5) = NaN`, `(45) = NaN`, `(50) = NaN`, `(100) = NaN`, `(+Inf) = NaN`; `(44.3) = 1.0`. Near zero: rel. err 1.3e-3 at 1e-5, 100 % at 1e-8. `gelu`, `sigmoid`, `silu` fine. +* *Repro:* `python3 activation_probe.py ../../../../zig/zig-out/lib/libaxiom_zig.so`. +* *Reach:* `backend_tanh(::ZigBackend)`, `backend_tanh!`, `SmartBackend`. `tanh` absent from `backend_parity.jl`. + +=== J-04 Chunking underflow at `batch_size = 5` `[E]` — Medium (UB) + +* *Where:* `zig/src/threading.zig:392` (`parallel_layernorm`), `:469` (`parallel_rmsnorm`), `:523` (`parallel_batch`, used by batched softmax): `last_start = (num_threads−1)·chunk`, `last_count = batch_size − last_start` with `chunk = ceil(batch/num_threads)`, `num_threads = min(4, batch)`. For `batch = 5`: `chunk = 2`, `last_start = 6 > 5` → usize wrap. Reached when `total ≥ 8192` and `batch ≥ 4` (`:294–324`). +* *Observed:* Debug/ReleaseSafe: `panic: integer overflow` at `threading.zig:392`. `zig test -OReleaseFast` binary: *segfault*. Shipped `.so` (ReleaseFast): B=5 × {2048, 4096, 65536} correct with an intact canary after the output — LLVM's treatment of the UB happened to be benign in that compilation unit. It is undefined behaviour and build-dependent. +* *Repro:* `zig test -OReleaseSafe --dep axiom -Mroot=repro_underflow_canary.zig -Maxiom=../../../../zig/src/threading.zig` (panic); `-OReleaseFast` (crash); `python3 canary_probe.py …libaxiom_zig.so` (benign through the `.so`); `python3 chunking_probe.py …` (B = 4…17 through the `.so`). +* *Fix:* `last_count = batch_size -| last_start` (saturating) or derive per-thread ranges with `@min(start + chunk, batch_size)` as the element-wise `parallel_unary` already does (`:219`). Add B ∈ {1,…,9,13} to `zig build test` (Debug would have caught it). + +=== J-05 `axiom_matmul_checked` cost `[E]` — High (performance / claim) + +* *Where:* `zig_ffi.jl:114` always calls `axiom_matmul_checked`; `zig/src/axiom.zig:101` pre-pass over `m·n·k` products. +* *Observed:* checked vs unchecked: 0.311/0.035 ms (64²), 2.82/0.18 (128²), 24.8/2.17 (256²), 284.6/21.7 (512²). Single-thread OpenBLAS 512² = 2.3 ms. `benchmark/results_2026-02-20…` reports 25.6 ms at 512² — the unchecked kernel. +* *Repro:* `python3 matmul_cost.py ../../../../zig/zig-out/lib/libaxiom_zig.so`. +* *Fix:* check inputs in O(m·k + k·n) (vectorised `isfinite` scans) or the output once; keep the error contract; re-run the benchmark table. + +=== J-06 `maxpool2d` padding not passed `[S]` — Medium + +`zig_ffi.jl:495–496` computes `H_out/W_out` with `pH/pW`, allocates that +size, but `axiom_maxpool2d` receives only `N H_in W_in C kH kW sH sW`. With +`padding ≠ (0,0)` part of the output is never written. Fix together with J-02 +(reject padding or implement it in the kernel). + +=== J-08 Documented production path runs Julia `[S]` — High + +* *Chain:* `compile(model, backend=ZigBackend(path))` → `compile_to_backend(::ZigBackend)` (`abstract.jl:1584`) → `ZigCompiledModel` (`:2460`) → `zig_forward(model::Pipeline, …)` → `forward(pipeline, x)` → layers call `current_backend()` (global, still `JuliaBackend()`). +* *CI:* `test/ci/runtime_smoke.jl:67–79` does exactly this and never calls `set_backend!`; the assertions are shape/finiteness only. +* *Check:* with the library loaded, wrap `Axiom.backend_matmul(::ZigBackend, …)` with a counter (pattern in `test/ci/gpu_fallback.jl`), run the README production snippet, observe count 0. +* *Fix:* Phase 1 (policy bound at `compile`); interim: make `compile_to_backend(::ZigBackend)` call `set_backend!` or document that it does not. + +=== J-09 / J-10 Silent fallback and asserted availability `[S]` — High (runtime seam) + +* `zig_ffi.jl:51,102` and every wrapper: `if !zig_available() return (…)`. No counter, no warning, no strict option. `test/ci/backend_parity.jl:23` errors if unavailable — the *test* has a strict mode the library lacks. +* `abstract.jl:1700–1704` and `ext/AxiomCUDAExt.jl:16–20`: `_backend_env_available("AXIOM_CUDA_AVAILABLE")` is returned *before* `CUDA.functional()` is consulted, even with the extension loaded (`gpu_hooks.jl:77–81` does the same for the device count). `AXIOM_GPU_REQUIRED` appears only in `test/ci/gpu_hardware_smoke.jl:42` and `scripts/gpu-performance-evidence.jl:119`. +* *Design:* G.4. Interim: make `compile(…, backend=…)` error if `capability(backend).available == false` and add `AXIOM_ZIG_REQUIRED` with the same semantics as the coprocessor `_REQUIRED` flags. + +=== J-11 Hardware smoke cannot prove GPU execution `[S]` — Medium + +`gpu_hardware_smoke.jl:52–64`: `compiled = compile(model, backend=target, verify=false, optimize=:none)`; asserts `acc ≈ cpu`. `_gpu_forward_with_recovery` (`abstract.jl:407`) falls back to CPU on any error by default, so the assertion passes either way. Add `gpu_capability_report()["kernel_hooks_loaded"] == true` and a hook-call counter, and set `AXIOM_GPU_SELF_HEAL=0` in that job. + +=== J-12 `dim` ignored `[S]` — Medium + +`zig_ffi.jl:329` `backend_softmax(::ZigBackend, x, dim)` and `:351` `log_softmax` compute over the last dimension of the row-major copy regardless of `dim`. `SmartBackend.backend_softmax` (`abstract.jl:200`) forwards `dim`. Check: `backend_softmax(zig, randn(Float32, 3, 4), 1)` vs `JuliaBackend` — columns vs rows. + +=== J-13 / J-14 / J-15 / J-17 Contract gaps `[S]` + +* `abstract.jl:215` `backend_layernorm(sb::SmartBackend, …, nshape, eps)` calls the Zig 5-arg form without `nshape`; the Zig wrapper (`zig_ffi.jl:573`) treats `size(x, 2)` as hidden. `LayerNorm((B, H))` semantics differ. +* `zig_ffi.jl:536–545` accepts `training::Bool` and ignores it; GPU hooks likewise. +* `zig/src/attention.zig:29,268` early-return without writing output or signalling. No Julia wrapper today; the export exists. +* `abstract.jl:2495–2502` `zig_forward(model::Dense, x, lib_handle)` → + `backend_matmul(ZigBackend(""), x, model.weight)` only: no bias, no + activation, `x` is passed as a `Tensor` although the Zig method takes + `Matrix{Float32}` (→ `MethodError` `[static]`), and the result is a raw + matrix. `ZigCompiledModel` (`:2460–2480`) `dlopen`s `backend.lib_path` into + `lib_handle` but only uses it for a `dlsym` presence check — execution goes + through the global `_zig_lib` loaded from `AXIOM_ZIG_LIB`, which may be a + different file or absent. For a `Pipeline` the generic + `zig_forward(model, x, _) = forward(model, x)` (`:2481–2483`) runs pure + Julia (J-08). + +=== J-16 Thread spawn failure `[S]` — NOT-YET-VERIFIED + +`threading.zig:225,268,387` `}) catch null;` then the join loop skips `null` +handles. The chunk for that thread is never computed; the output buffer +retains previous contents. Could not be forced in this sandbox (would need +`RLIMIT_NPROC`/`ulimit -u` low enough during the call). Fix: on spawn failure +run the chunk inline on the calling thread. + +=== J-18 / J-19 Precision paths `[S]` — NOT-YET-VERIFIED (High / Medium) + +* `abstract.jl:1398–1408` `convert_precision(::AbstractLayer, T)`: + `setfield!(model, name, converted)` where `Dense{Float32}` has + `weight::Matrix{Float32}`; `setfield!` does not `convert` → `TypeError`. + Not covered by `test/ci/optimization_passes.jl` (tests `:float32`, `:mixed`). +* `abstract.jl:1476–1500` `forward(::MixedPrecisionWrapper)`: for a + `Pipeline`, `parameters()` is `NamedTuple()` (`layers/abstract.jl:136`, no + `Pipeline` method), so only the input is rounded; for a bare `Dense` the + first `setfield!` throws. No `try/finally`. +* *Check:* D.5 snippet. + +=== J-20 Two reference kernel sets `[S]` — Medium + +`abstract.jl` Float32-specialised `backend_conv2d/avgpool2d/maxpool2d/…` vs +`julia_backend.jl` generic `T`. Dispatch picks by dtype; summation orders +differ; Float32 `avgpool2d` (`abstract.jl:598`) has no `count_include_pad`. +Check: compare `backend_conv2d(JuliaBackend(), Float32 arrays…)` with the +same call on `Float64.(…)` converted back — differences beyond Float32 +rounding indicate order differences; more directly, `@which` shows two +methods in two files. + +=== J-21 Bare `try … catch end` `[S]` — Medium + +`abstract.jl:1078–1085`, `normalization.jl:128–138`, `:364–372`, +`conv.jl:137`. Any exception (including a genuine bug in a kernel wrapper) +becomes a silent CPU result. Diagnostics counters in `abstract.jl` are not +incremented from these sites. + +=== J-27 `from_pytorch` shadowing `[S]` — NOT-YET-VERIFIED + +`integrations/interop.jl:348` `from_pytorch(path::AbstractString; strict)` +(JSON descriptor); `ext/AxiomPyTorchExt.jl:39` `Axiom.from_pytorch(model_path::String)` +(`torch.load`). For a `String` argument the extension method is more specific, +so loading PyCall + torch changes what `from_pytorch("model.json")` does, and +`from_pytorch(path; strict=false)` raises a keyword-argument `MethodError`. +Check: `using PyCall, Axiom; methods(Axiom.from_pytorch)`; call with a JSON +descriptor path. + +=== J-28 Shape-in-type recompilation `[S]` — NOT-YET-VERIFIED + +`types/tensor.jl:161`. Measurement in E.5. + +=== J-29 / J-30 Small API contract gaps `[S]` — Low + +* `julia_backend.jl:372–376` `backend_flatten(_, x, start_dim)` reshapes to + `(size(x,1), prod(size(x)[start_dim:end]))`; for `start_dim ≠ 2` on a + 4-D input this is a `DimensionMismatch` (or silently wrong when a middle + dimension is 1). `julia_backend.jl:378–380` returns `x` itself when + `!training`. +* `zig_ffi.jl:138` `backend_relu` → `axiom_relu_checked` (errors on NaN; + tested in `backend_parity.jl:49`); `backend_relu!` → `axiom_relu_inplace` + (unchecked, propagates NaN). Decide one contract per op. + +=== J-31 / J-32 / J-35 Documentation vs artifacts `[E]` + +* `nm -D --defined-only zig/zig-out/lib/libaxiom_zig.so | grep -c ' T axiom_'` → 44; `stat -c %s` → 1,101,096. Claims at `zig/src/axiom.zig:13`, `TOPOLOGY.adoc:145–159,273`, `ABI-FFI-README.adoc:16,73,100`. +* `cd ffi/zig && zig build` → `src/main.zig:55:16: error` (`export fn Axiom.jl_init()`); same token at `:74,90,114,136,149,185,199,204,216,247`. Claim at `ABI-FFI-README.adoc:108–112`. +* Benchmarks: J-05 numbers; `benchmark/results_2026-02-20_julia-rust-zig.adoc` and `ROADMAP.adoc:25` mention a Rust backend absent from the tree. + +=== J-33 / J-34 / J-36 / J-37 / J-39 Documentation hygiene `[S]` + +* `grep -rn AXIOM_SMT_RUNNER src ext zig` → none; `README.adoc:353`, `PROOF-PROGRESS.adoc:57,234`. +* `PROOF-PROGRESS.adoc:55,224` "Zig backend PLANNED / not yet wired" vs `README.adoc:123` "Production path: optional Zig backend" vs `ROADMAP.adoc:93` "Production-hardened GPU paths" vs `REGISTRY-READINESS.adoc:47–54`. +* `Justfile:128` Zig "0.13"; `mise.toml:7` `latest`; `ci.yml:75,105` `0.15.2`; `zig/build.zig` uses `b.addLibrary` (≥ 0.14) with no declared minimum — Zig 0.13 fails to build. +* `README.adoc:309` "15 backends". +* `src/Abi/Foreign.idr` vs `nm -D`. + +=== J-38 Provenance and the proof layer `[S]` — Medium (design) + +No struct in `verification/`, `proof_export.jl`, `model_metadata.jl` carries +backend, kernel version, ABI version, dtype or summation order. +`ext/AxiomSMTExt.jl` declares variables as `Real` (`SMTLib.jl:734–736`) and +contains no reference to weights or layers; `checker.jl:295` +`ValidProbabilities ⇔ last_layer isa Softmax`. The certificate therefore +cannot distinguish "verified on reference" from "verified on Zig with the +J-01 defect". Design: G.5 (embed `ExecutionSummary` fingerprint). + +=== J-40 Configuration surface `[S]` — Low + +`grep -rhoE 'AXIOM_[A-Z0-9_]+' src ext | sort -u | wc -l` → 62. Strict mode is +`AXIOM__REQUIRED` (coprocessors), `AXIOM_GPU_SELF_HEAL=0` (GPUs, runtime +errors only), and absent for Zig. One documented schema and one spelling +(`Policy.strict`) — G. + +== J.3 Suggested issue order + +. J-01 (crash), J-02, J-03 (wrong values) — one issue each with the repro + script attached; fixes are local and small. +. J-05 + J-35 together (performance claim vs. current wrapper). +. J-08 + J-09 + J-10 + J-11 as one "requested vs executed backend" epic + pointing at G/H. +. J-18/J-19 after running the D.5 check. +. J-32 + J-31 + J-33 + J-34 + J-36 + J-37 + J-39 as one documentation sweep. +. Remainder as individual low/medium tickets. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/README.adoc b/docs/investigation/2026-09-26-silicon-core-recon/README.adoc new file mode 100644 index 0000000..c226f43 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/README.adoc @@ -0,0 +1,91 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Axiom.jl — Silicon-core reconnaissance (2026-09-26) +:toc: +:toclevels: 2 + +Investigation of whether Axiom.jl combines too many responsibilities, whether +its native/GPU/coprocessor execution paths are what the documentation says they +are, and whether a standalone runtime package (working names `SiliconCore.jl` / +`CoprocessorRuntime.jl`) should be extracted. + +*Scope discipline.* This is a reconnaissance and design deliverable. No source +file under `src/`, `ext/`, `zig/`, `ffi/` or `test/` was modified. No +dependency was added. No PR is opened by this work. Everything here lives under +`docs/investigation/2026-09-26-silicon-core-recon/` on the session branch +`arena/01a0de35-axiom-jl` (branched from `main` @ `79e6f48`). + +== Deliverables + +[cols="1,3,3"] +|=== +| ID | File | One-line answer + +| A | link:A-component-map.adoc[Component map] | 19 sub-systems, 11 of them tested in CI; 9 "backends" are type stubs; 2 trees are dead (vendored AcceleratorGate, `ffi/zig`). +| B | link:B-backend-status.adoc[Backend status table] | 1 reference backend; 1 native backend with 4 confirmed defects; 3 GPU extensions with no hardware evidence; 9 env-var stubs. +| C | link:C-abi-ffi-discrepancies.adoc[ABI/FFI discrepancy report] | 44 real exports vs. "~36/32" documented; second FFI tree does not compile; Idris ABI spec covers 3 of 44 symbols; no ABI version check on the Julia side. +| D | link:D-numerical-parity-risks.adoc[Numerical parity risk report] | Pooling layout bug (wrong values), `tanh` NaN for x ≥ 44.5, BatchNorm wrong/crash above 4096 features, `dim` ignored, two summation orders inside the *reference* backend. +| E | link:E-memory-performance.adoc[Memory/performance report] | `axiom_matmul_checked` is 9–16× slower than the unchecked kernel the benchmarks were measured with; per-call `dlsym`, per-call thread spawn, permutedims copies on every FFI call, shape-in-type recompilation. +| F | link:F-extraction-recommendation.adoc[Extraction recommendation] | *Option D now* (defer; stabilise internal interfaces), with an explicit exit criterion to *Option B* — realised by superseding the already-extracted `AcceleratorGate.jl`, not by a third package. +| G | link:G-api-boundary.adoc[Proposed package/API boundary] | Minimal runtime protocol: `Backend`, `Capability`, `ExecutionReport` (requested/selected/executed, fallback_used, precision, device, kernel/ABI version), `strict` mode, diagnostics. +| H | link:H-staged-plan.adoc[Staged plan] | Phase 0 fixes + parity tests → Phase 1 internal `Runtime` seam → Phase 2 evidence gate → Phase 3 (conditional) extraction. +| I | link:I-not-recommended.adoc[Changes explicitly NOT recommended] | No repo split now, no `SiliconCore.jl` from stubs, no GPU deps, no replacing reference kernels, no global warning suppression, no third backend hierarchy. +| J | link:J-upstream-issues.adoc[Upstream issues with evidence] | 40 issues, each with severity, evidence type (empirical vs static), reproduction, and bucket (fix-in-Axiom / future-standalone / not-yet-verified). +| — | link:repro/[repro/] | Minimal reproductions (Zig test files + Python/ctypes probes against the built `.so`). +|=== + +== How the evidence was obtained + +[cols="1,3"] +|=== +| Environment | Linux x86-64 sandbox, 2 CPUs, 3 GB RAM. Zig 0.15.2 (the version pinned in `.github/workflows/ci.yml:75`). Python 3 + numpy 1.26 for `ctypes` probes. `gcc`, `objdump`, `readelf`, `nm`. +| Native library | Built exactly as CI does: `cd zig && zig build -Doptimize=ReleaseFast` → `zig/zig-out/lib/libaxiom_zig.so` (1,101,096 bytes, 44 `axiom_*` exports, zero `NEEDED` entries). `zig build test` passes. `zig fmt --check src/` is clean. +| Julia | *Not available in the sandbox* (all Julia distribution hosts were unreachable; PyPI-hosted installers fetch from the same hosts). Every Julia-level statement in these reports is therefore *static analysis of the source* and is labelled `[static]`. Statements labelled `[empirical]` were executed against the real compiled Zig library or the Zig sources. Maintainer-runnable Julia scripts are specified in D and J so each `[static]` claim can be confirmed or refuted in minutes. +| Git history | The checkout is a single-commit shallow clone (`79e6f48`, "fix: resolve estate gates and Rust/Creusot debt (#87) (#106)"). Provenance questions such as "when did `_checked` kernels replace the benchmarked ones" could not be answered from history; they are answered from artifacts (benchmark results vs. current wrapper code). +|=== + +== Executive summary + +. *Does Axiom.jl combine too many responsibilities?* Yes — 19 identifiable + sub-systems in one package (model core, autograd/training, shape DSL, + heuristic + SMT verification, proof export to four assistants, post-quantum + certificate signing via a Rust cdylib, backend selection, nine coprocessor + stubs, a Zig kernel library, a second orphaned FFI tree, an Idris ABI + specification, three GPU extensions, HuggingFace/PyTorch/ONNX interop, an + HTTP serving layer, model packaging). But the *damage* is not caused by + package count; it is caused by *missing seams inside the package*: layers + read a global `current_backend()`, kernels exist in two Julia copies plus + Zig, proofs never reference the backend that executes the model, and + fallbacks are silent. Splitting the repository would multiply surface area + without creating the missing seams. +. *Is the native path what the docs say?* Partly. The Zig library is real, + libc-free, SIMD/threaded and passes its unit tests. But: the *documented* + production path (`compile(model, backend=ZigBackend(path))` on a + `Sequential`) runs pure Julia unless `set_backend!` is also called; the + Julia wrapper always uses `axiom_matmul_checked`, which is 9–16× slower + than the kernel the published benchmarks measured; the pooling wrappers pass + column-major memory to row-major kernels and return wrong values; `tanh` + overflows to NaN above 44.5; BatchNorm with more than 4096 features + returns wrong values and segfaults from 8192 features — reachable from the + ordinary layer path when the Zig backend is active. +. *Are the GPU backends verified?* No. The extensions contain real + `CUDA.jl`/`AMDGPU.jl`/`Metal.jl` code, but hardware CI is opt-in and the + baseline file that hardware runs would populate is empty. The hardware smoke + test cannot distinguish GPU execution from CPU fallback. `AXIOM_CUDA_AVAILABLE=1` + makes `cuda_available()` return `true` without a device. +. *Does the proof layer prove the runtime?* No. `@prove` strategies 1 and 3 + are string heuristics (documented as such); the SMT path encodes free + variables over `Real` and never encodes the model, weights or a backend; + `verify()`'s `ValidProbabilities` is `last_layer isa Softmax`. No + certificate or proof artifact records which backend/kernel/ABI executed. +. *Extraction decision:* Do not extract now. The runtime seam that a + `SiliconCore.jl` would own does not yet exist as an interface inside Axiom, + and the one previous extraction (`AcceleratorGate.jl`, "extracted from + Axiom.jl's backend module") is vendored back into Axiom as dead code with a + disjoint type hierarchy. Build the seam in-tree first (Phase 1 in H), keep + it small (G), gate on evidence (Phase 2), then decide. + +== Conventions used in the reports + +* `[empirical]` — executed in this investigation; script in `repro/`. +* `[static]` — read from source; not executed here; maintainer check provided. +* `file:line` references are against commit `79e6f48`. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/README.adoc b/docs/investigation/2026-09-26-silicon-core-recon/repro/README.adoc new file mode 100644 index 0000000..6547a3a --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/README.adoc @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Reproductions + +All scripts are read-only probes; none modifies the repository. Build the +library first exactly as CI does (Zig 0.15.2): + + cd zig && zig build -Doptimize=ReleaseFast # -> zig/zig-out/lib/libaxiom_zig.so + +Python probes need `numpy` (`ctypes` is standard library). Run them from this +directory; the `.so` path argument is `../../../../zig/zig-out/lib/libaxiom_zig.so`. + +[cols="2,3,2"] +|=== +| File | What it shows | Issue + +| `batchnorm_probe.py` | `axiom_batchnorm` silently wrong for 4097–8191 features, SIGSEGV from 8192 (each case in a subprocess) | J-01 +| `repro_batchnorm.zig` | Same defect as an index-out-of-bounds panic in ReleaseSafe | J-01 +| `layout_probe.py` | Pooling wrappers' column-major buffers vs row-major kernels → wrong values; `−Inf`/NaN window contracts | J-02, J-07 +| `activation_probe.py` | `axiom_tanh` NaN for x ≥ 44.5 / +Inf; near-zero cancellation; gelu/sigmoid fine | J-03 +| `repro_underflow.zig` | `parallel_layernorm` batch=5 integer-overflow panic (ReleaseSafe) | J-04 +| `repro_underflow_canary.zig` | Same function: `-OReleaseSafe` panics, `-OReleaseFast` test binary crashes | J-04 +| `canary_probe.py` | Through the shipped `.so`, batch=5 is (accidentally) benign: rows correct, canary intact | J-04 +| `chunking_probe.py` | softmax/layernorm for batch 4…17 × 2048 through the `.so` | J-04 +| `matmul_cost.py` | `axiom_matmul_checked` vs `axiom_matmul` timing (9–16×) | J-05 +|=== + +Zig-level reproductions: + + zig test -OReleaseSafe --dep axiom -Mroot=repro_batchnorm.zig -Maxiom=../../../../zig/src/axiom.zig + zig test -OReleaseSafe --dep axiom -Mroot=repro_underflow.zig -Maxiom=../../../../zig/src/axiom.zig + zig test -OReleaseSafe --dep axiom -Mroot=repro_underflow_canary.zig -Maxiom=../../../../zig/src/threading.zig + zig test -OReleaseFast --dep axiom -Mroot=repro_underflow_canary.zig -Maxiom=../../../../zig/src/threading.zig + +Note: the `-O` flag must precede the `-M` module flags (it is per-module in +the Zig 0.15 CLI); placed afterwards it is ignored and the build is Debug. diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py new file mode 100644 index 0000000..d134ee4 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py @@ -0,0 +1,34 @@ +# SPDX-License-Identifier: MPL-2.0 +"""Probe Zig activation kernels (built libaxiom_zig.so) for overflow / cancellation. +Usage: PYTHONPATH= python3 activation_probe.py zig/zig-out/lib/libaxiom_zig.so +Compares against float32 reference formulas evaluated in float64 then rounded.""" +import ctypes, sys, numpy as np +lib = ctypes.CDLL(sys.argv[1]) +f32p = ctypes.POINTER(ctypes.c_float) +def call(sym, x): + x = np.ascontiguousarray(x, dtype=np.float32); y = np.zeros_like(x) + fn = getattr(lib, sym); fn.restype = None + fn.argtypes = [f32p, f32p, ctypes.c_size_t] + fn(x.ctypes.data_as(f32p), y.ctypes.data_as(f32p), x.size); return y +def gelu_ref(x): # same tanh-approx formula Julia's gelu uses, evaluated in float64 + x = x.astype(np.float64); c = np.sqrt(2/np.pi) + return (0.5*x*(1+np.tanh(c*(x+0.044715*x**3)))).astype(np.float32) +xs = np.array([1e-8, 1e-5, 1e-3, 5, 9, 10, 10.5, 11, 12, 20, 44, 44.3, 44.5, 45, 50, 100, -50, -100, float('inf'), float('-inf')], dtype=np.float32) +print(f"{'x':>10} | {'zig tanh':>12} {'ref tanh':>12} | {'zig gelu':>12} {'ref gelu':>12} | {'zig sigmoid':>12} {'ref':>12}") +zt, zg, zs = call('axiom_tanh', xs), call('axiom_gelu', xs), call('axiom_sigmoid', xs) +rt = np.tanh(xs.astype(np.float64)).astype(np.float32); rg = gelu_ref(xs) +rs = (1/(1+np.exp(-xs.astype(np.float64)))).astype(np.float32) +for i, x in enumerate(xs): + flag = "" + if not np.isfinite(zt[i]) and np.isfinite(rt[i]): flag += " TANH-NaN" + if not np.isfinite(zg[i]) and np.isfinite(rg[i]): flag += " GELU-NaN" + if np.isfinite(zt[i]) and rt[i] != 0 and abs(zt[i]-rt[i])/abs(rt[i]) > 1e-4: flag += f" tanh-relerr={abs(zt[i]-rt[i])/abs(rt[i]):.1e}" + print(f"{x:>10.4g} | {zt[i]:>12.6g} {rt[i]:>12.6g} | {zg[i]:>12.6g} {rg[i]:>12.6g} | {zs[i]:>12.6g} {rs[i]:>12.6g}{flag}") +# in-place variants use the same formula +xt = xs.copy(); fn = lib.axiom_tanh_inplace; fn.restype=None; fn.argtypes=[f32p, ctypes.c_size_t]; fn(xt.ctypes.data_as(f32p), xt.size) +print("\naxiom_tanh_inplace(50) =", xt[list(xs).index(np.float32(50))], " axiom_tanh_inplace(11)=", xt[list(xs).index(np.float32(11))]) +# realistic batch: how often does a standard-normal*sigma pre-activation trip GELU? +rng = np.random.default_rng(0) +for sigma in (1, 3, 5, 8): + pre = (rng.standard_normal(1_000_000)*sigma).astype(np.float32) + g = call('axiom_gelu', pre); print(f"gelu on N(0,{sigma}²) x1e6: NaN count = {np.isnan(g).sum()}, max|x|={np.abs(pre).max():.1f}") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/batchnorm_probe.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/batchnorm_probe.py new file mode 100644 index 0000000..d716b20 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/batchnorm_probe.py @@ -0,0 +1,22 @@ +# SPDX-License-Identifier: MPL-2.0 +"""axiom_batchnorm uses a fixed [4096]f32 stack scratch (norm.zig:143). Probe num_features > 4096 +through the production .so, each case in a subprocess (stack corruption may crash the process). +Usage: PYTHONPATH= python3 batchnorm_probe.py zig/zig-out/lib/libaxiom_zig.so""" +import sys, subprocess +child = r''' +import ctypes, sys, numpy as np +lib = ctypes.CDLL(sys.argv[1]); F = int(sys.argv[2]); B = 2 +f32p = ctypes.POINTER(ctypes.c_float) +rng = np.random.default_rng(0) +x = rng.standard_normal((B, F)).astype(np.float32); y = np.zeros_like(x) +g = np.ones(F, np.float32); b = np.zeros(F, np.float32); m = np.zeros(F, np.float32); v = np.ones(F, np.float32) +fn = lib.axiom_batchnorm; fn.restype = None +fn.argtypes = [f32p, f32p, f32p, f32p, f32p, f32p, ctypes.c_size_t, ctypes.c_size_t, ctypes.c_float] +fn(x.ctypes.data_as(f32p), y.ctypes.data_as(f32p), g.ctypes.data_as(f32p), b.ctypes.data_as(f32p), m.ctypes.data_as(f32p), v.ctypes.data_as(f32p), B * F, F, 1e-5) +ref = (x - m) / np.sqrt(v + 1e-5) +print(int((~np.isclose(y, ref, atol=1e-4)).sum()), "of", B * F) +''' +for F in (4096, 4097, 4100, 8192, 65536, 1_000_000): + r = subprocess.run([sys.executable, "-c", child, sys.argv[1], str(F)], capture_output=True, text=True) + out = r.stdout.strip() if r.returncode == 0 else f"CRASH exit={r.returncode} {r.stderr.strip().splitlines()[-1][:80] if r.stderr.strip() else '(signal)'}" + print(f"num_features={F:>8}: {out}") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py new file mode 100644 index 0000000..15333a3 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py @@ -0,0 +1,17 @@ +# SPDX-License-Identifier: MPL-2.0 +"""Call the production libaxiom_zig.so axiom_layernorm with B=5,H=2048 (the chunking-underflow case) +and check (a) row correctness and (b) a canary region after the output buffer. +Usage: PYTHONPATH= python3 canary_probe.py zig/zig-out/lib/libaxiom_zig.so""" +import ctypes, sys, numpy as np +lib = ctypes.CDLL(sys.argv[1]); f32p = ctypes.POINTER(ctypes.c_float) +for (B, H) in [(5, 2048), (5, 4096), (5, 65536)]: + x = np.random.default_rng(0).standard_normal((B, H)).astype(np.float32) + canary = 8 * H + ybuf = np.full(B * H + canary, 12345.0, np.float32) # output rows followed by canary + g = np.ones(H, np.float32); b = np.zeros(H, np.float32) + fn = lib.axiom_layernorm; fn.restype = None + fn.argtypes = [f32p, f32p, f32p, f32p, ctypes.c_size_t, ctypes.c_size_t, ctypes.c_float] + fn(x.ctypes.data_as(f32p), ybuf.ctypes.data_as(f32p), g.ctypes.data_as(f32p), b.ctypes.data_as(f32p), B, H, 1e-5) + y = ybuf[:B*H].reshape(B, H); can = ybuf[B*H:] + ref = (x - x.mean(1, keepdims=True)) / np.sqrt(x.var(1, keepdims=True) + 1e-5) + print(f"B={B} H={H}: bad_rows={int((~np.isclose(y, ref, atol=1e-3)).any(1).sum())} canary_overwritten={int((can != 12345.0).sum())}/{canary}") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/chunking_probe.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/chunking_probe.py new file mode 100644 index 0000000..a2c5663 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/chunking_probe.py @@ -0,0 +1,29 @@ +# SPDX-License-Identifier: MPL-2.0 +"""Which batch sizes trip the chunking underflow in parallel_layernorm/rmsnorm/softmax? +Runs each case in a subprocess because the ReleaseFast .so may segfault / corrupt memory. +Usage: PYTHONPATH= python3 chunking_probe.py zig/zig-out/lib/libaxiom_zig.so""" +import sys, subprocess, json +lib = sys.argv[1] +child = r''' +import ctypes, sys, numpy as np +lib = ctypes.CDLL(sys.argv[1]); B, H, op = int(sys.argv[2]), int(sys.argv[3]), sys.argv[4] +f32p = ctypes.POINTER(ctypes.c_float) +x = np.random.default_rng(0).standard_normal((B, H)).astype(np.float32); y = np.full((B, H), 7.0, np.float32) +if op == "softmax": + fn = lib.axiom_softmax; fn.argtypes = [f32p, f32p, ctypes.c_size_t, ctypes.c_size_t]; fn.restype = None + fn(x.ctypes.data_as(f32p), y.ctypes.data_as(f32p), B, H) + ref = np.exp(x - x.max(1, keepdims=True)); ref /= ref.sum(1, keepdims=True) +elif op == "layernorm": + g = np.ones(H, np.float32); b = np.zeros(H, np.float32) + fn = lib.axiom_layernorm; fn.argtypes = [f32p, f32p, f32p, f32p, ctypes.c_size_t, ctypes.c_size_t, ctypes.c_float]; fn.restype = None + fn(x.ctypes.data_as(f32p), y.ctypes.data_as(f32p), g.ctypes.data_as(f32p), b.ctypes.data_as(f32p), B, H, 1e-5) + m = x.mean(1, keepdims=True); v = x.var(1, keepdims=True); ref = (x - m) / np.sqrt(v + 1e-5) +bad = int((~np.isclose(y, ref, atol=1e-4)).sum()) +print(bad) +''' +for op in ("softmax", "layernorm"): + for B in (4, 5, 6, 7, 8, 9, 13, 17): + H = 2048 + r = subprocess.run([sys.executable, "-c", child, lib, str(B), str(H), op], capture_output=True, text=True) + status = f"exit={r.returncode}" + (f" mismatches={r.stdout.strip()}" if r.returncode == 0 else f" ({r.stderr.strip().splitlines()[-1][:60] if r.stderr.strip() else 'signal'})") + print(f"{op:>9} B={B:>2} H={H}: {status}") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/layout_probe.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/layout_probe.py new file mode 100644 index 0000000..f26ea79 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/layout_probe.py @@ -0,0 +1,79 @@ +# SPDX-License-Identifier: MPL-2.0 +""" +Layout probe for the Julia -> Zig pooling wrappers. + +src/backends/zig_ffi.jl passes Julia's column-major (N,H,W,C) buffer *directly* +to axiom_maxpool2d / axiom_global_avgpool2d (no _to_row_major_vec), while +zig/src/pool.zig indexes row-major NHWC. This script reproduces exactly what +the Julia wrapper does (column-major bytes in, column-major interpretation of +the output) and compares with the mathematically correct pooling result. + +Also probes: padding silently dropped, -Inf window handling, NaN handling. +""" +import ctypes, sys +import numpy as np + +lib = ctypes.CDLL(sys.argv[1]) +f32p = ctypes.POINTER(ctypes.c_float) +sz = ctypes.c_size_t + +lib.axiom_maxpool2d.argtypes = [f32p, f32p, sz, sz, sz, sz, sz, sz, sz, sz] +lib.axiom_maxpool2d.restype = None +lib.axiom_global_avgpool2d.argtypes = [f32p, f32p, sz, sz, sz, sz] +lib.axiom_global_avgpool2d.restype = None + +def ref_maxpool(x, k, s): + N, H, W, C = x.shape + Ho, Wo = (H - k) // s + 1, (W - k) // s + 1 + y = np.empty((N, Ho, Wo, C), np.float32) + for n in range(N): + for c in range(C): + for i in range(Ho): + for j in range(Wo): + y[n, i, j, c] = x[n, i*s:i*s+k, j*s:j*s+k, c].max() + return y + +def julia_style_maxpool(x, k, s): + """Mimic backend_maxpool2d(::ZigBackend): pass column-major bytes as-is, + read output back as column-major (N,Ho,Wo,C).""" + N, H, W, C = x.shape + Ho, Wo = (H - k) // s + 1, (W - k) // s + 1 + xin = np.asfortranarray(x) # Julia memory order + out = np.zeros(N*Ho*Wo*C, np.float32) + lib.axiom_maxpool2d(xin.ctypes.data_as(f32p), out.ctypes.data_as(f32p), + N, H, W, C, k, k, s, s) + return out.reshape((N, Ho, Wo, C), order="F") # Julia reads back column-major + +def julia_style_gap(x): + N, H, W, C = x.shape + xin = np.asfortranarray(x) + out = np.zeros(N*C, np.float32) + lib.axiom_global_avgpool2d(xin.ctypes.data_as(f32p), out.ctypes.data_as(f32p), N, H, W, C) + return out.reshape((N, C), order="F") + +rng = np.random.default_rng(0) +print("case | max|zig-ref| | mismatched elements") +for (N, H, W, C, k, s) in [(1, 4, 4, 1, 2, 2), (1, 4, 4, 2, 2, 2), (2, 4, 4, 1, 2, 2), (2, 6, 6, 3, 2, 2), (1, 5, 3, 1, 2, 1)]: + x = rng.standard_normal((N, H, W, C)).astype(np.float32) + ref = ref_maxpool(x, k, s) + got = julia_style_maxpool(x, k, s) + bad = int((~np.isclose(ref, got)).sum()) + print(f"maxpool N={N} H={H} W={W} C={C} k={k} s={s} | {np.abs(ref-got).max():10.4f} | {bad}/{ref.size}") + +for (N, H, W, C) in [(1, 3, 3, 1), (1, 3, 3, 2), (2, 3, 3, 1), (2, 3, 3, 4)]: + x = rng.standard_normal((N, H, W, C)).astype(np.float32) + ref = x.mean(axis=(1, 2)) + got = julia_style_gap(x) + bad = int((~np.isclose(ref, got)).sum()) + print(f"gap N={N} H={H} W={W} C={C} | {np.abs(ref-got).max():10.4f} | {bad}/{ref.size}") + +print() +print("Edge-case contracts (row-major single-channel so layout is not a factor):") +x = np.full((1, 2, 2, 1), -np.inf, np.float32) +out = np.zeros(1, np.float32) +lib.axiom_maxpool2d(np.ascontiguousarray(x).ctypes.data_as(f32p), out.ctypes.data_as(f32p), 1, 2, 2, 1, 2, 2, 2, 2) +print(f" all -Inf window -> zig={out[0]!r} julia(maximum)=-Inf (zig initialises max at -floatmax)") +x = np.array([[1.0, np.nan], [0.5, 0.25]], np.float32).reshape(1, 2, 2, 1) +out = np.zeros(1, np.float32) +lib.axiom_maxpool2d(np.ascontiguousarray(x).ctypes.data_as(f32p), out.ctypes.data_as(f32p), 1, 2, 2, 1, 2, 2, 2, 2) +print(f" window with NaN -> zig={out[0]!r} julia(maximum)=NaN (zig `val > max` skips NaN)") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py new file mode 100644 index 0000000..37f12de --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py @@ -0,0 +1,32 @@ +# SPDX-License-Identifier: MPL-2.0 +"""Cost of axiom_matmul_checked vs axiom_matmul (the Julia wrapper always uses +the checked one). The checked variant runs a scalar O(m*n*k) finiteness +pre-pass (matmulCellFinite) before the tiled SIMD kernel.""" +import ctypes, sys, time +import numpy as np + +lib = ctypes.CDLL(sys.argv[1]) +f32p = ctypes.POINTER(ctypes.c_float) +sz = ctypes.c_size_t +lib.axiom_matmul.argtypes = [f32p, f32p, f32p, sz, sz, sz] +lib.axiom_matmul.restype = None +lib.axiom_matmul_checked.argtypes = [f32p, f32p, f32p, sz, sz, sz] +lib.axiom_matmul_checked.restype = ctypes.c_uint32 + +rng = np.random.default_rng(1) +print(f"{'m=k=n':>7} | {'unchecked ms':>12} | {'checked ms':>10} | ratio | numpy(BLAS) ms") +for n in (64, 128, 256, 512): + a = np.ascontiguousarray(rng.standard_normal((n, n)).astype(np.float32)) + b = np.ascontiguousarray(rng.standard_normal((n, n)).astype(np.float32)) + c = np.zeros((n, n), np.float32) + reps = 5 if n >= 512 else 20 + def bench(fn): + best = 1e9 + for _ in range(reps): + t = time.perf_counter(); fn(); best = min(best, time.perf_counter() - t) + return best * 1e3 + tu = bench(lambda: lib.axiom_matmul(a.ctypes.data_as(f32p), b.ctypes.data_as(f32p), c.ctypes.data_as(f32p), n, n, n)) + tc = bench(lambda: lib.axiom_matmul_checked(a.ctypes.data_as(f32p), b.ctypes.data_as(f32p), c.ctypes.data_as(f32p), n, n, n)) + tn = bench(lambda: a @ b) + ok = np.allclose(c, a @ b, atol=1e-3, rtol=1e-4) + print(f"{n:>7} | {tu:12.3f} | {tc:10.3f} | {tc/tu:5.2f} | {tn:.3f} (result matches BLAS: {ok})") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_batchnorm.zig b/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_batchnorm.zig new file mode 100644 index 0000000..79d1577 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_batchnorm.zig @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: MPL-2.0 +// Reproduction: norm.batchnorm uses a fixed `[4096]f32` stack scratch buffer +// indexed by `num_features` with no bound check. num_features > 4096 writes +// past the stack array. In ReleaseSafe/Debug this is an index-out-of-bounds +// panic; through the shipped ReleaseFast .so it is silently wrong (4097..8191) +// and SIGSEGV from 8192 features (see batchnorm_probe.py). +// Run: zig test -OReleaseSafe --dep axiom -Mroot=repro_batchnorm.zig -Maxiom=../../../../zig/src/axiom.zig +const std = @import("std"); +const axiom = @import("axiom"); + +test "batchnorm num_features=4097 overflows fixed stack scratch" { + const B: usize = 2; + const F: usize = 4097; + const alloc = std.testing.allocator; + const x = try alloc.alloc(f32, B * F); + defer alloc.free(x); + const y = try alloc.alloc(f32, B * F); + defer alloc.free(y); + const gamma = try alloc.alloc(f32, F); + defer alloc.free(gamma); + const beta = try alloc.alloc(f32, F); + defer alloc.free(beta); + const rmean = try alloc.alloc(f32, F); + defer alloc.free(rmean); + const rvar = try alloc.alloc(f32, F); + defer alloc.free(rvar); + @memset(x, 1.0); + @memset(gamma, 1.0); + @memset(beta, 0.0); + @memset(rmean, 0.0); + @memset(rvar, 1.0); + axiom.norm.batchnorm(x.ptr, y.ptr, gamma.ptr, beta.ptr, rmean.ptr, rvar.ptr, B, F, 1e-5); +} diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow.zig b/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow.zig new file mode 100644 index 0000000..698c444 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow.zig @@ -0,0 +1,45 @@ +// SPDX-License-Identifier: MPL-2.0 +// Reproduction: batch_size == 5 underflow in threading.parallel_layernorm / +// parallel_rmsnorm / parallel_batch (softmax). +// +// Condition to reach the parallel path: total >= 8192 and batch_size >= 4. +// With batch_size = 5: num_threads = min(4, 5) = 4; chunk = ceil(5/4) = 2; +// last_start = (4-1)*2 = 6 > 5 => `batch_size - last_start` wraps (usize). +// +// Build/run against the repository's zig/src tree: +// zig test -OReleaseSafe --dep axiom -Mroot=repro_underflow.zig -Maxiom=../../../../zig/src/axiom.zig +const std = @import("std"); +const axiom = @import("axiom"); + +test "layernorm batch_size=5 hidden=2048 reaches usize underflow" { + const B: usize = 5; + const H: usize = 2048; // 5*2048 = 10240 >= BATCH_THREAD_THRESHOLD (8192) + const alloc = std.testing.allocator; + const x = try alloc.alloc(f32, B * H); + defer alloc.free(x); + const y = try alloc.alloc(f32, B * H); + defer alloc.free(y); + const gamma = try alloc.alloc(f32, H); + defer alloc.free(gamma); + const beta = try alloc.alloc(f32, H); + defer alloc.free(beta); + for (x, 0..) |*v, i| v.* = @floatFromInt(i % 17); + @memset(gamma, 1.0); + @memset(beta, 0.0); + @memset(y, 0.0); + // In ReleaseSafe/Debug this panics with "integer overflow" (or out-of-bounds). + // In ReleaseFast it silently reads/writes out of bounds. + axiom.threading.parallel_layernorm(x.ptr, y.ptr, gamma.ptr, beta.ptr, B, H, 1e-5); +} + +test "softmax batch_size=5 classes=2048 reaches usize underflow" { + const B: usize = 5; + const C: usize = 2048; + const alloc = std.testing.allocator; + const x = try alloc.alloc(f32, B * C); + defer alloc.free(x); + const y = try alloc.alloc(f32, B * C); + defer alloc.free(y); + for (x, 0..) |*v, i| v.* = @floatFromInt(i % 13); + axiom.threading.parallel_softmax_batched(x.ptr, y.ptr, B, C); +} diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow_canary.zig b/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow_canary.zig new file mode 100644 index 0000000..1129980 --- /dev/null +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/repro_underflow_canary.zig @@ -0,0 +1,53 @@ +// SPDX-License-Identifier: MPL-2.0 +// Does the chunking underflow in parallel_layernorm (threading.zig:392) write out of bounds +// in ReleaseFast? Output buffer is followed by a canary region; rows are checked against a +// scalar reference. Run: +// zig test --dep axiom -Mroot=repro_underflow_canary.zig -Maxiom=../../../../zig/src/threading.zig -OReleaseFast +// zig test --dep axiom -Mroot=repro_underflow_canary.zig -Maxiom=../../../../zig/src/threading.zig -OReleaseSafe (panics) +const std = @import("std"); +const threading = @import("axiom"); + +test "parallel_layernorm B=5 H=2048: canary after output" { + const B: usize = 5; + const H: usize = 2048; + const n = B * H; + const canary_len: usize = 4 * H; + var x: [n]f32 = undefined; + var y: [n + 4 * 2048]f32 = undefined; // output + canary + var gamma: [H]f32 = undefined; + var beta: [H]f32 = undefined; + for (0..n) |i| x[i] = @floatFromInt((i * 7919) % 101); + for (0..H) |i| { + gamma[i] = 1.0; + beta[i] = 0.0; + } + for (0..n + canary_len) |i| y[i] = 12345.0; + threading.parallel_layernorm(&x, &y, &gamma, &beta, B, H, 1e-5); + // rows + var bad_rows: usize = 0; + for (0..B) |b| { + var mean: f64 = 0; + for (0..H) |i| mean += x[b * H + i]; + mean /= @floatFromInt(H); + var v: f64 = 0; + for (0..H) |i| { + const d = x[b * H + i] - mean; + v += d * d; + } + v /= @floatFromInt(H); + const inv = 1.0 / @sqrt(v + 1e-5); + var row_bad = false; + for (0..H) |i| { + const ref: f32 = @floatCast((x[b * H + i] - mean) * inv); + if (@abs(y[b * H + i] - ref) > 1e-3) row_bad = true; + } + if (row_bad) bad_rows += 1; + } + var canary_hits: usize = 0; + for (n..n + canary_len) |i| { + if (y[i] != 12345.0) canary_hits += 1; + } + std.debug.print("\nbad_rows={d} canary_overwritten={d}/{d}\n", .{ bad_rows, canary_hits, canary_len }); + try std.testing.expectEqual(@as(usize, 0), bad_rows); + try std.testing.expectEqual(@as(usize, 0), canary_hits); +} From c0f3274600c4fb136669667713bd2f520f556d5d Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sat, 26 Sep 2026 15:41:12 +0000 Subject: [PATCH 2/2] style(repro): one statement per line in probe scripts (CodeFactor E702) Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .../repro/activation_probe.py | 24 +++++++++++++------ .../repro/canary_probe.py | 12 ++++++---- .../repro/matmul_cost.py | 4 +++- 3 files changed, 28 insertions(+), 12 deletions(-) diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py index d134ee4..8f886e9 100644 --- a/docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/activation_probe.py @@ -6,17 +6,22 @@ lib = ctypes.CDLL(sys.argv[1]) f32p = ctypes.POINTER(ctypes.c_float) def call(sym, x): - x = np.ascontiguousarray(x, dtype=np.float32); y = np.zeros_like(x) - fn = getattr(lib, sym); fn.restype = None + x = np.ascontiguousarray(x, dtype=np.float32) + y = np.zeros_like(x) + fn = getattr(lib, sym) + fn.restype = None fn.argtypes = [f32p, f32p, ctypes.c_size_t] - fn(x.ctypes.data_as(f32p), y.ctypes.data_as(f32p), x.size); return y + fn(x.ctypes.data_as(f32p), y.ctypes.data_as(f32p), x.size) + return y def gelu_ref(x): # same tanh-approx formula Julia's gelu uses, evaluated in float64 - x = x.astype(np.float64); c = np.sqrt(2/np.pi) + x = x.astype(np.float64) + c = np.sqrt(2/np.pi) return (0.5*x*(1+np.tanh(c*(x+0.044715*x**3)))).astype(np.float32) xs = np.array([1e-8, 1e-5, 1e-3, 5, 9, 10, 10.5, 11, 12, 20, 44, 44.3, 44.5, 45, 50, 100, -50, -100, float('inf'), float('-inf')], dtype=np.float32) print(f"{'x':>10} | {'zig tanh':>12} {'ref tanh':>12} | {'zig gelu':>12} {'ref gelu':>12} | {'zig sigmoid':>12} {'ref':>12}") zt, zg, zs = call('axiom_tanh', xs), call('axiom_gelu', xs), call('axiom_sigmoid', xs) -rt = np.tanh(xs.astype(np.float64)).astype(np.float32); rg = gelu_ref(xs) +rt = np.tanh(xs.astype(np.float64)).astype(np.float32) +rg = gelu_ref(xs) rs = (1/(1+np.exp(-xs.astype(np.float64)))).astype(np.float32) for i, x in enumerate(xs): flag = "" @@ -25,10 +30,15 @@ def gelu_ref(x): # same tanh-approx formula Julia's gelu uses, evaluated in flo if np.isfinite(zt[i]) and rt[i] != 0 and abs(zt[i]-rt[i])/abs(rt[i]) > 1e-4: flag += f" tanh-relerr={abs(zt[i]-rt[i])/abs(rt[i]):.1e}" print(f"{x:>10.4g} | {zt[i]:>12.6g} {rt[i]:>12.6g} | {zg[i]:>12.6g} {rg[i]:>12.6g} | {zs[i]:>12.6g} {rs[i]:>12.6g}{flag}") # in-place variants use the same formula -xt = xs.copy(); fn = lib.axiom_tanh_inplace; fn.restype=None; fn.argtypes=[f32p, ctypes.c_size_t]; fn(xt.ctypes.data_as(f32p), xt.size) +xt = xs.copy() +fn = lib.axiom_tanh_inplace +fn.restype=None +fn.argtypes=[f32p, ctypes.c_size_t] +fn(xt.ctypes.data_as(f32p), xt.size) print("\naxiom_tanh_inplace(50) =", xt[list(xs).index(np.float32(50))], " axiom_tanh_inplace(11)=", xt[list(xs).index(np.float32(11))]) # realistic batch: how often does a standard-normal*sigma pre-activation trip GELU? rng = np.random.default_rng(0) for sigma in (1, 3, 5, 8): pre = (rng.standard_normal(1_000_000)*sigma).astype(np.float32) - g = call('axiom_gelu', pre); print(f"gelu on N(0,{sigma}²) x1e6: NaN count = {np.isnan(g).sum()}, max|x|={np.abs(pre).max():.1f}") + g = call('axiom_gelu', pre) + print(f"gelu on N(0,{sigma}²) x1e6: NaN count = {np.isnan(g).sum()}, max|x|={np.abs(pre).max():.1f}") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py index 15333a3..982c964 100644 --- a/docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/canary_probe.py @@ -3,15 +3,19 @@ and check (a) row correctness and (b) a canary region after the output buffer. Usage: PYTHONPATH= python3 canary_probe.py zig/zig-out/lib/libaxiom_zig.so""" import ctypes, sys, numpy as np -lib = ctypes.CDLL(sys.argv[1]); f32p = ctypes.POINTER(ctypes.c_float) +lib = ctypes.CDLL(sys.argv[1]) +f32p = ctypes.POINTER(ctypes.c_float) for (B, H) in [(5, 2048), (5, 4096), (5, 65536)]: x = np.random.default_rng(0).standard_normal((B, H)).astype(np.float32) canary = 8 * H ybuf = np.full(B * H + canary, 12345.0, np.float32) # output rows followed by canary - g = np.ones(H, np.float32); b = np.zeros(H, np.float32) - fn = lib.axiom_layernorm; fn.restype = None + g = np.ones(H, np.float32) + b = np.zeros(H, np.float32) + fn = lib.axiom_layernorm + fn.restype = None fn.argtypes = [f32p, f32p, f32p, f32p, ctypes.c_size_t, ctypes.c_size_t, ctypes.c_float] fn(x.ctypes.data_as(f32p), ybuf.ctypes.data_as(f32p), g.ctypes.data_as(f32p), b.ctypes.data_as(f32p), B, H, 1e-5) - y = ybuf[:B*H].reshape(B, H); can = ybuf[B*H:] + y = ybuf[:B*H].reshape(B, H) + can = ybuf[B*H:] ref = (x - x.mean(1, keepdims=True)) / np.sqrt(x.var(1, keepdims=True) + 1e-5) print(f"B={B} H={H}: bad_rows={int((~np.isclose(y, ref, atol=1e-3)).any(1).sum())} canary_overwritten={int((can != 12345.0).sum())}/{canary}") diff --git a/docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py b/docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py index 37f12de..79f3346 100644 --- a/docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py +++ b/docs/investigation/2026-09-26-silicon-core-recon/repro/matmul_cost.py @@ -23,7 +23,9 @@ def bench(fn): best = 1e9 for _ in range(reps): - t = time.perf_counter(); fn(); best = min(best, time.perf_counter() - t) + t = time.perf_counter() + fn() + best = min(best, time.perf_counter() - t) return best * 1e3 tu = bench(lambda: lib.axiom_matmul(a.ctypes.data_as(f32p), b.ctypes.data_as(f32p), c.ctypes.data_as(f32p), n, n, n)) tc = bench(lambda: lib.axiom_matmul_checked(a.ctypes.data_as(f32p), b.ctypes.data_as(f32p), c.ctypes.data_as(f32p), n, n, n))