nx_nofloat_rope_gate.nx source

1// nx_nofloat_rope_gate.nx -- HARD-EVIDENCE gate for RoPE (rotary position embedding) backward + RoPE composed 2// into the attention path. Advances CAP-NF-ATTN-FULL: with RoPE the attention is positionally-aware AND still 3// fully differentiable in pure integer Q16. RoPE is parameter-free (orthogonal rotation), so its backward is 4// the inverse rotation -- here proven correct by finite differences AND inside the full attention block. 5// 6// A1 RoPE gradcheck : loss=mse(RoPE(x), t); tape grad dL/dx == central finite difference. 7// A2 attention+RoPE gradcheck: X->{Q,K,V}; RoPE(Q),RoPE(K); S=QK^T; scale; causal softmax; O=A.V; mse; 8// gradcheck dL/dWq -- the gradient flowing through RoPE + softmax + both matmuls (the real RoPE-attn backward). 9// D neg-control teeth : a wrong RoPE grad is rejected. 10// C bit-exact : the attention+RoPE gradient is identical across two runs (determinism). 11// 12// Evidence -> knowledge/status/nofloat_rope.log. Sovereign: imports nx_nofloat_autograd (pure integer) + nx_syscalls. 13// HONEST scope: single-head; output-projection + multi-head/GQA remain (bookkeeping over matmul+vadd). expect_exit: 0 14import "nx_nofloat_autograd.nx" 15import "nx_syscalls.nx" 16import "nx_gate_emit_lib.nx" 17 18const RLOG: *u8 = "knowledge/status/nofloat_rope.log" 19const Q16: i64 = 65536 20 21 22func g_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v } 23func r_ws(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 } 24func r_wn(fd: i64, v: i64) -> i64 { let b: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(fd,"-" as *u8,1);m=0-m} let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48;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(fd,b,k); return 0 } 25 26// ---- A1: RoPE gradcheck (loss = mse(RoPE(x), target)) ---- 27func rope_loss(tape: *i64, vals: *i64, st: *i64, Xs: *i64, T: i64, hd: i64, Ts: *i64, leaves: *i64) -> i64 { 28 st[0]=0; st[1]=0 29 let nX: i64 = nfa_leaf(tape,vals,st,T,hd,Xs,0) 30 let nR: i64 = nfa_rope(tape,vals,st,nX) 31 let nt: i64 = nfa_leaf(tape,vals,st,T,hd,Ts,0) 32 let loss: i64 = nfa_mse(tape,vals,st,nR,nt) 33 leaves[0]=nX 34 return loss 35} 36func rope_lossval(tape: *i64, vals: *i64, st: *i64, Xs: *i64, T: i64, hd: i64, Ts: *i64) -> i64 { 37 let lv: *i64 = sys_mmap(8) as *i64 38 let loss: i64 = rope_loss(tape,vals,st,Xs,T,hd,Ts,lv) 39 return nfa_val(tape,vals,loss,0) 40} 41 42// ---- A2: attention + RoPE forward (leaves[0..3]=nWq,nWk,nWv,nX) -> O node ---- 43func ar_fwd(tape: *i64, vals: *i64, st: *i64, Xs: *i64, Wqs: *i64, Wks: *i64, Wvs: *i64, T: i64, d: i64, scale: i64, leaves: *i64) -> i64 { 44 st[0]=0; st[1]=0 45 let nX: i64 = nfa_leaf(tape,vals,st,T,d,Xs,0) 46 let nWq: i64 = nfa_leaf(tape,vals,st,d,d,Wqs,0) 47 let nWk: i64 = nfa_leaf(tape,vals,st,d,d,Wks,0) 48 let nWv: i64 = nfa_leaf(tape,vals,st,d,d,Wvs,0) 49 let nQ: i64 = nfa_matmul(tape,vals,st,nX,nWq) 50 let nK: i64 = nfa_matmul(tape,vals,st,nX,nWk) 51 let nV: i64 = nfa_matmul(tape,vals,st,nX,nWv) 52 let nQr: i64 = nfa_rope(tape,vals,st,nQ) 53 let nKr: i64 = nfa_rope(tape,vals,st,nK) 54 let nS: i64 = nfa_matmul_nt(tape,vals,st,nQr,nKr) 55 let nSs: i64 = nfa_cmul(tape,vals,st,nS,scale) 56 let nA: i64 = nfa_softmax_rows(tape,vals,st,nSs,1) 57 let nO: i64 = nfa_matmul(tape,vals,st,nA,nV) 58 leaves[0]=nWq; leaves[1]=nWk; leaves[2]=nWv; leaves[3]=nX 59 return nO 60} 61func ar_loss(tape: *i64, vals: *i64, st: *i64, Xs: *i64, Wqs: *i64, Wks: *i64, Wvs: *i64, Ts: *i64, T: i64, d: i64, scale: i64, leaves: *i64) -> i64 { 62 let nO: i64 = ar_fwd(tape,vals,st,Xs,Wqs,Wks,Wvs,T,d,scale,leaves) 63 let nt: i64 = nfa_leaf(tape,vals,st,T,d,Ts,0) 64 return nfa_mse(tape,vals,st,nO,nt) 65} 66func ar_lossval(tape: *i64, vals: *i64, st: *i64, Xs: *i64, Wqs: *i64, Wks: *i64, Wvs: *i64, Ts: *i64, T: i64, d: i64, scale: i64) -> i64 { 67 let lv: *i64 = sys_mmap(4*8) as *i64 68 let loss: i64 = ar_loss(tape,vals,st,Xs,Wqs,Wks,Wvs,Ts,T,d,scale,lv) 69 return nfa_val(tape,vals,loss,0) 70} 71 72func main() -> i64 { 73 g_puts("nx_nofloat_rope gate (RoPE backward + RoPE-in-attention, PURE INTEGER Q16 -- MEASURED)\n" as *u8) 74 var pass: i64=0; var total: i64=0 75 let tape: *i64 = sys_mmap(512*7*8) as *i64 76 let vals: *i64 = sys_mmap(8192*8) as *i64 77 let grads: *i64 = sys_mmap(8192*8) as *i64 78 let st: *i64 = sys_mmap(2*8) as *i64 79 let h: i64 = 512 80 let floor_q: i64 = 4096 81 82 // ---- A1: RoPE gradcheck ---- 83 let T: i64 = 3; let hd: i64 = 2 84 let Xs: *i64 = sys_mmap(T*hd*8) as *i64; Xs[0]=32768; Xs[1]=49152; Xs[2]=0-16384; Xs[3]=65536; Xs[4]=24576; Xs[5]=0-40960 85 let Ts: *i64 = sys_mmap(T*hd*8) as *i64; Ts[0]=13107; Ts[1]=0-6554; Ts[2]=19661; Ts[3]=6554; Ts[4]=0-26214; Ts[5]=32768 86 let lv: *i64 = sys_mmap(8) as *i64 87 let loss1: i64 = rope_loss(tape,vals,st,Xs,T,hd,Ts,lv) 88 nfa_backward(tape,vals,grads,st[0],loss1) 89 let nX: i64 = lv[0] 90 var r1_ok: i64 = 1; var r1_worst: i64 = 0 91 var pi: i64 = 0 92 while pi < T*hd { 93 let ana: i64 = nfa_grad(tape,grads,nX,pi) 94 let xp: *i64 = sys_mmap(T*hd*8) as *i64 95 let xm: *i64 = sys_mmap(T*hd*8) as *i64 96 var z: i64=0 97 while z<T*hd { xp[z]=Xs[z]; xm[z]=Xs[z]; z=z+1 } 98 xp[pi]=Xs[pi]+h; xm[pi]=Xs[pi]-h 99 let lp: i64 = rope_lossval(tape,vals,st,xp,T,hd,Ts) 100 let lm: i64 = rope_lossval(tape,vals,st,xm,T,hd,Ts) 101 let fd: i64 = ((lp-lm)*Q16)/(2*h) 102 let num: i64 = g_abs(fd-ana) 103 var den: i64 = g_abs(ana); if den<floor_q { den=floor_q } 104 if num >= ((4096*den)>>16) { r1_ok=0 } // tol 1/16 105 let rel: i64 = (num*1000)/den 106 if rel>r1_worst { r1_worst=rel } 107 pi=pi+1 108 } 109 g_puts(" [measure] RoPE worst rel grad err = " as *u8); g_pn(r1_worst); g_puts(" /1000 (tol=62)\n" as *u8) 110 pass=pass+g_check("A1: RoPE gradcheck -- rotation backward (rotate by -angle) == finite differences" as *u8, r1_ok); total=total+1 111 112 // ---- A2: attention + RoPE gradcheck wrt Wq ---- 113 let d: i64 = 2; let scale: i64 = 46341 114 let aX: *i64 = sys_mmap(T*d*8) as *i64; aX[0]=32768; aX[1]=16384; aX[2]=0-16384; aX[3]=49152; aX[4]=65536; aX[5]=0-32768 115 let Wq: *i64 = sys_mmap(d*d*8) as *i64; Wq[0]=49152; Wq[1]=0-16384; Wq[2]=32768; Wq[3]=65536 116 let Wk: *i64 = sys_mmap(d*d*8) as *i64; Wk[0]=16384; Wk[1]=32768; Wk[2]=0-32768; Wk[3]=49152 117 let Wv: *i64 = sys_mmap(d*d*8) as *i64; Wv[0]=65536; Wv[1]=0-32768; Wv[2]=16384; Wv[3]=49152 118 let aT: *i64 = sys_mmap(T*d*8) as *i64; aT[0]=13107; aT[1]=0-6554; aT[2]=19661; aT[3]=6554; aT[4]=0-13107; aT[5]=26214 119 let lv2: *i64 = sys_mmap(4*8) as *i64 120 let loss2: i64 = ar_loss(tape,vals,st,aX,Wq,Wk,Wv,aT,T,d,scale,lv2) 121 nfa_backward(tape,vals,grads,st[0],loss2) 122 let nWq: i64 = lv2[0] 123 var r2_ok: i64 = 1; var r2_worst: i64 = 0 124 var qi: i64 = 0 125 while qi < d*d { 126 let ana: i64 = nfa_grad(tape,grads,nWq,qi) 127 let wqp: *i64 = sys_mmap(d*d*8) as *i64 128 let wqm: *i64 = sys_mmap(d*d*8) as *i64 129 var z: i64=0 130 while z<d*d { wqp[z]=Wq[z]; wqm[z]=Wq[z]; z=z+1 } 131 wqp[qi]=Wq[qi]+h; wqm[qi]=Wq[qi]-h 132 let lp: i64 = ar_lossval(tape,vals,st,aX,wqp,Wk,Wv,aT,T,d,scale) 133 let lm: i64 = ar_lossval(tape,vals,st,aX,wqm,Wk,Wv,aT,T,d,scale) 134 let fd: i64 = ((lp-lm)*Q16)/(2*h) 135 let num: i64 = g_abs(fd-ana) 136 var den: i64 = g_abs(ana); if den<floor_q { den=floor_q } 137 if num >= ((8192*den)>>16) { r2_ok=0 } // tol 1/8 (long chain through RoPE+softmax) 138 let rel: i64 = (num*1000)/den 139 if rel>r2_worst { r2_worst=rel } 140 qi=qi+1 141 } 142 g_puts(" [measure] attention+RoPE dL/dWq worst rel grad err = " as *u8); g_pn(r2_worst); g_puts(" /1000 (tol=125)\n" as *u8) 143 pass=pass+g_check("A2: attention+RoPE gradcheck -- dL/dWq through RoPE + causal-softmax + QK^T + A.V == finite diff" as *u8, r2_ok); total=total+1 144 145 // ---- D: neg-control teeth (RoPE) ---- 146 let lossd: i64 = rope_loss(tape,vals,st,Xs,T,hd,Ts,lv) 147 nfa_backward(tape,vals,grads,st[0],lossd) 148 let rana0: i64 = nfa_grad(tape,grads,lv[0],0) 149 let xp0: *i64 = sys_mmap(T*hd*8) as *i64 150 let xm0: *i64 = sys_mmap(T*hd*8) as *i64 151 var z0: i64=0 152 while z0<T*hd { xp0[z0]=Xs[z0]; xm0[z0]=Xs[z0]; z0=z0+1 } 153 xp0[0]=Xs[0]+h; xm0[0]=Xs[0]-h 154 let fdr0: i64 = ((rope_lossval(tape,vals,st,xp0,T,hd,Ts) - rope_lossval(tape,vals,st,xm0,T,hd,Ts))*Q16)/(2*h) 155 let bad: i64 = 0 - rana0 156 var rden0: i64 = g_abs(rana0); if rden0<floor_q { rden0=floor_q } 157 var caught: i64 = 1 158 if g_abs(fdr0-bad) < ((4096*rden0)>>16) { caught=0 } 159 pass=pass+g_check("D: neg-control -- a deliberately WRONG RoPE grad is rejected (teeth)" as *u8, caught); total=total+1 160 161 // ---- C: bit-exact (attention+RoPE gradient identical across two runs) ---- 162 let lvc: *i64 = sys_mmap(4*8) as *i64 163 let lossc: i64 = ar_loss(tape,vals,st,aX,Wq,Wk,Wv,aT,T,d,scale,lvc) 164 nfa_backward(tape,vals,grads,st[0],lossc) 165 let gA: i64 = nfa_grad(tape,grads,lvc[0],0); let gB: i64 = nfa_grad(tape,grads,lvc[0],1) 166 let lossc2: i64 = ar_loss(tape,vals,st,aX,Wq,Wk,Wv,aT,T,d,scale,lvc) 167 nfa_backward(tape,vals,grads,st[0],lossc2) 168 let gA2: i64 = nfa_grad(tape,grads,lvc[0],0); let gB2: i64 = nfa_grad(tape,grads,lvc[0],1) 169 var bitexact: i64 = 1 170 if gA2 != gA { bitexact=0 } 171 if gB2 != gB { bitexact=0 } 172 pass=pass+g_check("C: bit-exact -- attention+RoPE gradient identical across two runs (determinism)" as *u8, bitexact); total=total+1 173 174 // ---- emit ---- 175 var okall: i64=0; if pass==total { okall=1 } 176 let logf: i64 = sys_openat_append(RLOG, 420) 177 if logf >= 0 { 178 r_ws(logf,"NOFLOATROPE A1_rope=" as *u8); r_wn(logf,r1_ok); r_ws(logf," A2_attn_rope=" as *u8); r_wn(logf,r2_ok) 179 r_ws(logf," D=" as *u8); r_wn(logf,caught); r_ws(logf," C=" as *u8); r_wn(logf,bitexact) 180 if okall==1 { r_ws(logf," verdict=GREEN\n" as *u8) } else { r_ws(logf," verdict=RED\n" as *u8) } 181 sys_close(logf) 182 } 183 g_puts("---- nofloat_rope gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 184 if okall==1 { g_puts("verdict=GREEN\n" as *u8); sys_exit(0); return 0 } 185 g_puts("verdict=RED\n" as *u8); sys_exit(1); return 1 186}