Stream: MetaCoq

Topic: REPL for MetaCoq?


view this post on Zulip Karl Palmskog (Feb 10 2022 at 16:10):

How far are we from getting this using MetaCoq? https://cakeml.org/candle/index.html

view this post on Zulip Théo Winterhalter (Feb 10 2022 at 16:29):

I'm not sure exactly what you mean?

view this post on Zulip Enrico Tassi (Feb 10 2022 at 16:34):

Implementing hol light in a verified version of gallina...

view this post on Zulip Enrico Tassi (Feb 10 2022 at 16:35):

or implementing the whole Coq in gallina?

view this post on Zulip Enrico Tassi (Feb 10 2022 at 16:38):

or Coq in SML?

view this post on Zulip Enrico Tassi (Feb 10 2022 at 16:40):

All seem a light year away to me, and not super interesting either

view this post on Zulip Yannick Forster (Feb 10 2022 at 16:42):

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)

view this post on Zulip Yannick Forster (Feb 10 2022 at 16:43):

(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

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 16:44):

"all the way down" but no hardware verification?

view this post on Zulip Yannick Forster (Feb 10 2022 at 16:47):

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

view this post on Zulip Karl Palmskog (Feb 10 2022 at 16:52):

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.)

view this post on Zulip Enrico Tassi (Feb 10 2022 at 16:56):

I'm waiting for the verified camlp5 parser : -)

view this post on Zulip Enrico Tassi (Feb 10 2022 at 17:20):

Anyway good luck with extraction, that alone woud be a leap forward for our TCB

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:22):

we are also waiting for some CertiCoq proofs, verified extraction should be orthogonal to that?

view this post on Zulip Yannick Forster (Feb 10 2022 at 17:24):

Right, yes, indeed, I forgot :) It doesn't matter which route to an executable you take

view this post on Zulip Yannick Forster (Feb 10 2022 at 17:25):

I got distracted by the "in CakeML" part

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:25):

well, it matters at hardware level, arguably

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:26):

if you go CertiCoq, you will get to ISA level via CompCert

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:27):

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.

view this post on Zulip Yannick Forster (Feb 10 2022 at 17:27):

Yes, exactly

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:29):

the Lightbulb system verification by Chlipala's team went further [down to silicon], but they elided both OCaml and CompCert altogether.

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:30):

(I'm not sure other groups will be able to reuse their tooling, though)

view this post on Zulip Yannick Forster (Feb 10 2022 at 17:30):

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

view this post on Zulip Matthieu Sozeau (Feb 10 2022 at 17:32):

I don't think we'll need the whole module system to extract MetaCoq's safechecker.

view this post on Zulip Matthieu Sozeau (Feb 10 2022 at 17:32):

Or to typecheck it

view this post on Zulip Michael Soegtrop (Feb 10 2022 at 17:32):

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?

view this post on Zulip Matthieu Sozeau (Feb 10 2022 at 17:33):

I think it should handle 1 and 2 indeed

view this post on Zulip Matthieu Sozeau (Feb 10 2022 at 17:34):

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.

view this post on Zulip Matthieu Sozeau (Feb 10 2022 at 17:36):

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)

view this post on Zulip Michael Soegtrop (Feb 10 2022 at 17:59):

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.

view this post on Zulip Matthieu Sozeau (Feb 11 2022 at 19:41):

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 :)

view this post on Zulip Michael Soegtrop (Feb 11 2022 at 20:41):

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.

view this post on Zulip Paolo Giarrusso (Feb 11 2022 at 23:44):

Does “no exponential blowup” mean you need hash-consing in Gallina?

view this post on Zulip Matthieu Sozeau (Feb 14 2022 at 14:51):

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

view this post on Zulip Matthieu Sozeau (Feb 14 2022 at 14:51):

I don't think we introduced any exponential blowup, but our datastructures are very naive for now.

view this post on Zulip Paolo Giarrusso (Feb 14 2022 at 15:20):

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?

view this post on Zulip Paolo Giarrusso (Feb 14 2022 at 15:22):

Ah, maybe that's what you meant with "abstract away in MetaCoq's formalization so that it can be implemented efficiently"

view this post on Zulip Matthieu Sozeau (Feb 14 2022 at 19:05):

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

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:07):

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

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:07):

it becomes interesting when there are upper layers generating huge terms over which there is no control and a lot of duplication

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:08):

otherwise if you feed to the checker explicit constr it's the responsibility of the caller to make it fit in memory

view this post on Zulip Gaëtan Gilbert (Feb 14 2022 at 19:11):

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

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:14):

but this is outside of the TCB anyways

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:15):

I mean, this is going to be an OCaml shim so you can be clever with pointers there

view this post on Zulip Matthieu Sozeau (Feb 14 2022 at 19:37):

Indeed, all sharing is lost by the first translation.

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:42):

You're talking about the template-to-pcuic one?

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:42):

if so I'm not sure that this one is so problematic, assuming that the constr-to-template preserves sharing

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:43):

from my experience, hashconsing is not so much important for the structure of the term than for the leaves

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:43):

typically, the critical part is hashconsing of constants / inductives

view this post on Zulip Pierre-Marie Pédrot (Feb 14 2022 at 19:44):

and template-to-pcuic doesn't touch that one

view this post on Zulip Matthieu Sozeau (Feb 14 2022 at 21:48):

You mean hashconsing of the references to constants and inductives in mkConst and mkInd then?

view this post on Zulip Matthieu Sozeau (Feb 14 2022 at 21:49):

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

view this post on Zulip Michael Soegtrop (Feb 15 2022 at 09:01):

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).

view this post on Zulip Matthieu Sozeau (Feb 15 2022 at 09:47):

IIRC CompCert's issue is that it uses a vm_compute that cannot be tractably replaced by standard conversion.

view this post on Zulip Michael Soegtrop (Feb 15 2022 at 10:01):

Why would this be so? I understand that it will get slower but why would it need 100x more memory?

view this post on Zulip Matthieu Sozeau (Feb 15 2022 at 12:45):

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.

view this post on Zulip Gaëtan Gilbert (Feb 15 2022 at 12:46):

IIRC compcert was an issue with coqchk defunctorializing, not vm (or maybe in addition to vm)

view this post on Zulip Michael Soegtrop (Feb 15 2022 at 13:06):

@Gaëtan Gilbert : "defunctorializing" means deep unfolding of module functors?

view this post on Zulip Michael Soegtrop (Feb 15 2022 at 13:08):

@Matthieu Sozeau : so you are saying that the reduction algorithm implemented by vm_compute is infeasible to implement in MetaCoq?

view this post on Zulip Matthieu Sozeau (Feb 15 2022 at 13:09):

No, that we could do, at least in principle.

view this post on Zulip Gaëtan Gilbert (Feb 15 2022 at 13:10):

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: Aug 11 2022 at 02:03 UTC