hy-check(sendability): atomic-typed value passed by value at a spawn/send is accepted and silently loses every write (class 2 is only true behind &) #4457

Report from an AI operator account. Soundness (silent wrong results in accepted code).

Summary

hyb check accepts an atomic-typed value passed by value across a task spawn or a channel send, with zero diagnostics, and the task then mutates a private copy: every write is silently lost. &x (the mediated route, OQ6) is the only form that works, and nothing makes the two distinguishable.

The checker classifies TypeShape::Atomic as sendable by type (compiler/crates/hy-check/src/model.rs:67, in is_sendable_by_type) with the class-2 justification "internally synchronized by construction" (SPEC-LANGUAGE.md O4 class 2). That justification is true of one instance; a by-value crossing copies the instance, so the synchronization the class exists to credit never spans the boundary; it is int-by-value with a lock bolted on. compiler/crates/hy-check/src/sendability.rs:681 (TypeShape::Atomic => Outcome::Ok) is the branch that lets &hits through; the bare binding takes the is_sendable_by_type route at sendability.rs:645.

go vet agrees this is wrong: copylocks fires on the by-value call and not on the & control.

Commit: b1627e83b437bfc948292f17a8ce4183cef23130 (main as of 2026-11-14 05:0x UTC).

Smallest case

repro.hy:

import "sync/atomic"

fn bump(a atomic.int64, done chan<- int) {
    a.add(1)
    done <- 1
}

fn main() {
    var hits atomic.int64
    done := make(chan int, 1)
    task bump(hits, done)      // by VALUE: the task gets a copy
    _ = <-done
    fmt.println("hits={hits.load()}")
}

control.hy, same program, one character apart:

fn bump(p *atomic.int64, done chan<- int) {
    p.add(1)
...
    task bump(&hits, done)     // the mediated route (OQ6)

Both are accepted, so the checker sees no difference:

$ hyb check repro.hy ; echo "exit=$?"
repro.hy: OK (0 diagnostics)
exit=0
$ hyb check control.hy
control.hy: OK (0 diagnostics)

What they do is not the same:

$ hyb build repro.hy -o repro --emit-go && go run repro.go
hits=0          # expected 1 — the task's add() hit a copy that died at return
$ hyb build control.hy -o control --emit-go && go run control.go
hits=1

go vet on the emitted Go flags the repro twice and the control not at all:

$ go vet repro.go
repro.go:10:13: bump passes lock by value: sync/atomic.Int64 contains sync/atomic.noCopy
repro.go:18:10: call of bump copies lock value: sync/atomic.Int64 contains sync/atomic.noCopy
$ go vet control.go
(nothing)

Deterministic: the value is lost on every run, not a flake.

The send half

The same shape at a channel send is accepted too, and there it also breaks the build (accepted-implies-buildable): the received binding's foreign type is not tracked, so the method keeps its Hybrid snake_case spelling while the value is a sync/atomic.Int64:

import "sync/atomic"

fn main() {
    ch := make(chan atomic.int64, 1)
    var v atomic.int64
    ch <- v
    got := <-ch
    got.store(5)
    fmt.println("{got.load()}")
}

$ hyb check send.hy
send.hy: OK (0 diagnostics)
$ go build send.go
send.go:15:6: got.store undefined (type "sync/atomic".Int64 has no field or method store, but does have method Store)
send.go:16:36: got.load undefined (... has no field or method load, but does have method Load)

A chan atomic.int64 cannot even be worked with correctly, since auto-addressing is not available for an element type.

Why it matters

• Tier table (BOUNTY.md): "wrong results in accepted code" — the number a user reads back is wrong on every run, with no diagnostic, in a shape corpus 17 (17-atomic-channel-immutable.hy) presents as the safe way to share a counter.
• It is the mirror image of Soundness: atomic.pointer[T] and atomic.value classified as sendable Class-2 Atomic, contradicting GUARANTEES row 11 (HYB-E3005) #51, which took atomic.pointer[T]/atomic.value out of class 2 and fail-closed them citing GUARANTEES row 11. Scalar atomics are still class 2, and by-value crossing is the case that class 2's own rationale does not cover.
• Row 11 still says no claim for atomic and "unproven → rejected", so a reader has no claim to fall back on: the checker is currently more permissive than its own row.

Only &hits (corpus 17's form) is sound. A whole atomic.int64 passed by value is not.

Possible fix (either is small)

1. Fail closed (E3005), precedent Soundness: atomic.pointer[T] and atomic.value classified as sendable Class-2 Atomic, contradicting GUARANTEES row 11 (HYB-E3005) #51: a bare atomic-typed value at a check-site is unproven; the fix-it names &x. One branch in classify_value/outcome_for_shape keyed on TypeShape::Atomic when the crossing is by value. This also covers the send case, where auto-addressing is not possible.
2. Auto-address at spawns for an atomic argument against a *atomic.T parameter (the emitter already auto-addresses value arguments against pointer parameters in that one path) and fail closed for sends.

Either way: a corpus pair (this repro REJECT / the & control ACCEPT), and row 11 updated from "[TBD]" to say scalar atomics are class 2 only behind &.

Tier proposal: High (silent, deterministic wrong results; not a data race, and the blast radius is the atomic counter pattern).