nx_synth_test.nx source

1// nx_synth_test.nx -- watch the team WRITE programs from specs. Each target is given 2// ONLY as input/output examples; the synthesizer discovers a program, which is then 3// checked on HELD-OUT inputs (so it generalizes -- not memorised). I wrote no 4// program here; the search wrote all of them. Known answer: every target synthesized 5// + held-out-verified -> exit 0. 6 7import "nx_synth.nx" 8 9func sy_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 10func sy_num(v: i64) -> i64 { 11 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 12 let t: *u8 = sys_mmap(28); var k: i64 = 0 13 if m == 0 { t[0] = 48; k = 1 } 14 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 15 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 16 sys_write(1, b, k); return 0 17} 18func sy_opname(o: i64) -> *u8 { 19 if o == OP_ADD { return "add" as *u8 } 20 if o == OP_SUB { return "sub" as *u8 } 21 if o == OP_MUL { return "mul" as *u8 } 22 return "shl" as *u8 23} 24func sy_describe(op: *i64, a: *i64, b: *i64, L: i64) -> i64 { 25 var t: i64 = 0 26 while t < L { 27 sy_puts(" s" as *u8); sy_num(t + 2); sy_puts("=" as *u8); sy_puts(sy_opname(op[t])) 28 sy_puts("(s" as *u8); sy_num(a[t]); sy_puts("," as *u8) 29 if op[t] == OP_SHL { sy_puts("#" as *u8); sy_num(b[t]) } else { sy_puts("s" as *u8); sy_num(b[t]) } 30 sy_puts(")" as *u8) 31 t = t + 1 32 } 33 return 0 34} 35 36// the targets -- the synthesizer NEVER sees these formulas, only their outputs. 37func sy_target(id: i64, x: i64) -> i64 { 38 if id == 0 { return x * 7 } 39 if id == 1 { return x * x } 40 if id == 2 { return x * x + x } 41 if id == 3 { return x + 1 } 42 if id == 4 { return x + x } 43 return 0 44} 45func sy_name(id: i64) -> *u8 { 46 if id == 0 { return "f(x)=x*7" as *u8 } 47 if id == 1 { return "f(x)=x*x" as *u8 } 48 if id == 2 { return "f(x)=x*x+x" as *u8 } 49 if id == 3 { return "f(x)=x+1" as *u8 } 50 return "f(x)=2x" as *u8 51} 52 53func main() -> i64 { 54 sy_puts("=== the team WRITES programs from input/output examples (synthesis) ===\n" as *u8) 55 let ex_x: *i64 = sys_mmap(8 * 32) as *i64 56 let ex_y: *i64 = sys_mmap(8 * 32) as *i64 57 let op: *i64 = sys_mmap(8 * 4) as *i64 58 let a: *i64 = sys_mmap(8 * 4) as *i64 59 let b: *i64 = sys_mmap(8 * 4) as *i64 60 61 var written: i64 = 0 62 var generalized: i64 = 0 63 let ntargets: i64 = 5 64 var id: i64 = 0 65 while id < ntargets { 66 // spec = 24 examples x=0..23 (kept small so x*x fits sane ranges). 67 var nex: i64 = 0 68 var x: i64 = 0 69 while x < 24 { ex_x[nex] = x; ex_y[nex] = sy_target(id, x); nex = nex + 1; x = x + 1 } 70 71 let L: i64 = synth_find(ex_x, ex_y, nex, op, a, b) // WRITE the program 72 sy_puts(" " as *u8); sy_puts(sy_name(id)); sy_puts(" ->" as *u8) 73 if L == 0 { sy_puts(" (not found in bound)\n" as *u8); id = id + 1; } 74 else { 75 written = written + 1 76 sy_describe(op, a, b, L) 77 // verify on HELD-OUT inputs x=30..49 (never in the spec). 78 var ok: i64 = 1 79 var hx: i64 = 30 80 let syc: *i64 = sys_mmap(8 * 8) 81 while hx < 50 { if synth_eval(op, a, b, L, hx, syc) != sy_target(id, hx) { ok = 0 } hx = hx + 1 } 82 if ok == 1 { generalized = generalized + 1; sy_puts(" [held-out OK]\n" as *u8) } 83 else { sy_puts(" [OVERFIT -- held-out FAIL]\n" as *u8) } 84 id = id + 1 85 } 86 } 87 88 sy_puts("----------------------------------------------------------------\n" as *u8) 89 sy_puts(" programs WRITTEN by search: " as *u8); sy_num(written); sy_puts("/" as *u8); sy_num(ntargets) 90 sy_puts(" generalized (held-out): " as *u8); sy_num(generalized); sy_puts("/" as *u8); sy_num(ntargets); sy_puts("\n" as *u8) 91 sy_puts(" the team discovered each program from the goal -- I wrote no program here.\n" as *u8) 92 93 if written != ntargets { sys_exit(1); return 1 } 94 if generalized != ntargets { sys_exit(2); return 2 } 95 sys_exit(0) 96 return 0 97}