From f8f3aec018099bd02d03abb8b773fcdbadac6a97 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 19 May 2026 18:53:00 +0100 Subject: [PATCH] vcl-ut #25 P5c (step 5): recompute-PCC wasm32 entry (fail-closed; isolated unsafe boundary) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The recompute-PCC tier's executable artefact. Under the locked two-tier design (VERIFICATION-STANCE.adoc): the consumer is shipped this wasm module + the wire bytes of a (Statement, OctadSchema) + the producer's claimed level, RE-RUNS the certified decision here, and compares. Guarantee = corpus proof (checkLevelNSound, once) + conformance pin (P5c-4) — NOT the wasm's type system. New crate src/interface/recompute-wasm (standalone workspace; only dep = the in-repo forbid-unsafe vcltotal-parse via internal path-dep): - src/lib.rs — `vcl_recompute(stmt_ptr,len,schema_ptr,len) -> i64` (+ `vcl_alloc`/`vcl_dealloc` for the host to stage bytes). Fail-closed: any WireError, null ptr, or unmet level → -1; the only non-negative result is a genuinely recomputed certified level. - The ONLY unsafe in the whole recompute path is one audited, documented host/guest memory-ABI block (slice::from_raw_parts) — which IS the declared trust boundary. All decode/decision logic stays in the #![forbid(unsafe_code)] vcltotal-parse crate. User decision (recorded): separate crate + isolated documented unsafe, not wasm-bindgen, not exported-buffer. - Builds to real wasm: `cargo build --release --target wasm32-unknown-unknown` → 50KB vcltotal_recompute_wasm.wasm. `panic = "abort"` (no unwinding runtime; a by-construction unreachable panic traps, never UB). - Host tests green (garbage/null fail-closed; well-formed → 0); clippy -D warnings clean; fmt clean. Mechanism findings (disclosed, not faked — estate doctrine): - plain wasm32-unknown-unknown is SUFFICIENT for the recompute argument: nothing structured crosses the boundary needing type-preservation (opaque bytes in, i64 out, decoder+decider run INSIDE). AffineScript dependent/affine typing was load-bearing only for the REJECTED proof-term-transport tier. - affinescriptiser is NOT used here, for two independent reasons, documented in AFFINESCRIPTISER-NA.adoc: (1) it structurally requires >=1 [[resources]] and this entry is a pure resource-free verdict function — faking a resource to satisfy the tool would be the exact cargo-culting the verification-honesty doctrine forbids; (2) its own wasm backend is Phase-2-pending (verified). The wasm verdict is identical to the conformance-pinned native verdict by construction (deterministic cargo build of the same pinned, pure, total source). Adds README.adoc + AFFINESCRIPTISER-NA.adoc; .gitignore excludes /target (no build artefact committed). The fail-closed C/Zig C-ABI shim (Phase 3d) stays the attestation FALLBACK tier; the two-tier wiring + stance flip + ADR are P5c-6. Refs hyperpolymath/vcl-ut#25. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/interface/recompute-wasm/.gitignore | 1 + .../recompute-wasm/AFFINESCRIPTISER-NA.adoc | 80 +++++++ src/interface/recompute-wasm/Cargo.lock | 14 ++ src/interface/recompute-wasm/Cargo.toml | 39 ++++ src/interface/recompute-wasm/README.adoc | 65 ++++++ src/interface/recompute-wasm/src/lib.rs | 198 ++++++++++++++++++ 6 files changed, 397 insertions(+) create mode 100644 src/interface/recompute-wasm/.gitignore create mode 100644 src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc create mode 100644 src/interface/recompute-wasm/Cargo.lock create mode 100644 src/interface/recompute-wasm/Cargo.toml create mode 100644 src/interface/recompute-wasm/README.adoc create mode 100644 src/interface/recompute-wasm/src/lib.rs diff --git a/src/interface/recompute-wasm/.gitignore b/src/interface/recompute-wasm/.gitignore new file mode 100644 index 0000000..ea8c4bf --- /dev/null +++ b/src/interface/recompute-wasm/.gitignore @@ -0,0 +1 @@ +/target diff --git a/src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc b/src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc new file mode 100644 index 0000000..344fced --- /dev/null +++ b/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) + +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. diff --git a/src/interface/recompute-wasm/Cargo.lock b/src/interface/recompute-wasm/Cargo.lock new file mode 100644 index 0000000..3aa45f5 --- /dev/null +++ b/src/interface/recompute-wasm/Cargo.lock @@ -0,0 +1,14 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "vcltotal-parse" +version = "0.1.0" + +[[package]] +name = "vcltotal-recompute-wasm" +version = "0.1.0" +dependencies = [ + "vcltotal-parse", +] diff --git a/src/interface/recompute-wasm/Cargo.toml b/src/interface/recompute-wasm/Cargo.toml new file mode 100644 index 0000000..eae0b10 --- /dev/null +++ b/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 "] +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" diff --git a/src/interface/recompute-wasm/README.adoc b/src/interface/recompute-wasm/README.adoc new file mode 100644 index 0000000..304a9ce --- /dev/null +++ b/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) + +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`. diff --git a/src/interface/recompute-wasm/src/lib.rs b/src/interface/recompute-wasm/src/lib.rs new file mode 100644 index 0000000..7351908 --- /dev/null +++ b/src/interface/recompute-wasm/src/lib.rs @@ -0,0 +1,198 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! P5c (#25) — the recompute-PCC tier's `wasm32` entry point. +//! +//! ROLE (see `VERIFICATION-STANCE.adoc`'s two-tier boundary model). +//! Under the locked recompute design, the consumer is shipped this +//! wasm module + the wire bytes of a `(Statement, OctadSchema)` + the +//! producer's claimed safety level. The consumer **re-runs the +//! certified decision** here and compares. The guarantee is NOT the +//! wasm's type system: it is (a) the corpus proof `checkLevelNSound` +//! (machine-checked once, offline-re-checkable with idris2), and (b) +//! the cross-language conformance pin (`tests/conformance_emit.rs` ⇄ +//! `WireConformance`) that `vcltotal_parse::certified_level` is a +//! faithful image of the corpus decision. This crate adds only the +//! host/guest memory ABI; it introduces no decision logic. +//! +//! Plain `wasm32-unknown-unknown` is *sufficient* for this argument: +//! nothing structured crosses the boundary that needs type-preservation +//! — opaque wire bytes go in, an `i64` verdict comes out, and the +//! decoder+decider run *inside* the module on those bytes. AffineScript +//! dependent/affine typing was load-bearing only for the *rejected* +//! proof-term-transport tier. +//! +//! Why NOT `affinescriptiser` here (disclosed, not an oversight). The +//! estate's Rust→typed-wasm wrapper is resource-oriented: it +//! *structurally requires* at least one `[[resources]]` entry +//! (allocator/deallocator/affinity) and exists to prove at-most-once +//! resource use. This entry is a **pure total verdict function** — it +//! owns no file descriptors, sockets, GPU buffers or linear handles, +//! so there is nothing for the affine checker to track; declaring a +//! fake resource purely to satisfy the tool would be exactly the kind +//! of cargo-culting the estate verification-honesty doctrine forbids. +//! (Independently, affinescriptiser's own wasm backend is +//! Phase-2-pending.) The recompute security argument does not need it: +//! soundness is the corpus proof, faithfulness is the conformance pin, +//! and the wasm is a deterministic `cargo build` of the pinned source. +//! See `src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc`. +//! +//! UNSAFE POLICY. All decision/decoding logic lives in the +//! `#![forbid(unsafe_code)]` `vcltotal-parse` crate. The ONLY `unsafe` +//! in the entire recompute path is the small, audited host/guest +//! memory-ABI block below — which *is* the declared trust boundary +//! (the host is trusted to pass valid `(ptr, len)` into linear +//! memory). Every byte of judgement remains in the verified-posture +//! crate. +//! +//! FAIL-CLOSED. Any malformed wire input (`WireError`) yields `-1` +//! (Reject) — never a fabricated level. `certified_level` itself +//! returns `-1` when any required level is not established. So the +//! only non-negative result is a genuinely recomputed certified level. + +#![deny(clippy::undocumented_unsafe_blocks)] + +use core::slice; +use vcltotal_parse::{certified_level, from_wire, from_wire_schema}; + +/// Allocate `len` bytes of guest linear memory and return a pointer the +/// host can write wire bytes into. Pair with [`vcl_dealloc`]. +/// +/// # Safety +/// Caller (the host) must later pass the returned pointer and the same +/// `len` to [`vcl_dealloc`] exactly once, and must not retain it after. +#[no_mangle] +pub extern "C" fn vcl_alloc(len: usize) -> *mut u8 { + let mut buf = Vec::::with_capacity(len); + let ptr = buf.as_mut_ptr(); + core::mem::forget(buf); + ptr +} + +/// Free a buffer previously returned by [`vcl_alloc`]. +/// +/// # Safety +/// `ptr`/`len` must be exactly a pair returned by one prior +/// [`vcl_alloc`] call, not yet freed. +#[no_mangle] +pub unsafe extern "C" fn vcl_dealloc(ptr: *mut u8, len: usize) { + if !ptr.is_null() && len != 0 { + // SAFETY: by this function's documented contract `ptr`/`len` + // are exactly a prior `vcl_alloc` pair (capacity == len, never + // freed). Reconstituting and dropping the `Vec` frees it. + unsafe { + drop(Vec::from_raw_parts(ptr, 0, len)); + } + } +} + +/// Recompute the certified safety level of a wire-encoded +/// `(Statement, OctadSchema)`. +/// +/// Returns the certified level (`0..=10`) iff every required level is +/// re-established by the faithful in-corpus-image decider; `-1` +/// (Reject) on any decode failure or any unmet level — fail-closed, +/// never a fabricated level. +/// +/// # Safety +/// `stmt_ptr`/`stmt_len` and `schema_ptr`/`schema_len` must each +/// describe an initialised, readable byte range in guest linear memory +/// (typically buffers from [`vcl_alloc`] the host filled). This is the +/// declared host↔guest trust boundary. +#[no_mangle] +pub unsafe extern "C" fn vcl_recompute( + stmt_ptr: *const u8, + stmt_len: usize, + schema_ptr: *const u8, + schema_len: usize, +) -> i64 { + if stmt_ptr.is_null() || schema_ptr.is_null() { + return -1; + } + // SAFETY: the *only* unsafe in the recompute path. By this + // function's documented ABI contract the two (ptr, len) pairs are + // valid initialised ranges in guest linear memory. We immediately + // narrow to shared slices and hand them to the + // `#![forbid(unsafe_code)]` decoder; no raw pointer escapes. + let (stmt_bytes, schema_bytes) = unsafe { + ( + slice::from_raw_parts(stmt_ptr, stmt_len), + slice::from_raw_parts(schema_ptr, schema_len), + ) + }; + match (from_wire(stmt_bytes), from_wire_schema(schema_bytes)) { + (Ok(stmt), Ok(schema)) => certified_level(&stmt, &schema), + _ => -1, + } +} + +#[cfg(test)] +mod tests { + #![allow(clippy::unwrap_used)] + use super::*; + use vcltotal_parse::{to_wire, to_wire_schema}; + + // The native-target faithfulness pin is in + // `vcltotal-parse`'s conformance harness (Rust `certified_level` + // == corpus on shared bytes). The wasm artefact is `cargo build` + // of that *same* source, so the verdict is identical by + // construction (pure, total, deterministic integer logic — no + // platform-dependent behaviour). This test re-asserts the + // fail-closed boundary contract through the actual entry on the + // host target. + fn rt(stmt: &[u8], schema: &[u8]) -> i64 { + // SAFETY: valid slices from owned Vecs (test only). + unsafe { vcl_recompute(stmt.as_ptr(), stmt.len(), schema.as_ptr(), schema.len()) } + } + + #[test] + fn garbage_is_fail_closed_not_a_level() { + assert_eq!(rt(b"", b""), -1); + assert_eq!(rt(b"not-vclw", b"not-vcls"), -1); + assert_eq!(rt(&[0xff; 64], &[0xff; 64]), -1); + } + + #[test] + fn null_pointers_reject() { + // SAFETY: deliberately passing null — the entry checks for it. + let r = unsafe { vcl_recompute(core::ptr::null(), 0, core::ptr::null(), 0) }; + assert_eq!(r, -1); + } + + #[test] + fn well_formed_roundtrips_through_the_boundary() { + // Minimal valid Statement (SELECT * FROM STORE "s", + // requestedLevel ParseSafe) + empty-ish schema ⇒ level 0 + // (ParseSafe gate is unconditional). + use vcltotal_parse::ast::*; + use vcltotal_parse::schema::*; + let s = Statement { + select_items: vec![SelectItem::Star], + source: Source::Store("s".to_string()), + where_clause: None, + group_by: vec![], + having: None, + order_by: vec![], + limit: None, + offset: None, + proof_clause: None, + effect_decl: None, + version_const: None, + linear_annot: None, + epistemic_clause: None, + requested_level: SafetyLevel::ParseSafe, + }; + let m = |modality, fields| ModalitySchema { modality, fields }; + let sc = OctadSchema { + graph: m(Modality::Graph, vec![]), + vector: m(Modality::Vector, vec![]), + tensor: m(Modality::Tensor, vec![]), + semantic: m(Modality::Semantic, vec![]), + document: m(Modality::Document, vec![]), + temporal: m(Modality::Temporal, vec![]), + provenance: m(Modality::Provenance, vec![]), + spatial: m(Modality::Spatial, vec![]), + }; + assert_eq!(rt(&to_wire(&s), &to_wire_schema(&sc)), 0); + } +}