feat(verification): SNIFs 2 — sharpen SEC-1, gate the buffer ABI, add a behaviour gate

SEC-1 (SnifIsolation.agda): wire confidentiality into the operational theorem (deniability re-derived over the run via run-deniable/fault-via-observe + a two-distinct-secret SecretWitness), model the real 6-origin error taxonomy (TrapOrigin guestFault/hostBudget/preExec + a call front-end + PreExecWitness), and add a non-trivial-Alive recovery witness (PartialAlive). All mutation-confirmed load-bearing by a 4-skeptic adversarial re-audit (--safe --without-K, every targeted mutation rejected).

ABI-7: BufferAbi.idr models all 7 buffer_abi exports (multi-value/void-faithful WasmSig), raising gated ABI coverage to 15/20 Zig sites; abi_conformance.py is now guest-aware. CI-1: conformance runs as a CI job in proofs.yml. GAP-1b: snif_metamorphic_test.exs — dep-free metamorphic relations over the scalar kernels (found + corrected the checked_add wrapping-vs-name misnomer).

Reconcile: ffi rsr-template marked scaffold; PROOF-NEEDS.md rendered; the two Rust guest trees documented as deliberate. Docs (PROOF-STATUS/README/CHANGELOG) reconciled to the verified state.

Gate green this commit: just proof-check-all (exit 0), just abi-conformance (15 specs), mix test (30/30, OTP 25).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

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

CHANGELOG.md

@@ -13,3 +13,45 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 <!-- Run: just changelog -->
 
 ## [Unreleased]
+
+### Fixed
+- **Formal proofs now actually machine-check.** The 7 Idris2/Lean4 proofs were marked
+  "100% proven" since 2026-04-16, but `Foreign`/`Platform`/`Compliance` never compiled
+  (Idris2 unbound-implicit auto-binding; unary-`Nat` blow-up on 65536-scale arithmetic)
+  and no CI job ever ran a prover. All 6 Idris2 modules + the Lean4 module now pass.
+- **Justfile was unparseable by `just`** (line 2 used `//` instead of `#`), which broke
+  every recipe including `build-wasm` used by the e2e gate. Fixed.
+- **Proof gate was decorative.** `just proof-check-*` used a broken `idris2 --check`
+  invocation (no `--source-dir`, never resolved the `ABI.*` graph) and silently passed
+  when the prover was absent (SKIP = exit 0). Now uses the correct invocation and
+  fails-on-skip.
+- **`checked_add` doc-comment corrected.** The comment claimed "overflow -> trap" but the body is
+  `a +% b` (wrapping); the GAP-1b metamorphic gate surfaced the contradiction. The comment now
+  states the wrapping behaviour accurately (the trapping-overflow demo is `crash_overflow`); the
+  export name is unchanged.
+
+### Changed
+- Project gloss **"Safe NIFs" → "Safer NIFs"** (acronym SNIF unchanged): WASM sandboxing
+  makes NIFs *safer*, not provably *safe*. Living docs + paper/citation titles updated.
+  NOTE: the paper carries Zenodo DOI 10.5281/zenodo.19520245 under the old title — the
+  rename should be reflected on the next Zenodo version/deposit.
+- Re-modeled `Platform.idr` WASM memory-size facts over `Integer` (was unary `Nat`).
+
+### Added
+- `.github/workflows/proofs.yml` — real CI proof gate (Idris2 + Lean4 via Nix).
+- **SNIFs 2 — sharpened verification.** SEC-1 (`SnifIsolation.agda`) now wires confidentiality into
+  the operational theorem (deniability re-derived over the actual run via `run-deniable` /
+  `fault-via-observe` + a two-distinct-secret `SecretWitness`), models the real 6-origin error
+  taxonomy (`TrapOrigin` guestFault / hostBudget / preExec + a `call` front-end + `PreExecWitness`),
+  and adds a non-trivial-`Alive` recovery witness (`PartialAlive`) — all mutation-confirmed
+  load-bearing by a 4-skeptic adversarial re-audit (`--safe --without-K`, every targeted mutation
+  rejected).
+- **ABI-7 buffer-guest coverage.** `verification/proofs/idris2/ABI/BufferAbi.idr` models all 7
+  `buffer_abi` exports (multi-value/void-faithful `WasmSig`), raising gated ABI coverage to 15 of 20
+  Zig export sites; `verification/tools/abi_conformance.py` is now guest-aware (per-guest model
+  manifest, multi-value/void parsing). The conformance gate now runs in CI (`proofs.yml`, CI-1).
+- **GAP-1b behaviour gate.** `demo/test/snif_metamorphic_test.exs` — dependency-free metamorphic
+  relations over the scalar kernels (fibonacci recurrence + base cases; `checked_add` `wrap32`
+  oracle + boundary-wrap).
+- `AFFIRMATION.adoc` — point-in-time, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION
+  trio); SPDX header parked for the owner to add + sign.

CITATION.cff

@@ -1,5 +1,5 @@
 cff-version: 1.2.0
