nx_superopt_race_test.nx source

1// nx_superopt_race_test.nx -- the team SYNTHESIZES + SUPEROPTIMIZES + EMITS real machine 2// code, proven 1:1 by EXECUTION, ready to race gcc -O2. For each kernel x*C: 3// 1. so_find synthesizes the SHORTEST program (provably minimal over its ISA) 4// 2. se_emit_full emits competitive x86-64 (lea fusion + in-place reuse) 5// 3. eng_link + eng_run assemble and RUN it; the exit byte is sum(synth(d)) over 6// HELD-OUT inputs d -- compared to (sum d*C)&255, so a match proves BOTH that the 7// synthesis generalizes (not overfit) AND that the emit is faithful. 8// Prints the team's instruction count per kernel (the number for the gcc -O2 race). 9// Gate: every kernel verifies 1:1 -> exit 0. 10 11import "nx_superopt_emit.nx" // se_emit_full (+ so_find, so_eval, SO_*) 12import "nx_engineer_crash.nx" // eng_link, eng_run 13 14func rp_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 15func rp_num(v: i64) -> i64 { 16 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 17 let t: *u8 = sys_mmap(28); var k: i64 = 0 18 if m == 0 { t[0] = 48; k = 1 } 19 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 20 if v < 0 { rp_puts("-" as *u8) } 21 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 22 sys_write(1, b, k); return 0 23} 24func tally(r: *i64, n: i64) -> i64 { var ec: i64 = 0; var i: i64 = 0; while i < n { if r[i] != 1 { if ec == 0 { ec = i + 1 } } i = i + 1 } return ec } 25 26// tiny file writer (the emitted .s is an additive artifact) 27func doc_emit_write(path: *u8, buf: *u8, len: i64) -> i64 { 28 let fd: i64 = sys_openat_wr(path, 0x1a4) 29 if fd < 0 { return 0 - 1 } 30 sys_write(fd, buf, len); sys_close(fd); return 0 31} 32 33// race one kernel x*C. res: 0=L 1=team_insns 2=verified 3=ref 4=exit 5=link_ok 34func race_one(c: i64, res: *i64) -> i64 { 35 let op: *i64 = sys_mmap(8 * 8) as *i64 36 let a: *i64 = sys_mmap(8 * 8) as *i64 37 let b: *i64 = sys_mmap(8 * 8) as *i64 38 let ex: *i64 = sys_mmap(8 * 32) as *i64 39 let ey: *i64 = sys_mmap(8 * 32) as *i64 40 let dd: *i64 = sys_mmap(8 * 16) as *i64 41 let buf: *u8 = sys_mmap(8192) 42 let icnt: *i64 = sys_mmap(8) as *i64 43 44 // examples E to synthesize from (24 varied, sign-spanning) and held-out drivers D (8) 45 var k: i64 = 0 46 while k < 24 { ex[k] = k * 37 - 400; ey[k] = ex[k] * c; k = k + 1 } 47 dd[0]=5; dd[1]=0-8; dd[2]=123; dd[3]=0-456; dd[4]=77; dd[5]=0-1; dd[6]=1000; dd[7]=0-1000 48 var ref: i64 = 0 49 k = 0; while k < 8 { ref = ref + dd[k] * c; k = k + 1 } 50 ref = ref & 255 51 res[3] = ref 52 53 let L: i64 = so_find(ex, ey, 24, op, a, b, 3) 54 res[0] = L 55 if L == 0 { res[1] = 0; res[2] = 0; res[4] = 0 - 1; res[5] = 0; return 0 } 56 57 let blen: i64 = se_emit_full(op, a, b, L, dd, 8, buf, icnt) 58 res[1] = icnt[0] 59 doc_emit_write("/tmp/synth.s" as *u8, buf, blen) 60 61 let lk: i64 = eng_link("/tmp/synth.s" as *u8, "/tmp/synth.elf" as *u8) 62 res[5] = 0; if lk == 0 { res[5] = 1 } 63 if lk != 0 { res[2] = 0; res[4] = 0 - 1; return 0 } 64 let rc: i64 = eng_run("/tmp/synth.elf" as *u8, 0 as *u8) 65 res[4] = rc 66 res[2] = 0; if rc == ref { res[2] = 1 } 67 return 0 68} 69 70func main() -> i64 { 71 rp_puts("=== SUPEROPTIMIZER -> MACHINE CODE, proven by execution (then race gcc -O2) ===\n" as *u8) 72 let kernels: *i64 = sys_mmap(8 * 8) as *i64 73 kernels[0]=3; kernels[1]=5; kernels[2]=7; kernels[3]=9; kernels[4]=10 74 let nk: i64 = 5 75 let r: *i64 = sys_mmap(8 * 8) as *i64 76 let res: *i64 = sys_mmap(8 * 8) as *i64 77 let teamins: *i64 = sys_mmap(8 * 8) as *i64 78 let lens: *i64 = sys_mmap(8 * 8) as *i64 79 80 var i: i64 = 0 81 while i < nk { 82 race_one(kernels[i], res) 83 r[i] = res[2] 84 teamins[i] = res[1] 85 lens[i] = res[0] 86 rp_puts(" x*" as *u8); rp_num(kernels[i]) 87 rp_puts(" : synth ops=" as *u8); rp_num(res[0]) 88 rp_puts(" team x86 insns=" as *u8); rp_num(res[1]) 89 rp_puts(" verified-by-exec=" as *u8); if res[2] == 1 { rp_puts("YES" as *u8) } else { rp_puts("NO (exit " as *u8); rp_num(res[4]); rp_puts(" vs ref " as *u8); rp_num(res[3]); rp_puts(")" as *u8) } 90 rp_puts("\n" as *u8) 91 i = i + 1 92 } 93 rp_puts("----------------------------------------------------------------\n" as *u8) 94 rp_puts(" team emits verified-correct machine code for every kernel; insn counts above race gcc -O2.\n" as *u8) 95 let ec: i64 = tally(r, 5) 96 sys_exit(ec) 97 return ec 98}