Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
123 lines (97 loc) · 5.83 KB

EXPLAINME.adoc

File metadata and controls

123 lines (97 loc) · 5.83 KB
Raw

SNIFs — EXPLAINME

This file provides code-level evidence and implementation details for the SNIF (Safer Native Implemented Functions) architecture.

Table of Contents

Claim-to-implementation map

Crash Isolation

Any crash in a NIF normally kills the entire BEAM VM…​ WebAssembly sandboxing provides genuine crash isolation.

— README.adoc
How this is implemented

We use wasmex to load Zig-compiled WASM modules. The demo/ folder contains tests that trigger null-pointer dereferences and overflows in the Zig guest; the host Elixir process receives a standard error tuple instead of a segmentation fault.

Deterministic Safety

Always compile Zig WASM with -OReleaseSafe.

— README.adoc
How this is implemented

The Justfile build recipes enforce -OReleaseSafe for all priv/*.wasm artifacts, ensuring that bounds checks are preserved in the binary.

Scope ceiling: a safer NIF, and nothing past it

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.

Relationship to Groove and the Cleave

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

Path Proves

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).

Dogfooded Across The Account

Technology / Pattern Used here Also used in

Idris2 ABI / capability proofs

verification/proofs/idris2/ABI/ models each guest’s export signature; the conformance gate fails on model↔binary drift.

bag-of-actions (capability Protocol.idr), proven (Idris2 proven-library)

Zig → wasm32-freestanding (-OReleaseSafe) guests

The SNIF kernel (zig/src/safe_nif.zig) compiles to a trapping wasm guest — UB becomes a trap, not a silent wrong answer.

bag-of-actions (estate.zig FFI), gossamer (Zig ABI)

--safe machine-checked proofs

SEC-1 crash-isolation is mechanised in --safe --without-K Agda (SnifIsolation.agda).

echo-types (loss-with-residue, constructive Agda)

Known gaps

Caution

SEC-1 is proven modulo an explicit TCB. The crash-isolation theorem holds relative to the FaithfulRuntime record hypothesis (the wasmtime/wasmex runtime behaves as modelled). This is an honest assumption boundary, not a postulate — see PROOF-STATUS.md for the trusted-base statement.
Caution

ABI conformance gates 15 of ~20 Zig export sites. buffer_abi is fully modelled (7/7); safe_nif coverage is partial. Tracked in PROOF-NEEDS.md (ABI-7).
Caution

The Rust→wasm32 guest path is wired but dual-sourced. rust/crates/demo-guest (workspace) and rust-guest/ (standalone) are not yet reconciled; the exit/keep decision is recorded in the repo’s Dustfile.