From 2adf260c2847c71aa2c281182d134941d53c5f86 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 14:09:25 +0100 Subject: [PATCH] refactor(tw): extract Tw_section.Encode.ownership; delete orphan tw_ownership_section.ml MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Establishes lib/tw_section.{ml,mli} as the canonical home for typed-wasm custom-section wire encoders, sized to absorb proposal 0001's two new sections (typedwasm.regions, typedwasm.capabilities) when they land. Changes: - lib/tw_section.ml{,i} created. Encode.ownership operates on pre-byte-encoded triples ((int * int list * int) list) — avoids a Codegen→Tw_section→Codegen type cycle while keeping the byte layout intact. - lib/codegen.ml:159-177 — build_ownership_section body replaced with a 6-line wrapper that maps ownership_kind→byte and delegates to Tw_section.Encode.ownership. Same signature, byte-equal output. - lib/dune — tw_section module added. - lib/tw_ownership_section.ml DELETED. Was orphan: not in lib/dune modules list, no callers, only string-mentioned in tw_verify.ml's stale doc comment (which is also fixed here). - lib/tw_verify.ml:213 — stale doc comment updated: Tw_ownership_section.build_section → Tw_section.Encode.ownership. Rationale: hyperpolymath/affinescript#444 — prevent the 3-sections × 2-copies = 6-encoder fan-out when proposal 0001 (hyperpolymath/typed-wasm#34, hyperpolymath/typed-wasm#76) lands. Sharing the internal LE writers (write_u32_le / write_u8) inside Tw_section.Encode means future Encode.regions / Encode.capabilities land in one place rather than duplicating the buffer plumbing. ADR-021 v2-emit flip is OUT OF SCOPE. Tw_section.Encode.ownership ships v1. When the cross-repo coordination unblocks, the flip is a localised change to this one module. Tea_* hand-rolled fixture encoders (lib/tea_bridge.ml, lib/tea_cs_bridge.ml, lib/tea_router.ml) are intentionally NOT migrated in this PR — they hard-code demo bytes for tea demonstrations, which is a separate concern from the live producer-side dedup. Verification: dune build clean; dune runtest 352/352 passing (round-trip tests would catch any byte divergence). Refs hyperpolymath/affinescript#444 Refs hyperpolymath/typed-wasm#34 Refs hyperpolymath/typed-wasm#76 --- lib/codegen.ml | 24 +++------- lib/dune | 1 + lib/tw_ownership_section.ml | 96 ------------------------------------- lib/tw_section.ml | 25 ++++++++++ lib/tw_section.mli | 36 ++++++++++++++ lib/tw_verify.ml | 2 +- 6 files changed, 69 insertions(+), 115 deletions(-) delete mode 100644 lib/tw_ownership_section.ml create mode 100644 lib/tw_section.ml create mode 100644 lib/tw_section.mli diff --git a/lib/codegen.ml b/lib/codegen.ml index 57910041..22a7aa06 100644 --- a/lib/codegen.ml +++ b/lib/codegen.ml @@ -157,24 +157,12 @@ let ownership_kind_byte = function u8* param_kind (one per param, see kind encoding above) u8 return_kind *) let build_ownership_section (annots : (int * ownership_kind list * ownership_kind) list) : bytes = - if annots = [] then Bytes.empty - else - let buf = Buffer.create 64 in - let write_u32_le n = - Buffer.add_char buf (Char.chr (n land 0xff)); - Buffer.add_char buf (Char.chr ((n lsr 8) land 0xff)); - Buffer.add_char buf (Char.chr ((n lsr 16) land 0xff)); - Buffer.add_char buf (Char.chr ((n lsr 24) land 0xff)) - in - let write_u8 n = Buffer.add_char buf (Char.chr (n land 0xff)) in - write_u32_le (List.length annots); - List.iter (fun (func_idx, param_kinds, ret_kind) -> - write_u32_le func_idx; - write_u8 (List.length param_kinds); - List.iter (fun k -> write_u8 (ownership_kind_byte k)) param_kinds; - write_u8 (ownership_kind_byte ret_kind) - ) annots; - Buffer.to_bytes buf + Tw_section.Encode.ownership + (List.map (fun (func_idx, param_kinds, ret_kind) -> + (func_idx, + List.map ownership_kind_byte param_kinds, + ownership_kind_byte ret_kind)) + annots) (** Map AffineScript type to WASM value type *) let type_to_wasm (ty : type_expr) : value_type result = diff --git a/lib/dune b/lib/dune index e3e49431..218a7e90 100644 --- a/lib/dune +++ b/lib/dune @@ -82,6 +82,7 @@ token trait tw_interface + tw_section tw_verify typecheck types diff --git a/lib/tw_ownership_section.ml b/lib/tw_ownership_section.ml deleted file mode 100644 index 43ca496e..00000000 --- a/lib/tw_ownership_section.ml +++ /dev/null @@ -1,96 +0,0 @@ -(* SPDX-License-Identifier: MPL-2.0 *) -(* SPDX-FileCopyrightText: 2026 hyperpolymath *) -(* - * tw_ownership_section.ml — the dedicated home for the - * `typedwasm.ownership` Wasm custom section: kind encoding, - * extraction from the AST, and binary serialisation. - * - * Extracted from lib/codegen.ml at 2026-05-24 per Tranche A3 of - * docs/specs/TYPED-WASM-ROADMAP.adoc. Behaviour-preserving move. - * - * The format itself is specified in - * docs/specs/TYPED-WASM-INTERFACE.adoc (v1, current) and - * docs/specs/TYPED-WASM-ROADMAP.adoc §"Tranche B" (v2, the - * ratified ADR-020 widening; landed via [Tw_verify] parse-support - * first, with the producer-emit flip deferred to the coordinated - * landing window per ADR-021 — see TYPED-WASM-COORDINATION-LEDGER.adoc - * Q-001). - * - * Backwards compatibility: [Codegen] re-exports the same names so - * `open Codegen` continues to expose [ownership_kind] and friends — - * downstream callers ([Tw_verify], [Tw_interface], [Test_e2e]) need - * no change. - *) - -open Ast - -(** Ownership kind for typed-wasm schema annotations. - Maps AffineScript ownership qualifiers to typed-wasm Level 7/10 - verification. *) -type ownership_kind = - | Unrestricted (** Plain value, no ownership constraint (Wasm i32/f64 etc.) *) - | Linear (** TyOwn / own — consumed exactly once (typed-wasm Level 10) *) - | SharedBorrow (** TyRef / ref — read-only aliasing safety (typed-wasm Level 7) *) - | ExclBorrow (** TyMut / mut — exclusive mutable aliasing safety (typed-wasm Level 7) *) - -(** Extract ownership kind from a parameter declaration. - Checks [p.p_ownership] first; falls back to the shape of [p.p_ty]. *) -let ownership_kind_of_param (p : param) : ownership_kind = - match p.p_ownership with - | Some Own -> Linear - | Some Ref -> SharedBorrow - | Some Mut -> ExclBorrow - | None -> - match p.p_ty with - | TyOwn _ -> Linear - | TyRef _ -> SharedBorrow - | TyMut _ -> ExclBorrow - | _ -> Unrestricted - -(** Extract ownership kind from an optional return type expression *) -let ownership_kind_of_ret (ret : type_expr option) : ownership_kind = - match ret with - | Some (TyOwn _) -> Linear - | Some (TyRef _) -> SharedBorrow - | Some (TyMut _) -> ExclBorrow - | _ -> Unrestricted - -(** Encode an [ownership_kind] as a single byte (0..3). *) -let ownership_kind_byte = function - | Unrestricted -> 0 - | Linear -> 1 - | SharedBorrow -> 2 - | ExclBorrow -> 3 - -(** Build the payload for the [typedwasm.ownership] Wasm custom section. - - v1 encoding (current emit; LE): - u32 entry_count - per entry: - u32 func_index - u8 param_count - u8* param_kind (one per param, see kind encoding above) - u8 return_kind - - Returns [Bytes.empty] when there are no annotations so the - caller can omit the section entirely. *) -let build_section - (annots : (int * ownership_kind list * ownership_kind) list) : bytes = - if annots = [] then Bytes.empty - else - let buf = Buffer.create 64 in - let write_u32_le n = - Buffer.add_char buf (Char.chr (n land 0xff)); - Buffer.add_char buf (Char.chr ((n lsr 8) land 0xff)); - Buffer.add_char buf (Char.chr ((n lsr 16) land 0xff)); - Buffer.add_char buf (Char.chr ((n lsr 24) land 0xff)) - in - let write_u8 n = Buffer.add_char buf (Char.chr (n land 0xff)) in - write_u32_le (List.length annots); - List.iter (fun (func_idx, param_kinds, ret_kind) -> - write_u32_le func_idx; - write_u8 (List.length param_kinds); - List.iter (fun k -> write_u8 (ownership_kind_byte k)) param_kinds; - write_u8 (ownership_kind_byte ret_kind) - ) annots; - Buffer.to_bytes buf diff --git a/lib/tw_section.ml b/lib/tw_section.ml new file mode 100644 index 00000000..49df9e0f --- /dev/null +++ b/lib/tw_section.ml @@ -0,0 +1,25 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 hyperpolymath *) + +module Encode = struct + let write_u32_le buf n = + Buffer.add_char buf (Char.chr (n land 0xff)); + Buffer.add_char buf (Char.chr ((n lsr 8) land 0xff)); + Buffer.add_char buf (Char.chr ((n lsr 16) land 0xff)); + Buffer.add_char buf (Char.chr ((n lsr 24) land 0xff)) + + let write_u8 buf n = Buffer.add_char buf (Char.chr (n land 0xff)) + + let ownership (annots : (int * int list * int) list) : bytes = + if annots = [] then Bytes.empty + else + let buf = Buffer.create 64 in + write_u32_le buf (List.length annots); + List.iter (fun (func_idx, param_kind_bytes, ret_kind_byte) -> + write_u32_le buf func_idx; + write_u8 buf (List.length param_kind_bytes); + List.iter (fun b -> write_u8 buf b) param_kind_bytes; + write_u8 buf ret_kind_byte + ) annots; + Buffer.to_bytes buf +end diff --git a/lib/tw_section.mli b/lib/tw_section.mli new file mode 100644 index 00000000..c3dd75b4 --- /dev/null +++ b/lib/tw_section.mli @@ -0,0 +1,36 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 hyperpolymath *) + +(** Canonical home for typed-wasm custom-section encoders. + + Wire encoders operate on pre-byte-encoded triples to keep this + module free of any dependency on producer-side ownership types + (avoiding a cycle with [Codegen]). Callers map their domain + types to bytes before invoking. + + Forward-compatibility slot for typed-wasm proposal 0001 (issue + hyperpolymath/typed-wasm#34): [Encode.regions] and + [Encode.capabilities] land here when the proposal promotes to + [accepted]. Sharing the internal LE writers (u8 / u32le / leb128) + inside this module prevents the 3-sections × 2-copies = 6-encoder + fan-out flagged by hyperpolymath/affinescript#444. *) + +module Encode : sig + (** v1 wire format for [typedwasm.ownership]: + u32le entry_count + per entry: + u32le func_index + u8 param_count + u8* param_kind (one per param) + u8 return_kind + + Caller responsibilities: + - Map domain ownership type → byte before calling + (see [Codegen.ownership_kind_byte]). + - Empty input → [Bytes.empty]; caller omits the section. + + Producer-emit is v1 per ADR-021. Parser-side v2 support lives in + [Tw_verify.parse_ownership_section_payload]; emit-side flip is + cross-repo-coordinated, not local to this function. *) + val ownership : (int * int list * int) list -> bytes +end diff --git a/lib/tw_verify.ml b/lib/tw_verify.ml index 70530aed..9dece61c 100644 --- a/lib/tw_verify.ml +++ b/lib/tw_verify.ml @@ -210,7 +210,7 @@ let verify_module Per ADR-021's coordinated landing protocol, this verifier ships parse-support FIRST. AffineScript's emitter ([Codegen.build_ownership_ - section] / [Tw_ownership_section.build_section]) stays on v1 until + section] / [Tw_section.Encode.ownership]) stays on v1 until [hyperpolymath/typed-wasm]'s Rust verifier + [hyperpolymath/ephapax]'s OCaml verifier also ship parse-support; then all producers flip to v2 emit together. See [docs/specs/TYPED-WASM-COORDINATION-LEDGER.adoc]