Skip to content

Commit 6573406

Browse files
committed
feat(tw_verify): v2-parse support for affinescript.ownership (ADR-020)
Lands the verifier-side (parse) half of ADR-020 (ownership-section schema versioning), per ADR-021's coordinated landing protocol — verifier ships parse-support FIRST, then producers flip emit together. This PR is the AffineScript leg. On-wire change (parse-only this PR; emit stays on v1): v1 (legacy, unversioned, what we emit today): u32le count entry* v2 (ADR-020, parse-only here): u8 0xAF (* sentinel — "AffineScript Format" *) u8 version (* 0x02 *) u32le count entry* (* same entry shape as v1 *) Dispatch: a v2 section starts with the 0xAF sentinel byte. v1 readers fail cleanly on v2 sections (the sentinel pollutes the entry-count low byte and yields an implausible count); v2 readers see the sentinel and branch. Unknown v2.X versions yield [] (sound fallback per ADR-021's conservative-disposition axis: loud-correct rather than silent-wrong). What this PR does: * lib/tw_verify.ml `parse_ownership_section_payload` — now dispatches v1 vs v2 on the leading sentinel byte; v1 path preserved verbatim, v2 path adds two leading bytes + identical entry decoding. * test/test_e2e.ml — two new hermetic alcotest cases under "E2E TypedWasm ownership schema": * v2 parse round-trip on a hand-constructed payload * v2.99 (unknown future version) -> [] (sound fallback). What this PR does NOT do (deliberately): * Does NOT flip the producer-side emitter — that stays on v1 until hyperpolymath/typed-wasm's Rust verifier and hyperpolymath/ephapax's verifier also ship parse-support. Coordinated landing per ADR-021 axis 2. * Does NOT re-add ADR-020 / ADR-021 to META.a2ml or the docs/specs/TYPED-WASM-COORDINATION-LEDGER files. Both ADRs are owner-ratified (2026-05-24); the file artefacts were lost in PR #344's squash-merge. This PR cites them inline (verifier comment + commit message) and a separate doc-only follow-up should restore them to META.a2ml. Not yet locally verified — no OCaml toolchain in remote execution env. CI is the verification surface. The v1 path is byte-for-byte unchanged from the pre-PR shape; the v2 path is new code reachable only on a sentinel byte AffineScript does not currently emit. So the existing v1 round-trip tests (test_ownership_*) MUST still pass; the two new v2 tests are pure addition. Refs ADR-020 (parse-side), ADR-021 (coordinated landing).
1 parent a00f285 commit 6573406

2 files changed

Lines changed: 148 additions & 31 deletions

File tree

lib/tw_verify.ml

