How far are we from getting this using MetaCoq? https://cakeml.org/candle/index.html
I'm not sure exactly what you mean?
Implementing hol light in a verified version of gallina...
or implementing the whole Coq in gallina?
or Coq in SML?
All seem a light year away to me, and not super interesting either
I'm interpreting the question as "How far away are we from having an executable which is verified all the way down and feels like a Coq REPL". Then one possible answer is: We need (1) verified extraction to OCaml (working on it!), (2) a verified compiler from OCaml to assembly, and (3) make MetaCoq powerful enough s.t. the verified type checker can type check itself (i.e. support some more things, amongst them modules)
(1) is a realistic project (I hope), (2) is very hard and time-consuming, (3) is conceivable, but nobody is working on e.g. modules at the moment as far as I know
"all the way down" but no hardware verification?
I think that would be the meaning of "all the way down" applying to the Candle project, so yes, in this case we could also interpret it excluding hardware verification
I meant basically what Yannick said, i.e., how can one get end-to-end verified interaction with the MetaCoq checker (and check itself, etc.)
I'm waiting for the verified camlp5 parser : -)
Anyway good luck with extraction, that alone woud be a leap forward for our TCB
we are also waiting for some CertiCoq proofs, verified extraction should be orthogonal to that?
Right, yes, indeed, I forgot :) It doesn't matter which route to an executable you take
I got distracted by the "in CakeML" part
well, it matters at hardware level, arguably
if you go CertiCoq, you will get to ISA level via CompCert
I think verified extraction will not verify an OCaml compiler, so you get to an abstract semantics for (a part of) OCaml? And then trust ocamlc and friends.
the Lightbulb system verification by Chlipala's team went further [down to silicon], but they elided both OCaml and CompCert altogether.
(I'm not sure other groups will be able to reuse their tooling, though)
Actually, (3) from above is just nice to have. We could relatively soon have a verified REPL (without any support for tactics, without a parser) which supports a small fragment of Coq, most notably it cannot typecheck various parts of its own implementation
I don't think we'll need the whole module system to extract MetaCoq's safechecker.
Or to typecheck it
Just for my understanding: are there known reasons why CertiCoq could not be used for such a project? Would this cover (1) and (2) above so that just (3) remains?
I think it should handle 1 and 2 indeed
We already have a verified erasure and compilation down to ASM from it, I think it's not necessary to go through ocaml at all.
Now having said that, efficient type-checking might require clever data structures that we are not using yet. We're only starting to see what we need to abstract away in MetaCoq's formalization so that it can be implemented efficiently (e.g. the graph of universe constraints)
I am looking forward to it :-) Even if it would be 1000x slower than coqc it would be useful in practice. One works interactively with Coq, so there can be a large speed difference between interactive work with coqc/coqtop and offline proof checking over the weekend.
Yep, hopefully we can bring it down to 10x slower in the common case. In principle, we could also implement yet another checker in VST and show that it simulates the verified one and use all kind of clever tricks to speed it up :)
Of course speed doesn't hurt, but I don't think it is essential for such a project. What I would find more important than the constant average speed factor is that there is nothing which leads to say an exponential blow up compared to normal coq.
Does “no exponential blowup” mean you need hash-consing in Gallina?
I think we're comparing the extracted checker from MetaCoq (in OCaml) and Coq's kernel, so that wouldn't require hash-consing in Gallina itself
I don't think we introduced any exponential blowup, but our datastructures are very naive for now.
but how would the extracted checker implement hash-consing if the Gallina code doesn't? I guess you'd write the hash-consing primitives in OCaml, even if that extends the TCB?
Ah, maybe that's what you meant with "abstract away in MetaCoq's formalization so that it can be implemented efficiently"
Ah, my bad, if we need hash-consing in the extracted code, then indeed we have to devise a way to make it appear at the Gallina level
coqchk doesn't use hashconsing at all, and I don't see why a metacoq checker should either if you don't implement anything else than the kernel
it becomes interesting when there are upper layers generating huge terms over which there is no control and a lot of duplication
otherwise if you feed to the checker explicit
constr it's the responsibility of the caller to make it fit in memory
coqchk doesn't use hashconsing at all
but coqc did the hashconsing
when translating ocaml constr to metacoq constr sharing is broken if you don't re-hashcons
but this is outside of the TCB anyways
I mean, this is going to be an OCaml shim so you can be clever with pointers there
Indeed, all sharing is lost by the first translation.
You're talking about the template-to-pcuic one?
if so I'm not sure that this one is so problematic, assuming that the constr-to-template preserves sharing
from my experience, hashconsing is not so much important for the structure of the term than for the leaves
typically, the critical part is hashconsing of constants / inductives
and template-to-pcuic doesn't touch that one
You mean hashconsing of the references to constants and inductives in mkConst and mkInd then?
Well, there is first a phase from Coq's AST to template, that might need to be tweaked a bit to preserve sharing of these references
What I meant is that it wouldn't be nice if a MetaCoq based checker couldn't handle things coqc can handle with say 100x the time (on average for large projects, individual files could be slower) and say 4x or 8x the memory. This doesn't seem to be true for coqchk. E.g. when I last tried (about 4 years back) coqchk could not handle CompCert on a machine with 128 GB RAM (afair I even tried 768 GB or 1.5TB RAM) while coqc can handle CompCert on a machine with 4 GB RAM (all single threaded make).
IIRC CompCert's issue is that it uses a vm_compute that cannot be tractably replaced by standard conversion.
Why would this be so? I understand that it will get slower but why would it need 100x more memory?
It could be so because the standard conversion takes a different path of reduction that is hopeless I guess. But I don't remember exactly.
IIRC compcert was an issue with coqchk defunctorializing, not vm (or maybe in addition to vm)
@Gaëtan Gilbert : "defunctorializing" means deep unfolding of module functors?
@Matthieu Sozeau : so you are saying that the reduction algorithm implemented by
vm_compute is infeasible to implement in MetaCoq?
No, that we could do, at least in principle.
I mean if you have
Module F(A:T). Definition bla := fun x : A.t => x. End F. Module M := F X.
it will check
M.bla := fun x : X.t => x
Last updated: Jun 01 2023 at 12:01 UTC