proof(verifier-spec): ADR-0005 — MkTrustedFixture audit boundary (closes #103) (#155)

## Summary

Closes #103 by taking **path (3)** from the
issue's three closure paths — an explicit ADR pinning `MkTrustedFixture`
as the formal audit boundary for `VerifierAccepts` / `SourceAccepts`.

PR #79 (`06ec00e`) landed TOTAL bodies for `VerifierSpecAgreement` and
`SourceVerifierAgreement`. What remained per #103: the trust-injection
moment (every `VADifferential` / `SADifferential` ultimately routes
through `MkTrustedFixture`) needed a load-bearing, named,
cross-referenced specification rather than an inline docstring.

## What lands

### `docs/decisions/0005-trustedfixture-audit-boundary.adoc` (new ADR,
Accepted)

Pins three inspection invariants every `MkTrustedFixture m` construction
site is audited against:

- **I1 Provenance** — `(trustedFixtureName, trustedFixtureId)` must
correspond to an existing row in
`crates/typed-wasm-verify/tests/cross_compat.rs`.
- **I2 Witness fidelity** — `trustedWitness : FunctionsAccepted
m.functions` must be the structural witness the harness's ACCEPT verdict
establishes; rejected fixtures yield no `MkTrustedFixture`.
- **I3 Module shape** — the indexing `ModuleSummary` must mirror the
harness's `ModuleSummary` reconstruction for the same fixture bytes
(function order + decoded ownership intents).

