Stream: MetaCoq

Topic: MetaCoq for AST generation


view this post on Zulip Karl Palmskog (Aug 16 2023 at 15:11):

It seems a lot of people are writing "ad-hoc" tools that generate Coq code as .v files with some AST they need, like converting a program-as-a-string into the corresponding Coq AST term. The most famous example might be CompCert's clightgen.

Just to double check, surely it would make more sense for people to now write these tools inside Coq using Template-Coq? This would at a minimum avoid having to keep up with changes to .v syntax, right?

view this post on Zulip Pierre-Marie Pédrot (Aug 16 2023 at 15:13):

It's unclear to me what's the stablest approach. The internal AST of Coq kernel term does change from time to time, and probably more so than the Gallina syntax. The vernacular command syntax in general is less stable but I'm not sure this is relevant for this use case.

view this post on Zulip Karl Palmskog (Aug 16 2023 at 15:15):

but let's say you instead of generating .v you go from string to sexp, and then put the sexp inside Coq, and use Template-Coq on the sexp-inside-Coq. Isn't this theoretically more robust for the long term (than maintaining .v generation)?

view this post on Zulip Pierre-Marie Pédrot (Aug 16 2023 at 15:20):

I'd personally withhold my judgement until acquiring actual evidence of purported robustness. Scripts generating v files are not the major point of failure in this scenario.

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 15:42):

Can template-coq run elaboration now? IIUC from Gregory, a while ago you had to create elaborated terms including universes.

view this post on Zulip Yannick Forster (Aug 16 2023 at 15:44):

No elaboration, but you do not have to annotate universes anymore

view this post on Zulip Karl Palmskog (Aug 16 2023 at 15:48):

it seems to me there would be some TCB reduction if all you need to do is write a string-to-sexp tool outside Coq for your language, since the sexp-to-AST-term part using Template-Coq could be reasoned about (right?)

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 15:52):

Actually, what's the string-to-sexp intended to be? In clightgen's case, is the "string" the C program?

view this post on Zulip Yannick Forster (Aug 16 2023 at 15:56):

Karl Palmskog said:

since the sexp-to-AST-term part using Template-Coq could be reasoned about (right?)

You could reason about it, yes. But what would a statement you'd like to prove look like?

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 15:57):

It seems most concerns are about the part outside of Coq — whether it outputs a s-exp or a Coq term, what's the difference?

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 15:58):

One I see is extra (buggy) intermediate steps, people writing proofs cannot inspect the .v file any more, nor can build tools cache the .vo output as easily.

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 16:00):

Right now, in the case of bedrock's brick, building ASTs takes around 20% of our build time, and inspecting ASTs in source form is occasionally useful. Bricks AST is a Coq map, using Print on a Coq map, OTOH, typically isn't as informative.

view this post on Zulip Karl Palmskog (Aug 16 2023 at 16:35):

I was thinking one could use printing-only notations like for Clight in VST to inspect generated AST terms

view this post on Zulip Karl Palmskog (Aug 16 2023 at 16:37):

property would be something like: assuming this sexp abstractly represents a valid AST, this is the AST-as-Coq-term I get from the function inside Coq

view this post on Zulip Karl Palmskog (Aug 16 2023 at 16:39):

Paolo Giarrusso said:

Actually, what's the string-to-sexp intended to be? In clightgen's case, is the "string" the C program?

The closest equivalent for this is CakeML, which has a parser which both accepts a program as a string and a program as a sexp

view this post on Zulip Karl Palmskog (Aug 16 2023 at 16:39):

the sexp representation is nice because it can be exported to inside HOL4

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 19:06):

IIUC, this makes a difference if you trust your external program to generate the correct sexp, but not to generate the correct .v file, and/or you do not trust Coq elaboration or its use by generated code?

view this post on Zulip Karl Palmskog (Aug 16 2023 at 22:56):

in a bunch of projects, content of some source file needs to added into Coq as a bunch of AST term definitions. Rather than writing a new custom clightgen every time, seems better to use sexps or similar as an exchange format. Parse the source into the intermediate format, use generalized clightgen tool for that format, write the rest inside Coq.

view this post on Zulip Karl Palmskog (Aug 16 2023 at 23:00):

everything can be mistrusted, but making the clightgen analogue generic, one is at least not starting from scratch with trust every time

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 23:43):

In this setup, you might consider writing the sexp->value parser as a Coq function rather than metafunction

view this post on Zulip Karl Palmskog (Aug 16 2023 at 23:46):

you mean just defining a bunch of strings (holding the sexps) as Coq constants, and then actually running a parser inside Coq on those strings? Seems like that has the possibility to be really slow.

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 23:48):

I thought you wanted to do the same, but running the Gallina parser in metacoq — what makes that faster?

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 23:49):

There's one bit of metaprogramming, but it's just Definition AST := Eval vm_compute (parser input).

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 23:57):

but okay, that only works for generating data in one (or few) data structures, not to generate Coq constants or notations.

view this post on Zulip Jason Gross (Aug 17 2023 at 03:59):

If running the parser in vm_compute is too slow, you can have a workflow where you do something like Definition prog : TemplateMonad.Extractable.TM unit := parser input., then you do Recursive Extraction prog., and then you compile and link the resulting ml file as a Coq plugin, which will then add the definitions when loaded (hopefully only once?). But the plugin shim needed to support this should be pretty small. And you can always run it in vm_compute + MetaCoq Run if you want a smaller TCB. (Or you could eventually use MetaCoq's proven extraction, once it's ready.)

view this post on Zulip Jason Gross (Aug 17 2023 at 04:04):

Probably the strongest theorem you might want to prove, if you stick the parser in Coq, is that you write some pretty-printer on an intermediate format (something that losslessly encodes the original input but also has a trivial forgetful surjection onto the datastructure you plan to prove theorems about), and then you prove that pretty-print and parse round-trip in both directions.

view this post on Zulip Karl Palmskog (Aug 17 2023 at 07:11):

I guess vm_compute might be fast enough. Doing the plugin thing sounds like more pain than it's worth...


Last updated: Jul 23 2024 at 21:01 UTC