一篇论文把编译器先形式化再重写的路子搬到 2D 光栅化。它给 Skia 的命令语言建了套能在定理证明器里推理的语义，机械化物 453 行，借此证明几组等价但更快的指令序列，再对命令缓冲做单趟重写。99 个真实站点截图上几何平均提速 18.7%，被改写的 35 个全部提速，幅度 1.035 到 3.584 倍。图形调优和浏览器渲染流水线的人值得读，尤其手里拿得到客户端指令 dump、怀疑指令空烧 GPU 的场合。
库已经够快了为什么还要改调用它的那串指令
Skia 的贡献者名单上有 109 人，每 4 周切一个稳定版本。2021 到 2025 年团队写了新后端 Graphite，目标是光栅化时间改善约 15%。库这一侧卷到这份上。
瓶颈挪到了上游。Chrome 与 Skia 同公司同步开发，照样吐出一串低效命令，多余的合成图层，为绕开 API 差异硬加的转换层，都在里面。库的语义复杂，执行模型不透明，怎么写等价但更省的指令，没人能保证不出错。
论文划了条界。Halide 管单条绘图与混合指令的实现和调度，这套语义只管命令语言本身。搬过来的是验证加重写的方法学，常量折叠、公共子表达式消除这类经典手段文中一个都没有。
怎么证明两串指令画出来一样
语义分三层。底层是抽象模型，Image 把 Point 映到 Color，Shape 把 Point 映到 Bool，另有 Blend 与 Filter。中层是 Layer 项，Empty、DrawShape、BlendLayer 三个构造子，各挂一个 Paint，里面放填充 Image、Filter、Blend。顶层是命令语言，Draw、Clip、Save 与 SaveLayer 配 Restore、顺序组合，执行状态为一句一栈加一层一栈。
语义用 Lean 4 机械化，453 行。实例化里 Point 是实数二元组，Color 是带预乘 alpha 的实数四元组。实数把抗锯齿和舍入整个假设掉了，所以等价只是抗锯齿与舍入之外的等价。论文与 Skia 工程团队确认过这个取舍可以接受，Skia 本来也不保证抗锯齿行为。
一层合成图层贵在哪
SaveLayer 要单独分配一层，再跑一次混合，省掉它是收益最直接的一刀。四条规则各有硬前提。
- 规则一换成不开图层，条件写在层里的每条 Draw 都用 SrcOver 混合，层内不含 SaveLayer，Lean 版还要求填充色不透明，依据是 SrcOver 可结合。
- 规则二把 saveLayer 配 DstIn 做矩形掩码换成裁剪加直接画图，Skia 对矩形与圆角矩形裁剪有快速路径，前提是内层无 SaveLayer、只含裁剪操作、颜色滤波后不透明。
- 规则三删掉 Chrome 为 SVG 掩码补的亮度转换层，改成直接算掩码填充色的亮度，无条件成立，可内层有多条 Draw 时不成立，亮度与混合不可交换。
- 规则四删多余渐变掩码，条件是渐变每个色标都不透明，它来自某些站点共用的框架，论文脚注提到这几个站 2026 年 1 月合计月访问量略超 50 亿。
四条规则单看都平凡。论文的说法是，写合法的替换模式试了很多次，关键前提全靠语义挖出来。
32 微秒换 18.7% 这笔账怎么算
优化器挂在客户端 flush 前。Skia 把命令记进 SkRecord，缓冲由指针数组加一块 arena 组成。改写就在 arena 新建对象再改指针，删除命令改成 NoOp，新命令先进 insertion buffer，pass 结束后一趟线性扫描合并，这技巧借自 WebKit 的 B3。
每条规则是一个单趟 pass，共用一套回调接口。模式匹配用有限状态机，SaveLayer 深度交给 Frame 栈，栈放在 Skia 的 STArray 里，前 8 个元素栈上分配，Chrome 程序的层深都很浅。
账面数字。99 个 benchmark 几何平均 18.7%，35 个被改写的全部提速，另 32 个变慢却都没被优化过，判为噪声，未优化者区间只有 1.000 到 1.410。优化时间随命令数线性增长，全部低于 32 微秒，加回光栅化时间后多数仍提速，最大 3.561 倍。旧 Ganesh 加 OpenGL 得 13.2%，Intel 硬件加 Vulkan 得 16.0%。论文的结论性观察，旧后端跑优化后的程序约等于新后端跑原始程序。
像素对不上怎么确认只是抗锯齿
正确性查两层。一层逐段证明等价，优化器输出每个 pass 之后的 skp 形成轨迹，经 Skia 自带解析器转 JSON 再转成 Lean 项，逐段断言与上一步等价。99 个里 42 个能完整转换，34 个通过，剩 8 个卡在证明搜索超时。
第二层像素比对，优化前后都光栅化成 PNG，统计单通道差异超过 1% 的像素。19 个 benchmark 报出显著差异，逐个看过，全落在曲线形状边缘，正是抗锯齿该出现的地方，肉眼分不出两者渲染结果。
这套办法的边界在哪
覆盖面是第一道坎。mask filters、模糊、image filters、SkSL、位图都没建模，程序沾上它们，转换这关就过不去；新抓的 180 个站点 benchmark 上，删渐变掩码的规则一次都没触发，它本是针对特定框架的点优化。
第二道坎，重写安全换不来性能。那台 Intel 机器上唯一被显著拖慢的是一个设计工具站点的 benchmark，多个 pass 之后吐出复杂裁剪路径，论文建议在旧后端上按路径复杂度关掉对应 pass。
引用数字记住限定，18.7% 出自这批含 SaveLayer 的 Web 截图 benchmark，不是所有渲染场景。论文也没有 Chrome 端到端帧率数据，只测了光栅化时间。