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}