vcl-ut #25 P5c (step 5): recompute-PCC wasm32 entry (fail-closed; isolated unsafe boundary)

src/interface/recompute-wasm/.gitignore

@@ -0,0 +1 @@
+/target

src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc

@@ -0,0 +1,80 @@
+= Why affinescriptiser is not used for the recompute-wasm entry
+:toc:
+
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+P5c (vcl-ut#25) ships the recompute-PCC tier as a `wasm32` module
+built by the standard Rust target, *not* via `affinescriptiser`. This
+records precisely why — disclosed, not an oversight, per the estate
+verification-honesty doctrine (`VERIFICATION-STANCE.adoc`).
+
+== The two reasons (either alone is sufficient)
+
+. *affinescriptiser is structurally resource-oriented.* Its manifest
+  `validate` rejects any manifest without `[[resources]]`:
++
+[source]
+----
+Error: At least one [[resources]] entry is required
+----
++
+The tool exists to wrap code that owns resources (file descriptors,
+sockets, GPU buffers, linear tokens) and prove *at-most-once* use via
+AffineScript affine types. The recompute entry
+(`vcl_recompute`) is a **pure total verdict function**: decode wire
+bytes → re-run the certified decision → return an `i64`. It owns no
+resources, allocates nothing that crosses the boundary, and holds no
+linear handles. There is nothing for the affine checker to track.
+Declaring a *fabricated* resource solely to satisfy the tool would be
+cargo-culting a proof obligation — precisely what the estate doctrine
+forbids ("never fake an obligation to satisfy a tool").
+
+. *affinescriptiser's wasm backend is Phase-2-pending.* `affinescriptiser
+  build` currently emits `(AffineScript compiler integration pending —
+  Phase 2)` and produces no wasm. (Verified 2026-05-19.)
+
+== Why this costs nothing
+
+Under the locked recompute design (`VERIFICATION-STANCE.adoc`
+two-tier boundary model) the security argument does **not** rest on the
+wasm's type system:
+
+* *Soundness* is the corpus proof `checkLevelNSound` — machine-checked
+  once in the CI-gated Idris corpus, offline-re-checkable with idris2.
+* *Faithfulness* of the Rust decider to that corpus is machine-pinned
+  by the cross-language conformance fixtures
+  (`tests/conformance_emit.rs` ⇄ `VclTotal.Interface.WireConformance`).
+* The wasm artefact is a *deterministic* `cargo build --release
+  --target wasm32-unknown-unknown` of that exact pinned source — pure,
+  total, deterministic integer logic with no platform-dependent
+  behaviour — so the wasm verdict is identical to the pinned native
+  verdict by construction.
+* Nothing structured crosses the module boundary that would need
+  type-preservation: opaque wire bytes in, an `i64` out; the
+  decoder+decider run *inside* the module. Plain
+  `wasm32-unknown-unknown` is therefore sufficient. AffineScript
+  dependent/affine typing was load-bearing only for the *rejected*
+  proof-term-transport tier, not for recompute.
+
+== Build
+
+[source,sh]
+----
+cd src/interface/recompute-wasm
+cargo build --release --target wasm32-unknown-unknown
+# → target/wasm32-unknown-unknown/release/vcltotal_recompute_wasm.wasm
+----
+
+The single `unsafe` in the whole recompute path is one audited
+host/guest memory-ABI block in `src/lib.rs` (the declared trust
+boundary); all decoding/decision logic stays in the
+`#![forbid(unsafe_code)]` `vcltotal-parse` crate.
+
+== If affinescriptiser later applies
+
+Should affinescriptiser's wasm backend land *and* a future revision
+genuinely introduce a tracked resource at this boundary (none is
+foreseen — a verdict function is pure by nature), this decision should
+be revisited. Until then, using it here would be a false signal.
+Tracked: hyperpolymath/vcl-ut#25.

src/interface/recompute-wasm/Cargo.toml

@@ -0,0 +1,39 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+
+# Standalone workspace root (same rationale as ../parse/Cargo.toml): the
+# parent virtual workspace has a pre-existing unresolvable external
+# path-dep, so this boundary crate builds/gates in isolation. Its ONLY
+# dependency is the in-repo, forbid-unsafe `vcltotal-parse` (internal
+# path-dep — resolves in a standalone checkout, unlike the broken
+# `../../../echidna/...` member).
+[workspace]
+
+[package]
+name = "vcltotal-recompute-wasm"
+version = "0.1.0"
+edition = "2021"
+license = "PMPL-1.0-or-later"
+authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
+repository = "https://github.com/hyperpolymath/vcl-ut"
+description = "P5c (#25): the recompute-PCC tier's wasm32 entry. Wraps the forbid-unsafe `vcltotal-parse` decoder+decider; the ONLY unsafe is one audited host/guest memory-ABI block (the declared trust boundary)."
+
+[lib]
+name = "vcltotal_recompute_wasm"
+crate-type = ["cdylib", "rlib"]
+path = "src/lib.rs"
+
+[dependencies]
+vcltotal-parse = { path = "../parse" }
+
+# Total/panic-free is inherited from `vcltotal-parse`'s static SPARK
+# lint set (the decoder/decider carry no panics). `panic = "abort"`
+# removes the unwinding runtime from the cdylib so a (by-construction
+# unreachable) panic is a trap, never UB.
+[profile.release]
+panic = "abort"
+opt-level = "z"
+lto = true
+strip = true
+
+[profile.dev]
+panic = "abort"

src/interface/recompute-wasm/README.adoc

@@ -0,0 +1,65 @@
+= vcltotal-recompute-wasm
+:toc:
+
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+P5c of hyperpolymath/vcl-ut#25 — the **recompute-PCC tier's `wasm32`
+entry**. See `verification/proofs/VERIFICATION-STANCE.adoc` (the
+authoritative catalogue) for the two-tier boundary model.
+
+== Role
+
+The consumer (hypatia / verisim) is shipped this wasm module + the wire
+bytes of a `(Statement, OctadSchema)` + the producer's claimed safety
+level. It **re-runs the certified decision** and compares. The trust
+argument is *not* the wasm's type system:
+
+* *Soundness* — the corpus proof `checkLevelNSound`, machine-checked
+  once in the CI-gated Idris corpus, offline-re-checkable with idris2.
+* *Faithfulness* — `vcltotal_parse::certified_level` is pinned to the
+  corpus decision by `tests/conformance_emit.rs` ⇄
+  `VclTotal.Interface.WireConformance`.
+* This crate adds only the host/guest memory ABI; no decision logic.
+
+== Fail-closed
+
+Any malformed wire input, or any required safety level not
+re-established, yields `-1` (Reject) — never a fabricated level. The
+only non-negative result is a genuinely recomputed certified level
+(`0..=10`).
+
+== Unsafe policy
+
+All decoding/decision logic lives in the `#![forbid(unsafe_code)]`
+`vcltotal-parse` crate. The **only** `unsafe` in the recompute path is
+one small, audited host/guest memory-ABI block in `src/lib.rs` — which
+*is* the declared trust boundary (the host is trusted to pass valid
+`(ptr, len)` into guest linear memory).
+
+== Build
+
+[source,sh]
+----
+cargo build --release --target wasm32-unknown-unknown
+# → target/wasm32-unknown-unknown/release/vcltotal_recompute_wasm.wasm
+----
+
+`rustup target add wasm32-unknown-unknown` if missing (non-interactive).
+
+== ABI
+
+[cols="1,3"]
+|===
+| `vcl_alloc(len) -> *mut u8`        | allocate a guest buffer for the host to fill
+| `vcl_dealloc(ptr, len)`           | free a `vcl_alloc` buffer
+| `vcl_recompute(sp,sl,cp,cl) -> i64`| decode `(Statement,OctadSchema)` wire bytes, recompute certified level; `-1` = Reject
+|===
+
+== Not affinescriptiser
+
+The estate Rust→typed-wasm wrapper is *not* used here: it structurally
+requires `[[resources]]` and this entry is a pure resource-free verdict
+function (and its wasm backend is Phase-2-pending). Faking a resource
+to satisfy it would violate the verification-honesty doctrine. Full
+rationale: `AFFINESCRIPTISER-NA.adoc`.