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

Until now, `ExprHandle` handler arms and `ExprTry` catch arms were
checked *sequentially* against a shared state — so moves and
borrows from arm i polluted the state seen by arm i+1, even though
only one arm runs at runtime.  This produced spurious UseAfterMove
on the second of two catch arms that independently move the same
value, etc.

Slice C-light closes this for handlers and try/catch by mirroring
the snapshot-restore-merge pattern that `ExprMatch` already does
inline.  The merge logic — intersection-on-borrows, union-on-
moves, first-error propagation, dedupe against the base — is now
factored into a single helper, `merge_arm_results`, so all CFG-
join sites agree on "what state survives the join":

- Errors: propagate the first error seen, left-to-right.
- Borrows: intersection across arms (a borrow survives the join
  only if it survived every arm; branch-local borrows naturally
  die at arm exit via `check_block`'s borrows_at_entry restore).
- Moves: union across arms, deduplicated against the base — a
  place is reported as moved post-join if any arm moved it
  (conservative-sound).

`ExprMatch`'s inlined logic is *deliberately left untouched* — same
semantics as the new helper, but its tests have been stable since
PR #240; refactoring it would add risk without ergonomic upside
on this PR.  A future cleanup can converge them.

ExprHandle (`handle body { return(_) => ..., op(p1, p2) => ... }`):
mutually exclusive continuations dispatched on whether the body
returned normally or performed an effect-op.  Body runs against
the current state, then each arm runs against the post-body state
independently via the helper.

ExprTry (`try { body } catch { p => arm; ... } finally { ... }`):
body runs first via `check_block` (so its block-local borrows are
cleaned at block exit; its moves persist).  The snapshot is taken
*after* check_block — so the catch arms run against a state that
already includes the body's moves (conservatively assuming body
might have moved before throwing).  Catch arms merge via the
helper; `finally` then runs deterministically against the merged
post-catch state.

Tests (E2E Borrow Graph, +2):

- `slice_c_catch_arm_isolation.affine` (positive): three catch
  arms, two of which independently `drop_int(y)`.  Pre-Slice-C
  this was rejected — arm 2's `drop_int(y)` saw arm 1's move and
  fired UseAfterMove.  Post-Slice-C every arm starts from the
  post-body state and succeeds independently.

- `slice_c_body_move_persists.affine` (anti-regression): the
  try-body moves `y`; the catch arm matches `_` and ignores `y`;
  after the `try`, a `read_int(y)` must still fail
  UseAfterMove because the body might have moved before throwing.
  This pins that the helper's dedupe-against-base correctly
  preserves body-side moves through the merge.  The current
  `state.moved` propagation does this for free (the snapshot
  *captures* body's moves into base_moved, and the merge sets
  `state.moved <- base_moved @ unique_new`), but the test pins
  the invariant so a future refactor cannot drop it.

ExprHandle is implemented in parallel but has no dedicated test
fixture: the AffineScript test corpus has no live `handle`
expressions outside the parser's own 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.

Anti-regression sweep: all existing borrow / linear-arrow /
quantity fixtures audited.  The `try_catch_*` and `try_finally`
fixtures already in the gate (e/Try semantics smoke tests) are
single-arm and don't touch moves, so they go through the new path
unchanged.  Move-or-borrow scenarios crossing `ExprHandle`/
`ExprTry` are net-new fixtures here.

Docs updated:
- `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 (origin variables, ADR-gated), C' (loop soundness),
  D (quantity integration), plus ref-to-ref binding.

NOTE: container has no OCaml toolchain; `dune build` / `dune runtest`
not run locally. CI is the source of truth.  Mechanically scoped to
two arms of `check_expr` plus one new helper.

Author: claude

.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-alt.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),
+    _ => ()
+  }
+}