hy-check(channel_liveness): capability identity leaks between function bodies — a move tx in one fn rejects another fn's own tx (declaration order decides) #4462

Activity

1. dukenordj-rgb commented on Nov 14, 2026

   

   dukenordj-rgb

   on Nov 14, 2026

   Contributor

   More actions

   VERDICT: VIABLE

   Root Cause Analysis

   The channel liveness analysis pass in compiler/crates/hy-check/src/channel_liveness.rs maintains state (ScopeState, moved_caps, and capability-to-pipe mappings) across the entire file scope rather than isolating them per function definition. When a function body is checked, its scope is pushed onto a file-level root. Upon leaving the function scope, pop_scope promotes moved capabilities upward to the file-level parent scope. Consequently, any linear capability name consumed via a move in an earlier function persists in the global scope stack and poisons subsequent functions that declare a local variable or parameter with the identical identifier.

   Code Patch

   To scope capability liveness and movement strictly to individual function boundaries while still correctly propagating moves from nested closures or blocks up to their enclosing function body, check_fn must initialize an isolated capability environment and scope stack.

   // compiler/crates/hy-check/src/channel_liveness.rs
   
   impl<'a> ChannelLivenessChecker<'a> {
       fn check_fn(&mut self, fn_node: &ast::FnDecl) -> Result<(), CheckError> {
           // Isolate function-level capability state and scope stack
           let outer_moved = std::mem::take(&mut self.current_scope.moved_caps);
           let outer_pipes = std::mem::take(&mut self.cap_to_pipe);
           
           self.push_scope();
           
           // Process function parameters and body
           for param in &fn_node.params {
               self.declare_cap(&param.name);
           }
           self.check_block(&fn_node.body);
           
           // Ensure terminal linear invariants are checked for this function body
           self.verify_terminal_invariants();
           
           self.pop_scope();
           
           // Restore outer state (or handle inter-procedural flow if required)
           self.current_scope.moved_caps = outer_moved;
           self.cap_to_pipe = outer_pipes;
           
           Ok(())
       }
   }

   Note: Ensure nested closures within fn_node.body continue to share the function-local scope by pushing child scopes rather than re-initializing the function boundary.

   Regression Test Coverage

   Add an integration regression test to compiler/crates/hy-check/tests/liveness_ui.rs validating that helper-first and main-first declaration orders behave identically:

   #[test]
   fn test_capability_identity_isolation_across_functions() {
       let source = r#"
           fn push_three(tx hy.send_cap[int]) {
               for i in 0..3 {
                   tx.send(i)
               }
               tx.close()
           }
   
           fn main() {
               tx, rx := hy.pipe[int]()
               task push_three(move tx)
               for v in rx {
                   fmt.println("{v}")
               }
           }
       "";
       assert_eq!(hy_check::check_str(source).diagnostics.len(), 0);
   }