code wiki / _hdl_build / nx_eqsat_dsl_bench.nx

nx_eqsat_dsl_bench.nx source

↩ module page · 139 lines · 7333 B

1// nx_eqsat_dsl_bench.nx -- RULE-HEAVY race: the sovereign NishiLang DSL e-matcher 2// vs egg 0.11 (race_egg/examples/nx_dsl_bench.rs), SAME expression, SAME 4 rules, 3// engine-only (build->saturate->recompute_best->extract->read-root), honest us/op. 4// 5// The DSL e-matcher (nx_eqsat_apply_dsl_table over a DATA table) drives saturation 6// -- the same general matcher proven byte-equivalent to the inline rules and proven 7// to apply the new (xor x x)==0 data rule. Here it runs the 4-rule subset that egg 8// races (add_zero, sub_self, mul_one, mul_pow2) so the e-matching work is 1:1. 9// 10// Rule-heavy expression (touches 4 rules in ONE graph): 11// (+ (* (- y y) 1) (* x 8)) 12// (- y y) -> 0 (sub_self) 13// (* 0 1) -> 0 (mul_one) 14// (+ 0 (* x 8)) -> (* x 8) (add_zero) 15// (* x 8) -> (<< x 3) (mul_pow2) best extracted = (<< x 3) 16// 17// FAIL LOUD: if the extracted root is not SHL the harness sys_exit(nonzero) BEFORE 18// timing -- a fast wrong answer is not a win. Same honesty discipline as the 19// existing nx_eqsat_race_bench.nx (egg's exact pipeline, no proxy, no proof 20// machinery in the timed loop -- egg has none). 21// 22// Output (one line): NX_DSL_BENCH iters=100000 total_us=<t> us_per_op_ns=<u> 23 24import "nx_eqsat.nx" 25const K_MAGIC_100000: i64 = 100000 26 27func _emit_num(v: i64) -> i64 { 28 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 29 let t2: *u8 = sys_mmap(28); var t: i64 = 0 30 if n == 0 { t2[0] = 48; t = 1 } 31 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 32 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 33 b[t] = 32; sys_write(1, b, t + 1); return 0 34} 35func _emit_str(s: *u8, len: i64) -> i64 { sys_write(1, s, len); return 0 } 36func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 37 38// Fill the 4-rule subset matching egg's race set (rows in saturate apply order). 39func _fill_4rule_table(table: *NxDslRule) -> i64 { 40 // add_zero: (add x 0)==x (dual_order) 41 nx_eqsat_dsl_set_row(table, 0, NX_EQSAT_RULE_ADD_ZERO, NX_EQ_OP_ADD, 42 DSL_VAR, 0, DSL_CONST, 0, RHS_BIND_A, 0, SC_NONE, CNT_EVERY, 1) 43 // sub_self: (sub x x)==0 44 nx_eqsat_dsl_set_row(table, 1, NX_EQSAT_RULE_SUB_SELF, NX_EQ_OP_SUB, 45 DSL_VAR, 0, DSL_SAME_AS_A, 0, RHS_CONST, 0, SC_NONE, CNT_EVERY, 0) 46 // mul_one: (mul x 1)==x (right-const only) 47 nx_eqsat_dsl_set_row(table, 2, NX_EQSAT_RULE_MUL_ONE, NX_EQ_OP_MUL, 48 DSL_VAR, 0, DSL_CONST, 1, RHS_BIND_A, 0, SC_NONE, CNT_EVERY, 0) 49 // mul_pow2: (mul x 2^k)==(shl x k) for k<W (dual_order, real-merge counting) 50 nx_eqsat_dsl_set_row(table, 3, NX_EQSAT_RULE_MUL_POW2, NX_EQ_OP_MUL, 51 DSL_VAR, 0, DSL_CONST, 0, RHS_SHL_A_BY_LOG2B, 0, 52 SC_POW2_B_KLTW, CNT_REAL_MERGE, 1) 53 return 4 54} 55 56// ONE full optimize-and-read iteration via the DSL e-matcher on a fresh e-graph. 57// Builds (+ (* (- y y) 1) (* x 8)); returns the extracted root op of the top ADD 58// class; writes the shift const to shift_out[0] when SHL. Scratch is reused (the 59// e-graph is fully re-init'd each call) so per-iter mmap churn is not charged. 60func _one_iter(eg: *NxEGraph, table: *NxDslRule, 61 nodes: *NxENode, cap_nodes: i64, 62 classes: *NxEClass, cap_cls: i64, 63 shift_out: *i64) -> i64 { 64 if nx_eqsat_init(eg, nodes, cap_nodes, classes, cap_cls) != NX_EQSAT_OK { return 0 - 100 } 65 if nx_eqsat_enable_dsl(eg, table, 4, 8) != NX_EQSAT_OK { return 0 - 105 } 66 // BUILD (+ (* (- y y) 1) (* x 8)) -- egg's parse analogue. 67 let y: i64 = nx_eqsat_add_var(eg, 1) 68 let suby: i64 = nx_eqsat_add_binary(eg, NX_EQ_OP_SUB, y, y) // (- y y) 69 let one: i64 = nx_eqsat_add_const(eg, 1) 70 let m1: i64 = nx_eqsat_add_binary(eg, NX_EQ_OP_MUL, suby, one) // (* (- y y) 1) 71 let x: i64 = nx_eqsat_add_var(eg, 0) 72 let c8: i64 = nx_eqsat_add_const(eg, 8) 73 let m8: i64 = nx_eqsat_add_binary(eg, NX_EQ_OP_MUL, x, c8) // (* x 8) 74 let top: i64 = nx_eqsat_add_binary(eg, NX_EQ_OP_ADD, m1, m8) // (+ ... ...) 75 if top < 0 { return 0 - 101 } 76 // SATURATE via the DSL e-matcher (egg's Runner::run). The equivalence closure 77 // is reached within a few iterations; the CNT_EVERY identity rules (add_zero/ 78 // sub_self/mul_one, byte-identical to inline) keep re-counting matches so the 79 // loop returns STEP_BUDGET rather than SATURATED -- exactly as egg's Runner 80 // stops at its iteration limit. Either return code is fine; the FAIL-LOUD 81 // correctness gate (extracted root == SHL/3) is the real verdict. 82 nx_eqsat_saturate(eg, 16) 83 // EXTRACT (egg's bottom-up cost pass + find_best). 84 if nx_eqsat_recompute_best(eg) != NX_EQSAT_OK { return 0 - 103 } 85 let best: i64 = nx_eqsat_extract_best_node(eg, top) 86 if best < 0 { return 0 - 104 } 87 let root_op: i64 = eg.nodes[best].op 88 if root_op == NX_EQ_OP_SHL { 89 let kid1: i64 = eg.nodes[best].kid1 90 let kcanon: i64 = nx_eqsat_find(eg, kid1) 91 let knode: i64 = eg.classes[kcanon].best_node 92 shift_out[0] = eg.nodes[knode].payload 93 } 94 return root_op 95} 96 97func main() -> i64 { 98 let cap_nodes: i64 = 64 99 let cap_cls: i64 = 64 100 let nodes: *NxENode = sys_mmap(cap_nodes * 64) as *NxENode 101 let classes: *NxEClass = sys_mmap(cap_cls * 32) as *NxEClass 102 let eg: *NxEGraph = sys_mmap(256) as *NxEGraph 103 let shift_out: *i64 = sys_mmap(8) as *i64 104 let table: *NxDslRule = sys_mmap(8 * 96) as *NxDslRule 105 _fill_4rule_table(table) 106 107 // CORRECTNESS GATE (FAIL LOUD, before timing): extracted root MUST be (shl x 3). 108 shift_out[0] = 0 - 1 109 let check_op: i64 = _one_iter(eg, table, nodes, cap_nodes, classes, cap_cls, shift_out) 110 if check_op != NX_EQ_OP_SHL { sys_exit(80); return 80 } 111 if shift_out[0] != 3 { sys_exit(81); return 81 } 112 113 // TIMED LOOP -- 100000 iterations, each independently verified (a mid-run 114 // regression cannot masquerade as a fast time). 115 let iters: i64 = K_MAGIC_100000 116 let t0: i64 = sys_clock_now_us() 117 var k: i64 = 0 118 while k < iters { 119 shift_out[0] = 0 - 1 120 let op: i64 = _one_iter(eg, table, nodes, cap_nodes, classes, cap_cls, shift_out) 121 if op != NX_EQ_OP_SHL { sys_exit(82); return 82 } 122 if shift_out[0] != 3 { sys_exit(83); return 83 } 123 k = k + 1 124 } 125 let t1: i64 = sys_clock_now_us() 126 let total_us: i64 = t1 - t0 127 let us_per_op_ns: i64 = (total_us * 1000) / iters 128 129 let s1: *u8 = sys_mmap(16); s1[0]=78;s1[1]=88;s1[2]=95;s1[3]=68;s1[4]=83;s1[5]=76;s1[6]=95;s1[7]=66;s1[8]=69;s1[9]=78;s1[10]=67;s1[11]=72;s1[12]=32 // "NX_DSL_BENCH " 130 _emit_str(s1, 13) 131 let s2: *u8 = sys_mmap(16); s2[0]=105;s2[1]=116;s2[2]=101;s2[3]=114;s2[4]=115;s2[5]=61 // "iters=" 132 _emit_str(s2, 6); _emit_num(iters) 133 let s3: *u8 = sys_mmap(16); s3[0]=116;s3[1]=111;s3[2]=116;s3[3]=97;s3[4]=108;s3[5]=95;s3[6]=117;s3[7]=115;s3[8]=61 // "total_us=" 134 _emit_str(s3, 9); _emit_num(total_us) 135 let s4: *u8 = sys_mmap(24); s4[0]=117;s4[1]=115;s4[2]=95;s4[3]=112;s4[4]=101;s4[5]=114;s4[6]=95;s4[7]=111;s4[8]=112;s4[9]=95;s4[10]=110;s4[11]=115;s4[12]=61 // "us_per_op_ns=" 136 _emit_str(s4, 13); _emit_num(us_per_op_ns) 137 _nl() 138 sys_exit(0); return 0 139}