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

↩ module page · 244 lines · 11794 B
1import "nx_gate_gn.nx"
2import "nx_gate_base.nx"
3// nx_ncf_loop_gate.nx -- X-AUT-NCF-001 RUNG 2: SYNTHESIZE A BOUNDED LOOP (iteration) -- a strictly stronger
4// control-flow construct than rung 1's conditional. Escalation discipline: rung 1 proved branch>linear; this
5// proves LOOP>(branch AND linear). Target 2^x is EXPONENTIAL, so the negative controls are decisive:
6//   T1 linear-only synthesis PROVABLY FAILS (no op-list = exponential)
7//   T2 single-conditional (rung-1 branch) PROVABLY FAILS (2 affine regions cannot fit 5 exponential points)
8//   -> only a LOOP fits. T3 the organ SEARCHES a bounded-loop grammar + finds acc=1; repeat x: acc*=2.
9//   T4 MATERIALIZE the synthesized loop -> GOD-BUILD (nx_cc->nxasm, no gcc) -> run HELD-OUT {5->32,6->64}.
10//   T5 GENERALITY: a 2nd loop spec (sum 1..x) synthesizes a DIFFERENT loop body (uses the index i).
11// Builds ON the god-cycle materialize->god-build->verify mechanism. NOTE: search_linear/search_branch are
12// re-included as the gate's self-contained negative controls (ecosystem gate style); the clean DRY follow-up
13// is to extract nx_ncf_synth.nx (shared grammar+searchers+materialize) for all rungs to import.
14// expect_exit: 0  license_tier: ORIGINAL
15import "nx_syscalls.nx"
16
17const NCL_ORGAN:  *u8 = "runtime/_hdl_build/ncf_loop_organ.nx"
18const NCL_NAME:   *u8 = "ncf_loop_organ"
19const NCL_RESULT: *u8 = "knowledge/status/ncf_loop_out.bin"
20const NCL_RUNNER: *u8 = "_offc/nx_sov_build_run.elf"
21
22func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw("  PASS " as *u8) } else { gw("  FAIL " as *u8) } gw(name); gw("
23" as *u8); return ok }
24func gcat(buf: *u8, off: i64, s: *u8) -> i64 { var o: i64=off; var i: i64=0; while s[i]!=(0 as u8){ buf[o]=s[i]; o=o+1; i=i+1 } return o }
25func gcatn(buf: *u8, off: i64, v: i64) -> i64 { var o: i64=off; if v==0 { buf[o]=48 as u8; return o+1 } var m: i64=v; if m<0 { buf[o]=45 as u8; o=o+1; m=0-m } let t: *u8=sys_mmap(24); var k: i64=0; while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 } var i: i64=0; while i<k { buf[o]=t[k-1-i]; o=o+1; i=i+1 } return o }
26
27// ---- negative-control grammar (rung 1): affine ops + a single conditional ----
28func op_eval(op: i64, arg: i64, x: i64) -> i64 {
  if op==0 { return x }
  if op==1 { return 0 - x }
  if op==2 { return x + arg }
  if op==3 { return x * arg }
  if op==4 { return x * 0 }
  return x
35}
36func pred_eval(pred: i64, k: i64, x: i64) -> i64 {
  if pred==0 { if x<0 { return 1 } return 0 }
  if pred==1 { if x<k { return 1 } return 0 }
  if pred==2 { if x>k { return 1 } return 0 }
  return 0
41}
42func search_linear(xs: *i64, ys: *i64, n: i64) -> i64 {
  var op1: i64=0
  while op1<5 {
      var a1: i64=0-4
      while a1<=4 {
          var ok: i64=1; var i: i64=0
          while i<n { if op_eval(op1,a1,xs[i])!=ys[i] { ok=0; i=n } else { i=i+1 } }
          if ok==1 { return 1 }
          a1=a1+1
      }
      op1=op1+1
  }
  var p: i64=0
  while p<5 {
      var qq: i64=0
      while qq<5 {
          var a: i64=0-3
          while a<=3 {
              var b: i64=0-3
              while b<=3 {
                  var ok2: i64=1; var j: i64=0
                  while j<n { let r1: i64=op_eval(p,a,xs[j]); if op_eval(qq,b,r1)!=ys[j] { ok2=0; j=n } else { j=j+1 } }
                  if ok2==1 { return 1 }
                  b=b+1
              }
              a=a+1
          }
          qq=qq+1
      }
      p=p+1
  }
  return 0
74}
75func search_branch(xs: *i64, ys: *i64, n: i64) -> i64 {
  var pred: i64=0
  while pred<3 {
      var k: i64=0-3
      while k<=3 {
          var top: i64=0
          while top<5 {
              var ta: i64=0-3
              while ta<=3 {
                  var eop: i64=0
                  while eop<5 {
                      var ea: i64=0-3
                      while ea<=3 {
                          var ok: i64=1; var i: i64=0
                          while i<n {
                              var r: i64=0
                              if pred_eval(pred,k,xs[i])==1 { r=op_eval(top,ta,xs[i]) } else { r=op_eval(eop,ea,xs[i]) }
                              if r!=ys[i] { ok=0; i=n } else { i=i+1 }
                          }
                          if ok==1 { return 1 }
                          ea=ea+1
                      }
                      eop=eop+1
                  }
                  ta=ta+1
              }
              top=top+1
          }
          k=k+1
      }
      pred=pred+1
  }
  return 0
108}
109
110// ---- the NEW construct: a bounded loop  acc=init; for i in 1..=x { acc = body(acc,i,c) }  ----
111// body ops: 0 = acc+c   1 = acc*c   2 = acc+i   3 = acc*i
112func loop_eval(init: i64, bop: i64, c: i64, x: i64) -> i64 {
  var acc: i64=init
  var i: i64=1
  while i<=x {
      if bop==0 { acc=acc+c }
      if bop==1 { acc=acc*c }
      if bop==2 { acc=acc+i }
      if bop==3 { acc=acc*i }
      i=i+1
  }
  return acc
123}
124// search the loop grammar; fill form=[init,bop,c]; return 1 if a loop fits all examples.
125func search_loop(xs: *i64, ys: *i64, n: i64, form: *i64) -> i64 {
  var init: i64=0
  while init<3 {
      var bop: i64=0
      while bop<4 {
          var c: i64=0-2
          while c<=3 {
              var ok: i64=1; var i: i64=0
              while i<n { if loop_eval(init,bop,c,xs[i])!=ys[i] { ok=0; i=n } else { i=i+1 } }
              if ok==1 { form[0]=init; form[1]=bop; form[2]=c; return 1 }
              c=c+1
          }
          bop=bop+1
      }
      init=init+1
  }
  return 0
142}
143
144func cat_body(buf: *u8, off: i64, bop: i64, c: i64) -> i64 {
  var o: i64=off
  if bop==0 { o=gcat(buf,o,"        acc = acc + " as *u8); o=gcatn(buf,o,c) }
  if bop==1 { o=gcat(buf,o,"        acc = acc * " as *u8); o=gcatn(buf,o,c) }
  if bop==2 { o=gcat(buf,o,"        acc = acc + i" as *u8) }
  if bop==3 { o=gcat(buf,o,"        acc = acc * i" as *u8) }
  o=gcat(buf,o,"\n" as *u8)
  return o
152}
153// MATERIALIZE the synthesized loop as a real organ testing HELD-OUT {5->32, 6->64} -> (f(5)*1000)+f(6).
154func emit_loop(form: *i64) -> i64 {
  let buf: *u8=sys_mmap(8192); var o: i64=0
  o=gcat(buf,o,"// SYNTHESIZED CONTROL FLOW (a bounded loop) + GOD-BUILT by nx_ncf_loop_gate. license_tier: ORIGINAL\n" as *u8)
  o=gcat(buf,o,"import \"nx_syscalls.nx\"\nfunc f(x: i64) -> i64 {\n    var acc: i64 = " as *u8)
  o=gcatn(buf,o,form[0])
  o=gcat(buf,o,"\n    var i: i64 = 1\n    while i <= x {\n" as *u8)
  o=cat_body(buf,o,form[1],form[2])
  o=gcat(buf,o,"        i = i + 1\n    }\n    return acc\n}\n" as *u8)
  o=gcat(buf,o,"func main() -> i64 {\n    let p: *i64 = sys_mmap(8) as *i64\n    p[0] = (f(5) * 1000) + f(6)\n    let fd: i64 = sys_openat_wr(\"knowledge/status/ncf_loop_out.bin\" as *u8, 420)\n    if fd >= 0 { sys_write(fd, p as *u8, 8); sys_close(fd) }\n    return 0\n}\n" as *u8)
  let fd: i64=sys_openat_wr(NCL_ORGAN,420)
  if fd<0 { return 0-1 }
  sys_write(fd,buf,o); sys_close(fd)
  return 0
167}
168func god_build(name: *u8) -> i64 {
  let pid: i64=sys_fork()
  if pid==0 {
      let dn: i64=sys_openat_wr("/dev/null\x00" as *u8,420)
      if dn>=0 { sys_dup3(dn,1,0); sys_dup3(dn,2,0) }
      let argv: *i64=sys_mmap(64) as *i64
      argv[0]=NCL_RUNNER as i64; argv[1]=name as i64; argv[2]=0
      let envp: *i64=sys_mmap(16) as *i64
      envp[0]="PATH=/usr/bin:/bin" as *u8 as i64; envp[1]=0
      sys_execve(NCL_RUNNER,argv,envp)
      sys_exit(127)
  }
  let st: *i64=sys_mmap(16) as *i64
  sys_wait4(pid,st,0)
  return (st[0]>>8)&0xff
183}
184func read_i64(path: *u8) -> i64 {
  let lenp: *i64=sys_mmap(16) as *i64
  let buf: *u8=sys_read_file(path,lenp)
  if (buf as i64)==0 { return 0-999999 }
  if lenp[0]<8 { return 0-888888 }
  let p: *i64=buf as *i64
  return p[0]
191}
192
193func main() -> i64 {
  gw("=== nx_ncf_loop: SYNTHESIZE A BOUNDED LOOP (X-AUT-NCF-001 rung 2) -- LOOP > (branch AND linear) ===\n" as *u8)
  var pass: i64=0; var total: i64=0
196
  // SPEC = 2^x: exponential -> needs a LOOP. examples {0..4}, HELD-OUT {5->32, 6->64}.
  let xs: *i64=sys_mmap(64) as *i64; let ys: *i64=sys_mmap(64) as *i64
  xs[0]=0; xs[1]=1; xs[2]=2; xs[3]=3; xs[4]=4
  ys[0]=1; ys[1]=2; ys[2]=4; ys[3]=8; ys[4]=16
  let n: i64=5
202
  let sp: *i64=sys_mmap(8) as *i64; sp[0]=0-1
  let sfd: i64=sys_openat_wr(NCL_RESULT,420); if sfd>=0 { sys_write(sfd,sp as *u8,8); sys_close(sfd) }
205
  // T1 NEG-CONTROL A: linear-only FAILS (exponential is not affine).
  let lin: i64=search_linear(xs,ys,n)
  total=total+1; if lin==0 { pass=pass+1; gw("  [PASS] " as *u8) } else { gw("  [FAIL] " as *u8) }
  gw("T1 NEG-CONTROL: linear-only synthesis FAILS on 2^x, lin_found=" as *u8); gn(lin); gw("\n" as *u8)
210
  // T2 NEG-CONTROL B (the key escalation): a single CONDITIONAL also FAILS -> a LOOP is necessary.
  let br: i64=search_branch(xs,ys,n)
  total=total+1; if br==0 { pass=pass+1; gw("  [PASS] " as *u8) } else { gw("  [FAIL] " as *u8) }
  gw("T2 NEG-CONTROL: single-conditional (rung 1) FAILS on 2^x (2 affine regions != exponential) -> LOOP necessary, branch_found=" as *u8); gn(br); gw("\n" as *u8)
215
  // T3 SYNTHESIS: the organ searches the bounded-loop grammar + authors the loop.
  let form: *i64=sys_mmap(64) as *i64
  let lp: i64=search_loop(xs,ys,n,form)
  total=total+1; if lp==1 { pass=pass+1; gw("  [PASS] " as *u8) } else { gw("  [FAIL] " as *u8) }
  gw("T3 SYNTHESIS: loop SEARCHED+FOUND acc=" as *u8); gn(form[0]); gw("; repeat x { body=" as *u8); gn(form[1]); gw(" c=" as *u8); gn(form[2]); gw(" } for 2^x\n" as *u8)
221
  // T4 MATERIALIZE -> GOD-BUILD -> run HELD-OUT -> verify (2^5=32, 2^6=64 -> 32064).
  var emitted: i64=0; if lp==1 { if emit_loop(form)==0 { emitted=1 } }
  var built: i64=0; if emitted==1 { if god_build(NCL_NAME)==0 { built=1 } }
  let produced: i64=read_i64(NCL_RESULT)
  total=total+1; if produced==32064 { pass=pass+1; gw("  [PASS] " as *u8) } else { gw("  [FAIL] " as *u8) }
  gw("T4 MATERIALIZE+GOD-BUILD: synthesized loop compiled (nx_cc->nxasm, no gcc) + ran HELD-OUT -> produced=" as *u8); gn(produced); gw(" (expect 32064 = 2^5*1000+2^6)\n" as *u8)
228
  // T5 GENERALITY: sum 1..x needs a DIFFERENT loop body (uses index i); linear still fails.
  let xs2: *i64=sys_mmap(64) as *i64; let ys2: *i64=sys_mmap(64) as *i64
  xs2[0]=0; xs2[1]=1; xs2[2]=2; xs2[3]=3; xs2[4]=4
  ys2[0]=0; ys2[1]=1; ys2[2]=3; ys2[3]=6; ys2[4]=10
  let lin2: i64=search_linear(xs2,ys2,n)
  let form2: *i64=sys_mmap(64) as *i64
  let lp2: i64=search_loop(xs2,ys2,n,form2)
  var diff: i64=0; if form2[1]!=form[1] { diff=1 }
  total=total+1; if lin2==0 { if lp2==1 { if diff==1 { pass=pass+1; gw("  [PASS] " as *u8) } else { gw("  [FAIL] " as *u8) } } else { gw("  [FAIL] " as *u8) } } else { gw("  [FAIL] " as *u8) }
  gw("T5 GENERALITY: sum(1..x) -> linear fails(" as *u8); gn(lin2); gw("), loop synthesized(" as *u8); gn(lp2); gw(") with DIFFERENT body=" as *u8); gn(form2[1]); gw(" (uses index i) vs 2^x body=" as *u8); gn(form[1]); gw("\n" as *u8)
239
  gw("\n  HONEST SCOPE: synthesizes a single bounded loop (one accumulator, index-or-const body) from a fixed grammar; nested loops + loop+branch composition + multi-arg are further rungs. Construct ladder now: linear < conditional < BOUNDED LOOP, each with its own proving negative control.\n" as *u8)
  gw("NCF-LOOP verdict=" as *u8)
  if pass==total { gw("GREEN passes=" as *u8); gn(pass); gw("/" as *u8); gn(total); gw(" -- the team SYNTHESIZED + GOD-BUILT a bounded loop (author-share>0): X-AUT-NCF-001 rung 2\n" as *u8); sys_exit(0); return 0 }
  gw("RED passes=" as *u8); gn(pass); gw("/" as *u8); gn(total); gw("\n" as *u8); sys_exit(1); return 1
244}
nx_ncf_loop_gate.nx source

`nx_ncf_loop_gate.nx` source
