feat(tw_verify): Stage 9 — per-path min/max linearity analysis

Replace branch-max single-count with per-path (min_uses, max_uses) range
analysis in the typed-wasm ownership verifier.

Key changes:
- tw_verify.ml: `count_uses_range` returns (min, max) across all paths.
  For `If` nodes: min=min(then,else), max=max(then,else). Sequential instrs
  sum their ranges. `LinearDroppedOnSomePath` error added for min=0, max≥1.
- tea_router.ml: `fn_push` else-branch now `[LocalGet 0; Drop]` instead of
  `[]`. Ownership is explicitly discharged when the stack is full, giving
  min=1, max=1 on both paths — clean under per-path analysis.
- test_e2e.ml: 2 new E2E tests (one-arm drop → LinearDroppedOnSomePath;
  explicit else-drop → OK). Test 7 comment updated. Bridge/router verify
  comments updated. 161/161 tests.

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

Author: hyperpolymath

lib/tea_router.ml

@@ -158,7 +158,13 @@ let fn_init : func = {
     the back-stack if the stack is not full.
 
     Encoding: [stack_data[stack_len] := screen_tag; stack_len += 1].
-    [screen_tag] is Linear — consumed exactly once per TEA update cycle. *)
+    [screen_tag] is Linear — consumed exactly once per TEA update cycle.
+
+    When the stack is full the screen_tag is explicitly dropped via [Drop]
+    rather than left in an unused-param else-branch.  This satisfies the
+    per-path linearity verifier: both branches consume param 0 exactly once
+    (store in the then-branch, explicit drop in the else-branch), giving
+    min_uses = 1, max_uses = 1 → OK. *)
 let fn_push : func = {
   f_type   = 1;
   f_locals = [];
@@ -189,8 +195,8 @@ let fn_push : func = {
         I32Add;
         I32Store (2, 0);
       ],
-      (* else: stack full — no-op, message consumed but state unchanged *)
-      []
+      (* else: stack full — explicitly consume screen_tag (ownership discharged) *)
+      [ LocalGet 0; Drop ]
     );
   ];
 }

lib/tw_verify.ml

@@ -1,7 +1,7 @@
 (* SPDX-License-Identifier: PMPL-1.0-or-later *)
 (* SPDX-FileCopyrightText: 2024-2026 hyperpolymath *)
 
