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

↩ module page · 254 lines · 13733 B
1// nx_superopt_test.nx -- GATE + proof for the mechanized superoptimizer organ
2// (nx_superopt.nx, the AUTHOR leg of the Sovereign Invention Engine). Proves, with
3// NO LLM in the loop, one full PROPOSE/SCORE/VERIFY/EMIT invention tick on the
4// smallest end-to-end-provable example:
5//
6//   SEED (mul x 8)  -->  EMIT (shl x 3).
7//
8// It self-asserts a known answer + sys_exit(0), establishing:
9//   (1) the loop FOUND a cheaper equivalent of the seed (cand_count==3, root=SHL,
10//       shift=3) -- PROPOSE via nx_eqsat saturation, EMIT via the extractor.
11//   (2) the cheaper form is TRIANGULATED-EQUIVALENT to the seed over a
12//       dense(exhaustive small-width) + random + edge battery via THREE genuinely
13//       independent legs -- AND we prove the check would CATCH a non-equivalent
14//       candidate (the (shl x 2) negative control is REJECTED by the same battery).
15//   (3) the cost STRICTLY decreased on the honest metric, twice independently:
16//       Tier-1 e-graph op-cost 3 -> 1, AND Tier-2 honest gate-level latency at
17//       W=64: MUL = 2*ceil(log2 64) = 12  ->  SHL = ceil(log2 64) = 6.
18//
19// LEG INDEPENDENCE (the keystone honesty defense -- legs must not collude on the
20// same i64 instruction): LEG0 = candidate emit-DAG interp; LEG1 = candidate
21// lowered-NxGsim gate-sim (independent code path); LEG2 = the SEED's value via a
22// shift-FREE repeated-doubling multiply (never takes the candidate's `<<` path).
23// ORACLE = the SEED emit-DAG (mul x 8) interpreted directly. A wrong shift count
24// makes LEG2 (and the oracle) disagree with LEG0/LEG1 -- exactly what the negative
25// control demonstrates is CAUGHT.
26//
27// KNOWN ANSWER (FAIL LOUD), one line:
28//   "<found> <seed_cost> <cand_cost> <seed_lat> <cand_lat> <root_op> <cand_count>
29//    <bpass> <btotal> <neg_rejected> <neg_first_bad_leg>"
30//   = "1 3 1 12 6 11 3 <N> <N> 1 0 "   where N = battery vector count, root_op 11 = SHL,
31//   neg_rejected 1 = the (shl x 2) wrong candidate FAILED the battery,
32//   neg_first_bad_leg 0 = leg 0 (emit-interp of the wrong candidate) first diverged.
33// Expected: "1 3 1 12 6 11 3 585 585 1 0 " run=0
34
35import "nx_superopt.nx"
36
37const SO_W: i64 = 64        // honest-metric datapath width for Tier-2 scoring
38
39func _emit_num(v: i64) -> i64 {
  let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n }
  let t2: *u8 = sys_mmap(28); var t: i64 = 0
  if n == 0 { t2[0] = 48; t = 1 }
  while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
  var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
  b[t] = 32; sys_write(1, b, t + 1); return 0
46}
47func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
48
49// Compose the single "found" verdict: a strictly-cheaper, fully-triangulated,
50// verified-equivalent candidate was emitted iff the battery was all-pass AND both
51// cost tiers strictly decreased. Pure boolean fold (no side effects).
52func found_or(bpass: i64, btotal: i64, cand_cost: i64, seed_cost: i64) -> i64 {
  if bpass != btotal { return 0 }
  if cand_cost >= seed_cost { return 0 }
  return 1
56}
57
58func main() -> i64 {
  // ===== PROPOSE + EMIT: seed (mul x 8) -> candidate (shl x 3) ==============
  // Build the seed in g, saturate to the equivalence closure, recompute the
  // bottom-up cost extractor, then emit the cost-minimal DAG = the candidate.
  let nodes: *NxENode = sys_mmap(256 * 128) as *NxENode
  let classes: *NxEClass = sys_mmap(256 * 64) as *NxEClass
  let g: *NxEGraph = sys_mmap(256) as *NxEGraph
  if nx_eqsat_init(g, nodes, 256, classes, 256) != NX_EQSAT_OK { sys_exit(10); return 10 }
  let x: i64 = nx_eqsat_add_var(g, 0)
  let eight: i64 = nx_eqsat_add_const(g, 8)
  let seed_root_cls: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_MUL, x, eight)
