_cegis_authored.nx source

1// AUTHORED BY THE NISHI BUILDER (nx_module_author cegis template) -- S3.5 mechanized CEGIS. 2// search<->oracle counterexample loop; tutoring: specs/2026-06-09-tutoring-code-synthesis-rung1.md 3// + the S3 impostor lesson in projects/2026-06-09-code-synthesis-sclass-exceed-roadmap.md. 4import "nx_syscalls.nx" 5func _cg_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 6func _cg_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 } 7func _cg_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 } 8func _cg_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 } 9func _cg_fsig(fd2: i64, v: i64) -> i64 { if v < 0 { _cg_fputs(fd2, "0 - " as *u8); _cg_fnum(fd2, 0 - v) } else { _cg_fnum(fd2, v) } return 0 } 10const CG_KMAX: i64 = 32 11const CG_NCOMP: i64 = 12 12const CG_MAXTERM: i64 = 30000 13const CG_MAXLVL: i64 = 4 14const CG_HCAP: i64 = 131072 15const CG_BUDGET: i64 = 8000000 16const CG_MAXROUND: i64 = 10 17func cg_arity(c: i64) -> i64 { if c == 12 { return 1 } return 2 } 18func cg_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 } 19func cg_apply(c: i64, a: i64, b: i64) -> i64 { 20 if c == 1 { if a <= b { return 1 } return 0 } 21 if c == 2 { return a & b } 22 if c == 3 { return a >> (b & 63) } 23 if c == 4 { if a < b { return a } return b } 24 if c == 5 { if a > b { return a } return b } 25 if c == 6 { return a + b } 26 if c == 7 { return a - b } 27 if c == 8 { return a * b } 28 if c == 9 { return a << (b & 63) } 29 if c == 10 { if b == 0 { return 0 } return a / b } 30 if c == 11 { if b == 0 { return 0 } return a % b } 31 if c == 12 { if a < 0 { return 0 - a } return a } 32 return 0 33} 34func cg_vech(vecs: *i64, ix: i64, kk: i64) -> i64 { 35 var h: i64 = 1469 36 var q: i64 = 0 37 while q < kk { h = h * 131 + vecs[ix*CG_KMAX+q]; q = q + 1 } 38 if h < 0 { h = 0 - h } 39 return h 40} 41func cg_vec_eq(vecs: *i64, x: i64, y: i64, kk: i64) -> i64 { 42 var q: i64 = 0 43 while q < kk { if vecs[x*CG_KMAX+q] != vecs[y*CG_KMAX+q] { return 0 } q = q + 1 } 44 return 1 45} 46func cg_insert(vecs: *i64, hash: *i64, nterm: i64, kk: i64) -> i64 { 47 let h0: i64 = cg_vech(vecs, nterm, kk) & (CG_HCAP - 1) 48 var s: i64 = h0 49 var go: i64 = 1 50 while go == 1 { 51 if hash[s] == 0 { hash[s] = nterm + 1; return 1 } 52 if cg_vec_eq(vecs, hash[s] - 1, nterm, kk) == 1 { return 0 } 53 s = s + 1 54 if s >= CG_HCAP { s = 0 } 55 if s == h0 { return 0 } 56 } 57 return 0 58} 59func cg_is_target(vecs: *i64, ix: i64, kx: *i64, kk: i64) -> i64 { 60 var q: i64 = 0 61 while q < kk { if vecs[ix*CG_KMAX+q] != kx[q] { return 0 } q = q + 1 } 62 return 1 63} 64func cg_search(ka: *i64, kb: *i64, kx: *i64, kk: i64, cons: *i64, ncon: i64, terms: *i64, vecs: *i64, hash: *i64, stats: *i64) -> i64 { 65 var s: i64 = 0 66 while s < CG_HCAP { hash[s] = 0; s = s + 1 } 67 var nt: i64 = 0 68 var cand: i64 = 0 69 var q: i64 = 0 70 q = 0 71 while q < kk { vecs[nt*CG_KMAX+q] = ka[q]; q = q + 1 } 72 terms[nt*5+0] = 0 73 terms[nt*5+1] = 0 74 terms[nt*5+2] = 0 75 terms[nt*5+3] = 0 76 terms[nt*5+4] = 1 77 if cg_insert(vecs, hash, nt, kk) == 1 { if cg_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=1; return nt } nt = nt + 1 } 78 q = 0 79 while q < kk { vecs[nt*CG_KMAX+q] = kb[q]; q = q + 1 } 80 terms[nt*5+0] = 0 81 terms[nt*5+1] = 1 82 terms[nt*5+2] = 0 83 terms[nt*5+3] = 0 84 terms[nt*5+4] = 1 85 if cg_insert(vecs, hash, nt, kk) == 1 { if cg_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=1; return nt } nt = nt + 1 } 86 var ci: i64 = 0 87 while ci < ncon { 88 q = 0 89 while q < kk { vecs[nt*CG_KMAX+q] = cons[ci]; q = q + 1 } 90 terms[nt*5+0] = 1 91 terms[nt*5+1] = cons[ci] 92 terms[nt*5+2] = 0 93 terms[nt*5+3] = 0 94 terms[nt*5+4] = 1 95 if cg_insert(vecs, hash, nt, kk) == 1 { if cg_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=1; return nt } nt = nt + 1 } 96 ci = ci + 1 97 } 98 var lvl: i64 = 2 99 while lvl <= CG_MAXLVL { 100 let n0: i64 = nt 101 var c: i64 = 1 102 while c <= CG_NCOMP { 103 var x: i64 = 0 104 while x < n0 { 105 if cg_arity(c) == 1 { 106 if terms[x*5+4] == lvl - 1 { 107 if nt >= CG_MAXTERM { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 } 108 if cand > CG_BUDGET { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 } 109 cand = cand + 1 110 q = 0 111 while q < kk { vecs[nt*CG_KMAX+q] = cg_apply(c, vecs[x*CG_KMAX+q], 0); q = q + 1 } 112 if cg_insert(vecs, hash, nt, kk) == 1 { 113 terms[nt*5+0] = 2 114 terms[nt*5+1] = c 115 terms[nt*5+2] = x 116 terms[nt*5+3] = 0 117 terms[nt*5+4] = lvl 118 if cg_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=lvl; return nt } 119 nt = nt + 1 120 } 121 } 122 } 123 else { 124 var y: i64 = 0 125 while y < n0 { 126 var mx: i64 = terms[x*5+4] 127 if terms[y*5+4] > mx { mx = terms[y*5+4] } 128 if terms[x*5+0] == 1 { if terms[y*5+0] == 1 { mx = 0 - 1 } } 129 if cg_comm(c) == 1 { if x > y { mx = 0 - 1 } } 130 if mx == lvl - 1 { 131 if nt >= CG_MAXTERM { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 } 132 if cand > CG_BUDGET { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 } 133 cand = cand + 1 134 q = 0 135 while q < kk { vecs[nt*CG_KMAX+q] = cg_apply(c, vecs[x*CG_KMAX+q], vecs[y*CG_KMAX+q]); q = q + 1 } 136 if cg_insert(vecs, hash, nt, kk) == 1 { 137 terms[nt*5+0] = 2 138 terms[nt*5+1] = c 139 terms[nt*5+2] = x 140 terms[nt*5+3] = y 141 terms[nt*5+4] = lvl 142 if cg_is_target(vecs, nt, kx, kk) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=lvl; return nt } 143 nt = nt + 1 144 } 145 } 146 y = y + 1 147 } 148 } 149 x = x + 1 150 } 151 c = c + 1 152 } 153 lvl = lvl + 1 154 } 155 stats[0]=cand 156 stats[1]=nt 157 stats[2]=CG_MAXLVL 158 stats[3]=0 159 return 0 - 1 160} 161func cg_eval(terms: *i64, ix: i64, a: i64, b: i64) -> i64 { 162 let kind: i64 = terms[ix*5+0] 163 if kind == 0 { if terms[ix*5+1] == 0 { return a } return b } 164 if kind == 1 { return terms[ix*5+1] } 165 let c: i64 = terms[ix*5+1] 166 let lv: i64 = cg_eval(terms, terms[ix*5+2], a, b) 167 var rv: i64 = 0 168 if cg_arity(c) == 2 { rv = cg_eval(terms, terms[ix*5+3], a, b) } 169 return cg_apply(c, lv, rv) 170} 171func cg_oracle(oid: i64, a: i64, b: i64) -> i64 { 172 if oid == 1 { if a >= 10 { if b <= 99 { return 1 } } return 0 } 173 if oid == 2 { return (a >> (b & 63)) & 7 } 174 var x: i64 = a 175 if x < 0 { x = 0 } 176 if x > b { x = b } 177 return x 178} 179func cg_find_cex(terms: *i64, r: i64, oid: i64, ka: *i64, kb: *i64, kx: *i64, kbox: *i64) -> i64 { 180 var pa: i64 = 0 - 60 181 while pa <= 140 { 182 var pb: i64 = 0 - 60 183 while pb <= 140 { 184 let want: i64 = cg_oracle(oid, pa, pb) 185 let got: i64 = cg_eval(terms, r, pa, pb) 186 if got != want { 187 let kk: i64 = kbox[0] 188 if kk >= CG_KMAX { return 2 } 189 ka[kk] = pa 190 kb[kk] = pb 191 kx[kk] = want 192 kbox[0] = kk + 1 193 return 1 194 } 195 pb = pb + 1 196 } 197 pa = pa + 1 198 } 199 return 0 200} 201func cg_comp_name(c: i64) -> *u8 { 202 if c == 1 { return "_c_le" as *u8 } 203 if c == 2 { return "_c_and" as *u8 } 204 if c == 3 { return "_c_shr" as *u8 } 205 if c == 4 { return "_c_min" as *u8 } 206 if c == 5 { return "_c_max" as *u8 } 207 if c == 6 { return "_c_add" as *u8 } 208 if c == 7 { return "_c_sub" as *u8 } 209 if c == 8 { return "_c_mul" as *u8 } 210 if c == 9 { return "_c_shl" as *u8 } 211 if c == 10 { return "_c_div" as *u8 } 212 if c == 11 { return "_c_mod" as *u8 } 213 return "_c_abs" as *u8 214} 215func cg_emit_term(ofd: i64, terms: *i64, ix: i64) -> i64 { 216 let kind: i64 = terms[ix*5+0] 217 if kind == 0 { if terms[ix*5+1] == 0 { _cg_fputs(ofd, "a" as *u8) } else { _cg_fputs(ofd, "b" as *u8) } return 0 } 218 if kind == 1 { _cg_fsig(ofd, terms[ix*5+1]); return 0 } 219 _cg_fputs(ofd, cg_comp_name(terms[ix*5+1])); _cg_fputs(ofd, "(" as *u8) 220 cg_emit_term(ofd, terms, terms[ix*5+2]) 221 if cg_arity(terms[ix*5+1]) == 2 { _cg_fputs(ofd, ", " as *u8); cg_emit_term(ofd, terms, terms[ix*5+3]) } 222 _cg_fputs(ofd, ")" as *u8) 223 return 0 224} 225func cg_emit_module(path: *u8, terms: *i64, ix: i64, ka: *i64, kb: *i64, kx: *i64, kk: i64) -> i64 { 226 let ofd: i64 = sys_openat_wr(path, 0x1a4) 227 if ofd < 0 { return 0 - 1 } 228 _cg_fputs(ofd, "// CONVERGED BY THE NISHI TEAM CEGIS LOOP (_cegis_authored): counterexample-guided,\n" as *u8) 229 _cg_fputs(ofd, "// zero disagreements with the oracle on the full probe domain. NOT retrieved.\n" as *u8) 230 _cg_fputs(ofd, "import \"nx_syscalls.nx\"\n" as *u8) 231 _cg_fputs(ofd, "func _c_le(a: i64, b: i64) -> i64 { if a <= b { return 1 } return 0 }\n" as *u8) 232 _cg_fputs(ofd, "func _c_and(a: i64, b: i64) -> i64 { return a & b }\n" as *u8) 233 _cg_fputs(ofd, "func _c_shr(a: i64, b: i64) -> i64 { return a >> (b & 63) }\n" as *u8) 234 _cg_fputs(ofd, "func _c_min(a: i64, b: i64) -> i64 { if a < b { return a } return b }\n" as *u8) 235 _cg_fputs(ofd, "func _c_max(a: i64, b: i64) -> i64 { if a > b { return a } return b }\n" as *u8) 236 _cg_fputs(ofd, "func _c_add(a: i64, b: i64) -> i64 { return a + b }\n" as *u8) 237 _cg_fputs(ofd, "func _c_sub(a: i64, b: i64) -> i64 { return a - b }\n" as *u8) 238 _cg_fputs(ofd, "func _c_mul(a: i64, b: i64) -> i64 { return a * b }\n" as *u8) 239 _cg_fputs(ofd, "func _c_shl(a: i64, b: i64) -> i64 { return a << (b & 63) }\n" as *u8) 240 _cg_fputs(ofd, "func _c_div(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a / b }\n" as *u8) 241 _cg_fputs(ofd, "func _c_mod(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a % b }\n" as *u8) 242 _cg_fputs(ofd, "func _c_abs(a: i64) -> i64 { if a < 0 { return 0 - a } return a }\n" as *u8) 243 _cg_fputs(ofd, "func resynth(a: i64, b: i64) -> i64 { return " as *u8) 244 cg_emit_term(ofd, terms, ix) 245 _cg_fputs(ofd, " }\n" as *u8) 246 _cg_fputs(ofd, "func main() -> i64 {\n" as *u8) 247 _cg_fputs(ofd, " let ka: *i64 = sys_mmap(256) as *i64\n" as *u8) 248 _cg_fputs(ofd, " let kb: *i64 = sys_mmap(256) as *i64\n" as *u8) 249 _cg_fputs(ofd, " let kx: *i64 = sys_mmap(256) as *i64\n" as *u8) 250 var q: i64 = 0 251 while q < kk { 252 _cg_fputs(ofd, " ka[" as *u8); _cg_fnum(ofd, q); _cg_fputs(ofd, "] = " as *u8); _cg_fsig(ofd, ka[q]); _cg_fputs(ofd, "\n" as *u8) 253 _cg_fputs(ofd, " kb[" as *u8); _cg_fnum(ofd, q); _cg_fputs(ofd, "] = " as *u8); _cg_fsig(ofd, kb[q]); _cg_fputs(ofd, "\n" as *u8) 254 _cg_fputs(ofd, " kx[" as *u8); _cg_fnum(ofd, q); _cg_fputs(ofd, "] = " as *u8); _cg_fsig(ofd, kx[q]); _cg_fputs(ofd, "\n" as *u8) 255 q = q + 1 256 } 257 _cg_fputs(ofd, " var i: i64 = 0\n" as *u8) 258 _cg_fputs(ofd, " while i < " as *u8); _cg_fnum(ofd, kk); _cg_fputs(ofd, " {\n" as *u8) 259 _cg_fputs(ofd, " if resynth(ka[i], kb[i]) != kx[i] { sys_exit(1) }\n" as *u8) 260 _cg_fputs(ofd, " i = i + 1\n" as *u8) 261 _cg_fputs(ofd, " }\n" as *u8) 262 _cg_fputs(ofd, " sys_exit(0)\n return 0\n}\n" as *u8) 263 sys_close(ofd) 264 return 0 265} 266func cg_corpus_line(label: *u8, verdict: *u8, terms: *i64, ix: i64, rounds: i64, kk: i64, cand: i64) -> i64 { 267 let cfd: i64 = sys_openat_append("knowledge/library/synth_corpus.log" as *u8, 0x1a4) 268 if cfd < 0 { return 0 - 1 } 269 _cg_fputs(cfd, "SYNTH engine=cegis spec=" as *u8); _cg_fputs(cfd, label) 270 _cg_fputs(cfd, " verdict=" as *u8); _cg_fputs(cfd, verdict) 271 _cg_fputs(cfd, " rounds=" as *u8); _cg_fnum(cfd, rounds) 272 _cg_fputs(cfd, " k=" as *u8); _cg_fnum(cfd, kk) 273 _cg_fputs(cfd, " cand=" as *u8); _cg_fnum(cfd, cand) 274 _cg_fputs(cfd, " expr=" as *u8) 275 if ix >= 0 { cg_emit_term(cfd, terms, ix) } else { _cg_fputs(cfd, "none" as *u8) } 276 _cg_fputs(cfd, "\n" as *u8) 277 sys_close(cfd) 278 return 0 279} 280func cg_solve(label: *u8, path: *u8, oid: i64, cons: *i64, ncon: i64, terms: *i64, vecs: *i64, hash: *i64) -> i64 { 281 let ka: *i64 = sys_mmap(256) as *i64 282 let kb: *i64 = sys_mmap(256) as *i64 283 let kx: *i64 = sys_mmap(256) as *i64 284 let kbox: *i64 = sys_mmap(16) as *i64 285 let stats: *i64 = sys_mmap(64) as *i64 286 ka[0] = 0 287 kb[0] = 0 288 ka[1] = 1 289 kb[1] = 1 290 ka[2] = 16 291 kb[2] = 8 292 ka[3] = 100 293 kb[3] = 50 294 var s: i64 = 0 295 while s < 4 { kx[s] = cg_oracle(oid, ka[s], kb[s]); s = s + 1 } 296 kbox[0] = 4 297 var round: i64 = 0 298 var won: i64 = 0 299 var done: i64 = 0 300 while done == 0 { 301 round = round + 1 302 if round > CG_MAXROUND { _cg_puts("CEGIS spec=" as *u8); _cg_puts(label); _cg_puts(" ROUNDS-CAP (honest stop)\n" as *u8); cg_corpus_line(label, "ROUNDS-CAP" as *u8, terms, 0 - 1, round, kbox[0], stats[0]); done = 1 } 303 else { 304 stats[3] = 0 305 let r: i64 = cg_search(ka, kb, kx, kbox[0], cons, ncon, terms, vecs, hash, stats) 306 if r < 0 { _cg_puts("CEGIS spec=" as *u8); _cg_puts(label); _cg_puts(" SEARCH-EXHAUSTED round=" as *u8); _cg_num(round); _cg_puts("\n" as *u8); cg_corpus_line(label, "EXHAUSTED" as *u8, terms, 0 - 1, round, kbox[0], stats[0]); done = 1 } 307 else { 308 let cx: i64 = cg_find_cex(terms, r, oid, ka, kb, kx, kbox) 309 if cx == 0 { 310 _cg_puts("CEGIS spec=" as *u8); _cg_puts(label) 311 _cg_puts(" CONVERGED rounds=" as *u8); _cg_num(round) 312 _cg_puts(" k=" as *u8); _cg_num(kbox[0]) 313 _cg_puts(" cand=" as *u8); _cg_num(stats[0]) 314 _cg_puts(" -> " as *u8); _cg_puts(path); _cg_puts("\n" as *u8) 315 cg_emit_module(path, terms, r, ka, kb, kx, kbox[0]) 316 cg_corpus_line(label, "CONVERGED" as *u8, terms, r, round, kbox[0], stats[0]) 317 won = 1 318 done = 1 319 } 320 else { if cx == 2 { _cg_puts("CEGIS spec=" as *u8); _cg_puts(label); _cg_puts(" K-CAP (honest stop)\n" as *u8); cg_corpus_line(label, "K-CAP" as *u8, terms, 0 - 1, round, kbox[0], stats[0]); done = 1 } } 321 } 322 } 323 } 324 return won 325} 326func main() -> i64 { 327 _cg_puts("=== BUILDER-AUTHORED CEGIS: oracle-driven counterexample loop, 3 convergences ===\n" as *u8) 328 let terms: *i64 = sys_mmap(2097152) as *i64 329 let vecs: *i64 = sys_mmap(8388608) as *i64 330 let hash: *i64 = sys_mmap(1048576) as *i64 331 let cons: *i64 = sys_mmap(64) as *i64 332 cons[0] = 0 333 cons[1] = 1 334 cons[2] = 3 335 cons[3] = 7 336 cons[4] = 10 337 cons[5] = 99 338 var won: i64 = 0 339 won = won + cg_solve("validator-core" as *u8, "runtime/_hdl_build/_cegis_validator.nx" as *u8, 1, cons, 6, terms, vecs, hash) 340 won = won + cg_solve("bitfield-extract" as *u8, "runtime/_hdl_build/_cegis_bitfield.nx" as *u8, 2, cons, 6, terms, vecs, hash) 341 won = won + cg_solve("clamp" as *u8, "runtime/_hdl_build/_cegis_clamp.nx" as *u8, 3, cons, 6, terms, vecs, hash) 342 _cg_puts("CEGIS GATE: " as *u8); _cg_num(won); _cg_puts("/3 converged on the full probe domain\n" as *u8) 343 if won == 3 { sys_exit(0); return 0 } 344 sys_exit(1) 345 return 1 346}