vcl-ut #25 P5d: Tier-2 C-ABI Ed25519 attestation fallback (RESOLVED) — closes the workstream

CHANGELOG.md

@@ -63,11 +63,23 @@ CI-gated and green:
   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:
+  `AFFINESCRIPTISER-NA.adoc`, not faked).
+- Phase 5 / vcl-ut#25 — **Tier-2 (P5d) RESOLVED**: `src/interface/attest`
+  (`vcltotal-attest`) mints/verifies an Ed25519 attestation over
+  `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` (level =
+  the conformance-pinned `certified_level`, signed iff `0..=10`,
+  fail-closed); the previously-OWED `vclut_rs_verify` backend is this
+  crate, linked into `ffi/zig/src/lib.zig` (`vclut_verify_wire`) by
+  `build.zig` (`zig build test` 4/4, end-to-end). Unforgeable + bound
+  (roundtrip + 5 tamper variants + fail-closed + C-ABI tests).
+  `ed25519-dalek`/`sha2` contained to the Tier-2 crate; zero-dep
+  forbid-unsafe core untouched; one audited host/guest `unsafe` block.
+  Spec `src/interface/attest/ATTESTATION-FORMAT.adoc`; ADR-0002 →
+  both tiers RESOLVED. **The vcl-ut#25 boundary-reinforcement
+  workstream is complete** (only the precisely-scoped disclosed limits
+  remain — not gaps). A re-checkable proof is impossible *only* over
+  the C-ABI fallback tier; Tier-2 is honestly its weaker
+  trusted-certifier ceiling (canonical two-tier model:
   `verification/proofs/VERIFICATION-STANCE.adoc`).
 
 `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative,

PROOF-NEEDS.md

@@ -61,10 +61,14 @@
   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
+  `affinescriptiser` N/A (disclosed). **P5d — RESOLVED (Tier-2
+  fallback):** `src/interface/attest` mints/verifies an Ed25519
+  attestation bound to `(sha256(stmt_wire), sha256(schema_wire),
+  level)` (fail-closed); the `vclut_rs_verify` backend is linked into
+  `ffi/zig` (`vclut_verify_wire`, `zig build test` green end-to-end).
+  Trusted-certifier (weaker than Tier-1), crypto contained. **The
+  vcl-ut#25 workstream is complete** — only precisely-scoped disclosed
+  limits remain (not gaps). 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

docs/decisions/0002-ffi-attestation-trust-boundary.adoc

@@ -8,8 +8,10 @@ Date: 2026-05-19
 
 ## Status
 
-Accepted (Tier-1 RESOLVED; Tier-2 / P5d OWED). Tracked:
-hyperpolymath/vcl-ut#25. Authoritative companion:
+Accepted (**both tiers RESOLVED** — Tier-1 recompute-PCC over `wasm32`;
+Tier-2 / P5d C-ABI Ed25519 attestation fallback, `src/interface/attest`
+linked into the Zig shim). 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*.
@@ -75,12 +77,22 @@ 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.
+**Tier-2 — C-ABI trusted-certifier attestation (fallback, P5d,
+RESOLVED).** For consumers that cannot run the Tier-1 wasm:
+`src/interface/attest` (`vcltotal-attest`) mints an Ed25519 signature
+over `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level`, where
+`level` is the conformance-pinned `vcltotal_parse::certified_level`
+(signed iff `0..=10`, fail-closed); the consumer Ed25519-verifies
+against the certifier's public key. Unforgeable and bound (tamper /
+wrong-key all reject — machine-tested). The previously-OWED
+`vclut_rs_verify` backend is this crate, linked into the `ffi/zig`
+shim (`vclut_verify_wire`) by `build.zig`; `zig build test` exercises
+the boundary end-to-end. Strictly weaker than Tier-1 (pure trust in
+the minting certifier + that it ran the pinned decider), and labelled
+as such everywhere. Spec:
+`src/interface/attest/ATTESTATION-FORMAT.adoc`; crypto
+(`ed25519-dalek`/`sha2`) contained to this Tier-2 crate, the
+zero-dep forbid-unsafe core untouched.
 
 ## Consequences
 
@@ -99,8 +111,12 @@ scaffolding; the signed contract + `vclut_rs_verify` linkage are OWED.
   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
+- P5d (Tier-2) is **delivered**: non-wasm consumers get a verifiable
+  bound attestation (fail-closed) instead of only the bare shim. The
+  vcl-ut#25 boundary-reinforcement workstream is complete; what
+  remains are the precisely-scoped disclosed limits above, not gaps.
+- (historical) Until P5d landed, non-wasm consumers received 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

ffi/zig/build.zig

@@ -7,26 +7,49 @@
 //   - libvclut_ffi.so       shared library for Idris2 / OCaml / SPARK consumers
 //   - libvclut_ffi.a        static library variant
 //   - test runner           `zig build test`
+//
+// P5d (vcl-ut#25): the Tier-2 attestation backend `vclut_rs_verify`
+// (previously declared-but-unlinked, NAMED OWED) is now the Rust
+// `vcltotal-attest` crate (`src/interface/attest`). build.zig compiles
+// that staticlib via cargo and links it into every artefact (incl. the
+// test runner), so the shim's `vclut_verify_wire` calls a real,
+// conformance-pinned, fail-closed backend — not a stub.
 
 const std = @import("std");
 
 pub fn build(b: *std.Build) void {
     const target = b.standardTargetOptions(.{});
     const optimize = b.standardOptimizeOption(.{});
 
+    // Build the Rust Tier-2 backend staticlib (libvcltotal_attest.a).
+    const cargo = b.addSystemCommand(&.{
+        "cargo",                "build",
+        "--release",            "--manifest-path",
+        "../../src/interface/attest/Cargo.toml",
+    });
+
+    const attest_a = b.path("../../src/interface/attest/target/release/libvcltotal_attest.a");
+
     const lib_mod = b.createModule(.{
         .root_source_file = b.path("src/lib.zig"),
         .target = target,
         .optimize = optimize,
         .link_libc = true,
     });
+    // Link the Rust Tier-2 staticlib. glibc (link_libc) covers
+    // pthread/dl/m/rt; `gcc_s` provides the `_Unwind_*` personality
+    // symbols Rust `std` references (backtrace/personality) even under
+    // `panic = "abort"`. This is the standard Rust-staticlib companion.
+    lib_mod.addObjectFile(attest_a);
+    lib_mod.linkSystemLibrary("gcc_s", .{});
 
     // Shared library variant
     const shared = b.addLibrary(.{
         .name = "vclut_ffi",
         .root_module = lib_mod,
         .linkage = .dynamic,
     });
+    shared.step.dependOn(&cargo.step);
     b.installArtifact(shared);
 
     // Static library variant
@@ -35,12 +58,14 @@ pub fn build(b: *std.Build) void {
         .root_module = lib_mod,
         .linkage = .static,
     });
+    static.step.dependOn(&cargo.step);
     b.installArtifact(static);
 
-    // Tests
+    // Tests (linked against the real Rust backend)
     const tests = b.addTest(.{
         .root_module = lib_mod,
     });
+    tests.step.dependOn(&cargo.step);
     const run_tests = b.addRunArtifact(tests);
     const test_step = b.step("test", "Run vcl-ut FFI tests");
     test_step.dependOn(&run_tests.step);

ffi/zig/src/lib.zig

@@ -41,6 +41,32 @@ fn clearLastError() void {
     last_error_len = 0;
 }
 
+// ──────────────────────────────────────────────────────────────────────
+// Tier-2 backend (P5d, vcl-ut#25) — the real `vclut_rs_verify`.
+//
+// Previously NAMED OWED ("declared in intent but not linked"). Now
+// implemented by the Rust `vcltotal-attest` crate
+// (`src/interface/attest`) and linked by build.zig. It decodes the
+// wire `(Statement, OctadSchema)`, runs the conformance-pinned
+// `vcltotal_parse::certified_level` (the same faithful image of the
+// Idris corpus decision Tier-1 uses), and on a genuine level mints an
+// Ed25519 attestation bound to `(sha256(stmt_wire), sha256(schema_wire),
+// level)`. Fail-closed: a Reject / decode failure yields -1 and NO
+// token. This is the Tier-2 *fallback* (trusted-certifier attestation)
+// — explicitly weaker than Tier-1 recompute-PCC; see
+// verification/proofs/VERIFICATION-STANCE.adoc.
+// ──────────────────────────────────────────────────────────────────────
+
+extern fn vclut_rs_verify(
+    stmt_ptr: [*]const u8,
+    stmt_len: usize,
+    schema_ptr: [*]const u8,
+    schema_len: usize,
+    sk_ptr: [*]const u8,
+    out_ptr: [*]u8,
+    out_cap: usize,
+) callconv(.c) i64;
+
 // ──────────────────────────────────────────────────────────────────────
 // C-ABI exports
 // ──────────────────────────────────────────────────────────────────────
@@ -91,6 +117,48 @@ pub export fn vclut_verify_query(
 /// Get the last error message. Returns an empty string when no error
 /// is pending. Caller does not own the pointer; copy before the next
 /// FFI call.
+/// Tier-2 (P5d): verify a wire-marshalled `(Statement, OctadSchema)`
+/// and, on a genuine certified level, emit a signed attestation.
+///
+/// `stmt`/`schema` are the v1 wire bytes (the C-ABI marshalling, same
+/// shape as the Tier-1 recompute module). `sk` is the certifier's
+/// 32-byte Ed25519 seed (real provisioning is deployment, via the
+/// estate token vault). On success returns the level `0..10` and
+/// writes a 65-byte token `[level:1][sig:64]` into `out` (needs
+/// `out_cap >= 65`). Returns -1 (Rejected) — writing nothing,
+/// `vclut_last_error` set — on any decode failure, a Reject level, a
+/// null pointer, or insufficient `out_cap`. **Fail-closed:** never a
+/// token for a level the certifier did not establish.
+pub export fn vclut_verify_wire(
+    stmt_ptr: [*]const u8,
+    stmt_len: usize,
+    schema_ptr: [*]const u8,
+    schema_len: usize,
+    sk_ptr: [*]const u8,
+    out_ptr: [*]u8,
+    out_cap: usize,
+) callconv(.c) c_int {
+    clearLastError();
+    const rc = vclut_rs_verify(
+        stmt_ptr,
+        stmt_len,
+        schema_ptr,
+        schema_len,
+        sk_ptr,
+        out_ptr,
+        out_cap,
+    );
+    if (rc < 0) {
+        setLastError("Rejected (fail-closed): no genuine certified " ++
+            "level — Tier-2 attestation NOT minted. The verification " ++
+            "authority is the conformance-pinned certified_level; see " ++
+            "verification/proofs/VERIFICATION-STANCE.adoc");
+        return -1;
+    }
+    // 0..10 fits c_int; rc is bounded by the Rust backend.
+    return @intCast(rc);
+}
+
 pub export fn vclut_last_error() callconv(.c) [*:0]const u8 {
     if (last_error_len == 0) return "";
     return @ptrCast(&last_error_buf[0]);
@@ -123,3 +191,21 @@ test "verify is fail-closed: no fabricated level without a backend" {
     // and it never returns a "verified" (>=1) level here
     try std.testing.expect(rc < 1);
 }
+
+// P5d integration: the REAL Rust Tier-2 backend is linked
+// (libvcltotal_attest.a via build.zig). Garbage wire bytes must
+// decode-fail in the conformance-pinned decoder ⇒ no attestation ⇒
+// -1, end-to-end across the Zig↔Rust boundary. (A positive path needs
+// a valid wire (Statement,OctadSchema), exhaustively covered by the
+// Rust crate's own roundtrip/tamper suite; this asserts the
+// fail-closed contract through the actual linked symbol.)
+test "vclut_verify_wire fail-closed on garbage via the linked Rust backend" {
+    _ = vclut_init();
+    var out: [65]u8 = [_]u8{0xAA} ** 65;
+    const sk = [_]u8{7} ** 32;
+    const bad = [_]u8{0xFF} ** 8;
+    const rc = vclut_verify_wire(&bad, bad.len, &bad, bad.len, &sk, &out, out.len);
+    try std.testing.expectEqual(@as(c_int, -1), rc);
+    // out untouched on the fail-closed path
+    for (out) |byte| try std.testing.expectEqual(@as(u8, 0xAA), byte);
+}

src/interface/attest/.gitignore

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

src/interface/attest/ATTESTATION-FORMAT.adoc

@@ -0,0 +1,93 @@
+= VCL-total Tier-2 Attestation Format v1 (P5d, vcl-ut#25)
+:toc:
+
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+Normative format for the **Tier-2 (C-ABI trusted-certifier
+attestation) FALLBACK**. See `verification/proofs/VERIFICATION-STANCE.adoc`
+(authoritative) for the two-tier boundary model and ADR
+`docs/decisions/0002-ffi-attestation-trust-boundary.adoc` for the
+rationale. Tier-1 (recompute-PCC over `wasm32`) is the achieved tier;
+this is the explicit *weaker* fallback for consumers that cannot run
+the Tier-1 module.
+
+== Trust model (stated, not hidden)
+
+A C ABI erases types, so it cannot carry a re-checkable dependent
+proof. The honest ceiling is *trusted-certifier attestation*: the
+consumer **trusts** that (a) the Ed25519 private key is held only by a
+genuine certifier and (b) that certifier ran the conformance-pinned
+`vcltotal_parse::certified_level` (the same faithful image of the Idris
+corpus decision Tier-1 uses) before signing. The token is *unforgeable*
+and *bound*: it cannot be fabricated, transplanted onto a different
+query/schema, or have its level escalated. This is strictly weaker than
+Tier-1 (which trusts neither (a) nor (b) — it recomputes). It is **not**
+a re-checkable proof and does not claim to be.
+
+== Signed message (81 bytes, fixed)
+
+[cols="1,3"]
+|===
+| `DOMAIN`        | 16 bytes — `"VCLT-ATTEST-v1\0\0"` (protocol/version domain separation; a signature here can never be replayed as any other protocol)
+| `sha256(stmt_wire)`   | 32 bytes — SHA-256 of the v1 `Statement` wire bytes (`VCLW…`, see `WIRE-FORMAT.adoc`)
+| `sha256(schema_wire)` | 32 bytes — SHA-256 of the v1 `OctadSchema` wire bytes (`VCLS…`)
+| `level`         | 1 byte — the certified level `0..=10`
+|===
+
+`token = Ed25519_sign(certifier_sk, DOMAIN ‖ sha256(stmt_wire) ‖
+sha256(schema_wire) ‖ level)` — a detached 64-byte signature.
+
+`schema_id` is `sha256(schema_wire)` (content-addressed; no external
+registry/trust). "query" in the issue-#25 phrasing
+`(sha256(query), schema_id, level)` is the marshalled `Statement`
+(`sha256(stmt_wire)`).
+
+== Wire token layout (C-ABI `out`)
+
+65 bytes: `[ level : u8 ][ sig : 64 bytes ]`.
+
+== Mint / verify
+
+* *Mint* (certifier side): decode `(stmt_wire, schema_wire)`; run
+  `certified_level`; **iff** `0 <= level <= 10`, sign and emit the
+  token. Any decode failure or Reject ⇒ **no token** (fail-closed —
+  never a token for an unestablished level).
+* *Verify* (consumer side): recompute the 81-byte message from the
+  wire bytes the consumer holds + the attested `level`; Ed25519-verify
+  against the certifier's public key. Accept the level iff verification
+  succeeds. Verification does **not** re-run the decider — that is
+  Tier-1's role; Tier-2 trusts the certifier by construction of a C
+  ABI.
+
+A tampered `stmt_wire`, `schema_wire`, `level`, or `sig`, or a wrong
+public key, all fail verification (machine-tested:
+`src/interface/attest` — roundtrip + 5 tamper variants + fail-closed +
+C-ABI).
+
+== C-ABI
+
+`vclut_rs_verify(stmt_ptr, stmt_len, schema_ptr, schema_len, sk_ptr,
+out_ptr, out_cap) -> i64` (Rust, `src/interface/attest`), linked into
+the Zig shim `ffi/zig/src/lib.zig` and exposed as
+`vclut_verify_wire(...)`. Returns the level `0..10` (and writes the
+65-byte token) or `-1` Rejected (writes nothing; `vclut_last_error`
+set). `sk_ptr` is the certifier's 32-byte Ed25519 seed — **real key
+provisioning is deployment**, via the estate token vault
+(`hyperpolymath/reasonably-good-token-vault`); the test key
+(`[7u8;32]`) is NOT a real certifier key.
+
+== Crypto
+
+Ed25519 via `ed25519-dalek` (de-facto standard, widely audited;
+maintainer decision 2026-05-19), SHA-256 via `sha2`. Both are
+*contained* in the separate `vcltotal-attest` crate (Tier-2 only) and
+never touch the zero-dependency, `#![forbid(unsafe_code)]`
+`vcltotal-parse` core. The only `unsafe` is one audited host/guest
+C-ABI memory block.
+
+== Versioning
+
+Any change to the wire formats, message layout, or crypto bumps
+`DOMAIN` (`VCLT-ATTEST-vN`) so old signatures cannot be
+reinterpreted. Tracked: hyperpolymath/vcl-ut#25.