Also names the supersession path: a future **WasmCert-Isabelle
tie-back** (issue #103 path 1) or **constructive Rust-verifier
soundness** (issue #103 path 2) would each ship as a fresh ADR
superseding 0005 by collapsing the audit boundary into a constructive
proof.

### `docs/decisions/README.adoc`

Index row for ADR-0005 + 1-line owner-line header normalisation (hook
compliance).

### `src/abi/TypedWasm/ABI/VerifierSpec.idr`

6-line docstring addition near `MkTrustedFixture` cross-referencing
ADR-0005 so a reader landing on the record's definition can find the
invariants without rediscovering them. Single grep point for trust
injections preserved: \`git grep MkTrustedFixture\`. Same 1-line
owner-line normalisation as #152's Epistemic.idr (parenthetical removal
only; no licence change, no SPDX change; owner-approved via
AskUserQuestion mid-session).

### `PROOF-NEEDS.md`

New `RECONCILIATION 2026-06-02` banner recording the closure with the
I1/I2/I3 summary and the supersession note. Matches the convention of
the prior `RECONCILIATION 2026-05-27 (post-A10 items 7 + 8 bodies
closed)` banner. Same 3-line owner-line header normalisation already
landed on #153's branch.

## Stacking

This PR is **stacked on #152** (`proof/epistemic-fresh-pin-102`) — base
set accordingly. Reason: #152 contains the HEAD build fix for
`composeWitnessLegacyAgree`; #103's docstring edit on `VerifierSpec.idr`
requires a clean package build to land. The incremental diff (visible
here) is **only** the ADR + cross-references — 4 files / +351 lines / -2
lines.

When #152 merges, this PR will rebase forward to `main` and be a
1-commit fast-forward.

## What this is not

- **Not** a constructive proof of Rust-verifier soundness. The Rust
verifier remains the trusted base for the differential path; ADR-0005
pins the audit story for that trust, not its discharge.
- **Not** a change to any Idris2 type. PR #79's record shape remains
canonical.
- **Not** a gate on the structural path. `VAStructural` and
`SAStructural` continue to inject zero trust.

## Test plan

- [x] `src/abi/TypedWasm/ABI/VerifierSpec.idr` type-checks rc=0 in
isolation (`idris2 --check`).
- [x] Whole-package build rc=0, 22/22 modules, 0 errors (only
pre-existing shadowing warnings).
- [x] No `believe_me` / `assert_total` / `postulate` / `sorry` /
`assert_smaller` introduced.
- [x] `%default total` preserved across the arc.
- [x] No SPDX-License-Identifier line changed in any file.
Owner-attribution normalisation only on files where the pre-commit hook
required it (parenthetical removal — same micro-pattern as #152's
Epistemic.idr and #153's PROOF-NEEDS.md).
- [ ] CI green on stacked head.

## Cross-references

- Closes #103.
- Refs #79 — statement-level landing of agreement records (commit
`06ec00e`).
- Refs #74 — superseded alternative design (`RegisteredFixture` GADT +
`Maybe`-returning bridges); composable add-on if a fixture-table module
is ever wanted.
- Refs #102, #152, #153 — companion proof work in flight (this PR stacks
on #152).

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

Author: hyperpolymath

.claude/CLAUDE.md

@@ -26,32 +26,6 @@ cd ffi/zig && zig build test
 cd src/abi && idris2 --check Proofs.idr
 ```
 
-## Environment & Toolchain (operational)
-
-**Provisioning:** `just provision` (→ `tools/provision.sh`) installs the full toolchain;
-`just setup` runs provision + `just deps` (a presence check). `setup.sh` bootstraps `just`
-then calls `just setup`.
-
-- **JS runtime is Deno**, not node (estate npm→Deno migration, #133 / standards#253). The
-  `.affine` parser sources compile to `.mjs` (`affinescript.json`); those `.mjs` run under
-  Deno. Test harnesses use `deno run` via the Justfile `deno_run` var / `deno.json` tasks,
-  with scoped perms `--allow-read --allow-write --allow-run --allow-env --allow-sys`. There
-  is **no `package.json`** (removed in #133) and no lockfile (only `node:` builtins).
-- **AffineScript is an OCaml compiler, NOT an npm package** (`@hyperpolymath/affinescript`
-  404s on npmjs). Built from `hyperpolymath/affinescript` with opam + dune at the SHA pinned
-  in `.github/workflows/c5-regenerate.yml` (`AFFINESCRIPT_SHA`); binary is
-  `_build/default/bin/main.exe`. Building it is the unblock for the #127 front-end→IR seam.
-- **wasmtime** (the #132 capstone execution gate) installs via `cargo install wasmtime-cli`.
-
-**Network policy (Claude Code remote env):** `github.com` release assets, crates.io, npmjs,
-and ubuntu apt are reachable; `deno.land`/`dl.deno.land`, `api.github.com`, and `wasmtime.dev`
-are denylisted (`x-deny-reason: host_not_allowed`). Fetch deno/just from **github.com release
-assets** (not the vendor install scripts); wasmtime via crates.io.
-
-**Git proxy:** serves only `hyperpolymath/typed-wasm`, but direct `git clone
-https://github.com/...` works (github.com is allowed). Ref-deletes return HTTP 403 —
-**branch deletion is GitHub-UI-only** (there is no MCP delete-branch tool either).
-
 ## Key Design Decisions
 
 - Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI)

.claude/README.md

@@ -17,14 +17,11 @@ Checked-in, team-shared configuration for Claude Code sessions on typed-wasm.
 
 ### Permissions (`permissions.allow`)
 
-A **non-destructive** allowlist that cuts permission prompts for the commands used routinely in
-this repo: read-only git inspection (`status/log/diff/fetch/show/ls-files/ls-tree/branch/
-rev-parse/merge-base/for-each-ref/check-attr`, `git bundle verify`/`list-heads`), the cargo
-dev loop (`cargo build/test/run/clippy`, `cargo fmt --check`, `cargo metadata/audit`) — which is
-non-destructive to the source tree (build artifacts land in `target/`; `tw build` writes only the
-`.wasm`/`.wat` you name), `diff -rq`, and `curl` **restricted to
-`https://raw.githubusercontent.com/`** (used to compare sibling-estate repos without a full
-clone). No push, no source-mutating, and no destructive commands are granted — those still
+A **read-only** allowlist that cuts permission prompts for the inspection commands used
+routinely in this repo: `git status/log/diff/fetch/show/ls-files/ls-tree/branch/rev-parse/
+merge-base/for-each-ref/check-attr`, `git bundle verify`/`list-heads`, `diff -rq`, and
+`curl` **restricted to `https://raw.githubusercontent.com/`** (used to compare sibling-estate
+repos without a full clone). No write, push, or destructive commands are granted — those still
 prompt.
 
 ### Hooks (`hooks.SessionStart`)

.claude/settings.json

@@ -17,13 +17,6 @@
       "Bash(git check-attr:*)",
       "Bash(git bundle verify:*)",
       "Bash(git bundle list-heads:*)",
-      "Bash(cargo build:*)",
-      "Bash(cargo run:*)",
-      "Bash(cargo test:*)",
-      "Bash(cargo clippy:*)",
-      "Bash(cargo fmt --check:*)",
-      "Bash(cargo metadata:*)",
-      "Bash(cargo audit:*)",
       "Bash(diff -rq:*)",
       "Bash(curl -s https://raw.githubusercontent.com/:*)",
       "Bash(curl -sI https://raw.githubusercontent.com/:*)",

.github/workflows/boj-build.yml

@@ -13,7 +13,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       - name: Trigger BoJ Server (Casket/ssg-mcp)
         run: |
           # Send a secure trigger to boj-server to build this repository

.github/workflows/c5-regenerate.yml

@@ -39,10 +39,10 @@ jobs:
 
     steps:
       - name: Checkout typed-wasm
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Checkout affinescript at pinned SHA
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: hyperpolymath/affinescript
           ref: ${{ env.AFFINESCRIPT_SHA }}

.github/workflows/cargo-audit.yml

@@ -39,7 +39,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       # Match the cargo-verify pattern in e2e.yml: use the preinstalled
       # rustup directly rather than a SHA-pinned third-party action.

.github/workflows/codeql.yml

@@ -35,15 +35,15 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Initialize CodeQL
-        uses: github/codeql-action/init@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3
+        uses: github/codeql-action/init@7211b7c8077ea37d8641b6271f6a365a22a5fbfa # v3
         with:
           languages: ${{ matrix.language }}
           build-mode: ${{ matrix.build-mode }}
 
       - name: Perform CodeQL Analysis
-        uses: github/codeql-action/analyze@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3
+        uses: github/codeql-action/analyze@7211b7c8077ea37d8641b6271f6a365a22a5fbfa # v3
         with:
           category: "/language:${{ matrix.language }}"

.github/workflows/dogfood-gate.yml

@@ -29,7 +29,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Check for A2ML files
         id: detect
@@ -48,7 +48,7 @@ jobs:
       - name: Validate A2ML manifests
         if: steps.detect.outputs.count > 0
         continue-on-error: true
-        uses: hyperpolymath/a2ml-validate-action@6bff6ec134fc977e86d25166a5c522ddea5c1e78 # main
+        uses: hyperpolymath/a2ml-validate-action@59145c7d1039fa3059b3ecacdb50ee23d7505898 # main
         with:
           path: '.'
           strict: 'false'
@@ -79,7 +79,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Check for K9 files
         id: detect
@@ -132,7 +132,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Scan for invisible characters
         id: lint
@@ -196,7 +196,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Check for Groove manifest
         id: groove
@@ -256,7 +256,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Generate dogfooding scorecard
         run: |

.github/workflows/e2e.yml

@@ -5,7 +5,7 @@
 #
 # Runs on every PR and push to main. Three jobs:
 #   structural   — fast structural checks (no compiler required)
-#   smoke        — Deno harnesses (AffineScript parser + aspect/proof envelopes)
+#   smoke        — Node.js smoke test (AffineScript parser + example files)
 #   build-e2e    — Full Idris2 + Zig build then E2E
 #   cargo-verify — Cargo workspace build + test (typed-wasm-verify crate)
 name: E2E Validation
@@ -33,82 +33,81 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Run structural E2E checks
         run: E2E_BUILD=0 bash tests/e2e.sh
 
   # --------------------------------------------------------------------------
-  # Job 2: Smoke test — Deno harness validation
+  # Job 2: Smoke test — Node.js parser validation
   # --------------------------------------------------------------------------
   smoke:
-    name: Smoke test (Deno AffineScript harnesses)
+    name: Smoke test (Node.js AffineScript parser)
     runs-on: ubuntu-latest
-    env:
-      # Scoped permissions covering the harnesses' needs (file read/write,
-      # subprocess spawn for idris2, env). See deno.json / Justfile `deno_run`.
-      DENO_RUN: "deno run --allow-read --allow-write --allow-run --allow-env --allow-sys"
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
-
-      # Deno is the project's JS runtime (estate npm→Deno migration, #133 /
-      # standards#253). deno.land is denied by some network policies, so install
-      # straight from the GitHub release assets — the same curl pattern the
-      # Idris2 / Zig steps use below.
-      - name: Install Deno
-        run: |
-          DENO_VERSION="2.8.1"
-          curl -fsSL -o /tmp/deno.zip \
-            "https://github.com/denoland/deno/releases/download/v${DENO_VERSION}/deno-x86_64-unknown-linux-gnu.zip"
-          mkdir -p "$HOME/.deno/bin"
-          unzip -oq /tmp/deno.zip -d "$HOME/.deno/bin"
-          echo "$HOME/.deno/bin" >> "$GITHUB_PATH"
-          "$HOME/.deno/bin/deno" --version
-
-      # The AffineScript parser compiler is OCaml (opam + dune, NOT npm — see
-      # tools/provision.sh). Building it is expensive (~5 min) and is exercised by
-      # c5-regenerate.yml, not here. If it happens to be on PATH, build; otherwise
-      # skip and let the guarded steps below handle the artefact-absent case.
-      - name: Build parser (AffineScript, if provisioned)
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Set up Node.js
+        uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
+        with:
+          node-version: '25'
+
+      - name: Install npm deps
+        run: npm install --no-audit --no-fund --silent
+
+      # Phase 0 NOTE (issue #48): Track A's parser migration replaced
+      # ReScript (.res + rescript.json + rescript build) with AffineScript
+      # (.affine + affinescript.json + @hyperpolymath/affinescript compiler).
+      # The compiler isn't yet declared as an npm dep in package.json so
+      # `npm install` can't fetch it on a clean CI runner. Detect the
+      # AffineScript or ReScript binary if either is present after install,
+      # build with whichever is available, otherwise skip and let downstream
+      # steps handle the artefact-absent case (they're already guarded).
+      - name: Build parser (AffineScript preferred, ReScript fallback)
         run: |
-          if command -v affinescript >/dev/null 2>&1; then
-            echo "Building parser with AffineScript..."
-            affinescript build
+          if [ -x node_modules/.bin/affinescript ]; then
+            echo "Building with AffineScript..."
+            node_modules/.bin/affinescript build
+          elif [ -x node_modules/.bin/rescript ]; then
+            echo "Building with ReScript (migration fallback)..."
+            node_modules/.bin/rescript build
           else
-            echo "::warning::affinescript (OCaml) not provisioned — skipping parser build."
-            echo "::warning::smoke / property / benchmark steps will skip if src/parser/Parser.mjs is absent."
+            echo "::warning::No parser compiler available — skipping build."
+            echo "::warning::Track A parser-migration is incomplete; see #48."
+            echo "::warning::Downstream smoke / aspect / property / benchmark"
+            echo "::warning::steps will skip if src/parser/Parser.mjs is absent."
           fi
 
       - name: Run smoke test (skip if parser artefacts absent)
         run: |
           if [ -f src/parser/Parser.mjs ]; then
-            $DENO_RUN tests/smoke/e2e-smoke.mjs
+            node tests/smoke/e2e-smoke.mjs
           else
             echo "::warning::src/parser/Parser.mjs absent — skipping smoke test."
           fi
 
       - name: Run aspect tests (claim + security envelopes — no parser dep)
         run: |
-          $DENO_RUN tests/aspect/claim-envelope.mjs
-          $DENO_RUN tests/aspect/security-envelope.mjs
+          node tests/aspect/claim-envelope.mjs
+          node tests/aspect/security-envelope.mjs
 
       - name: Run property tests (skip if parser artefacts absent)
         run: |
           if [ -f src/parser/Parser.mjs ]; then
-            $DENO_RUN tests/property/property_test.mjs
+            node tests/property/property_test.mjs
           else
             echo "::warning::src/parser/Parser.mjs absent — skipping property tests."
           fi
 
       - name: Run proof regression (named theorems + idris2 typecheck if present)
-        run: $DENO_RUN tests/proof/regression.mjs
+        run: node tests/proof/regression.mjs
 
       - name: Run parser benchmark (skip if parser artefacts absent)
         run: |
           if [ -f src/parser/Parser.mjs ]; then
-            BENCH_ITERS=20 $DENO_RUN benchmarks/parser-bench.mjs
+            BENCH_ITERS=20 node benchmarks/parser-bench.mjs
           else
             echo "::warning::src/parser/Parser.mjs absent — skipping benchmark."
           fi
@@ -122,7 +121,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       # ---- Idris2 ----
       # 0.8.0 is the version the src/abi/ proofs are written against
@@ -159,18 +158,11 @@ jobs:
           tar -xJf /tmp/zig.tar.xz -C /opt
           ln -s "/opt/${ZIG_DIR}/zig" /usr/local/bin/zig
 
-      # ---- Deno (JS runtime for the smoke harness within the E2E script) ----
-      # Installed from the GitHub release assets (deno.land is denied by some
-      # network policies); matches the curl pattern above. See tests/e2e.sh.
-      - name: Install Deno
-        run: |
-          DENO_VERSION="2.8.1"
-          curl -fsSL -o /tmp/deno.zip \
-            "https://github.com/denoland/deno/releases/download/v${DENO_VERSION}/deno-x86_64-unknown-linux-gnu.zip"
-          mkdir -p "$HOME/.deno/bin"
-          unzip -oq /tmp/deno.zip -d "$HOME/.deno/bin"
-          echo "$HOME/.deno/bin" >> "$GITHUB_PATH"
-          "$HOME/.deno/bin/deno" --version
+      # ---- Node (for smoke test within E2E script) ----
+      - name: Set up Node.js
+        uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
+        with:
+          node-version: '25'
 
       # ---- Full E2E ----
       # Phase 0 NOTE (issue #48): this step has been persistently red since
@@ -198,7 +190,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       # ubuntu-latest ships rustup preinstalled; call it directly rather than
       # routing through dtolnay/rust-toolchain (the SHA-pinned action was
@@ -214,12 +206,3 @@ jobs:
 
       - name: Cargo test (workspace)
         run: cargo test --workspace --locked
-
-      # Explicit named step for the IR-level round-trip corpus (#130).
-      # Already covered by the workspace test above, but naming it
-      # explicitly makes any regression in the verify(emit(m)) loop
-      # surface as a clearly-named failure. Surface .twasm corpus is
-      # blocked on the front-end → IR seam (#127); this is the cheap-wire
-      # half of #130.
-      - name: Round-trip soundness corpus (IR-level slice — refs #130)
-        run: cargo test --test corpus -p typed-wasm-codegen --locked

.github/workflows/release.yml

@@ -25,7 +25,7 @@ jobs:
     permissions:
       contents: read
     steps:
-      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Build
         run: |
@@ -52,7 +52,7 @@ jobs:
       changelog: ${{ steps.cliff.outputs.content }}
       version: ${{ steps.version.outputs.version }}
     steps:
-      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           fetch-depth: 0
 
@@ -95,7 +95,7 @@ jobs:
     permissions:
       contents: write
     steps:
-      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       # TODO: Download build artifacts if uploading to the release
       # - uses: actions/download-artifact@v4