[seenorht]

Summary

Fixes #4416 by tracking function parameter capabilities (\hy.send_cap[T]\ and \hy.recv_cap[T]) in \compiler/crates/hy-check/src/channel_liveness.rs:

1. Parameter Capability Registration: In \check_fn, iterates over \.params\ and registers capabilities (\is_send_cap\ and \is_recv_cap) via
   egister_param_cap, ensuring \ x\ and
   x\ are recognized by \is_cap, \is_tx, \is_rx, and tracked in \cap_to_pipe.
2. Terminal Invariant Checks: Updates \check_terminal_invariants\ to check single-endpoint capabilities (!pipe.tx.is_empty()\ and !pipe.rx.is_empty()), enforcing that send parameters must be closed (\HYB-E4004) and receive parameters must be drained (\HYB-E4005) before function scope exit if not transferred via \move.
3. Affine Transfer & Boundary Invariants: Automatically enforces \HYB-E3001\ on double-moves or use-after-moves of parameter capabilities, and \HYB-E3002\ on unmoved or reference captures across task boundaries.
4. Per-Function Scope Isolation: Clears \scope_stack, \cap_to_pipe, and \pipes_all\ at the start of each top-level \check_fn, eliminating cross-function identifier leakage.
5. Closure Support: Tracks parameter capabilities declared on \Expr::FnLit\ closures, and cleans up the duplicate unreachable \Expr::FnLit\ match arm.

Tests

Added 6 canonical regression tests in \compiler/crates/hy-check/tests/channel_liveness_4200.rs:

• \ est_param_cap_unclosed_sender_reject: Rejects unclosed send capability parameter (\HYB-E4004).
• \ est_param_cap_undrained_receiver_reject: Rejects undrained receive capability parameter (\HYB-E4005).
• \ est_param_cap_double_move_reject: Rejects duplicate \move\ of parameter capability (\HYB-E3001).
• \ est_param_cap_use_after_move_reject: Rejects use after move of parameter capability (\HYB-E3001).
• \ est_param_cap_unmoved_task_capture_reject: Rejects bare capture of parameter capability across task boundary (\HYB-E3002).
• \ est_param_cap_valid_worker_lifecycle_accept: Accepts full valid parameter capability lifecycle (
  x.drain(), \ x.close()).

Bounty & Settlement

Per BOUNTY.md and discussion #295:

• Track: W-026 / P0 Soundness (Milestone 1, [wildcard] Statically verifiable nursery cancellation and channel lifecycle invariants via structured effect types #4200)
• Wallet: \