feat(borrow): CFG-join for ExprHandle + ExprTry catch arms (CORE-01 pt3 Slice C-light, Refs #177) (#358)

## Summary

CORE-01 Phase 3 **Slice C-light** — CFG-join semantics for `ExprHandle`
handler arms and `ExprTry` catch arms. Both were previously checked
*sequentially* against a shared state, so moves/borrows from arm i
polluted the state seen by arm i+1 — even though only one arm runs at
runtime. This PR mirrors the snapshot-restore-merge pattern that
`ExprMatch` already does inline, and factors the merge logic into a
`merge_arm_results` helper that all CFG-join sites can share.

### Before (sequential)

```affine
fn catch_arm_isolation() -> Unit {
  let y = 100;
  try { 0 } catch {
    0 => drop_int(y),
    1 => drop_int(y),     // ← spurious UseAfterMove: arm 0 polluted state.moved
    _ => ()
  }
}
```

### After (isolated)

Each arm runs against the post-body state independently; the merge takes
intersection of borrows and union of moves.

## Mechanics

New helper near `check_expr` in `lib/borrow.ml`:

```ocaml
val merge_arm_results :
  state -> borrow list -> move_record list ->
  (unit result * borrow list * move_record list) list ->
  unit result
```

- Errors: propagates the first error seen.
- Borrows: intersection across arms (branch-local borrows die at
arm-block exit anyway; this just formalises the join).
- Moves: union across arms, deduplicated against the base — a place is
moved post-join if any arm moved it (conservative-sound).

Wired into `ExprHandle` and `ExprTry`. `ExprMatch`'s inlined logic is
**deliberately untouched** — same semantics, but PR-scope discipline
says don't refactor a stable code path here.

For `ExprTry`: `check_block(body)` runs first (its block-local borrows
are cleaned at block exit; moves persist). The snapshot is taken *after*
check_block, so catch arms see the body's moves in `base_moved`. The
merge's dedupe-against-base preserves them through the join. `finally`
runs deterministically after the merge.

## Tests (E2E Borrow Graph, +2)

| Fixture | Direction | Expected |
|---|---|---|
| `slice_c_catch_arm_isolation.affine` | positive | Ok — two arms
independently move `y`, currently rejected with spurious UseAfterMove |
| `slice_c_body_move_persists.affine` | anti-regression | UseAfterMove
on `read_int(y)` after the body moved `y`, even with a `_ =>` catch arm
|

## Scope of this PR

`ExprHandle` is implemented in parallel but has **no dedicated test
fixture** — the AffineScript test corpus has no live `handle`
expressions outside the parser's grammar tests, so an end-to-end
borrow-graph fixture for it would be the first. The code path is
exercised whenever a real `handle` appears; until then, soundness is by
symmetry with `ExprTry`.

**Deferred (Slices C-full / C' / D):**
- **Slice C-full** — true Polonius origin/region variables on
`TyRef`/`TyMut` with subset constraints + datalog-style
loan-live-at-point solver. Architectural change to the type system;
ADR-gated.
- **Slice C'** — loop soundness via a 2-iteration check on
`StmtWhile`/`StmtFor`. Coupled to a `StmtAssign` clear-on-rewrite fix
(assignment is currently treated as a read of LHS, so the naive 2-iter
spuriously fails on legitimate re-assignment loops).
- **Ref-to-ref binding** — `r = some_other_ref_var` (RHS not a direct
`&place`) still leaves the ref-binding stale. Symmetric let/assign
limitation.
- **Slice D** — tighter quantity-checker integration for captured
linears.

## Docs

- `STATE.a2ml` `borrow-checker` →
`phase-3-parts-1-3-Slices-A-B-C-light-landed`
- `CAPABILITY-MATRIX.adoc` borrow-checker row records Slice C-light
- `TECH-DEBT-alt.adoc` CORE-01 row narrows residual to C-full / C' / D +
ref-to-ref binding

## Test plan

- [ ] CI `build` (opam exec -- dune build) green
- [ ] CI `Run tests` (opam exec -- dune runtest) — `E2E Borrow Graph`
count +2
- [ ] Existing `try_catch_*` / `try_finally` fixtures (single-arm Int
expressions, no move/borrow) untouched

**Local-build caveat**: container has no OCaml toolchain; CI is the
source of truth.

Refs #177

---
_Generated by [Claude
Code](https://claude.ai/code/session_01TLERhquTknLCfyjv7eQU8b)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -71,7 +71,7 @@ test-files = 54
 # the feature is not enforced on user programs through the CLI pipeline.
 affine-types = "wired-and-reachable (Track A Manhattan plan complete 2026-04-10. Quantity semiring in lib/quantity.ml; invoked from typecheck.ml:1206 inside the standard CLI pipeline. Surface syntax per ADR-007 hybrid: @linear/@erased/@unrestricted attributes (Option C primary) on let/stmt-let/param/lambda-param, AND :1/:0/:ω numeric sugar (Option B) on let/stmt-let. Scaled Let rule per ADR-002 implemented in lib/quantity.ml ExprLet/StmtLet — closes BUG-001 (ω-let smuggles linear values) and BUG-002 (zero-let erasure). Four regression fixtures in test/e2e/fixtures/ exercise both surface forms. Behavioural enforcement verified via E2E Quantity test suite — 4 new passing tests, 0 regressions.)"
 linear-arrows = "enforced (2026-04-11): Three-part fix landed. (1) typecheck.ml lambda synth: |@linear x: T| e now synthesises T -[1]-> U (was always QOmega). (2) typecheck.ml lambda check mode: explicit param quantity annotation validated against expected TArrow quantity; unannotated params inherit context quantity. (3) quantity.ml ExprLambda: added env.errors accumulator; annotated lambda params declared via env_declare so env_use tracks them; usage verified with check_quantity after body walk; violations pushed to env.errors and drained at end of check_function_quantities (step 4). Saved/restored env.quantities entries to prevent scope leakage. Two E2E fixtures + 2 passing tests. 75 tests total, 0 regressions. Commit d2f9b7b pushed."
-borrow-checker = "phase-3-parts-1-3-Slices-A-and-B-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted (&local escaping its block), shared-XOR-exclusive enforced at use sites (UseWhileExclusivelyBorrowed), ownership derived from param type TyOwn/TyRef/TyMut, call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape + &mut e parser surface (zero Menhir conflict delta — exclusive borrow finally expressible from real source). pt3 Slice A (PR #335) NLL last-use expiry: forward pre-pass compute_last_use_index maps each symbol to its greatest mentioning statement index; check_block expires ref-bindings introduced in-block once their binder is dead. Unblocks `let r = &x; print(*r); x = 2` and `let m = &mut x; let y = *m; x` (2 positive + 1 anti-regression in E2E Borrow Graph). pt3 Slice B (this PR) flow-sensitive escape via re-assignment: `outer = &y` in StmtAssign now pre-releases the held borrow and re-binds the (binder → new_borrow) ref-graph entry to the freshly-created borrow, so NLL last-use + return-escape see the *current* referent. 3 hermetic tests (2 positive + 1 anti-regression). Residual (Slices C–D): origin/region variables (Polonius surface) + loan-live-at-point dataflow for CFG joins in ExprHandle/ExprTry/loops; tighter quantity integration for captured linears; reborrow through indirection (RHS that is a ref-typed value rather than a direct &place). Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT.adoc CORE-01."
+borrow-checker = "phase-3-parts-1-3-Slices-A-B-C-light-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted, shared-XOR-exclusive enforced at use sites, ownership from param type TyOwn/TyRef/TyMut, call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape + &mut e parser surface. pt3 Slice A (PR #335) NLL last-use expiry: compute_last_use_index pre-pass; check_block expires in-block ref-bindings once their binder is dead. pt3 Slice B (effectively #354/#355/#356 after #351 procedural close) flow-sensitive escape via re-assignment: `outer = &y` in StmtAssign pre-releases the held borrow and re-binds the ref-graph entry to the freshly-created borrow. pt3 Slice C-light (this PR) CFG-join semantics for non-match join constructs: ExprHandle handler arms and ExprTry catch arms are now isolated via snapshot-restore-merge (factored merge_arm_results helper, mirroring ExprMatch's inlined logic) — moves/borrows from arm i no longer pollute arm i+1. 2 hermetic tests (positive: independent catch-arm moves OK; anti-regression: body-side move persists past the try). Residual (Slices C-full, C', D): true Polonius origin/region variables on TyRef/TyMut with subset constraints + datalog-style solver (architectural; ADR-gated); loop soundness via 2-iter check (coupled to StmtAssign clear-on-rewrite fix); reborrow through indirection (ref-to-ref binding); quantity-checker tightening for captured linears. Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT-alt.adoc CORE-01."
 row-polymorphism = "60% (records + effects rows implemented in typecheck/unify; not fully exercised end-to-end)"
 effects = "interpreter-complete (handler dispatch, PerformEffect propagation, ExprResume, multi-arg ops all wired in interp.ml 2026-04-11). WasmGC: ops registered as unreachable stubs; ExprHandle/ExprResume reject with UnsupportedFeature — full WASM dispatch needs EH proposal or CPS transform."
 dependent-types = "parse-only (TRefined AST node exists and refinement predicates parse, but predicates do not reduce; no SMT/decision procedure wired in)"

docs/CAPABILITY-MATRIX.adoc

@@ -107,10 +107,19 @@ now pre-releases the held borrow and re-binds the
 so the NLL last-use + return-escape analyses see the *current* referent
 after re-assignment, not the stale original (3 hermetic tests: old
 released, new tracked by NLL, anti-regression that new borrow still
-protects). *Deferred (Slices C–D):* origin/region variables (Polonius
-surface) + loan-live-at-point dataflow across CFG joins for
-`ExprHandle`/`ExprTry`/loops; tighter quantity integration for captured
-linears; reborrow through indirection (RHS not a direct `&place`).
+protects). *Part 3 Slice C-light* (Refs #177): CFG-join semantics for
+non-match join constructs — `ExprHandle` handler arms and `ExprTry`
+catch arms are now isolated via snapshot-restore-merge (factored
+`merge_arm_results` helper, mirroring `ExprMatch`'s inlined logic).
+Moves/borrows from arm i no longer pollute arm i+1; finally runs
+deterministically against the merged post-catch state. 2 hermetic
+tests (positive + anti-regression). *Deferred (Slices C-full / C' /
+D):* true Polonius origin/region variables on `TyRef`/`TyMut` with
+subset constraints + datalog-style loan-live-at-point solver
+(ADR-gated); loop soundness via 2-iter check on `StmtWhile`/
+`StmtFor` (coupled to a `StmtAssign` clear-on-rewrite fix); reborrow
+through indirection (RHS not a direct `&place`); quantity-checker
+tightening for captured linears.
 
 |Quantity / affine types |*enforced* |QTT semiring in `lib/quantity.ml`,
 invoked inside the standard CLI pipeline. `@linear`/`@erased`/`@unrestricted`

docs/TECH-DEBT.adoc

@@ -164,15 +164,29 @@ the same-target reborrow (`r = &mut x` while `r` already holds
 `&mut x`) does not trip `ConflictingBorrow` on the about-to-be-replaced
 exclusive borrow. 3 hermetic tests in "E2E Borrow Graph" (old released,
 new tracked by NLL, anti-regression that new borrow still protects its
-new target). *Slices C–D residual:* origin/region variables (Polonius
-surface) + loan-live-at-point dataflow across CFG joins for
-`ExprHandle`/`ExprTry`/loops; tighter quantity integration for captured
-linears; reborrow through indirection (`r = some_other_ref_var` RHS does
-not yet copy the other binder's graph entry — symmetric let/assign
-limitation, parks with the let-graph's same restriction). |S1 |pt1 #240
-+ pt2 return-escape + `&mut` surface + pt3 Slices A+B DONE (Refs #177);
-residual = Slices C–D (origin variables, quantity integration,
-ref-to-ref binding) — issue #177
+new target). *Part 3 Slice C-light LANDED* (Refs #177): CFG-join
+semantics for non-match join constructs — `ExprHandle` handler arms
+and `ExprTry` catch arms are now isolated via snapshot-restore-merge,
+extracted into a `merge_arm_results` helper that mirrors `ExprMatch`'s
+inlined logic (intersection on borrows, union on moves, first-error
+propagation). Moves/borrows from arm i no longer pollute arm i+1;
+`finally` runs deterministically against the merged post-catch state.
+2 hermetic tests in "E2E Borrow Graph" (positive: two catch arms can
+independently move the same value; anti-regression: body-side moves
+still propagate past the try, preserving conservative correctness).
+*Residual (Slices C-full / C' / D):* true Polonius origin/region
+variables on `TyRef`/`TyMut` with subset constraints and a datalog-
+style loan-live-at-point solver (architectural change to the type
+system; ADR-gated); loop soundness via a 2-iteration check on
+`StmtWhile`/`StmtFor` (coupled to a `StmtAssign` clear-on-rewrite
+fix — assignment is currently treated as a read of LHS, so the
+naive 2-iter spuriously fails on legitimate re-assignment loops);
+reborrow through indirection (`r = some_other_ref_var` RHS, parks
+with the let-graph's same restriction); tighter quantity-checker
+integration for captured linears. |S1 |pt1 #240 + pt2 return-escape
++ `&mut` surface + pt3 Slices A+B+C-light DONE (Refs #177); residual
+= Slices C-full (origin variables, ADR-gated), C' (loop soundness),
+D (quantity integration), plus ref-to-ref binding — issue #177
 |CORE-02 |Effect-handler dispatch on WasmGC (was `UnsupportedFeature`;
 the chosen path is CPS over the EH proposal). The #225 CPS line closed
 the async slice; #234 generalised the boundary recogniser from a

lib/borrow.ml

@@ -669,6 +669,60 @@ let compute_last_use_index (symbols : Symbol.t) (blk : block)
    | None -> ());
   tbl
 
+(** Merge per-arm post-states after a multi-arm CFG-join construct
+    ([ExprHandle], [ExprTry] catch). Each [arm_result] is a triple
+    [(result, post_arm_borrows, post_arm_moved)] captured immediately
+    after running the arm against the snapshotted base state.
+
+    - Errors: propagates the first error seen (left-to-right).
+    - Borrows: intersection across arms — a borrow is alive post-join
+      only if it is alive at the end of every arm. (Branch-local
+      borrows naturally die at arm exit because the arm body is
+      typically a block whose [check_block] clears them; this just
+      formalises that semantics across the join.)
+    - Moves: union — a place is moved post-join if any arm moved it,
+      deduplicated against the base so we don't double-count moves
+      that already existed before the arms.
+
+    Mirrors the inlined logic in [ExprMatch]'s arm-merge so all CFG-
+    join sites share one notion of "what state survives the join".
+    CORE-01 pt3 Slice C / #177 (CFG-join semantics for non-match
+    join constructs). *)
+let merge_arm_results (state : state)
+    (base_borrows : borrow list) (base_moved : move_record list)
+    (arm_results : (unit result * borrow list * move_record list) list)
+    : unit result =
+  let errors = List.filter_map (fun (r, _, _) ->
+    match r with Error e -> Some e | Ok () -> None) arm_results in
+  match errors with
+  | e :: _ -> Error e
+  | [] ->
+    let all_borrows = List.map (fun (_, bs, _) -> bs) arm_results in
+    let merged_borrows = match all_borrows with
+      | [] -> base_borrows
+      | first :: rest ->
+        List.fold_left (fun acc arm_borrows ->
+          List.filter (fun b ->
+            List.exists (fun b' -> b.b_id = b'.b_id) arm_borrows
+          ) acc
+        ) first rest
+    in
+    let all_moves = List.concat_map (fun (_, _, ms) ->
+      List.filter (fun mr ->
+        not (List.exists (fun base_mr ->
+          places_overlap mr.m_place base_mr.m_place
+        ) base_moved)
+      ) ms
+    ) arm_results in
+    let unique_moves = List.fold_left (fun acc mr ->
+      if List.exists (fun mr' -> places_overlap mr.m_place mr'.m_place) acc
+      then acc
+      else mr :: acc
+    ) [] all_moves in
+    state.borrows <- merged_borrows;
+    state.moved <- base_moved @ unique_moves;
+    Ok ()
+
 (** Check borrows in an expression *)
 let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr : expr) : unit result =
   match expr with
@@ -1046,12 +1100,26 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr :
 
   | ExprHandle eh ->
     let* () = check_expr ctx state symbols eh.eh_body in
-    List.fold_left (fun acc arm ->
-      let* () = acc in
-      match arm with
-      | HandlerReturn (_pat, body) -> check_expr ctx state symbols body
-      | HandlerOp (_op, _pats, body) -> check_expr ctx state symbols body
-    ) (Ok ()) eh.eh_handlers
+    (* CFG-join (CORE-01 pt3 Slice C / #177): handler arms are
+       mutually exclusive continuations dispatched on whether the
+       body returned normally ([HandlerReturn]) or performed an
+       effect-op ([HandlerOp]). Each arm runs against the post-body
+       state independently; moves/borrows from one arm must NOT
+       leak into the next. Mirrors [ExprMatch]'s arm-isolation
+       pattern via [merge_arm_results]. *)
+    let base_borrows = state.borrows in
+    let base_moved = state.moved in
+    let arm_results = List.map (fun arm ->
+      state.borrows <- base_borrows;
+      state.moved <- base_moved;
+      let body = match arm with
+        | HandlerReturn (_pat, b) -> b
+        | HandlerOp (_op, _pats, b) -> b
+      in
+      let r = check_expr ctx state symbols body in
+      (r, state.borrows, state.moved)
+    ) eh.eh_handlers in
+    merge_arm_results state base_borrows base_moved arm_results
 
   | ExprResume e_opt ->
     begin match e_opt with
@@ -1060,18 +1128,32 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr :
     end
 
   | ExprTry et ->
+    (* CFG-join (CORE-01 pt3 Slice C / #177): body runs first, then
+       either succeeds (no-exception path → post-body state
+       propagates) or raises (one catch arm runs).  Catch arms are
+       alternative continuations from the post-body state, so each
+       arm runs against that state independently — moves/borrows
+       must not leak between catch arms.  Finally runs
+       deterministically against the merged post-catch state. *)
     let* () = check_block ctx state symbols et.et_body in
+    let base_borrows = state.borrows in
+    let base_moved = state.moved in
     let* () = match et.et_catch with
+      | None -> Ok ()
       | Some arms ->
-        List.fold_left (fun acc arm ->
-          let* () = acc in
-          let* () = match arm.ma_guard with
-            | Some g -> check_expr ctx state symbols g
-            | None -> Ok ()
+        let arm_results = List.map (fun arm ->
+          state.borrows <- base_borrows;
+          state.moved <- base_moved;
+          let r =
+            let open Result in
+            bind (match arm.ma_guard with
+              | Some g -> check_expr ctx state symbols g
+              | None -> Ok ())
+              (fun () -> check_expr ctx state symbols arm.ma_body)
           in
-          check_expr ctx state symbols arm.ma_body
-        ) (Ok ()) arms
-      | None -> Ok ()
+          (r, state.borrows, state.moved)
+        ) arms in
+        merge_arm_results state base_borrows base_moved arm_results
     in
     begin match et.et_finally with
       | Some blk -> check_block ctx state symbols blk
@@ -1385,15 +1467,35 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
    freshly-created borrow. NLL last-use + return-escape now see the
    *current* referent after re-assignment, not the stale original.
 
+   CORE-01 pt3 Slice C (CFG-join semantics for non-match join
+   constructs): [ExprHandle] handler arms and [ExprTry] catch arms
+   are mutually exclusive continuations from the post-body state.
+   Previously both were checked sequentially against a shared
+   state, so moves/borrows from arm i polluted arm i+1 — a
+   spurious UseAfterMove on the second of two arms that
+   independently move the same value, etc.  Both now snapshot the
+   post-body state, run each arm independently, and merge via
+   [merge_arm_results] (same intersection-borrows / union-moves
+   semantics already used inline by [ExprMatch], now extracted to
+   one helper so all CFG-join sites agree).  Finally runs after
+   the merge, deterministically, against the merged state.
+
    Still deferred:
    - Reborrow through indirection: `r = some_other_ref_var` (RHS not a
      direct `&place`) does not yet copy the other binder's graph
      entry — the ref-binding stays stale.  Same limitation as
      [record_ref_binding] for the let-graph path; would require
      symmetric let/assign handling for ref-to-ref binding.
-   - Origin/region variables (Polonius surface) + loan-live-at-point
-     dataflow across CFG joins for `ExprHandle`/`ExprTry`/loops
-     (Slice C).
+   - Origin/region variables (true Polonius surface) — a region
+     var on each [TyRef]/[TyMut] with subset constraints and a
+     proper datalog-style loan-live-at-point solver.  Architectural
+     change to the type system; ADR-gated.
+   - Loop soundness (`StmtWhile`/`StmtFor`): a single body pass
+     misses multi-iteration move conflicts.  A 2-iteration check
+     would catch them but requires fixing the assignment-clears-
+     move imprecision first (assignment is currently treated as a
+     read of LHS, so `x = …` after a prior move spuriously fails).
+     Couple Slice C' with the StmtAssign clear-on-rewrite fix.
    - Tighter integration with the quantity checker for captured
      linears (Slice D).
 *)

test/e2e/fixtures/slice_c_body_move_persists.affine

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice C / #177 anti-regression: a move performed in
+// the try-body must still be visible after the try/catch (this is
+// the conservative-correct path — body might have moved before
+// throwing, so the post-try state must reflect that the move
+// possibly happened). The Slice C arm-isolation refactor must not
+// drop body-side moves. Reading `y` after the try should error
+// UseAfterMove regardless of what the catch arm does.
+// Expected: Error UseAfterMove.
+
+module SliceCBodyMovePersists;
+
+fn drop_int(x: own Int) -> Unit = ();
+fn read_int(x: Int) -> Int = 0;
+
+fn body_move_persists() -> Int {
+  let y = 100;
+  let r = try {
+    drop_int(y);
+    0
+  } catch {
+    _ => 0
+  };
+  read_int(y) + r
+}

test/e2e/fixtures/slice_c_catch_arm_isolation.affine

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice C / #177: try/catch arm isolation. Each catch
+// arm is an alternative continuation — only one runs at runtime —
+// so moves performed in one arm must not pollute the state seen by
+// the next arm. Without Slice C, the second arm's `drop_int(y)`
+// would see `y` as already moved (by the first arm) and error
+// UseAfterMove. With Slice C, each arm snapshots the post-body
+// state and runs independently. Expected: Ok.
+
+module SliceCCatchArmIsolation;
+
+fn drop_int(x: own Int) -> Unit = ();
+
+fn catch_arm_isolation(flag: Int) -> Unit {
+  let y = 100;
+  try {
+    flag
+  } catch {
+    0 => drop_int(y),
+    1 => drop_int(y),
+    _ => ()
+  }
+}