Coqaml · Verified Extraction from Coq to OCaml with GADTs
Horizon 2020 — Marie Skłodowska-Curie Actions
- Duration
- 2021-12-01 → 2023-11-30
- EU contribution
- €184,708
- Participants
- 1
- Scheme
- MSCA-IF
Lines connect the coordinator with its partners.
Results in brief
Verified Extraction from Coq to OCaml with GADTs
Problem and Societal Impact: The Coqaml project addresses critical challenges in the utilization of Coq's extraction mechanism, particularly the fact that unsafe casts are inserted even though they are unwanted for industrial applications. The project has identified that extraction guarantees can only be given for a well-defined subset of Coq code. Present applications, such as the CompCert C compiler, have been shown to fall into this fragment, enabling to prove that their extracted code is indeed guaranteed to be correct. By enhancing the extraction process, Coqaml aimed to make verified components more applicable, ultimately contributing to the broader goal of ensuring correctness and trustworthiness in security-critical applications, including cryptographic primitives and smart contracts. Regarding the three main objectives of the project, all central goals were reached. Verification of Coq's Extraction: We used the MetaCoq ecosystem to provide a machine checked proof that translation from the Coq proof assistant into OCaml is correct. We proved that the OCaml code behaves just like the original Coq program. We reached our main goal to ensure that both researcher and industry trust Coq's extraction process more, so important applications (like CompCert and Fiat-Crypto) can rely on it. Industrial Applicability Enhancement: We improved how Coq's extraction works for real-world projects by providing precise conditions when guarantees can be provided. We observed that targeting untyped code both gets rid of unsafe casts and eliminates the need to implement optimizations, which historically were there for readability reasons. Documentation and Accessibility: We implemented extraction as a MetaCoq program for easier adaptation by third parties, and improved the MetaCoq ecosystem, addressing the high entrance barrier. We established. MetaCoq and Coqaml as accessible open-source projects in the Coq ecosystem. MetaCoq is now part of the Coq platform and thus by default installed for every user installing Coq, and Coqaml will be included into Coq soon. We organized scientific events to enhance the visibility of MetaCoq and verified extraction, most notably a tutorial at the POPL '24 conference.
Data: CORDIS, © European Union
Project objective
The Coq proof assistant is a popular tool to verify the correctness of security-critical software. The CompCert C compiler, some implementations of blockchain languages, and the implementation of the P-256 elliptic curve in Google’s BoringSSL library are all OCaml programs obtained by extraction from Coq functions.While a type checker for Coq has recently been verified via a machine-checked mathematical proof based on the MetaCoq project for verified meta-programming, the extraction process from Coq to OCaml is still part of the trusted computing base (TCB).The Coqaml project will minimise the TCB for extracted programs even further by also providing a machine-checked correctness proof for the extraction mechanism to OCaml. Under the supervision of Nicolas Tabareau, head of the Inria Gallinette team in Nantes, the experienced researcher (ER) will implement Coq's extraction as mechanically verified MetaCoq-plugin, obtaining the guarantee that extracted OCaml programs behave exactly like the Coq function specified.In order to be usable in industrial applications, Coqaml will include a novel extraction targeting generalized algebraic datatypes (GADTs) in OCaml. The project includes a secondment of the ER to Nomadic Labs in Paris, who require GADTs as target for Coq's extraction. The intermediate semantic correctness proof for type and proof erasure, allowing axioms like functional extensionality or proof irrelevance in verified programs, can also be exploited in other extraction projects like the CertiCoq compiler from Coq to C code.The Coqaml project is interdisciplanary by design, spanning logic, type theory, programming languages, and compilers. The density of some of the world’s leading experts on Coq and type theory in the Gallinette team and the expertise at Nomadic Labs will ensure that the environment is ideal for the success of the Coqaml project and the most beneficial development of the ER, greatly enhancing his future career prospects.
Original text from CORDIS.
Participants
- INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET AUTOMATIQUE · Le Chesnay CedexCoordinatorFrance
Links
Data: CORDIS, © European Union