code wiki / _hdl_build / _type_search_authored.nx
`_type_search_authored.nx` source

↩ module page · 351 lines · 14958 B
1// AUTHORED BY THE NISHI BUILDER (nx_module_author type-search template) -- S3 rung-1 synthesizer.
2// Obs-equiv bottom-up search; tutoring: specs/2026-06-09-tutoring-code-synthesis-rung1.md PART B.
3import "nx_syscalls.nx"
4func _ts_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 _ts_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 _ts_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 _ts_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 _ts_fsig(fd2: i64, v: i64) -> i64 { if v < 0 { _ts_fputs(fd2, "0 - " as *u8); _ts_fnum(fd2, 0 - v) } else { _ts_fnum(fd2, v) } return 0 }
9const TS_K: i64 = 8
10const TS_NCOMP: i64 = 12
11const TS_MAXTERM: i64 = 30000
12const TS_MAXLVL: i64 = 4
13const TS_HCAP: i64 = 131072
14const TS_BUDGET: i64 = 8000000
15func ts_arity(c: i64) -> i64 { if c == 12 { return 1 } return 2 }
16func ts_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 ts_apply(c: i64, a: i64, b: i64) -> i64 {
  if c == 1 { if a <= b { return 1 } return 0 }
  if c == 2 { return a & b }
  if c == 3 { return a >> (b & 63) }
  if c == 4 { if a < b { return a } return b }
  if c == 5 { if a > b { return a } return b }
  if c == 6 { return a + b }
  if c == 7 { return a - b }
  if c == 8 { return a * b }
  if c == 9 { return a << (b & 63) }
  if c == 10 { if b == 0 { return 0 } return a / b }
  if c == 11 { if b == 0 { return 0 } return a % b }
  if c == 12 { if a < 0 { return 0 - a } return a }
  return 0
31}
32func ts_vech(vecs: *i64, ix: i64) -> i64 {
  var h: i64 = 1469
  var k: i64 = 0
  while k < TS_K { h = h * 131 + vecs[ix*TS_K+k]; k = k + 1 }
  if h < 0 { h = 0 - h }
  return h
38}
39func ts_vec_eq(vecs: *i64, x: i64, y: i64) -> i64 {
  var k: i64 = 0
  while k < TS_K { if vecs[x*TS_K+k] != vecs[y*TS_K+k] { return 0 } k = k + 1 }
  return 1
43}
44func ts_insert(vecs: *i64, hash: *i64, nterm: i64) -> i64 {
  let h0: i64 = ts_vech(vecs, nterm) & (TS_HCAP - 1)
  var s: i64 = h0
  var go: i64 = 1
  while go == 1 {
      if hash[s] == 0 { hash[s] = nterm + 1; return 1 }
      if ts_vec_eq(vecs, hash[s] - 1, nterm) == 1 { return 0 }
      s = s + 1
      if s >= TS_HCAP { s = 0 }
      if s == h0 { return 0 }
  }
  return 0
56}
57func ts_is_target(vecs: *i64, ix: i64, kx: *i64) -> i64 {
  var k: i64 = 0
  while k < TS_K { if vecs[ix*TS_K+k] != kx[k] { return 0 } k = k + 1 }
  return 1
61}
62func ts_search(ka: *i64, kb: *i64, kx: *i64, cons: *i64, ncon: i64, terms: *i64, vecs: *i64, hash: *i64, stats: *i64) -> i64 {
  var s: i64 = 0
  while s < TS_HCAP { hash[s] = 0; s = s + 1 }
  var nt: i64 = 0
  var cand: i64 = 0
  var k: i64 = 0
  k = 0
  while k < TS_K { vecs[nt*TS_K+k] = ka[k]; k = k + 1 }
  terms[nt*5+0] = 0
  terms[nt*5+1] = 0
  terms[nt*5+2] = 0
  terms[nt*5+3] = 0
  terms[nt*5+4] = 1
  if ts_insert(vecs, hash, nt) == 1 { if ts_is_target(vecs, nt, kx) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=1; return nt } nt = nt + 1 }
  k = 0
  while k < TS_K { vecs[nt*TS_K+k] = kb[k]; k = k + 1 }
  terms[nt*5+0] = 0
  terms[nt*5+1] = 1
  terms[nt*5+2] = 0
  terms[nt*5+3] = 0
  terms[nt*5+4] = 1
  if ts_insert(vecs, hash, nt) == 1 { if ts_is_target(vecs, nt, kx) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=1; return nt } nt = nt + 1 }
  var ci: i64 = 0
  while ci < ncon {
      k = 0
      while k < TS_K { vecs[nt*TS_K+k] = cons[ci]; k = k + 1 }
      terms[nt*5+0] = 1
      terms[nt*5+1] = cons[ci]
      terms[nt*5+2] = 0
      terms[nt*5+3] = 0
      terms[nt*5+4] = 1
      if ts_insert(vecs, hash, nt) == 1 { if ts_is_target(vecs, nt, kx) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=1; return nt } nt = nt + 1 }
      ci = ci + 1
  }
  var lvl: i64 = 2
  while lvl <= TS_MAXLVL {
      let n0: i64 = nt
      var c: i64 = 1
      while c <= TS_NCOMP {
          var x: i64 = 0
          while x < n0 {
              if ts_arity(c) == 1 {
                  if terms[x*5+4] == lvl - 1 {
                      if nt >= TS_MAXTERM { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 }
                      if cand > TS_BUDGET { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 }
                      cand = cand + 1
                      k = 0
                      while k < TS_K { vecs[nt*TS_K+k] = ts_apply(c, vecs[x*TS_K+k], 0); k = k + 1 }
                      if ts_insert(vecs, hash, nt) == 1 {
                          terms[nt*5+0] = 2
                          terms[nt*5+1] = c
                          terms[nt*5+2] = x
                          terms[nt*5+3] = 0
                          terms[nt*5+4] = lvl
                          if ts_is_target(vecs, nt, kx) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=lvl; return nt }
                          nt = nt + 1
                      }
                  }
              }
              else {
                  var y: i64 = 0
                  while y < n0 {
                      var mx: i64 = terms[x*5+4]
                      if terms[y*5+4] > mx { mx = terms[y*5+4] }
                      if terms[x*5+0] == 1 { if terms[y*5+0] == 1 { mx = 0 - 1 } }
                      if ts_comm(c) == 1 { if x > y { mx = 0 - 1 } }
                      if mx == lvl - 1 {
                          if nt >= TS_MAXTERM { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 }
                          if cand > TS_BUDGET { stats[0]=cand; stats[1]=nt; stats[2]=lvl; stats[3]=1; return 0 - 1 }
                          cand = cand + 1
                          k = 0
                          while k < TS_K { vecs[nt*TS_K+k] = ts_apply(c, vecs[x*TS_K+k], vecs[y*TS_K+k]); k = k + 1 }
                          if ts_insert(vecs, hash, nt) == 1 {
                              terms[nt*5+0] = 2
                              terms[nt*5+1] = c
                              terms[nt*5+2] = x
                              terms[nt*5+3] = y
                              terms[nt*5+4] = lvl
                              if ts_is_target(vecs, nt, kx) == 1 { stats[0]=cand; stats[1]=nt+1; stats[2]=lvl; return nt }
                              nt = nt + 1
                          }
                      }
                      y = y + 1
                  }
              }
              x = x + 1
          }
          c = c + 1
      }
      lvl = lvl + 1
  }
  stats[0]=cand
  stats[1]=nt
  stats[2]=TS_MAXLVL
  stats[3]=0
  return 0 - 1
