Axiom flagship hardening (2) — honest proof claims (G03–G05) + design diary (#47)

## Summary

Follow-up to the merged #46 (which closed the first two P1 soundness
holes). This branch was **restarted from the post-merge `main`** — it
does not re-stack the squashed pilot. It closes three "proof honesty"
gaps and captures the initiative's decision record in-repo.

### G03 — proof-assistant import verification was fake (high)
`proof_export.jl` judged a Lean/Coq/Isabelle proof "complete" merely for
**lacking** `sorry`/`Admitted`/`oops` — so an empty file, or `theorem
foo : True := trivial`, passed as verified. Now a proof must contain
**at least one substantive** (non-vacuous, non-boilerplate)
theorem/lemma statement; empty/trivial proofs report `:incomplete`.
*(Fixing this exposed two pre-existing test fixtures that were
themselves vacuous `:= trivial` proofs — updated to substantive
statements.)*

### G04 — `@prove` overclaim (high)
`dsl/prove.jl` (+ `docs/wiki/Verification.md`) documented `@prove` as
"symbolic execution" / "formal verification", but it is a **substring
match on the printed AST**. Relabelled honestly (experimental heuristic;
**not** symbolic execution or a theorem prover; real proving is the
SMT/Idris2 path). No behaviour change — every remaining mention is now
an explicit negation.

### G05 — Idris2 ABI is a disconnected demo (high; honest relabel)
`src/Abi/*.idr` declare a generic surface that does **not** match the
~36 real `axiom_*` zig exports used by `src/backends/zig_ffi.jl`.
Labelled as an **illustrative scaffold** (not a proof of the production
FFI boundary) in each file + `ABI-FFI-README.md`, pointed at the real
boundary (`zig/` + `zig_ffi.jl`), and flagged the **orphan `ffi/zig/`
tree (zero `axiom_*` exports)** as a KNOWN ISSUE. Full ABI↔zig
connection is tracked follow-up (Idris2 is CI-only here).

### Design record captured online
`docs/design-diary/PEPYS-DESIGN-DIARY.adoc` (the running "Samuel Pepys"
decision log) and `docs/design-diary/ULTRAPLAN.adoc` (executive summary,
41-item gap register, phased plan, decision forks, estate wiring,
risks).

## Verification (independent re-run, not self-graded)
- `Pkg.test()` on the rebased base → **670 / 670 pass** (651 + 19 new
G03 assertions).
- Grep confirms no affirmative "symbolic execution" / "formal
verification" claim remains attached to `@prove`.

