{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:22:19Z","timestamp":1760059339695,"version":"build-2065373602"},"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\u2014a 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 high-level 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"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9608-0774","authenticated-orcid":false,"given":"Yanning","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]},{"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"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9127-7314","authenticated-orcid":false,"given":"Luke","family":"Pearson","sequence":"additional","affiliation":[{"name":"Polychain Capital, San Francisco, USA"}]},{"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"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_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_2_1_2_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_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_21"},{"key":"e_1_2_1_4_1","unstructured":"Miguel Ambrona Anne-Laure Schmitt Raphael R. Toledo and Danny Willems. 2022. New optimization techniques for PlonK\u2019s arithmetization. Cryptology ePrint Archive Paper 2022\/462. https:\/\/eprint.iacr.org\/2022\/462"},{"key":"e_1_2_1_5_1","unstructured":"Anoma. 2021. Juvix. https:\/\/docs.juvix.org\/"},{"key":"e_1_2_1_6_1","volume-title":"Jolt: SNARKs for Virtual Machines via Lookups. Cryptology ePrint Archive, Paper 2023\/1217. https:\/\/eprint.iacr.org\/2023\/1217","author":"Arun Arasu","year":"2023","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_2_1_7_1","unstructured":"Aztec. [n. d.]. Noir. https:\/\/github.com\/noir-lang\/noir Accessed: 2024-9-10"},{"key":"e_1_2_1_8_1","unstructured":"Aztec. 2022. Introducing Noir. https:\/\/noir-lang.org\/"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3232813"},{"key":"e_1_2_1_11_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. https:\/\/eprint.iacr.org\/2018\/046"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.36"},{"key":"e_1_2_1_13_1","volume-title":"23rd USENIX Security Symposium (USENIX Security 14)","author":"Ben-Sasson Eli","year":"2014","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. isbn:978-1-931971-15-7 https:\/\/www.usenix.org\/conference\/usenixsecurity14\/technical-sessions\/presentation\/ben-sasson"},{"key":"e_1_2_1_14_1","unstructured":"Daniel Benarroch Kobi Gurkan Ron Kahat Aur\u00e9lien Nicolas and Eran Tromer. 2019. zkInterface a standard tool for zero-knowledge interoperability. https:\/\/docs.zkproof.org\/pages\/standards\/accepted-workshop3\/proposal-zkinterface.pdf"},{"key":"e_1_2_1_15_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_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30617-4_17"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45721-1_26"},{"key":"e_1_2_1_18_1","volume-title":"LEO: A Programming Language for Formally Verified, Zero-Knowledge Applications. https:\/\/docs.zkproof.org\/pages\/standards\/accepted-workshop4\/proposal-leo.pdf","author":"Chin Collin","year":"2021","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_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454050"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/Cybermatics_2018.2018.00199"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_2_1_24_1","volume-title":"Williamson","author":"Gabizon Ariel","year":"2020","unstructured":"Ariel Gabizon and Zachary J. Williamson. 2020. plookup: A simplified polynomial protocol for lookup tables. Cryptology ePrint Archive, Paper 2020\/315. https:\/\/eprint.iacr.org\/2020\/315"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 3rd ZKProof Workshop.","author":"Gabizon Ariel","unstructured":"Ariel Gabizon and Zachary J. Williamson. 2020. The turbo-plonk program syntax for specifying snark programs. In Proceedings of the 3rd ZKProof Workshop."},{"key":"e_1_2_1_26_1","volume-title":"PLONK: Permutations over Lagrange-bases for Oecumenical Noninteractive arguments of Knowledge. Cryptology ePrint Archive, Paper 2019\/953. https:\/\/eprint.iacr.org\/2019\/953","author":"Gabizon Ariel","year":"2019","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_2_1_27_1","unstructured":"Lior Goldberg Shahar Papini and Michael Riabzev. 2021. Cairo \u2013 a Turing-complete STARK-friendly CPU architecture. Cryptology ePrint Archive Paper 2021\/1063. https:\/\/eprint.iacr.org\/2021\/1063"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22178"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49896-5_11"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385996"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00078"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16920330"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833782"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_8"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_2_1_38_1","unstructured":"Plonky3 Contributors. 2024. Plonky3: A Toolkit for Polynomial IOPs (PIOPs). https:\/\/github.com\/Plonky3\/Plonky3 Accessed: 2024-11-15"},{"key":"e_1_2_1_39_1","unstructured":"Polygon. 2022. Bring Ethereum to everyone. https:\/\/polygon.technology\/polygon-zkevm"},{"key":"e_1_2_1_40_1","unstructured":"Privacy & Scaling Explorations. [n. d.]. Chiquito. https:\/\/github.com\/privacy-scaling-explorations\/chiquito Accessed: 2024-9-10"},{"key":"e_1_2_1_41_1","unstructured":"Privacy & Scaling Explorations. 2024. halo2. https:\/\/github.com\/privacy-ethereum\/halo2 Accessed: 2024-9-10"},{"key":"e_1_2_1_42_1","unstructured":"Privacy & Scaling Explorations. 2024. PSE zkEVM. https:\/\/github.com\/privacy-scaling-explorations\/zkevm-circuits Accessed: 2024-9-10"},{"key":"e_1_2_1_43_1","unstructured":"RISC Zero. [n. d.]. RISC Zero. https:\/\/github.com\/risc0\/risc0 Accessed: 2024-9-10"},{"key":"e_1_2_1_44_1","unstructured":"Scroll. [n. d.]. Scroll zkEVM. https:\/\/github.com\/scroll-tech\/zkevm-circuits Accessed: 2024-9-10"},{"key":"e_1_2_1_45_1","unstructured":"Scroll. 2022. The Native zkEVM Scaling Solution for Ethereum. https:\/\/scroll.io\/"},{"key":"e_1_2_1_46_1","volume-title":"Program Synthesis by Sketching. Ph. D. Dissertation","author":"Solar-Lezama Armando","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph. D. Dissertation. Berkeley, CA, USA. isbn:978-1-109-09745-0 AAI3353225"},{"key":"e_1_2_1_47_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_2_1_48_1","unstructured":"StarkWare Industries. 2020. Arithmetization I: How to Represent Computation as Algebra. https:\/\/medium.com\/starkware\/arithmetization-i-15c046390862 Accessed: 2024-11-15"},{"key":"e_1_2_1_49_1","unstructured":"Succinct Labs. [n. d.]. SP1. https:\/\/github.com\/succinctlabs\/sp1 Accessed: 2024-9-10"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062365"},{"key":"e_1_2_1_52_1","unstructured":"Zac Williamson. 2021. Aztec\u2019s ZK-ZK-Rollup looking behind the cryptocurtain. https:\/\/medium.com\/aztec-protocol\/aztecs-zk-zk-rollup-looking-behind-the-cryptocurtain-2b8af1fca619 Accessed: 2024-9-10"},{"key":"e_1_2_1_53_1","unstructured":"Zcash. [n. d.]. halo2. https:\/\/github.com\/zcash\/halo2 Accessed: 2024-9-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":[[2025,10,9]],"date-time":"2025-10-09T17:47:40Z","timestamp":1760032060000},"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"}}]}}