nx_nofloat_softmax_gate.nx source
↩ module page · 107 lines · 6388 B
1// nx_nofloat_softmax_gate.nx -- a SYSTEM for the HARD no-float primitive: fixed-point exp + softmax.
2// Transformers / attention (LLM + coding-LLM) need softmax = exp(x)/sum(exp) -- but exp is a transcendental,
3// and float exp is NON-DETERMINISTIC. This builds it from the hardware rung up in pure INTEGER Q16:
4// exp(x) = 2^(x*log2 e); split x*log2e into integer + fraction; 2^int = bit-shift; 2^frac = a small
5// minimax-tuned integer Horner polynomial (endpoints pinned exact). Every op is integer -> BIT-EXACT
6// DETERMINISTIC (the no-float exceed [[nx_nofloat_exceed_gate]]). Accuracy is verified SELF-CONSISTENTLY
7// (no float oracle): exp(0)=1, exp(-ln2)=1/2, exp(-2ln2)=1/4, and the functional equation exp(a)exp(b)=
8// exp(a+b). Softmax determinism: forward-sum == reverse-sum, bit-identical (float cannot promise this).
9// This is the reusable approach for fixed-point transcendentals -> unlocks no-float attention/transformers.
10// No hw writes (Rule 26). expect_exit: 0 license_tier: ORIGINAL
11import "nx_syscalls.nx"
12import "nx_gate_verdict.nx"
13
14// Q16 constants
15const Q1: i64 = 65536 // 1.0
16const LOG2E: i64 = 94548 // log2(e) = 1.4426950
17const PC0: i64 = 65536 // 2^f Horner: pinned so 2^0=1, 2^1=2 exact
18const PC1: i64 = 45426
19const PC2: i64 = 15743
20const PC3: i64 = 4367
21const LN2: i64 = 45426 // ln(2) = 0.6931472
22
23func sm_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
24func sm_num(v: i64) -> i64 { let b: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(1,"-" as *u8,1)} let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 }
25func absd(a: i64, b: i64) -> i64 { if a>b { return a-b } return b-a }
26
27// fixed-point exp for x <= 0 (Q16) -> exp(x) in Q16, (0, 65536]. Pure integer => deterministic.
28func fx_exp(x: i64) -> i64 {
29 var xm: i64 = 0 - x // |x|, >= 0 (x>0 clamped below)
30 if x > 0 { xm = 0 }
31 let ym: i64 = (xm * LOG2E) >> 16 // |x|*log2(e), Q16, >= 0
32 let yi: i64 = ym >> 16 // integer part of |y|
33 let yf: i64 = ym - (yi << 16) // fraction [0,65536)
34 let g: i64 = Q1 - yf // 1-frac, (0,65536]
35 var t: i64 = PC3
36 t = PC2 + ((g * t) >> 16)
37 t = PC1 + ((g * t) >> 16)
38 t = PC0 + ((g * t) >> 16) // 2^g in Q16 [65536,131072]
39 t = t >> 1 // 2^(-frac) = 2^g / 2
40 if yi >= 31 { return 0 } // underflow -> 0
41 return t >> yi // * 2^(-int)
42}
43
44// fixed-point softmax (Q16). rev=0 sum forward, rev=1 sum reverse -> outputs MUST match (determinism).
45func fx_softmax(x: *i64, out: *i64, e: *i64, n: i64, rev: i64) -> i64 {
46 var m: i64 = x[0]
47 var i: i64 = 1
48 while i<n { if x[i]>m { m=x[i] } i=i+1 }
49 i=0
50 while i<n { e[i] = fx_exp(x[i]-m); i=i+1 }
51 var s: i64 = 0
52 if rev==0 { i=0; while i<n { s=s+e[i]; i=i+1 } } else { i=n-1; while i>=0 { s=s+e[i]; i=i-1 } }
53 if s<=0 { s=1 }
54 i=0
55 while i<n { out[i] = (e[i]<<16)/s; i=i+1 }
56 return s
57}
58
59func main() -> i64 {
60 sm_puts("SYSTEM for a HARD no-float primitive: fixed-point exp + softmax (deterministic transcendentals)\n\n" as *u8)
61 let TOL: i64 = 1200 // ~1.8% of Q16 -- 3rd-order poly accuracy, honest
62
63 let e0: i64 = fx_exp(0)
64 let eh: i64 = fx_exp(0 - LN2) // exp(-ln2) = 1/2
65 let eq: i64 = fx_exp(0 - 2*LN2) // exp(-2ln2) = 1/4
66 let prod: i64 = (eh * eh) >> 16 // exp(-ln2)^2 should == exp(-2ln2)
67
68 sm_puts(" exp(0) = "); sm_num(e0); sm_puts(" (want 65536 = 1.0)\n");
69 sm_puts(" exp(-ln2) = "); sm_num(eh); sm_puts(" (want 32768 = 0.5)\n");
70 sm_puts(" exp(-2ln2)= "); sm_num(eq); sm_puts(" (want 16384 = 0.25)\n");
71 sm_puts(" exp(-ln2)^2 = "); sm_num(prod); sm_puts(" (functional eq: should == exp(-2ln2))\n\n");
72
73 // softmax on a test vector (Q16 logits)
74 let n: i64 = 6
75 let x: *i64 = sys_mmap(n*8) as *i64
76 x[0]=0; x[1]=65536; x[2]=131072; x[3]=0-65536; x[4]=32768; x[5]=98304 // 0,1,2,-1,0.5,1.5
77 let ef: *i64 = sys_mmap(n*8) as *i64
78 let of: *i64 = sys_mmap(n*8) as *i64
79 let orr: *i64 = sys_mmap(n*8) as *i64
80 fx_softmax(x, of, ef, n, 0) // forward sum
81 fx_softmax(x, orr, ef, n, 1) // reverse sum
82 var osum: i64 = 0
83 var detmis: i64 = 0
84 var i: i64 = 0
85 while i<n { osum=osum+of[i]; if of[i]!=orr[i] { detmis=detmis+1 } i=i+1 }
86
87 sm_puts(" softmax(0,1,2,-1,0.5,1.5) Q16: ["); i=0; while i<n { sm_num(of[i]); if i<n-1 { sm_puts(", ") } i=i+1 } sm_puts("]\n");
88 sm_puts(" sum of outputs = "); sm_num(osum); sm_puts(" (want ~65536 = 1.0) determinism mism (fwd vs rev) = "); sm_num(detmis); sm_puts("\n\n");
89
90 var pass: i64=0
91 var ttl: i64=0
92 ttl=ttl+1; sm_puts(" T1 exp(0) EXACT == 1.0 (65536): "); if e0==65536 { pass=pass+1; sm_puts("PASS\n") } else { sm_puts("FAIL\n") }
93 ttl=ttl+1; sm_puts(" T2 exp(-ln2) ~ 0.5 and exp(-2ln2) ~ 0.25 (self-consistent known values): "); if absd(eh,32768)<=TOL { if absd(eq,16384)<=TOL { pass=pass+1; sm_puts("PASS\n") } else { sm_puts("FAIL\n") } } else { sm_puts("FAIL\n") }
94 ttl=ttl+1; sm_puts(" T3 FUNCTIONAL EQ exp(-ln2)^2 == exp(-2ln2) (proves it is truly exponential): "); if absd(prod,eq)<=TOL { pass=pass+1; sm_puts("PASS\n") } else { sm_puts("FAIL\n") }
95 ttl=ttl+1; sm_puts(" T4 softmax sums to ~1.0 AND is DETERMINISTIC (fwd-sum == rev-sum, 0 mism): "); if absd(osum,65536)<=TOL { if detmis==0 { pass=pass+1; sm_puts("PASS\n") } else { sm_puts("FAIL\n") } } else { sm_puts("FAIL\n") }
96
97 sm_puts("NX-NOFLOAT-SOFTMAX-GATE passed "); sm_num(pass); sm_puts("/"); sm_num(ttl)
98 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
99 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
100 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
101 let ctr__dry: *i64 = gv_ctr()
102 ctr__dry[0] = pass
103 ctr__dry[1] = ttl
104 let rc__dry: i64 = gv_verdict("NOFLOAT-SOFTMAX-GATE" as *u8, ctr__dry, "deterministic fixed-point exp+softmax -- the no-float transcendental SYSTEM for attention/transformers)" as *u8)
105 sys_exit(rc__dry)
106 return rc__dry
107}