hyperpolymath · hyperpolymath · May 19, 2026 · May 19, 2026
@@ -43,17 +43,32 @@ CI-gated and green:
   it byte-for-byte conformant with the Rust `to_wire` encoder by `Refl`
   on golden fixtures (regeneration oracle:
   `src/interface/parse/tests/conformance_emit.rs`). The C-ABI
-  `Statement` marshalling *decode* side is now certified. Disclosed:
+  `Statement` marshalling *decode* side is certified. Disclosed:
   the NaN *payload* is not preserved across the Idris `Double` boundary
   (finite + infinite values bit-exact; Rust proptest remains the
-  exhaustive float witness). OWED: **P5c — typed-wasm PCC transport**
-  (proof term + checker kernel the consumer re-runs; *re-checkable*,
-  TCB = checker kernel; the estate-aligned objective — the `ffi/zig`
-  fail-closed shim is retained only as the C-ABI attestation
-  *fallback*, not the endpoint); **P5d** — the signed-attestation
-  fallback contract for C-only consumers. Re-checkable transport is
-  impossible only over a C ABI, not over typed-wasm (two-tier boundary
-  model: `verification/proofs/VERIFICATION-STANCE.adoc`).
+  exhaustive float witness).
+- Phase 5 / vcl-ut#25 — **Tier-1 recompute-PCC RESOLVED**: P5c-1 (#30)
+  certified `OctadSchema` codec (closes schema-marshalling OWED);
+  P5c-2/3/4 (#31) `vcltotal_parse::decider` — a faithful Rust port of
+  the corpus decision core (`Schema`/`Decide`/`Checker`
+  `checkLevel0..10`/`certifiedLevel`), machine-pinned to the corpus's
+  public deciders via `WireConformance` on shared golden bytes
+  (find-dependent verdicts pinned Rust-side + input-value conformance,
+  disclosed); P5c-5 (#32) the recompute **`wasm32`** artefact
+  `src/interface/recompute-wasm` (`vcl_recompute`, fail-closed, one
+  audited host/guest `unsafe` block; all logic in the forbid-unsafe
+  crate); P5c-6 (this change) the `OWED→RESOLVED` stance flip + ADR
+  `docs/decisions/0002-ffi-attestation-trust-boundary.adoc`. The
+  consumer **re-runs** the certified decision and compares — PCC by
+  recomputation, not proof transport. Plain `wasm32` suffices (type
+  system not load-bearing under recompute); `affinescriptiser` N/A
+  (resource-required + wasm-backend-pending; disclosed in
+  `AFFINESCRIPTISER-NA.adoc`, not faked). **OWED — P5d (Tier-2
+  fallback):** the C-ABI signed-attestation contract +
+  `vclut_rs_verify` linkage for consumers that cannot run the wasm.
+  A re-checkable proof is impossible *only* over the C-ABI fallback
+  tier (canonical two-tier model:
+  `verification/proofs/VERIFICATION-STANCE.adoc`).
 
 `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative,
 precisely-scoped catalogue (residual OWED items disclosed, not masked).

@@ -7,7 +7,7 @@
 - **Languages**: Rust, ReScript, Idris2, Zig
 - **Existing ABI proofs**: `src/interface/abi/*.idr` + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`, `Composition.idr`
 - **Machine-verified**: the full `VclTotal` proof corpus — `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0 (`idris2 --build`, exit 0, `%default total`, **zero proof-escape symbols**, CI-gated by `.github/workflows/proof-corpus.yml`) as **12 modules** (`ABI.{Types,Layout,LayoutProofs}` + `Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}` + `Interface.{WireDecode,WireConformance}`), plus the self-contained `verification/proofs/SafetyL4Model.idr` (`--check`, exit 0). Phases 1–4 are on `origin/main` (PRs #21/#22/#23/#24); Phase 5 / vcl-ut#25 (trusted Rust parser P5a #26, wire codec P5b-step-1 #28, **certified Idris wire decoder + cross-language `Refl` conformance** P5b-step-2) reinforces the FFI boundary.
-- **Status (Phase 0 → 4 RESOLVED, honestly; Phase 5 boundary reinforcement in progress)**: the Phase-0 blockers are fixed, not faked — the corpus compiles and is machine-checked; `ABI.Types`/`Grammar` errors repaired; **L2/L3/L5 de-vacuized** (Phase 2, evidence-carrying predicates over `Core.Decide`); all ten levels carry `checkLevelNSound` and `Checker.certifyAt`/`certifyRequested` assemble a genuine dependent `SafetyCertificate` (Phase 3); the Zig FFI is no longer a fabricating stub — it is **fail-closed** with a proof-gated `Checker.certifiedLevel` mint (Phase 3d). **Phase 5 (vcl-ut#25)**: a trusted Rust/SPARK-grade parser + a deterministic versioned wire codec exist, and the *decode* side of the C-ABI `Statement` marshalling is now **certified** — `VclTotal.Interface.WireDecode` is a total (zero-escape) decoder proven byte-for-byte conformant with the Rust encoder by `Refl` (`WireConformance`). Remaining honest gaps are precisely scoped (P5c = typed-wasm PCC proof-transport — proof term + checker kernel the consumer re-runs, *re-checkable*, the estate-aligned objective; the C-ABI/Zig shim retained only as the fail-closed attestation fallback; P5d = signed-attestation *fallback* contract for C-only consumers; plus L3 subquery/heuristic scoping; L9/L10 predicate depth; the additive↔ceil `alignUp` sliver; the disclosed NaN-payload limitation of the Idris `Double` boundary). Re-checkable transport is impossible *only* over a C ABI, not over the estate's typed-wasm target. `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, proof-backed catalogue and takes precedence over this file.
+- **Status (Phase 0 → 4 RESOLVED, honestly; Phase 5 boundary reinforcement in progress)**: the Phase-0 blockers are fixed, not faked — the corpus compiles and is machine-checked; `ABI.Types`/`Grammar` errors repaired; **L2/L3/L5 de-vacuized** (Phase 2, evidence-carrying predicates over `Core.Decide`); all ten levels carry `checkLevelNSound` and `Checker.certifyAt`/`certifyRequested` assemble a genuine dependent `SafetyCertificate` (Phase 3); the Zig FFI is no longer a fabricating stub — it is **fail-closed** with a proof-gated `Checker.certifiedLevel` mint (Phase 3d). **Phase 5 (vcl-ut#25)**: a trusted Rust/SPARK-grade parser + a deterministic versioned wire codec exist, and the *decode* side of the C-ABI `Statement` marshalling is now **certified** — `VclTotal.Interface.WireDecode` is a total (zero-escape) decoder proven byte-for-byte conformant with the Rust encoder by `Refl` (`WireConformance`). **P5c (vcl-ut#25) — Tier-1 recompute-PCC RESOLVED** (#26/#28/#29/#30/#31/#32): trusted Rust parser, certified `Statement`+`OctadSchema` decoder (`Refl`-pinned), faithful Rust decision port machine-pinned to the corpus, and a fail-closed recompute `wasm32` artefact the consumer re-runs. Remaining honest gaps precisely scoped: **P5d** = C-ABI signed-attestation *fallback* contract for non-wasm consumers (Tier-2, OWED); plus the disclosed limits (NaN-payload reconstruction; cross-module `Refl` non-reduction of `find`/`elemBy` ⇒ schema-resolution-dependent verdicts pinned Rust-side + input-value conformance; L3 subquery/heuristic scoping; L9/L10 predicate depth; additive↔ceil `alignUp` sliver). A re-checkable proof is impossible *only* over the C-ABI fallback tier; Tier-1 sidesteps it by recomputation, not proof transport. `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, proof-backed catalogue and takes precedence over this file.
 
 ## What Needs Proving
 
@@ -52,15 +52,20 @@
   Idris decoder into the certified `Statement`, proven byte-for-byte
   conformant with the Rust encoder by `Refl` in
   `VclTotal.Interface.WireConformance`. The marshalling seam's *decode*
-  side is therefore now machine-verified. **P5c** (the estate-aligned
-  objective): transport the certificate over the **typed-wasm** target
-  as a proof term + a small checker kernel the consumer re-runs —
-  proof-carrying code, *re-checkable*, TCB = checker kernel + typed-wasm
-  verifier (re-checkable transport is impossible only over a C ABI; the
-  `ffi/zig` fail-closed shim is retained only as the C-ABI attestation
-  fallback). **P5d** (fallback tier): the signed-attestation contract
-  for consumers reachable only over C. Both OWED; see the two-tier
-  boundary model in `verification/proofs/VERIFICATION-STANCE.adoc`.
+  side is machine-verified. **P5c — RESOLVED (Tier-1 recompute-PCC):**
+  the consumer re-runs the certified decision itself from the
+  fail-closed `wasm32` module `src/interface/recompute-wasm`
+  (`vcl_recompute`); the decision core is a faithful Rust port of the
+  corpus (`Schema`/`Decide`/`Checker`) machine-pinned via
+  `WireConformance`. TCB = conformance-pinned decider image + wasm
+  runtime + the once-proved corpus (offline-re-checkable) — *not* a
+  trusted tag, *not* a transported proof object. Plain `wasm32`
+  suffices (type system not load-bearing under recompute);
+  `affinescriptiser` N/A (disclosed). **P5d — OWED (Tier-2 fallback):**
+  the C-ABI signed-attestation contract + `vclut_rs_verify` linkage,
+  for consumers that cannot run the wasm; the `ffi/zig` fail-closed
+  shim is its scaffolding. See the canonical two-tier boundary model
+  in `verification/proofs/VERIFICATION-STANCE.adoc` (authoritative).
 - Optional future work: prove the ReScript frontend faithfully tracks
   the Idris2 grammar (low priority; it is a convenience frontend, not a
   trust anchor).

@@ -0,0 +1,109 @@
+= Architecture Decision Record: 0002-ffi-attestation-trust-boundary
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# 2. FFI trust boundary: recompute-PCC over wasm32 (Tier-1), C-ABI attestation (Tier-2)
+
+Date: 2026-05-19
+
+## Status
+
+Accepted (Tier-1 RESOLVED; Tier-2 / P5d OWED). Tracked:
+hyperpolymath/vcl-ut#25. Authoritative companion:
+`verification/proofs/VERIFICATION-STANCE.adoc` (canonical two-tier
+boundary model) — this ADR records *why*; the stance records *what is
+and is not proven*.
+
+## Context
+
+vcl-ut is the doubly-trusted hypatia↔verisim interface. The Idris2
+corpus proves, machine-checked and CI-gated, that the 10-level VCL-total
+decision procedure is sound (`checkLevelNSound`,
+`Checker.certifyAt`/`certifyRequested` assembling a dependent
+`SafetyCertificate`). The open question was how a *consumer* obtains
+that guarantee across a process/language boundary.
+
+Constraints established during Phase 5:
+
+- A **C ABI erases types to machine words**: a dependent
+  `SafetyCertificate` cannot cross it as a re-checkable object. Over a
+  C ABI the honest ceiling is *trusted-certifier attestation* (trust
+  the minting checker; the token is unforgeable, bound to
+  `(sha256(query), schema_id, level)`).
+- A **proof-term-PCC** design (ship a core proof term + a small
+  dependent kernel the consumer runs) was considered and **rejected**:
+  Idris2 0.8.0 ships no embeddable verified core kernel, and building
+  one is its own subproject of unbounded scope.
+- The estate's `affinescriptiser` (Rust→typed-wasm wrapper) **does not
+  apply**: it structurally requires ≥1 `[[resources]]` and the
+  verdict entry is a pure resource-free function (fabricating a
+  resource to satisfy the tool would violate the verification-honesty
+  doctrine), and its wasm backend is Phase-2-pending. (Disclosed:
+  `src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc`.)
+
+## Decision
+
+Adopt a **two-tier boundary**:
+
+**Tier-1 — recompute-PCC over plain `wasm32` (the achieved tier).**
+The consumer is shipped the `wasm32` module
+`src/interface/recompute-wasm` (`vcl_recompute`) + the wire bytes of a
+`(Statement, OctadSchema)` + the producer's claimed level, and
+**re-runs the certified decision itself**, comparing its verdict to
+the claim. This is proof-carrying code by *recomputation*, not by
+transporting a proof object. The consumer's TCB is:
+
+1. the once-proved corpus soundness (`checkLevelNSound`),
+   machine-checked in the CI-gated Idris corpus and *offline*
+   re-checkable with idris2 — never in the runtime path;
+2. the cross-language conformance pin that
+   `vcltotal_parse::certified_level` is a faithful image of that
+   corpus decision (`tests/conformance_emit.rs` ⇄
+   `VclTotal.Interface.WireConformance`, `Refl` on shared golden
+   bytes); and
+3. the wasm runtime — *not* the whole certifier, *not* a level tag
+   taken on faith.
+
+Plain `wasm32-unknown-unknown` is **sufficient and not a compromise**:
+nothing structured crosses the boundary that needs type-preservation
+(opaque wire bytes in, an `i64` out; the decoder+decider run *inside*
+the module), so the wasm *type system* is not load-bearing. The wasm
+verdict equals the conformance-pinned native verdict by construction
+(deterministic build of pinned, pure, total source). The path is
+fail-closed: any malformed input or unmet level → Reject, never a
+fabricated level. The only `unsafe` is one audited host/guest
+memory-ABI block — the declared trust boundary — with all
+decode/decision logic in the `#![forbid(unsafe_code)]` crate.
+
+**Tier-2 — C-ABI trusted-certifier attestation (fallback, P5d, OWED).**
+For consumers that cannot run the Tier-1 wasm: a signed token bound to
+`(sha256(query), schema_id, level)`, verified against the certifier's
+public key. Strictly weaker (pure trust in the minting certifier), and
+labelled as such. The fail-closed `ffi/zig` shim (Phase 3d) is its
+scaffolding; the signed contract + `vclut_rs_verify` linkage are OWED.
+
+## Consequences
+
+- The headline "no re-checkable proof across an FFI" objection is
+  **dissolved for Tier-1**: it was only ever true of an *untyped C
+  ABI*, and Tier-1 sidesteps it by recomputation rather than proof
+  transport. Recompute is, in one respect, *stronger* than proof-object
+  PCC — the consumer need not trust a transported term's provenance;
+  its cost is recomputation, negligible for a static AST decision.
+- The certifier (the Idris corpus) stays the single source of
+  verification truth, machine-checked once; the runtime never carries
+  a proof object.
+- Disclosed, precisely-scoped limits remain (NaN-payload
+  reconstruction; cross-module `Refl` non-reduction of
+  `find`/`elemBy`, so schema-resolution-dependent verdicts are pinned
+  Rust-side + by input-value conformance; L9/L10 predicate depth;
+  additive↔ceil `alignUp` sliver). These are stated in
+  VERIFICATION-STANCE.adoc, not faked.
+- P5d (Tier-2) is the remaining boundary work; until it lands,
+  non-wasm consumers receive only the fail-closed shim (no fabricated
+  level).
+- Revisit only if a future revision genuinely introduces a tracked
+  resource at this boundary (none foreseen for a pure verdict
+  function) or if a verified embeddable dependent kernel becomes
+  available (which would enable, but is not required for, an
+  additional proof-object tier).