Skip to content

Commit e4e3f99

Browse files
Merge pull request #34 from hyperpolymath/reinforce/vclut-25-phase5d-attest
vcl-ut #25 P5d: Tier-2 C-ABI Ed25519 attestation fallback (RESOLVED) — closes the workstream
2 parents 2b52266 + 2b4cc26 commit e4e3f99

12 files changed

Lines changed: 1168 additions & 87 deletions

File tree

CHANGELOG.md

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -63,11 +63,23 @@ CI-gated and green:
6363
recomputation, not proof transport. Plain `wasm32` suffices (type
6464
system not load-bearing under recompute); `affinescriptiser` N/A
6565
(resource-required + wasm-backend-pending; disclosed in
66-
`AFFINESCRIPTISER-NA.adoc`, not faked). **OWED — P5d (Tier-2
67-
fallback):** the C-ABI signed-attestation contract +
68-
`vclut_rs_verify` linkage for consumers that cannot run the wasm.
69-
A re-checkable proof is impossible *only* over the C-ABI fallback
70-
tier (canonical two-tier model:
66+
`AFFINESCRIPTISER-NA.adoc`, not faked).
67+
- Phase 5 / vcl-ut#25**Tier-2 (P5d) RESOLVED**: `src/interface/attest`
68+
(`vcltotal-attest`) mints/verifies an Ed25519 attestation over
69+
`DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` (level =
70+
the conformance-pinned `certified_level`, signed iff `0..=10`,
71+
fail-closed); the previously-OWED `vclut_rs_verify` backend is this
72+
crate, linked into `ffi/zig/src/lib.zig` (`vclut_verify_wire`) by
73+
`build.zig` (`zig build test` 4/4, end-to-end). Unforgeable + bound
74+
(roundtrip + 5 tamper variants + fail-closed + C-ABI tests).
75+
`ed25519-dalek`/`sha2` contained to the Tier-2 crate; zero-dep
76+
forbid-unsafe core untouched; one audited host/guest `unsafe` block.
77+
Spec `src/interface/attest/ATTESTATION-FORMAT.adoc`; ADR-0002 →
78+
both tiers RESOLVED. **The vcl-ut#25 boundary-reinforcement
79+
workstream is complete** (only the precisely-scoped disclosed limits
80+
remain — not gaps). A re-checkable proof is impossible *only* over
81+
the C-ABI fallback tier; Tier-2 is honestly its weaker
82+
trusted-certifier ceiling (canonical two-tier model:
7183
`verification/proofs/VERIFICATION-STANCE.adoc`).
7284

7385
`verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative,

PROOF-NEEDS.md

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -61,10 +61,14 @@
6161
runtime + the once-proved corpus (offline-re-checkable) — *not* a
6262
trusted tag, *not* a transported proof object. Plain `wasm32`
6363
suffices (type system not load-bearing under recompute);
64-
`affinescriptiser` N/A (disclosed). **P5d — OWED (Tier-2 fallback):**
65-
the C-ABI signed-attestation contract + `vclut_rs_verify` linkage,
66-
for consumers that cannot run the wasm; the `ffi/zig` fail-closed
67-
shim is its scaffolding. See the canonical two-tier boundary model
64+
`affinescriptiser` N/A (disclosed). **P5d — RESOLVED (Tier-2
65+
fallback):** `src/interface/attest` mints/verifies an Ed25519
66+
attestation bound to `(sha256(stmt_wire), sha256(schema_wire),
67+
level)` (fail-closed); the `vclut_rs_verify` backend is linked into
68+
`ffi/zig` (`vclut_verify_wire`, `zig build test` green end-to-end).
69+
Trusted-certifier (weaker than Tier-1), crypto contained. **The
70+
vcl-ut#25 workstream is complete** — only precisely-scoped disclosed
71+
limits remain (not gaps). See the canonical two-tier boundary model
6872
in `verification/proofs/VERIFICATION-STANCE.adoc` (authoritative).
6973
- Optional future work: prove the ReScript frontend faithfully tracks
7074
the Idris2 grammar (low priority; it is a convenience frontend, not a

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

Lines changed: 26 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,10 @@ Date: 2026-05-19
88

99
## Status
1010

11-
Accepted (Tier-1 RESOLVED; Tier-2 / P5d OWED). Tracked:
12-
hyperpolymath/vcl-ut#25. Authoritative companion:
11+
Accepted (**both tiers RESOLVED** — Tier-1 recompute-PCC over `wasm32`;
12+
Tier-2 / P5d C-ABI Ed25519 attestation fallback, `src/interface/attest`
13+
linked into the Zig shim). Tracked: hyperpolymath/vcl-ut#25.
14+
Authoritative companion:
1315
`verification/proofs/VERIFICATION-STANCE.adoc` (canonical two-tier
1416
boundary model) — this ADR records *why*; the stance records *what is
1517
and is not proven*.
@@ -75,12 +77,22 @@ fabricated level. The only `unsafe` is one audited host/guest
7577
memory-ABI block — the declared trust boundary — with all
7678
decode/decision logic in the `#![forbid(unsafe_code)]` crate.
7779

