[Optimization] Peephole Optimizations

Reference:
https://blog.regehr.org/archives/2485

Local Peephole Optimization and Compositional Refinement

Let f be a function targeted for peephole optimization. 

We can structurally decompose f into a target redex o (the optimizable instruction sequence) and a continuation context r (the residual program), such that:

f = r ∘ o

By definition, a correct optimization yields a refined sequence o′ that refines the original sequence o, denoted as:

o ⊑ o′

To lift this local optimization to the function level, we rely on the compositionality of the refinement relation. For any valid refinement definition, the context r must act as a monotonic operator:

If x ⊑ y, then r(x) ⊑ r(y)

Applying compositionality to our decomposition:

r(o) ⊑ r(o′)

Because f = r(o), it transitively follows that:

f ⊑ r(o′)

This proves that the locally optimized function refines the original function. By inductively applying this compositionality principle, we can scale this local refinement guarantee across the entire program.