Guilherme Silva (Feb 06 2022 at 21:53): Guilherme Silva (Feb 06 2022 at 21:53):I have watched this video: https://youtu.be/StQ40osfQTo
He told that Coq is fully verified. So is it fully verified like CakeML?
Is there an implementation of a CPU processor in Coq?
If not, is the semantics of some architecture already formalized on it (like RISK-V)? Is the semantic good enough to assure that some optimization will for sure reduce the time of a program for example?
Karl Palmskog (Feb 06 2022 at 22:08):it sounds like you are asking about the CertiCoq compiler. To my knowledge, the latest exact status of verification is here: https://github.com/CertiCoq/certicoq/wiki/The-CertiCoq-pipeline
Since CertiCoq generates Clight, which is defined and compiled by CompCert, you'll have to look at CompCert for the RISC-V questions: https://github.com/absint/compcert
Notification Bot (Feb 06 2022 at 22:08):This topic was moved here from #Coq users > CertiCoq processor by Karl Palmskog
Karl Palmskog (Feb 06 2022 at 22:14):I would be surprised if there are any immediate plans to bootstrap/self-compile CertiCoq(+CompCert) like CakeML does, but someone else here might be able to clarify
Tim Carstens (Feb 07 2022 at 18:03):CertiCoq (the Coq to C compiler) is mostly verified (the team continues to work on adding new features, completing the verification, etc - we recently updated everything to Coq 8.14 and compcert 3.9). At this time, the garbage collector & most layers of the compiler have been verified. I believe it's on track to achieve end-to-end verification sometime relatively soon.
Compilation from C to assembly language is performed by your choice of gcc or compcert. Strictly speaking, the verification only applies if you use compcert, of course. Anyway, compcert has models for x86, arm, riscv, ppc, and perhaps others. The models are reasonable, especially given that the architecture maintainers (Intel, IBM, etc) do not publish rigorous specs of their ISAs.
Are the models good enough to assure that optimizations will for sure reduce the time of a program? I don't believe so (I don't think compcert gives a timing model). But in principle such work could be done if it had an owner.
Tim Carstens (Feb 08 2022 at 01:01):(Such a model would be relevant for real-time systems, so it is possible someone has published on this topic already)
Karl Palmskog (Feb 08 2022 at 01:30):I thought the "golden model" approved by the maintainers of RISC-V was the one generated [for Coq/Isabelle/etc.] by Sail?
Karl Palmskog (Feb 08 2022 at 01:32):in any case, there seem to be at least three distinct RISC-V models in Coq at the moment, namely, the one in CompCert, https://github.com/mit-plv/riscv-coq and the one from Sail
Karl Palmskog (Feb 08 2022 at 01:33):@Tim Carstens if CertiCoq verification has progressed so much that https://github.com/CertiCoq/certicoq/wiki/The-CertiCoq-pipeline is out of date, please update the wiki page, since this question may come up a lot
Tim Carstens (Feb 08 2022 at 01:54):Riscv is definitely the closest to being foundationally correct. But there is still an important gap: the link between the ISA and compcert’s runtime environment. That gap belongs to the OS people and not the ISA people, I suppose.
The verification status is mostly correct, but it does not account for some of the simplification that occurred when we updated to Coq 8.14. I’ll bring it up in the lab meeting
Karl Palmskog (Feb 08 2022 at 02:10):I don't think the pretty-printing of C(light) code is verified? We were discussing elsewhere of how one would want to compile Coq Clight ASTs directly via CompCert, so as to avoid unverified conversion between to/from C files.
Karl Palmskog (Feb 08 2022 at 02:11):but sure, in the grand scheme of things it's a minor detail. Nevertheless, interesting in a head-to-head CakeML comparison.
Tim Carstens (Feb 08 2022 at 02:56):CakeML is an awesome project, it’s really inspiring
Karl Palmskog (Feb 08 2022 at 02:58):I completely agree at a high level, but the real/CPU time required to bootstrap it [CakeML] is really annoying (like, a day)
Tim Carstens (Feb 08 2022 at 02:58):I’d love to skip the pretty printing phase, and likely we could make that into a supported mode with some relatively minor work
Though one nice thing about the pretty printer is that (I think) it only relies on the open source parts of compcert
Tim Carstens (Feb 08 2022 at 02:59):(Sorry, should have said “free” parts of compcert; the entire thing is open source, of course)
Karl Palmskog (Feb 08 2022 at 03:01):hmm, I think what you said first is correct - there are open source (according to OSI) parts of CompCert, and there are those where "source is available", but not OSI-approved
Tim Carstens (Feb 08 2022 at 03:02):Yes, that’s exactly correct
Tim Carstens (Feb 08 2022 at 03:05):To their credit, their pricing is not outrageous. And as far as I know, they have not done any heavy-handed enforcement of their licensing terms (in contrast to some commercial software vendors, who attack companies and hobbyists alike).
If I were them I would adjust the license somewhat to clarify what they want hobbyists to do, but apart from that critique they’ve been pretty cool imho
Karl Palmskog (Feb 08 2022 at 03:08):the main drawback is the time we habitually spend around here to figure out whether we are in compliance with the license or not, e.g., for clightgen. Same argument as one might have against using "full GPL"
Tim Carstens (Feb 08 2022 at 03:21):I feel like the opam packages could be structured better in this regard. It would be nice to track & separate along that critical issue
Tim Carstens (Feb 08 2022 at 03:22):But I am hopeful that this issue will fade in time for various reasons
Tim Carstens (Feb 08 2022 at 03:22):Though probably not this year
Karl Palmskog (Feb 08 2022 at 03:22):Michael did have separate open source packages for CompCert. But he removed them quite recently, you may want to check with him why
Tim Carstens (Feb 08 2022 at 03:23):Yes, I need to sync up with him on compcert. Him and I were discussing the non-x86 targets last year
Karl Palmskog (Feb 08 2022 at 03:25):we do try to have all opam packages in the Coq opam archive provide an SPDX identifier. This helps license analysis a bit, but we don't have manpower to audit or check compliance.
Karl Palmskog (Feb 08 2022 at 03:26):the main ecosystem licensing issue is arguably not CompCert, but the fact that the quite widely used CECILL-C and CECILL-B are not GPL compatible, which leads to all kinds of trouble...
Karl Palmskog (Feb 08 2022 at 03:28):for example, if you use MathComp + something-full-GPL, you likely are not allowed to distribute your .vo files
Karl Palmskog (Feb 08 2022 at 03:33):but on a more positive note, I hope we can get some packaging for CertiCoq. There is now a career path of sorts for generally useful Coq projects, where they first get packaged (opam/Nix/etc.), then have regular releases and finally join the Platform
Last updated: Feb 06 2023 at 06:29 UTC