Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
301 lines (257 loc) · 16.8 KB

AFFIRMATION.adoc

File metadata and controls

301 lines (257 loc) · 16.8 KB
Raw

AFFIRMATION — SNIFs (Safer NIFs), as of 2026-06-16

the No-Bullshit file: what we affirm was true and checkable at this moment

Note

Genre. An affirmation is a solemn declaration of the truth of a statement, made by someone who declines to swear an oath. That is exactly what this is: our truth-as-best-believed at a stamped instant — binding on our honesty, not a claim of infallibility. It is not the README and not the EXPLAINME:

File Answers Tense

README

Where is this going, and why? — what SNIF is, why care, quick start

future / aspirational

EXPLAINME

How is it built, and what’s the evidence? — claim-to-code mapping

descriptive / mechanism

AFFIRMATION (this file)

What can we honestly affirm was true and checkable at a stamped moment?

a frozen instant, falsifiable

It is deliberately small, dated, and signed, so a reader can hold us to exactly what we affirmed, when we affirmed it.
Table of Contents

What this is, and how it is designed to work

What it is. A short, dated, jointly-signed snapshot of what we can honestly and verifiably claim about this repo at one exact moment. Nothing here is marketing and nothing is a promise about the future — both of those live in the README. This file is the receipt.

How it is designed to work. Three moving parts make it trustworthy:

  1. Ground truth, not memory. Every claim below was produced by running the tool in the session that wrote this file — the proof checkers, the ABI conformance gate, and the in-BEAM test suite — on 2026-06-16. If a status doc or a memory said otherwise, the live run wins and we flag the contradiction.

  2. A frozen anchor. The file names the exact commit SHA, branch, UTC timestamp, working-tree delta, and toolchain (see Verifiable anchor), so "true" always means "true at this point". Move the SHA and the file becomes a draft until re-run.

  3. A real signature. It is landed by a signed git commit; that signature over this content at the anchored SHA is what makes the affirmation tamper-evident and attributable — not the prose alone.

We are fallible. We can be wrong, stale, or simply mistaken about our own work. This file is our best honest belief, not a proof of its own correctness. Treat it as a falsifiable claim, not gospel.

The epistemic contract (read this before you trust or attack)

This document records our best joint belief at the timestamp below. It is not a guarantee of correctness. We may be wrong. We may have missed something — a hole, a stale doc, or a proof that checks an idealised model we then fail to match in the running runtime.

No intentional overclaim. That is the only guarantee here: we have not knowingly inflated anything. Where something is tested-but-not-proved, we say so. Where a proof covers a model and trusts the real runtime, we say so. Where something is ledgered, weak, or merely-an-interface-check, we say so. An honest claim here that turns out false is an error to fix — not a lie.

Standing invitation to refute. You are invited to bulldoze any claim in this file. The fair form of the attack is:

  1. Read this file at the stamped commit.

  2. Reproduce (or fail to reproduce) the checks in Reproduce it yourself.

  3. Then tell us where the discrepancy is, against the artefact as it stood at this moment — so we can either justify it or concede it on the record.

An attack that skips steps 1–2 is attacking a strawman of a different date.

No fights before the facts are cleared up. We are not interested in a dispute over a claim until the discrepancy has actually been checked against the artefact at this commit and we have had the chance to either justify it or concede it on the record. Good faith both ways: bring a reproducible discrepancy and we will fix the claim, the doc, or the code — promptly and without defensiveness. The goal is a corrected record, not a won argument.

Verifiable anchor

Repo

hyperpolymath/snifs (Safer NIFs — native compute for the BEAM via a wasmtime sandbox)

Branch

main (anchor is current main HEAD; this refresh is landed by a child commit via a docs PR)

Commit (HEAD / anchor)

70d9f65fd2a57f216f35636f09cadbb3c5ca87c1 — main after PR #39 (the SNIFs 2 work + the prior affirmation) and PR #40 (checked_add made genuinely checked). This refreshed AFFIRMATION is landed by a signed child of this commit, so parent == anchor SHA.

