|
| 1 | +# SPDX-License-Identifier: MPL-2.0 |
| 2 | +# Bustfile — design-aetiology / "bust" contract for snifs |
| 3 | +# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +# |
| 5 | +# Paired runner: bust.ncl (NOT YET PRESENT — paired .ncl runners are an |
| 6 | +# estate-wide gap; cf the Adjustfile contractile-sync |
| 7 | +# check. Do not assume a runner exists.) |
| 8 | +# Verb: bust |
| 9 | +# |
| 10 | +# Semantics: BUST is about *broken* — the slang "damn, this thing is bust". |
| 11 | +# It records WHY things break (or nearly broke), cause-first, as |
| 12 | +# design aetiology — causal help/error/removal, NOT a bandaid that |
| 13 | +# suppresses the symptom. (Sibling: DUST = exnovation, the clean |
| 14 | +# reduction-to-dust / deliberate removal of a thing.) |
| 15 | +# Run with: bust check (list failure modes + recovery status) |
| 16 | +# Fix with: bust fix (apply the causal recovery where deterministic; advisory otherwise) |
| 17 | + |
| 18 | +@abstract: |
| 19 | +The snifs Bustfile in two disjoint halves. |
| 20 | + |
| 21 | + ## Failure Modes — OPEN, actionable defect contracts: a class that CAN break, |
| 22 | + each pairing a detection probe with a causal recovery. This is the half a |
| 23 | + `bust` runner / k9 gate would drill (declared -> drilled -> verified | failing). |
| 24 | + |
| 25 | + ## Near-Hit Cases — CLOSED, non-actionable recognition records: something that |
| 26 | + COULD have bitten but DID NOT, written down with its aetiology so future work |
| 27 | + recognises the same shape rather than re-stumbling into it. A near-hit is NOT a |
| 28 | + defect, has no recovery to drill, and must never be auto-promoted into a Failure |
| 29 | + Mode (that would invent an open issue from a non-issue). It only graduates by an |
| 30 | + explicit human decision. |
| 31 | +@end |
| 32 | + |
| 33 | +## Failure Modes |
| 34 | + |
| 35 | +### releasefast-guest-silent-wrong-answers |
| 36 | +- description: A SNIF guest built with `-Doptimize=ReleaseFast` (or `ReleaseSmall`) strips Zig's runtime safety traps (overflow, bounds, unreachable). At the wasm32-freestanding guest boundary the same fault that should TRAP becomes undefined behaviour — the guest returns a plausible-but-wrong value across the buffer ABI and the BEAM host accepts a silently corrupt answer. There is no crash to observe. |
| 37 | +- cause: optimisation-for-speed removes the only mechanism (safety traps) that surfaces ABI/arithmetic violations at the cleave surface; ReleaseSafe keeps the trap and converts the same bug into an *observable* guest trap the host catches as `{:error, _}`. |
| 38 | +- probe: ! grep -qE 'optimize *= *\.(ReleaseFast|ReleaseSmall)' zig/src/*.zig build.zig 2>/dev/null # shipped guest must be ReleaseSafe |
| 39 | +- probe: just abi-conformance # + a differential corpus: ReleaseSafe vs ReleaseFast must AGREE on edge inputs — divergence == this mode firing |
| 40 | +- recovery: build/ship the guest `-OReleaseSafe` (traps preserved); CI-gate so a ReleaseFast artifact cannot ship; on a field wrong-answer, rebuild ReleaseSafe and replay the differential corpus to localise the trapping input. |
| 41 | +- severity: critical |
| 42 | +- status: declared |
| 43 | + |
| 44 | +### wasmex-nif-guest-load-failure |
| 45 | +- description: The host-side wasmex NIF, or the `.wasm` guest it loads, fails to instantiate — a missing/renamed export, ABI/version skew between the Idris2-verified model and the real Zig exports, wrong wasm target, or a NIF that won't link into the BEAM. The Elixir call surfaces `{:error, _}` (or a NIF load crash) instead of a working SNIF. |
| 46 | +- cause: the guest export set drifted from the verified ABI (`verification/proofs/idris2/ABI/*`), or the guest was built for the wrong target / missing an export, so wasmex cannot bind the expected interface at instantiation — boundary-erosion / ABI-drift, exactly the class `abi_conformance.py` guards. |
| 47 | +- probe: just abi-conformance # signature drift gate (safe_nif + buffer_abi vs Foreign.idr / BufferAbi.idr) |
| 48 | +- probe: cd demo && mix test # host-side instantiate + call; must not be {:error, _} for the happy path |
| 49 | +- recovery: re-sync exports to the Idris2 ABI model (realign safe_nif.zig + buffer_abi.zig against Foreign.idr / BufferAbi.idr), rebuild for wasm32-freestanding, re-run `just abi-conformance` until green, then re-instantiate. |
| 50 | +- severity: critical |
| 51 | +- status: declared |
| 52 | + |
| 53 | +## Near-Hit Cases |
| 54 | + |
| 55 | +# RECOGNITION LEDGER — read, do not drill. Entries here are NOT defects and NOT |
| 56 | +# merge-gated. A `bust` runner / k9 gate binds ONLY to "## Failure Modes" above. |
| 57 | +# Do not migrate these into Failure Modes; promotion is a human decision via the |
| 58 | +# entry's `graduates_to_failure_mode_if:` trip-condition. |
| 59 | + |
| 60 | +### zig-0.15.2-opaque-with-fields-template-rot |
| 61 | +- kind: near-hit |
| 62 | +- status: recognised |
| 63 | +- not_an_issue: true |
| 64 | +- class: toolchain # (extends the runner's failure-class enum; near-hits do not bind the runner) |
| 65 | +- surfaced_by: cross-repo AFFIRMATION signal, 2026-06-16 — typed-wasm's `ffi/zig` was found genuinely BUST under Zig 0.15.2 (its `tests/e2e.sh` Zig step fails, 48/1/6); we then checked whether the same shape bites snifs. |
| 66 | +- what_almost_broke: the rsr-template `src/interface/ffi/src/main.zig` carries pre-0.15 Zig patterns — an `opaque { ...fields... }` (`Handle`) and `std.heap.c_allocator` — that Zig 0.15.2 rejects. Rendered and built, it would not compile. |
| 67 | +- why_it_did_not_bite: that file is *unrendered dead scaffold* — it still holds `{{project}}` placeholders and is wired into NO build / test / gate (`tests/e2e.sh` does not touch it; `src/interface/ffi/build.zig`'s compile step is commented out; the proof + conformance gates use `zig/src/safe_nif.zig` + `buffer_abi.zig` only). A direct compile dies at the `{{project}}` placeholder *before* even reaching the type errors. The LIVE guests compile clean under Zig 0.15.2 (verified this session). |
| 68 | +- aetiology: |
| 69 | + - root-1-template: the rsr-template shipped a generic C-FFI example written in pre-0.15 Zig idioms; snifs never rendered it (it uses `zig/src/safe_nif.zig` instead), so the dead patterns sat latent. |
| 70 | + - root-2-toolchain: Zig 0.15.2 tightened two things — `opaque` may no longer carry fields, and `std.heap.c_allocator` now requires explicit libc linking. |
| 71 | + - mechanism: `opaque {}` *means* "a type whose size/layout is unknown"; a field declares a layout, so opaque-with-fields is a contradiction and 0.15.2 correctly forbids it (declarations remain legal). `c_allocator` calls libc `malloc`/`free`, which a `wasm32-freestanding` guest has no business linking. |
| 72 | + - non-cause-ruled-out: this is NOT a Zig regression (the change is load-bearing type discipline, by design — nothing to fix upstream) and NOT a defect in the live SNIF guests (they never used these patterns and build clean). The bustedness is entirely contained in the dead template. |
| 73 | +- recognition: treat Zig 0.15.2's tightening as type discipline to CONFORM TO, not work around. If this template is ever rendered + built, use the opaque-handle idiom (a concrete `struct`, hand C an `*anyopaque` / `*Handle` token, recover via `@ptrCast`/`@alignCast`) and a freestanding allocator (`FixedBufferAllocator` / page-style over a static buffer) — never `c_allocator` at the wasm32-freestanding boundary. Early signal it is about to bite for real: anyone rendering the `{{project}}` placeholders or wiring `src/interface/ffi/` into a build/CI step. |
| 74 | +- graduates_to_failure_mode_if: the ffi scaffold is rendered and wired into a real build/gate — at which point "ffi guest won't compile under the toolchain" becomes a live Failure Mode deserving a recovery contract. |
| 75 | +- notes: companion to the `SCAFFOLD` banner atop `src/interface/ffi/src/main.zig` (extended 2026-06-16 with this Zig-0.15.2 note) and PROOF-STATUS.md "Scaffold (NOT counted, NOT gated)". The same pattern is genuinely *bust* in typed-wasm — there it is a real failure, here a recognised near-hit. |
0 commit comments