nx_synth_oe.nx source

1// nx_synth_oe.nx -- the synthesizer SCALED to S-class technique: bottom-up 2// enumerative synthesis with OBSERVATIONAL-EQUIVALENCE pruning. Two sub-programs 3// that produce the SAME output vector on the example inputs are interchangeable, so 4// only ONE representative per distinct behaviour is kept. The search is then bounded 5// by the number of distinct BEHAVIOURS, not the (exponential) number of programs -- 6// the exact technique SOTA program synthesizers use to scale, and it lets us reach 7// depth-3+ programs the naive <=2 enumerator never could. 8// 9// Research: Udupa et al., "TRANSIT: Specifying Protocols with Concolic Snippets," 10// PLDI 2013 (observational equivalence); Alur et al., EUSolver / SyGuS; Massalin, 11// AFIPS 1987 (superoptimizer). Exceed is MEASURED: candidates tried (P) vs distinct 12// values kept (V); P/V is the collapse the pruning buys, A/B on the same task. 13 14import "nx_syscalls.nx" 15const SOE_MAGIC_3750763034362895579: i64 = 3750763034362895579 16const SOE_MAGIC_1099511628211: i64 = 1099511628211 17 18const SOE_ADD: i64 = 0 19const SOE_SUB: i64 = 1 20const SOE_MUL: i64 = 2 21const SOE_SHL: i64 = 3 22 23const SOE_MAXV: i64 = 4000 24const SOE_HT: i64 = 16384 // power of two 25 26struct SoeCtx { 27 vecs: *i64, // MAXV * nex (output vector per value) 28 kind: *i64, // 0=leaf-x, 1=leaf-const, 2=op 29 op: *i64, 30 pa: *i64, 31 pb: *i64, 32 lit: *i64, 33 ht: *i64, // hash table -> value index, or -1 34 nval: i64, 35 nex: i64, 36 tried: i64, // P: candidate combinations evaluated 37 found: i64, // value index of the target, or -1 38 target: *i64, // target output vector 39} 40 41// recursively evaluate the program rooted at value v on input x (for held-out check). 42func soe_eval(c: *SoeCtx, v: i64, x: i64) -> i64 { 43 let k: i64 = c.kind[v] 44 if k == 0 { return x } 45 if k == 1 { return c.lit[v] } 46 let o: i64 = c.op[v] 47 if o == SOE_SHL { return soe_eval(c, c.pa[v], x) << c.lit[v] } 48 let a: i64 = soe_eval(c, c.pa[v], x) 49 let b: i64 = soe_eval(c, c.pb[v], x) 50 if o == SOE_ADD { return a + b } 51 if o == SOE_SUB { return a - b } 52 if o == SOE_MUL { return a * b } 53 return 0 54} 55 56func soe_hash(tmp: *i64, nex: i64) -> i64 { 57 var h: i64 = 0 - SOE_MAGIC_3750763034362895579 58 var i: i64 = 0 59 while i < nex { h = h ^ tmp[i]; h = h * SOE_MAGIC_1099511628211; i = i + 1 } 60 if h < 0 { h = 0 - h } 61 return h 62} 63func soe_vec_eq(c: *SoeCtx, v: i64, tmp: *i64) -> i64 { 64 var i: i64 = 0 65 let base: i64 = (c.vecs as i64) + v * c.nex * 8 66 while i < c.nex { let p: *i64 = (base + i * 8) as *i64; if p[0] != tmp[i] { return 0 } i = i + 1 } 67 return 1 68} 69// returns existing value idx with vec==tmp, or -1. 70func soe_lookup(c: *SoeCtx, tmp: *i64) -> i64 { 71 var slot: i64 = soe_hash(tmp, c.nex) & (SOE_HT - 1) 72 var guard: i64 = 0 73 while guard < SOE_HT { 74 let v: i64 = c.ht[slot] 75 if v < 0 { return 0 - 1 } 76 if soe_vec_eq(c, v, tmp) == 1 { return v } 77 slot = (slot + 1) & (SOE_HT - 1) 78 guard = guard + 1 79 } 80 return 0 - 1 81} 82// insert tmp as a NEW value with the given program info; returns its index (or -1 if full). 83func soe_insert(c: *SoeCtx, tmp: *i64, kind: i64, op: i64, pa: i64, pb: i64, lit: i64) -> i64 { 84 if c.nval >= SOE_MAXV { return 0 - 1 } 85 let v: i64 = c.nval 86 let base: i64 = (c.vecs as i64) + v * c.nex * 8 87 var i: i64 = 0 88 while i < c.nex { let p: *i64 = (base + i * 8) as *i64; p[0] = tmp[i]; i = i + 1 } 89 c.kind[v] = kind; c.op[v] = op; c.pa[v] = pa; c.pb[v] = pb; c.lit[v] = lit 90 c.nval = v + 1 91 var slot: i64 = soe_hash(tmp, c.nex) & (SOE_HT - 1) 92 while c.ht[slot] >= 0 { slot = (slot + 1) & (SOE_HT - 1) } 93 c.ht[slot] = v 94 // target check 95 if soe_vec_eq(c, v, c.target) == 1 { if c.found < 0 { c.found = v } } 96 return v 97} 98 99// add a candidate vector (already computed in tmp): dedupe, insert if new. 100func soe_offer(c: *SoeCtx, tmp: *i64, op: i64, pa: i64, pb: i64, lit: i64) -> i64 { 101 c.tried = c.tried + 1 102 if soe_lookup(c, tmp) >= 0 { return 0 } 103 soe_insert(c, tmp, 2, op, pa, pb, lit) 104 return 0 105} 106 107// bottom-up synthesis: build distinct behaviours until the target appears or rounds 108// are exhausted. ex_x/ex_y are the spec; returns the root value idx or -1. 109func soe_synth(c: *SoeCtx, ex_x: *i64, ex_y: *i64, nex: i64, rounds: i64) -> i64 { 110 c.nex = nex; c.nval = 0; c.tried = 0; c.found = 0 - 1 111 var i: i64 = 0 112 while i < SOE_HT { c.ht[i] = 0 - 1; i = i + 1 } 113 let tmp: *i64 = sys_mmap(8 * nex) 114 // target vector 115 i = 0; while i < nex { c.target[i] = ex_y[i]; i = i + 1 } 116 // leaves: x, const 1 117 i = 0; while i < nex { tmp[i] = ex_x[i]; i = i + 1 } 118 soe_insert(c, tmp, 0, 0, 0, 0, 0) // leaf x 119 i = 0; while i < nex { tmp[i] = 1; i = i + 1 } 120 soe_insert(c, tmp, 1, 0, 0, 0, 1) // leaf const 1 121 if c.found >= 0 { return c.found } 122 123 var r: i64 = 0 124 while r < rounds { 125 let start: i64 = c.nval 126 var u: i64 = 0 127 while u < start { 128 // SHL u by imm 1..5 129 var sh: i64 = 1 130 while sh < 6 { 131 var j: i64 = 0 132 while j < nex { let pu: *i64 = ((c.vecs as i64) + u * nex * 8 + j * 8) as *i64; tmp[j] = pu[0] << sh; j = j + 1 } 133 soe_offer(c, tmp, SOE_SHL, u, 0, sh) 134 sh = sh + 1 135 } 136 var v: i64 = 0 137 while v < start { 138 var oo: i64 = 0 139 while oo < 3 { 140 var j: i64 = 0 141 while j < nex { 142 let pu: *i64 = ((c.vecs as i64) + u * nex * 8 + j * 8) as *i64 143 let pv: *i64 = ((c.vecs as i64) + v * nex * 8 + j * 8) as *i64 144 var rr: i64 = 0 145 if oo == SOE_ADD { rr = pu[0] + pv[0] } 146 if oo == SOE_SUB { rr = pu[0] - pv[0] } 147 if oo == SOE_MUL { rr = pu[0] * pv[0] } 148 tmp[j] = rr 149 j = j + 1 150 } 151 soe_offer(c, tmp, oo, u, v, 0) 152 oo = oo + 1 153 } 154 v = v + 1 155 } 156 if c.found >= 0 { return c.found } 157 u = u + 1 158 } 159 if c.found >= 0 { return c.found } 160 r = r + 1 161 } 162 return c.found 163} 164 165// allocate a context with all its arrays. 166func soe_new(nex: i64) -> *SoeCtx { 167 let c: *SoeCtx = sys_mmap(128) as *SoeCtx 168 c.vecs = sys_mmap(8 * SOE_MAXV * nex) as *i64 169 c.kind = sys_mmap(8 * SOE_MAXV) as *i64 170 c.op = sys_mmap(8 * SOE_MAXV) as *i64 171 c.pa = sys_mmap(8 * SOE_MAXV) as *i64 172 c.pb = sys_mmap(8 * SOE_MAXV) as *i64 173 c.lit = sys_mmap(8 * SOE_MAXV) as *i64 174 c.ht = sys_mmap(8 * SOE_HT) as *i64 175 c.target = sys_mmap(8 * nex) as *i64 176 c.nex = nex 177 return c 178}