code wiki / _hdl_build / nx_nofloat_attn_gate.nx
`nx_nofloat_attn_gate.nx` source

↩ module page · 252 lines · 14255 B
1// nx_nofloat_attn_gate.nx -- HARD-EVIDENCE gate for the ATTENTION-CORE backward (CAP-NF-ATTN-CORE): a single-head
2// CAUSAL self-attention block backprops end-to-end in PURE INTEGER Q16. This is the heart of CAP-NF-TRAIN-ATTN.
3// New ops proven: matmul (C=A.B), matmul_nt (S=Q.K^T), cmul (1/sqrt(d) scale), causal softmax_rows.
4//
5//   A1 matmul gradcheck      : C=A.B, loss=mse(C,t); tape grad dL/dA == central finite difference.
6//   A2 matmul_nt gradcheck   : S=A.B^T (the Q.K^T form); tape grad == finite difference.
7//   A3 attention-core gradcheck: full path X->{Q,K,V}=X.W -> S=Q.K^T -> scale -> CAUSAL softmax rows -> O=A.V ->
8//      mse; gradcheck dL/dWq, the gradient that flows THROUGH softmax + both matmuls (the real attention backward).
9//   D  neg-control teeth     : a deliberately wrong matmul grad is rejected.
10//   B  attention LEARNS      : with Wq,Wk fixed (attention pattern A fixed), the VALUE path O=A.(X.Wv) is linear ->
11//      train Wv from zero to a realizable target; assert loss collapses + Wv converges (the value projection trains).
12//   C  bit-exact             : train twice -> identical integer Wv (determinism is structural for integer).
13//
14// Evidence -> knowledge/status/nofloat_attn.log. Sovereign: imports nx_nofloat_autograd (pure integer) + nx_syscalls.
15// HONEST scope: this is the attention CORE (matmuls + causal softmax). RoPE + output-projection + multi-head are the
16// next sub-rung (CAP-NF-TRAIN-ATTN full). license_tier: ORIGINAL  expect_exit: 0
17import "nx_nofloat_autograd.nx"
18import "nx_syscalls.nx"
19import "nx_gate_emit_lib.nx"
20import "nx_gate_verdict.nx"
21
22const ALOG: *u8 = "knowledge/status/nofloat_attn.log"
23const Q16:  i64 = 65536
24
25
26func g_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v }
27func q_milli(q: i64) -> i64 { var neg: i64=0; var a: i64=q; if a<0 { neg=1; a=0-a } let m: i64=(a*1000)/Q16; if neg==1 { return 0-m } return m }
28func a_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 }
29func a_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 }
30
31// ---- 2x2x2 matmul / matmul_nt gradcheck (op=8 matmul, op=9 matmul_nt) ----
32func mm_loss(tape: *i64, vals: *i64, st: *i64, op: i64, As: *i64, Bs: *i64, Ts: *i64, leaves: *i64) -> i64 {
  st[0]=0; st[1]=0
  let nA: i64 = nfa_leaf(tape,vals,st,2,2,As,0)
  let nB: i64 = nfa_leaf(tape,vals,st,2,2,Bs,0)
  var nC: i64 = nA
  if op == 8 { nC = nfa_matmul(tape,vals,st,nA,nB) }
  if op == 9 { nC = nfa_matmul_nt(tape,vals,st,nA,nB) }
  let nt: i64 = nfa_leaf(tape,vals,st,2,2,Ts,0)
  let loss: i64 = nfa_mse(tape,vals,st,nC,nt)
  leaves[0]=nA
  return loss
43}
44func mm_lossval(tape: *i64, vals: *i64, st: *i64, op: i64, As: *i64, Bs: *i64, Ts: *i64) -> i64 {
  let lv: *i64 = sys_mmap(8) as *i64
  let loss: i64 = mm_loss(tape,vals,st,op,As,Bs,Ts,lv)
  return nfa_val(tape,vals,loss,0)
48}
49func mm_fd(tape: *i64, vals: *i64, st: *i64, op: i64, As: *i64, Bs: *i64, Ts: *i64, pi: i64, h: i64) -> i64 {
  let ap: *i64 = sys_mmap(4*8) as *i64
  let am: *i64 = sys_mmap(4*8) as *i64
  var i: i64=0
  while i<4 { ap[i]=As[i]; am[i]=As[i]; i=i+1 }
  ap[pi]=As[pi]+h; am[pi]=As[pi]-h
  let lp: i64 = mm_lossval(tape,vals,st,op,ap,Bs,Ts)
  let lm: i64 = mm_lossval(tape,vals,st,op,am,Bs,Ts)
  return ((lp-lm)*Q16)/(2*h)
58}
59func mm_gradcheck(tape: *i64, vals: *i64, grads: *i64, st: *i64, op: i64, As: *i64, Bs: *i64, Ts: *i64, h: i64, tol_q: i64, floor_q: i64, worst: *i64) -> i64 {
  let lv: *i64 = sys_mmap(8) as *i64
  let loss: i64 = mm_loss(tape,vals,st,op,As,Bs,Ts,lv)
  nfa_backward(tape,vals,grads,st[0],loss)
  let nA: i64 = lv[0]
  var ok: i64=1; worst[0]=0
  var i: i64=0
  while i<4 {
      let ana: i64 = nfa_grad(tape,grads,nA,i)
      let fd: i64 = mm_fd(tape,vals,st,op,As,Bs,Ts,i,h)
      let num: i64 = g_abs(fd-ana)
      var den: i64 = g_abs(ana); if den<floor_q { den=floor_q }
      if num >= ((tol_q*den)>>16) { ok=0 }
      let rel: i64 = (num*1000)/den
      if rel>worst[0] { worst[0]=rel }
      i=i+1
  }
  return ok
77}
78
79// ---- single-head causal attention forward on the tape; leaves[0..3]=nWq,nWk,nWv,nX; returns the O node ----
80func attn_fwd(tape: *i64, vals: *i64, st: *i64, Xs: *i64, Wqs: *i64, Wks: *i64, Wvs: *i64, T: i64, d: i64, scale: i64, leaves: *i64) -> i64 {
  st[0]=0; st[1]=0
  let nX:  i64 = nfa_leaf(tape,vals,st,T,d,Xs,0)
  let nWq: i64 = nfa_leaf(tape,vals,st,d,d,Wqs,0)
  let nWk: i64 = nfa_leaf(tape,vals,st,d,d,Wks,0)
  let nWv: i64 = nfa_leaf(tape,vals,st,d,d,Wvs,0)
  let nQ:  i64 = nfa_matmul(tape,vals,st,nX,nWq)
  let nK:  i64 = nfa_matmul(tape,vals,st,nX,nWk)
  let nV:  i64 = nfa_matmul(tape,vals,st,nX,nWv)
  let nS:  i64 = nfa_matmul_nt(tape,vals,st,nQ,nK)
  let nSs: i64 = nfa_cmul(tape,vals,st,nS,scale)
  let nA:  i64 = nfa_softmax_rows(tape,vals,st,nSs,1)
  let nO:  i64 = nfa_matmul(tape,vals,st,nA,nV)
  leaves[0]=nWq; leaves[1]=nWk; leaves[2]=nWv; leaves[3]=nX
  return nO
95}
96func attn_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 {
  let nO: i64 = attn_fwd(tape,vals,st,Xs,Wqs,Wks,Wvs,T,d,scale,leaves)
  let nt: i64 = nfa_leaf(tape,vals,st,T,d,Ts,0)
  return nfa_mse(tape,vals,st,nO,nt)
100}
101func attn_lossval(tape: *i64, vals: *i64, st: *i64, Xs: *i64, Wqs: *i64, Wks: *i64, Wvs: *i64, Ts: *i64, T: i64, d: i64, scale: i64) -> i64 {
  let lv: *i64 = sys_mmap(4*8) as *i64
  let loss: i64 = attn_loss(tape,vals,st,Xs,Wqs,Wks,Wvs,Ts,T,d,scale,lv)
  return nfa_val(tape,vals,loss,0)
105}
106// copy the O (attention output) values for given weights into outO (for realizable target generation)
107func attn_out(tape: *i64, vals: *i64, st: *i64, Xs: *i64, Wqs: *i64, Wks: *i64, Wvs: *i64, T: i64, d: i64, scale: i64, outO: *i64) -> i64 {
  let lv: *i64 = sys_mmap(4*8) as *i64
  let nO: i64 = attn_fwd(tape,vals,st,Xs,Wqs,Wks,Wvs,T,d,scale,lv)
  var i: i64 = 0
  while i < T*d { outO[i] = nfa_val(tape,vals,nO,i); i = i + 1 }
  return 0
113}
114
115func main() -> i64 {
  g_puts("nx_nofloat_attn gate (single-head CAUSAL attention backprops in PURE INTEGER Q16 -- MEASURED)\n" as *u8)
  var pass: i64=0; var total: i64=0
  let tape:  *i64 = sys_mmap(512*7*8) as *i64
  let vals:  *i64 = sys_mmap(8192*8) as *i64
  let grads: *i64 = sys_mmap(8192*8) as *i64
  let st:    *i64 = sys_mmap(2*8) as *i64
  let h: i64 = 512
  let floor_q: i64 = 4096
  let worst: *i64 = sys_mmap(8) as *i64
125
  // ---- A1: matmul gradcheck ----
  let A1: *i64 = sys_mmap(4*8) as *i64; A1[0]=32768; A1[1]=0-16384; A1[2]=49152; A1[3]=65536
  let B1: *i64 = sys_mmap(4*8) as *i64; B1[0]=65536; B1[1]=16384; B1[2]=0-32768; B1[3]=49152
  let T1: *i64 = sys_mmap(4*8) as *i64; T1[0]=13107; T1[1]=6554; T1[2]=0-19661; T1[3]=26214
  let mm_ok: i64 = mm_gradcheck(tape,vals,grads,st,8,A1,B1,T1,h,4096,floor_q,worst)
  g_puts("  [measure] matmul worst rel grad err = " as *u8); g_pn(worst[0]); g_puts(" /1000 (tol=62)\n" as *u8)
  pass=pass+g_check("A1: matmul gradcheck -- C=A.B backward (dA=dC.B^T) == finite differences" as *u8, mm_ok); total=total+1
133
  // ---- A2: matmul_nt gradcheck ----
  let mmnt_ok: i64 = mm_gradcheck(tape,vals,grads,st,9,A1,B1,T1,h,4096,floor_q,worst)
  g_puts("  [measure] matmul_nt worst rel grad err = " as *u8); g_pn(worst[0]); g_puts(" /1000 (tol=62)\n" as *u8)
  pass=pass+g_check("A2: matmul_nt gradcheck -- S=A.B^T (Q.K^T) backward == finite differences" as *u8, mmnt_ok); total=total+1
138
  // ---- A3: full attention-core gradcheck wrt Wq (through causal softmax + both matmuls) ----
  let T: i64 = 3; let d: i64 = 2; let scale: i64 = 46341      // 1/sqrt(2) Q16
  let Xs: *i64 = sys_mmap(T*d*8) as *i64; Xs[0]=32768; Xs[1]=16384; Xs[2]=0-16384; Xs[3]=49152; Xs[4]=65536; Xs[5]=0-32768
  let Wq: *i64 = sys_mmap(d*d*8) as *i64; Wq[0]=49152; Wq[1]=0-16384; Wq[2]=32768; Wq[3]=65536
  let Wk: *i64 = sys_mmap(d*d*8) as *i64; Wk[0]=16384; Wk[1]=32768; Wk[2]=0-32768; Wk[3]=49152
  let Wv: *i64 = sys_mmap(d*d*8) as *i64; Wv[0]=65536; Wv[1]=0-32768; Wv[2]=16384; Wv[3]=49152
  let Tg: *i64 = sys_mmap(T*d*8) as *i64; Tg[0]=13107; Tg[1]=0-6554; Tg[2]=19661; Tg[3]=6554; Tg[4]=0-13107; Tg[5]=26214
  let lv: *i64 = sys_mmap(4*8) as *i64
  let loss: i64 = attn_loss(tape,vals,st,Xs,Wq,Wk,Wv,Tg,T,d,scale,lv)
  nfa_backward(tape,vals,grads,st[0],loss)
  let nWq: i64 = lv[0]
  var a3_ok: i64 = 1; var a3_worst: i64 = 0
  var pi: i64 = 0
  while pi < d*d {
      let ana: i64 = nfa_grad(tape,grads,nWq,pi)
      let wqp: *i64 = sys_mmap(d*d*8) as *i64
      let wqm: *i64 = sys_mmap(d*d*8) as *i64
      var z: i64=0
      while z<d*d { wqp[z]=Wq[z]; wqm[z]=Wq[z]; z=z+1 }
      wqp[pi]=Wq[pi]+h; wqm[pi]=Wq[pi]-h
      let lp: i64 = attn_lossval(tape,vals,st,Xs,wqp,Wk,Wv,Tg,T,d,scale)
      let lm: i64 = attn_lossval(tape,vals,st,Xs,wqm,Wk,Wv,Tg,T,d,scale)
      let fd: i64 = ((lp-lm)*Q16)/(2*h)
      let num: i64 = g_abs(fd-ana)
      var den: i64 = g_abs(ana); if den<floor_q { den=floor_q }
      if num >= ((8192*den)>>16) { a3_ok=0 }       // tol 1/8 (long fixed-point chain through softmax)
      let rel: i64 = (num*1000)/den
      if rel>a3_worst { a3_worst=rel }
      pi=pi+1
  }
  g_puts("  [measure] attention dL/dWq worst rel grad err = " as *u8); g_pn(a3_worst); g_puts(" /1000 (tol=125)\n" as *u8)
  pass=pass+g_check("A3: attention-core gradcheck -- dL/dWq through causal-softmax + Q.K^T + A.V == finite diff" as *u8, a3_ok); total=total+1
171
  // ---- D: neg-control teeth (matmul) ----
  let lvd: *i64 = sys_mmap(8) as *i64
  let lossd: i64 = mm_loss(tape,vals,st,8,A1,B1,T1,lvd)
  nfa_backward(tape,vals,grads,st[0],lossd)
  let ana0: i64 = nfa_grad(tape,grads,lvd[0],0)
  let fd0: i64 = mm_fd(tape,vals,st,8,A1,B1,T1,0,h)
  let bad: i64 = 0 - ana0
  var den0: i64 = g_abs(ana0); if den0<floor_q { den0=floor_q }
  var caught: i64 = 1
  if g_abs(fd0-bad) < ((4096*den0)>>16) { caught=0 }
  pass=pass+g_check("D: neg-control -- a deliberately WRONG matmul grad is rejected (teeth)" as *u8, caught); total=total+1
183
  // ---- B: attention value-path LEARNS (Wq,Wk fixed -> A fixed -> O=A.(X.Wv) convex in Wv) ----
  let Wvt: *i64 = sys_mmap(d*d*8) as *i64; Wvt[0]=65536; Wvt[1]=0-32768; Wvt[2]=16384; Wvt[3]=49152   // Wv* target
  let tgt: *i64 = sys_mmap(T*d*8) as *i64
  attn_out(tape,vals,st,Xs,Wq,Wk,Wvt,T,d,scale,tgt)            // realizable target = attention out with Wv*
  let Wvp: *i64 = sys_mmap(d*d*8) as *i64; Wvp[0]=0; Wvp[1]=0; Wvp[2]=0; Wvp[3]=0   // learn from zero
  let lvb: *i64 = sys_mmap(4*8) as *i64
  let gW: *i64 = sys_mmap(d*d*8) as *i64
  var lf: i64 = 0; var ll: i64 = 0
  var ep: i64 = 0
  while ep < 6000 {
      let lossb: i64 = attn_loss(tape,vals,st,Xs,Wq,Wk,Wvp,tgt,T,d,scale,lvb)
      nfa_backward(tape,vals,grads,st[0],lossb)
      if ep==0 { lf = nfa_val(tape,vals,lossb,0) }
      ll = nfa_val(tape,vals,lossb,0)
      var z: i64=0
      while z<d*d { gW[z]=nfa_grad(tape,grads,lvb[2],z); z=z+1 }   // lvb[2] = nWv leaf
      nfa_sgd(Wvp, gW, d*d, 1024)
      ep=ep+1
  }
  g_puts("  [measure] attention Wv-learn loss: start=" as *u8); g_pn(lf); g_puts(" end=" as *u8); g_pn(ll)
  g_puts("  Wv=[" as *u8); g_pn(Wvp[0]); g_puts("," as *u8); g_pn(Wvp[1]); g_puts("," as *u8); g_pn(Wvp[2]); g_puts("," as *u8); g_pn(Wvp[3]); g_puts("] vs Wv*=[65536,-32768,16384,49152]\n" as *u8)
  var learns: i64 = 1
  if ll*10 > lf { learns=0 }
  if g_abs(Wvp[0]-65536)>9830 { learns=0 }
  if g_abs(Wvp[1]+32768)>9830 { learns=0 }
  if g_abs(Wvp[2]-16384)>9830 { learns=0 }
  if g_abs(Wvp[3]-49152)>9830 { learns=0 }
  if lf<=0 { learns=0 }
  pass=pass+g_check("B: attention value-path LEARNS in pure integer -- Wv converges to target, loss collapses" as *u8, learns); total=total+1
213
  // ---- C: bit-exact ----
  let Wvp2: *i64 = sys_mmap(d*d*8) as *i64; Wvp2[0]=0; Wvp2[1]=0; Wvp2[2]=0; Wvp2[3]=0
  let lvc: *i64 = sys_mmap(4*8) as *i64
  let gW2: *i64 = sys_mmap(d*d*8) as *i64
  var ep2: i64=0
  while ep2 < 6000 {
      let lossc: i64 = attn_loss(tape,vals,st,Xs,Wq,Wk,Wvp2,tgt,T,d,scale,lvc)
      nfa_backward(tape,vals,grads,st[0],lossc)
      var z: i64=0
      while z<d*d { gW2[z]=nfa_grad(tape,grads,lvc[2],z); z=z+1 }
      nfa_sgd(Wvp2, gW2, d*d, 1024)
      ep2=ep2+1
  }
  var bitexact: i64 = 1
  var z2: i64=0
  while z2<d*d { if Wvp2[z2]!=Wvp[z2] { bitexact=0 } z2=z2+1 }
  pass=pass+g_check("C: bit-exact -- training twice gives IDENTICAL integer Wv (determinism)" as *u8, bitexact); total=total+1
231
  // ---- emit ----
  var okall: i64=0; if pass==total { okall=1 }
  let logf: i64 = sys_openat_append(ALOG, 420)
  if logf >= 0 {
      a_ws(logf,"NOFLOATATTN ops=matmul,matmul_nt,cmul,causal_softmax_rows A1=" as *u8); a_wn(logf,mm_ok)
      a_ws(logf," A2=" as *u8); a_wn(logf,mmnt_ok); a_ws(logf," A3_attn=" as *u8); a_wn(logf,a3_ok); a_ws(logf," D=" as *u8); a_wn(logf,caught)
      a_ws(logf," B_learns=" as *u8); a_wn(logf,learns); a_ws(logf," C_bitexact=" as *u8); a_wn(logf,bitexact)
      if okall==1 { a_ws(logf," verdict=GREEN\n" as *u8) } else { a_ws(logf," verdict=RED\n" as *u8) }
      sys_close(logf)
  }
  g_puts("---- nofloat_attn gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8)
  // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
  // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
  // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
  let ctr__dry: *i64 = gv_ctr()
  ctr__dry[0] = pass
  ctr__dry[1] = total
  let rc__dry: i64 = gv_verdict("NOFLOAT-ATTN-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
252}
nx_nofloat_attn_gate.nx source

`nx_nofloat_attn_gate.nx` source
