[soundness] generic struct type-argument erasure in hy-check bypasses Tier-0 alias freeze (HYB-E3003), non-owned move (HYB-E3004), const deep immutability (HYB-E3006), closure/handle move perimeter (HYB-E3001/E3002), A3 slot loans (HYB-E3102), and N1/N3 (HYB-E4001/E4002) #772

The smallest .hy program that demonstrates it

Repro 1 — Tier-0 shallow-copy alias freeze bypass (HYB-E3003, O5.2) -> go test -race DATA RACE

struct box[t] {
    v t
}

fn worker(b box[map[string]int], done chan<- bool) {
    for i in 0..1000 {
        b.v["k"] = i
    }
    done <- true
}

fn main() {
    done := make(chan bool, 1)
    b1 := box[map[string]int]{v: map[string]int{"k": 0}}
    b2 := b1
    task worker(move b1, done)
    for i in 0..1000 {
        b2.v["k"] = i + 1
    }
    <-done
}

Repro 2 — Non-owned parameter/capture move bypass (HYB-E3004, O5.1) -> go test -race DATA RACE

struct box[t] {
    v t
}

fn worker(b box[map[string]int], done chan<- bool) {
    for i in 0..1000 {
        b.v["k"] = i
    }
    done <- true
}

fn leak(p box[map[string]int], done chan<- bool) {
    b := p
    task worker(move b, done)
}

fn main() {
    done := make(chan bool, 1)
    orig := box[map[string]int]{v: map[string]int{"k": 0}}
    leak(orig, done)
    for i in 0..1000 {
        orig.v["k"] = i + 1
    }
    <-done
}

Repro 3 — const deep-immutability bypass (HYB-E3006, T22) -> go test -race DATA RACE

struct box[t] {
    v t
}

const shared_box = box[map[string]int]{v: map[string]int{"k": 0}}

fn writer(done chan<- bool) {
    c := shared_box
    for i in 0..1000 {
        c.v["k"] = i
    }
    done <- true
}

fn main() {
    d1 := make(chan bool, 1)
    d2 := make(chan bool, 1)
    task writer(d1)
    task writer(d2)
    <-d1
    <-d2
}

Repro 4 — Closure / BorrowHandle / Mutex move perimeter bypass (HYB-E3001 / HYB-E3002, A5 / O7 / O11) -> go test -race DATA RACE

struct box[t] {
    v t
}

fn run_box(b box[fn()], done chan<- bool) {
    for i in 0..1000 {
        b.v()
    }
    done <- true
}

fn main() {
    done := make(chan bool, 1)
    m := map[string]int{"k": 0}
    b := box[fn()]{v: fn() { m["k"] = m["k"] + 1 }}
    task run_box(move b, done)
    for i in 0..1000 {
        m["k"] = i
    }
    <-done
}

Repro 5 — A3 map-slot loan invalidation bypass (HYB-E3102, O8) & N1/N3 (HYB-E4001 / HYB-E4002)

import "fmt"

struct box[t] {
    v t
}

enum msg {
    data(int)
    quit
}

fn main() {
    m := map[string]int{"a": 1}
    b := box[map[string]int]{v: m}
    p := &b.v["a"]
    delete(m, "a")
    fmt.println(p)

    nil_box := box[map[string]int]{v: nil}
    var uninit_box box[msg]
    _ = nil_box
    _ = uninit_box
}

Negative Control (must continue to be accepted with 0 diagnostics)

struct box[t] {
    v t
}

fn worker(b box[int], done chan<- int) {
    done <- b.v + 1
}

fn main() {
    done := make(chan int, 1)
    b1 := box[int]{v: 41}
    b2 := b1
    task worker(move b1, done)
    b2.v = 99
    _ = <-done
}

What the checker should say

• Repro 1: Reject with HYB-E3003 (b2 shares reference storage with moved b1 via generic field v: map[string]int, so b2.v["k"] = ... is a post-move use of a frozen shallow-copy peer).
• Repro 2: Reject with HYB-E3004 (b := p copies reference-bearing parameter p: box[map[string]int], which is not owned by leak and cannot be moved into task worker).
• Repro 3: Reject with HYB-E3006 (c := shared_box shares reference storage with const shared_box, so c.v["k"] = i writes through a const).
• Repro 4: Reject with HYB-E3001 (box[fn()] holds a closure at field .v; closures are never sendable even with move).
• Repro 5: Reject with HYB-E3102 (delete(m, "a") while map-slot loan p := &b.v["a"] is live), HYB-E4001 (nil initializer for v: map[string]int), and HYB-E4002 (uninitialized var uninit_box box[msg] whose payload-first enum msg has no zero value).
• Negative Control: Accept (box[int] is a pure value-copy struct with no reference/closure/handle fields).

What it actually said

hyb check accepts all five repros with 0 diagnostics (Verdict::Accept), and go test -race on the emitted Go reports concurrent map read/write panics and data races for Repros 1–4.

Claimed severity

P0 — Soundness bug (hyb check accepts a race / UB / invalid state that GUARANTEES.md rows O4, O5.1, O5.2, O7, O8, O11, A3, A5, T22, N1, and N3 promise to reject).

Anything else

Root Cause in compiler/crates/hy-check/src/:

1. Checker::named_shape_depth (shape.rs:80-84) strips generic type arguments via Self::base_named_type_str(name) and returns TypeShape::Struct(Some("box")) for box[map[string]int], erasing the concrete type argument map[string]int.
2. In self.structs.get("box"), field v has the raw type parameter TypeExpr::Named { name: "t" }, whose shape_of_type is TypeShape::Unknown.
3. Although sendability.rs:2228-2341 already defines parse_generic_type_args, substitute_type_params, and struct_fields_for_type (used only for channel-direction checking), none of the core shape/aliasing/sendability/loan/immutability/nil/zero-value queries substitute concrete type arguments into generic struct fields or generic call returns:
   • shape_may_share_at (shape.rs:132-140) sees TypeShape::Unknown for field v and returns false! Thus shape_may_share and binding_may_share return false for box[map[string]int], box[[]int], box[*int], etc., completely disabling record_storage_from_snapshot (may-share edges, non_owned_origin propagation, const share-group linking) and const_arg_root.
   • field_shape (shape.rs:301-312) and ty_of_expr for Expr::Field (shape.rs:643-648) return TypeShape::Unknown and Some(Named("t")) for b.v, breaking A3 map-slot loan detection on &b.v["a"] and non-owned field projection (m := p.v; move m).
   • shape_carries_handle_at (shape.rs:171-179), shape_holds_closure (sendability.rs:166-177), shape_holds_unmovable_leaf (sendability.rs:198-209), shape_is_const_sendable (sendability.rs:225-236), struct_has_mutex_field (sendability.rs:583-609), check_composite_nils (sendability.rs:978-1033), and no_zero_value_reason (shape.rs:828-845) all inspect raw un-substituted field types in self.structs.