{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:40:01Z","timestamp":1750671601929,"version":"3.41.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,4,11]],"date-time":"2025-04-11T00:00:00Z","timestamp":1744329600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,4,11]],"date-time":"2025-04-11T00:00:00Z","timestamp":1744329600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100008047","name":"Carnegie Mellon University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100008047","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            <jats:italic>CairoZero<\/jats:italic> is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.\n<\/jats:p>","DOI":"10.1007\/s10817-025-09723-y","type":"journal-article","created":{"date-parts":[[2025,4,11]],"date-time":"2025-04-11T08:16:59Z","timestamp":1744359419000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Proof-Producing Compiler for Blockchain Applications"],"prefix":"10.1007","volume":"69","author":[{"given":"Jeremy","family":"Avigad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lior","family":"Goldberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Levit","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoav","family":"Seginer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alon","family":"Titelman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,4,11]]},"reference":[{"issue":"7","key":"9723_CR1","doi-asserted-by":"publisher","first-page":"1287","DOI":"10.1007\/s10817-020-09559-8","volume":"64","author":"O Abrahamsson","year":"2020","unstructured":"Abrahamsson, O., Ho, S., Kanabar, H., Kumar, R., Myreen, M.O., Norrish, M., Tan, Y.K.: Proof-producing synthesis of CakeML from monadic HOL functions. J. Autom. Reason. 64(7), 1287\u20131306 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09559-8","journal-title":"J. Autom. Reason."},{"issue":"7","key":"9723_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/390013.808479","volume":"5","author":"FE Allen","year":"1970","unstructured":"Allen, F.E.: Control flow analysis. SIGPLAN Not. 5(7), 1\u201319 (1970). https:\/\/doi.org\/10.1145\/390013.808479","journal-title":"SIGPLAN Not."},{"key":"9723_CR3","doi-asserted-by":"publisher","first-page":"6","DOI":"10.4230\/LIPICS.ITP.2023.6","volume-title":"Interactive Theorem Proving (ITP) 2023. LIPIcs","author":"DK Angdinata","year":"2023","unstructured":"Angdinata, D.K., Xu, J.: An elementary formal proof of the group law on Weierstrass elliptic curves in any characteristic. In: Naumowicz, A., Thiemann, R. (eds.) Interactive Theorem Proving (ITP) 2023. LIPIcs, vol. 268, pp. 6\u20131619. Leibniz-Zentrum f\u00fcr Informatik, Schloss Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.6"},{"key":"9723_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.4230\/LIPICS.ITP.2023.7","volume-title":"Interactive Theorem Proving (ITP) 2023. LIPIcs","author":"J Avigad","year":"2023","unstructured":"Avigad, J., Goldberg, L., Levit, D., Seginer, Y., Titelman, A.: A proof-producing compiler for blockchain applications. In: Naumowicz, A., Thiemann, R. (eds.) Interactive Theorem Proving (ITP) 2023. LIPIcs, vol. 268, pp. 7\u20131719. Leibniz-Zentrum f\u00fcr Informatik, Schloss Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.7"},{"key":"9723_CR5","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1145\/3497775.3503675","volume-title":"Certified Programs and Proofs (CPP) 2022","author":"J Avigad","year":"2022","unstructured":"Avigad, J., Goldberg, L., Levit, D., Seginer, Y., Titelman, A.: A verified algebraic representation of Cairo program execution. In: Popescu, A., Zdancewic, S. (eds.) Certified Programs and Proofs (CPP) 2022, pp. 153\u2013165. ACM, New York (2022). https:\/\/doi.org\/10.1145\/3497775.3503675"},{"key":"9723_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-08970-6_6","volume-title":"Interactive Theorem Proving (ITP) 2014","author":"E Bartzia","year":"2014","unstructured":"Bartzia, E., Strub, P.: A formal library for elliptic curves in the Coq proof assistant. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving (ITP) 2014, pp. 77\u201392. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_6"},{"key":"9723_CR7","unstructured":"Ben-Sasson, E., Bentov, I., Horesh, Y., Riabzev, M.: Scalable, transparent, and post-quantum secure computational integrity. IACR Cryptol. ePrint Arch. 2018, 46 (2018). http:\/\/eprint.iacr.org\/2018\/046"},{"key":"9723_CR8","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-030-53518-6_5","volume-title":"Intelligent Computer Mathematics (CICM) 2020","author":"M Carneiro","year":"2020","unstructured":"Carneiro, M.: Metamath Zero: Designing a theorem prover prover. In: Benzm\u00fcller, C., Miller, B.R. (eds.) Intelligent Computer Mathematics (CICM) 2020, pp. 71\u201388. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_5"},{"key":"9723_CR9","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/2500365.2500592","volume-title":"International Conference on Functional Programming (ICFP) 2013","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: Morrisett, G., Uustalu, T. (eds.) International Conference on Functional Programming (ICFP) 2013, pp. 391\u2013402. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2500365.2500592"},{"issue":"8","key":"9723_CR10","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). https:\/\/doi.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"key":"9723_CR11","unstructured":"Erbsen, A.: Crafting certified elliptic curve cryptography implementations in Coq. PhD thesis, Massachusetts Institute of Technology (2017)"},{"issue":"1","key":"9723_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/3421473.3421477","volume":"54","author":"A Erbsen","year":"2020","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic: with proofs, without compromises. ACM SIGOPS Oper. Syst. Rev. 54(1), 23\u201330 (2020). https:\/\/doi.org\/10.1145\/3421473.3421477","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"9723_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"European Symposium on Programming (ESOP) 2013","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2013Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) European Symposium on Programming (ESOP) 2013, pp. 125\u2013128. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"9723_CR14","unstructured":"Goldberg, L., Papini, S., Riabzev, M.: Cairo - a Turing-complete STARK-friendly CPU architecture. IACR Cryptol. ePrint Arch. 1063 (2021). https:\/\/eprint.iacr.org\/2021\/1063"},{"key":"9723_CR15","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-030-51054-1_15","volume-title":"International Joint Conference on Automated Reasoning (IJCAR) 2020","author":"TC Hales","year":"2020","unstructured":"Hales, T.C., Raya, R.: Formal proof of the group law for edwards elliptic curves. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) International Joint Conference on Automated Reasoning (IJCAR) 2020, pp. 254\u2013269. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_15"},{"key":"9723_CR16","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/2535838.2535841","volume-title":"Principles of Programming Languages (POPL) 2014","author":"R Kumar","year":"2014","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) Principles of Programming Languages (POPL) 2014, pp. 179\u2013192. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535841"},{"key":"9723_CR17","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) 2010\u201316th","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) 2010\u201316th, pp. 348\u2013370. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"issue":"7","key":"9723_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"9723_CR19","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Conference on Automated Deduction (CADE) 2015","author":"LM Moura","year":"2015","unstructured":"Moura, L.M., Kong, S., Avigad, J., Doorn, F., Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Conference on Automated Deduction (CADE) 2015, pp. 378\u2013388. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"9723_CR20","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Conference on Automated Deduction (CADE) 2021","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) Conference on Automated Deduction (CADE) 2021, pp. 625\u2013635. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"9723_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-00722-4_2","volume-title":"Compiler Construction (CC) 2009","author":"MO Myreen","year":"2009","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Extensible proof-producing compilation. In: Moor, O., Schwartzbach, M.I. (eds.) Compiler Construction (CC) 2009, pp. 2\u201316. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-00722-4_2"},{"key":"9723_CR22","doi-asserted-by":"publisher","unstructured":"Protzenko, J., Parno, B., Fromherz, A., Hawblitzel, C., Polubelova, M., Bhargavan, K., Beurdouche, B., Choi, J., Delignat-Lavaud, A., Fournet, C., Kulatova, N., Ramananandro, T., Rastogi, A., Swamy, N., Wintersteiger, C.M., B\u00e9guelin, S.Z.: Evercrypt: A fast, verified, cross-platform cryptographic provider. In: IEEE Symposium on Security and Privacy (SP) 2020, pp. 983\u20131002. IEEE, Piscataway (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00114","DOI":"10.1109\/SP40000.2020.00114"},{"key":"9723_CR23","doi-asserted-by":"publisher","unstructured":"Schwabe, P., Viguier, B., Weerwag, T., Wiedijk, F.: A Coq proof of the correctness of X25519 in TweetNaCl. In: Computer Security Foundations Symposium (CSF) 2021, pp. 1\u201316. IEEE, Piscataway (2021). https:\/\/doi.org\/10.1109\/CSF51468.2021.00023","DOI":"10.1109\/CSF51468.2021.00023"},{"issue":"4","key":"9723_CR24","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1017\/S0956796813000142","volume":"23","author":"N Swamy","year":"2013","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. J. Funct. Program. 23(4), 402\u2013451 (2013). https:\/\/doi.org\/10.1017\/S0956796813000142","journal-title":"J. Funct. Program."},{"key":"9723_CR25","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1145\/3372885.3373824","volume-title":"Certified Programs and Proofs (CPP) 2020","author":"The mathlib community","year":"2020","unstructured":"The mathlib community: The Lean mathematical library. In: Blanchette, J., Hritcu, C. (eds.) Certified Programs and Proofs (CPP) 2020, pp. 367\u2013381. ACM, New York (2020). https:\/\/doi.org\/10.1145\/3372885.3373824"},{"key":"9723_CR26","unstructured":"Th\u00e9ry, L.: Proving the group law for elliptic curves formally. Technical Report RT-0330, INRIA (2007). https:\/\/hal.inria.fr\/inria-00129237"},{"key":"9723_CR27","doi-asserted-by":"publisher","first-page":"1789","DOI":"10.1145\/3133956.3134043","volume-title":"Conference on Computer and Communications Security (CCS) 2017","author":"JK Zinzindohou\u00e9","year":"2017","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: A verified modern cryptographic library. In: Thuraisingham, B., Evans, D., Malkin, T., Xu, D. (eds.) Conference on Computer and Communications Security (CCS) 2017, pp. 1789\u20131806. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3133956.3134043"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09723-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09723-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09723-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:04:16Z","timestamp":1750669456000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09723-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,11]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["9723"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09723-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,4,11]]},"assertion":[{"value":"27 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 April 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"9"}}