A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler
Article No.: 240, Pages 121 - 146
Abstract
This article describes a programming language for writing low-level libraries for computer algebra systems. Such libraries (GMP, BLAS/LAPACK, etc) are usually written in C, Fortran, and Assembly, and make heavy use of arrays and pointers. The proposed language, halfway between C and Rust, is designed to be safe and to ease the deductive verification of programs, while being low-level enough to be suitable for this kind of computationally intensive applications. This article also describes a compiler for this language, based on CompCert. The safety of the language has been formally proved using the Coq proof assistant, and so has the property of semantics preservation for the compiler. While the language is not yet feature-complete, this article shows what it entails to design a new domain-specific programming language along its formally verified compiler.
References
[1]
Andrew W. Appel. 2011. Verified Software Toolchain. In 20th European Symposium on Programming, Gilles Barthe (Ed.) (Lecture Notes in Computer Science, Vol. 6602). 1–17. https://doi.org/10.1007/978-3-642-19718-5_1
[2]
Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Transactions on Programming Languages and Systems, 36, 1 (2014), Article 4, March, 35 pages. https://doi.org/10.1145/2579080
[3]
Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. 2018. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning, 61 (2018), June, 367–422. https://doi.org/10.1007/s10817-018-9457-5
[4]
Jean-Louis Colaço, Baptiste Pauget, and Marc Pouzet. 2023. Polymorphic Types with Polynomial Sizes. In 9th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming. 36–49. https://doi.org/10.1145/3589246.3595372
[5]
Archibald Samuel Elliott, Andrew Ruef, Michael Hicks, and David Tarditi. 2018. Checked C: Making C safe by extension. In 2018 IEEE Cybersecurity Development (SecDev). 53–60. https://doi.org/10.1109/SecDev.2018.00015
[6]
Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, and Alexandre Bérard. 2023. Formally Verifying Optimizations with Block Simulations. Proceedings of the ACM on Programming Languages, 7, OOPSLA2 (2023), Oct., 59–88. https://doi.org/10.1145/3622799
[7]
Troels Henriksen and Martin Elsman. 2021. Towards size-dependent types for array programming. In 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming, Tze Meng Low and Jeremy Gibbons (Eds.). 1–14. https://doi.org/10.1145/3460944.3464310
[8]
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. 2020. Verification of Programs with Pointers in SPARK. In 22nd International Conference on Formal Engineering Methods, Shang-Wei Lin, Zhe Hou, and Brendan Mahony (Eds.) (Lecture Notes in Computer Science, Vol. 12531). 55–72. https://doi.org/10.1007/978-3-030-63406-3_4
[9]
Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer. 2019. Stacked borrows: an aliasing model for Rust. Proceedings of the ACM on Programming Languages, 4, POPL (2019), Article 41, Dec., 32 pages. https://doi.org/10.1145/3371109
[10]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2, POPL (2017), Article 66, Dec., 34 pages. https://doi.org/10.1145/3158154
[11]
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In 41st ACM SIGPLAN Symposium on Principles of Programming Languages, Peter Sewell (Ed.). 179–191. https://doi.org/10.1145/2535838.2535841
[12]
Xavier Leroy. 2009. A formally verified compiler back-end. Journal of Automated Reasoning, 43, 4 (2009), 363–446. https://doi.org/10.1007/s10817-009-9155-4
[13]
Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814
[14]
Xavier Leroy and Sandrine Blazy. 2008. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41, 1 (2008), 1–31. https://doi.org/10.1007/s10817-008-9099-0
[15]
Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, David Van Horn, and Michael Hicks. 2022. A formal model of Checked C. In 35th IEEE Symposium on Computer Security Foundations. 49–63. https://doi.org/10.1109/CSF54842.2022.9919657
[16]
Guillaume Melquiond and Raphaël Rieu-Helft. 2023. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. Journal of Symbolic Computation, 115 (2023), 74–95. https://doi.org/10.1016/j.jsc.2022.07.007
[17]
Josué Moreau and Guillaume Melquiond. 2024. A Safe Low-level Language for Computer Algebra and its Formally Verified Compiler. https://doi.org/10.5281/zenodo.11502426 Software Artifact
[18]
Magnus O. Myreen. 2021. The CakeML Project’s Quest for Ever Stronger Correctness Theorems. In 12th International Conference on Interactive Theorem Proving, Liron Cohen and Cezary Kaliszyk (Eds.) (Leibniz International Proceedings in Informatics, Vol. 193). Article 1, 10 pages. https://doi.org/10.4230/LIPIcs.ITP.2021.1
[19]
Raphaël Rieu-Helft. 2020. Development and verification of arbitrary-precision integer arithmetic libraries. Université Paris-Saclay. https://theses.hal.science/tel-03032942
[20]
Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, and Michael Hicks. 2019. Achieving Safety Incrementally with Checked C. In 8th International Conference on Principles of Security and Trust, Flemming Nielson and David Sands (Eds.) (Lecture Notes in Computer Science, Vol. 11426). 76–98. https://doi.org/10.1007/978-3-030-17138-4_4
[21]
Kai Trojahner and Clemens Grelck. 2009. Dependently typed array programs don’t go wrong. Journal of Logic and Algebraic Programming, 78, 7 (2009), Aug., 643–664. https://doi.org/10.1016/j.jlap.2009.03.002
[22]
Hongwei Xi and Frank Pfenning. 1998. Eliminating Array Bound Checking through Dependent Types. ACM SIGPLAN Notices, 33, 5 (1998), May, 249–257. https://doi.org/10.1145/277652.277732
[23]
Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. ACM SIGPLAN Notices, 47, 1 (2012), Jan., 427–440. https://doi.org/10.1145/2103621.2103709
Index Terms
- A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler
Recommendations
Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional ProgrammingCompiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different ...
A Formally Verified Compiler Back-end
This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming ...
Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP '15Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2024
1031 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 August 2024
Published in PACMPL Volume 8, Issue ICFP
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- European Research Council
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 250Total Downloads
- Downloads (Last 12 months)250
- Downloads (Last 6 weeks)70
Reflects downloads up to 09 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in