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" 17import "nx_gate_verdict.nx" 18 19const RLOG: *u8 = "knowledge/status/nofloat_rope.log" 20const Q16: i64 = 65536 21 22 23func g_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v } 24func 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 } 25func 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 } 26 27// ---- A1: RoPE gradcheck (loss = mse(RoPE(x), target)) ---- 28func rope_loss(tape: *i64, vals: *i64, st: *i64, Xs: *i64, T: i64, hd: i64, Ts: *i64, leaves: *i64) -> i64 { 29 st[0]=0; st[1]=0 30 let nX: i64 = nfa_leaf(tape,vals,st,T,hd,Xs,0) 31 let nR: i64 = nfa_rope(tape,vals,st,nX) 32 let nt: i64 = nfa_leaf(tape,vals,st,T,hd,Ts,0) 33 let loss: i64 = nfa_mse(tape,vals,st,nR,nt) 34 leaves[0]=nX 35 return loss 36} 37func rope_lossval(tape: *i64, vals: *i64, st: *i64, Xs: *i64, T: i64, hd: i64, Ts: *i64) -> i64 { 38 let lv: *i64 = sys_mmap(8) as *i64 39 let loss: i64 = rope_loss(tape,vals,st,Xs,T,hd,Ts,lv) 40 return nfa_val(tape,vals,loss,0) 41} 42 43// ---- A2: attention + RoPE forward (leaves[0..3]=nWq,nWk,nWv,nX) -> O node ---- 44func 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 { 45 st[0]=0; st[1]=0 46 let nX: i64 = nfa_leaf(tape,vals,st,T,d,Xs,0) 47 let nWq: i64 = nfa_leaf(tape,vals,st,d,d,Wqs,0) 48 let nWk: i64 = nfa_leaf(tape,vals,st,d,d,Wks,0) 49 let nWv: i64 = nfa_leaf(tape,vals,st,d,d,Wvs,0) 50 let nQ: i64 = nfa_matmul(tape,vals,st,nX,nWq) 51 let nK: i64 = nfa_matmul(tape,vals,st,nX,nWk) 52 let nV: i64 = nfa_matmul(tape,vals,st,nX,nWv) 53 let nQr: i64 = nfa_rope(tape,vals,st,nQ) 54 let nKr: i64 = nfa_rope(tape,vals,st,nK) 55 let nS: i64 = nfa_matmul_nt(tape,vals,st,nQr,nKr) 56 let nSs: i64 = nfa_cmul(tape,vals,st,nS,scale) 57 let nA: i64 = nfa_softmax_rows(tape,vals,st,nSs,1) 58 let nO: i64 = nfa_matmul(tape,vals,st,nA,nV) 59 leaves[0]=nWq; leaves[1]=nWk; leaves[2]=nWv; leaves[3]=nX 60 return nO 61} 62func 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 { 63 let nO: i64 = ar_fwd(tape,vals,st,Xs,Wqs,Wks,Wvs,T,d,scale,leaves) 64 let nt: i64 = nfa_leaf(tape,vals,st,T,d,Ts,0) 65 return nfa_mse(tape,vals,st,nO,nt) 66} 67func 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 { 68 let lv: *i64 = sys_mmap(4*8) as *i64 69 let loss: i64 = ar_loss(tape,vals,st,Xs,Wqs,Wks,Wvs,Ts,T,d,scale,lv) 70 return nfa_val(tape,vals,loss,0) 71} 72 73func main() -> i64 { 74 g_puts("nx_nofloat_rope gate (RoPE backward + RoPE-in-attention, PURE INTEGER Q16 -- MEASURED)\n" as *u8) 75 var pass: i64=0; var total: i64=0 76 let tape: *i64 = sys_mmap(512*7*8) as *i64 77 let vals: *i64 = sys_mmap(8192*8) as *i64 78 let grads: *i64 = sys_mmap(8192*8) as *i64 79 let st: *i64 = sys_mmap(2*8) as *i64 80 let h: i64 = 512 81 let floor_q: i64 = 4096 82 83 // ---- A1: RoPE gradcheck ---- 84 let T: i64 = 3; let hd: i64 = 2 85 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 86 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 87 let lv: *i64 = sys_mmap(8) as *i64 88 let loss1: i64 = rope_loss(tape,vals,st,Xs,T,hd,Ts,lv) 89 nfa_backward(tape,vals,grads,st[0],loss1) 90 let nX: i64 = lv[0] 91 var r1_ok: i64 = 1; var r1_worst: i64 = 0 92 var pi: i64 = 0 93 while pi < T*hd { 94 let ana: i64 = nfa_grad(tape,grads,nX,pi) 95 let xp: *i64 = sys_mmap(T*hd*8) as *i64 96 let xm: *i64 = sys_mmap(T*hd*8) as *i64 97 var z: i64=0 98 while z<T*hd { xp[z]=Xs[z]; xm[z]=Xs[z]; z=z+1 } 99 xp[pi]=Xs[pi]+h; xm[pi]=Xs[pi]-h 100 let lp: i64 = rope_lossval(tape,vals,st,xp,T,hd,Ts) 101 let lm: i64 = rope_lossval(tape,vals,st,xm,T,hd,Ts) 102 let fd: i64 = ((lp-lm)*Q16)/(2*h) 103 let num: i64 = g_abs(fd-ana) 104 var den: i64 = g_abs(ana); if den<floor_q { den=floor_q } 105 if num >= ((4096*den)>>16) { r1_ok=0 } // tol 1/16 106 let rel: i64 = (num*1000)/den 107 if rel>r1_worst { r1_worst=rel } 108 pi=pi+1 109 } 110 g_puts(" [measure] RoPE worst rel grad err = " as *u8); g_pn(r1_worst); g_puts(" /1000 (tol=62)\n" as *u8) 111 pass=pass+g_check("A1: RoPE gradcheck -- rotation backward (rotate by -angle) == finite differences" as *u8, r1_ok); total=total+1 112 113 // ---- A2: attention + RoPE gradcheck wrt Wq ---- 114 let d: i64 = 2; let scale: i64 = 46341 115 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 116 let Wq: *i64 = sys_mmap(d*d*8) as *i64; Wq[0]=49152; Wq[1]=0-16384; Wq[2]=32768; Wq[3]=65536 117 let Wk: *i64 = sys_mmap(d*d*8) as *i64; Wk[0]=16384; Wk[1]=32768; Wk[2]=0-32768; Wk[3]=49152 118 let Wv: *i64 = sys_mmap(d*d*8) as *i64; Wv[0]=65536; Wv[1]=0-32768; Wv[2]=16384; Wv[3]=49152 119 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 120 let lv2: *i64 = sys_mmap(4*8) as *i64 121 let loss2: i64 = ar_loss(tape,vals,st,aX,Wq,Wk,Wv,aT,T,d,scale,lv2) 122 nfa_backward(tape,vals,grads,st[0],loss2) 123 let nWq: i64 = lv2[0] 124 var r2_ok: i64 = 1; var r2_worst: i64 = 0 125 var qi: i64 = 0 126 while qi < d*d { 127 let ana: i64 = nfa_grad(tape,grads,nWq,qi) 128 let wqp: *i64 = sys_mmap(d*d*8) as *i64 129 let wqm: *i64 = sys_mmap(d*d*8) as *i64 130 var z: i64=0 131 while z<d*d { wqp[z]=Wq[z]; wqm[z]=Wq[z]; z=z+1 } 132 wqp[qi]=Wq[qi]+h; wqm[qi]=Wq[qi]-h 133 let lp: i64 = ar_lossval(tape,vals,st,aX,wqp,Wk,Wv,aT,T,d,scale) 134 let lm: i64 = ar_lossval(tape,vals,st,aX,wqm,Wk,Wv,aT,T,d,scale) 135 let fd: i64 = ((lp-lm)*Q16)/(2*h) 136 let num: i64 = g_abs(fd-ana) 137 var den: i64 = g_abs(ana); if den<floor_q { den=floor_q } 138 if num >= ((8192*den)>>16) { r2_ok=0 } // tol 1/8 (long chain through RoPE+softmax) 139 let rel: i64 = (num*1000)/den 140 if rel>r2_worst { r2_worst=rel } 141 qi=qi+1 142 } 143 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) 144 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 145 146 // ---- D: neg-control teeth (RoPE) ---- 147 let lossd: i64 = rope_loss(tape,vals,st,Xs,T,hd,Ts,lv) 148 nfa_backward(tape,vals,grads,st[0],lossd) 149 let rana0: i64 = nfa_grad(tape,grads,lv[0],0) 150 let xp0: *i64 = sys_mmap(T*hd*8) as *i64 151 let xm0: *i64 = sys_mmap(T*hd*8) as *i64 152 var z0: i64=0 153 while z0<T*hd { xp0[z0]=Xs[z0]; xm0[z0]=Xs[z0]; z0=z0+1 } 154 xp0[0]=Xs[0]+h; xm0[0]=Xs[0]-h 155 let fdr0: i64 = ((rope_lossval(tape,vals,st,xp0,T,hd,Ts) - rope_lossval(tape,vals,st,xm0,T,hd,Ts))*Q16)/(2*h) 156 let bad: i64 = 0 - rana0 157 var rden0: i64 = g_abs(rana0); if rden0<floor_q { rden0=floor_q } 158 var caught: i64 = 1 159 if g_abs(fdr0-bad) < ((4096*rden0)>>16) { caught=0 } 160 pass=pass+g_check("D: neg-control -- a deliberately WRONG RoPE grad is rejected (teeth)" as *u8, caught); total=total+1 161 162 // ---- C: bit-exact (attention+RoPE gradient identical across two runs) ---- 163 let lvc: *i64 = sys_mmap(4*8) as *i64 164 let lossc: i64 = ar_loss(tape,vals,st,aX,Wq,Wk,Wv,aT,T,d,scale,lvc) 165 nfa_backward(tape,vals,grads,st[0],lossc) 166 let gA: i64 = nfa_grad(tape,grads,lvc[0],0); let gB: i64 = nfa_grad(tape,grads,lvc[0],1) 167 let lossc2: i64 = ar_loss(tape,vals,st,aX,Wq,Wk,Wv,aT,T,d,scale,lvc) 168 nfa_backward(tape,vals,grads,st[0],lossc2) 169 let gA2: i64 = nfa_grad(tape,grads,lvc[0],0); let gB2: i64 = nfa_grad(tape,grads,lvc[0],1) 170 var bitexact: i64 = 1 171 if gA2 != gA { bitexact=0 } 172 if gB2 != gB { bitexact=0 } 173 pass=pass+g_check("C: bit-exact -- attention+RoPE gradient identical across two runs (determinism)" as *u8, bitexact); total=total+1 174 175 // ---- emit ---- 176 var okall: i64=0; if pass==total { okall=1 } 177 let logf: i64 = sys_openat_append(RLOG, 420) 178 if logf >= 0 { 179 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) 180 r_ws(logf," D=" as *u8); r_wn(logf,caught); r_ws(logf," C=" as *u8); r_wn(logf,bitexact) 181 if okall==1 { r_ws(logf," verdict=GREEN\n" as *u8) } else { r_ws(logf," verdict=RED\n" as *u8) } 182 sys_close(logf) 183 } 184 g_puts("---- nofloat_rope gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 185 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 186 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 187 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 188 let ctr__dry: *i64 = gv_ctr() 189 ctr__dry[0] = pass 190 ctr__dry[1] = total 191 let rc__dry: i64 = gv_verdict("NOFLOAT-ROPE-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 192 sys_exit(rc__dry) 193 return rc__dry 194}