nx_eqsat_wire_probe.nx source
↩ module page · 32 lines · 1735 B
1// nx_eqsat_wire_probe.nx -- LN8 WIRING WITNESS (lang.plan rung LN8, symbol opt_eqsat_pass).
2//
3// The pass itself is proven by nx_opt_eqsat_pass_gate (10/10) on an in-memory IR fixture. THIS file
4// is the witness that the SHIPPING PIPELINE runs it: compiled by the toolchain compiler under
5// --ir-dump, the post-opt IR of ewp_xor_self must carry NO live OP_XOR (op=12) whose result is a
6// non-constant -- the x ^ x instruction folds to the constant 0 through the e-graph, which the
7// incumbent opt_const_fold structurally cannot do (it needs BOTH operands constant). The control
8// ewp_xor_pair (x ^ y, two distinct params) MUST keep its xor. Behaviour is identical either way
9// (the gate runs the binary too: exit code = the same small number with or without the pass).
10//
11// Built with --no-crash-guard inside the gate so the dumped IR is this file plus nx_syscalls only.
12// license_tier: ORIGINAL No hw writes (Rule 26).
13import "nx_syscalls.nx"
14
15// x ^ x with x a RUNTIME parameter: const_fold cannot see it, eqsat folds it to 0.
16func ewp_xor_self(x: i64) -> i64 {
17 return x ^ x
18}
19
20// Control: x ^ y with distinct params -- nothing to fold, the xor MUST survive.
21func ewp_xor_pair(x: i64, y: i64) -> i64 {
22 return x ^ y
23}
24
25func main(argc: i64, argv: *i64) -> i64 {
26 // argc is a runtime value; (argc ^ argc) is 0 whether or not it was folded, so the exit code is
27 // argc + 3 either way (argc is 1 when run with no arguments -> exit 4; 2 with one -> exit 5).
28 let a: i64 = ewp_xor_self(argc)
29 let b: i64 = ewp_xor_pair(argc, argc + 1) // argc ^ (argc+1): low bit flips, a real value
30 if b == 0 { return 99 } // cannot happen: keeps ewp_xor_pair live
31 return a + argc + 3
32}