nx_opt_eqsat_oracle_gate.nx source

1// nx_opt_eqsat_oracle_gate.nx -- THE EQUALITY-SATURATION ENGINE USED AS AN ORACLE OVER THE SHIPPING 2// OPTIMIZER. Written 2026-08-14, the day nx_eqsat compiled for the first time. 3// 4// WHY THIS GATE EXISTS. nx_opt.nx's opt_strength_reduce rewrites `x * 2^k` into `x << k` and its 5// comment calls that "always safe". nx_eqsat_rule_proof_test proves the same identity by exhaustive 6// triangulation -- but only for k in [0, W), because at k >= W the identity is FALSE: 2^k mod 2^W is 0, 7// so x*2^k collapses to zero while x<<k is out of range. nx_rule_soundness measured that boundary 8// 2048/2048. So the shipping compiler performs a rewrite whose soundness has a domain, and until now 9// nothing connected the two: the engine knew the boundary and the optimizer never asked. 10// 11// WHAT I FOUND WHEN I CHECKED, STATED PLAINLY: the optimizer is CORRECT. is_pow2 rejects n <= 1, and a 12// POSITIVE i64 constant caps k at 62, because 2^63 does not fit and reads as negative. 62 < 64, so the 13// unsound region is unreachable and there is no miscompile here. I am not manufacturing a finding. 14// 15// WHAT IS ACTUALLY WRONG IS THAT THIS IS TRUE BY ACCIDENT OF THE TYPE, NOT BY AN ASSERTED INVARIANT. 16// Nothing in nx_opt names W, nothing checks the shift it emits against the domain the proof covers, and 17// a wider constant type or an edited is_pow2 would delete the guarantee in silence -- the failure mode 18// being a SILENT WRONG VALUE, the worst class this estate tracks. This gate makes the accident an 19// invariant: it asserts, over the WHOLE domain the optimizer can reach and not a sample of it, that 20// every shift is_pow2 will ever emit falls inside the region the engine proved sound, AND that the 21// engine independently agrees with the optimizer at every one of those k. 22// 23// THIS IS A REAL CONSUMER RELATIONSHIP, AND IT IS NOT THE ONE THE WATCH CONTRACT WANTS. lang_opt_eqsat_pass 24// contracts an opt_eqsat_pass symbol in nx_opt.nx -- eqsat REWRITING the IR. That is not what this is, and 25// I am not naming this function opt_eqsat_pass to make a page turn green. This is the engine constraining 26// a hand-written pass, which is worth having on its own and is the honest thing to claim. 27// BITE-PROVEN 2026-08-14, both directions, on the deployed binary. Raising OEO_MAX_REACHABLE_K from 28// 62 to 63 drove it RED 9/12 with exactly the three domain teeth failing -- recognised, shift-correct, 29// and engine-agrees -- while every negative control and the boundary tooth stayed PASS. That is the 30// non-vacuity proof AND an independent confirmation of the reason stated above: at k=63, 1<<63 does not 31// fit a positive i64, is_pow2 refuses it, and the reachable count drops to 62. The 62 ceiling is now 32// MEASURED rather than argued. Restoring the constant reproduced the pre-bite artifact byte-for-byte 33// (sha 5628f24d, src e6cf8320). 34// 35// AND THE RESTORE ITSELF FOUND SOMETHING. Promoting the restored binary was REFUSED: it is byte-identical 36// to the generation that was live BEFORE the mutant, so the seq1484 backwards-walk guard reads it as an 37// earlier generation and declines, while /api/rollback is edge-only by design. So a mutation experiment 38// that restores perfectly CANNOT re-promote its own restoration -- the very byte-identity that proves the 39// restore correct is what makes it unpromotable. This header note is the forward generation that carries 40// the restored constant back to live. 41// license_tier: ORIGINAL expect_exit: 0 42import "nx_gate_verdict.nx" 43import "nx_eqsat.nx" 44import "nx_opt.nx" 45 46const OEO_CAP_NODES: i64 = 64 47const OEO_CAP_CLS: i64 = 64 48// The largest k reachable from a POSITIVE i64 power-of-two constant: 2^62 fits, 2^63 does not. 49const OEO_MAX_REACHABLE_K: i64 = 62 50 51// Ask the ENGINE, independently of the optimizer: does it merge mul(x, mulc) with shl(x, shamt)? 52func oeo_engine_merges(mulc: i64, shamt: i64) -> i64 { 53 let nodes: *NxENode = sys_mmap(OEO_CAP_NODES * 64) as *NxENode 54 let classes: *NxEClass = sys_mmap(OEO_CAP_CLS * 32) as *NxEClass 55 let g: *NxEGraph = sys_mmap(NX_EQSAT_GRAPH_BYTES) as *NxEGraph 56 if nx_eqsat_init(g, nodes, OEO_CAP_NODES, classes, OEO_CAP_CLS) != NX_EQSAT_OK { return 0 - 1 } 57 let x: i64 = nx_eqsat_add_var(g, 0) 58 let cm: i64 = nx_eqsat_add_const(g, mulc) 59 let cs: i64 = nx_eqsat_add_const(g, shamt) 60 let m: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_MUL, x, cm) 61 let s: i64 = nx_eqsat_add_binary(g, NX_EQ_OP_SHL, x, cs) 62 nx_eqsat_saturate(g, 32) 63 if nx_eqsat_find(g, m) == nx_eqsat_find(g, s) { return 1 } 64 return 0 65} 66 67func main() -> i64 { 68 gv_head("nx_opt x nx_eqsat oracle gate -- every shift the optimizer can emit lies inside the proven-sound domain" as *u8) 69 let ctr: *i64 = gv_ctr() 70 71 let shp: *i64 = sys_mmap(16) as *i64 72 73 // ---- DOMAIN SWEEP: every power of two the optimizer can actually see. NOT A SAMPLE: k runs the 74 // whole reachable range, and the count is asserted below so a shortened loop cannot pass quietly. 75 var recognised: i64 = 0 76 var shift_correct: i64 = 0 77 var max_k: i64 = 0 78 var engine_agrees: i64 = 0 79 var k: i64 = 1 80 while k <= OEO_MAX_REACHABLE_K { 81 let n: i64 = 1 << k 82 *shp = 0 - 1 83 if is_pow2(n, shp) == 1 { 84 recognised = recognised + 1 85 if shp[0] == k { shift_correct = shift_correct + 1 } 86 if shp[0] > max_k { max_k = shp[0] } 87 // THE DIFFERENTIAL STEP: the engine is asked the same question, from its own rule set. 88 if oeo_engine_merges(n, k) == 1 { engine_agrees = engine_agrees + 1 } 89 } 90 k = k + 1 91 } 92 93 gv_check("every reachable power of two is recognised by the optimizer" as *u8, recognised == OEO_MAX_REACHABLE_K, ctr) 94 gv_check("the emitted shift amount equals k at every one of them" as *u8, shift_correct == OEO_MAX_REACHABLE_K, ctr) 95 // THE LOAD-BEARING TOOTH. This is the invariant that was previously true only by accident. 96 gv_check("the LARGEST shift the optimizer can emit is strictly inside the proven-sound domain" as *u8, max_k < NX_EQSAT_W, ctr) 97 // THE DIFFERENTIAL RESULT: two independent implementations, whole domain, no disagreement. 98 gv_check("the equality-saturation engine agrees the rewrite is legal at EVERY reachable k" as *u8, engine_agrees == OEO_MAX_REACHABLE_K, ctr) 99 // BIND THE AGGREGATE TO ITS DENOMINATOR: all four counts above are trivially satisfied by an empty 100 // sweep, so the sweep length itself is a tooth. 101 gv_check("the sweep ran the whole reachable domain and not a prefix of it" as *u8, k == OEO_MAX_REACHABLE_K + 1, ctr) 102 // LOCKSTEP ON THE DECLARED DOMAIN, which is a DIFFERENT question from the measured one above. 103 // max_k reports what the optimizer was OBSERVED to emit; this pins what this gate CLAIMS the 104 // reachable ceiling is against the engine's own operating width. If someone narrows NX_EQSAT_W -- 105 // porting the engine to a 32-bit word, say -- the observed teeth would still pass while every 106 // conclusion drawn here silently stopped being true, because the sound region would have moved 107 // beneath a domain constant that did not. 108 gv_check("the declared reachable ceiling sits strictly below the engine operating width" as *u8, OEO_MAX_REACHABLE_K < NX_EQSAT_W, ctr) 109 110 // ---- NEGATIVE CONTROLS on the optimizer predicate. Without these, an is_pow2 that returned 1 for 111 // every input would score full marks on everything above. 112 *shp = 0 - 1 113 gv_check("neg-control-zero-is-not-a-power-of-two" as *u8, is_pow2(0, shp) == 0, ctr) 114 *shp = 0 - 1 115 gv_check("neg-control-one-is-refused-so-a-zero-shift-is-never-emitted" as *u8, is_pow2(1, shp) == 0, ctr) 116 *shp = 0 - 1 117 gv_check("neg-control-three-is-not-a-power-of-two" as *u8, is_pow2(3, shp) == 0, ctr) 118 *shp = 0 - 1 119 gv_check("neg-control-six-has-a-set-low-bit-and-is-refused" as *u8, is_pow2(6, shp) == 0, ctr) 120 *shp = 0 - 1 121 // A NEGATIVE multiplier is how a 2^63 literal actually presents in an i64, and it is exactly the 122 // input that would reach the unsound region if it were accepted. 123 gv_check("neg-control-a-negative-multiplier-is-refused" as *u8, is_pow2(0 - 8, shp) == 0, ctr) 124 125 // ---- NEGATIVE CONTROLS on the engine side. Without these the differential tooth above would pass 126 // for an engine that merged every pair it was handed. 127 gv_check("neg-control-engine-does-NOT-merge-mul-8-with-shl-4" as *u8, oeo_engine_merges(8, 4) == 0, ctr) 128 gv_check("neg-control-engine-does-NOT-merge-a-non-power-of-two-multiplier" as *u8, oeo_engine_merges(6, 2) == 0, ctr) 129 130 return gv_verdict("nx_opt_eqsat_oracle_gate" as *u8, ctr, 131 "whole-domain differential check: the shipping strength-reduction pass and the proven equality-saturation rule agree at every reachable k, and the largest shift the optimizer can emit is inside the sound region" as *u8) 132}