nx_opt_eqsat_wire_gate.nx source
↩ module page · 140 lines · 6789 B
1// nx_opt_eqsat_wire_gate.nx -- GATE for LN8 "equality saturation CONSUMED by the backend"
2// (lang.plan rung LN8, symbol opt_eqsat_pass). nx_opt_eqsat_pass_gate proves the PASS on an
3// in-memory IR fixture; THIS gate proves the SHIPPING PIPELINE runs it: the toolchain compiler
4// (argv[1], default the live builder) is driven over runtime/nx_eqsat_wire_probe.nx with --ir-dump
5// and the post-opt IR is read back.
6//
7// Observables (both measured 2026-08-23 on the first wired build, neither assumed):
8// * ewp_xor_self (x ^ x, x a runtime param): the xor folds to the constant 0 through the e-graph
9// and is then dead-code-eliminated, so the dump carries NO `op=12` line whose operands are the
10// SAME value id; the emitted asm goes from `xorq %rcx, %rax` to `movabsq $0, %rax`.
11// * ewp_xor_pair (x ^ y, distinct params): the xor SURVIVES -- exactly one `op=12` line with
12// o0 != o1. This is the anti-vacuity control: a pipeline that deleted every xor would fail it.
13// * Behaviour is unchanged: the probe exits argc+3 with and without the pass (exit 4 unarg'd).
14// A pre-LN8 compiler (no pass in opt_run) fails the fold tooth and keeps both xors; a pre-LN8 compiler
15// without --ir-dump fails the dump-present tooth too -- both are the bite, attributable.
16//
17// Driver = nx_ccgate_lib. Data captures in /tmp/nxeqw/, RUNNABLES under _build/ (NAS /tmp noexec).
18// Usage: nx_opt_eqsat_wire_gate [compiler_elf] (CWD = the tree root, like nx_cc_equiv_gate)
19// license_tier: ORIGINAL No hw writes (Rule 26).
20import "nx_syscalls.nx"
21import "nx_gate_verdict.nx"
22import "nx_ccgate_lib.nx"
23
24// The probe's documented exit code when run with no arguments: argc(1) + 3.
25const EWG_EXPECT_EXIT: i64 = 4
26
27// Count dump lines that are an OP_XOR (op=12) whose two operands are the SAME value id, and lines
28// whose operands DIFFER. Parses the nx_ir_dump line shape `i=N op=N n=N r=N k=N ci=N o0=N o1=N`.
29// Returns via out[0]=same, out[1]=different, out[2]=total xor lines; -1 in out[0] if unreadable.
30func ewg_count_xor(path: *u8, out: *i64) -> i64 {
31 out[0] = 0; out[1] = 0; out[2] = 0
32 let szp: *i64 = sys_mmap(16) as *i64
33 let b: *u8 = sys_read_file(path, szp)
34 if (b as i64) == 0 { out[0] = 0 - 1; return 0 - 1 }
35 let n: i64 = szp[0]
36 var ls: i64 = 0
37 var i: i64 = 0
38 var go: i64 = 1
39 while go == 1 {
40 var at_end: i64 = 0
41 if i >= n { at_end = 1 }
42 var is_nl: i64 = 0
43 if at_end == 0 { if b[i] == (10 as u8) { is_nl = 1 } }
44 if at_end == 1 { is_nl = 1 }
45 if is_nl == 1 {
46 if ccg_mem_has(b, ls, i, "op=12 \x00" as *u8, 6) == 1 {
47 out[2] = out[2] + 1
48 let o0: i64 = ewg_field(b, ls, i, "o0=\x00" as *u8, 3)
49 let o1: i64 = ewg_field(b, ls, i, "o1=\x00" as *u8, 3)
50 if o0 == o1 { out[0] = out[0] + 1 } else { out[1] = out[1] + 1 }
51 }
52 ls = i + 1
53 if at_end == 1 { go = 0 }
54 }
55 i = i + 1
56 }
57 return 0
58}
59
60// Parse the decimal after `key` inside b[lo,hi); -1 if absent. Sign handled (the dump prints -1 for
61// absent operands).
62func ewg_field(b: *u8, lo: i64, hi: i64, key: *u8, kl: i64) -> i64 {
63 var p: i64 = lo
64 var at: i64 = 0 - 1
65 var go: i64 = 1
66 while go == 1 {
67 if p + kl > hi { go = 0 } else {
68 if ccg_mem_has(b, p, p + kl, key, kl) == 1 { at = p + kl; go = 0 } else { p = p + 1 }
69 }
70 }
71 if at < 0 { return 0 - 1 }
72 var neg: i64 = 0
73 if b[at] == (45 as u8) { neg = 1; at = at + 1 }
74 var v: i64 = 0
75 var dg: i64 = 1
76 while dg == 1 {
77 if at >= hi { dg = 0 } else {
78 let c: i64 = b[at] as i64
79 if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); at = at + 1 } else { dg = 0 } } else { dg = 0 }
80 }
81 }
82 if neg == 1 { return 0 - v }
83 return v
84}
85
86func main(argc: i64, argv: *i64) -> i64 {
87 var cc: *u8 = "_offc/nx_cc_sovereign.elf\x00"
88 if argc >= 2 { cc = argv[1] as *u8 }
89 ccg_anchor_root()
90 sys_mkdir("/tmp/nxeqw\x00" as *u8, CCG_MODE_X)
91 let pid: i64 = ccg_pid()
92 let p_s: *u8 = ccg_path("/tmp/nxeqw/w_\x00" as *u8, pid, ".s\x00" as *u8)
93 let p_e: *u8 = ccg_path("/tmp/nxeqw/w_\x00" as *u8, pid, ".err\x00" as *u8)
94 let p_elf: *u8 = ccg_path("_build/nxeqw_w_\x00" as *u8, pid, ".elf\x00" as *u8)
95 let p_asm: *u8 = ccg_path("_build/nxeqw_asm_\x00" as *u8, pid, ".elf\x00" as *u8)
96
97 let ctr: *i64 = gv_ctr()
98 gv_head("=== nx_opt_eqsat_wire_gate -- LN8 eqsat consumed by the pipeline: x^x folds in the shipping compiler, x^y survives, behaviour unchanged ===" as *u8)
99
100 let fix: *u8 = "runtime/nx_eqsat_wire_probe.nx\x00"
101 // ONE flag slot in ccg_build; --ir-dump is the flag, and --no-crash-guard is NOT passed because
102 // the count below keys on operand identity, not on the absolute number of xor lines -- the guard
103 // closure may carry its own xors (distinct operands), which land in the `different` bucket.
104 let bw: i64 = ccg_build(cc, "--ir-dump\x00" as *u8, fix, p_s, p_elf, p_e, p_asm)
105 ccg_val("build_rc" as *u8, bw)
106 var t1: i64 = 0
107 if bw == 0 { t1 = 1 }
108 gv_check("T1 probe-compiles-under-ir-dump (flag accepted, fixture is a normal citizen)" as *u8, t1, ctr)
109
110 // nx_ir_dump header shape: "== IR DUMP <label> nv=N nb=N ni=N" (measured from the emitter, not
111 // its doc comment, which spells the fields long-form).
112 let hdrs: i64 = ccg_file_count_lines_with2(p_e, "== IR DUMP\x00" as *u8, "nv=\x00" as *u8)
113 ccg_val("ir_dump_headers" as *u8, hdrs)
114 var t2: i64 = 0
115 if hdrs > 0 { t2 = 1 }
116 gv_check("T2 ir-dump-present (a compiler without --ir-dump cannot be judged by this gate and must fail here, not pass vacuously)" as *u8, t2, ctr)
117
118 let cnt: *i64 = sys_mmap(32) as *i64
119 ewg_count_xor(p_e, cnt)
120 ccg_val("xor_same_operand_lines" as *u8, cnt[0])
121 ccg_val("xor_distinct_operand_lines" as *u8, cnt[1])
122 ccg_val("xor_lines_total" as *u8, cnt[2])
123 var t3: i64 = 0
124 if cnt[0] == 0 { if hdrs > 0 { t3 = 1 } }
125 gv_check("T3 xor-self-FOLDED (no live OP_XOR with identical operands survives opt -- the LN8 done-rule, const_fold cannot do this)" as *u8, t3, ctr)
126 var t4: i64 = 0
127 if cnt[1] >= 1 { t4 = 1 }
128 gv_check("T4 neg-control-xor-pair-SURVIVES (x ^ y keeps its xor: the pipeline did not delete every xor)" as *u8, t4, ctr)
129
130 var ex: i64 = 0 - 1
131 if bw == 0 { ex = ccg_phase(p_elf, 0 as *u8) }
132 ccg_val("probe_exit" as *u8, ex)
133 var t5: i64 = 0
134 if ex == EWG_EXPECT_EXIT { t5 = 1 }
135 gv_check("T5 behaviour-unchanged (probe exits argc+3 = 4: folding x^x to 0 changed no observable)" as *u8, t5, ctr)
136
137 let rc: i64 = gv_verdict("EQSAT-WIRE-LN8" as *u8, ctr, "eqsat pass live in opt_run" as *u8)
138 sys_exit(rc)
139 return rc
140}