## Residuals (tracked)
Real hybrid **Ed448+Dilithium5** certificate signing (G01 auth layer,
reusing `opsm`'s `pqcrypto` crates), full Idris2-ABI↔zig connection
(G05), plus the broader flagship work (Aqua/JET/Documenter, RegistryCI,
panic-attack gate, RSR completeness, doc reconciliation).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1

---
_Generated by [Claude
Code](https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

ABI-FFI-README.md

@@ -2,15 +2,28 @@
 
 This file documents the current ABI/FFI split for Axiom.jl.
 
-## Canonical ABI Spec (Idris2)
+## Idris2 ABI Scaffold (illustrative, not the production ABI proof)
 
-The Idris2 ABI scaffold now lives under:
+The Idris2 ABI scaffold lives under:
 
 - `src/Abi/Types.idr`
 - `src/Abi/Layout.idr`
 - `src/Abi/Foreign.idr`
 
-These modules use concrete `axiom_*` symbol names and no unresolved template placeholders.
+These modules use concrete `axiom_*` symbol names and no unresolved template
+placeholders, but they declare a **generic** lifecycle/callback surface
+(`axiom_init`, `axiom_process`, `axiom_register_callback`, ...) that does
+**not** match the ~36 real Zig kernel exports (`axiom_matmul`, `axiom_relu`,
+`axiom_conv2d`, and the rest of `zig/src/axiom.zig`) actually consumed by
+`src/backends/zig_ffi.jl`. Treat this scaffold as a
+worked illustration of the hyperpolymath ABI-FFI pattern (Idris2 ABI + Zig
+FFI), not as a proof binding Axiom's production kernels. The `Verify.*`
+functions in `Types.idr` are `putStrLn` stubs, not executed proofs.
+
+**ROADMAP (future work, not yet started):** extend the `.idr` declarations
+to cover the real `axiom_*` Zig exports and replace the `Verify` stubs with
+genuine size/alignment/signature proofs checked against `zig/src/axiom.zig`
+and `ffi/zig/include/axiom.h`.
 
 ### Idris2 validation
 
@@ -25,20 +38,55 @@ idris2 --source-dir src --check src/Abi/Foreign.idr
 Current production-tested backend FFI path is Julia <-> Zig:
 
 - Julia bridge: `src/backends/zig_ffi.jl`
-- Zig C ABI exports: `ffi/zig/src/main.zig`
+- Zig C ABI exports: `zig/src/axiom.zig` (compiled to `libaxiom_zig.so` via
+  `zig/build.zig`; this is the artifact CI, benchmarks, and
+  `AXIOM_ZIG_LIB`/`ZigBackend(...)` actually load -- see `.github/workflows/ci.yml`,
+  `benchmark/*.jl`, `README.md`)
 
 This path is covered by CI/readiness checks (backend parity + runtime smoke).
 
-## Zig FFI Status
-
-`ffi/zig/` is now concrete (non-template) and exports concrete `axiom_*` symbols:
-
-- implementation: `ffi/zig/src/main.zig`
-- build/test entry: `ffi/zig/build.zig`
-- integration coverage: `ffi/zig/test/integration_test.zig`
-- C header: `ffi/zig/include/axiom.h`
-
-Validation:
+## KNOWN ISSUE: orphan second Zig FFI tree (`ffi/zig/` vs `zig/`)
+
+There are **two** Zig trees in this repository and they are not the same
+code:
+
+- **`zig/`** (repo root) -- the real, production Zig backend. `zig/src/axiom.zig`
+  exports the ~36 real `axiom_*` kernels (`axiom_matmul`, `axiom_relu`,
+  `axiom_conv2d`, activations, norm, pooling, attention, ...) consumed by
+  `src/backends/zig_ffi.jl` and built into `libaxiom_zig.so`.
+- **`ffi/zig/`** -- a separate, smaller Zig tree (`ffi/zig/src/main.zig`,
+  `ffi/zig/build.zig`, `ffi/zig/include/axiom.h`) that exports **zero**
+  `axiom_*` kernel symbols (`grep -c "export fn axiom_"` = 0) and instead
+  implements a different, generic lifecycle/callback C ABI matching the
+  `src/Abi/*.idr` scaffold's naming (`axiom_init`, `axiom_process`,
+  `axiom_register_callback`, ...). Its header comment even points at
+  `src/abi/Foreign.idr`, a stale/incorrect path (the real directory is
+  `src/Abi/`, capital A) -- further evidence this tree has drifted from the
+  rest of the repo and is not wired into anything Julia actually loads.
+
+**This is flagged, not fixed here.** `ffi/zig/` is not deleted -- it may be
+salvageable as the eventual real implementation backing the `src/Abi/*.idr`
+scaffold (see ROADMAP notes above), but as of this writing it is disconnected
+from both the production Zig backend and the Idris2 ABI's stated symbol
+surface. Anyone relying on "the Zig FFI" should confirm which of the two
+trees they mean; for release/readiness purposes only `zig/` is authoritative
+(next section).
+
+## Zig FFI Status (production: `zig/`)
+
+`zig/` is the sole production-tested native backend and exports concrete
+`axiom_*` symbols (~36, see `TOPOLOGY.md`):
+
+- implementation: `zig/src/axiom.zig`
+- build entry: `zig/build.zig`
+- Julia-side wiring: `src/backends/zig_ffi.jl`
+
+The separate `ffi/zig/` tree (`ffi/zig/src/main.zig`, `ffi/zig/build.zig`,
+`ffi/zig/test/integration_test.zig`, `ffi/zig/include/axiom.h`) is also
+concrete (non-template) and internally self-consistent, but -- per the
+orphan-tree note above -- exports a different, generic `axiom_*` surface
+that is not the production kernel FFI. Its own validation still works
+in isolation:
 
 ```bash
 cd ffi/zig
@@ -55,6 +103,11 @@ zig build test
 
 ## Practical Guidance
 
-For release/readiness decisions, treat the Zig FFI path as authoritative.
-Treat Idris2 ABI files as formal scaffold/specification that now typechecks and
-uses concrete Axiom naming.
+For release/readiness decisions, treat `zig/` + `src/backends/zig_ffi.jl` as
+the authoritative production FFI boundary. Treat the Idris2 `src/Abi/*.idr`
+files as an illustrative ABI-FFI scaffold that typechecks and uses concrete
+Axiom naming, but does **not** prove or specify the production kernel FFI --
+see the ROADMAP notes above for what closing that gap would require. Treat
+`ffi/zig/` as a flagged, currently-disconnected second Zig tree (see
+"KNOWN ISSUE" above) pending a decision on whether to wire it to the
+`src/Abi/*.idr` scaffold, fold it into `zig/`, or retire it.