Lines changed: 97 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -187,13 +187,34 @@ let verify_module
187187
(** Parse the [affinescript.ownership] custom section payload into structured
188188
[(func_idx, param_kinds, ret_kind)] annotations.
189189
190-
Binary encoding (from [Codegen.build_ownership_section]):
190+
Supports BOTH v1 (legacy, unversioned) and v2 (ADR-020, accepted
191+
+ ratified 2026-05-24) on-wire formats; v2 is identified by the
192+
[0xAF] sentinel byte followed by a version byte. v1 readers
193+
fail cleanly on v2 sections (the sentinel pollutes the
194+
entry-count low byte and yields an implausible count); v2
195+
readers see the sentinel and dispatch.
196+
197+
v1 layout (legacy, unversioned):
191198
u32le count
192199
for each entry:
193200
u32le func_idx
194201
u8 n_params
195202
u8[n] param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow)
196-
u8 ret_kind *)
203+
u8 ret_kind
204+
205+
v2 layout (ADR-020):
206+
u8 0xAF (* "AffineScript Format" sentinel *)
207+
u8 version (* 0x02 for v2.0 *)
208+
u32le count
209+
entry* (* same entry shape as v1 *)
210+
211+
Per ADR-021's coordinated landing protocol, this verifier ships
212+
parse-support FIRST. AffineScript's emitter ([Codegen.build_ownership_
213+
section] / [Tw_ownership_section.build_section]) stays on v1 until
214+
[hyperpolymath/typed-wasm]'s Rust verifier + [hyperpolymath/ephapax]'s
215+
OCaml verifier also ship parse-support; then all producers flip to v2
216+
emit together. See [docs/specs/TYPED-WASM-COORDINATION-LEDGER.adoc]
217+
Q-001 for the current state of the cross-repo rollout. *)
197218
let parse_ownership_section_payload
198219
(payload : bytes)
199220
: (int * ownership_kind list * ownership_kind) list =
@@ -205,33 +226,81 @@ let parse_ownership_section_payload
205226
in
206227
let pos = ref 0 in
207228
let len = Bytes.length payload in
208-
let read_u32_le () =
209-
if !pos + 4 > len then 0
210-
else begin
211-
let b0 = Char.code (Bytes.get payload !pos) in
212-
let b1 = Char.code (Bytes.get payload (!pos + 1)) in
213-
let b2 = Char.code (Bytes.get payload (!pos + 2)) in
214-
let b3 = Char.code (Bytes.get payload (!pos + 3)) in
215-
pos := !pos + 4;
216-
b0 lor (b1 lsl 8) lor (b2 lsl 16) lor (b3 lsl 24)
217-
end
229+
(* v2 sentinel dispatch. Two bytes minimum: [0xAF, version]. The
230+
sentinel is byte-distinct from any v1 entry-count low byte for
231+
a module with <= 0xAE entries (i.e. effectively every module);
232+
ADR-020 catalogues this trade-off explicitly. *)
233+
let v2_detected =
234+
len >= 2
235+
&& Char.code (Bytes.get payload 0) = 0xAF
218236
in
219-
let read_u8 () =
220-
if !pos >= len then 0
221-
else begin
222-
let b = Char.code (Bytes.get payload !pos) in
223-
pos := !pos + 1;
224-
b
225-
end
226-
in
227-
let count = read_u32_le () in
228-
List.init count (fun _ ->
229-
let func_idx = read_u32_le () in
230-
let n_params = read_u8 () in
231-
let param_kinds = List.init n_params (fun _ -> kind_of_byte (read_u8 ())) in
232-
let ret_kind = kind_of_byte (read_u8 ()) in
233-
(func_idx, param_kinds, ret_kind)
234-
)
237+
if v2_detected then begin
238+
let v2_version = Char.code (Bytes.get payload 1) in
239+
pos := 2;
240+
(* v2.0 is the only known version today. An unknown v2.X is a
241+
future-version section we cannot interpret; per ADR-021
242+
conservative-disposition (sound fallback), treat as empty.
243+
The verifier therefore enforces nothing on the section —
244+
loud-correct rather than silent-wrong. *)
245+
if v2_version <> 0x02 then []
246+
else
247+
let read_u32_le () =
248+
if !pos + 4 > len then 0
249+
else begin
250+
let b0 = Char.code (Bytes.get payload !pos) in
251+
let b1 = Char.code (Bytes.get payload (!pos + 1)) in
252+
let b2 = Char.code (Bytes.get payload (!pos + 2)) in
253+
let b3 = Char.code (Bytes.get payload (!pos + 3)) in
254+
pos := !pos + 4;
255+
b0 lor (b1 lsl 8) lor (b2 lsl 16) lor (b3 lsl 24)
256+
end
257+
in
258+
let read_u8 () =
259+
if !pos >= len then 0
260+
else begin
261+
let b = Char.code (Bytes.get payload !pos) in
262+
pos := !pos + 1;
263+
b
264+
end
265+
in
266+
let count = read_u32_le () in
267+
List.init count (fun _ ->
268+
let func_idx = read_u32_le () in
269+
let n_params = read_u8 () in
270+
let param_kinds = List.init n_params (fun _ -> kind_of_byte (read_u8 ())) in
271+
let ret_kind = kind_of_byte (read_u8 ()) in
272+
(func_idx, param_kinds, ret_kind))
273+
end else begin
274+
(* v1 (legacy) path. Identical to the pre-ADR-020 behaviour;
275+
preserved verbatim for backward compatibility with already-
276+
emitted modules and with the in-tree fixtures. *)
277+
let read_u32_le () =
278+
if !pos + 4 > len then 0
279+
else begin
280+
let b0 = Char.code (Bytes.get payload !pos) in
281+
let b1 = Char.code (Bytes.get payload (!pos + 1)) in
282+
let b2 = Char.code (Bytes.get payload (!pos + 2)) in
283+
let b3 = Char.code (Bytes.get payload (!pos + 3)) in
284+
pos := !pos + 4;
285+
b0 lor (b1 lsl 8) lor (b2 lsl 16) lor (b3 lsl 24)
286+
end
287+
in
288+
let read_u8 () =
289+
if !pos >= len then 0
290+
else begin
291+
let b = Char.code (Bytes.get payload !pos) in
292+
pos := !pos + 1;
293+
b
294+
end
295+
in
296+
let count = read_u32_le () in
297+
List.init count (fun _ ->
298+
let func_idx = read_u32_le () in
299+
let n_params = read_u8 () in
300+
let param_kinds = List.init n_params (fun _ -> kind_of_byte (read_u8 ())) in
301+
let ret_kind = kind_of_byte (read_u8 ()) in
302+
(func_idx, param_kinds, ret_kind))
303+
end
235304

