Exp-2026-10-12 — the fp16 M envelope is a PREDICATE, not a ceiling

Board 10.3.0.235 (Radxa ROCK 5B+, 6.1.115-vendor-rk35xx-fix). Shipped 7b2db23, make test ALL PASS, attest refreshed.

★ This started as a performance question and turned out to be a correctness bug on the main fp16 path, at exactly attention's shape. 54 of 126 swept cells were returning wrong answers with no error and no decline.

The probe

tools/re/f16_stream_envelope_probe.c — a (K, N, M) sweep, every cell graded against a CPU fp32 reference and reported as a pass rate over 6 reps, scanned upward at every M (never bisected; the envelope is non-monotone). 126 cells.

The rule, which reproduces every cell

The failure is entirely determined by the 0x1040 value the program emits:

12 CBUF banks x 32 KB.   0x1040 = WEIGHT_BANK[7:4] | DATA_BANK[3:0]

activations occupy banks [0, dreq);  the WEIGHT WINDOW STARTS AT BANK DATA_BANK
and runs min(wreq, WEIGHT_BANK) banks, wrapping into the activations past bank 11.

CORRECT  iff   dreq <= DATA_BANK   AND   DATA_BANK + min(wreq, WEIGHT_BANK) <= 12

At every well-formed K the encoding keeps DATA_BANK + WEIGHT_BANK == 12 exactly — 0xb1 at K=256 and at the sched=0 default, 0xa2 @512, 0x84 @1024, 0x48 @2048, 0x1b at the floor — so the second clause is free and the model reduces to the banks × 32 KB cap already in the tree. Confirmed 18/18 PASS at K=256 N=1024; nothing changes at K=256/512/1024/2048.

K=128 is the sole exception. It needs half-bank steps (slope = (int)7.5 = 7) that the encoding cannot express, and its base is 0xb8 = D8/W11 — sum 19, not 12. Measured boundaries, each by upward scan with 0/6 on the far side:

group	0x1040	correct while	at K=128
mg=1 (mc≤64)	0xb8 D8/W11	wreq ≤ 4	N ≤ 512
mg=2 (mc≤128)	0xb1 D1/W11	always	every N
mg=3 (mc≤192)	0xaa D10/W10	wreq ≤ 2	N ≤ 256
mg=4 (mc≤256)	0xa3 D3/W10	wreq ≤ 9	N ≤ 1152

★★ Four things this contradicts, including one that was believed all day

1. ork_f16_mm_run — the MAIN fp16 path — is NOT correct throughout. At K=128 N=2048 M=64 it reads max|diff| 5.12 against |C|max 2.17; M=32 N=2048 → 3.39; M=64 N=3584 → 2.05. It looked correct only because its per-core column split happened to shrink Ncore below the boundary at the N values anyone had tried. This is attention's exact shape — K = head_dim = 128, N = n_kv — so the main path was silently wrong there, not merely the stream pair.
2. The chain was not "correct at N=1024". It is correct only at certain M: M=16–64 FAIL, 80–128 PASS, 144–192 FAIL, 224–256 PASS, 288–320 FAIL, 384 PASS, 448 FAIL, 512 PASS. Perfectly explained by the model — 288 = 256+32, and the 32-row remainder tile is illegal.
3. "K=128 has a measured contiguous prefix of 256" holds only at N ≤ 256. At N ≥ 1024 the usable set is a hole, not a prefix.
4. ork_f16_mm_run_stream's ~100× slowness is not K=128-specific. At K=256 N=1024 M=512 it is correct and still 538 ms against the chain's 4.5 ms. A separate, unfixed defect in the fp16 doorbell path — and the reason declining those shapes costs nothing.

What shipped

orki_f16_mc_ok(K, N, sched, mc) — the predicate. orki_f16_mcap_n now returns the largest legal tile; orki_f16_mtile_n returns the largest tile whose remainder is also legal (0 = do not partition).

Callers differ by what they can actually do about it, which is the part worth copying:

• orki_run PADS. A and C go through its own Af/Cc scratch, so a short last tile is computed at the next legal height and the extra rows are never gathered or read back (orki_f16_mcpad). This keeps ork_f16_mm_run runnable at every M.
• colsplit threads the round's widest per-core N (h->f16_ncmax) through both of its program-count sites — legality is monotone decreasing in N, so one number is right for every core.
• The stream pair indexes the caller's buffers and cannot pad, so it picks a legal tile+remainder and refuses (-2) when none exists.
• core/dyn.c's fp16 gate asks the predicate about the actual program height, using the sched that path synthesises with.

Evidence

	before	after
envelope cells	54 of 126 = 0/6 FAIL (`max	diff

★ The chain's usable region GREW. At K=128 N=1024 and N=2048 it now passes at every M ≥ 80, including 144/160/192/288/320/448, which were wrong before. The refused set is exactly M ≤ 64 at K=128 with N > 512, where no legal program height exists — and where both stream arms were wrong anyway.

The performance lever survives: H=4 K=128 N=1024 M=512 chain = 1.48× over per-head, bit-exact (N=2048: 1.09×).

The cost, stated plainly: K=128 N=2048 M=64 goes 66.1 → 35.3 GMAC/s. A 2×-tall program buys the correct answer.

Regression: examples/test_f16_narrow_n.c (already in make test) gains 8 ork_f16_mm_run cases at K=128 and a new stream_case() with 5 cases over both stream entrypoints, bar = bit-exact OR refused. The existing positive control still FAILs as required.

Open

1. ork_f16_mm_run_stream is ~100× slower than the chain at every K, correct or not (538 ms vs 4.5 ms for 4×[512,256]×[256,1024]). Separate defect in the fp16 doorbell path.
2. The stream pair could PAD like orki_run does and recover the refused M ≤ 64 at K=128 N>512, but it indexes the caller's A/C directly, so that needs staging changes.
3. Why DATA_BANK + WEIGHT_BANK == 13 works at all (K=128 mg=4 = D3/W10) when the CBUF has 12 banks. The predicate D + wuse <= 12 fits 126/126 cells, so the model is right about use; the allocation arithmetic is one bank looser than the physical count and that is unexplained.

The generalisable lesson

An envelope expressed as a ceiling (mcap) cannot describe a rule with a hole in it, and a caller that only knows a ceiling cannot decline what it cannot compute. Expressing it as a predicate let three callers respond differently according to what each is able to do — pad, narrow, or refuse — and that is what both fixed the correctness bug and widened the usable region at the same time.