69
  // Tier-1 SCORE of the SEED, taken BEFORE saturation merges the class, so the
  // cheapest member is still the mul (cost 3). (find() on the pre-saturation
  // class returns the mul; we read its cost via the op model directly.)
  let seed_cost: i64 = nx_eqsat_class_cost(g, seed_root_cls)
74
  let sat: i64 = nx_eqsat_saturate(g, 16)
  if nx_eqsat_recompute_best(g) != NX_EQSAT_OK { sys_exit(11); return 11 }
  let cand_cost: i64 = nx_eqsat_best_cost(g, seed_root_cls)   // Tier-1 candidate cost
78
  // EMIT the candidate (cost-minimal) DAG.
  let cand_out: *NxEmitNode = sys_mmap(64 * 40) as *NxEmitNode
  let cnt: *i64 = sys_mmap(8) as *i64
  cnt[0] = 0
  let cand_root: i64 = nx_eqsat_emit(g, seed_root_cls, cand_out, 64, cnt)
  if cand_root < 0 { sys_exit(12); return 12 }
  let cand_count: i64 = cnt[0]
  let cand_root_op: i64 = cand_out[cand_root].op
87
  // Build the SEED (mul x 8) DAG in a SEPARATE, UN-saturated e-graph so we can
  // emit it as the ORACLE expression (g's root now resolves to the SHL form).
  let snodes: *NxENode = sys_mmap(256 * 128) as *NxENode
  let sclasses: *NxEClass = sys_mmap(256 * 64) as *NxEClass
  let sg: *NxEGraph = sys_mmap(256) as *NxEGraph
  if nx_eqsat_init(sg, snodes, 256, sclasses, 256) != NX_EQSAT_OK { sys_exit(13); return 13 }
  let sx: i64 = nx_eqsat_add_var(sg, 0)
  let s8: i64 = nx_eqsat_add_const(sg, 8)
  let sm: i64 = nx_eqsat_add_binary(sg, NX_EQ_OP_MUL, sx, s8)
  if nx_eqsat_recompute_best(sg) != NX_EQSAT_OK { sys_exit(14); return 14 }
  let seed_out: *NxEmitNode = sys_mmap(64 * 40) as *NxEmitNode
  let scnt: *i64 = sys_mmap(8) as *i64
  scnt[0] = 0
  let seed_root: i64 = nx_eqsat_emit(sg, sm, seed_out, 64, scnt)
  if seed_root < 0 { sys_exit(15); return 15 }
  let seed_count: i64 = scnt[0]
104
  // ===== SCORE Tier-2: lower BOTH DAGs, honest width-weighted critical path ==
  // Candidate netlist (also reused as LEG1 in VERIFY).
  let ccells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell
  let cvals:  *i64 = sys_mmap(64 * 8) as *i64
  let cgs:    *NxGsim = sys_mmap(64) as *NxGsim
  let cvar_net: *i64 = sys_mmap(8 * 8) as *i64
  var vi: i64 = 0; while vi < 8 { cvar_net[vi] = 0 - 1; vi = vi + 1 }
  if nx_superopt_lower_to_gsim(cand_out, cand_count, ccells, cvals, cgs, cvar_net, 8) != NX_SUPEROPT_OK { sys_exit(16); return 16 }
  let cdepth: *i64 = sys_mmap(64 * 8) as *i64
  let cand_lat: i64 = nx_lat_honest(cgs, cdepth, SO_W)
115
  // Seed netlist (Tier-2 score of the seed).
  let scells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell
  let svals:  *i64 = sys_mmap(64 * 8) as *i64
  let sgs:    *NxGsim = sys_mmap(64) as *NxGsim
  let svar_net: *i64 = sys_mmap(8 * 8) as *i64
  var si: i64 = 0; while si < 8 { svar_net[si] = 0 - 1; si = si + 1 }
  if nx_superopt_lower_to_gsim(seed_out, seed_count, scells, svals, sgs, svar_net, 8) != NX_SUPEROPT_OK { sys_exit(17); return 17 }
  let sdepth: *i64 = sys_mmap(64 * 8) as *i64
  let seed_lat: i64 = nx_lat_honest(sgs, sdepth, SO_W)