Permalink

https://github.com/hyperpolymath/snifs/tree/70d9f65fd2a57f216f35636f09cadbb3c5ca87c1

Verified (UTC)

2026-06-16T15:03:15Z

Toolchain

Idris2 0.8.0 · Lean 4.13.0 · Agda 2.8.0 · Zig 0.15.2 · wasm-tools 1.249.0 · Elixir 1.18.4 / Erlang OTP 25 · wasmex 0.14.0 · Python 3.12.3 · just 1.50.0
Note

State at this anchor (a REFRESH). This supersedes the first affirmation (anchored to a82bb31, landed in PR #39), which correctly described checked_add as a wrapping misnomer at that moment. Since then PR #40 made checked_add genuinely checked (overflow traps), so this refresh is re-anchored to main HEAD 70d9f65, which carries the full SNIFs 2 verification plus that change — all committed and merged (signed, id_ed25519_signing). The gate results below were re-run against this main checkout at the verified UTC above. Build artifacts (priv/.wasm, .agdai, zig/buffer_abi_build/) are intentionally not committed — CI rebuilds them. This AFFIRMATION is landed by a signed child of the anchor; if its parent SHA matches the anchor and the commit verifies, it is anchored. Move HEAD past it and re-run Reproduce it yourself before trusting it.

Companion documents and repo metadata (cross-check)

This affirmation should be read against the repo’s own public claims. Where they drift from what we verified, we say so here rather than leave the reader to find out.

  • README.adoc — present. "SNIFs: Safer Native Implemented Functions for the BEAM via WebAssembly Sandboxing". Sells the vision + the scope ceiling; this file is its receipt for one moment.

  • EXPLAINME.adoc — present. Maps README claims to code paths and carries the corrected "SNIF realizes a cleave instance, not the cleave" framing. The estate trio (README / EXPLAINME / AFFIRMATION) is complete for this repo once this file lands.

  • PROOF-STATUS.md / PROOF-NEEDS.md — the living ledgers this snapshot cites, reconciled to the verified state in the anchor commit: PROOF-STATUS.md now counts 10 gated artifacts, marks SEC-1 F1/F2 RESOLVED (keeping F3/F4/F5 as standing precision notes), and records ABI-7 at 15/20 + CI-1 done.

  • GitHub repo description — corrected this session to "SNIFs: Safer Native Implemented Functions for the BEAM via WebAssembly Sandboxing" (it previously said "Safe"; the project renamed "Safe NIFs" → "Safer NIFs" — see CHANGELOG — because the end-to-end guarantee is not unconditional, see The honest nuance you must not lose).

  • GitHub topics — beam, elixir, erlang, fault-tolerance, nif, research, wasmtime, webassembly, crash-isolation. Under-claim: there is no formal-verification topic, although the repo now carries 10 machine-checked proof artifacts + a machine-checked operational isolation theorem. The tags undersell the verification rather than oversell it.

The honest state (one breath)

SNIFs is a working, machine-verified "safer NIF" for the BEAM: native compute/buffer functions compiled to WebAssembly and run in a wasmtime sandbox, so a guest fault becomes a catchable {:error, _} and the BEAM survives. The in-BEAM demo is green, the formal gate is green (including an operational crash-isolation theorem with deniability and a 6-origin error taxonomy wired in), and the interface + a slice of behaviour are gated against the real built wasm — yet it remains "Safer", not "Safe": one explicit runtime-faithfulness assumption is trusted, not yet machine-discharged, and several coverage items are honestly ledgered.

What is solid (and how we checked)

  • The formal gate is green — verified this moment. just proof-check-all → exit 0: 7 Idris2 modules (Types, ABI/{Layout,Platform,Pointers,Foreign,Compliance,BufferAbi}), 1 Lean4 (ApiTypes), 2 Agda (SnifVerdict, SnifIsolation, both agda --safe --without-K), plus the dangerous-pattern scan (no believe_me/postulate/sorry/Admitted).

  • SEC-1 — the operational crash-isolation theorem — typechecks. verification/proofs/agda/SnifIsolation.agda proves, by induction over a fuelled host↔guest small-step model: verdict ∈ ok ⊕ trap, host survives every outcome, the trap carries no guest value, and — newly wired into the operational run — the fault residue is the redacted secret only, so two faults with equal redaction are host-indistinguishable (run-deniable). The verdict now models the real 6-origin taxonomy (guest-fault / host-budget / pre-exec) via a call front-end, not a binary trap. It is proven modulo an explicit FaithfulRuntime record hypothesis (the TCB) — see The honest nuance you must not lose.

  • Interface conformance is gated against the real binaries. just abi-conformance → exit 0: 15 ABI specs across 2 guests (safe_nif 8, buffer_abi 7) — the built wasm’s real export signatures match the verified Idris2 model exactly, including three void-returning buffer exports.

  • In-BEAM behaviour runs. mix test (in demo/) → 30 tests, 0 failures on Erlang/OTP 25, Elixir 1.18.4, with the precompiled wasmex 0.14 NIF. This includes crash isolation across every failure mode (OOB / unreachable / @panic / overflow / div-zero → {:error,_}, BEAM alive after each) and a new dependency-free metamorphic behaviour gate over the numeric kernels.

The honest nuance you must not lose

  1. "Safer", not "Safe" — the runtime TCB is trusted, not proven. SEC-1 is proven over a model whose first argument is a FaithfulRuntime record bundling primitive single-step facts (wasmtime never gets stuck; a trapped step is caught and surfaced as {:error,} with the scheduler preserved). The prose claim that this record is _faithful to wasmtime/wasmex — "wasmtime ⊨ FaithfulRuntime" — is assumed, not discharged in a prover (it is the named open item SEC-1-TCB, a WasmCert-Coq effort). This residual assumption is exactly why the project is Safer NIFs.

  2. Model ↔ code faithfulness is only partly mechanised. The proofs verify a logical model. The ABI conformance gate closes the interface slice of model↔code (signatures match the real wasm); the metamorphic tests close a behaviour slice (the kernels behave as modelled). The general claim "the Agda model mirrors the Zig/Rust/wasmex code" is argued + tested, not itself machine-verified.

  3. Honest proof labels (not over-claims). In SEC-1, okOrTrap and noForgery are structural facts about the Verdict datatype (true with no runtime in scope); the load-bearing, TCB-consuming content is host preservation (survives). noForgery is the parametric non-existence of a total extractor, not an instance-level claim. We state these rather than dress them up.

Known-incomplete but honestly fenced (loud failure, never silent miscompile)

  • The isolation thesis depends on building guests with -OReleaseSafe. Under -OReleaseFast the same faults become silent wrong answers — this is demonstrated, on purpose, as the negative control in the demo suite (e.g. an OOB read returns a plausible adjacent value). The shipped guests are ReleaseSafe; the ReleaseFast artifact exists only to keep that danger visible and tested.

Outstanding / weak / refuted (no spin)

  • SEC-1-TCB — open. Discharging "wasmtime ⊨ FaithfulRuntime" in-prover (WASM trap-soundness; trap → {:error,_}; scheduler resumed) is the remaining half of an end-to-end isolation proof. Not started here.

  • ABI-7 — partial. 15 of ~20 Zig export sites are modelled+gated (safe_nif
    buffer_abi). burble_fft (fft/ifft/…) is not built into any artifact and uses (ptr,len) slice marshalling = the deeper ABI-6 obligation; it and the two Rust guests are ledgered, not gated (PROOF-NEEDS.md).

  • GAP-1b — partial. The metamorphic behaviour gate covers the scalar kernels (fibonacci recurrence/monotonicity/i64-width; checked_add overflow-traps / exact-sum oracle); the buffer kernels (sum_f32 permutation-invariance, scale-then-sum) are the next increment.

  • Finding surfaced by the gate — now RESOLVED. The gate first showed checked_add was a misnomer — a two’s-complement wrapping a +% b, not a checked add. It was made genuinely checked in PR #40: overflow now traps (@addWithOverflow
    unreachable → WASM trap → {:error,_}, BEAM survives), exact sum otherwise, and the metamorphic oracle was flipped to match. Name and behaviour now agree.

  • CI — now required. The ABI conformance gate runs as a CI job (proofs.yml) and is now a required status check on main (branch-protection), so interface drift blocks merge.

  • Adversarial mutation re-audit — completed, verdict SOLID. Four independent skeptics mutation-tested the SEC-1 sharpening (--safe --without-K): every targeted mutation was rejected as expected, so F1 (lossy redaction), F2 (the pre-exec coverage + the guestFault tag) and F5 (the partial Alive) are genuinely load-bearing — not vacuous; --safe is enforced (an injected postulate is rejected) and run/drive totality is real (a non-decreasing-fuel mutation is rejected). The only weakness it found was stale prose, corrected in the anchor commit.

  • Required-check + Zenodo. Making the conformance gate a required status check is owner-only branch-protection (pending). The paper’s Zenodo DOI still carries the old "Safe" title; the rename should land on the next deposit.

