code wiki / _hdl_build / _loop_synth_authored.nx
_loop_synth_authored.nx source
↩ module page · 403 lines · 17365 B
1// AUTHORED BY THE NISHI BUILDER (nx_module_author loop-synth template) -- S4 fold schema.
2// Schema-with-holes synthesis; tutoring: specs/2026-06-09-tutoring-code-synthesis-rung2-schemas.md
3import "nx_syscalls.nx"
4func _ls_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
5func _ls_num(v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(1,"-" as *u8,1)}; let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48;k=1}; while m>0{t[k]=48+(m%10);m=m/10;k=k+1}; var i: i64=0; while i<k{bb[i]=t[k-1-i];i=i+1}; sys_write(1,bb,k); return 0 }
6func _ls_fputs(fd2: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd2,s,n); return 0 }
7func _ls_fnum(fd2: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(fd2,"-" as *u8,1)}; let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48;k=1}; while m>0{t[k]=48+(m%10);m=m/10;k=k+1}; var i: i64=0; while i<k{bb[i]=t[k-1-i];i=i+1}; sys_write(fd2,bb,k); return 0 }
8func _ls_fsig(fd2: i64, v: i64) -> i64 { if v < 0 { _ls_fputs(fd2, "0 - " as *u8); _ls_fnum(fd2, 0 - v) } else { _ls_fnum(fd2, v) } return 0 }
9const LS_NPAIR: i64 = 16
10const LS_NCOMP: i64 = 12
11const LS_MAXTERM: i64 = 60000
12const LS_MAXLVL: i64 = 3
13const LS_HCAP: i64 = 131072
14const LS_BUDGET: i64 = 4000000
15func ls_arity(c: i64) -> i64 { if c == 12 { return 1 } return 2 }
16func ls_comm(c: i64) -> i64 { if c == 2 { return 1 } if c == 3 { return 1 } if c == 4 { return 1 } if c == 5 { return 1 } if c == 6 { return 1 } return 0 }
17func ls_apply(c: i64, a: i64, b: i64) -> i64 {
18 if c == 1 { if a <= b { return 1 } return 0 }
19 if c == 2 { return a + b }
20 if c == 3 { if a > b { return a } return b }
21 if c == 4 { if a < b { return a } return b }
22 if c == 5 { return a * b }
23 if c == 6 { return a & b }
24 if c == 7 { return a >> (b & 63) }
25 if c == 8 { return a - b }
26 if c == 9 { return a << (b & 63) }
27 if c == 10 { if b == 0 { return 0 } return a / b }
28 if c == 11 { if b == 0 { return 0 } return a % b }
29 if c == 12 { if a < 0 { return 0 - a } return a }
30 return 0
31}
32func ls_vech(vecs: *i64, ix: i64) -> i64 {
33 var h: i64 = 1469
34 var q: i64 = 0
35 while q < LS_NPAIR { h = h * 131 + vecs[ix*LS_NPAIR+q]; q = q + 1 }
36 if h < 0 { h = 0 - h }
37 return h
38}
39func ls_vec_eq(vecs: *i64, x: i64, y: i64) -> i64 {
40 var q: i64 = 0
41 while q < LS_NPAIR { if vecs[x*LS_NPAIR+q] != vecs[y*LS_NPAIR+q] { return 0 } q = q + 1 }
42 return 1
43}
44func ls_insert(vecs: *i64, hash: *i64, nterm: i64) -> i64 {
45 let h0: i64 = ls_vech(vecs, nterm) & (LS_HCAP - 1)
46 var s: i64 = h0
47 var go: i64 = 1
48 while go == 1 {
49 if hash[s] == 0 { hash[s] = nterm + 1; return 1 }
50 if ls_vec_eq(vecs, hash[s] - 1, nterm) == 1 { return 0 }
51 s = s + 1
52 if s >= LS_HCAP { s = 0 }
53 if s == h0 { return 0 }
54 }
55 return 0
56}
57func ls_enum_steps(pa: *i64, pb: *i64, cons: *i64, ncon: i64, terms: *i64, vecs: *i64, hash: *i64, stats: *i64) -> i64 {
58 var s: i64 = 0
59 while s < LS_HCAP { hash[s] = 0; s = s + 1 }
60 var nt: i64 = 0
61 var cand: i64 = 0
62 var q: i64 = 0
63 q = 0
64 while q < LS_NPAIR { vecs[nt*LS_NPAIR+q] = pa[q]; q = q + 1 }
65 terms[nt*5+0] = 0
66 terms[nt*5+1] = 0
67 terms[nt*5+2] = 0
68 terms[nt*5+3] = 0
69 terms[nt*5+4] = 1
70 if ls_insert(vecs, hash, nt) == 1 { nt = nt + 1 }
71 q = 0
72 while q < LS_NPAIR { vecs[nt*LS_NPAIR+q] = pb[q]; q = q + 1 }
73 terms[nt*5+0] = 0
74 terms[nt*5+1] = 1
75 terms[nt*5+2] = 0
76 terms[nt*5+3] = 0
77 terms[nt*5+4] = 1
78 if ls_insert(vecs, hash, nt) == 1 { nt = nt + 1 }
79 var ci: i64 = 0
80 while ci < ncon {
81 q = 0
82 while q < LS_NPAIR { vecs[nt*LS_NPAIR+q] = cons[ci]; q = q + 1 }
83 terms[nt*5+0] = 1
84 terms[nt*5+1] = cons[ci]
85 terms[nt*5+2] = 0
86 terms[nt*5+3] = 0
87 terms[nt*5+4] = 1
88 if ls_insert(vecs, hash, nt) == 1 { nt = nt + 1 }
89 ci = ci + 1
90 }
91 var lvl: i64 = 2
92 var full: i64 = 0
93 while lvl <= LS_MAXLVL {
94 let n0: i64 = nt
95 var c: i64 = 1
96 while c <= LS_NCOMP {
97 var x: i64 = 0
98 while x < n0 {
99 if ls_arity(c) == 1 {
100 if terms[x*5+4] == lvl - 1 { if nt < LS_MAXTERM { if cand <= LS_BUDGET {
101 cand = cand + 1
102 q = 0
103 while q < LS_NPAIR { vecs[nt*LS_NPAIR+q] = ls_apply(c, vecs[x*LS_NPAIR+q], 0); q = q + 1 }
104 if ls_insert(vecs, hash, nt) == 1 {
105 terms[nt*5+0] = 2
106 terms[nt*5+1] = c
107 terms[nt*5+2] = x
108 terms[nt*5+3] = 0
109 terms[nt*5+4] = lvl
110 nt = nt + 1
111 }
112 } else { full = 1 } } else { full = 1 } }
113 }
114 else {
115 var y: i64 = 0
116 while y < n0 {
117 var mx: i64 = terms[x*5+4]
118 if terms[y*5+4] > mx { mx = terms[y*5+4] }
119 if terms[x*5+0] == 1 { if terms[y*5+0] == 1 { mx = 0 - 1 } }
120 if ls_comm(c) == 1 { if x > y { mx = 0 - 1 } }
121 if mx == lvl - 1 { if nt < LS_MAXTERM { if cand <= LS_BUDGET {
122 cand = cand + 1
123 q = 0
124 while q < LS_NPAIR { vecs[nt*LS_NPAIR+q] = ls_apply(c, vecs[x*LS_NPAIR+q], vecs[y*LS_NPAIR+q]); q = q + 1 }
125 if ls_insert(vecs, hash, nt) == 1 {
126 terms[nt*5+0] = 2
127 terms[nt*5+1] = c
128 terms[nt*5+2] = x
129 terms[nt*5+3] = y
130 terms[nt*5+4] = lvl
131 nt = nt + 1
132 }
133 } else { full = 1 } } else { full = 1 } }
134 y = y + 1
135 }
136 }
137 x = x + 1
138 }
139 c = c + 1
140 }
141 lvl = lvl + 1
142 }
143 stats[0] = cand
144 stats[1] = full
145 return nt
146}
147func ls_eval(terms: *i64, ix: i64, a: i64, b: i64) -> i64 {
148 let kind: i64 = terms[ix*5+0]
149 if kind == 0 { if terms[ix*5+1] == 0 { return a } return b }
150 if kind == 1 { return terms[ix*5+1] }
151 let c: i64 = terms[ix*5+1]
152 let lv: i64 = ls_eval(terms, terms[ix*5+2], a, b)
153 var rv: i64 = 0
154 if ls_arity(c) == 2 { rv = ls_eval(terms, terms[ix*5+3], a, b) }
155 return ls_apply(c, lv, rv)
156}
157func ls_byte(seed: i64, i: i64) -> i64 {
158 if (seed + i) % 3 == 0 { return 0 }
159 return (seed * 131 + i * 37) & 255
160}
161func ls_run(init: i64, terms: *i64, ix: i64, seed: i64, len: i64) -> i64 {
162 var acc: i64 = init
163 var i: i64 = 0
164 while i < len { acc = ls_eval(terms, ix, acc, ls_byte(seed, i)); i = i + 1 }
165 return acc
166}
167func ls_oracle(oid: i64, seed: i64, len: i64) -> i64 {
168 var acc: i64 = 0
169 var i: i64 = 0
170 while i < len {
171 let b: i64 = ls_byte(seed, i)
172 if oid == 1 { acc = acc + b }
173 if oid == 2 { if b > acc { acc = b } }
174 if oid == 3 { if b >= 1 { acc = acc + 1 } }
175 if oid == 4 { acc = acc * 31 + b }
176 i = i + 1
177 }
178 return acc
179}
180func ls_check_spec(init: i64, terms: *i64, ix: i64, oid: i64, lens: *i64) -> i64 {
181 var si: i64 = 0
182 while si < 4 {
183 var seed: i64 = si + 1
184 if si == 3 { seed = 5 }
185 var li: i64 = 0
186 while li < 8 {
187 if ls_run(init, terms, ix, seed, lens[li]) != ls_oracle(oid, seed, lens[li]) { return 0 }
188 li = li + 1
189 }
190 si = si + 1
191 }
192 return 1
193}
194func ls_verify(init: i64, terms: *i64, ix: i64, oid: i64) -> i64 {
195 var seed: i64 = 1
196 while seed <= 8 {
197 var len: i64 = 0
198 while len < 50 {
199 if ls_run(init, terms, ix, seed, len) != ls_oracle(oid, seed, len) { return 0 }
200 len = len + 1
201 }
202 seed = seed + 1
203 }
204 return 1
205}
206func ls_comp_name(c: i64) -> *u8 {
207 if c == 1 { return "_c_le" as *u8 }
208 if c == 2 { return "_c_add" as *u8 }
209 if c == 3 { return "_c_max" as *u8 }
210 if c == 4 { return "_c_min" as *u8 }
211 if c == 5 { return "_c_mul" as *u8 }
212 if c == 6 { return "_c_and" as *u8 }
213 if c == 7 { return "_c_shr" as *u8 }
214 if c == 8 { return "_c_sub" as *u8 }
215 if c == 9 { return "_c_shl" as *u8 }
216 if c == 10 { return "_c_div" as *u8 }
217 if c == 11 { return "_c_mod" as *u8 }
218 return "_c_abs" as *u8
219}
220func ls_emit_term(ofd: i64, terms: *i64, ix: i64) -> i64 {
221 let kind: i64 = terms[ix*5+0]
222 if kind == 0 { if terms[ix*5+1] == 0 { _ls_fputs(ofd, "a" as *u8) } else { _ls_fputs(ofd, "b" as *u8) } return 0 }
223 if kind == 1 { _ls_fsig(ofd, terms[ix*5+1]); return 0 }
224 _ls_fputs(ofd, ls_comp_name(terms[ix*5+1])); _ls_fputs(ofd, "(" as *u8)
225 ls_emit_term(ofd, terms, terms[ix*5+2])
226 if ls_arity(terms[ix*5+1]) == 2 { _ls_fputs(ofd, ", " as *u8); ls_emit_term(ofd, terms, terms[ix*5+3]) }
227 _ls_fputs(ofd, ")" as *u8)
228 return 0
229}
230func ls_emit_module(path: *u8, init: i64, terms: *i64, ix: i64) -> i64 {
231 let ofd: i64 = sys_openat_wr(path, 0x1a4)
232 if ofd < 0 { return 0 - 1 }
233 _ls_fputs(ofd, "// SYNTHESIZED BY THE NISHI TEAM (fold schema, _loop_synth_authored): the loop skeleton\n" as *u8)
234 _ls_fputs(ofd, "// is the sketch; INIT+STEP were derived from oracle queries and held-out-verified.\n" as *u8)
235 _ls_fputs(ofd, "import \"nx_syscalls.nx\"\n" as *u8)
236 _ls_fputs(ofd, "func _c_le(a: i64, b: i64) -> i64 { if a <= b { return 1 } return 0 }\n" as *u8)
237 _ls_fputs(ofd, "func _c_add(a: i64, b: i64) -> i64 { return a + b }\n" as *u8)
238 _ls_fputs(ofd, "func _c_max(a: i64, b: i64) -> i64 { if a > b { return a } return b }\n" as *u8)
239 _ls_fputs(ofd, "func _c_min(a: i64, b: i64) -> i64 { if a < b { return a } return b }\n" as *u8)
240 _ls_fputs(ofd, "func _c_mul(a: i64, b: i64) -> i64 { return a * b }\n" as *u8)
241 _ls_fputs(ofd, "func _c_and(a: i64, b: i64) -> i64 { return a & b }\n" as *u8)
242 _ls_fputs(ofd, "func _c_shr(a: i64, b: i64) -> i64 { return a >> (b & 63) }\n" as *u8)
243 _ls_fputs(ofd, "func _c_sub(a: i64, b: i64) -> i64 { return a - b }\n" as *u8)
244 _ls_fputs(ofd, "func _c_shl(a: i64, b: i64) -> i64 { return a << (b & 63) }\n" as *u8)
245 _ls_fputs(ofd, "func _c_div(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a / b }\n" as *u8)
246 _ls_fputs(ofd, "func _c_mod(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a % b }\n" as *u8)
247 _ls_fputs(ofd, "func _c_abs(a: i64) -> i64 { if a < 0 { return 0 - a } return a }\n" as *u8)
248 _ls_fputs(ofd, "func step(a: i64, b: i64) -> i64 { return " as *u8)
249 ls_emit_term(ofd, terms, ix)
250 _ls_fputs(ofd, " }\n" as *u8)
251 _ls_fputs(ofd, "func synth(buf: *u8, n: i64) -> i64 {\n" as *u8)
252 _ls_fputs(ofd, " var acc: i64 = " as *u8); _ls_fsig(ofd, init); _ls_fputs(ofd, "\n" as *u8)
253 _ls_fputs(ofd, " var i: i64 = 0\n" as *u8)
254 _ls_fputs(ofd, " while i < n { acc = step(acc, buf[i] as i64); i = i + 1 }\n" as *u8)
255 _ls_fputs(ofd, " return acc\n}\n" as *u8)
256 _ls_fputs(ofd, "func _g_byte(seed: i64, i: i64) -> i64 {\n" as *u8)
257 _ls_fputs(ofd, " if (seed + i) % 3 == 0 { return 0 }\n" as *u8)
258 _ls_fputs(ofd, " return (seed * 131 + i * 37) & 255\n}\n" as *u8)
259 _ls_fputs(ofd, "func main() -> i64 {\n" as *u8)
260 _ls_fputs(ofd, " let s: *i64 = sys_mmap(64) as *i64\n" as *u8)
261 _ls_fputs(ofd, " let l: *i64 = sys_mmap(64) as *i64\n" as *u8)
262 _ls_fputs(ofd, " let e: *i64 = sys_mmap(64) as *i64\n" as *u8)
263 var t: i64 = 0
264 while t < 6 {
265 var sd: i64 = 1
266 if t % 2 == 1 { sd = 5 }
267 var ln: i64 = 0
268 if t >= 2 { ln = 7 }
269 if t >= 4 { ln = 11 }
270 _ls_fputs(ofd, " s[" as *u8); _ls_fnum(ofd, t); _ls_fputs(ofd, "] = " as *u8); _ls_fnum(ofd, sd); _ls_fputs(ofd, "\n" as *u8)
271 _ls_fputs(ofd, " l[" as *u8); _ls_fnum(ofd, t); _ls_fputs(ofd, "] = " as *u8); _ls_fnum(ofd, ln); _ls_fputs(ofd, "\n" as *u8)
272 _ls_fputs(ofd, " e[" as *u8); _ls_fnum(ofd, t); _ls_fputs(ofd, "] = " as *u8); _ls_fsig(ofd, ls_run(init, terms, ix, sd, ln)); _ls_fputs(ofd, "\n" as *u8)
273 t = t + 1
274 }
275 _ls_fputs(ofd, " let buf: *u8 = sys_mmap(64)\n" as *u8)
276 _ls_fputs(ofd, " var t: i64 = 0\n" as *u8)
277 _ls_fputs(ofd, " while t < 6 {\n" as *u8)
278 _ls_fputs(ofd, " var j: i64 = 0\n" as *u8)
279 _ls_fputs(ofd, " while j < l[t] { buf[j] = _g_byte(s[t], j) as u8; j = j + 1 }\n" as *u8)
280 _ls_fputs(ofd, " if synth(buf, l[t]) != e[t] { sys_exit(1) }\n" as *u8)
281 _ls_fputs(ofd, " t = t + 1\n" as *u8)
282 _ls_fputs(ofd, " }\n" as *u8)
283 _ls_fputs(ofd, " sys_exit(0)\n return 0\n}\n" as *u8)
284 sys_close(ofd)
285 return 0
286}
287func ls_corpus_line(label: *u8, verdict: *u8, init: i64, terms: *i64, ix: i64, scanned: i64) -> i64 {
288 let cfd: i64 = sys_openat_append("knowledge/library/synth_corpus.log" as *u8, 0x1a4)
289 if cfd < 0 { return 0 - 1 }
290 _ls_fputs(cfd, "SYNTH engine=loop-synth schema=fold spec=" as *u8); _ls_fputs(cfd, label)
291 _ls_fputs(cfd, " verdict=" as *u8); _ls_fputs(cfd, verdict)
292 _ls_fputs(cfd, " scanned=" as *u8); _ls_fnum(cfd, scanned)
293 _ls_fputs(cfd, " init=" as *u8); _ls_fsig(cfd, init)
294 _ls_fputs(cfd, " step=" as *u8)
295 if ix >= 0 { ls_emit_term(cfd, terms, ix) } else { _ls_fputs(cfd, "none" as *u8) }
296 _ls_fputs(cfd, "\n" as *u8)
297 sys_close(cfd)
298 return 0
299}
300func ls_solve(label: *u8, path: *u8, oid: i64, cons: *i64, ncon: i64, terms: *i64, nk: i64, lens: *i64) -> i64 {
301 var s: i64 = 0
302 var won: i64 = 0
303 while s < nk {
304 var ci: i64 = 0
305 while ci < ncon {
306 if won == 0 {
307 if ls_check_spec(cons[ci], terms, s, oid, lens) == 1 {
308 if ls_verify(cons[ci], terms, s, oid) == 1 {
309 _ls_puts("LSYNTH spec=" as *u8); _ls_puts(label)
310 _ls_puts(" SOLVED init=" as *u8); _ls_num(cons[ci])
311 _ls_puts(" step=" as *u8); ls_emit_term(1, terms, s)
312 _ls_puts(" -> " as *u8); _ls_puts(path); _ls_puts("\n" as *u8)
313 ls_emit_module(path, cons[ci], terms, s)
314 ls_corpus_line(label, "CONVERGED" as *u8, cons[ci], terms, s, s + 1)
315 won = 1
316 }
317 else {
318 _ls_puts("LSYNTH spec=" as *u8); _ls_puts(label); _ls_puts(" VERIFY-FAIL (impostor caught at held-out sweep, continuing)\n" as *u8)
319 ls_corpus_line(label, "VERIFY-FAIL" as *u8, cons[ci], terms, s, s + 1)
320 }
321 }
322 }
323 ci = ci + 1
324 }
325 if won == 1 { s = nk } else { s = s + 1 }
326 }
327 if won == 0 {
328 _ls_puts("LSYNTH spec=" as *u8); _ls_puts(label); _ls_puts(" SEARCH-EXHAUSTED (honest stop)\n" as *u8)
329 ls_corpus_line(label, "EXHAUSTED" as *u8, 0, terms, 0 - 1, nk)
330 }
331 return won
332}
333func main() -> i64 {
334 _ls_puts("=== BUILDER-AUTHORED LOOP-SYNTH: fold schema, 4 held-out derivations ===\n" as *u8)
335 let terms: *i64 = sys_mmap(4194304) as *i64
336 let vecs: *i64 = sys_mmap(8388608) as *i64
337 let hash: *i64 = sys_mmap(1048576) as *i64
338 let stats: *i64 = sys_mmap(64) as *i64
339 let cons: *i64 = sys_mmap(64) as *i64
340 cons[0] = 0
341 cons[1] = 1
342 cons[2] = 3
343 cons[3] = 7
344 cons[4] = 10
345 cons[5] = 31
346 cons[6] = 99
347 let pa: *i64 = sys_mmap(256) as *i64
348 let pb: *i64 = sys_mmap(256) as *i64
349 pa[0]=0
350 pb[0]=0
351 pa[1]=0
352 pb[1]=1
353 pa[2]=0
354 pb[2]=73
355 pa[3]=0
356 pb[3]=255
357 pa[4]=1
358 pb[4]=0
359 pa[5]=1
360 pb[5]=255
361 pa[6]=5
362 pb[6]=1
363 pa[7]=5
364 pb[7]=73
365 pa[8]=31
366 pb[8]=0
367 pa[9]=31
368 pb[9]=31
369 pa[10]=100
370 pb[10]=73
371 pa[11]=100
372 pb[11]=255
373 pa[12]=255
374 pb[12]=1
375 pa[13]=255
376 pb[13]=255
377 pa[14]=1000
378 pb[14]=37
379 pa[15]=4096
380 pb[15]=250
381 let lens: *i64 = sys_mmap(64) as *i64
382 lens[0]=0
383 lens[1]=1
384 lens[2]=2
385 lens[3]=3
386 lens[4]=5
387 lens[5]=7
388 lens[6]=9
389 lens[7]=11
390 let nk: i64 = ls_enum_steps(pa, pb, cons, 7, terms, vecs, hash, stats)
391 _ls_puts(" step space: kept=" as *u8); _ls_num(nk); _ls_puts(" cand=" as *u8); _ls_num(stats[0])
392 if stats[1] == 1 { _ls_puts(" (CAP-HIT: partial coverage, honest)" as *u8) }
393 _ls_puts("\n" as *u8)
394 var won: i64 = 0
395 won = won + ls_solve("sum-bytes" as *u8, "runtime/_hdl_build/_loopsynth_sum.nx" as *u8, 1, cons, 7, terms, nk, lens)
396 won = won + ls_solve("max-byte" as *u8, "runtime/_hdl_build/_loopsynth_maxbyte.nx" as *u8, 2, cons, 7, terms, nk, lens)
397 won = won + ls_solve("count-nonzero" as *u8, "runtime/_hdl_build/_loopsynth_countnz.nx" as *u8, 3, cons, 7, terms, nk, lens)
398 won = won + ls_solve("hash31" as *u8, "runtime/_hdl_build/_loopsynth_hash31.nx" as *u8, 4, cons, 7, terms, nk, lens)
399 _ls_puts("LOOP-SYNTH GATE: " as *u8); _ls_num(won); _ls_puts("/4 fold functions derived + held-out verified\n" as *u8)
400 if won == 4 { sys_exit(0); return 0 }
401 sys_exit(1)
402 return 1
403}