nx_synth_oe_test.nx source

1// nx_synth_oe_test.nx -- scale + EXCEED for the synthesizer, measured. The 2// observational-equivalence synthesizer reaches DEPTH-3 programs the naive <=2 3// enumerator (nx_synth) cannot, and we MEASURE the pruning that makes it possible: 4// candidates tried (P) vs distinct behaviours kept (V). P/V is the collapse the 5// SOTA technique buys -- A/B on the same task. Each synthesized program is checked 6// on HELD-OUT inputs (not in the spec). Known answer: all targets found, held-out 7// verified, at least one is depth-3, and V < P (dedup working) -> exit 0. 8 9import "nx_synth_oe.nx" 10 11func oe_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 12func oe_num(v: i64) -> i64 { 13 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 14 let t: *u8 = sys_mmap(28); var k: i64 = 0 15 if m == 0 { t[0] = 48; k = 1 } 16 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 17 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 18 sys_write(1, b, k); return 0 19} 20func oe_depth(c: *SoeCtx, v: i64) -> i64 { 21 if c.kind[v] != 2 { return 0 } 22 if c.op[v] == SOE_SHL { return 1 + oe_depth(c, c.pa[v]) } 23 var da: i64 = oe_depth(c, c.pa[v]) 24 var db: i64 = oe_depth(c, c.pb[v]) 25 if db > da { da = db } 26 return 1 + da 27} 28 29func oe_target(id: i64, x: i64) -> i64 { 30 if id == 0 { return x * x + x } // depth 2 31 if id == 1 { return x * x * x + x * x } // depth 3 (x^3 + x^2) 32 if id == 2 { return x * x * x * x } // x^4 33 return x * x * x + 1 // depth 3 (x^3 + 1) 34} 35func oe_name(id: i64) -> *u8 { 36 if id == 0 { return "x^2+x " as *u8 } 37 if id == 1 { return "x^3+x^2" as *u8 } 38 if id == 2 { return "x^4 " as *u8 } 39 return "x^3+1 " as *u8 40} 41 42func main() -> i64 { 43 oe_puts("=== synthesizer scaled: observational-equivalence, depth-3+, MEASURED ===\n" as *u8) 44 let nex: i64 = 8 45 let c: *SoeCtx = soe_new(nex) 46 let ex_x: *i64 = sys_mmap(8 * 16) as *i64 47 let ex_y: *i64 = sys_mmap(8 * 16) as *i64 48 49 var found_all: i64 = 0 50 var gen_all: i64 = 0 51 var depth3: i64 = 0 52 var prune_ok: i64 = 0 53 let nt: i64 = 4 54 var id: i64 = 0 55 while id < nt { 56 var i: i64 = 0 57 while i < nex { ex_x[i] = i; ex_y[i] = oe_target(id, i); i = i + 1 } // spec: x=0..7 58 let root: i64 = soe_synth(c, ex_x, ex_y, nex, 4) 59 oe_puts(" " as *u8); oe_puts(oe_name(id)) 60 if root < 0 { oe_puts(" NOT FOUND\n" as *u8) } 61 else { 62 found_all = found_all + 1 63 let d: i64 = oe_depth(c, root) 64 if d >= 3 { depth3 = depth3 + 1 } 65 // held-out check x=8..15 66 var ok: i64 = 1 67 var hx: i64 = 8 68 while hx < 16 { if soe_eval(c, root, hx) != oe_target(id, hx) { ok = 0 } hx = hx + 1 } 69 if ok == 1 { gen_all = gen_all + 1 } 70 if c.nval < c.tried { prune_ok = prune_ok + 1 } 71 oe_puts(" depth=" as *u8); oe_num(d) 72 oe_puts(" tried(P)=" as *u8); oe_num(c.tried) 73 oe_puts(" kept(V)=" as *u8); oe_num(c.nval) 74 oe_puts(" prune P/V=" as *u8); if c.nval > 0 { oe_num(c.tried / c.nval) } 75 if ok == 1 { oe_puts("x held-out OK\n" as *u8) } else { oe_puts("x HELD-OUT FAIL\n" as *u8) } 76 } 77 id = id + 1 78 } 79 80 oe_puts("----------------------------------------------------------------\n" as *u8) 81 oe_puts(" found " as *u8); oe_num(found_all); oe_puts("/" as *u8); oe_num(nt) 82 oe_puts(" generalized " as *u8); oe_num(gen_all); oe_puts("/" as *u8); oe_num(nt) 83 oe_puts(" depth>=3 " as *u8); oe_num(depth3); oe_puts("\n" as *u8) 84 oe_puts(" observational equivalence collapses many tried programs to few distinct\n" as *u8) 85 oe_puts(" behaviours -- reaching depths the naive <=2 enumerator never could.\n" as *u8) 86 87 // GATE: all found + generalized, at least one depth-3 (scaled past naive), and 88 // the pruning is real (V < P) on every target. 89 if found_all != nt { sys_exit(1); return 1 } 90 if gen_all != nt { sys_exit(2); return 2 } 91 if depth3 < 1 { sys_exit(3); return 3 } 92 if prune_ok != nt { sys_exit(4); return 4 } 93 sys_exit(0) 94 return 0 95}