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?
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
This topic was moved here from #Coq users > CertiCoq processor by Karl Palmskog
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
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.
(Such a model would be relevant for real-time systems, so it is possible someone has published on this topic already)
I thought the "golden model" approved by the maintainers of RISC-V was the one generated [for Coq/Isabelle/etc.] by Sail?
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
@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
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
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.
but sure, in the grand scheme of things it's a minor detail. Nevertheless, interesting in a head-to-head CakeML comparison.
CakeML is an awesome project, it’s really inspiring
I completely agree at a high level, but the real/CPU time required to bootstrap it [CakeML] is really annoying (like, a day)
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
(Sorry, should have said “free” parts of compcert; the entire thing is open source, of course)
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
Yes, that’s exactly correct
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
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"
I feel like the opam packages could be structured better in this regard. It would be nice to track & separate along that critical issue
But I am hopeful that this issue will fade in time for various reasons
Though probably not this year
Michael did have separate open source packages for CompCert. But he removed them quite recently, you may want to check with him why
Yes, I need to sync up with him on compcert. Him and I were discussing the non-x86 targets last year
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.
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...
for example, if you use MathComp + something-full-GPL, you likely are not allowed to distribute your
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