Reproduce it yourself

From the repo root, at the anchor commit above (you need the toolchain in Verifiable anchor):

just proof-check-all     # expect exit 0:
                         #   7 Idris2 OK, 1 Lean4 OK, 2 Agda OK (SnifVerdict + SnifIsolation),
                         #   dangerous-pattern scan PASS
just abi-conformance     # expect exit 0: builds safe_nif + buffer_abi wasm, then
                         #   "all 2 guest(s) conform (15 ABI specs verified ...)"
cd demo && mix test      # expect "30 tests, 0 failures" (OTP 25 / Elixir 1.18.4)

For the SEC-1 proof on its own (the exact gate invocation):

agda -i verification/proofs/agda --safe --without-K --no-libraries \
     verification/proofs/agda/SnifIsolation.agda     # expect exit 0

One-line characterisation (quote this)

"A working, machine-verified Safer NIF for the BEAM: native compute sandboxed in wasmtime so a guest fault becomes {:error,_} and the VM survives — with an operational crash-isolation theorem (deniability + 6-origin taxonomy, Agda --safe), an interface gate matching 15 export signatures to the real wasm, and a behaviour gate over the scalar kernels — all green this moment; Safer not Safe because one runtime-faithfulness assumption is trusted, not yet proven, and burble_fft/Rust/buffer-behaviour coverage is honestly ledgered. No intentional overclaim."

Joint attestation

We, the undersigned, assert that to the best of our joint belief at the timestamp above, every claim in this file is true and was checked as described — with no intentional overclaim, and with the open gaps stated rather than hidden.

  • Engineering party (AI): Claude Opus 4.8 (claude-opus-4-8[1m]) — ran the proof gate, the ABI conformance gate, and the in-BEAM test suite recorded here on 2026-06-16T15:03:15Z (against main at the anchor state) and stands behind the wording above as a faithful report of those runs.

  • Owner / maintainer: Jonathan D.A. Jewell — signs by committing this file with -S (id_ed25519_signing); the git commit signature over this content, whose parent is the anchor SHA recorded above, is the cryptographic form of this affirmation.

    Signed-off-date: 2026-06-16

Tip
 The authoritative, tamper-evident signature is the signed git commit that lands this file; its parent is the anchor SHA 70d9f65. If that parent matches Verifiable anchor and the commit verifies (id_ed25519_signing), this affirmation is anchored. If HEAD later moves past it, re-run Reproduce it yourself and write a fresh affirmation rather than trusting a stale one.