236305
(** Level 13 — module isolation (negative form). A well-isolated
237306
module owns its private linear memory and reaches other modules

test/test_e2e.ml

Lines changed: 51 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1214,10 +1214,58 @@ let test_ownership_entry_count () =
12141214
Alcotest.(check bool) "at least 4 entries (one per function)" true
12151215
(List.length entries >= 4)
12161216

1217+
(* ADR-020 (accepted + ratified 2026-05-24): hermetic round-trip on a
1218+
hand-constructed v2 payload — 0xAF sentinel + u8 version 0x02 +
1219+
the same entry shape as v1. Verifier-parse-support is the FIRST
1220+
leg of the coordinated landing per ADR-021 axis 2; this test
1221+
pins the v2 parse contract against the gate. Future v2.X versions
1222+
that this v2.0 reader does not understand MUST yield an empty
1223+
annotation list (sound fallback). *)
1224+
let test_ownership_v2_parse_roundtrip () =
1225+
let buf = Buffer.create 32 in
1226+
let add_u8 n = Buffer.add_char buf (Char.chr (n land 0xff)) in
1227+
let add_u32_le n =
1228+
add_u8 (n land 0xff);
1229+
add_u8 ((n lsr 8) land 0xff);
1230+
add_u8 ((n lsr 16) land 0xff);
1231+
add_u8 ((n lsr 24) land 0xff)
1232+
in
1233+
(* v2 header *)
1234+
add_u8 0xAF;
1235+
add_u8 0x02;
1236+
(* one entry: func 7, params [Linear; SharedBorrow], ret Unrestricted *)
1237+
add_u32_le 1;
1238+
add_u32_le 7;
1239+
add_u8 2;
1240+
add_u8 1; (* Linear *)
1241+
add_u8 2; (* SharedBorrow *)
1242+
add_u8 0; (* Unrestricted ret *)
1243+
let payload = Buffer.to_bytes buf in
1244+
let entries = Tw_verify.parse_ownership_section_payload payload in
1245+
match entries with
1246+
| [(7, [Codegen.Linear; Codegen.SharedBorrow], Codegen.Unrestricted)] -> ()
1247+
| other ->
1248+
Alcotest.failf
1249+
"v2 parse mismatch: got %d entries (expected exactly the one canonical entry)"
1250+
(List.length other)
1251+
1252+
let test_ownership_v2_unknown_version_empty () =
1253+
(* A v2.99 section (unknown future version) must yield [] — sound
1254+
fallback per ADR-021 conservative-disposition. *)
1255+
let buf = Buffer.create 4 in
1256+
Buffer.add_char buf (Char.chr 0xAF);
1257+
Buffer.add_char buf (Char.chr 0x99);
1258+
Buffer.add_char buf (Char.chr 0x00);
1259+
Buffer.add_char buf (Char.chr 0x00);
1260+
let entries = Tw_verify.parse_ownership_section_payload (Buffer.to_bytes buf) in
1261+
Alcotest.(check int) "unknown v2.X yields []" 0 (List.length entries)
1262+
12171263
let ownership_schema_tests = [
1218-
Alcotest.test_case "section present" `Quick test_ownership_section_present;
1219-
Alcotest.test_case "round-trip kinds" `Quick test_ownership_roundtrip;
1220-
Alcotest.test_case "entry count" `Quick test_ownership_entry_count;
1264+
Alcotest.test_case "section present" `Quick test_ownership_section_present;
1265+
Alcotest.test_case "round-trip kinds" `Quick test_ownership_roundtrip;
1266+
Alcotest.test_case "entry count" `Quick test_ownership_entry_count;
1267+
Alcotest.test_case "v2 parse round-trip (ADR-020)" `Quick test_ownership_v2_parse_roundtrip;
1268+
Alcotest.test_case "v2 unknown version -> [] (ADR-021)" `Quick test_ownership_v2_unknown_version_empty;
12211269
]
12221270

12231271
(* ============================================================================

0 commit comments

Comments
 (0)