78-
**Tier-2 — C-ABI trusted-certifier attestation (fallback, P5d, OWED).**
79-
For consumers that cannot run the Tier-1 wasm: a signed token bound to
80-
`(sha256(query), schema_id, level)`, verified against the certifier's
81-
public key. Strictly weaker (pure trust in the minting certifier), and
82-
labelled as such. The fail-closed `ffi/zig` shim (Phase 3d) is its
83-
scaffolding; the signed contract + `vclut_rs_verify` linkage are OWED.
80+
**Tier-2 — C-ABI trusted-certifier attestation (fallback, P5d,
81+
RESOLVED).** For consumers that cannot run the Tier-1 wasm:
82+
`src/interface/attest` (`vcltotal-attest`) mints an Ed25519 signature
83+
over `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level`, where
84+
`level` is the conformance-pinned `vcltotal_parse::certified_level`
85+
(signed iff `0..=10`, fail-closed); the consumer Ed25519-verifies
86+
against the certifier's public key. Unforgeable and bound (tamper /
87+
wrong-key all reject — machine-tested). The previously-OWED
88+
`vclut_rs_verify` backend is this crate, linked into the `ffi/zig`
89+
shim (`vclut_verify_wire`) by `build.zig`; `zig build test` exercises
90+
the boundary end-to-end. Strictly weaker than Tier-1 (pure trust in
91+
the minting certifier + that it ran the pinned decider), and labelled
92+
as such everywhere. Spec:
93+
`src/interface/attest/ATTESTATION-FORMAT.adoc`; crypto
94+
(`ed25519-dalek`/`sha2`) contained to this Tier-2 crate, the
95+
zero-dep forbid-unsafe core untouched.
8496

8597
## Consequences
8698

