nx_nn_gate.nx source

1// nx_nn_gate.nx -- proves the sovereign fixed-point neural inference substrate (nx_nn): a 2-layer MLP forward pass 2// computes a KNOWN function bit-exactly, and the Q-scale descaling is correct. This is the inference machinery the 3// neural PLC / learned RVQ codebook runs on the phone CPU; with trained weights it becomes the net. 4import "nx_syscalls.nx" 5import "nx_gate_emit_lib.nx" 6import "nx_nn.nx" 7 8func main() -> i64 { 9 g_puts("nx_nn gate (fixed-point neural inference substrate: a known 2-layer MLP, MEASURED)\n" as *u8) 10 var pass: i64 = 0; var total: i64 = 0 11 12 // input vector (I=4) 13 let inp: *i64 = sys_mmap(4*8) as *i64 14 inp[0]=3; inp[1]=0-2; inp[2]=5; inp[3]=0-1 15 // Layer 1: W1 = identity (4x4), b1 = 0, Qshift 0 -> h_pre = in; then ReLU -> h = [3,0,5,0] 16 let W1: *i64 = sys_mmap(16*8) as *i64 17 var i: i64=0; while i<16 { W1[i]=0; i=i+1 } 18 W1[0]=1; W1[5]=1; W1[10]=1; W1[15]=1 19 let b1: *i64 = sys_mmap(4*8) as *i64 20 i=0; while i<4 { b1[i]=0; i=i+1 } 21 let h: *i64 = sys_mmap(4*8) as *i64 22 nn_linear(inp, 4, W1, b1, 4, 0, h) 23 nn_relu(h, 4) 24 // Layer 2: W2 row0 = [1,1,1,1] (sum), row1 = [1,0,1,0] (select), b2 = [0,0] -> out = [3+0+5+0, 3+5] = [8,8] 25 let W2: *i64 = sys_mmap(8*8) as *i64 26 W2[0]=1; W2[1]=1; W2[2]=1; W2[3]=1 27 W2[4]=1; W2[5]=0; W2[6]=1; W2[7]=0 28 let b2: *i64 = sys_mmap(2*8) as *i64 29 b2[0]=0; b2[1]=0 30 let out: *i64 = sys_mmap(2*8) as *i64 31 nn_linear(h, 4, W2, b2, 2, 0, out) 32 33 g_puts(" [measure] in=[3,-2,5,-1] -> ReLU(in)=[" as *u8); g_pn(h[0]); g_puts("," as *u8); g_pn(h[1]); g_puts("," as *u8); g_pn(h[2]); g_puts("," as *u8); g_pn(h[3]); g_puts("] -> MLP out=[" as *u8); g_pn(out[0]); g_puts("," as *u8); g_pn(out[1]); g_puts("] (expect [8,8])\n" as *u8) 34 35 pass = pass + g_check("ReLU layer correct (negatives zeroed: h=[3,0,5,0])" as *u8, (h[0]==3) & (h[1]==0) & (h[2]==5) & (h[3]==0)); total=total+1 36 pass = pass + g_check("2-layer MLP forward pass computes the known function (out=[8,8])" as *u8, (out[0]==8) & (out[1]==8)); total=total+1 37 38 // Q-scale descaling: in=[2,3] Q8 (=512,768), W=[256,256] (=1.0 each, Q8), Qshift 8, b=0 -> out = (512*256+768*256)>>8 = 2+3 = 5 (Q0)... in Q8 = (a) (512+768)=1280 in Q8 = 5.0 39 let qin: *i64 = sys_mmap(2*8) as *i64; qin[0]=512; qin[1]=768 // 2.0, 3.0 in Q8 40 let qW: *i64 = sys_mmap(2*8) as *i64; qW[0]=256; qW[1]=256 // 1.0, 1.0 in Q8 41 let qb: *i64 = sys_mmap(1*8) as *i64; qb[0]=0 42 let qout: *i64 = sys_mmap(1*8) as *i64 43 nn_linear(qin, 2, qW, qb, 1, 8, qout) // (512*256 + 768*256)>>8 = 1280 (= 5.0 in Q8) 44 g_puts(" [measure] Q8 layer: 2.0*1.0 + 3.0*1.0 = " as *u8); g_pn(qout[0]); g_puts(" (Q8; 1280 = 5.0)\n" as *u8) 45 pass = pass + g_check("fixed-point Q-scale descaling correct (1280 = 5.0 in Q8)" as *u8, qout[0] == 1280); total=total+1 46 47 g_puts("---- nn gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 48 if pass == total { g_puts("verdict=GREEN\n" as *u8); sys_exit(0); return 0 } 49 g_puts("verdict=RED\n" as *u8); sys_exit(1); return 1 50}