一句话：提出 Skia 2D 图形库的形式语义 μSkia，并在 Lean 中机械化，用于验证并优化 Chrome 生成的光栅化指令。
光栅化决定应用所绘像素颜色。Skia 等库虽高度优化，应用仍会提交低效指令序列，连 Chrome 在 Top 100 网站上也如此；根源是语义复杂、执行模型不透明。本文提出 μSkia：Skia 2D 图形库的形式语义，并在 Lean 中机械化，覆盖画布状态、层栈、混合与颜色滤镜，分三层以分离关注点、便于扩展。作者归纳 Chrome 生成的四种次优模式及替换，用 μSkia 验证其正确性及微妙条件，并实现高性能优化器。在 Top 100 网站的 139 个程序上，优化器比 Skia 最新 GPU 后端加速 1.12×，优化仅需 0.03 ms，且跨网站、后端与 GPU 保持；优化轨迹被载入 μSkia 并在 Lean 中验证翻译，实现端到端验证。
Rasterization is the process of determining the color of every pixel drawn by an application. Powerful rasterization libraries like Skia, CoreGraphics, and Direct2D put exceptional effort into drawing, blending, and rendering efficiently. Yet applications are still hindered by the inefficient sequences of instructions that they ask these libraries to perform. Even Google Chrome, a highly optimized web browser co-developed with the Skia rasterization library, still produces inefficient instruction sequences even on the top 100 most visited websites. The underlying reason for this inefficiency is that rasterization libraries have complex semantics and opaque and non-obvious execution models. To address this issue, we introduce μSkia, a formal semantics for the Skia 2D graphics library, and mechanize this semantics in Lean. μSkia covers language and graphics features like canvas state, the layer stack, blending, and color filters, and the semantics itself is split into three strata to separate concerns and enable extensibility. We then identify four patterns of sub-optimal Skia code produced by Google Chrome, and then write replacements for each pattern. μSkia allows us to verify that the replacements are correct, including identifying numerous tricky side conditions. We then develop a high-performance Skia optimizer that applies these patterns to speed up rasterization. On 139 Skia programs gathered from the top 100 websites, this optimizer yields a speedup of 1.12× over Skia's most modern GPU backend, while taking just 0.03 ms for optimization. The speedups persist across a variety of websites, Skia backends, and GPUs. To provide true, end-to-end verification, optimization traces produced by the optimizer are loaded back into the μSkia semantics and translation validated in Lean.
@article{paperbot12087,
title = {Semantics for 2D Rasterization},
author = {Bhargav Kulkarni and Henry Whiting and Pavel Panchekha},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839471}
}