nx_opt_eqsat_oracle_gate.nx

nx_opt_eqsat_oracle_gate.nx -- THE EQUALITY-SATURATION ENGINE USED AS AN ORACLE OVER THE SHIPPING OPTIMIZER. Written 2026-08-14, the day nx_eqsat compiled for the first time. WHY THIS GATE EXISTS. nx_opt.nx's opt_strength_reduce rewrites `x * 2^k` into `x << k` and its comment calls that "always safe". nx_eqsat_rule_proof_test proves the same identity by exhaustive triangulation -- but only for k in [0, W), because at k >= W the identity is FALSE: 2^k mod 2^W is 0, so x*2^k collapses to zero while x<<k is out of range. nx_rule_soundness measured that boundary 2048/2048. So the shipping compiler performs a rewrite whose soundness has a domain, and until now nothing connected the two: the engine knew the boundary and the optimizer never asked. WHAT I FOUND WHEN I CHECKED, STATED PLAINLY: the optimizer is CORRECT. is_pow2 rejects n <= 1, and a POSITIVE i64 constant caps k at 62, because 2^63 does not fit and reads as negative. 62 < 64, so the unsound region is unreachable and there is no miscompile here. I am not manufacturing a finding. WHAT IS ACTUALLY WRONG IS THAT THIS IS TRUE BY ACCIDENT OF THE TYPE, NOT BY AN ASSERTED INVARIANT. Nothing in nx_opt names W, nothing checks the shift it emits against the domain the proof covers, and a wider constant type or an edited is_pow2 would delete the guarantee in silence -- the failure mode being a SILENT WRONG VALUE, the worst class this estate tracks. This gate makes the accident an invariant: it asserts, over the WHOLE domain the optimizer can reach and not a sample of it, that every shift is_pow2 will ever emit falls inside the region the engine proved sound, AND that the engine independently agrees with the optimizer at every one of those k. THIS IS A REAL CONSUMER RELATIONSHIP, AND IT IS NOT THE ONE THE WATCH CONTRACT WANTS. lang_opt_eqsat_pass contracts an opt_eqsat_pass symbol in nx_opt.nx -- eqsat REWRITING the IR. That is not what this is, and I am not naming this function opt_eqsat_pass to make a page turn green. This is the engine constraining a hand-written pass, which is worth having on its own and is the honest thing to claim. BITE-PROVEN 2026-08-14, both directions, on the deployed binary. Raising OEO_MAX_REACHABLE_K from 62 to 63 drove it RED 9/12 with exactly the three domain teeth failing -- recognised, shift-correct, and engine-agrees -- while every negative control and the boundary tooth stayed PASS. That is the non-vacuity proof AND an independent confirmation of the reason stated above: at k=63, 1<<63 does not fit a positive i64, is_pow2 refuses it, and the reachable count drops to 62. The 62 ceiling is now MEASURED rather than argued. Restoring the constant reproduced the pre-bite artifact byte-for-byte (sha 5628f24d, src e6cf8320). AND THE RESTORE ITSELF FOUND SOMETHING. Promoting the restored binary was REFUSED: it is byte-identical to the generation that was live BEFORE the mutant, so the seq1484 backwards-walk guard reads it as an earlier generation and declines, while /api/rollback is edge-only by design. So a mutation experiment that restores perfectly CANNOT re-promote its own restoration -- the very byte-identity that proves the restore correct is what makes it unpromotable. This header note is the forward generation that carries the restored constant back to live.