_attn_exp_hoist_gate.nx source
↩ module page · 44 lines · 2382 B
1// _attn_exp_hoist_gate.nx -- byte-identity gate for SPD-ALG-TENSOR-001 (attention-exp-lut-hoist).
2// Proves the hoisted hot-path _attn_exp_q10_lut(x, lut) returns values BYTE-IDENTICAL to the
3// per-call _attn_exp_q10(x) across the full input range, so moving the LUT build above the
4// softmax / flash-attention loops changes ZERO outputs (only the per-element sys_mmap count:
5// R*C -> 1). NEG control proves teeth. Emits the SPDGATE probe the speed census re_has-matches.
6// Sovereign native lane: exit 0 = GREEN, N = first failed assertion. One build+run (LM-009/010).
7import "nx_syscalls.nx"
8import "nx_attention.nx"
9
10const AEH_LOG: *u8 = "knowledge/status/speed_gate.log"
11
12func gw(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 }
13
14func main() -> i64 {
15 // Build the LUT once (the hoisted form's shared input).
16 let lut: *i64 = (sys_mmap(16 * 8)) as *i64
17 _attn_exp_lut_fill(lut)
18
19 // 1. Full-range byte-identity: the per-call _attn_exp_q10(x) MUST equal the hoisted
20 // _attn_exp_q10_lut(x, lut) for EVERY x in [-7900, 256] -- covers all 16 bins, both
21 // clamps (x>=0 and neg>=7680), the positive path, and every interpolation fraction.
22 var x: nx_int = 0 - 7900
23 while x <= 256 {
24 if _attn_exp_q10(x) != _attn_exp_q10_lut(x, lut) { return 1 }
25 x = x + 1
26 }
27
28 // 2. Anchor values (match nx_attention_test:137-142): exp(0)=1024, far-neg=0, pos clamp=1024.
29 if _attn_exp_q10_lut(0, lut) != 1024 { return 2 }
30 if _attn_exp_q10_lut(0 - 10240, lut) != 0 { return 3 }
31 if _attn_exp_q10_lut(99999, lut) != 1024 { return 4 }
32
33 // 3. NEG control: the function MUST vary with x (a constant-returning impl is caught here).
34 if _attn_exp_q10_lut(0 - 512, lut) == _attn_exp_q10_lut(0 - 2048, lut) { return 5 }
35
36 // GREEN: emit the probe (speed census re_has matches feature=attention-exp-lut-hoist).
37 gw(1, "SPDGATE feature=attention-exp-lut-hoist verdict=GREEN base_mmap=RxC-per-element new=1-per-call hoisted=softmax+flash ||MARK=knowledge/status/speed_gate.log::SPDGATE::verdict=GREEN\n" as *u8)
38 let lf: i64 = sys_openat_append(AEH_LOG, 420)
39 if lf >= 0 {
40 gw(lf, "SPDGATE feature=attention-exp-lut-hoist verdict=GREEN base_mmap=RxC-per-element new=1-per-call hoisted=softmax+flash\n" as *u8)
41 sys_close(lf)
42 }
43 return 0
44}