158}
159func ts_comp_name(c: i64) -> *u8 {
  if c == 1 { return "_c_le" as *u8 }
  if c == 2 { return "_c_and" as *u8 }
  if c == 3 { return "_c_shr" as *u8 }
  if c == 4 { return "_c_min" as *u8 }
  if c == 5 { return "_c_max" as *u8 }
  if c == 6 { return "_c_add" as *u8 }
  if c == 7 { return "_c_sub" as *u8 }
  if c == 8 { return "_c_mul" as *u8 }
  if c == 9 { return "_c_shl" as *u8 }
  if c == 10 { return "_c_div" as *u8 }
  if c == 11 { return "_c_mod" as *u8 }
  return "_c_abs" as *u8
172}
173func ts_emit_term(ofd: i64, terms: *i64, ix: i64) -> i64 {
  let kind: i64 = terms[ix*5+0]
  if kind == 0 { if terms[ix*5+1] == 0 { _ts_fputs(ofd, "a" as *u8) } else { _ts_fputs(ofd, "b" as *u8) } return 0 }
  if kind == 1 { _ts_fsig(ofd, terms[ix*5+1]); return 0 }
  _ts_fputs(ofd, ts_comp_name(terms[ix*5+1])); _ts_fputs(ofd, "(" as *u8)
  ts_emit_term(ofd, terms, terms[ix*5+2])
  if ts_arity(terms[ix*5+1]) == 2 { _ts_fputs(ofd, ", " as *u8); ts_emit_term(ofd, terms, terms[ix*5+3]) }
  _ts_fputs(ofd, ")" as *u8)
  return 0
182}
183func ts_emit_module(path: *u8, terms: *i64, ix: i64, ka: *i64, kb: *i64, kx: *i64) -> i64 {
  let ofd: i64 = sys_openat_wr(path, 0x1a4)
  if ofd < 0 { return 0 - 1 }
  _ts_fputs(ofd, "// RE-SYNTHESIZED BY THE NISHI TEAM (_type_search_authored): derived from KATs by\n" as *u8)
  _ts_fputs(ofd, "// observational-equivalence search over a primitive pool. NOT retrieved -- the pool\n" as *u8)
  _ts_fputs(ofd, "// holds no team function bodies. Silent main: exit 0 iff every KAT passes.\n" as *u8)
  _ts_fputs(ofd, "import \"nx_syscalls.nx\"\n" as *u8)
  _ts_fputs(ofd, "func _c_le(a: i64, b: i64) -> i64 { if a <= b { return 1 } return 0 }\n" as *u8)
  _ts_fputs(ofd, "func _c_and(a: i64, b: i64) -> i64 { return a & b }\n" as *u8)
  _ts_fputs(ofd, "func _c_shr(a: i64, b: i64) -> i64 { return a >> (b & 63) }\n" as *u8)
  _ts_fputs(ofd, "func _c_min(a: i64, b: i64) -> i64 { if a < b { return a } return b }\n" as *u8)
  _ts_fputs(ofd, "func _c_max(a: i64, b: i64) -> i64 { if a > b { return a } return b }\n" as *u8)
  _ts_fputs(ofd, "func _c_add(a: i64, b: i64) -> i64 { return a + b }\n" as *u8)
  _ts_fputs(ofd, "func _c_sub(a: i64, b: i64) -> i64 { return a - b }\n" as *u8)
  _ts_fputs(ofd, "func _c_mul(a: i64, b: i64) -> i64 { return a * b }\n" as *u8)
  _ts_fputs(ofd, "func _c_shl(a: i64, b: i64) -> i64 { return a << (b & 63) }\n" as *u8)
  _ts_fputs(ofd, "func _c_div(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a / b }\n" as *u8)
  _ts_fputs(ofd, "func _c_mod(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a % b }\n" as *u8)
  _ts_fputs(ofd, "func _c_abs(a: i64) -> i64 { if a < 0 { return 0 - a } return a }\n" as *u8)
  _ts_fputs(ofd, "func resynth(a: i64, b: i64) -> i64 { return " as *u8)
  ts_emit_term(ofd, terms, ix)
  _ts_fputs(ofd, " }\n" as *u8)
  _ts_fputs(ofd, "func main() -> i64 {\n" as *u8)
  _ts_fputs(ofd, "    let ka: *i64 = sys_mmap(64) as *i64\n" as *u8)
  _ts_fputs(ofd, "    let kb: *i64 = sys_mmap(64) as *i64\n" as *u8)
  _ts_fputs(ofd, "    let kx: *i64 = sys_mmap(64) as *i64\n" as *u8)
  var k: i64 = 0
  while k < TS_K {
      _ts_fputs(ofd, "    ka[" as *u8); _ts_fnum(ofd, k); _ts_fputs(ofd, "] = " as *u8); _ts_fsig(ofd, ka[k]); _ts_fputs(ofd, "\n" as *u8)
      _ts_fputs(ofd, "    kb[" as *u8); _ts_fnum(ofd, k); _ts_fputs(ofd, "] = " as *u8); _ts_fsig(ofd, kb[k]); _ts_fputs(ofd, "\n" as *u8)
      _ts_fputs(ofd, "    kx[" as *u8); _ts_fnum(ofd, k); _ts_fputs(ofd, "] = " as *u8); _ts_fsig(ofd, kx[k]); _ts_fputs(ofd, "\n" as *u8)
      k = k + 1
  }
  _ts_fputs(ofd, "    var i: i64 = 0\n" as *u8)
  _ts_fputs(ofd, "    while i < 8 {\n" as *u8)
  _ts_fputs(ofd, "        if resynth(ka[i], kb[i]) != kx[i] { sys_exit(1) }\n" as *u8)
  _ts_fputs(ofd, "        i = i + 1\n" as *u8)
  _ts_fputs(ofd, "    }\n" as *u8)
  _ts_fputs(ofd, "    sys_exit(0)\n    return 0\n}\n" as *u8)
  sys_close(ofd)
  return 0
224}
225func ts_corpus_line(label: *u8, verdict: *u8, terms: *i64, ix: i64, kept: i64, cand: i64) -> i64 {
  let cfd: i64 = sys_openat_append("knowledge/library/synth_corpus.log" as *u8, 0x1a4)
  if cfd < 0 { return 0 - 1 }
  _ts_fputs(cfd, "SYNTH engine=type-search spec=" as *u8); _ts_fputs(cfd, label)
  _ts_fputs(cfd, " verdict=" as *u8); _ts_fputs(cfd, verdict)
  _ts_fputs(cfd, " kept=" as *u8); _ts_fnum(cfd, kept)
  _ts_fputs(cfd, " cand=" as *u8); _ts_fnum(cfd, cand)
  _ts_fputs(cfd, " expr=" as *u8)
  if ix >= 0 { ts_emit_term(cfd, terms, ix) } else { _ts_fputs(cfd, "none" as *u8) }
  _ts_fputs(cfd, "\n" as *u8)
  sys_close(cfd)
  return 0
237}
238func ts_round(label: *u8, path: *u8, ka: *i64, kb: *i64, kx: *i64, cons: *i64, ncon: i64, terms: *i64, vecs: *i64, hash: *i64) -> i64 {
  let stats: *i64 = sys_mmap(64) as *i64
  stats[3] = 0
  let r: i64 = ts_search(ka, kb, kx, cons, ncon, terms, vecs, hash, stats)
  _ts_puts("TSRCH spec=" as *u8); _ts_puts(label)
  _ts_puts(" cand=" as *u8); _ts_num(stats[0])
  _ts_puts(" kept=" as *u8); _ts_num(stats[1])
  _ts_puts(" lvl=" as *u8); _ts_num(stats[2])
  if r < 0 {
      if stats[3] == 1 { _ts_puts(" SEARCH-EXHAUSTED (budget/term-cap)\n" as *u8) } else { _ts_puts(" SEARCH-EXHAUSTED (depth)\n" as *u8) }
      ts_corpus_line(label, "EXHAUSTED" as *u8, terms, 0 - 1, stats[1], stats[0])
      return 0
  }
  _ts_puts(" FOUND -> " as *u8); _ts_puts(path); _ts_puts("\n" as *u8)
  ts_emit_module(path, terms, r, ka, kb, kx)
  ts_corpus_line(label, "FOUND" as *u8, terms, r, stats[1], stats[0])
  return 1
255}
256func main() -> i64 {
  _ts_puts("=== BUILDER-AUTHORED TYPE-SEARCH: obs-equiv synthesis, 3 held-out re-derivations ===\n" as *u8)
  let terms: *i64 = sys_mmap(1310720) as *i64
  let vecs: *i64 = sys_mmap(2097152) as *i64
  let hash: *i64 = sys_mmap(1048576) as *i64
  let cons: *i64 = sys_mmap(64) as *i64
  cons[0] = 0
  cons[1] = 1
  cons[2] = 3
  cons[3] = 7
  cons[4] = 10
  cons[5] = 99
  let ka: *i64 = sys_mmap(64) as *i64
  let kb: *i64 = sys_mmap(64) as *i64
  let kx: *i64 = sys_mmap(64) as *i64
  var won: i64 = 0
  ka[0]=10
  ka[1]=9
  ka[2]=10
  ka[3]=20
  ka[4]=50
  ka[5]=100
  ka[6]=9
  ka[7]=10
  kb[0]=99
  kb[1]=99
  kb[2]=100
  kb[3]=40
  kb[4]=42
  kb[5]=99
  kb[6]=0
  kb[7]=1000
  kx[0]=1
  kx[1]=0
  kx[2]=0
  kx[3]=1
  kx[4]=1
  kx[5]=1
  kx[6]=0
  kx[7]=0
  won = won + ts_round("validator-core" as *u8, "runtime/_hdl_build/_resynth_validator.nx" as *u8, ka, kb, kx, cons, 6, terms, vecs, hash)
  ka[0]=180
  ka[1]=255
  ka[2]=8
  ka[3]=1023
  ka[4]=64
  ka[5]=7
  ka[6]=256
  ka[7]=5
  kb[0]=2
  kb[1]=0
  kb[2]=3
  kb[3]=7
  kb[4]=6
  kb[5]=0
  kb[6]=8
  kb[7]=1
  kx[0]=5
  kx[1]=7
  kx[2]=1
  kx[3]=7
  kx[4]=1
  kx[5]=7
  kx[6]=1
  kx[7]=2
  won = won + ts_round("bitfield-extract" as *u8, "runtime/_hdl_build/_resynth_bitfield.nx" as *u8, ka, kb, kx, cons, 6, terms, vecs, hash)
  ka[0]=5
  ka[1]=0-3
  ka[2]=15
  ka[3]=0
  ka[4]=0-100
  ka[5]=7
  ka[6]=100
  ka[7]=0-1
  kb[0]=10
  kb[1]=10
  kb[2]=10
  kb[3]=0
  kb[4]=50
  kb[5]=7
  kb[6]=3
  kb[7]=0
  kx[0]=5
  kx[1]=0
  kx[2]=10
  kx[3]=0
  kx[4]=0
  kx[5]=7
  kx[6]=3
  kx[7]=0
  won = won + ts_round("clamp" as *u8, "runtime/_hdl_build/_resynth_clamp.nx" as *u8, ka, kb, kx, cons, 6, terms, vecs, hash)
  _ts_puts("TYPE-SEARCH GATE: " as *u8); _ts_num(won); _ts_puts("/3 re-synthesized (Engineer builds+runs the emitted modules next)\n" as *u8)
  if won == 3 { sys_exit(0); return 0 }
  sys_exit(1)
  return 1
351}
_type_search_authored.nx source

`_type_search_authored.nx` source
