[2603.23696] Semantics for 2D Rasterization (https://arxiv.org/static/browse/0.3.4/images/icons/apple-touch-icon.png) (../static/browse/0.3.4/images/icons/favicon-32x32.png) (../static/browse/0.3.4/images/icons/favicon-16x16.png) (../static/browse/0.3.4/images/icons/site.webmanifest) (https://arxiv.org/static/browse/0.3.4/images/icons/safari-pinned-tab.svg) (../static/browse/0.3.4/css/arXiv.css@v=20260318.css)  (../static/browse/0.3.4/css/arXiv-print.css@v=20200611.css)  (../static/browse/0.3.4/css/browse_search.css)  (../static/base/1.0.1/css/arxiv-header-footer.css@v=20260626.css)  (2603.23696.html)                  (../static/browse/0.3.4/css/tooltip.css)  (../../static.arxiv.org/js/bibex-dev/bibex.css@20200709.css)            (2603.23696.html#content) Skip to main content (https://arxiv.org/IgnoreMe)  (https://arxiv.org/) (archive)       (https://arxiv.org/search)    Search  (https://arxiv.org/user/create) Submit (https://info.arxiv.org/about/donate.html) Donate  (https://arxiv.org/login) Log in   Search arXiv (Search papers by title, author, abstract, or ID...) (all) (header)  Press Enter to search · (https://arxiv.org/search/advanced) Advanced search    Computer Science > Programming Languages  arXiv:2603.23696 (cs)  (../static/base/1.0.1/css/abs.css) [Submitted on 24 Mar 2026] Title: Semantics for 2D Rasterization Authors: (https://arxiv.org/search/cs?searchtype=author&query=Kulkarni,+B) Bhargav Kulkarni , (https://arxiv.org/search/cs?searchtype=author&query=Whiting,+H) Henry Whiting , (https://arxiv.org/search/cs?searchtype=author&query=Panchekha,+P) Pavel Panchekha  View a PDF of the paper titled Semantics for 2D Rasterization, by Bhargav Kulkarni and 2 other authors (https://arxiv.org/pdf/2603.23696) View PDF (https://arxiv.org/html/2603.23696v1) HTML (experimental) Abstract: 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 operations that they ask these libraries to perform. Even Google Chrome, a highly optimized program 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 $\mu$Skia, a formal semantics for the Skia 2D graphics library, and mechanize this semantics in Lean. $\mu$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. $\mu$Skia allows us to verify 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 99 Skia programs gathered from the top 100 websites, this optimizer yields a speedup of 18.7% over Skia's most modern GPU backend, while taking at most 32 $\mu$s 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 $\mu$Skia semantics and translation validated in Lean.  Comments: 23 pages, 15 figures  Subjects: Programming Languages (cs.PL)   (Association of Computing Machinery Classification) ACM classes: I.3; D.3.1; D.3.2  Cite as: (2603.23696.html) arXiv:2603.23696 [cs.PL]    (or (https://arxiv.org/abs/2603.23696v1) arXiv:2603.23696v1 [cs.PL] for this version)    (https://doi.org/10.48550/arXiv.2603.23696) https://doi.org/10.48550/arXiv.2603.23696   Focus to learn more   arXiv-issued DOI via DataCite        Submission history From: Bhargav Kulkarni [(https://arxiv.org/show-email/c5690592/2603.23696) view email ]  [v1] Tue, 24 Mar 2026 20:14:34 UTC (1,399 KB)    Full-text links: Access Paper: View a PDF of the paper titled Semantics for 2D Rasterization, by Bhargav Kulkarni and 2 other authors (https://arxiv.org/pdf/2603.23696) View PDF  (https://arxiv.org/html/2603.23696v1) HTML (experimental)  (https://arxiv.org/src/2603.23696) TeX Source    (http://creativecommons.org/licenses/by/4.0/) (Rights to this article) (license icon)  view license    Current browse context: cs.PL (https://arxiv.org/prevnext?id=2603.23696&function=prev&context=cs.PL) (previous in cs.PL (accesskey p)) < prev  |  (https://arxiv.org/prevnext?id=2603.23696&function=next&context=cs.PL) (next in cs.PL (accesskey n)) next >    (https://arxiv.org/list/cs.PL/new) new |  (https://arxiv.org/list/cs.PL/recent) recent |  (https://arxiv.org/list/cs.PL/2026-03) 2026-03  Change to browse by: (https://arxiv.org/abs/2603.23696?context=cs) cs    References & Citations (https://ui.adsabs.harvard.edu/abs/arXiv:2603.23696) NASA ADS  (https://scholar.google.com/scholar_lookup?arxiv_id=2603.23696) Google Scholar  (https://api.semanticscholar.org/arXiv:2603.23696) Semantic Scholar     export BibTeX citation Loading...  BibTeX formatted citation ×  loading...  Data provided by:      Bookmark  (http://www.bibsonomy.org/BibtexHandler?requTask=upload&url=https://arxiv.org/abs/2603.23696&description=Semantics for 2D Rasterization) (Bookmark on BibSonomy) (BibSonomy)   (https://reddit.com/submit?url=https://arxiv.org/abs/2603.23696&title=Semantics for 2D Rasterization) (Bookmark on Reddit) (Reddit)     Bibliographic Tools Bibliographic and Citation Tools  Bibliographic Explorer Toggle   Bibliographic Explorer ((https://info.arxiv.org/labs/showcase.html#arxiv-bibliographic-explorer) What is the Explorer? )    Connected Papers Toggle   Connected Papers ((https://www.connectedpapers.com/about) What is Connected Papers? )    Litmaps Toggle   Litmaps ((https://www.litmaps.co/) What is Litmaps? )    scite.ai Toggle   scite Smart Citations ((https://www.scite.ai/) What are Smart Citations? )         Code, Data, Media Code, Data and Media Associated with this Article  alphaXiv Toggle   alphaXiv ((https://alphaxiv.org/) What is alphaXiv? )    Links to Code Toggle   CatalyzeX Code Finder for Papers ((https://www.catalyzex.com) What is CatalyzeX? )    DagsHub Toggle   DagsHub ((https://dagshub.com/) What is DagsHub? )    GotitPub Toggle   Gotit.pub ((http://gotit.pub/faq) What is GotitPub? )    Huggingface Toggle   Hugging Face ((https://huggingface.co/huggingface) What is Huggingface? )    ScienceCast Toggle   ScienceCast ((https://sciencecast.org/welcome) What is ScienceCast? )           Demos Demos  Replicate Toggle   Replicate ((https://replicate.com/docs/arxiv/about) What is Replicate? )    Spaces Toggle   Hugging Face Spaces ((https://huggingface.co/docs/hub/spaces) What is Spaces? )    Spaces Toggle   TXYZ.AI ((https://txyz.ai) What is TXYZ.AI? )        Related Papers Recommenders and Search Tools  Link to Influence Flower   Influence Flower ((https://influencemap.cmlab.dev/) What are Influence Flowers? )    Core recommender toggle   CORE Recommender ((https://core.ac.uk/services/recommender) What is CORE? )     Author  Venue  Institution  Topic                About arXivLabs  arXivLabs: experimental projects with community collaborators arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? (https://info.arxiv.org/labs/index.html) Learn more about arXivLabs  .                (https://arxiv.org/auth/show-endorsers/2603.23696) Which authors of this paper are endorsers? | Disable MathJax ((https://info.arxiv.org/help/mathjax.html) What is MathJax? )      We gratefully acknowledge support from
        our major funders , (https://info.arxiv.org/about/ourmembers.html) member institutions  ,   ,
        and all contributors.  (https://info.arxiv.org/about) About · (https://info.arxiv.org/help) Help · (https://info.arxiv.org/help/contact.html) Contact · (https://info.arxiv.org/help/subscribe) Subscribe · (https://info.arxiv.org/help/license/index.html) Copyright · (https://info.arxiv.org/help/policies/privacy_policy.html) Privacy · (https://info.arxiv.org/help/web_accessibility.html) Accessibility · (https://status.arxiv.org) Operational Status(opens in new tab)    Major funding support from (https://www.simonsfoundation.org/) (Simons Foundation)  (https://www.sfi.org.bm/) (Simons Foundation International)  (https://www.schmidtsciences.org/) (Schmidt Sciences)