nx_synth.nx source

1// nx_synth.nx -- a PROGRAM SYNTHESIZER: the team WRITES a program from a spec, by 2// search. Given only input/output examples (NOT the formula), it enumerates small 3// straight-line programs over {ADD,SUB,MUL,SHL} and returns the shortest one that 4// reproduces every example -- then the caller checks it on held-out inputs so it is 5// a real program, not an overfit. This is "writing code on its own": the search 6// discovers the program; I only wrote the searcher + the DSL. 7// 8// Enumerative program synthesis (Massalin superoptimizer, AFIPS 1987; modern: CEGIS 9// -- Solar-Lezama, ASPLOS 2006). Slots: 0=x (input), 1=1 (a constant), 2.. computed. 10// Bounded to length <= 2 over a few ops -- small, but genuinely authored from a goal. 11 12import "nx_syscalls.nx" 13 14const OP_ADD: i64 = 0 15const OP_SUB: i64 = 1 16const OP_MUL: i64 = 2 17const OP_SHL: i64 = 3 18 19// run a candidate program on input x. op/a/b are L-element arrays. For SHL, b[t] is 20// an immediate shift; for the others b[t] is a slot index. Result = last slot. 21// s = caller scratch (size >= L+4), reused across millions of calls (allocating 22// here would mmap per eval and exhaust the address space). 23func synth_eval(op: *i64, a: *i64, b: *i64, L: i64, x: i64, s: *i64) -> i64 { 24 s[0] = x 25 s[1] = 1 26 var t: i64 = 0 27 while t < L { 28 let o: i64 = op[t] 29 let va: i64 = s[a[t]] 30 var r: i64 = 0 31 if o == OP_ADD { r = va + s[b[t]] } 32 if o == OP_SUB { r = va - s[b[t]] } 33 if o == OP_MUL { r = va * s[b[t]] } 34 if o == OP_SHL { r = va << b[t] } 35 s[t + 2] = r 36 t = t + 1 37 } 38 return s[L + 1] 39} 40 41func synth_matches(op: *i64, a: *i64, b: *i64, L: i64, ex_x: *i64, ex_y: *i64, nex: i64, s: *i64) -> i64 { 42 var k: i64 = 0 43 while k < nex { 44 if synth_eval(op, a, b, L, ex_x[k], s) != ex_y[k] { return 0 } 45 k = k + 1 46 } 47 return 1 48} 49 50// SEARCH: find the shortest program (L=1 then L=2) matching all examples. Writes it 51// into op/a/b and returns L, or 0 if none found within the bound. 52func synth_find(ex_x: *i64, ex_y: *i64, nex: i64, op: *i64, a: *i64, b: *i64) -> i64 { 53 let s: *i64 = sys_mmap(8 * 8) // one scratch, reused across the whole search 54 // ---- L = 1 : slot2 = OP(slot a, slot/imm b), operands from slots {0,1} ---- 55 var o1: i64 = 0 56 while o1 < 4 { 57 var a1: i64 = 0 58 while a1 < 2 { 59 var bmax: i64 = 2 60 if o1 == OP_SHL { bmax = 6 } 61 var b1: i64 = 0 62 while b1 < bmax { 63 op[0] = o1; a[0] = a1; b[0] = b1 64 if synth_matches(op, a, b, 1, ex_x, ex_y, nex, s) == 1 { return 1 } 65 b1 = b1 + 1 66 } 67 a1 = a1 + 1 68 } 69 o1 = o1 + 1 70 } 71 // ---- L = 2 : slot2 = OP1(.. slots 0,1); slot3 = OP2(.. slots 0,1,2) ---- 72 o1 = 0 73 while o1 < 4 { 74 var a1: i64 = 0 75 while a1 < 2 { 76 var bm1: i64 = 2 77 if o1 == OP_SHL { bm1 = 6 } 78 var b1: i64 = 0 79 while b1 < bm1 { 80 var o2: i64 = 0 81 while o2 < 4 { 82 var a2: i64 = 0 83 while a2 < 3 { 84 var bm2: i64 = 3 85 if o2 == OP_SHL { bm2 = 6 } 86 var b2: i64 = 0 87 while b2 < bm2 { 88 op[0] = o1; a[0] = a1; b[0] = b1 89 op[1] = o2; a[1] = a2; b[1] = b2 90 if synth_matches(op, a, b, 2, ex_x, ex_y, nex, s) == 1 { return 2 } 91 b2 = b2 + 1 92 } 93 a2 = a2 + 1 94 } 95 o2 = o2 + 1 96 } 97 b1 = b1 + 1 98 } 99 a1 = a1 + 1 100 } 101 o1 = o1 + 1 102 } 103 return 0 104}