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

↩ module page · 289 lines · 12080 B
1// nx_fnet_mix_gate.nx -- GATE for FNET-001 sub-quadratic Fourier token-mixer. Proves, by RUNNING (never
2// asserting):
3//
4//   CORRECTNESS
5//     C1  the generalized radix-2 FFT equals the naive O(n^2) DFT (same Q14 twiddles) at n=8 and n=16
6//         -- the butterfly decomposition is algebraically a real Fourier transform, not loop-counting.
7//     C2  the synthesized n=32 twiddle table matches the SHIPPED, gated nx_fft hardcoded W_32 table within
8//         1 Q14 unit -- so it is the SAME transform as the proven kernel, just generalized past N=32.
9//
10//   MEASURED SUB-QUADRATIC EXCEED (the thesis: math kills the VRAM/compute exponential)
11//     For hidden dim d=16 and sequence lengths n in {64,256,1024,4096}, both kernels are RUN on real
12//     deterministic data and their executed integer-MULTIPLY counts are measured:
13//       attention  = scores(Q@K^T, n*n*d) + softmax-normalize(n*n) + apply(@V, n*n*d) = 2*n^2*d + n^2   (O(n^2))
14//       fnet-mix   = 2*n*d*(log2 d + log2 n)                                                              (O(n log n))
15//     (softmax's transcendental exp is excluded for BOTH as a non-MAC, the standard FLOP convention; the
16//      two O(n^2*d) matmuls are the attention cost present in every attention variant.)
17//     Each measured count is asserted EQUAL to its structural closed form (the counter is faithful), and the
18//     gate proves: fnet_mul < attn_mul at every n, AND the attn/fnet ratio STRICTLY GROWS with n -- the
19//     quadratic-vs-linearithmic crossover, compounding as context lengthens. A real output checksum from each
20//     kernel is printed so the work cannot be dead-code-eliminated.
21//
22// Evidence -> knowledge/status/fnet_mix.log (FNETGATE authored=organ ... verdict=GREEN).
23// license_tier: ORIGINAL
24import "nx_fnet_mix.nx"     // the kernel under test (brings nx_fft + fx + nx_syscalls transitively)
25import "nx_syscalls.nx"     // sys_write / sys_openat_append / sys_close / sys_mmap
26import "nx_gate_verdict.nx"
27
28const FN_LOG: *u8 = "knowledge/status/fnet_mix.log"
29
30func fn_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 }
31func fn_wn(fd: i64, v: i64) -> i64 {
  let bb: *u8 = sys_mmap(28); var m: i64 = v
  if m < 0 { m = 0 - m; sys_write(fd, "-" as *u8, 1) }
  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 { bb[i] = t[k - 1 - i]; i = i + 1 }
  sys_write(fd, bb, k); return 0
40}
41func fn_abs(x: i64) -> i64 { if x < 0 { return 0 - x } return x }
42
43// ===== naive O(n^2) DFT reference (independent of the radix-2 butterfly) =============================
44// out[k] = sum_j in[j] * exp(-2*pi*i*j*k/n), Q14 twiddles synthesized by the same sovereign CORDIC.
45func fn_dft(in_re: *i64, in_im: *i64, n: i64, out_re: *i64, out_im: *i64) -> i64 {
  var k: i64 = 0
  while k < n {
      var sr: i64 = 0
      var si: i64 = 0
      var j: i64 = 0
      while j < n {
          let idx: i64 = (j * k) % n
          let ang: i64 = FX_TWO_PI * idx / n
          let wr: i64 = fnet_q16_to_q14(fx_cos(ang))
          let wi: i64 = fnet_q16_to_q14(0 - fx_sin(ang))
          sr = sr + (in_re[j] * wr - in_im[j] * wi) / NX_FFT_Q
          si = si + (in_re[j] * wi + in_im[j] * wr) / NX_FFT_Q
          j = j + 1
      }
      out_re[k] = sr
      out_im[k] = si
      k = k + 1
  }
  return 0
65}
66
67// C1: max abs diff between the generalized FFT and the naive DFT on a deterministic input of length n.
68func fn_c1_fft_vs_dft(n: i64) -> i64 {
  let ar: *i64 = (sys_mmap(n * 8)) as *i64
  let ai: *i64 = (sys_mmap(n * 8)) as *i64
  let br: *i64 = (sys_mmap(n * 8)) as *i64
  let bi: *i64 = (sys_mmap(n * 8)) as *i64
  var i: i64 = 0
  while i < n {
      let v: i64 = ((i * 3 + 1) % 9) - 4   // deterministic input in [-4,4]
      ar[i] = v; ai[i] = 0
      br[i] = v; bi[i] = 0
      i = i + 1
  }
  let twr: *i64 = (sys_mmap(n * 8)) as *i64
  let twi: *i64 = (sys_mmap(n * 8)) as *i64
  fnet_build_twiddles(n, twr, twi)
  let opc: *i64 = (sys_mmap(8)) as *i64
  *opc = 0
  fnet_fft_fwd(ar, ai, n, twr, twi, opc)        // FFT in place over (ar,ai)
  let or2: *i64 = (sys_mmap(n * 8)) as *i64
  let oi2: *i64 = (sys_mmap(n * 8)) as *i64
  fn_dft(br, bi, n, or2, oi2)                   // DFT over (br,bi) -> (or2,oi2)
  var maxd: i64 = 0
  i = 0
  while i < n {
      let d1: i64 = fn_abs(ar[i] - or2[i])
      let d2: i64 = fn_abs(ai[i] - oi2[i])
      if d1 > maxd { maxd = d1 }
      if d2 > maxd { maxd = d2 }
      i = i + 1
  }
  return maxd
99}
100
101// C2: max abs diff between synthesized n=32 twiddles and the SHIPPED nx_fft hardcoded W_32 table.
102func fn_c2_twiddle_match() -> i64 {
  let hr: *i64 = (sys_mmap(16 * 8)) as *i64
  let hi: *i64 = (sys_mmap(16 * 8)) as *i64
  hr[0]=16384; hr[1]=16069; hr[2]=15137; hr[3]=13623; hr[4]=11585; hr[5]=9102; hr[6]=6270; hr[7]=3196
  hr[8]=0; hr[9]=0-3196; hr[10]=0-6270; hr[11]=0-9102; hr[12]=0-11585; hr[13]=0-13623; hr[14]=0-15137; hr[15]=0-16069
  hi[0]=0; hi[1]=0-3196; hi[2]=0-6270; hi[3]=0-9102; hi[4]=0-11585; hi[5]=0-13623; hi[6]=0-15137; hi[7]=0-16069
  hi[8]=0-16384; hi[9]=0-16069; hi[10]=0-15137; hi[11]=0-13623; hi[12]=0-11585; hi[13]=0-9102; hi[14]=0-6270; hi[15]=0-3196
  let gr: *i64 = (sys_mmap(16 * 8)) as *i64
  let gi: *i64 = (sys_mmap(16 * 8)) as *i64
  fnet_build_twiddles(32, gr, gi)
  var maxd: i64 = 0
  var k: i64 = 0
  while k < 16 {
      let d1: i64 = fn_abs(gr[k] - hr[k])
      let d2: i64 = fn_abs(gi[k] - hi[k])
      if d1 > maxd { maxd = d1 }
      if d2 > maxd { maxd = d2 }
      k = k + 1
  }
  return maxd
122}
123
124// ===== attention baseline: faithful scaled-dot-product attention MAC count + real checksum ===========
125// Counts integer multiplies: scores (n*n*d) + softmax-normalize (n*n) + apply (n*n*d) = 2*n^2*d + n^2.
126// Streamed one query row at a time so memory stays O(n). Writes checksum via chk; returns the multiply count.
127func fn_attn_measure(n: i64, d: i64, chk: *i64) -> i64 {
  let q: *i64 = (sys_mmap(n * d * 8)) as *i64
  let kk: *i64 = (sys_mmap(n * d * 8)) as *i64
  let vv: *i64 = (sys_mmap(n * d * 8)) as *i64
  var f: i64 = 0
  while f < n * d {
      q[f]  = ((f * 7 + 3) % 11) - 5
      kk[f] = ((f * 5 + 1) % 9) - 4
      vv[f] = ((f * 3 + 2) % 7) - 3
      f = f + 1
  }
  let row: *i64 = (sys_mmap(n * 8)) as *i64
  var mul: i64 = 0
  var checksum: i64 = 0
  var i: i64 = 0
  while i < n {
      // scores[j] = dot(Q[i,:], K[j,:])  -- n*d multiplies
      var j: i64 = 0
      while j < n {
          var acc: i64 = 0
          var t: i64 = 0
          while t < d {
              acc = acc + q[i * d + t] * kk[j * d + t]
              mul = mul + 1
              t = t + 1
          }
          row[j] = acc
          j = j + 1
      }
      // softmax: max-subtract + bounded positive surrogate (the exp is a non-MAC, excluded by FLOP
      // convention from both kernels); then normalize -- n multiplies.
      var mx: i64 = row[0]
      j = 1
      while j < n { if row[j] > mx { mx = row[j] } j = j + 1 }
      var sum: i64 = 0
      j = 0
      while j < n {
          var w: i64 = 8192 + (row[j] - mx)
          if w < 1 { w = 1 }
          row[j] = w
          sum = sum + w
          j = j + 1
      }
      if sum <= 0 { sum = 1 }
      j = 0
      while j < n { row[j] = (row[j] * 1024) / sum; mul = mul + 1; j = j + 1 }
      // apply: out[i,c] = sum_j weights[j] * V[j,c]  -- n*d multiplies
      var c: i64 = 0
      while c < d {
          var oacc: i64 = 0
          var j2: i64 = 0
          while j2 < n {
              oacc = oacc + row[j2] * vv[j2 * d + c]
              mul = mul + 1
              j2 = j2 + 1
          }
          checksum = checksum + (oacc / 1024)
          c = c + 1
      }
      i = i + 1
  }
  *chk = checksum
  return mul
190}
191
192// ===== fnet baseline: run the real mixer, read its executed-multiply counter + real checksum ==========
193func fn_fnet_measure(n: i64, d: i64, chk: *i64) -> i64 {
  let xr: *i64 = (sys_mmap(n * d * 8)) as *i64
  let xi: *i64 = (sys_mmap(n * d * 8)) as *i64
  var f: i64 = 0
  while f < n * d { xr[f] = ((f * 7 + 3) % 11) - 5; xi[f] = 0; f = f + 1 }
  let opc: *i64 = (sys_mmap(8)) as *i64
  *opc = 0
  fnet_mix(xr, xi, n, d, opc)
  var checksum: i64 = 0
  f = 0
  while f < n * d { checksum = checksum + xr[f]; f = f + 1 }
  *chk = checksum
  return *opc
206}
207
208func fn_emit(fd: i64, c1a: i64, c1b: i64, c2: i64, ns: *i64, am: *i64, fm: *i64, rt: *i64, chk: i64, ok: i64) -> i64 {
  fn_w(fd, "FNETGATE authored=organ kernel=fnet-fourier-mix metric=int-multiplies d=16" as *u8)
  fn_w(fd, " c1_fft_vs_dft_n8=" as *u8); fn_wn(fd, c1a)
  fn_w(fd, " c1_fft_vs_dft_n16=" as *u8); fn_wn(fd, c1b)
  fn_w(fd, " c2_twiddle_maxdiff_vs_nxfft=" as *u8); fn_wn(fd, c2)
  var i: i64 = 0
  while i < 4 {
      fn_w(fd, " | n=" as *u8); fn_wn(fd, ns[i])
      fn_w(fd, " attn_mul=" as *u8); fn_wn(fd, am[i])
      fn_w(fd, " fnet_mul=" as *u8); fn_wn(fd, fm[i])
      fn_w(fd, " ratio=" as *u8); fn_wn(fd, rt[i])
      i = i + 1
  }
  fn_w(fd, " work_chk=" as *u8); fn_wn(fd, chk)
  if ok == 1 { fn_w(fd, " verdict=GREEN\n" as *u8) } else { fn_w(fd, " verdict=RED\n" as *u8) }
  return 0
224}
225
226func main() -> i64 {
  var ok: i64 = 1
228
  // --- correctness ---
  let c1a: i64 = fn_c1_fft_vs_dft(8)
  let c1b: i64 = fn_c1_fft_vs_dft(16)
  let c2:  i64 = fn_c2_twiddle_match()
  if c1a > 32 { ok = 0 }              // bound ~ 4*n fixed-point accumulation; actuals reported
  if c1b > 64 { ok = 0 }
  if c2  > 1  { ok = 0 }              // synthesized twiddles within 1 Q14 unit of the shipped table
236
  // --- measured sub-quadratic crossover ---
  let d: i64 = 16
  let ns: *i64 = (sys_mmap(4 * 8)) as *i64
  ns[0] = 64; ns[1] = 256; ns[2] = 1024; ns[3] = 4096
  let am: *i64 = (sys_mmap(4 * 8)) as *i64
  let fm: *i64 = (sys_mmap(4 * 8)) as *i64
  let rt: *i64 = (sys_mmap(4 * 8)) as *i64
  let chkbox: *i64 = (sys_mmap(8)) as *i64
  var work_chk: i64 = 0
246
  var i: i64 = 0
  while i < 4 {
      let n: i64 = ns[i]
      let amul: i64 = fn_attn_measure(n, d, chkbox)
      work_chk = work_chk + *chkbox
      let fmul: i64 = fn_fnet_measure(n, d, chkbox)
      work_chk = work_chk + *chkbox
      am[i] = amul
      fm[i] = fmul
      rt[i] = amul / fmul
257
      // counter-faithfulness: measured count == structural closed form (proves the counters are real).
      let attn_expect: i64 = 2 * n * n * d + n * n
      let ln: i64 = nx_fft_log2(n)
      let ld: i64 = nx_fft_log2(d)
      let fnet_expect: i64 = 2 * n * d * (ld + ln)
      if amul != attn_expect { ok = 0 }
      if fmul != fnet_expect { ok = 0 }
265
      // exceed: fnet strictly cheaper at every n.
      if fmul >= amul { ok = 0 }
      i = i + 1
  }
270
  // crossover: the attn/fnet advantage STRICTLY GROWS with sequence length (quadratic vs linearithmic).
  if rt[1] <= rt[0] { ok = 0 }
  if rt[2] <= rt[1] { ok = 0 }
  if rt[3] <= rt[2] { ok = 0 }
275
  fn_emit(1, c1a, c1b, c2, ns, am, fm, rt, work_chk, ok)
  let lf: i64 = sys_openat_append(FN_LOG, 420)
  if lf >= 0 { fn_emit(lf, c1a, c1b, c2, ns, am, fm, rt, work_chk, ok); sys_close(lf) }
279
  // 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] = ok
  ctr__dry[1] = 1
  let rc__dry: i64 = gv_verdict("FNET-MIX-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
289}
nx_fnet_mix_gate.nx source

`nx_fnet_mix_gate.nx` source
