SNIFs 2: sharpen SEC-1 (deniability + taxonomy), gate the buffer ABI, behaviour gate + AFFIRMATION + Bustfile near-hit (#39)

## Summary

SNIFs 2 — sharpened verification, a ground-truthed honesty snapshot, and
a recorded near-hit. Signed commits (`id_ed25519_signing`, all
`signed=G`):

- **a82bb31** — the work
- **e60a94c** — `AFFIRMATION.adoc` (anchored to `a82bb31`; **parent ==
anchor**)
- **32bbe33** — Bustfile near-hit (Zig 0.15.2) + scaffold-banner note

### SEC-1 — operational crash-isolation (Agda `--safe --without-K`)
- **F1**: confidentiality wired into the operational run (`run-deniable`
/ `fault-via-observe` + a two-distinct-secret `SecretWitness`).
- **F2**: real 6-origin error taxonomy (`TrapOrigin`
guestFault/hostBudget/preExec + a `call` front-end + `PreExecWitness`).
- **F5**: non-trivial-`Alive` recovery witness (`PartialAlive`).
- All **mutation-confirmed load-bearing** by a 4-skeptic adversarial
re-audit (every targeted mutation rejected; `--safe` enforced;
`run`/`drive` totality real).

### ABI-7 + CI-1 + GAP-1b
- `BufferAbi.idr` models all 7 `buffer_abi` exports
(multi-value/void-faithful) → **15/20** Zig export sites gated;
guest-aware `abi_conformance.py`.
- Conformance now runs as a CI job in `proofs.yml`.
- `snif_metamorphic_test.exs` — dep-free metamorphic relations over the
scalar kernels; surfaced + corrected the `checked_add` wrapping-vs-name
misnomer.

### Honesty + aetiology
- `AFFIRMATION.adoc`: ground-truthed snapshot; **Safer-not-Safe**
(SEC-1-TCB trusted), ABI-7 15/20, GAP-1b scalar-only all stated.
- `docs/templates/contractiles/bust/Bustfile.a2ml`: the Zig-0.15.2
ffi-template breakage as a **near-hit** (recognition, not a fix) —
by-design type discipline; inert here (dead scaffold), genuinely *bust*
in typed-wasm.

## Verification (green at `a82bb31`)
- `just proof-check-all` → exit 0 (10 gated artifacts)
- `just abi-conformance` → 15 specs / 2 guests
- `mix test` → 30/30 (OTP 25)

## Base-branch note (flagged, not swept in)
This branch sits on the owner's pre-existing local commit **913d141**
("restore third-party vendored deps to pristine upstream licences") —
the branch HEAD when this work began, not yet on `main`. It is a
**licence** commit and the owner's own work; included here **with
explicit owner permission for this PR**, called out openly. Rebasing it
out was avoided deliberately because it would rewrite `a82bb31` and
break the AFFIRMATION's anchor.

## Owner follow-ups (not in this PR)
- Make `abi-conformance` a **required** status check (branch-protection,
owner-only).
- Zenodo DOI still carries the old "Safe" title (next deposit).
- Decide whether to **rename** the `checked_add` export (comment
corrected; name kept).

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

Author: hyperpolymath

.github/workflows/proofs.yml

@@ -0,0 +1,81 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Proof gate for SNIFS: machine-checks the formal verification artifacts.
+# If this gate is red, the repo's "proven" claim is void. It replaces the
+# previously decorative `just proof-check-*` targets, which silently passed when
+# the prover was absent (SKIP = exit 0) and used a broken idris2 invocation that
+# never resolved the ABI.* module graph — so the proofs were never actually checked.
+#
+# Toolchain is provided via Nix (nixpkgs#idris2, nixpkgs#lean4) — estate-standard,
+# reproducible, and avoids unpinned setup actions. NOTE: this consumes CI minutes;
+# if/when the bag-of-actions migration lands, this gate should move onto owned compute.
+# To make it BLOCKING, add the job names "Formal proofs — Idris2 + Lean4" AND
+# "ABI conformance — interface drift gate" to branch-protection required status
+# checks (owner-only). The ABI job (added 2026-06-16, SNIFs 2) builds the wasm
+# guests and fails if their real export signatures drift from the verified Idris2
+# ABI model (Foreign.idr + BufferAbi.idr) — closing the gap-1 interface gate in CI
+# instead of only on a local `just abi-conformance`.
+
+name: Proof Gate
+on:
+  push:
+    branches: [main, master, develop]
+    paths:
+      - 'verification/**'
+      - 'zig/**'
+      - 'Justfile'
+      - '.github/workflows/proofs.yml'
+  pull_request:
+    branches: [main, master]
+    paths:
+      - 'verification/**'
+      - 'zig/**'
+      - 'Justfile'
+      - '.github/workflows/proofs.yml'
+  workflow_dispatch:
+permissions: read-all
+concurrency:
+  group: proofs-${{ github.ref }}
+  cancel-in-progress: true
+jobs:
+  proofs:
+    name: Formal proofs — Idris2 + Lean4
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
+
+      - name: Install Nix (Determinate installer)
+        run: |
+          curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix \
+            | sh -s -- install --no-confirm
+
+      - name: Check Idris2 + Lean4 proofs (fail-on-skip, real invocation)
+        run: |
+          . /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh
+          nix shell nixpkgs#idris2 nixpkgs#lean4 nixpkgs#agda nixpkgs#just \
+            --command bash -c 'just proof-check-all'
+
+  abi-conformance:
+    name: ABI conformance — interface drift gate
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
+
+      - name: Install Nix (Determinate installer)
+        run: |
+          curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix \
+            | sh -s -- install --no-confirm
+
+      - name: Build wasm guests + check ABI signatures vs the verified Idris2 model
+        run: |
+          . /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh
+          # Zig 0.15+ is required (matches the repo toolchain + the safe_nif/buffer_abi build
+          # flags). The recipe builds both guests, then the multi-guest conformance tool fails
+          # on any export-signature drift from Foreign.idr / BufferAbi.idr.
+          nix shell nixpkgs#zig nixpkgs#wasm-tools nixpkgs#python3 nixpkgs#just \
+            --command bash -c 'just abi-conformance'

.github/workflows/rust-guest-verify.yml

@@ -0,0 +1,61 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Rust SNIF guest: build + verifier-on-by-default gate (ADR-0005).
+# Fail-closed. The source verifier (Kani) runs as a standard build step.
+name: Rust SNIF guest verify
+on:
+  push:
+    branches: [main, master]
+    paths: ["rust/**", ".github/workflows/rust-guest-verify.yml"]
+  pull_request:
+    paths: ["rust/**", ".github/workflows/rust-guest-verify.yml"]
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: rust
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Toolchain + wasm32 target
+        run: |
+          rustup toolchain install 1.95.0 --profile minimal
+          rustup default 1.95.0
+          rustup component add clippy
+          rustup target add wasm32-unknown-unknown
+
+      # ── Static gates (run for free) ────────────────────────────────────
+      # #![forbid(unsafe_code)] on snif-logic and #![deny(unsafe_code)] on the
+      # others are enforced by these compiles.
+      - name: Build guest (ReleaseSafe invariant from [profile.release])
+        run: cargo build --release --target wasm32-unknown-unknown
+
+      - name: wasm validate + assert ZERO imports (self-contained sandbox)
+        run: |
+          W=target/wasm32-unknown-unknown/release/demo_guest.wasm
+          cargo install wasm-tools --locked || true
+          wasm-tools validate "$W"
+          if wasm-tools print "$W" | grep -q '(import'; then
+            echo "::error::guest has imports — not self-contained"; exit 1
+          fi
+
+      - name: Clippy (pedantic, warnings = errors)
+        run: cargo clippy --all-targets -- -D warnings -W clippy::pedantic
+
+      - name: Supply-chain (bans rustler stack)
+        run: |
+          cargo install cargo-deny --locked || true
+          cargo deny check
+
+      # ── The source verifier: verifier-on-by-default ────────────────────
+      - name: Kani (proves snif-logic harnesses)
+        run: |
+          cargo install --locked kani-verifier || true
+          cargo kani setup || true
+          cargo kani -p snif-logic

.machine_readable/META.a2ml

@@ -3,7 +3,7 @@
 
 (meta
   (project "snif")
-  (full-name "SNIFs: Safe Native Implemented Functions for the BEAM via WebAssembly Sandboxing")
+  (full-name "SNIFs: Safer Native Implemented Functions for the BEAM via WebAssembly Sandboxing")
   (license "MPL-2.0")
   (author "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>")
   (architecture-decisions

.machine_readable/contractiles/bust/Bustfile.a2ml

@@ -0,0 +1,75 @@
+# SPDX-License-Identifier: MPL-2.0
+# Bustfile — design-aetiology / "bust" contract for snifs
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Paired runner: bust.ncl   (NOT YET PRESENT — paired .ncl runners are an
+#                            estate-wide gap; cf the Adjustfile contractile-sync
+#                            check. Do not assume a runner exists.)
+# Verb:          bust
+#
+# Semantics: BUST is about *broken* — the slang "damn, this thing is bust".
+#            It records WHY things break (or nearly broke), cause-first, as
+#            design aetiology — causal help/error/removal, NOT a bandaid that
+#            suppresses the symptom. (Sibling: DUST = exnovation, the clean
+#            reduction-to-dust / deliberate removal of a thing.)
+# Run with:  bust check    (list failure modes + recovery status)
+# Fix with:  bust fix      (apply the causal recovery where deterministic; advisory otherwise)
+
+@abstract:
+The snifs Bustfile in two disjoint halves.
+
+  ## Failure Modes  — OPEN, actionable defect contracts: a class that CAN break,
+  each pairing a detection probe with a causal recovery. This is the half a
+  `bust` runner / k9 gate would drill (declared -> drilled -> verified | failing).
+
+  ## Near-Hit Cases — CLOSED, non-actionable recognition records: something that
+  COULD have bitten but DID NOT, written down with its aetiology so future work
+  recognises the same shape rather than re-stumbling into it. A near-hit is NOT a
+  defect, has no recovery to drill, and must never be auto-promoted into a Failure
+  Mode (that would invent an open issue from a non-issue). It only graduates by an
+  explicit human decision.
+@end
+
+## Failure Modes
+
+### releasefast-guest-silent-wrong-answers
+- 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.
+- 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, _}`.
+- probe: ! grep -qE 'optimize *= *\.(ReleaseFast|ReleaseSmall)' zig/src/*.zig build.zig 2>/dev/null  # shipped guest must be ReleaseSafe
+- probe: just abi-conformance  # + a differential corpus: ReleaseSafe vs ReleaseFast must AGREE on edge inputs — divergence == this mode firing
+- 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.
+- severity: critical
+- status: declared
+
+### wasmex-nif-guest-load-failure
+- 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.
+- 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.
+- probe: just abi-conformance  # signature drift gate (safe_nif + buffer_abi vs Foreign.idr / BufferAbi.idr)
+- probe: cd demo && mix test    # host-side instantiate + call; must not be {:error, _} for the happy path
+- 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.
+- severity: critical
+- status: declared
+
+## Near-Hit Cases
+
+# RECOGNITION LEDGER — read, do not drill. Entries here are NOT defects and NOT
+# merge-gated. A `bust` runner / k9 gate binds ONLY to "## Failure Modes" above.
+# Do not migrate these into Failure Modes; promotion is a human decision via the
+# entry's `graduates_to_failure_mode_if:` trip-condition.
+
+### zig-0.15.2-opaque-with-fields-template-rot
+- kind: near-hit
+- status: recognised
+- not_an_issue: true
+- class: toolchain            # (extends the runner's failure-class enum; near-hits do not bind the runner)
+- 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.
+- 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.
+- 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).
+- aetiology:
+  - 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.
+  - 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.
+  - 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.
+  - 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.
+- 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.
+- 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.
+- 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.

.machine_readable/contractiles/dust/Dustfile.a2ml

@@ -0,0 +1,50 @@
+# SPDX-License-Identifier: MPL-2.0
+# Dustfile — exnovation contract for snifs
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Paired runner: dust.ncl   (NOT YET PRESENT — paired .ncl runners are an
+#                            estate-wide gap; cf the Adjustfile contractile-sync
+#                            check. Do not assume a runner exists.)
+# Verb:          dust
+#
+# Semantics: DUST is exnovation — the deliberate, CLEAN reduction-to-dust of a
+#            thing, "without the mess". Per component it declares a disposition
+#            (deprecate / untangle / dependency-exit / keep-forever) plus an
+#            explicit exit-condition, so a removal is a recorded decision with a
+#            trigger, never an ad-hoc deletion. (Sibling: BUST = broken — WHY
+#            things break.) Nothing here removes anything by itself.
+# Run with:  dust check    (list exnovation declarations + whether the exit-condition holds)
+# Fix with:  dust fix       (execute a declared exnovation only when its exit-condition is met)
+
+@abstract:
+Exnovation declarations for snifs. Each entry names a component, its disposition
+(deprecate / untangle / dependency-exit / keep-forever), the rationale, and the
+explicit exit-condition that must hold before the removal is carried out. This is
+the deliberate-retirement ledger; it states intent + trigger, it does not delete.
+@end
+
+## Exnovation Declarations
+
+### rsr-template-ffi-scaffold
+- target: src/interface/ffi/  (the unrendered rsr-template C-FFI tree, incl. src/main.zig, build.zig, test/integration_test.zig)
+- disposition: deprecate
+- rationale: dead scaffold — unrendered (`{{project}}` placeholders), wired into no build or gate, and would not compile under Zig 0.15.2 even if rendered (see the Bustfile near-hit `zig-0.15.2-opaque-with-fields-template-rot`). The real guest ABI is `zig/src/{safe_nif,buffer_abi}.zig` + `verification/proofs/idris2/ABI/*` + `abi_conformance.py`.
+- exit-condition: remove once the template-instantiation tooling (`tests/e2e/template_instantiation_test.sh`, `scripts/validate-template.sh`, `benches/template_bench.sh`) no longer requires the ffi scaffold present, OR once that tooling is itself retired. Until then KEEP as the untouched rsr-template baseline (it is harmless: it builds nothing).
+- status: declared
+- severity: advisory
+
+### orphan-rust-guest-wasm-artifact
+- target: priv/demo_guest_rust.wasm  (813-byte build artifact in the working tree)
+- disposition: dependency-exit
+- rationale: a stale built artifact NOT loaded by the demo — `SnifDemo.RustGuest` loads `rust/target/.../demo_guest.wasm`, not this. It is a generated leftover, not source. (`priv/*.wasm` is gitignored, so it is never committed.)
+- exit-condition: deletable from the working tree at any time; it is regenerated on demand from `rust/crates/demo-guest`. No source depends on this path.
+- status: declared
+- severity: advisory
+
+### keep-forever-dual-rust-guest-trees
+- target: rust/ (Cargo workspace, canonical) and rust-guest/ (standalone single-crate experiment)
+- disposition: keep-forever
+- rationale: NOT duplication-to-exnovate — owner-declared deliberate (see rust-guest/README.adoc + ADR-0005). The workspace `rust/crates/demo-guest` is the demo's guest; `rust-guest/` is the minimal proof-of-shape. Recorded here so a future hygiene sweep does not "dedupe" them.
+- exit-condition: none — explicit keep. Revisit only on owner instruction.
+- status: declared
+- severity: advisory