code wiki / _hdl_build / _synth_bench_authored.nx
_synth_bench_authored.nx source
↩ module page · 484 lines · 18358 B
1// AUTHORED BY THE NISHI BUILDER (nx_module_author synth-bench template) -- S6 suite compose-v1.
2import "nx_syscalls.nx"
3func _sb_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
4func _sb_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 }
5func _sb_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 }
6func _sb_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 }
7const SB_KMAX: i64 = 64
8const SB_NCOMP: i64 = 12
9const SB_MAXTERM: i64 = 30000
10const SB_MAXLVL: i64 = 4
11const SB_HCAP: i64 = 131072
12const SB_BUDGET: i64 = 8000000
13const SB_MAXROUND: i64 = 16
14const SB_SLICE: i64 = 150000
15func sb_arity(c: i64) -> i64 { if c == 12 { return 1 } return 2 }
16func sb_comm(c: i64) -> i64 { if c == 2 { return 1 } if c == 4 { return 1 } if c == 5 { return 1 } if c == 6 { return 1 } if c == 8 { return 1 } return 0 }
17func sb_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 { return a >> (b & 63) }
21 if c == 4 { if a < b { return a } return b }
22 if c == 5 { if a > b { return a } return b }
23 if c == 6 { return a + b }
24 if c == 7 { return a - b }
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 sb_oracle(oid: i64, a: i64, b: i64) -> i64 {
33 if oid == 1 { return (a + b) / 2 }
34 if oid == 2 { var d: i64 = a - b; if d < 0 { d = 0 - d } return d }
35 if oid == 3 { var h: i64 = a - b; if h < 0 { h = 0 } return h }
36 if oid == 4 { return a - (a % 8) }
37 if oid == 5 { return (a * b) >> 7 }
38 if oid == 6 { return (a + b) & 1 }
39 if oid == 7 { if a == b { return 1 } return 0 }
40 var mx: i64 = a
41 if b > mx { mx = b }
42 return mx >> 1
43}
44func sb_claude(oid: i64, a: i64, b: i64) -> i64 {
45 if oid == 1 { return sb_apply(10, sb_apply(6, a, b), 2) }
46 if oid == 2 { return sb_apply(12, sb_apply(7, a, b), 0) }
47 if oid == 3 { return sb_apply(5, sb_apply(7, a, b), 0) }
48 if oid == 4 { return sb_apply(7, a, sb_apply(11, a, 8)) }
49 if oid == 5 { return sb_apply(3, sb_apply(8, a, b), 7) }
50 if oid == 6 { return sb_apply(2, sb_apply(6, a, b), 1) }
51 if oid == 7 { return sb_apply(2, sb_apply(1, a, b), sb_apply(1, b, a)) }
52 return sb_apply(3, sb_apply(5, a, b), 1)
53}
54func sb_vech(vecs: *i64, ix: i64, kk: i64) -> i64 {
55 var h: i64 = 1469
56 var q: i64 = 0
57 while q < kk { h = h * 131 + vecs[ix*SB_KMAX+q]; q = q + 1 }
58 if h < 0 { h = 0 - h }
59 return h
60}
61func sb_vec_eq(vecs: *i64, x: i64, y: i64, kk: i64) -> i64 {
62 var q: i64 = 0
63 while q < kk { if vecs[x*SB_KMAX+q] != vecs[y*SB_KMAX+q] { return 0 } q = q + 1 }
64 return 1
65}
66func sb_insert(vecs: *i64, hash: *i64, nterm: i64, kk: i64) -> i64 {
67 let h0: i64 = sb_vech(vecs, nterm, kk) & (SB_HCAP - 1)
68 var s: i64 = h0
69 var go: i64 = 1
70 while go == 1 {
71 if hash[s] == 0 { hash[s] = nterm + 1; return 1 }
72 if sb_vec_eq(vecs, hash[s] - 1, nterm, kk) == 1 { return 0 }
73 s = s + 1
74 if s >= SB_HCAP { s = 0 }
75 if s == h0 { return 0 }
76 }
77 return 0
78}
79func sb_is_target(vecs: *i64, ix: i64, kx: *i64, kk: i64) -> i64 {
80 var q: i64 = 0
81 while q < kk { if vecs[ix*SB_KMAX+q] != kx[q] { return 0 } q = q + 1 }
82 return 1
83}
84func sb_search(ka: *i64, kb: *i64, kx: *i64, kk: i64, cons: *i64, ncon: i64, terms: *i64, vecs: *i64, hash: *i64, stats: *i64) -> i64 {
85 var s: i64 = 0
86 while s < SB_HCAP { hash[s] = 0; s = s + 1 }
87 var nt: i64 = 0
88 var cand: i64 = 0
89 var q: i64 = 0
90 q = 0
91 while q < kk { vecs[nt*SB_KMAX+q] = ka[q]; q = q + 1 }
92 terms[nt*5+0] = 0
93 terms[nt*5+1] = 0
94 terms[nt*5+2] = 0
95 terms[nt*5+3] = 0
96 terms[nt*5+4] = 1
97 if sb_insert(vecs, hash, nt, kk) == 1 { if sb_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; return nt } nt = nt + 1 }
98 q = 0
99 while q < kk { vecs[nt*SB_KMAX+q] = kb[q]; q = q + 1 }
100 terms[nt*5+0] = 0
101 terms[nt*5+1] = 1
102 terms[nt*5+2] = 0
103 terms[nt*5+3] = 0
104 terms[nt*5+4] = 1
105 if sb_insert(vecs, hash, nt, kk) == 1 { if sb_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; return nt } nt = nt + 1 }
106 var ci: i64 = 0
107 while ci < ncon {
108 q = 0
109 while q < kk { vecs[nt*SB_KMAX+q] = cons[ci]; q = q + 1 }
110 terms[nt*5+0] = 1
111 terms[nt*5+1] = cons[ci]
112 terms[nt*5+2] = 0
113 terms[nt*5+3] = 0
114 terms[nt*5+4] = 1
115 if sb_insert(vecs, hash, nt, kk) == 1 { if sb_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; return nt } nt = nt + 1 }
116 ci = ci + 1
117 }
118 var lvl: i64 = 2
119 while lvl <= SB_MAXLVL {
120 let n0: i64 = nt
121 let cp: *i64 = sys_mmap(256) as *i64
122 let cdone: *i64 = sys_mmap(256) as *i64
123 var c: i64 = 1
124 while c <= SB_NCOMP { cp[c] = 0; cdone[c] = 0; c = c + 1 }
125 var anyleft: i64 = 1
126 while anyleft == 1 {
127 anyleft = 0
128 c = 1
129 while c <= SB_NCOMP {
130 if cdone[c] == 0 {
131 var steps: i64 = 0
132 var p: i64 = cp[c]
133 var space: i64 = n0
134 if sb_arity(c) == 2 { space = n0 * n0 }
135 var stop2: i64 = 0
136 while stop2 == 0 {
137 if p >= space { cdone[c] = 1; stop2 = 1 }
138 else { if steps >= SB_SLICE { stop2 = 1 }
139 else {
140 steps = steps + 1
141 var x: i64 = p
142 var y: i64 = 0
143 if sb_arity(c) == 2 { x = p / n0; y = p % n0 }
144 var mx: i64 = terms[x*5+4]
145 if sb_arity(c) == 2 {
146 if terms[y*5+4] > mx { mx = terms[y*5+4] }
147 if terms[x*5+0] == 1 { if terms[y*5+0] == 1 { mx = 0 - 1 } }
148 if sb_comm(c) == 1 { if x > y { mx = 0 - 1 } }
149 }
150 if mx == lvl - 1 {
151 if cand > SB_BUDGET { stats[0] = cand; return 0 - 1 }
152 cand = cand + 1
153 var slot: i64 = nt
154 if nt >= SB_MAXTERM { slot = SB_MAXTERM }
155 q = 0
156 if sb_arity(c) == 2 { while q < kk { vecs[slot*SB_KMAX+q] = sb_apply(c, vecs[x*SB_KMAX+q], vecs[y*SB_KMAX+q]); q = q + 1 } }
157 else { while q < kk { vecs[slot*SB_KMAX+q] = sb_apply(c, vecs[x*SB_KMAX+q], 0); q = q + 1 } }
158 if sb_is_target(vecs, slot, kx, kk) == 1 {
159 terms[slot*5+0] = 2
160 terms[slot*5+1] = c
161 terms[slot*5+2] = x
162 terms[slot*5+3] = y
163 terms[slot*5+4] = lvl
164 stats[0] = cand
165 return slot
166 }
167 if nt < SB_MAXTERM {
168 if sb_insert(vecs, hash, nt, kk) == 1 {
169 terms[nt*5+0] = 2
170 terms[nt*5+1] = c
171 terms[nt*5+2] = x
172 terms[nt*5+3] = y
173 terms[nt*5+4] = lvl
174 nt = nt + 1
175 }
176 }
177 }
178 p = p + 1
179 } }
180 }
181 cp[c] = p
182 if cdone[c] == 0 { anyleft = 1 }
183 }
184 c = c + 1
185 }
186 }
187 lvl = lvl + 1
188 }
189 stats[0] = cand
190 return 0 - 1
191}
192func sb_eval(terms: *i64, ix: i64, a: i64, b: i64) -> i64 {
193 let kind: i64 = terms[ix*5+0]
194 if kind == 0 { if terms[ix*5+1] == 0 { return a } return b }
195 if kind == 1 { return terms[ix*5+1] }
196 let c: i64 = terms[ix*5+1]
197 let lv: i64 = sb_eval(terms, terms[ix*5+2], a, b)
198 var rv: i64 = 0
199 if sb_arity(c) == 2 { rv = sb_eval(terms, terms[ix*5+3], a, b) }
200 return sb_apply(c, lv, rv)
201}
202func sb_find_cex(terms: *i64, r: i64, oid: i64, ka: *i64, kb: *i64, kx: *i64, kbox: *i64, mode: i64, hterms: *i64, hroot: *i64) -> i64 {
203 var added: i64 = 0
204 var qd: i64 = 0
205 while qd < 4 {
206 var palo: i64 = 0 - 60
207 var pahi: i64 = 39
208 if qd >= 2 { palo = 40; pahi = 140 }
209 var pblo: i64 = 0 - 60
210 var pbhi: i64 = 39
211 if qd % 2 == 1 { pblo = 40; pbhi = 140 }
212 var found: i64 = 0
213 var pa: i64 = palo
214 while pa <= pahi {
215 if found == 0 {
216 var pb: i64 = pblo
217 while pb <= pbhi {
218 if found == 0 {
219 let want: i64 = sb_oracle2(mode, oid, pa, pb, hterms, hroot)
220 if sb_eval(terms, r, pa, pb) != want {
221 let kk2: i64 = kbox[0]
222 if kk2 >= SB_KMAX { return 2 }
223 ka[kk2] = pa
224 kb[kk2] = pb
225 kx[kk2] = want
226 kbox[0] = kk2 + 1
227 added = added + 1
228 found = 1
229 }
230 }
231 pb = pb + 1
232 }
233 }
234 pa = pa + 1
235 }
236 qd = qd + 1
237 }
238 if added > 0 { return 1 }
239 return 0
240}
241func ng_rand(sbox: *i64) -> i64 {
242 sbox[0] = (sbox[0] * 1103515245 + 12345) & 2147483647
243 return sbox[0]
244}
245func ng_gen(seed: i64, hterms: *i64, hb: *i64, cset: *i64, pa16: *i64, pb16: *i64) -> i64 {
246 let sbox: *i64 = sys_mmap(16) as *i64
247 sbox[0] = (seed * 48271 + 11) & 2147483647
248 let av: *i64 = sys_mmap(256) as *i64
249 var na: i64 = 0
250 var base: i64 = hb[0]
251 hterms[base*5+0] = 0
252 hterms[base*5+1] = 0
253 hterms[base*5+2] = 0
254 hterms[base*5+3] = 0
255 hterms[base*5+4] = 1
256 av[na] = base
257 na = na + 1
258 base = base + 1
259 hterms[base*5+0] = 0
260 hterms[base*5+1] = 1
261 hterms[base*5+2] = 0
262 hterms[base*5+3] = 0
263 hterms[base*5+4] = 1
264 av[na] = base
265 na = na + 1
266 base = base + 1
267 var ci: i64 = 0
268 while ci < 3 {
269 hterms[base*5+0] = 1
270 hterms[base*5+1] = cset[ng_rand(sbox) % 7]
271 hterms[base*5+2] = 0
272 hterms[base*5+3] = 0
273 hterms[base*5+4] = 1
274 av[na] = base
275 na = na + 1
276 base = base + 1
277 ci = ci + 1
278 }
279 var root: i64 = av[0]
280 var st: i64 = 0
281 while st < 4 {
282 let c: i64 = 1 + (ng_rand(sbox) % 12)
283 let xi: i64 = av[ng_rand(sbox) % na]
284 let yi: i64 = av[ng_rand(sbox) % na]
285 hterms[base*5+0] = 2
286 hterms[base*5+1] = c
287 hterms[base*5+2] = xi
288 hterms[base*5+3] = yi
289 hterms[base*5+4] = 2
290 av[na] = base
291 na = na + 1
292 root = base
293 base = base + 1
294 st = st + 1
295 }
296 hb[0] = base
297 var allc: i64 = 1
298 var eqa: i64 = 1
299 var eqb: i64 = 1
300 let v0: i64 = sb_eval(hterms, root, pa16[0], pb16[0])
301 var t2: i64 = 0
302 while t2 < 16 {
303 let vv: i64 = sb_eval(hterms, root, pa16[t2], pb16[t2])
304 if vv != v0 { allc = 0 }
305 if vv != pa16[t2] { eqa = 0 }
306 if vv != pb16[t2] { eqb = 0 }
307 t2 = t2 + 1
308 }
309 if allc == 1 { return 0 - 1 }
310 if eqa == 1 { return 0 - 1 }
311 if eqb == 1 { return 0 - 1 }
312 return root
313}
314func sb_oracle2(mode: i64, oid: i64, a: i64, b: i64, hterms: *i64, hroot: *i64) -> i64 {
315 if mode == 0 { return sb_oracle(oid, a, b) }
316 return sb_eval(hterms, hroot[oid], a, b)
317}
318func sb_claude_check(oid: i64) -> i64 {
319 var pa: i64 = 0 - 60
320 while pa <= 140 {
321 var pb: i64 = 0 - 60
322 while pb <= 140 {
323 if sb_claude(oid, pa, pb) != sb_oracle(oid, pa, pb) { return 0 }
324 pb = pb + 1
325 }
326 pa = pa + 1
327 }
328 return 1
329}
330func sb_solve(oid: i64, cons: *i64, ncon: i64, terms: *i64, vecs: *i64, hash: *i64, mode: i64, hterms: *i64, hroot: *i64) -> i64 {
331 let ka: *i64 = sys_mmap(512) as *i64
332 let kb: *i64 = sys_mmap(512) as *i64
333 let kx: *i64 = sys_mmap(512) as *i64
334 let kbox: *i64 = sys_mmap(16) as *i64
335 let stats: *i64 = sys_mmap(64) as *i64
336 ka[0] = 0
337 kb[0] = 0
338 ka[1] = 1
339 kb[1] = 1
340 ka[2] = 16
341 kb[2] = 8
342 ka[3] = 100
343 kb[3] = 50
344 var s: i64 = 0
345 while s < 4 { kx[s] = sb_oracle2(mode, oid, ka[s], kb[s], hterms, hroot); s = s + 1 }
346 kbox[0] = 4
347 var round: i64 = 0
348 var won: i64 = 0
349 var done: i64 = 0
350 while done == 0 {
351 round = round + 1
352 if round > SB_MAXROUND { done = 1 }
353 else {
354 let r: i64 = sb_search(ka, kb, kx, kbox[0], cons, ncon, terms, vecs, hash, stats)
355 if r < 0 { done = 1 }
356 else {
357 let cx: i64 = sb_find_cex(terms, r, oid, ka, kb, kx, kbox, mode, hterms, hroot)
358 if cx == 0 { won = 1; done = 1 }
359 else { if cx == 2 { done = 1 } }
360 }
361 }
362 }
363 _sb_puts(" spec=" as *u8); _sb_num(oid)
364 _sb_puts(" team=" as *u8); _sb_num(won)
365 _sb_puts(" rounds=" as *u8); _sb_num(round)
366 _sb_puts(" cand=" as *u8); _sb_num(stats[0]); _sb_puts("\n" as *u8)
367 return won
368}
369func main() -> i64 {
370 _sb_puts("=== S6 SYNTH-BENCH suite=compose-v1: 8 held-out specs, team CEGIS lane vs Claude lane ===\n" as *u8)
371 let terms: *i64 = sys_mmap(2097152) as *i64
372 let vecs: *i64 = sys_mmap(16777216) as *i64
373 let hash: *i64 = sys_mmap(1048576) as *i64
374 let cons: *i64 = sys_mmap(64) as *i64
375 cons[0] = 0
376 cons[1] = 1
377 cons[2] = 2
378 cons[3] = 7
379 cons[4] = 8
380 cons[5] = 10
381 cons[6] = 99
382 let hterms: *i64 = sys_mmap(65536) as *i64
383 let hroot: *i64 = sys_mmap(128) as *i64
384 var team: i64 = 0
385 var claude: i64 = 0
386 var oid: i64 = 1
387 while oid <= 8 {
388 team = team + sb_solve(oid, cons, 7, terms, vecs, hash, 0, hterms, hroot)
389 claude = claude + sb_claude_check(oid)
390 oid = oid + 1
391 }
392 let team_pm: i64 = team * 125
393 let claude_pm: i64 = claude * 125
394 _sb_puts("BENCH suite=compose-v1 team_permil=" as *u8); _sb_num(team_pm)
395 _sb_puts(" claude_permil=" as *u8); _sb_num(claude_pm)
396 var sc: i64 = 0
397 if team_pm >= claude_pm { sc = 1 }
398 if sc == 1 { _sb_puts(" verdict=S-CLASS-COMPOSE-ACHIEVED\n" as *u8) } else { _sb_puts(" verdict=NOT-YET\n" as *u8) }
399 let bfd: i64 = sys_openat_append("knowledge/status/synth_bench.log" as *u8, 0x1a4)
400 if bfd >= 0 {
401 _sb_fputs(bfd, "BENCH epoch=" as *u8); _sb_fnum(bfd, sys_now_realtime_sec())
402 _sb_fputs(bfd, " suite=compose-v1 team_permil=" as *u8); _sb_fnum(bfd, team_pm)
403 _sb_fputs(bfd, " claude_permil=" as *u8); _sb_fnum(bfd, claude_pm)
404 if sc == 1 { _sb_fputs(bfd, " verdict=S-CLASS-COMPOSE-ACHIEVED\n" as *u8) } else { _sb_fputs(bfd, " verdict=NOT-YET\n" as *u8) }
405 sys_close(bfd)
406 }
407 let pa16: *i64 = sys_mmap(256) as *i64
408 let pb16: *i64 = sys_mmap(256) as *i64
409 pa16[0]=0
410 pb16[0]=0
411 pa16[1]=1
412 pb16[1]=2
413 pa16[2]=5
414 pb16[2]=3
415 pa16[3]=10
416 pb16[3]=7
417 pa16[4]=0-4
418 pb16[4]=9
419 pa16[5]=13
420 pb16[5]=0-6
421 pa16[6]=99
422 pb16[6]=2
423 pa16[7]=0-60
424 pb16[7]=140
425 pa16[8]=7
426 pb16[8]=7
427 pa16[9]=2
428 pb16[9]=100
429 pa16[10]=50
430 pb16[10]=50
431 pa16[11]=0-1
432 pb16[11]=0-1
433 pa16[12]=8
434 pb16[12]=1
435 pa16[13]=3
436 pb16[13]=15
437 pa16[14]=140
438 pb16[14]=0-60
439 pa16[15]=11
440 pb16[15]=4
441 let hb: *i64 = sys_mmap(16) as *i64
442 hb[0] = 0
443 var made: i64 = 0
444 var seed: i64 = 1
445 while made < 12 {
446 let rr: i64 = ng_gen(seed, hterms, hb, cons, pa16, pb16)
447 if rr >= 0 { hroot[made] = rr; made = made + 1 }
448 seed = seed + 1
449 }
450 let sfd: i64 = sys_openat_wr("knowledge/status/novel_suite_samples.txt" as *u8, 0x1a4)
451 var sp: i64 = 0
452 while sp < 12 {
453 var pi: i64 = 0
454 while pi < 16 {
455 _sb_fputs(sfd, "spec=" as *u8); _sb_fnum(sfd, sp)
456 _sb_fputs(sfd, " a=" as *u8); _sb_fnum(sfd, pa16[pi])
457 _sb_fputs(sfd, " b=" as *u8); _sb_fnum(sfd, pb16[pi])
458 _sb_fputs(sfd, " out=" as *u8); _sb_fnum(sfd, sb_eval(hterms, hroot[sp], pa16[pi], pb16[pi]))
459 _sb_fputs(sfd, "\n" as *u8)
460 pi = pi + 1
461 }
462 sp = sp + 1
463 }
464 sys_close(sfd)
465 _sb_puts(" novel-v1: 12 hidden specs generated; samples -> knowledge/status/novel_suite_samples.txt\n" as *u8)
466 var nteam: i64 = 0
467 sp = 0
468 while sp < 12 {
469 nteam = nteam + sb_solve(sp, cons, 7, terms, vecs, hash, 1, hterms, hroot)
470 sp = sp + 1
471 }
472 let nt_pm: i64 = (nteam * 1000) / 12
473 _sb_puts("BENCH suite=novel-v1 team_permil=" as *u8); _sb_num(nt_pm); _sb_puts(" claude_permil=PENDING-BLIND-LANE\n" as *u8)
474 let nfd: i64 = sys_openat_append("knowledge/status/synth_bench.log" as *u8, 0x1a4)
475 if nfd >= 0 {
476 _sb_fputs(nfd, "BENCH epoch=" as *u8); _sb_fnum(nfd, sys_now_realtime_sec())
477 _sb_fputs(nfd, " suite=novel-v1 team_permil=" as *u8); _sb_fnum(nfd, nt_pm)
478 _sb_fputs(nfd, " claude_permil=PENDING-BLIND-LANE (protocol: Claude answers from the 16-pair samples ONLY; hidden terms never printed)\n" as *u8)
479 sys_close(nfd)
480 }
481 if sc == 1 { if team == 8 { sys_exit(0); return 0 } }
482 sys_exit(1)
483 return 1
484}