|
| 1 | += Architecture Decision Record: 0002-ffi-attestation-trust-boundary |
| 2 | +<!-- SPDX-License-Identifier: PMPL-1.0-or-later --> |
| 3 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> --> |
| 4 | + |
| 5 | +# 2. FFI trust boundary: recompute-PCC over wasm32 (Tier-1), C-ABI attestation (Tier-2) |
| 6 | + |
| 7 | +Date: 2026-05-19 |
| 8 | + |
| 9 | +## Status |
| 10 | + |
| 11 | +Accepted (Tier-1 RESOLVED; Tier-2 / P5d OWED). Tracked: |
| 12 | +hyperpolymath/vcl-ut#25. Authoritative companion: |
| 13 | +`verification/proofs/VERIFICATION-STANCE.adoc` (canonical two-tier |
| 14 | +boundary model) — this ADR records *why*; the stance records *what is |
| 15 | +and is not proven*. |
| 16 | + |
| 17 | +## Context |
| 18 | + |
| 19 | +vcl-ut is the doubly-trusted hypatia↔verisim interface. The Idris2 |
| 20 | +corpus proves, machine-checked and CI-gated, that the 10-level VCL-total |
| 21 | +decision procedure is sound (`checkLevelNSound`, |
| 22 | +`Checker.certifyAt`/`certifyRequested` assembling a dependent |
| 23 | +`SafetyCertificate`). The open question was how a *consumer* obtains |
| 24 | +that guarantee across a process/language boundary. |
| 25 | + |
| 26 | +Constraints established during Phase 5: |
| 27 | + |
| 28 | +- A **C ABI erases types to machine words**: a dependent |
| 29 | + `SafetyCertificate` cannot cross it as a re-checkable object. Over a |
| 30 | + C ABI the honest ceiling is *trusted-certifier attestation* (trust |
| 31 | + the minting checker; the token is unforgeable, bound to |
| 32 | + `(sha256(query), schema_id, level)`). |
| 33 | +- A **proof-term-PCC** design (ship a core proof term + a small |
| 34 | + dependent kernel the consumer runs) was considered and **rejected**: |
| 35 | + Idris2 0.8.0 ships no embeddable verified core kernel, and building |
| 36 | + one is its own subproject of unbounded scope. |
| 37 | +- The estate's `affinescriptiser` (Rust→typed-wasm wrapper) **does not |
| 38 | + apply**: it structurally requires ≥1 `[[resources]]` and the |
| 39 | + verdict entry is a pure resource-free function (fabricating a |
| 40 | + resource to satisfy the tool would violate the verification-honesty |
| 41 | + doctrine), and its wasm backend is Phase-2-pending. (Disclosed: |
| 42 | + `src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc`.) |
| 43 | +
|
| 44 | +## Decision |
| 45 | + |
| 46 | +Adopt a **two-tier boundary**: |
| 47 | + |
| 48 | +**Tier-1 — recompute-PCC over plain `wasm32` (the achieved tier).** |
| 49 | +The consumer is shipped the `wasm32` module |
| 50 | +`src/interface/recompute-wasm` (`vcl_recompute`) + the wire bytes of a |
| 51 | +`(Statement, OctadSchema)` + the producer's claimed level, and |
| 52 | +**re-runs the certified decision itself**, comparing its verdict to |
| 53 | +the claim. This is proof-carrying code by *recomputation*, not by |
| 54 | +transporting a proof object. The consumer's TCB is: |
| 55 | + |
| 56 | +1. the once-proved corpus soundness (`checkLevelNSound`), |
| 57 | + machine-checked in the CI-gated Idris corpus and *offline* |
| 58 | + re-checkable with idris2 — never in the runtime path; |
| 59 | +2. the cross-language conformance pin that |
| 60 | + `vcltotal_parse::certified_level` is a faithful image of that |
| 61 | + corpus decision (`tests/conformance_emit.rs` ⇄ |
| 62 | + `VclTotal.Interface.WireConformance`, `Refl` on shared golden |
| 63 | + bytes); and |
| 64 | +3. the wasm runtime — *not* the whole certifier, *not* a level tag |
| 65 | + taken on faith. |
| 66 | +
|
| 67 | +Plain `wasm32-unknown-unknown` is **sufficient and not a compromise**: |
| 68 | +nothing structured crosses the boundary that needs type-preservation |
| 69 | +(opaque wire bytes in, an `i64` out; the decoder+decider run *inside* |
| 70 | +the module), so the wasm *type system* is not load-bearing. The wasm |
| 71 | +verdict equals the conformance-pinned native verdict by construction |
| 72 | +(deterministic build of pinned, pure, total source). The path is |
| 73 | +fail-closed: any malformed input or unmet level → Reject, never a |
| 74 | +fabricated level. The only `unsafe` is one audited host/guest |
| 75 | +memory-ABI block — the declared trust boundary — with all |
| 76 | +decode/decision logic in the `#![forbid(unsafe_code)]` crate. |
| 77 | + |
| 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. |
| 84 | + |
| 85 | +## Consequences |
| 86 | + |
| 87 | +- The headline "no re-checkable proof across an FFI" objection is |
| 88 | + **dissolved for Tier-1**: it was only ever true of an *untyped C |
| 89 | + ABI*, and Tier-1 sidesteps it by recomputation rather than proof |
| 90 | + transport. Recompute is, in one respect, *stronger* than proof-object |
| 91 | + PCC — the consumer need not trust a transported term's provenance; |
| 92 | + its cost is recomputation, negligible for a static AST decision. |
| 93 | +- The certifier (the Idris corpus) stays the single source of |
| 94 | + verification truth, machine-checked once; the runtime never carries |
| 95 | + a proof object. |
| 96 | +- Disclosed, precisely-scoped limits remain (NaN-payload |
| 97 | + reconstruction; cross-module `Refl` non-reduction of |
| 98 | + `find`/`elemBy`, so schema-resolution-dependent verdicts are pinned |
| 99 | + Rust-side + by input-value conformance; L9/L10 predicate depth; |
| 100 | + additive↔ceil `alignUp` sliver). These are stated in |
| 101 | + 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 |
| 104 | + level). |
| 105 | +- Revisit only if a future revision genuinely introduces a tracked |
| 106 | + resource at this boundary (none foreseen for a pure verdict |
| 107 | + function) or if a verified embeddable dependent kernel becomes |
| 108 | + available (which would enable, but is not required for, an |
| 109 | + additional proof-object tier). |
0 commit comments