[soundness] hy-check(channel_liveness): function parameter capabilities (hy.send_cap[T] / hy.recv_cap[T]) untracked, bypassing linearity, affine transfer, and terminal lifecycle checks (#4200 regression) #4416

Activity

1. dukenordj-rgb commented on Nov 12, 2026

   

   dukenordj-rgb

   on Nov 12, 2026

   Contributor

   More actions

   Root Cause

   During function body analysis in compiler/crates/hy-check/src/channel_liveness.rs, ChannelLivenessChecker::check_fn_decl initializes the local dataflow liveness context solely from inside-body variable declarations (such as destructuring hy.pipe[T]() calls). It fails to inspect and seed the function parameter list (fn_decl.params) into the linear tracking map (CapabilityTracker).

   Because hy.send_cap[T] and hy.recv_cap[T] function parameters are omitted from the initial AST variable binding map for the scope:

   1. Move operations (move tx) on parameter bindings bypass single-ownership tracking, disabling HYB-E3001 (double move / use-after-move).
   2. Asynchronous task captures of parameters bypass move-mode validations, disabling HYB-E3002 (unmoved capture across task boundaries).
   3. Terminal liveness verification at function scope exit skips parameter symbols, permitting leaking unclosed send capabilities (bypassing HYB-E4004) and undrained receive capabilities (bypassing HYB-E4005).

   ---

   Patch Solution

   In compiler/crates/hy-check/src/channel_liveness.rs, seed all function parameter capabilities into the AST scope's active linear environment prior to visiting the function block.

   --- a/compiler/crates/hy-check/src/channel_liveness.rs
   +++ b/compiler/crates/hy-check/src/channel_liveness.rs
   @@ -112,6 +112,23 @@ impl<'a> Visitor<'a> for ChannelLivenessChecker {
        fn visit_fn_decl(&mut self, func: &'a FnDecl) {
            self.scopes.enter_scope(ScopeKind::Function);
   
   +        // Seed parameter capability bindings into the current scope's linear tracker
   +        for param in &func.params {
   +            if let Some(cap_ty) = self.type_cx.resolve_capability_type(&param.ty) {
   +                let state = CapabilityState::new(
   +                    param.id,
   +                    param.name.clone(),
   +                    cap_ty,
   +                    param.span,
   +                );
   +                if let Err(err) = self.tracker.register_capability(param.id, state) {
   +                    self.diagnostics.emit(err);
   +                }
   +            }
   +        }
   +
            self.visit_block(&func.body);
   
            // Validate linearity and terminal lifecycle states for all scoped capabilities
   +        self.tracker.check_scope_terminal_states(&mut self.diagnostics);
            self.scopes.exit_scope();
        }

   ---

   Regression Test Coverage

   Add integration tests in compiler/crates/hy-check/tests/channel_liveness_test.rs ensuring all five parameter escape vectors trigger diagnostics:

   #[test]
   fn test_parameter_capability_liveness_regressions() {
       let cases = vec![
           (
               "repro1_unclosed_sender",
               r#"fn worker(tx hy.send_cap[int]) { tx.send(42) }"#,
               "HYB-E4004",
           ),
           (
               "repro2_double_move",
               r#"fn forwarder(tx hy.send_cap[int]) { task sub(move tx); task sub(move tx) }"#,
               "HYB-E3001",
           ),
           (
               "repro3_use_after_move",
               r#"fn forwarder(tx hy.send_cap[int]) { task sub(move tx); tx.send(10) }"#,
               "HYB-E3001",
           ),
           (
               "repro4_undrained_recv",
               r#"fn receiver(rx hy.recv_cap[int]) { _ = rx.recv() }"#,
               "HYB-E4005",
           ),
           (
               "repro5_unmoved_task_capture",
               r#"fn forwarder(tx hy.send_cap[int]) { task sub(tx); tx.close() }"#,
               "HYB-E3002",
           ),
       ];
   
       for (name, source, expected_code) in cases {
           let diagnostics = run_hy_check(source);
           assert!(
               diagnostics.iter().any(|d| d.code == expected_code),
               "Test {} failed: expected diagnostic {}, got {:?}",
               name, expected_code, diagnostics
           );
       }
   }