-title: "SNIFs: Safe Native Implemented Functions for the BEAM via WebAssembly Sandboxing"
+title: "SNIFs: Safer Native Implemented Functions for the BEAM via WebAssembly Sandboxing"
 authors:
   - family-names: Jewell
     given-names: Jonathan D. A.

EXPLAINME.adoc

@@ -4,7 +4,7 @@
 :toc: preamble
 :icons: font
 
-This file provides code-level evidence and implementation details for the SNIF (Safe Native Implemented Functions) architecture.
+This file provides code-level evidence and implementation details for the SNIF (Safer Native Implemented Functions) architecture.
 
 == Claim-to-implementation map
 
@@ -28,20 +28,53 @@ ____
 How this is implemented::
 The `Justfile` build recipes enforce `-OReleaseSafe` for all `priv/*.wasm` artifacts, ensuring that bounds checks are preserved in the binary.
 
-== Relationship to Groove/Cleave
+== Scope ceiling: a safer NIF, and nothing past it
 
-SNIFs provide the **Physical Cleave Surface**. While the **Groove Protocol** defines "how services talk" (communication), the SNIF architecture defines **"how they touch"** (integration). By sandboxing native code in WASM, we ensure that the "join" between high-performance logic and the safe host environment is mathematically isolated and safe to "split."
+SNIF deliberately stops at *NIF-parity + crash-isolation*. The goal is to **adapt and
+perfect something that already exists** — the BEAM NIF — for the people who already use
+NIFs: a safer, like-for-like drop-in for native compute/buffer functions (see the README
+`Scope` section), *not* a new interface paradigm. Capabilities that go **beyond** what a
+NIF offers — graduated/tunable integration, capability negotiation, transaction-gating,
+permissions that depend on an integration "mode" — are **out of SNIF scope by design**. If
+an idea is good but takes us past the NIF goal, it belongs to the *cleave* and *groove*
+layers below, and is considered there, not bolted onto SNIF.
 
-== Repository Future: The Universal Pattern Hub
+== Relationship to Groove and the Cleave
 
-Per the v0.5 reposystem roadmap, this repository is transitioning from an Elixir-only research project into the **Universal Pattern Hub** for all Safe Native Interfaces across the estate (Rust/SPARK, Zig, and Ada).
+Three distinct layers; SNIF is the most conservative of them:
+
+* **SNIF — _perfecting an existing interface._** A SNIF **realizes a residue-clean cleave
+  _instance_ at one boundary** (BEAM host ↔ native guest): a guest trap becomes
+  `{:error, reason}`, the BEAM survives, and the error residue carries no recoverable guest
+  value (the `SnifVerdict` deniability proofs). It is *an* instance of a cleave, **not "the
+  cleave"** — the earlier phrasing "SNIFs provide the Physical Cleave Surface" overstated
+  this and is corrected here.
+* **Cleave — _the new implementation of graduated integration._** A transmutable surface
+  you can dial from near-raw FFI-ABI, through the SNIF sandbox (the safe *middle detent*),
+  to a tight Groove-defined internal-api; closeable to a standalone secure surface. SNIF
+  sits at the middle; the rest of the dial (transaction-gating, mode-indexed permissions,
+  the well-founded "staircase" teardown) is **cleave scope, not SNIF scope**.
+* **Groove — _something new, to move beyond current interface design._** The protocol for
+  *how services talk*: capability discovery + typed capability negotiation, soft (pub/sub)
+  ↔ hard (in-process) integration modes. SNIF merely *consumes* Groove as a communication
+  counterpart, and only at the v0.2 roadmap level — snifs ships no Groove code today.
+
+== Multi-language guests (still within the safer-NIF goal)
+
+The safer-NIF pattern is realizable across guest languages — Zig today, Rust→wasm32 wired,
+Ada/SPARK and estate wasm-native languages (typed-wasm/ephapax/affinescript) prospective.
+This is *breadth of guest language within the NIF goal*, **not** an expansion of SNIF's
+purpose. SNIF is not a "universal interface hub"; that "beyond current interface design"
+ambition lives in groove/cleave, not here.
 
 == Evidence Index
 
 [cols="2,3", options="header"]
 |===
 | Path | Proves
-| `zig/src/safe_nif.zig` | Implementation of trapped failure modes.
-| `demo/test/snif_test.exs` | Integration tests verifying BEAM survival.
-| `manifest.scm` | Guix environment for reproducible WASM builds.
+| `zig/src/safe_nif.zig` | Implementation of trapped failure modes (8 exports, ABI-modelled).
+| `demo/test/snif_demo_test.exs` | Integration tests verifying BEAM survival across every crash mode.
+| `verification/proofs/agda/SnifIsolation.agda` | SEC-1 operational crash-isolation, proven-modulo-explicit-TCB.
+| `verification/proofs/agda/SnifVerdict.agda` | Residue-clean (deniability) + non-forgery at the boundary.
+| `verification/tools/abi_conformance.py` | Model↔binary ABI drift gate (interface-level).
 |===