{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:07Z","timestamp":1784199967636,"version":"3.55.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["Faculty Research Award"],"award-info":[{"award-number":["Faculty Research Award"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100015595","name":"Ethereum Foundation","doi-asserted-by":"publisher","award":["Academic Award"],"award-info":[{"award-number":["Academic Award"]}],"id":[{"id":"10.13039\/501100015595","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1908494"],"award-info":[{"award-number":["1908494"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["N66001-22-2-4037"],"award-info":[{"award-number":["N66001-22-2-4037"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Zero-knowledge proof (ZKP) applications require translating high-level programs into arithmetic circuits\u2013a process that demands both correctness and efficiency. While recent DSLs improve usability, they often yield suboptimal circuits, and hand-optimized implementations remain difficult to construct and verify. We present Tabby, a synthesis-aided compiler that automates the generation of high-performance ZK circuits from highlevel code. Tabby introduces a domain-specific intermediate representation designed for symbolic reasoning and applies sketch-based program synthesis to derive optimized low-level implementations. By decomposing programs into reusable components and verifying semantic equivalence via SMT-based reasoning, Tabby ensures correctness while achieving substantial performance improvements. We evaluate Tabby on a suite of real-world ZKP applications and demonstrate significant reductions in proof generation time and circuit size against mainstream ZK compilers.<\/jats:p>","DOI":"10.1145\/3763110","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1671-1697","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9656-7073","authenticated-orcid":false,"given":"Junrui","family":"Liu","sequence":"first","affiliation":[{"name":"University of California at Santa Barbara, Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4847-9183","authenticated-orcid":false,"given":"Jiaxin","family":"Song","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9608-0774","authenticated-orcid":false,"given":"Yanning","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7027-8302","authenticated-orcid":false,"given":"Hanzhi","family":"Liu","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3517-445X","authenticated-orcid":false,"given":"Hongbo","family":"Wen","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9127-7314","authenticated-orcid":false,"given":"Luke","family":"Pearson","sequence":"additional","affiliation":[{"name":"Polychain Capital, San Francisco, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6494-3126","authenticated-orcid":false,"given":"Yanju","family":"Chen","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1000-1229","authenticated-orcid":false,"given":"Yu","family":"Feng","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"0xParC. 2023. Big integer arithmetic and secp256k1 ECC operations in circom. https:\/\/github.com\/0xPARC\/circom-ecdsa. Accessed: 2024-11-15."},{"key":"e_1_3_1_3_1","unstructured":"aayush thoughts. 2023. An Opinionated Overview of ZK Tooling and Proof Systems Right Now. https:\/\/blog.aayushg.com\/zk\/. Accessed: 2024-11-15."},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-131851_21"},{"key":"e_1_3_1_5_1","unstructured":"Miguel Ambrona Anne-Laure Schmitt Raphael R. Toledo and Danny Willems. 2022. New optimization techniques for PlonK's arithmetization. Cryptology ePrint Archive Paper 2022\/462. https:\/\/eprint.iacr.org\/2022\/462"},{"key":"e_1_3_1_6_1","unstructured":"Anoma. 2021. Juvix. https:\/\/docs.juvix.org\/."},{"key":"e_1_3_1_7_1","unstructured":"Arasu Arun Srinath Setty and Justin Thaler. 2023. Jolt: SNARKs for Virtual Machines via Lookups. Cryptology ePrint Archive Paper 2023\/1217. https:\/\/eprint.iacr.org\/2023\/1217"},{"key":"e_1_3_1_8_1","unstructured":"Aztec. [n. d.]. Noir. https:\/\/github.com\/noir-lang\/noir. Accessed: 2024-9-10."},{"key":"e_1_3_1_9_1","unstructured":"Aztec. 2022. Introducing Noir. https:\/\/noir-lang.org\/."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3232813"},{"key":"e_1_3_1_12_1","unstructured":"Eli Ben-Sasson Iddo Bentov Yinon Horesh and Michael Riabzev. 2018. Scalable transparent and post-quantum secure computational integrity. Cryptology ePrint Archive Paper 2018\/046. (2018). https:\/\/eprint.iacr.org\/2018\/046"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Eli Ben Sasson Alessandro Chiesa Christina Garman Matthew Green Ian Miers Eran Tromer and Madars Virza. 2014. Zerocash: Decentralized Anonymous Payments from Bitcoin. In 2014 IEEE Symposium on Security and Privacy. 459\u2013474. doi:10.1109\/SP.2014.36","DOI":"10.1109\/SP.2014.36"},{"key":"e_1_3_1_14_1","unstructured":"Eli Ben-Sasson Alessandro Chiesa Eran Tromer and Madars Virza. 2014. Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture. In 23rd USENIX Security Symposium (USENIX Security 14). USENIX Association San Diego CA 781\u2013796. https:\/\/www.usenix.org\/conference\/usenixsecurity14\/technical-sessions\/presentation\/ben-sasson"},{"key":"e_1_3_1_15_1","unstructured":"Daniel Benarroch Kobi Gurkan Ron Kahat Aur\u00e9lien Nicolas and Eran Tromer. 2019. zkInterface a standard tool for zeroknowledge interoperability. https:\/\/docs.zkproof.org\/pages\/standards\/accepted-workshop3\/proposal-zkinterface.pdf."},{"key":"e_1_3_1_16_1","unstructured":"Sean Bowe Jack Grigg and Daira Hopwood. 2019. Recursive Proof Composition without a Trusted Setup. Cryptology ePrint Archive Paper 2019\/1021. https:\/\/eprint.iacr.org\/2019\/1021"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30617-4_17"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45721-1_26"},{"key":"e_1_3_1_19_1","unstructured":"Collin Chin. 2021. LEO: A Programming Language for Formally Verified Zero-Knowledge Applications. https:\/\/docs.zkproof.org\/pages\/standards\/accepted-workshop4\/proposal-leo.pdf."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454050"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Jacob Eberhardt and Stefan Tai. 2018. ZoKrates - Scalable Privacy-Preserving Off-Chain Computations. In 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData). 1084\u20131091. doi:10.1109\/Cybermatics_2018.2018.00199","DOI":"10.1109\/Cybermatics_2018.2018.00199"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_3_1_25_1","unstructured":"Ariel Gabizon and Zachary J. Williamson. 2020a. plookup: A simplified polynomial protocol for lookup tables. Cryptology ePrint Archive Paper 2020\/315. https:\/\/eprint.iacr.org\/2020\/315"},{"key":"e_1_3_1_26_1","unstructured":"Ariel Gabizon and Zachary J. Williamson. 2020b. The turbo-plonk program syntax for specifying snark programs. In Proceedings of the 3rd ZKProof Workshop."},{"key":"e_1_3_1_27_1","unstructured":"Ariel Gabizon Zachary J. Williamson and Oana Ciobotaru. 2019. PLONK: Permutations over Lagrange-bases for Oecumenical Noninteractive arguments of Knowledge. Cryptology ePrint Archive Paper 2019\/953. https:\/\/eprint.iacr.org\/2019\/953"},{"key":"e_1_3_1_28_1","unstructured":"Lior Goldberg Shahar Papini and Michael Riabzev. 2021. Cairo - a Turing-complete STARK-friendly CPU architecture. Cryptology ePrint Archive Paper 2021\/1063. (2021). https:\/\/eprint.iacr.org\/2021\/1063"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22178"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49896-5_11"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Susmit Jha Sumit Gulwani Sanjit A. Seshia and Ashish Tiwari. 2010. Oracle-guided component-based program synthesis. In Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering - Volume 1 (Cape Town South Africa) (ICSE '10). Association for Computing Machinery New York NY USA 215\u2013224. doi:10.1145\/1806799.1806833","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385996"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Junrui Liu Ian Kretz Hanzhi Liu Bryan Tan Jonathan Wang Yi Sun Luke Pearson Anders Miltner I\u015f\u0131l Dillig and Yu Feng. 2024. Certifying Zero-Knowledge Circuits with Refinement Types. In 2024 IEEE Symposium on Security and Privacy (SP). 1741\u20131759. doi:10.1109\/SP54263.2024.00078","DOI":"10.1109\/SP54263.2024.00078"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Junrui Liu Jiaxin Song Yanning Chen Hanzhi Liu Hongbo Wen Luke Pearson Yanju Chen and Yu Feng. 2025. Tabby: A Synthesis-aided Compiler for High-performance Zero-knowledge Proof Circuits. Zenodo. doi:10.5281\/zenodo.16920330","DOI":"10.5281\/zenodo.16920330"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Alex Ozdemir Fraser Brown and Riad S. Wahby. 2022. CirC: Compiler infrastructure for proof systems software verification and more. In 2022 IEEE Symposium on Security and Privacy (SP). 2248\u20132266. doi:10.1109\/SP46214.2022.9833782","DOI":"10.1109\/SP46214.2022.9833782"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_8"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_1_39_1","unstructured":"Plonky3 Contributors. 2024. Plonky3: A Toolkit for Polynomial IOPs (PIOPs). https:\/\/github.com\/Plonky3\/Plonky3. Accessed: 2024\u201311-15."},{"key":"e_1_3_1_40_1","unstructured":"Polygon. 2022. Bring Ethereum to everyone. https:\/\/polygon.technology\/polygon-zkevm."},{"key":"e_1_3_1_41_1","unstructured":"Privacy & Scaling Explorations. [n. d.]. Chiquito. https:\/\/github.com\/privacy-scaling-explorations\/chiquito. Accessed: 2024\u20139-10."},{"key":"e_1_3_1_42_1","unstructured":"Privacy & Scaling Explorations. 2024a. halo2. https:\/\/github.com\/privacy-ethereum\/halo2. Accessed: 2024\u20139-10."},{"key":"e_1_3_1_43_1","unstructured":"Privacy & Scaling Explorations. 2024b. PSE zkEVM. https:\/\/github.com\/privacy-scaling-explorations\/zkevm-circuits. Accessed: 2024\u20139-10."},{"key":"e_1_3_1_44_1","unstructured":"RISC Zero. [n. d.]. RISC Zero. https:\/\/github.com\/risc0\/risc0. Accessed: 2024\u20139-10."},{"key":"e_1_3_1_45_1","unstructured":"Scroll. [n. d.]. Scroll zkEVM. https:\/\/github.com\/scroll-tech\/zkevm-circuits. Accessed: 2024\u20139-10."},{"key":"e_1_3_1_46_1","unstructured":"Scroll. 2022. The Native zkEVM Scaling Solution for Ethereum. https:\/\/scroll.io\/."},{"key":"e_1_3_1_47_1","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph. D. Dissertation. Berkeley CA USA. Advisor(s) Bodik Rastislav. AAI3353225."},{"key":"e_1_3_1_48_1","unstructured":"Fatemeh Heidari Soureshjani Mathias Hall-Andersen MohammadMahdi Jahanara Jeffrey Kam Jan Gorzny and Mohsen Ahmadvand. 2023. Automated Analysis of Halo2 Circuits. Cryptology ePrint Archive Paper 2023\/1051. https:\/\/eprint.iacr.org\/2023\/1051"},{"key":"e_1_3_1_49_1","unstructured":"StarkWare Industries. 2020. Arithmetization I: How to Represent Computation as Algebra. https:\/\/medium.com\/starkware\/arithmetization-i-15c046390862. Accessed: 2024\u201311-15."},{"key":"e_1_3_1_50_1","unstructured":"Succinct Labs. [n. d.]. SP1. https:\/\/github.com\/succinctlabs\/sp1. Accessed: 2024\u20139-10."},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062365"},{"key":"e_1_3_1_53_1","unstructured":"Zac Williamson. 2021. Aztec's ZK-ZK-Rollup looking behind the cryptocurtain. https:\/\/medium.com\/aztec-protocol\/aztecs-zk-zk-rollup-looking-behind-the-cryptocurtain-2b8af1fca619. Accessed: 2024\u20139-10."},{"key":"e_1_3_1_54_1","unstructured":"Zcash. [n. d.]. halo2. https:\/\/github.com\/zcash\/halo2. Accessed: 2024\u20139-10."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763110","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763110","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:07Z","timestamp":1784196427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":53,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763110"],"URL":"https:\/\/doi.org\/10.1145\/3763110","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}