Skip to content

fix(hy-emit): lower hy.pipe, hy.send_cap, and hy.recv_cap via channel capability prelude (fixes #4464) - #4468

Open
Khanhtnq wants to merge 1 commit into
limitlessprojects:mainfrom
Khanhtnq:fix/hy-emit-pipe-capabilities-4464
Open

Khanhtnq wants to merge 1 commit into
limitlessprojects:mainfrom
Khanhtnq:fix/hy-emit-pipe-capabilities-4464

Conversation

@Khanhtnq

Copy link
Copy Markdown
Contributor

Fixes #4464.

Problem

Programs using linear SPSC channel capabilities (hy.pipe[T], hy.send_cap[T], hy.recv_cap[T]) pass hy-check (Verdict::Accept), but hy-emit previously treated hy.* as an external Go package import (import "hy") with unlowered hy.SendCap / hy.RecvCap / hy.Pipe references, failing go build (package hy is not in std, GUARANTEES Row 13).

Solution

  • SPSC Capability Prelude (PIPE_PRELUDE): Emits generic Go directional channel capability types (hy_send_cap[t any], hy_recv_cap[t any]) with .send(v), .close(), .recv(), .drain(), and hy_pipe[t any](buf ...int) whenever capability pipes/types appear in emitted output, without registering "hy" as a Go import (while preserving unhijacked behavior if a local variable shadows hy).
  • Expression & Type Lowering: Lowers hy.send_cap[T] / hy.recv_cap[T] across parameters, results, locals, and type aliases, and lowers hy.pipe[T](...) / hy.new_pipe[T](...) across both Expr::Index and Expr::Field AST representations.
  • Provenance & Proof Witness Completeness: Propagates BindingKind::Chan and element struct/foreign shapes across :=, =, rx.recv(), and for v in rx range bindings, and records witness_send concurrency witnesses for tx.send(v) under hyb build --emit-proof.

Verification

  • Added 19 end-to-end integration tests in compiler/crates/hy-emit/tests/pipe_capabilities_4464.rs (exact #4464 cap.hy reproducer compiling via go build and outputting 0\n1\n2\n, P01/P07/P08/P10/P12/P13/P15/P16/P17/P20 patterns, struct/slice elements, type aliases, --package mode, --emit-proof witnesses, and cold hyb CLI execution).
  • cargo test --workspace, tools/corpus_harness.py (139/139), tools/check_guarantees.py, and tools/check_conflict_markers.py all pass cleanly.

@github-actions github-actions Bot added the bot:land-candidate Shepherd: fresh, gate-clean, verifiable (set from classify()) label Nov 14, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bot:land-candidate Shepherd: fresh, gate-clean, verifiable (set from classify())

Projects

None yet

1 participant