nx_fnet_grad_gate.nx source

1// nx_fnet_grad_gate.nx -- GATE for FNET-002: the FNet mixer's backward pass (VJP). Proves, by RUNNING, that 2// the mixer is SELF-ADJOINT, so dL/dx = fnet_mix(dL/dy) -- backprop is one forward mix, zero stored 3// activations, zero parameters. Three independent proofs (n=8, d=4 -> a 32-dim operator): 4// 5// G1 SYMMETRY extract the operator matrix M by impulse responses (M[:,k] = fnet_mix(S*e_k)); the 6// real-linear FNet operator must be SYMMETRIC (A = A^T) because it is the real part of a 7// Kronecker product of symmetric DFT matrices. Measure max|M[i,j]-M[j,i]|. 8// G2 ADJOINT TEST the relationship backprop relies on: <A x, g> == <x, A* g> with A* = A. Measure 9// |<Ax,g> - <x,Ag>| -- zero (to rounding) IFF using fnet_mix as the backward is the 10// correct VJP. 11// G3 GRADCHECK finite-difference the scalar loss L(x)=sum a*fnet_mix(x): central differences vs the 12// analytic backward fnet_mix_backward(a). Max |fd - analytic|. 13// 14// All three are robust to the Q14 fixed-point rounding (tolerances are a small % of signal, actuals reported). 15// Evidence -> knowledge/status/fnet_grad.log (FNETGRADGATE authored=organ ... verdict=GREEN). license_tier: ORIGINAL 16import "nx_fnet_mix.nx" 17import "nx_syscalls.nx" 18import "nx_gate_verdict.nx" 19 20const FG_LOG: *u8 = "knowledge/status/fnet_grad.log" 21 22func fg_w(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 } 23func fg_wn(fd: i64, v: i64) -> i64 { 24 let bb: *u8 = sys_mmap(28); var m: i64 = v 25 if m < 0 { m = 0 - m; sys_write(fd, "-" as *u8, 1) } 26 let t: *u8 = sys_mmap(28); var k: i64 = 0 27 if m == 0 { t[0] = 48; k = 1 } 28 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 29 var i: i64 = 0 30 while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } 31 sys_write(fd, bb, k); return 0 32} 33func fg_abs(x: i64) -> i64 { if x < 0 { return 0 - x } return x } 34 35// real part of fnet_mix applied to a real vector src[nd] -> out[nd] (fresh buffers; src untouched). 36func fg_forward(src: *i64, n: i64, d: i64, out: *i64) -> i64 { 37 let nd: i64 = n * d 38 let xr: *i64 = (sys_mmap(nd * 8)) as *i64 39 let xi: *i64 = (sys_mmap(nd * 8)) as *i64 40 var i: i64 = 0 41 while i < nd { xr[i] = src[i]; xi[i] = 0; i = i + 1 } 42 let opc: *i64 = (sys_mmap(8)) as *i64 43 *opc = 0 44 fnet_mix(xr, xi, n, d, opc) 45 i = 0 46 while i < nd { out[i] = xr[i]; i = i + 1 } 47 return 0 48} 49 50func main() -> i64 { 51 let n: i64 = 8 52 let d: i64 = 4 53 let nd: i64 = n * d 54 var ok: i64 = 1 55 56 // ---------- G1: extract operator matrix by impulse responses; measure asymmetry ---------- 57 let S: i64 = 65536 // large impulse so Q14 truncation is negligible vs entries 58 let mtx: *i64 = (sys_mmap(nd * nd * 8)) as *i64 59 let e: *i64 = (sys_mmap(nd * 8)) as *i64 60 let yk: *i64 = (sys_mmap(nd * 8)) as *i64 61 var col: i64 = 0 62 while col < nd { 63 var i: i64 = 0 64 while i < nd { e[i] = 0; i = i + 1 } 65 e[col] = S 66 fg_forward(e, n, d, yk) 67 i = 0 68 while i < nd { mtx[i * nd + col] = yk[i]; i = i + 1 } 69 col = col + 1 70 } 71 var asym: i64 = 0 72 var symmax: i64 = 0 73 var r: i64 = 0 74 while r < nd { 75 var c: i64 = 0 76 while c < nd { 77 let av: i64 = fg_abs(mtx[r * nd + c]) 78 if av > symmax { symmax = av } 79 let df: i64 = fg_abs(mtx[r * nd + c] - mtx[c * nd + r]) 80 if df > asym { asym = df } 81 c = c + 1 82 } 83 r = r + 1 84 } 85 86 // ---------- G2: adjoint dot-product test <Ax,g> vs <x,Ag> ---------- 87 let xv: *i64 = (sys_mmap(nd * 8)) as *i64 88 let gv: *i64 = (sys_mmap(nd * 8)) as *i64 89 var j: i64 = 0 90 while j < nd { 91 xv[j] = (((j * 37 + 11) % 211) - 105) * 15 92 gv[j] = (((j * 53 + 7) % 197) - 98) * 15 93 j = j + 1 94 } 95 let ax: *i64 = (sys_mmap(nd * 8)) as *i64 96 let ag: *i64 = (sys_mmap(nd * 8)) as *i64 97 fg_forward(xv, n, d, ax) 98 fg_forward(gv, n, d, ag) 99 var lhs: i64 = 0 100 var rhs: i64 = 0 101 j = 0 102 while j < nd { lhs = lhs + ax[j] * gv[j]; rhs = rhs + xv[j] * ag[j]; j = j + 1 } 103 let adjdiff: i64 = fg_abs(lhs - rhs) 104 105 // ---------- G3: finite-difference gradcheck of the self-adjoint backward ---------- 106 let a: *i64 = (sys_mmap(nd * 8)) as *i64 // loss weights (also the upstream gradient dL/dy) 107 let x0: *i64 = (sys_mmap(nd * 8)) as *i64 108 j = 0 109 while j < nd { 110 a[j] = (((j * 29 + 13) % 131) - 65) * 64 111 x0[j] = (((j * 41 + 5) % 233) - 116) * 18 112 j = j + 1 113 } 114 let analytic: *i64 = (sys_mmap(nd * 8)) as *i64 115 fg_forward(a, n, d, analytic) // dL/dx = fnet_mix_backward(a) = fnet_mix(a) 116 117 let eps: i64 = 512 118 let xp: *i64 = (sys_mmap(nd * 8)) as *i64 119 let xm: *i64 = (sys_mmap(nd * 8)) as *i64 120 let yp: *i64 = (sys_mmap(nd * 8)) as *i64 121 let ym: *i64 = (sys_mmap(nd * 8)) as *i64 122 var fdmax: i64 = 0 123 var fdana: i64 = 0 124 var k: i64 = 0 125 while k < nd { 126 var i: i64 = 0 127 while i < nd { xp[i] = x0[i]; xm[i] = x0[i]; i = i + 1 } 128 xp[k] = xp[k] + eps 129 xm[k] = xm[k] - eps 130 fg_forward(xp, n, d, yp) 131 fg_forward(xm, n, d, ym) 132 var lp: i64 = 0 133 var lm: i64 = 0 134 i = 0 135 while i < nd { lp = lp + a[i] * yp[i]; lm = lm + a[i] * ym[i]; i = i + 1 } 136 let fd: i64 = (lp - lm) / (2 * eps) 137 let df: i64 = fg_abs(fd - analytic[k]) 138 if df > fdmax { fdmax = df } 139 let av: i64 = fg_abs(analytic[k]) 140 if av > fdana { fdana = av } 141 k = k + 1 142 } 143 144 // ---------- verdicts (tolerances = small % of signal, robust to fixed-point rounding) ---------- 145 if symmax <= 0 { ok = 0 } 146 if fdana <= 0 { ok = 0 } 147 if asym * 100 > symmax { ok = 0 } // G1: asymmetry < 1% of peak entry 148 if adjdiff * 100 > fg_abs(lhs) { ok = 0 } // G2: adjoint residual < 1% of <Ax,g> 149 if fdmax * 20 > fdana { ok = 0 } // G3: gradcheck error < 5% of peak gradient 150 151 // emit 152 var f: i64 = 1 153 while f >= 0 { 154 let fd2: i64 = f 155 var lf: i64 = 1 156 if f == 0 { lf = sys_openat_append(FG_LOG, 420) } 157 if lf >= 0 { 158 fg_w(lf, "FNETGRADGATE authored=organ kernel=fnet-backward n=8 d=4 self-adjoint" as *u8) 159 fg_w(lf, " G1_asym=" as *u8); fg_wn(lf, asym); fg_w(lf, " sym_peak=" as *u8); fg_wn(lf, symmax) 160 fg_w(lf, " | G2_adj_lhs=" as *u8); fg_wn(lf, lhs); fg_w(lf, " adj_rhs=" as *u8); fg_wn(lf, rhs) 161 fg_w(lf, " adj_residual=" as *u8); fg_wn(lf, adjdiff) 162 fg_w(lf, " | G3_gradcheck_maxdiff=" as *u8); fg_wn(lf, fdmax); fg_w(lf, " grad_peak=" as *u8); fg_wn(lf, fdana) 163 if ok == 1 { fg_w(lf, " verdict=GREEN\n" as *u8) } else { fg_w(lf, " verdict=RED\n" as *u8) } 164 if f == 0 { sys_close(lf) } 165 } 166 f = f - 1 167 } 168 169 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 170 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 171 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 172 let ctr__dry: *i64 = gv_ctr() 173 ctr__dry[0] = ok 174 ctr__dry[1] = 1 175 let rc__dry: i64 = gv_verdict("FNET-GRAD-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 176 sys_exit(rc__dry) 177 return rc__dry 178}