Extracting functional programs from Coq, in Coq. (English) Zbl 07581654
Summary: We implement extraction of Coq programs to functional languages based on MetaCoq’s certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call \({\lambda^T_\square}\) . We complement the extraction functionality with a full pipeline that includes several standard transformations (e.g. eta-expansion and inlining) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised \({\lambda^T_\square}\) representation, we obtain code in two functional smart contract languages, Liquidity and CameLIGO, the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.
MSC:
| 68N18 | Functional programming and lambda calculus |
References:
| [1] | Abate, C., Haselwarter, P. G., Rivas, E., Muylder, A. V., Winterhalter, T., Hritcu, C., Maillard, K. & Spitters, B. (2021) SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. Cryptology ePrint Archive, Report 2021/397. Available at: https://eprint.iacr.org/2021/397. |
| [2] | Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Belanger, O., Sozeau, M. & Weaver, M. (2017) CertiCoq: A verified compiler for Coq. In CoqPL’2017. |
| [3] | Anand, A., Boulier, S., Cohen, C., Sozeau, M. & Tabareau, N. (2018) Towards certified meta-programming with typed template-Coq. In ITP18. LNCS, vol. 10895, pp. 20-39. Available at: https://hal.archives-ouvertes.fr/hal-01809681 · Zbl 1468.68071 |
| [4] | Annenkov, D. & Elsman, M. (2018) Certified compilation of financial contracts. In PPDP’2018. |
| [5] | Annenkov, D., Milo, M., Nielsen, J. B. & Spitters, B. (2021) Extracting smart contracts tested and verified in Coq. In CPP 2021. Association for Computing Machinery, pp. 105-121. Available at: https://doi.org/10.1145/3437992.3439934 |
| [6] | Annenkov, D., Nielsen, J. B. & Spitters, B. (2020) ConCert: A smart contract certification framework in Coq. In CPP’2020. |
| [7] | Atkey, R. (2018) Syntax and semantics of quantitative type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS’18. New York, NY, USA: Association for Computing Machinery, pp. 56-65. · Zbl 1452.03029 |
| [8] | Bahr, P., Berthold, J. & Elsman, M. (2015) Certified symbolic management of financial multi-party contracts. SIGPLAN Not. · Zbl 1360.68356 |
| [9] | Barras, B. & Bernardo, B. (2008) The implicit calculus of constructions as a programming language with dependent types. In Foundations of Software Science and Computational Structures, Amadio, R. (ed.). Springer Berlin Heidelberg, pp. 365-379. · Zbl 1138.68356 |
| [10] | Barras, B. & Grégoire, B. (2005) On the role of type decorations in the calculus of inductive constructions. In CSL. · Zbl 1136.03305 |
| [11] | Berardi, S. (1996) Pruning simply typed \(\lambda \) -terms. J. Logic. Comput.6(5), 663-681. Available at: https://doi.org/10.1093/logcom/6.5.663. · Zbl 0863.03007 |
| [12] | Berghofer, S. & Nipkow, T. (2002) Executing higher order logic. In Types for Proofs and Programs, Callaghan, P., Luo, Z., McKinna, J., Pollack, R. & Pollack, R. (eds). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 24-40. · Zbl 1054.68133 |
| [13] | Bernardo, B. (2015) Un Calcul des Constructions implicite avec sommes dépendantes et À inférence de type décidable. Theses, école polytechnique. Version soutenance. Available at: https://hal.inria.fr/tel-01197380 |
| [14] | Boehm, H., Demers, A. J. & Shenker, S. (1991) Mostly parallel garbage collection. In PLDI. ACM, pp. 157-164. |
| [15] | Boehm, H. & Weiser, M. D. (1988) Garbage collection in an uncooperative environment. Softw. Pract. Exp.18(9), 807-820. |
| [16] | Boerio, L. (1994) Extending pruning techniques to polymorphic second order \(\lambda \) -calculus. In Programming Languages and Systems—ESOP’94, Sannella, D. (ed.). Springer Berlin Heidelberg. |
| [17] | Bozman, C., Iguernlala, M., Laporte, M., Le Fessant, F. & Mebsout, A. (2018) Liquidity: OCaml pour la Blockchain. In JFLA18. |
| [18] | Brady, E. (2021) Idris 2: Quantitative type theory in practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021), Møller, A. & Sridharan, M. (eds). Leibniz International Proceedings in Informatics (LIPIcs), vol. 194. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 9:1-9:26. |
| [19] | Brady, E., Mcbride, C. & Mckinna, J. (2004) Inductive families need not store their indices. In Types for Proofs and Programs, Berardi, S., Coppo, M. & Damiani, F. (eds). Springer Berlin Heidelberg, pp. 115-129. · Zbl 1100.68546 |
| [20] | Chapman, J., Kireev, R., Nester, C. & Wadler, P. (2019) System F in Agda, for fun and profit. In MPC’19. · Zbl 1434.68079 |
| [21] | Chlipala, A. (2013) Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. · Zbl 1288.68001 |
| [22] | Cruz-Filipe, L.Letouzey, P. (2006) A large-scale experiment in executing extracted programs. Electron. Notes Theor. Comput. Sci. · Zbl 1273.68317 |
| [23] | Cruz-Filipe, L. & Spitters, B. (2003) Program extraction from large proof developments. In Theorem Proving in Higher Order Logics. · Zbl 1279.68287 |
| [24] | Danielsson, N. A. (2019) Logical properties of a modality for erasure. Accessed July 7, 2021. Available at: http://www.cse.chalmers.se/ nad/publications/danielsson-erased.pdf. |
| [25] | Dziembowski, S., Eckey, L. & Faust, S. (2018) FairSwap: How to fairly exchange digital goods. In ACM Conference on Computer and Communications Security. ACM, pp. 967-984. |
| [26] | Erbsen, A., Philipoom, J., Gross, J., Sloan, R. & Chlipala, A. (2019) Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In IEEE Symposium on Security and Privacy. |
| [27] | Feldman, R. (2020) Elm in Action. Manning. |
| [28] | Filliâtre, J.-C. & Letouzey, P. (2004) Functors for proofs and programs. In Programming Languages and Systems, Schmidt, D. (ed.). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 370-384. · Zbl 1126.68475 |
| [29] | Gilbert, G., Cockx, J., Sozeau, M. & Tabareau, N. (2019) Definitional proof-irrelevance without K. Proc. ACM Program. Lang. 3(POPL). |
| [30] | Haftmann, F. & Nipkow, T. (2007), A code generator framework for Isabelle/HOL. In Department of Computer Science, University of Kaiserslautern. |
| [31] | Hao, F., Ryan, P. Y. & Zieliński, P. (2010) Anonymous voting by two-round public discussion. IET Inf. Security4(2). |
| [32] | Henglein, F., Larsen, C. K. & Murawska, A. (2020) A formally verified static analysis framework for compositional contracts. In Financial Cryptography and Data Security (FC). |
| [33] | Hupel, L. & Nipkow, T. (2018) A verified compiler from Isabelle/HOL to CakeML. In Programming Languages and Systems, Ahmed, A. (ed.), pp. 999-1026. · Zbl 1418.68045 |
| [34] | Jung, R., Jourdan, J.-H., Krebbers, R. & Dreyer, D. (2021) Safe systems programming in rust. Commun. ACM64(4), 144-152. |
| [35] | Klabnik, S. & Nichols, C. (2018) The Rust Programming Language. USA: No Starch Press. |
| [36] | Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R. & Heiser, G. (2014) Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst.32(1), 2:1-2:70. |
| [37] | Kumar, R., Myreen, M. O., Norrish, M. & Owens, S. (2014) CakeML: A verified implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’14. ACM, pp. 179-191. Available at: http://doi.acm.org/10.1145/2535838.2535841 · Zbl 1284.68405 |
| [38] | Kusee, W. H. (2017) Compiling Agda to Haskell with Fewer Coercions. Master’s thesis. |
| [39] | Lamela Seijas, P. & Thompson, S. (2018) Marlowe: Financial contracts on blockchain. In International Symposium o Leveraging Applications of Formal Methods, Verification and Validation, Margaria, T. & Steffen, B. (eds). Industrial Practice. |
| [40] | Landin, P. J. (1964) The mechanical evaluation of expressions. Comput. J.6, 308-320. · Zbl 0122.36106 |
| [41] | Lee, O. & Yi, K. (1998) Proofs about a Folklore let-polymorphic type inference algorithm. ACM Trans. Program. Lang. Syst. |
| [42] | Leroy, X. (2006) Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In POPL, pp. 42-54. · Zbl 1369.68124 |
| [43] | Letouzey, P. (2003) A new extraction for Coq. In Types for Proofs and Programs, pp. 200-219. · Zbl 1023.68516 |
| [44] | Letouzey, P. (2004) Programmation fonctionnelle certifiée - L’extraction de programmes dans l’assistant Coq. PhD thesis, Université Paris-Sud. English version: https://www.irif.fr/ letouzey/download/these_letouzey_English.ps.gz. |
| [45] | Mccorry, P., Shahandashti, S. F. & Hao, F. (2017) A smart contract for boardroom voting with maximum voter privacy. In FC 2017. · Zbl 1460.94057 |
| [46] | Miquel, A. (2001) The implicit calculus of constructions: Extending pure type systems with an intersection type binder and subtyping. In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, TLCA’01. Springer-Verlag, pp. 344-359. · Zbl 0981.03029 |
| [47] | Mishra-Linger, N. & Sheard, T. (2008) Erasure and polymorphism in pure type systems. In Foundations of Software Science and Computational Structures, Amadio, R. (ed.). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 350-364. · Zbl 1138.68361 |
| [48] | Mullen, E., Pernsteiner, S., Wilcox, J. R., Tatlock, Z. & Grossman, D. (2018) Œuf: Minimizing the Coq extraction TCB. In CPP 2018. |
| [49] | Necula, G. C. (1997) Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’97. New York, NY, USA: Association for Computing Machinery, pp. 106-119. Available at: https://doi.org/10.1145/263699.263712 |
| [50] | Nielsen, J. B. & Spitters, B. (2019) Smart contract interactions in Coq. In FMBC’2019. |
| [51] | O’Connor, R. (2017) Simplicity: A new language for blockchains. In PLAS17. |
| [52] | Paraskevopoulou, Z., Li, J. M. & Appel, A. W. (2021) Compositional optimizations for certicoq. Proc. ACM Program. Lang. 5(ICFP). Available at: https://doi.org/10.1145/3473591. |
| [53] | Paulin-Mohring, C. (1989) Extracting \(F \omega \) ’s programs from proofs in the calculus of constructions. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages’, POPL’89. New York, NY, USA: Association for Computing Machinery, pp. 89-104. |
| [54] | Pit-Claudel, C., Wang, P., Delaware, B., Gross, J. & Chlipala, A. (2020) Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs. In Automated Reasoning, Peltier, N. & Sofronie-Stokkermans, V. (eds), pp. 119-137. · Zbl 07614665 |
| [55] | Prost, F. (1995) Marking techniques for extraction. Research Report LIP RR-1995-47, Laboratoire de l’informatique du parallélisme. Available at: https://hal-lara.archives-ouvertes.fr/hal-02102062. |
| [56] | Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A. & Chan, K. (2019) Safer smart contract programming with Scilla. In OOPSLA19. |
| [57] | Šinkarovs, A. & Cockx, J. (2021) Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection. |
| [58] | Sozeau, M., Anand, A., Boulier, S., Cohen, C., Forster, Y., Kunze, F., Malecha, G., Tabareau, N. & Winterhalter, T. (2020) The metacoq project. J. Autom. Reas. · Zbl 1468.68075 |
| [59] | Sozeau, M., Boulier, S., Forster, Y., Tabareau, N. & Winterhalter, T. (2019) Coq Coq Correct! verification of type checking and erasure for Coq, in Coq. In POPL’2019. |
| [60] | Sozeau, M. & Mangin, C. (2019) Equations reloaded: High-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang.3(ICFP). |
| [61] | Tanaka, A. (2021) Coq to C translation with partial evaluation. In Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2021, pp. 14-31. |
| [62] | Timany, A. & Sozeau, M. (2017) Consistency of the predicative calculus of cumulative inductive constructions (pCuIC). CoRR abs/1710.03912. Available at: http://arxiv.org/abs/1710.03912 |
| [63] | Watt, C. (2018) Mechanising and verifying the webAssembly specification. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, New York, NY, USA, pp. 53-65. |
| [64] | Weiss, A., Gierczak, O., Patterson, D., Matsakis, N. D. & Ahmed, A. (2019) Oxide: The Essence of Rust. arXiv e-prints. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
