Compiler-style optimization for drawing via Skia

Rasterization libraries like Skia perform complex drawing, blending, and color processing but expose opaque execution models that lead applications to emit inefficient instruction sequences. μSkia provides a formal, mechanized semantics for Skia’s 2D rasterization model, encoded in Lean. It models concrete features such as canvas state, the layer stack, blending modes, and color filters, and organizes the semantics into three strata to separate concerns and enable extensible reasoning about transformations. The mechanization makes many subtle execution details explicit so that semantic equivalences and side conditions are checkable rather than guessed.

Using μSkia, four common patterns of suboptimal Skia call sequences found in Chrome were identified and correct replacement transforms were written and formally verified, including handling tricky side conditions. Those rewrites were compiled into a high-performance optimizer that rewrites Skia programs at runtime; on 99 Skia programs extracted from the top 100 websites it yields an average 18.7% speedup over Skia’s current GPU backend while incurring at most 32 μs per optimization. The reported speedups generalize across different sites, Skia backends, and GPUs, and every optimization trace is reloaded into μSkia and validated in Lean for end-to-end correctness.