|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += snifs De-template Tidy — Continuation Guide |
| 4 | +:toc: preamble |
| 5 | +:icons: font |
| 6 | + |
| 7 | +Guide for any agent or maintainer continuing the snifs repository de-templating |
| 8 | +effort. The durable parts (rules, method, gotchas) below do not go stale; the |
| 9 | +live PR state in <<state>> is a dated snapshot — always re-check `gh pr list` and |
| 10 | +`git log --oneline -15` first. The full, evolving plan lives in |
| 11 | +`~/developer/dev-notes/2026-06-16-snifs-phase2-detemplate-plan.adoc`. |
| 12 | + |
| 13 | +== What snifs is (don't misframe it) |
| 14 | + |
| 15 | +SNIF = *Safer NIF*. Native code (Zig today, Rust wired) is compiled to |
| 16 | +`wasm32-freestanding` with `-OReleaseSafe` and run under `wasmtime` via `wasmex`, |
| 17 | +so a guest trap becomes a catchable `{:error, reason}` and the BEAM survives. It is |
| 18 | +a *research + reference repository* (architecture paper + working BEAM/WASM |
| 19 | +implementation + formal proofs), *not* an installable app. It is one realized point |
| 20 | +on the `cleave` dial — not "the cleave"; keep cleave/groove ambitions out. |
| 21 | + |
| 22 | +Ground-truth numbers (verify before repeating any claim): *21/21* in-BEAM ExUnit; |
| 23 | +*10* machine-checked proofs (6 Idris2 ABI + 1 Idris2 core + 1 Lean4 + 2 Agda); ABI |
| 24 | +conformance gates *15 of 20* Zig sites; `zig/src/safe_nif.zig` has *8 exports of |
| 25 | +which 5 are `crash_*`*. "Six crash modes", "11/11", or "7 proofs" = stale. |
| 26 | + |
| 27 | +[[state]] |
| 28 | +== Live state — snapshot 2026-06-17 (re-verify with `gh pr list`) |
| 29 | + |
| 30 | +[cols="1,2,3", options="header"] |
| 31 | +|=== |
| 32 | +| PR | Branch | Scope |
| 33 | +| #42 | `chore/repo-tidy-2026-06-16` | A–D tidy + safe-subset identity (11 commits) |
| 34 | +| #43 | `fix/manifest-parent-pointers` | WP-1: 5 manifest parent pointers |
| 35 | +| #44 | `chore/identity-snif-to-snifs` | WP-2: snif/rsr-template-repo → snifs (20 files) |
| 36 | +|=== |
| 37 | + |
| 38 | +All disjoint, signed, awaiting owner merge (admin-merge is owner-only). WP-1 and |
| 39 | +WP-2 done. WP-3 (CLADE clade-prefix) *dropped by owner decision* — leave the |
| 40 | +`[clade]` block in `.machine_readable/CLADE.a2ml` as-is. |
| 41 | + |
| 42 | +== Hard rules — non-negotiable |
| 43 | + |
| 44 | +. *Licence / SPDX = owner-only, flag-only.* Never auto-edit a LICENSE file, an |
| 45 | + `SPDX-License-Identifier`, or relicense — even if policy-correct. PMPL is forbidden |
| 46 | + outside `palimpsest-license` / `palimpsest-plasma` / `consent-aware-http`. |
| 47 | + `AFFIRMATION.adoc`'s dual `MPL-2.0 OR CC-BY-SA-4.0` is correct — leave it. |
| 48 | +. *Sign every commit:* `git commit -S` with `id_ed25519_signing` (NEVER the auth-only |
| 49 | + `id_ed25519`). Verify with `git verify-commit HEAD`. Never `--no-verify`. |
| 50 | +. *Keep the pre-commit hook strict.* It checks staged A/M files matching |
| 51 | + `\.(zig|ex|idr|eph|py|js|ts|rs|c|h|adoc|md)$` for *both* `SPDX-License-Identifier: |
| 52 | + MPL-2.0` *and* the literal `Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>`. |
| 53 | + `.a2ml`/`.toml`/`.yml`/`.txt`/deletions/renames are exempt. It also bars raw NIFs |
| 54 | + and C files. |
| 55 | +. *Stop before anything outward-facing.* Build and commit locally freely; STOP before |
| 56 | + push / PR / merge and let the owner decide. |
| 57 | +. *Scope discipline.* Do exactly the approved work-package. When you find more drift |
| 58 | + (you will), flag it — don't sweep it. |
| 59 | +. *Look before you delete or overwrite.* This bit twice already (a "paper stub" was a |
| 60 | + full superseded paper; a "placeholder MAINTAINERS" was filled). If a target |
| 61 | + contradicts how it was described, re-surface to the owner. Deletions are owner-gated, |
| 62 | + per file. |
| 63 | + |
| 64 | +== Remaining work |
| 65 | + |
| 66 | +*WP-4 — load-bearing config (its own PR; re-verify after).* |
| 67 | + |
| 68 | +* Root `Justfile`: `project := "rsr-template-repo"` → `snifs` (*16 `{{project}}` |
| 69 | + interpolation sites* — `just --list` + smoke recipes after); retarget help/tour/issues |
| 70 | + URLs; fix the self-check (~line 337) + template-derivation message (~870). `REPO :=` |
| 71 | + is defined but unused. |
| 72 | +* Contractile `Mustfile`/`Trustfile`/`Intentfile`/`Adjustfile` + generated `Justfile`: |
| 73 | + de-brand prose, and fix the two self-contradicting Mustfile checks — |
| 74 | + `no-placeholder-values` over-matches just-syntax `{{recipe}}` (scope to `{{[A-Z_]+}}`), |
| 75 | + and `template-readonly` greps a `RSR_TEMPLATE_DO_NOT_EDIT` marker that no longer exists |
| 76 | + (remove/repurpose). *Fix the check, never the repo, to satisfy a stale gate.* |
| 77 | + |
| 78 | +*WP-5 — deletions + format (its own PR; per-file owner approval).* |
| 79 | + |
| 80 | +* `docs/QUICKSTART.adoc` (dup of the root `QUICKSTART-*.adoc` trio) → delete. |
| 81 | +* `.machine_readable/ai/PLACEHOLDERS.adoc` (the init recipe says `rm` it) → delete. |
| 82 | +* `docs/RSR_OUTLINE.adoc` (pure template doc) → delete or rewrite as a snifs outline. |
| 83 | +* `READINESS.md` → `READINESS.adoc` (convert + fill `{{DATE}}` + snif→snifs). |
| 84 | + |
| 85 | +*Open decisions (get from owner before executing):* D-a (keep/remove bootstrap |
| 86 | +tooling: `scripts/validate-template.sh`, `setup.sh`, self-validating `k9` examples), |
| 87 | +D-c (Mustfile-check fix approach), D-d (confirm WP-5 deletions + RSR_OUTLINE |
| 88 | +delete-vs-rewrite), D-e (`docs/decisions/0000-template.adoc` keep-vs-neutralize), |
| 89 | +D-f (`docs/governance/` subtree numbering: normalize vs promote to root pillar). |
| 90 | + |
| 91 | +*Already deferred / flagged (don't silently absorb):* `docs/whitepapers/academic/snif.tex` |
| 92 | +(two `\url{}` → `snif`; published DOI'd paper — owner action: fix + `just paper` rebuild + |
| 93 | +re-deposit); the non-identity `{{PLACEHOLDER}}`s in `container/`/`security.txt`/`dep5` |
| 94 | +(separate fill task); `llm-warmup-*.md` thin boilerplate (phantom `just setup`); |
| 95 | +`.machine_readable/STATE.a2ml` stale overall. |
| 96 | + |
| 97 | +== Method that has worked |
| 98 | + |
| 99 | +. Cut every branch from *fresh `origin/main`* (`git fetch && git checkout -b <name> |
| 100 | + origin/main`) — local clones carry divergence; basing on a stale tip silently reverts |
| 101 | + other work. |
| 102 | +. One work-package = one small, disjoint PR. |
| 103 | +. Read-only map → owner-approve → execute → adversarially verify → STOP before push. |
| 104 | +. Verify deterministically before each commit: re-run every Mustfile `run:` check; |
| 105 | + simulate the hook; phantom-recipe scan (`just <x>` in `just --list`); dangling-reference |
| 106 | + scan; manifest parent-pointer resolution; `git verify-commit` each commit; confirm |
| 107 | + `AFFIRMATION.adoc` SPDX unchanged. |
| 108 | +. For substantive review, spin a short adversarial workflow (content-drift / |
| 109 | + cross-reference / completeness) — it caught a botched README header a self-check missed. |
| 110 | + |
| 111 | +== Gotchas that will bite |
| 112 | + |
| 113 | +* *`snif` vs `snifs`:* repo name/URLs are `snifs`, but the crate prefix `snif-` and the |
| 114 | + paper file `snif.pdf` are intentional — leave them. A blind sweep corrupts both; |
| 115 | + `hyperpolymath/snif`→`snifs` turns an existing `…/snifs` into `…/snifss` (substring |
| 116 | + trap) — collision-check first. |
| 117 | +* *Recipes: `just --list` is the only truth.* Real: `build-wasm`, `assail`, |
| 118 | + `container-build`/`-run`, `proof-check-all`, `abi-conformance`, `tour`, `doctor`, |
| 119 | + `paper`. Phantom (never reference): `setup`, `setup-dev`, `heal`, `uninstall`, |
| 120 | + `panic-scan`, `stapeln-export`/`-run`, `llm-context`. |
| 121 | +* *DOC-FORMAT:* AsciiDoc primary; `.md` only for GitHub-required files (SECURITY, |
| 122 | + CONTRIBUTING, CODE_OF_CONDUCT, CHANGELOG, copilot-instructions) and the standards root |
| 123 | + pointers (TOPOLOGY, PROOF-NEEDS, PROOF-STATUS, TEST-NEEDS, llm-warmup-*). |
| 124 | +* *AI-manifest convention:* a dir at depth N → `0.N-AI-MANIFEST.a2ml`, `level: N`, |
| 125 | + `parent: ../0.{N-1}-AI-MANIFEST.a2ml` (root children use `../0-AI-MANIFEST.a2ml`). |
| 126 | + `docs/governance/` violates this (D-f). |
| 127 | +* *`Containerfile` must stay at repo root* — `dogfood-gate.yml` checks `[ -f |
| 128 | + "Containerfile" ]` there. |
| 129 | +* *`.github/settings.yml`* is the probot/settings sync source — a wrong `name:` can rename |
| 130 | + the repo. |
| 131 | +* *`dogfood-gate.yml`'s `rsr-template-repo` refs are legitimate* (point users to the real |
| 132 | + template) — leave them. |
| 133 | + |
| 134 | +== Canonical facts |
| 135 | + |
| 136 | +* Owner literal: `Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>`. |
| 137 | +* Citation: _SNIFs: Safer Native Implemented Functions for the BEAM via WebAssembly |
| 138 | + Sandboxing_, Jewell, Jonathan D. A., 2026, DOI `10.5281/zenodo.19520245`, MPL-2.0. |
| 139 | + Canonical record = root `CITATION.cff`. |
| 140 | +* One-line purpose: _Safer NIFs: crash-isolated native interfaces for the BEAM via |
| 141 | + WebAssembly sandboxing._ |
0 commit comments