feat(affinescript): Stage 8 — auto-verify ownership on compile + bridge generators

Wire Tw_verify.verify_from_module into the compilation pipeline:
- compile (WASM 1.0 path): post-codegen ownership check, violations printed
  to stderr as warnings; compilation still succeeds (defence-in-depth)
- tea-bridge: ownership verified before binary is written; prints OK/violations
- router-bridge: same

Both bridge modules pass clean: TEA bridge fn_update uses LocalGet 0 once;
router fn_push uses LocalGet 0 in the then-branch only (branch-max=1 → OK).

Add 2 E2E tests:
- E2E TEA Bridge[6]: ownership verify: clean
- E2E TEA Router[8]: ownership verify: clean

159/159 tests passing.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

bin/main.ml

@@ -343,6 +343,12 @@ let eval_file face json path =
     public/assets/wasm/ directory, and load via AffineTEA.load(). *)
 let tea_bridge_cmd_fn output =
   let m = Affinescript.Tea_bridge.generate () in
+  (* Stage 8: auto-verify ownership constraints before writing. *)
+  (match Affinescript.Tw_verify.verify_from_module m with
+  | Ok () ->
+    Format.printf "typed-wasm ownership verification: OK@."
+  | Error errs ->
+    Affinescript.Tw_verify.pp_report Format.std_formatter errs);
   Affinescript.Wasm_encode.write_module_to_file output m;
   Format.printf "TEA bridge written to %s@." output;
   Format.printf "  affinescript_init()                     — initialise TitleModel@.";
@@ -365,6 +371,12 @@ let tea_bridge_cmd_fn output =
     public/assets/wasm/ directory, and load via AffineTEARouter.load(). *)
 let router_bridge_cmd_fn output =
   let m = Affinescript.Tea_router.generate () in
+  (* Stage 8: auto-verify ownership constraints before writing. *)
+  (match Affinescript.Tw_verify.verify_from_module m with
+  | Ok () ->
+    Format.printf "typed-wasm ownership verification: OK@."
+  | Error errs ->
+    Affinescript.Tw_verify.pp_report Format.std_formatter errs);
   Affinescript.Wasm_encode.write_module_to_file output m;
   Format.printf "Router bridge written to %s@." output;
   Format.printf "  affinescript_router_init()                          — initialise RouterModel@.";
@@ -515,6 +527,12 @@ let compile_file face json wasm_gc path output =
                   (Affinescript.Codegen.show_codegen_error e);
                 `Error (false, "Code generation error")
               | Ok wasm_module ->
+                (* Stage 8: auto-verify typed-wasm ownership constraints.
+                   Printed as informational; does not block compilation. *)
+                (match Affinescript.Tw_verify.verify_from_module wasm_module with
+                | Ok () -> ()
+                | Error errs ->
+                  Affinescript.Tw_verify.pp_report Format.err_formatter errs);
                 Affinescript.Wasm_encode.write_module_to_file output wasm_module;
                 Format.printf "Compiled %s -> %s (WASM)@." path output;
                 `Ok ())

test/test_e2e.ml

@@ -1290,13 +1290,26 @@ let test_bridge_tea_layout_section () =
     let version_byte = Char.code (Bytes.get payload 0) in
     Alcotest.(check int) "layout version byte = 1" 1 version_byte
 
+(** Stage 8: TEA bridge module passes typed-wasm Level 7/10 verification.
+    [fn_update] uses [LocalGet 0] (msg) exactly once — branch-max semantics
+    ensure the if/else in fn_push does not cause false positives here. *)
+let test_bridge_ownership_verify () =
+  let m = Tea_bridge.generate () in
+  match Tw_verify.verify_from_module m with
+  | Ok () -> ()   (* expected *)
+  | Error errs ->
+    let msg = String.concat "; " (List.map (fun e ->
+      Format.asprintf "%a" Tw_verify.pp_error e) errs) in
+    Alcotest.fail (Printf.sprintf "TEA bridge failed ownership verification: %s" msg)
+
 let tea_bridge_tests = [
   Alcotest.test_case "structure (7 funcs, 1 mem, 8 exports)" `Quick test_bridge_structure;
   Alcotest.test_case "export names all present"              `Quick test_bridge_export_names;
   Alcotest.test_case "two custom sections"                   `Quick test_bridge_custom_sections;
   Alcotest.test_case "Wasm binary magic + version"           `Quick test_bridge_wasm_magic;
   Alcotest.test_case "update msg param is Linear"            `Quick test_bridge_update_msg_linear;
   Alcotest.test_case "tea_layout section present + versioned" `Quick test_bridge_tea_layout_section;
+  Alcotest.test_case "ownership verify: clean"               `Quick test_bridge_ownership_verify;
 ]
 
 (* ============================================================================
@@ -1436,6 +1449,18 @@ let test_router_tea_layout_section () =
     let version_byte = Char.code (Bytes.get payload 0) in
     Alcotest.(check int) "layout version byte = 1" 1 version_byte
 
+(** Stage 8: Router bridge module passes typed-wasm Level 7/10 verification.
+    Branch-max semantics: fn_push uses [LocalGet 0] in the then-branch only
+    (else = stack full, silent drop).  max(1, 0) = 1 → OK. *)
+let test_router_ownership_verify () =
+  let m = Tea_router.generate () in
+  match Tw_verify.verify_from_module m with
+  | Ok () -> ()   (* expected *)
+  | Error errs ->
+    let msg = String.concat "; " (List.map (fun e ->
+      Format.asprintf "%a" Tw_verify.pp_error e) errs) in
+    Alcotest.fail (Printf.sprintf "Router bridge failed ownership verification: %s" msg)
+
 let tea_router_tests = [
   Alcotest.test_case "structure (11 funcs, 1 mem, 12 exports)" `Quick test_router_structure;
   Alcotest.test_case "export names all present"                 `Quick test_router_export_names;
@@ -1445,6 +1470,7 @@ let tea_router_tests = [
   Alcotest.test_case "present_popup param is Linear"            `Quick test_router_present_popup_param_linear;
   Alcotest.test_case "resize w+h params are both Linear"        `Quick test_router_resize_params_linear;
   Alcotest.test_case "tea_layout section present + versioned"   `Quick test_router_tea_layout_section;
+  Alcotest.test_case "ownership verify: clean"                  `Quick test_router_ownership_verify;
 ]
 
 (* ============================================================================