125
  // ===== VERIFY: triangulate candidate==seed over dense + random + edge ======
  let env: *i64 = sys_mmap(8 * 8) as *i64
  let cval_buf: *i64 = sys_mmap(64 * 8) as *i64   // emit-interp scratch (candidate)
  let sval_buf: *i64 = sys_mmap(64 * 8) as *i64   // emit-interp scratch (seed/oracle)
  let legs: *i64 = sys_mmap(8 * 8) as *i64
  let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict
  let t: *NxTriTally = sys_mmap(64) as *NxTriTally
  nx_tri_tally_init(t)
134
  // Bundle the verify context once (avoids the 16-arg call cap; clean 3-arg judge).
  let ctx: *NxSoCtx = sys_mmap(256) as *NxSoCtx
  ctx.cand_out = cand_out; ctx.cand_n = cand_count; ctx.cand_root = cand_root
  ctx.seed_out = seed_out; ctx.seed_n = seed_count; ctx.seed_root = seed_root
  ctx.gs = cgs; ctx.var_net = cvar_net; ctx.n_var = 1
  ctx.cval = 8
  ctx.env = env; ctx.cbuf = cval_buf; ctx.sbuf = sval_buf
  ctx.legs = legs; ctx.v = v; ctx.t = t
143
  var vec: i64 = 0
145
  // -- DENSE / EXHAUSTIVE at small width: every x in [-256, 256] (513 vectors).
  //    A complete proof over this bounded domain.
  var dx: i64 = 0 - 256
  while dx <= 256 {
      nx_superopt_judge(ctx, dx, vec)
      vec = vec + 1
      dx = dx + 1
  }
154
  // -- RANDOM: 64 LCG-seeded full-magnitude i64 vectors (interior coverage).
  var seed_lcg: i64 = 88172645463325252
  var ri: i64 = 0
  while ri < 64 {
      seed_lcg = seed_lcg * 6364136223846793005 + 1442695040888963407
      nx_superopt_judge(ctx, seed_lcg, vec)
      vec = vec + 1
      ri = ri + 1
  }
164
  // -- EDGE: 0,1,-1, INT_MIN, INT_MAX, large powers of two, sign-flip pairs --
  //    the values that break naive identities (overflow at MIN, shift-of-neg).
  let imin: i64 = 0 - 9223372036854775807 - 1
  let imax: i64 = 9223372036854775807
  let edges: *i64 = sys_mmap(8 * 8) as *i64
  edges[0] = 0
  edges[1] = 1
  edges[2] = 0 - 1
  let p60: i64 = 1 << 60
  var ei: i64 = 0
  while ei < 4 { nx_superopt_judge(ctx, edges[ei], vec); vec = vec + 1; ei = ei + 1 }
  nx_superopt_judge(ctx, imin, vec); vec = vec + 1
  nx_superopt_judge(ctx, imax, vec); vec = vec + 1
  nx_superopt_judge(ctx, p60, vec); vec = vec + 1
  nx_superopt_judge(ctx, 0 - p60, vec); vec = vec + 1
180
  let bpass: i64 = t.passed
  let btotal: i64 = t.total
183
  // ===== NEGATIVE CONTROL: the verifier MUST CATCH a non-equivalent candidate.
  // Hand-build a WRONG candidate (shl x 2) = x*4 != x*8. Run the SAME battery
  // legs against the SAME seed oracle: leg0 (emit-interp of (shl x 2)) and leg1
  // (its gate-sim) compute x*4, while the oracle + leg2 compute x*8 -- so for
  // any x != 0 the harness must report pass=0 with first_bad=0. A verifier that
  // cannot fail a planted bad rule is not a verifier.
  let wrong_out: *NxEmitNode = sys_mmap(64 * 40) as *NxEmitNode
  wrong_out[0].op = NX_EQ_OP_VAR;   wrong_out[0].payload = 0; wrong_out[0].c0 = 0 - 1; wrong_out[0].c1 = 0 - 1; wrong_out[0].c2 = 0 - 1
  wrong_out[1].op = NX_EQ_OP_CONST; wrong_out[1].payload = 2; wrong_out[1].c0 = 0 - 1; wrong_out[1].c1 = 0 - 1; wrong_out[1].c2 = 0 - 1
  wrong_out[2].op = NX_EQ_OP_SHL;   wrong_out[2].payload = 0; wrong_out[2].c0 = 0;     wrong_out[2].c1 = 1;     wrong_out[2].c2 = 0 - 1
  let wrong_n: i64 = 3
  let wrong_root: i64 = 2
  let wcells: *NxGsimCell = sys_mmap(64 * 48) as *NxGsimCell
  let wvals:  *i64 = sys_mmap(64 * 8) as *i64
  let wgs:    *NxGsim = sys_mmap(64) as *NxGsim
  let wvar_net: *i64 = sys_mmap(8 * 8) as *i64
  var wi: i64 = 0; while wi < 8 { wvar_net[wi] = 0 - 1; wi = wi + 1 }
  if nx_superopt_lower_to_gsim(wrong_out, wrong_n, wcells, wvals, wgs, wvar_net, 8) != NX_SUPEROPT_OK { sys_exit(18); return 18 }