@@ -99,8 +111,12 @@ scaffolding; the signed contract + `vclut_rs_verify` linkage are OWED.
99111
Rust-side + by input-value conformance; L9/L10 predicate depth;
100112
additive↔ceil `alignUp` sliver). These are stated in
101113
VERIFICATION-STANCE.adoc, not faked.
102-
- P5d (Tier-2) is the remaining boundary work; until it lands,
103-
non-wasm consumers receive only the fail-closed shim (no fabricated
114+
- P5d (Tier-2) is **delivered**: non-wasm consumers get a verifiable
115+
bound attestation (fail-closed) instead of only the bare shim. The
116+
vcl-ut#25 boundary-reinforcement workstream is complete; what
117+
remains are the precisely-scoped disclosed limits above, not gaps.
118+
- (historical) Until P5d landed, non-wasm consumers received only the
119+
fail-closed shim (no fabricated
104120
level).
105121
- Revisit only if a future revision genuinely introduces a tracked
106122
resource at this boundary (none foreseen for a pure verdict

ffi/zig/build.zig

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,26 +7,49 @@
77
// - libvclut_ffi.so shared library for Idris2 / OCaml / SPARK consumers
88
// - libvclut_ffi.a static library variant
99
// - test runner `zig build test`
10+
//
11+
// P5d (vcl-ut#25): the Tier-2 attestation backend `vclut_rs_verify`
12+
// (previously declared-but-unlinked, NAMED OWED) is now the Rust
13+
// `vcltotal-attest` crate (`src/interface/attest`). build.zig compiles
14+
// that staticlib via cargo and links it into every artefact (incl. the
15+
// test runner), so the shim's `vclut_verify_wire` calls a real,
16+
// conformance-pinned, fail-closed backend — not a stub.
1017

1118
const std = @import("std");
1219

1320
pub fn build(b: *std.Build) void {
1421
const target = b.standardTargetOptions(.{});
1522
const optimize = b.standardOptimizeOption(.{});
1623

24+
// Build the Rust Tier-2 backend staticlib (libvcltotal_attest.a).
25+
const cargo = b.addSystemCommand(&.{
26+
"cargo", "build",
27+
"--release", "--manifest-path",
28+
"../../src/interface/attest/Cargo.toml",
29+
});
30+
31+
const attest_a = b.path("../../src/interface/attest/target/release/libvcltotal_attest.a");
32+
1733
const lib_mod = b.createModule(.{
1834
.root_source_file = b.path("src/lib.zig"),
1935
.target = target,
2036
.optimize = optimize,
2137
.link_libc = true,
2238
});
39+
// Link the Rust Tier-2 staticlib. glibc (link_libc) covers
40+
// pthread/dl/m/rt; `gcc_s` provides the `_Unwind_*` personality
41+
// symbols Rust `std` references (backtrace/personality) even under
42+
// `panic = "abort"`. This is the standard Rust-staticlib companion.
43+
lib_mod.addObjectFile(attest_a);
44+
lib_mod.linkSystemLibrary("gcc_s", .{});
2345

2446
// Shared library variant
2547
const shared = b.addLibrary(.{
2648
.name = "vclut_ffi",
2749
.root_module = lib_mod,
2850
.linkage = .dynamic,
2951
});
52+
shared.step.dependOn(&cargo.step);
3053
b.installArtifact(shared);
3154

3255
// Static library variant
@@ -35,12 +58,14 @@ pub fn build(b: *std.Build) void {
3558
.root_module = lib_mod,
3659
.linkage = .static,
3760
});
61+
static.step.dependOn(&cargo.step);
3862
b.installArtifact(static);
3963

40-
// Tests
64+
// Tests (linked against the real Rust backend)
4165
const tests = b.addTest(.{
4266
.root_module = lib_mod,
4367
});
68+
tests.step.dependOn(&cargo.step);
4469
const run_tests = b.addRunArtifact(tests);
4570
const test_step = b.step("test", "Run vcl-ut FFI tests");
4671
test_step.dependOn(&run_tests.step);

ffi/zig/src/lib.zig

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,32 @@ fn clearLastError() void {
4141
last_error_len = 0;
4242
}
4343

44+
// ──────────────────────────────────────────────────────────────────────
45+
// Tier-2 backend (P5d, vcl-ut#25) — the real `vclut_rs_verify`.
46+
//
47+
// Previously NAMED OWED ("declared in intent but not linked"). Now
48+
// implemented by the Rust `vcltotal-attest` crate
49+
// (`src/interface/attest`) and linked by build.zig. It decodes the
50+
// wire `(Statement, OctadSchema)`, runs the conformance-pinned
51+
// `vcltotal_parse::certified_level` (the same faithful image of the
52+
// Idris corpus decision Tier-1 uses), and on a genuine level mints an
53+
// Ed25519 attestation bound to `(sha256(stmt_wire), sha256(schema_wire),
54+
// level)`. Fail-closed: a Reject / decode failure yields -1 and NO
55+
// token. This is the Tier-2 *fallback* (trusted-certifier attestation)
56+
// — explicitly weaker than Tier-1 recompute-PCC; see
57+
// verification/proofs/VERIFICATION-STANCE.adoc.
58+
// ──────────────────────────────────────────────────────────────────────
59+
60+
extern fn vclut_rs_verify(
61+
stmt_ptr: [*]const u8,
62+
stmt_len: usize,
63+
schema_ptr: [*]const u8,
64+
schema_len: usize,
65+
sk_ptr: [*]const u8,
66+
out_ptr: [*]u8,
67+
out_cap: usize,
68+
) callconv(.c) i64;
69+
4470
// ──────────────────────────────────────────────────────────────────────
4571
// C-ABI exports
4672
// ──────────────────────────────────────────────────────────────────────
@@ -91,6 +117,48 @@ pub export fn vclut_verify_query(
91117
/// Get the last error message. Returns an empty string when no error
92118
/// is pending. Caller does not own the pointer; copy before the next
93119
/// FFI call.
120+
/// Tier-2 (P5d): verify a wire-marshalled `(Statement, OctadSchema)`
121+
/// and, on a genuine certified level, emit a signed attestation.
122+
///
123+
/// `stmt`/`schema` are the v1 wire bytes (the C-ABI marshalling, same
124+
/// shape as the Tier-1 recompute module). `sk` is the certifier's
125+
/// 32-byte Ed25519 seed (real provisioning is deployment, via the
126+
/// estate token vault). On success returns the level `0..10` and
127+
/// writes a 65-byte token `[level:1][sig:64]` into `out` (needs
128+
/// `out_cap >= 65`). Returns -1 (Rejected) — writing nothing,
129+
/// `vclut_last_error` set — on any decode failure, a Reject level, a
130+
/// null pointer, or insufficient `out_cap`. **Fail-closed:** never a
131+
/// token for a level the certifier did not establish.
132+
pub export fn vclut_verify_wire(
133+
stmt_ptr: [*]const u8,
134+
stmt_len: usize,
135+
schema_ptr: [*]const u8,
136+
schema_len: usize,
137+
sk_ptr: [*]const u8,
138+
out_ptr: [*]u8,
139+
out_cap: usize,
140+
) callconv(.c) c_int {
141+
clearLastError();
142+
const rc = vclut_rs_verify(
143+
stmt_ptr,
144+
stmt_len,
145+
schema_ptr,
146+
schema_len,
147+
sk_ptr,
148+
out_ptr,
149+
out_cap,
150+
);
151+
if (rc < 0) {
152+
setLastError("Rejected (fail-closed): no genuine certified " ++
153+
"level — Tier-2 attestation NOT minted. The verification " ++
154+
"authority is the conformance-pinned certified_level; see " ++
155+
"verification/proofs/VERIFICATION-STANCE.adoc");
156+
return -1;
157+
}
158+
// 0..10 fits c_int; rc is bounded by the Rust backend.
159+
return @intCast(rc);
160+
}
161+
94162
pub export fn vclut_last_error() callconv(.c) [*:0]const u8 {
95163
if (last_error_len == 0) return "";
96164
return @ptrCast(&last_error_buf[0]);
@@ -123,3 +191,21 @@ test "verify is fail-closed: no fabricated level without a backend" {
123191
// and it never returns a "verified" (>=1) level here
124192
try std.testing.expect(rc < 1);
125193
}
194+
195+
// P5d integration: the REAL Rust Tier-2 backend is linked
196+
// (libvcltotal_attest.a via build.zig). Garbage wire bytes must
197+
// decode-fail in the conformance-pinned decoder ⇒ no attestation ⇒
198+
// -1, end-to-end across the Zig↔Rust boundary. (A positive path needs
199+
// a valid wire (Statement,OctadSchema), exhaustively covered by the
200+
// Rust crate's own roundtrip/tamper suite; this asserts the
201+
// fail-closed contract through the actual linked symbol.)
202+
test "vclut_verify_wire fail-closed on garbage via the linked Rust backend" {
203+
_ = vclut_init();
204+
var out: [65]u8 = [_]u8{0xAA} ** 65;
205+
const sk = [_]u8{7} ** 32;
206+
const bad = [_]u8{0xFF} ** 8;
207+
const rc = vclut_verify_wire(&bad, bad.len, &bad, bad.len, &sk, &out, out.len);
208+
try std.testing.expectEqual(@as(c_int, -1), rc);
209+
// out untouched on the fail-closed path
210+
for (out) |byte| try std.testing.expectEqual(@as(u8, 0xAA), byte);
211+
}

src/interface/attest/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/target
Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
= VCL-total Tier-2 Attestation Format v1 (P5d, vcl-ut#25)
2+
:toc:
3+
4+
// SPDX-License-Identifier: PMPL-1.0-or-later
5+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
6+
7+
Normative format for the **Tier-2 (C-ABI trusted-certifier
8+
attestation) FALLBACK**. See `verification/proofs/VERIFICATION-STANCE.adoc`
9+
(authoritative) for the two-tier boundary model and ADR
10+
`docs/decisions/0002-ffi-attestation-trust-boundary.adoc` for the
11+
rationale. Tier-1 (recompute-PCC over `wasm32`) is the achieved tier;
12+
this is the explicit *weaker* fallback for consumers that cannot run
13+
the Tier-1 module.
14+
15+
== Trust model (stated, not hidden)
16+
17+
A C ABI erases types, so it cannot carry a re-checkable dependent
18+
proof. The honest ceiling is *trusted-certifier attestation*: the
19+
consumer **trusts** that (a) the Ed25519 private key is held only by a
20+
genuine certifier and (b) that certifier ran the conformance-pinned
21+
`vcltotal_parse::certified_level` (the same faithful image of the Idris
22+
corpus decision Tier-1 uses) before signing. The token is *unforgeable*
23+
and *bound*: it cannot be fabricated, transplanted onto a different
24+
query/schema, or have its level escalated. This is strictly weaker than
25+
Tier-1 (which trusts neither (a) nor (b) — it recomputes). It is **not**
26+
a re-checkable proof and does not claim to be.
27+
28+
== Signed message (81 bytes, fixed)
29+
30+
[cols="1,3"]
31+
|===
32+
| `DOMAIN` | 16 bytes — `"VCLT-ATTEST-v1\0\0"` (protocol/version domain separation; a signature here can never be replayed as any other protocol)
33+
| `sha256(stmt_wire)` | 32 bytes — SHA-256 of the v1 `Statement` wire bytes (`VCLW…`, see `WIRE-FORMAT.adoc`)
34+
| `sha256(schema_wire)` | 32 bytes — SHA-256 of the v1 `OctadSchema` wire bytes (`VCLS…`)
35+
| `level` | 1 byte — the certified level `0..=10`
36+
|===
37+
38+
`token = Ed25519_sign(certifier_sk, DOMAIN ‖ sha256(stmt_wire) ‖
39+
sha256(schema_wire) ‖ level)` — a detached 64-byte signature.
40+
41+
`schema_id` is `sha256(schema_wire)` (content-addressed; no external
42+
registry/trust). "query" in the issue-#25 phrasing
43+
`(sha256(query), schema_id, level)` is the marshalled `Statement`
44+
(`sha256(stmt_wire)`).
45+
46+
== Wire token layout (C-ABI `out`)
47+
48+
65 bytes: `[ level : u8 ][ sig : 64 bytes ]`.
49+
50+
== Mint / verify
51+
52+
* *Mint* (certifier side): decode `(stmt_wire, schema_wire)`; run
53+
`certified_level`; **iff** `0 <= level <= 10`, sign and emit the
54+
token. Any decode failure or Reject ⇒ **no token** (fail-closed —
55+
never a token for an unestablished level).
56+
* *Verify* (consumer side): recompute the 81-byte message from the
57+
wire bytes the consumer holds + the attested `level`; Ed25519-verify
58+
against the certifier's public key. Accept the level iff verification
59+
succeeds. Verification does **not** re-run the decider — that is
60+
Tier-1's role; Tier-2 trusts the certifier by construction of a C
61+
ABI.
62+
63+
A tampered `stmt_wire`, `schema_wire`, `level`, or `sig`, or a wrong
64+
public key, all fail verification (machine-tested:
65+
`src/interface/attest` — roundtrip + 5 tamper variants + fail-closed +
66+
C-ABI).
67+
68+
== C-ABI
69+
70+
`vclut_rs_verify(stmt_ptr, stmt_len, schema_ptr, schema_len, sk_ptr,
71+
out_ptr, out_cap) -> i64` (Rust, `src/interface/attest`), linked into
72+
the Zig shim `ffi/zig/src/lib.zig` and exposed as
73+
`vclut_verify_wire(...)`. Returns the level `0..10` (and writes the
74+
65-byte token) or `-1` Rejected (writes nothing; `vclut_last_error`
75+
set). `sk_ptr` is the certifier's 32-byte Ed25519 seed — **real key
76+
provisioning is deployment**, via the estate token vault
77+
(`hyperpolymath/reasonably-good-token-vault`); the test key
78+
(`[7u8;32]`) is NOT a real certifier key.
79+
80+
== Crypto
81+
82+
Ed25519 via `ed25519-dalek` (de-facto standard, widely audited;
83+
maintainer decision 2026-05-19), SHA-256 via `sha2`. Both are
84+
*contained* in the separate `vcltotal-attest` crate (Tier-2 only) and
85+
never touch the zero-dependency, `#![forbid(unsafe_code)]`
86+
`vcltotal-parse` core. The only `unsafe` is one audited host/guest
87+
C-ABI memory block.
88+
89+
== Versioning
90+
91+
Any change to the wire formats, message layout, or crypto bumps
92+
`DOMAIN` (`VCLT-ATTEST-vN`) so old signatures cannot be
93+
reinterpreted. Tracked: hyperpolymath/vcl-ut#25.

0 commit comments

Comments
 (0)