-(** typed-wasm ownership verifier — Stage 7.
+(** typed-wasm ownership verifier — Stage 7 (per-path analysis added Stage 9).
 
     Statically verifies typed-wasm Level 7 (aliasing safety) and Level 10
     (linearity) constraints on AffineScript's Wasm IR.
@@ -13,21 +13,21 @@
     re-checks them on the emitted Wasm IR to catch any codegen bugs.
 
     Level 10 — Linearity: a parameter annotated [Linear] (TyOwn) must be
-    loaded exactly once in the function body.  Loading zero times means the
-    owned value is dropped; loading more than once means it may be duplicated.
+    loaded exactly once on every execution path.  Zero uses = dropped;
+    more than one use = possible duplication; non-zero use on some paths
+    but zero on others = partial drop (dropped on the zero-count path).
 
     Level 7 — Aliasing safety: a parameter annotated [ExclBorrow] (TyMut)
-    must be loaded at most once.  Multiple loads create aliased references to
-    the same mutable memory, violating exclusive-borrow invariants.
+    must be loaded at most once on any execution path.
 
-    [SharedBorrow] (TyRef) and [Unrestricted] params are not checked by this
-    pass (no constraints violated by multiple reads of a shared reference).
+    [SharedBorrow] (TyRef) and [Unrestricted] params are not checked.
 
-    Branch semantics: for [If] instructions, we take the {b max} of the
-    use-counts across the two branches (since only one branch executes at
-    runtime).  This is conservative: a linear param used exactly once in
-    each branch of an if/else is counted as 1 (correct), not 2.  Stage 8
-    will refine this with a per-path analysis if needed.
+    Branch semantics (per-path min/max): for [If] instructions we compute
+    [(min_then, max_then)] and [(min_else, max_else)] independently and
+    combine as [(min_then, max_then, min_else, max_else) →
+    (min min_then min_else, max max_then max_else)].  A Linear param used
+    exactly once in BOTH branches gives (1, 1) — OK.  A param used in the
+    then-branch only gives (min=0, max=1) — [LinearDroppedOnSomePath].
 
     @see typed-wasm LEVEL-STATUS.md — Level 7 and Level 10 sections.
 *)
@@ -41,37 +41,57 @@ open Codegen
 (** An ownership violation found in a Wasm function body. *)
 type ownership_error =
   | LinearNotUsed of { func_idx : int; param_idx : int }
-  (** Level 10: Linear parameter was never loaded — dropped without consumption.
-      The owned resource leaks. *)
+  (** Level 10: Linear parameter was never loaded on any path — dropped without
+      consumption.  The owned resource leaks unconditionally. *)
+  | LinearDroppedOnSomePath of { func_idx : int; param_idx : int }
+  (** Level 10: Linear parameter is consumed on some execution paths but
+      silently dropped on others (per-path min_uses = 0, max_uses >= 1).
+      The caller's ownership guarantee is satisfied only conditionally —
+      the drop path leaks the resource. *)
   | LinearUsedMultiple of { func_idx : int; param_idx : int; count : int }
-  (** Level 10: Linear parameter was loaded [count] times — potential duplication.
-      Only one consumer is permitted. *)
+  (** Level 10: Linear parameter was loaded [count] times on some path —
+      potential duplication.  Only one consumer is permitted. *)
   | ExclBorrowAliased of { func_idx : int; param_idx : int; count : int }
   (** Level 7: ExclBorrow parameter was loaded [count] times — aliasing violation.
       An exclusive borrow must not have multiple simultaneous references. *)
 
 (* ============================================================================
-   Use-count analysis
+   Per-path use-range analysis
    ============================================================================ *)
 
-(** Count how many times [local_idx] is loaded inside [instrs].
+(** Compute [(min_uses, max_uses)] — the minimum and maximum number of times
+    [local_idx] is loaded across all execution paths within [instrs].
 
-    For [If] nodes the branch counts are combined with [max] rather than
-    summed, reflecting that only one branch executes.  All other nodes are
-    summed.  Nested [Block] and [Loop] bodies are descended into. *)
-let rec count_uses (local_idx : int) (instrs : Wasm.instr list) : int =
-  List.fold_left (fun acc instr -> acc + uses_in_instr local_idx instr) 0 instrs
+    Sequential instructions sum their ranges: if instr A uses the param
+    (1, 1) times and instr B uses it (0, 1) times, the sequence is (1, 2).
 
-and uses_in_instr (local_idx : int) (instr : Wasm.instr) : int =
+    For [If] nodes only one branch executes, so we take the component-wise
+    min/max of the two branch ranges:
+      - [min = min(then_min, else_min)]: may be zero if one branch doesn't use it
+      - [max = max(then_max, else_max)]: the worst-case duplication count
+
+    Example: [If { LocalGet 0 } { LocalGet 0 }] → [(1, 1)] OK for Linear.
+    Example: [If { LocalGet 0 } { [] }]         → [(0, 1)] LinearDroppedOnSomePath.
+    Example: [If { LocalGet 0; LocalGet 0 } { LocalGet 0 }] → [(1, 2)]
+      → LinearUsedMultiple (max = 2).
+
+    Nested [Block] and [Loop] bodies are descended into (no new paths). *)
+let rec count_uses_range (local_idx : int) (instrs : Wasm.instr list) : int * int =
+  List.fold_left (fun (a_min, a_max) instr ->
+    let (i_min, i_max) = uses_range_in_instr local_idx instr in
+    (a_min + i_min, a_max + i_max)
+  ) (0, 0) instrs
+
+and uses_range_in_instr (local_idx : int) (instr : Wasm.instr) : int * int =
   match instr with
-  | Wasm.LocalGet n -> if n = local_idx then 1 else 0
+  | Wasm.LocalGet n -> if n = local_idx then (1, 1) else (0, 0)
   | Wasm.Block (_, body) | Wasm.Loop (_, body) ->
-    count_uses local_idx body
+    count_uses_range local_idx body
   | Wasm.If (_, then_, else_) ->
-    (* Only one branch executes: take max so that
-       If { then: LocalGet 0 } { else: LocalGet 0 } counts as 1, not 2. *)
-    max (count_uses local_idx then_) (count_uses local_idx else_)
-  | _ -> 0
+    let (t_min, t_max) = count_uses_range local_idx then_ in
+    let (e_min, e_max) = count_uses_range local_idx else_ in
+    (min t_min e_min, max t_max e_max)
+  | _ -> (0, 0)
 
 (* ============================================================================
    Per-function verification
@@ -82,27 +102,39 @@ and uses_in_instr (local_idx : int) (instr : Wasm.instr) : int =
     [func] is the Wasm function body.
     [param_kinds] are the ownership annotations for each parameter (in order).
     [func_idx] is the global function index (for error reporting).
-    Returns all violations found (empty list = clean). *)
+    Returns all violations found (empty list = clean).
+
+    Uses per-path min/max analysis:
+    - [LinearNotUsed]: max_uses = 0 (param dropped on every path)
+    - [LinearDroppedOnSomePath]: min_uses = 0, max_uses >= 1 (dropped conditionally)
+    - [LinearUsedMultiple]: max_uses > 1 (duplicated on some path)
+    Multiple violations can be reported for a single param (e.g. both
+    [LinearDroppedOnSomePath] and [LinearUsedMultiple] if min=0, max>1). *)
 let verify_function
     (func     : Wasm.func)
     (param_kinds : ownership_kind list)
     (func_idx : int)
   : ownership_error list =
   List.concat_map (fun (param_idx, kind) ->
-    let uses = count_uses param_idx func.Wasm.f_body in
+    let (min_uses, max_uses) = count_uses_range param_idx func.Wasm.f_body in
     match kind with
     | Linear ->
-      (* Exactly once: zero = dropped, >1 = may be duplicated. *)
-      if uses = 0 then
-        [LinearNotUsed { func_idx; param_idx }]
-      else if uses > 1 then
-        [LinearUsedMultiple { func_idx; param_idx; count = uses }]
-      else
-        []
+      (* Exactly once on every path: zero everywhere = dropped; zero on some
+         path = partial drop; more than one on some path = may duplicate. *)
+      let drop_errors =
+        if max_uses = 0 then [LinearNotUsed { func_idx; param_idx }]
+        else if min_uses = 0 then [LinearDroppedOnSomePath { func_idx; param_idx }]
+        else []
+      in
+      let dup_errors =
+        if max_uses > 1 then [LinearUsedMultiple { func_idx; param_idx; count = max_uses }]
+        else []
+      in
+      drop_errors @ dup_errors
     | ExclBorrow ->
-      (* At most once: >1 creates simultaneous aliases. *)
-      if uses > 1 then
-        [ExclBorrowAliased { func_idx; param_idx; count = uses }]
+      (* At most once on any path: max > 1 creates simultaneous aliases. *)
+      if max_uses > 1 then
+        [ExclBorrowAliased { func_idx; param_idx; count = max_uses }]
       else
         []
     | Unrestricted | SharedBorrow ->
@@ -217,12 +249,17 @@ let pp_error (fmt : Format.formatter) (err : ownership_error) : unit =
   | LinearNotUsed { func_idx; param_idx } ->
     Format.fprintf fmt
       "Level 10 violation: function %d, param %d — Linear (own) param dropped \
-       (must be consumed exactly once)"
+       on all paths (must be consumed exactly once)"
+      func_idx param_idx
+  | LinearDroppedOnSomePath { func_idx; param_idx } ->
+    Format.fprintf fmt
+      "Level 10 violation: function %d, param %d — Linear (own) param dropped \
+       on some paths (per-path min uses = 0; must be consumed on every path)"
       func_idx param_idx
   | LinearUsedMultiple { func_idx; param_idx; count } ->
     Format.fprintf fmt
       "Level 10 violation: function %d, param %d — Linear (own) param loaded \
-       %d times (exactly 1 required; possible duplication)"
+       %d times on some path (exactly 1 required; possible duplication)"
       func_idx param_idx count
   | ExclBorrowAliased { func_idx; param_idx; count } ->
     Format.fprintf fmt

test/test_e2e.ml

@@ -1291,8 +1291,8 @@ let test_bridge_tea_layout_section () =
     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. *)
