|
| 1 | += Architecture Decision Record: 0008-verifier-spec-of-record |
| 2 | +<!-- SPDX-License-Identifier: CC-BY-SA-4.0 --> |
| 3 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> |
| 4 | + |
| 5 | +# 8. `typed-wasm-verify` + the Idris2 `VerifierSpec` are the spec of record |
| 6 | + |
| 7 | +Date: 2026-07-07 |
| 8 | + |
| 9 | +## Status |
| 10 | + |
| 11 | +Accepted |
| 12 | + |
| 13 | +Owner direction (2026-07-07 session, independence construction path, |
| 14 | +item 4): flip the wire-level verifier's spec-of-record from |
| 15 | +AffineScript's OCaml files to this repository. Companion to |
| 16 | +link:0006-rust-frontend-canonical.adoc[ADR-0006] (which made the |
| 17 | +in-tree Rust parser the canonical front-end); this ADR removes the last |
| 18 | +structural dependency on a sibling repository. |
| 19 | + |
| 20 | +## Context |
| 21 | + |
| 22 | +`crates/typed-wasm-verify` began as a Rust port of |
| 23 | +`hyperpolymath/affinescript`'s `lib/tw_verify.ml` (intra-function |
| 24 | +L7/L10) and `lib/tw_interface.ml` (cross-module boundary). The port's |
| 25 | +own README pinned the handover criterion: |
| 26 | +
|
| 27 | +> The OCaml files remain the spec of record until behavioural parity is |
| 28 | +> established by the cross-compat test suite (workspace task C5). |
| 29 | +
|
| 30 | +That criterion is met, and exceeded: |
| 31 | +
|
| 32 | +* **C5 synthetic parity** — `tests/cross_compat.rs` (10 tests): a |
| 33 | + hand-built fixture table exercising both verifiers' semantics |
| 34 | + (accept + reject cases, intra- and cross-module), green. |
| 35 | +* **C5.1 real-producer parity** — `tests/cross_compat_real.rs` |
| 36 | + (5 tests) against real AffineScript-emitted bytes |
| 37 | + (`tests/fixtures/c5_real/`, capture pinned to affinescript |
| 38 | + `21edc159`), green. |
| 39 | +* Since the criterion was written, the Rust crate has grown **past** |
| 40 | + the OCaml reference: L13 negative-form isolation (PR #37), carrier |
| 41 | + passes for L2/L15 (`unstable-l2`/`unstable-l15`), L13 positive-form |
| 42 | + region imports + link-graph certification |
| 43 | + (link:0007-region-imports-carrier.adoc[ADR-0007]), access-typing, |
| 44 | + and third-producer conformance (`tests/third_producer_zig.rs`). The |
| 45 | + OCaml files cannot serve as spec of record for behaviour they do not |
| 46 | + implement. |
| 47 | +* The formal side already lives here: |
| 48 | + `src/abi/TypedWasm/ABI/VerifierSpec.idr` (total, no escape hatches) |
| 49 | + states what the verifier must decide; `MultiModule.idr` grounds the |
| 50 | + cross-module certificates. |
| 51 | + |
| 52 | +## Decision |
| 53 | + |
| 54 | +1. **Spec of record for wire-level verification is this repository**: |
| 55 | + the Idris2 `VerifierSpec.idr` (and `MultiModule.idr` for the |
| 56 | + cross-module layer) as the formal statement, and |
| 57 | + `crates/typed-wasm-verify` as the executable reference. |
| 58 | +2. **AffineScript's `lib/tw_verify.ml` / `lib/tw_interface.ml` are |
| 59 | + demoted to a conforming implementation** (and historical origin). |
| 60 | + On any behavioural divergence, the OCaml side is presumed wrong |
| 61 | + unless the Idris2 spec says otherwise; fixes flow AffineScript-ward. |
| 62 | +3. **The parity suites remain as regression armour**, not as a |
| 63 | + pending criterion: `cross_compat.rs` / `cross_compat_real.rs` keep |
| 64 | + pinning the shared semantics so the demoted implementation cannot |
| 65 | + silently drift while it remains in use. |
| 66 | +4. AffineScript's eventual adoption of `typed-wasm-verify` as its |
| 67 | + verifier (its Track B, queued for its v1.0) retires the OCaml files |
| 68 | + entirely; that is AffineScript's call to schedule. |
| 69 | +
|
| 70 | +## Consequences |
| 71 | + |
| 72 | +### Positive |
| 73 | + |
| 74 | +- typed-wasm's verification semantics are defined, proven, implemented, |
| 75 | + and tested in one repository — the compile-target independence |
| 76 | + property, completed on the verifier axis. |
| 77 | +- New carriers (ADR-0007 and the coming L8/L9 proposals) have exactly |
| 78 | + one place to specify behaviour; no cross-repo spec drift is possible. |
| 79 | +
|
| 80 | +### Negative |
| 81 | + |
| 82 | +- The OCaml implementation persists in AffineScript until its Track B |
| 83 | + lands; until then two implementations exist and the parity suites are |
| 84 | + load-bearing (they already run in CI here). |
| 85 | +
|
| 86 | +### Neutral |
| 87 | + |
| 88 | +- No wire-format change; no producer is affected. |
| 89 | +
|
| 90 | +## Cross-references |
| 91 | + |
| 92 | +* link:0006-rust-frontend-canonical.adoc[ADR-0006] — front-end |
| 93 | + canonicalisation (the sibling decision on the parser axis) |
| 94 | +* link:0007-region-imports-carrier.adoc[ADR-0007] — first carrier |
| 95 | + specified wholly under the new regime |
| 96 | +* `src/abi/TypedWasm/ABI/VerifierSpec.idr`, `MultiModule.idr` — the |
| 97 | + formal spec layer |
| 98 | +* `crates/typed-wasm-verify/tests/cross_compat.rs`, |
| 99 | + `tests/cross_compat_real.rs` — the met parity criterion |
| 100 | +* `crates/typed-wasm-verify/tests/third_producer_zig.rs` — producer |
| 101 | + neutrality under the new regime |
0 commit comments