202
  let wval_buf: *i64 = sys_mmap(64 * 8) as *i64
  let wt: *NxTriTally = sys_mmap(64) as *NxTriTally
  nx_tri_tally_init(wt)
  var neg_first_bad_leg: i64 = 0 - 7
  var wvec: i64 = 0
  var wx: i64 = 1
  while wx <= 64 {
      env[0] = wx
      let woracle: i64 = nx_superopt_eval_emit(seed_out, seed_count, seed_root, env, sval_buf)
      legs[0] = nx_superopt_eval_emit(wrong_out, wrong_n, wrong_root, env, wval_buf)  // x*4
      legs[1] = nx_superopt_gsim_eval(wgs, wvar_net, 1, env, wrong_root)              // x*4
      legs[2] = nx_superopt_mul_shiftadd(wx, 8)                                       // x*8 (true)
      nx_tri_pass_strict(legs, 3, woracle, 3, v)
      if wvec == 0 { neg_first_bad_leg = v.first_bad }   // record which leg diverged first
      nx_tri_tally_add(wt, v, wvec)
      wvec = wvec + 1
      wx = wx + 1
  }
  // The wrong candidate is REJECTED iff NOT all vectors passed.
  var neg_rejected: i64 = 0
  if wt.passed != wt.total { neg_rejected = 1 }
224
  _emit_num(found_or(bpass, btotal, cand_cost, seed_cost))
  _emit_num(seed_cost); _emit_num(cand_cost)
  _emit_num(seed_lat); _emit_num(cand_lat)
  _emit_num(cand_root_op); _emit_num(cand_count)
  _emit_num(bpass); _emit_num(btotal)
  _emit_num(neg_rejected); _emit_num(neg_first_bad_leg)
  _nl()
232
  // ===== FAIL-LOUD known-answer assertions ==================================
  // (1) loop FOUND a cheaper equivalent: emitted exactly (shl x 3).
  if cand_count != 3        { sys_exit(1); return 1 }
  if cand_root_op != NX_EQ_OP_SHL { sys_exit(2); return 2 }
  if cand_out[cand_out[cand_root].c1].payload != 3 { sys_exit(3); return 3 }   // shift amount = 3
  if cand_out[cand_out[cand_root].c0].op != NX_EQ_OP_VAR { sys_exit(4); return 4 }
  if sat != NX_EQSAT_SATURATED { sys_exit(5); return 5 }     // idempotent rule converged
  // (2) candidate is TRIANGULATED-EQUIVALENT to the seed over the whole battery.
  if btotal != 585         { sys_exit(6); return 6 }         // 513 dense + 64 random + 4 edge-arr + 4 edge-scalar = 585
  if bpass != btotal       { sys_exit(7); return 7 }         // every vector triangulated-equivalent
  // (2b) the verifier CATCHES a non-equivalent candidate (the negative control).
  if neg_rejected != 1     { sys_exit(8); return 8 }         // wrong (shl x 2) WAS rejected
  if neg_first_bad_leg != 0 { sys_exit(9); return 9 }        // leg 0 (emit-interp) first diverged
  // (3) cost STRICTLY decreased on the honest metric -- twice independently.
  if seed_cost != 3        { sys_exit(20); return 20 }       // Tier-1 seed op-cost = MUL(3)
  if cand_cost != 1        { sys_exit(21); return 21 }       // Tier-1 candidate op-cost = SHL(1)
  if cand_cost >= seed_cost { sys_exit(22); return 22 }      // Tier-1 strict decrease
  if seed_lat != 12        { sys_exit(23); return 23 }       // Tier-2 MUL = 2*log2(64) = 12
  if cand_lat != 6         { sys_exit(24); return 24 }       // Tier-2 SHL = log2(64) = 6
  if cand_lat >= seed_lat  { sys_exit(25); return 25 }       // Tier-2 strict decrease
  sys_exit(0); return 0
254}
nx_superopt_test.nx source

`nx_superopt_test.nx` source