+    [fn_update] uses [LocalGet 0] (msg) exactly once — per-path analysis
+    gives min=1, max=1 → OK. *)
 let test_bridge_ownership_verify () =
   let m = Tea_bridge.generate () in
   match Tw_verify.verify_from_module m with
@@ -1449,9 +1449,9 @@ 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. *)
+(** Stage 9: Router bridge module passes typed-wasm Level 7/10 verification.
+    fn_push: then-branch stores LocalGet 0, else-branch explicitly [LocalGet 0; Drop].
+    Per-path analysis: min(1,1)=1, max(1,1)=1 → OK. *)
 let test_router_ownership_verify () =
   let m = Tea_router.generate () in
   match Tw_verify.verify_from_module m with
@@ -2115,11 +2115,11 @@ let test_verify_unrestricted_ok () =
   let errs = Tw_verify.verify_module m (single_annot [Codegen.Unrestricted]) in
   Alcotest.(check bool) "unrestricted multi-load → OK" true (errs = [])
 
-(* ---- Test 7: If branch — Linear used once in each arm → branch-max=1 → OK ---- *)
+(* ---- Test 7: If branch — Linear used once in each arm → per-path (1,1) → OK ---- *)
 
 let test_verify_if_branch_ok () =
   (* if (1) { LocalGet 0 } else { LocalGet 0 }
-     Branch-max semantics: max(1, 1) = 1 → OK. *)
+     Per-path analysis: min(1,1)=1, max(1,1)=1 → OK. *)
   let body = [
     Wasm.I32Const 1l;
     Wasm.If (Wasm.BtType Wasm.I32,
@@ -2128,7 +2128,46 @@ let test_verify_if_branch_ok () =
   ] in
   let m = mk_single_func_module body in
   let errs = Tw_verify.verify_module m (single_annot [Codegen.Linear]) in
-  Alcotest.(check bool) "if/else each use once → branch-max OK" true (errs = [])
+  Alcotest.(check bool) "if/else each use once → per-path OK" true (errs = [])
+
+(* ---- Test 10: Linear dropped in one branch only → LinearDroppedOnSomePath ---- *)
+
+let test_verify_if_partial_drop () =
+  (* if (1) { LocalGet 0 } else { [] }
+     Per-path analysis: then=(1,1), else=(0,0) → combined (min=0, max=1).
+     min_uses=0, max_uses=1 → LinearDroppedOnSomePath violation. *)
+  let body = [
+    Wasm.I32Const 1l;
+    Wasm.If (Wasm.BtEmpty,
+      [Wasm.LocalGet 0; Wasm.Drop],
+      []);
+  ] in
+  let m = mk_single_func_module body in
+  let errs = Tw_verify.verify_module m (single_annot [Codegen.Linear]) in
+  Alcotest.(check bool) "linear dropped in one branch → LinearDroppedOnSomePath" true
+    (List.exists (function
+       | Tw_verify.LinearDroppedOnSomePath { param_idx = 0; _ } -> true
+       | _ -> false) errs)
+
+(* ---- Test 11: Linear consumed in then, explicitly dropped in else → OK ---- *)
+(*
+   This mirrors fn_push in tea_router.ml after Stage 9 fix.
+   then: LocalGet 0; I32Store  (uses param once)
+   else: LocalGet 0; Drop       (explicitly drops param)
+   Per-path: min(1,1)=1, max(1,1)=1 → OK. *)
+
+let test_verify_if_explicit_drop_ok () =
+  let body = [
+    Wasm.I32Const 1l;
+    Wasm.If (Wasm.BtEmpty,
+      (* then: use the value *)
+      [Wasm.LocalGet 0; Wasm.Drop],
+      (* else: explicitly discharge ownership *)
+      [Wasm.LocalGet 0; Wasm.Drop]);
+  ] in
+  let m = mk_single_func_module body in
+  let errs = Tw_verify.verify_module m (single_annot [Codegen.Linear]) in
+  Alcotest.(check bool) "explicit drop in else → per-path OK" true (errs = [])
 
 (* ---- Test 8: Pipeline — ownership_codegen.affine → LinearNotUsed expected ---- *)
 (*
@@ -2166,15 +2205,17 @@ let test_verify_pipeline_clean () =
       Alcotest.fail (Printf.sprintf "Unexpected violations: %s" msg))
 
 let tw_verify_tests = [
-  Alcotest.test_case "linear used once → OK"         `Quick test_verify_linear_ok;
-  Alcotest.test_case "linear dropped → violation"    `Quick test_verify_linear_dropped;
-  Alcotest.test_case "linear duplicated → violation" `Quick test_verify_linear_dup;
-  Alcotest.test_case "excl borrow once → OK"         `Quick test_verify_excl_ok;
-  Alcotest.test_case "excl borrow aliased → violation" `Quick test_verify_excl_aliased;
-  Alcotest.test_case "unrestricted multi-load → OK"  `Quick test_verify_unrestricted_ok;
-  Alcotest.test_case "if/else branch-max linear → OK" `Quick test_verify_if_branch_ok;
-  Alcotest.test_case "pipeline: dropped linear → violation" `Quick test_verify_pipeline_violations;
-  Alcotest.test_case "pipeline: clean fixture → OK"  `Quick test_verify_pipeline_clean;
+  Alcotest.test_case "linear used once → OK"                  `Quick test_verify_linear_ok;
+  Alcotest.test_case "linear dropped → violation"             `Quick test_verify_linear_dropped;
+  Alcotest.test_case "linear duplicated → violation"          `Quick test_verify_linear_dup;
+  Alcotest.test_case "excl borrow once → OK"                  `Quick test_verify_excl_ok;
+  Alcotest.test_case "excl borrow aliased → violation"        `Quick test_verify_excl_aliased;
+  Alcotest.test_case "unrestricted multi-load → OK"           `Quick test_verify_unrestricted_ok;
+  Alcotest.test_case "if/else per-path linear → OK"           `Quick test_verify_if_branch_ok;
+  Alcotest.test_case "pipeline: dropped linear → violation"   `Quick test_verify_pipeline_violations;
+  Alcotest.test_case "pipeline: clean fixture → OK"           `Quick test_verify_pipeline_clean;
+  Alcotest.test_case "if one-arm drop → LinearDroppedOnSomePath" `Quick test_verify_if_partial_drop;
+  Alcotest.test_case "if explicit else-drop → per-path OK"    `Quick test_verify_if_explicit_drop_ok;
 ]
 
 (* ============================================================================