Optimization as Refinement: Proving What a Compiler May Change Codex (AI) | Commissioned review v1 | 2026-10-22 Compiler optimizations transform programs across representations with different notions of values, undefined behavior, memory, and observation. This review connects CompCert, LLVM's intermediate representation, and Alive2 to a concrete question: when is an apparently obvious algebraic rewrite valid? Finite unsigned arithmetic and floating-point cancellation provide executable counterexamples, while a modular strength-reduction identity supplies a positive control. We explain why refinement can be more appropriate than equality of every internal behavior, why undefined behavior cannot be ignored, and why bounded translation validation differs from a compiler-wide proof. The proposed methodology couples semantic preconditions with performance measurements so that a faster program is compared only after its contract is preserved. No production compiler is newly verified or benchmarked in this article. The optimization problem is constrained A compiler is asked to reduce execution cost while preserving the behavior that the language promises. The cost may be latency, code size, energy, or compilation time; the permitted behavior depends on types, arithmetic rules, memory operations, exceptions, and observable interactions. A transformation that improves one objective by changing the contract is a different program, not simply a faster implementation. For example, replacing a calculation with a constant can be correct for mathematical integers, incorrect for modular unsigned integers, and conditionally correct for signed source arithmetic whose overflow is undefined. The surface syntax does not decide the answer. A useful optimization claim therefore includes the semantic preconditions alongside the rewritten expression. These preconditions should be represented in the implementation or proof, not left as an informal assumption about typical inputs. Three approaches to trustworthy transformation Leroy's CompCert work demonstrates a formally verified compiler and explains how semantic preservation supports confidence in compiled critical software. The original LLVM paper describes a common low-level representation and framework for analysis and transformation. Alive2 provides bounded translation validation for LLVM IR, checking specific transformations while controlling resource use. The approaches operate at different scopes. A compiler proof reasons about the transformations covered by its verified pipeline. Translation validation checks a particular before-and-after pair under the validator's modeled semantics and bounds. An intermediate representation makes analyses and transformations expressible but does not make them automatically correct. These distinctions matter when a project claims that using a familiar IR or running a validator has verified its entire toolchain. References: cs-07-1, cs-07-2, cs-07-3 Equality is sometimes the wrong relation A source program can permit multiple behaviors because of unspecified choices or nondeterminism. A compiler may select one permitted behavior without preserving every internal choice. A refinement view therefore asks whether the target introduces behavior that the source forbids, using the appropriate treatment of termination and undefined behavior. The details are language-specific. If the source has undefined behavior, the language may impose no requirement on that execution, but this does not authorize changing well-defined executions elsewhere. A validator must model the relevant distinction rather than treating undefined behavior as an arbitrary ordinary value. Similarly, an internal poison value in an IR is not interchangeable with a fixed integer. A review should state the actual semantic relation and avoid assuming that all values in an optimizer's data structures denote ordinary machine values. References: cs-07-1, cs-07-2 An eight-bit counterexample to a tempting rewrite Take an unsigned b-bit variable x and compare x plus one with x, using modular arithmetic. The comparison is true for every x except the maximum value. At that value, addition wraps to zero, so the comparison is false. Replacing the expression by true is therefore incorrect for unsigned arithmetic. For eight bits, exhaustive enumeration finds exactly one counterexample among 256 inputs: x equal to 255. A random test that rarely reaches the boundary can miss it. For a signed source type with undefined overflow, the corresponding optimization requires a different argument restricted to defined executions. The point is not that constant folding is dangerous in general. It is that the proof obligation follows the type and overflow contract, and a seemingly identical textual expression can belong to different contracts. A positive control in modular arithmetic For unsigned b-bit arithmetic, doubling x modulo two raised to b agrees with shifting x left by one and retaining the low b bits in the toy bit-vector model. This identity holds for every bit pattern and gives the test harness a positive control. The appendix enumerates all eight-bit inputs for both the valid and invalid rewrites. A source language may impose additional conditions on a shift, including the allowed shift count and the promoted operand type. The local model fixes the count at one and defines the operation directly on b-bit vectors. Extending its result to source C or C++ requires checking those language details. This explicit restriction is preferable to presenting a bit-vector identity as a universal source-level rewrite. Floating-point arithmetic preserves different information Let a be a large positive floating-point value. In exact arithmetic, the expressions a plus negative a, then plus one, and a plus the quantity negative a plus one are equal. In binary64 arithmetic with round-to-nearest behavior, the first expression evaluates to one, while the second can evaluate to zero when one is lost in rounding the intermediate negative a plus one. The numerical example uses powers of ten and records both evaluation orders. At a equal to ten raised to sixteen, the difference is visible on the declared binary64 model. This is a constructed arithmetic witness, not a benchmark of an optimizer. It explains why reassociation under relaxed floating-point options changes the accepted numerical contract. Such a trade-off can be appropriate, but it must be evaluated against error tolerances and downstream scientific use. Numerical error is an application-level quantity A small local difference can be irrelevant in one application and decisive in another. A threshold test, iterative solver, or ill-conditioned expression can amplify rounding changes. Conversely, a transformation can improve both speed and numerical accuracy by avoiding cancellation. There is no general rule that preserving the original evaluation order always produces the best approximation to the mathematical problem. The correct evaluation compares the transformed program with a declared reference and an error criterion appropriate to the task. Absolute and relative error answer different questions near zero. Reproducibility may require deterministic ordering even when another ordering is more accurate. A compiler study should therefore distinguish semantic permission, numerical quality, and repeatability. A relaxed language option permits certain changes; it does not establish that those changes are acceptable for a particular scientific claim. Translation validation needs an honest status A validator can prove a specific transformation under modeled assumptions, find a counterexample, time out, or encounter an unsupported feature. These outcomes should not be collapsed into a single pass-or-skip count. A timeout is an absence of a result, not evidence that the transformation is safe. Bounded techniques also need their bounds stated. A result about a loop unrolled to a fixed depth does not by itself prove all iteration counts. Conversely, an unbounded local algebraic check can be useful even within a tool that bounds other constructs. The review should identify which obligations were discharged and which were deferred. Alive2's bounded translation-validation framing is valuable precisely because it names this scope rather than claiming a blanket proof of every possible LLVM compilation. References: cs-07-2 Performance comparison begins after correctness Once a rewrite satisfies its semantic preconditions, its cost still depends on the target and surrounding code. Replacing one instruction with another may change dependency depth, vectorization, register pressure, or code layout. A microbenchmark that isolates the instruction can therefore disagree with an application benchmark. A proposed study should preserve the same input domain and correctness oracle across variants, inspect generated code, and use a workload that represents the intended use. Compiler flags and undefined-behavior assumptions must be held constant or explicitly treated as experimental factors. If one variant assumes restricted inputs while the other handles all inputs, the comparison should include the cost of enforcing that restriction. Otherwise the reported speedup partly measures a change in responsibility. A reviewable artifact for each transformation For every proposed optimization, retain the source and target expressions, the type and memory model, preconditions, the refinement relation, and the validation result. Add at least one boundary test and one known-invalid neighboring rewrite so that the harness can demonstrate sensitivity. For numerical transformations, retain the reference calculation and error metric. The local appendix implements this pattern for a valid modular doubling identity, an invalid unsigned comparison rewrite, and a floating-point reassociation witness. These examples are intentionally small enough to inspect completely. They are not substitutes for the full semantics of a real IR, but they show the level of specificity needed before a performance claim becomes meaningful. A reviewer can see exactly which assumption changes the answer. Conclusion: semantics are part of the optimization The scientific value of an optimization is the combination of a preserved contract and a measured improvement under a declared workload. Removing the contract from the report leaves a performance number whose meaning is uncertain. Removing the workload leaves a correct transformation whose practical benefit is unknown. The unsigned and floating-point witnesses show why familiar algebra is not sufficient across machine representations. The positive control shows that precise representation-level reasoning can still justify useful transformations. Compiler-wide proofs and translation validation contribute different forms of assurance; a rigorous account presents their scope, unsupported cases, and artifact relationship alongside the resulting code. Executed finite checks Exhaustive 8-bit rewrite and binary64 counterexample 258 assertions passed. Declared arithmetic expressions; no compiler binary or source-language undefined-behavior model. { "bad_inputs": [ 255 ], "float_results": [ 1.0, 0.0 ] } Code: analysis/examples.py; results: analysis/example-results.json Equations (1) (x+1)\bmod 2^b>x\quad\Longleftrightarrow\quad x<2^b-1 Unsigned bit-vector comparison for 0 <= x < 2^b; replacing it by true fails at the maximum value. (2) (2x)\bmod 2^b=(x\ll1)\bmod 2^b A fixed-count bit-vector identity. Source-language promotions and shift rules require separate checking. (3) \operatorname{fl}(\operatorname{fl}(a-a)+1)\ne\operatorname{fl}(a+\operatorname{fl}(-a+1)) A binary64 round-to-nearest witness occurs at a = 10^16; the left value is 1 and the right value is 0. (4) \operatorname{Beh}(T)\subseteq\operatorname{Beh}(S) Schematic target-to-source refinement, with language-specific handling of undefined behavior, observables, and termination. Analytical figures Figure 1. One boundary value defeats an optimization Unsigned 8-bit modular arithmetic. At x = 255 the increment wraps to zero, so replacing (x + 1 > x) by true is invalid under these semantics. figures/compiler-refinement-1.csv Figure 2. Evaluation order changes floating-point results IEEE-style binary64 calculations in the supplied NumPy environment. These constructed expressions are not a benchmark of LLVM or CompCert. figures/compiler-refinement-2.csv Comparison Method | Unit of assurance | Limit Verified compilation | Covered compiler pipeline and semantics | Unverified components outside the theorem Translation validation | A specific source/target pair | Bounds, unsupported constructs, solver outcomes Exhaustive bit-vector test | Every input of a fixed finite model | Different widths or source semantics Numerical benchmark | Error and cost on declared inputs | Unseen distributions and changed contracts Proposed validation protocol 1. Record the arithmetic type, overflow behavior, and observable effects. 2. Check valid and deliberately invalid rewrites on the same finite domain. 3. Preserve counterexamples as regression fixtures. 4. Treat validator timeout and unsupported cases as unresolved outcomes. 5. Measure numerical error against a stated reference before accepting reassociation. 6. Benchmark equivalent contracts with compiler versions, flags, generated code, and workload recorded. Limitations 1. The bit-vector checks cover eight-bit toy expressions rather than an installed compiler. 2. The floating-point figure assumes binary64 behavior and is not an empirical compiler comparison. 3. The review does not exhaust current LLVM semantics or every CompCert/Alive2 feature. 4. No claim is made that a finite test proves a transformation for all types, languages, or widths. Research questions 1. Which precondition makes the optimization valid, and where is that precondition enforced? 2. Does a relaxed numerical contract preserve the application-level scientific conclusion? 3. Which parts of the compilation and linking path remain outside the validation result? Source evidence cs-07-1: CompCert demonstrates semantic-preservation reasoning for a realistic verified compiler. Boundary: The guarantee follows the verified pipeline and stated source/target semantics. Locator: Abstract and semantic-preservation discussion. cs-07-2: Alive2 checks LLVM transformations through bounded translation validation. Boundary: Bounds, unsupported cases, and inconclusive solver results remain relevant. Locator: Abstract and validation scope. cs-07-3: LLVM provides a shared low-level representation and framework for analysis and transformation. Boundary: An IR's existence is not a proof that each transformation is correct. Locator: Abstract and representation design. References cs-07-1. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM (2009). https://xavierleroy.org/publi/compcert-CACM.pdf | DOI: 10.1145/1538788.1538814 cs-07-2. Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr. Alive2: bounded translation validation for LLVM. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (2021). https://web.ist.utl.pt/nuno.lopes/pubs/alive2-pldi21.pdf | DOI: 10.1145/3453483.3454030 cs-07-3. C. Lattner, V. Adve. LLVM: a compilation framework for lifelong program analysis & transformation. International Symposium on Code Generation and Optimization, 2004. CGO 2004. (2004). https://llvm.org/pubs/2004-01-30-CGO-LLVM.html | DOI: 10.1109/cgo.2004.1281665 cs-07-1 access: Primary record, abstract and selected accessible text; not an exhaustive full-text or supplementary-material audit. cs-07-2 access: Primary record, abstract and selected accessible text; not an exhaustive full-text or supplementary-material audit. cs-07-3 access: Primary record, abstract and selected accessible text; not an exhaustive full-text or supplementary-material audit. Provenance A focused analytical review of three selected foundational primary sources, with original worked examples. This is not an exhaustive or systematic survey of the literature through 2026. Source access and version notes are recorded with the bibliography. Written and technically self-reviewed by Codex (AI). References identify the original researchers; the analytical constructions and proposed evaluation designs are attributed to this article. Covers are conceptual ImageGen illustrations. Technical figures are computed from declared models or finite examples, with Python and CSV supplied. They are not measurements of deployed products or reproduced performance benchmarks. This local draft has no independent peer-review or journal-acceptance record. Bounded executable examples check the stated small models; they are not formal verification of the cited systems.