_gpu_compute_gate.nx source

1// _gpu_compute_gate.nx -- GPU-COMPUTE bit-identical CPU-vs-GPU gate (V-RAM-005 / X-DRV-003, the 2// CUDA-moat-escape thesis in miniature on the sovereign GPU-class device). Proves: 3// (1) GPU-COMPUTE -- the CANONICAL op-list emitter nx_drv_proto_emit, driven by gpu_compute_virt.spec 4// alone (zero emitter change), authors a SPIR-V-gated DOT8 compute driver; the sovereign rv64 emu 5// (+ rv64im_min_gpu) runs it: enable -> bind ring -> lay a DOT8 packet (SPIR-V magic + two int8 6// vectors a=[3,2,5,1] b=[4,6,1,2]) -> doorbell -> the device validates the SPIR-V magic, computes 7// dot=sum(a[i]*b[i]) and latches RESULTPEEK -> the driver reads it back == 0x1f. Serial CONTAINS 8// golden "GPUENRINGCMDDOT" + a clean halt. 9// (2) BIT-IDENTICAL -- the gate computes the SAME int8 dot product on the CPU (independent loop) and 10// asserts it == the value the GPU round-trip verified (0x1f=31). CPU lane == GPU lane, MEASURED. 11// (3) INPUT-TAMPER -- bump a[0] (3->4) in the spec, re-emit, re-run: the device computes a DIFFERENT 12// dot (35) so the driver's RESULTPEEK read-back verify fails -> the golden drops. This proves the 13// device REALLY computes from the input data (not a stuck constant) -- the no-false-green handle. 14// (4) DISTINCT -- the SAME emitter binary, driven by the echo GPU op-list, yields a different golden. 15// 16// Every verdict is a PRINTED marker off a REAL sovereign run; raw bytes read SOVEREIGNLY (sys_read). 17// NO qemu/gcc/openssl/python. Marker -> knowledge/status/driver_spec.log (GPUCOMPUTEGATE row). 18// Sovereign orchestration (fork/dup3/execve/wait4). license_tier: ORIGINAL 19import "nx_syscalls.nx" 20 21const EMIT_ELF: *u8 = "_offc/nx_drv_proto_emit.elf" 22const SOV_ELF: *u8 = "_offc/_gpu_run.elf" 23 24func q_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 25func q_fp(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 } 26func q_fn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{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{bb[i]=t[k-1-i];i=i+1}; sys_write(fd,bb,k); return 0 } 27 28func q_run1(prog: *u8, a1: *u8, outpath: *u8) -> i64 { 29 let pid: i64 = sys_fork() 30 if pid == 0 { 31 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 32 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 33 let argv: *i64 = sys_mmap(32) as *i64 34 argv[0] = prog as i64 35 argv[1] = a1 as i64 36 argv[2] = 0 37 let envp: *i64 = sys_mmap(16) as *i64 38 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0 39 sys_execve(prog, argv, envp) 40 sys_exit(127) 41 } 42 let st: *i64 = sys_mmap(16) as *i64 43 sys_wait4(pid, st, 0) 44 let sig: i64 = st[0] & 0x7f 45 if sig != 0 { return 128 + sig } 46 return (st[0] >> 8) & 0xff 47} 48 49func q_read(path: *u8, buf: *u8, cap: i64) -> i64 { 50 let fd: i64 = sys_openat_rd(path) 51 if fd < 0 { return 0 } 52 var n: i64 = 0 53 var go: i64 = 1 54 while go == 1 { let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n); if r <= 0 { go = 0 } else { n = n + r } if n >= cap - 1 { go = 0 } } 55 sys_close(fd) 56 return n 57} 58 59func q_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 60 if pl <= 0 { return 0 } 61 var i: i64 = 0 62 while i + pl <= n { 63 var k: i64 = 0; var hit: i64 = 1 64 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 65 if hit == 1 { return 1 } 66 i = i + 1 67 } 68 return 0 69} 70 71func q_strlen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } 72 73func q_streq(a: *u8, b: *u8) -> i64 { 74 var i: i64 = 0 75 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } 76 if b[i] != (0 as u8) { return 0 } 77 return 1 78} 79 80// emit a driver from spec, run it on the GPU sovereign emu; return 1 iff serial CONTAINS golden + halt. 81func q_emit_run(spec: *u8, out: *u8, goldout: *u8, gbuf: *u8, gcap: i64, serialpath: *u8) -> i64 { 82 let est: i64 = q_run1(EMIT_ELF, spec, "/tmp/_gpucmp_emit.out" as *u8) 83 if est != 0 { return 0 } 84 let gn: i64 = q_read(goldout, gbuf, gcap) 85 if gn <= 0 { return 0 } 86 gbuf[gn] = 0 as u8 87 let rst: i64 = q_run1(SOV_ELF, out, serialpath) 88 let sbuf: *u8 = sys_mmap(65536) 89 let sbn: i64 = q_read(serialpath, sbuf, 65536) 90 let has: i64 = q_buf_has(sbuf, sbn, gbuf, gn) 91 let halt: i64 = q_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21) 92 if rst == 0 { if has == 1 { if halt == 1 { return 1 } } } 93 return 0 94} 95 96func main() -> i64 { 97 q_p("=== GPU-compute bit-identical gate (V-RAM-005: SPIR-V-gated int8 dot product, CPU lane == GPU lane, sovereign emu, no qemu) ===\n" as *u8) 98 let lfd: i64 = sys_openat_append("knowledge/status/driver_spec.log" as *u8, 0x1a4) 99 100 let cmp_out: *u8 = "runtime/_hdl_build/_gpu_compute.bin" as *u8 101 let cmp_gold: *u8 = "runtime/_hdl_build/_gpu_compute.bin.gold" as *u8 102 let echo_out: *u8 = "runtime/_hdl_build/_gpu_dispatch.bin" as *u8 103 let echo_gold: *u8 = "runtime/_hdl_build/_gpu_dispatch.bin.gold" as *u8 104 105 let gC: *u8 = sys_mmap(2048) 106 let gE: *u8 = sys_mmap(2048) 107 108 // ---- (2) CPU reference: compute the SAME int8 dot product, independently, the same way ---- 109 let av: *i64 = sys_mmap(64) as *i64 110 let bv: *i64 = sys_mmap(64) as *i64 111 av[0] = 3; av[1] = 2; av[2] = 5; av[3] = 1 112 bv[0] = 4; bv[1] = 6; bv[2] = 1; bv[3] = 2 113 var cpu_dot: i64 = 0 114 var i: i64 = 0 115 while i < 4 { cpu_dot = cpu_dot + (av[i] * bv[i]); i = i + 1 } 116 let GPU_EXPECT: i64 = 0x1f // the value the driver's read-back verifies (baked in the spec) 117 var bit_identical: i64 = 0 118 if cpu_dot == GPU_EXPECT { bit_identical = 1 } 119 120 // ---- (1) GPU round-trip: the device computed the dot, the driver read it back == 0x1f ---- 121 let gpu_ok: i64 = q_emit_run("knowledge/specs/gpu_compute_virt.spec" as *u8, cmp_out, cmp_gold, gC, 2048, "/tmp/_gpucmp_serial.txt" as *u8) 122 123 // ---- (4) DISTINCT vs the echo GPU op-list (golden only) ---- 124 let eest: i64 = q_run1(EMIT_ELF, "knowledge/specs/gpu_dispatch_virt.spec" as *u8, "/tmp/_gpucmp_echo.out" as *u8) 125 let egn: i64 = q_read(echo_gold, gE, 2048) 126 if egn > 0 { gE[egn] = 0 as u8 } 127 var distinct: i64 = 0 128 if q_strlen(gC) > 0 { if q_strlen(gE) > 0 { if q_streq(gC, gE) == 0 { distinct = 1 } } } 129 130 // ---- (3) INPUT-TAMPER: bump a[0] 3->4 in the spec (the a-word 0x01050203 -> 0x01050204), re-emit, 131 // re-run. The device computes dot=35 != 31 -> the driver's RESULTPEEK verify fails -> golden drops. ---- 132 let sbuf: *u8 = sys_mmap(8192) 133 let sn: i64 = q_read("knowledge/specs/gpu_compute_virt.spec" as *u8, sbuf, 8192) 134 let pat: *u8 = "memstore 16 2 0x01050203" as *u8 135 let pl: i64 = q_strlen(pat) 136 var ppos: i64 = 0 - 1 137 var si: i64 = 0 138 while si + pl <= sn { 139 var kk: i64 = 0; var hh: i64 = 1 140 while kk < pl { if sbuf[si+kk] != pat[kk] { hh = 0; kk = pl } else { kk = kk + 1 } } 141 if hh == 1 { ppos = si; si = sn } else { si = si + 1 } 142 } 143 var input_tamper: i64 = 0 144 if ppos >= 0 { 145 sbuf[ppos + pl - 1] = 52 as u8 // last char '3' -> '4' (a[0] 3 -> 4, dot 31 -> 35) 146 let tfd: i64 = sys_openat_wr("/tmp/_gpucmp_tamper.spec" as *u8, 0x1a4) 147 if tfd >= 0 { sys_write(tfd, sbuf, sn); sys_close(tfd) } 148 // the tampered spec's `out` still points at cmp_out -> re-emitting OVERWRITES it; run + check. 149 let tet: i64 = q_run1(EMIT_ELF, "/tmp/_gpucmp_tamper.spec" as *u8, "/tmp/_gpucmp_temit.out" as *u8) 150 let trst: i64 = q_run1(SOV_ELF, cmp_out, "/tmp/_gpucmp_tserial.txt" as *u8) 151 let tbuf: *u8 = sys_mmap(65536) 152 let tbn: i64 = q_read("/tmp/_gpucmp_tserial.txt" as *u8, tbuf, 65536) 153 let drops: i64 = q_buf_has(tbuf, tbn, gC, q_strlen(gC)) // full golden should MISS 154 if tet == 0 { if trst == 0 { if drops == 0 { input_tamper = 1 } } } 155 // restore the clean image (re-emit the real spec). 156 q_run1(EMIT_ELF, "knowledge/specs/gpu_compute_virt.spec" as *u8, "/tmp/_gpucmp_emit.out" as *u8) 157 } 158 159 q_p(" gpu_compute=" as *u8) 160 if gpu_ok == 1 { q_p("GREEN(GPU..DOT: SPIR-V-gated int8 dot product round-trip, clean halt)" as *u8) } else { q_p("RED" as *u8) } 161 q_p(" bit_identical=" as *u8) 162 if bit_identical == 1 { q_p("yes(cpu_dot==gpu_readback==" as *u8); q_fn(1, cpu_dot); q_p(")" as *u8) } else { q_p("no(cpu_dot=" as *u8); q_fn(1, cpu_dot); q_p(")" as *u8) } 163 q_p(" input_tamper=" as *u8) 164 if input_tamper == 1 { q_p("rejected(a[0] bumped -> dot changes -> readback fails -> golden drops)" as *u8) } else { q_p("not-rejected" as *u8) } 165 q_p(" distinct=" as *u8) 166 if distinct == 1 { q_p("yes\n" as *u8) } else { q_p("no\n" as *u8) } 167 168 var pass: i64 = 0 169 if gpu_ok == 1 { if bit_identical == 1 { if input_tamper == 1 { if distinct == 1 { pass = 1 } } } } 170 171 if pass == 1 { 172 q_p("GPUCOMPUTEGATE verdict=GREEN (the canonical op-list emitter authored a SPIR-V-gated int8 DOT8 compute driver from gpu_compute_virt.spec; the sovereign GPU device computed the matmul-primitive dot product, the driver read it back, and it is BIT-IDENTICAL to the independent CPU reference (==31); an input tamper changed the device result and was REJECTED -- real compute, not a stuck constant. The sovereign GPU-compute / CUDA-moat-escape lane (V-RAM-005) is proven in miniature)\n" as *u8) 173 if lfd >= 0 { 174 q_fp(lfd, "GPUCOMPUTEGATE verdict=GREEN keystone=gpu-compute-bit-identical-cpu-vs-gpu runtime=sovereign-emu device=gpu-class kernel=int8-dot4(matmul-primitive) spirv-gated=0x07230203 cpu_dot=gpu_readback=" as *u8); q_fn(lfd, cpu_dot) 175 q_fp(lfd, " input_tamper=rejected distinct=yes emitter=nx_drv_proto_emit(zero-change) composes=spirv-lane(V-RAM-005) epoch=" as *u8); q_fn(lfd, sys_now_realtime_sec()); q_fp(lfd, "\n" as *u8); sys_close(lfd) 176 } 177 sys_exit(0); return 0 178 } 179 q_p("GPUCOMPUTEGATE verdict=RED (gpu_ok/bit_identical/input_tamper/distinct not all green)\n" as *u8) 180 if lfd >= 0 { 181 q_fp(lfd, "GPUCOMPUTEGATE verdict=RED gpu_ok=" as *u8); q_fn(lfd, gpu_ok) 182 q_fp(lfd, " bit_identical=" as *u8); q_fn(lfd, bit_identical) 183 q_fp(lfd, " input_tamper=" as *u8); q_fn(lfd, input_tamper) 184 q_fp(lfd, " distinct=" as *u8); q_fn(lfd, distinct); q_fp(lfd, "\n" as *u8); sys_close(lfd) 185 } 186 sys_exit(1) 187 return 1 188}