Stream: Coq users

Topic: Extraction pipeline inside and outside Coq

Meven Lennon-Bertrand (Apr 24 2022 at 15:05):

As to CertiCoq, it’s currently still somewhat work in progress, but there is a Gallina -> Gallina certified extraction pipeline in MetaCoq, which does all the fancy proof erasure, removes unit-typed arguments to functions, and so on, with a proof that it preserves evaluation. So you should be able to write a program in Gallina, use that extraction phase, then CertiCoq, then CompCert, and get a fully-certified pipeline from Coq down to the metal.

Meven Lennon-Bertrand (Apr 24 2022 at 15:06):

But there is probably less support to add some new functions at each level going down, and still prove these correct…

Karl Palmskog (Apr 24 2022 at 15:08):

I would settle for performing extraction inside Coq itself, to get "regular" functions from all my fancy sigma-type-functions which generate result+proof, but is this possible currently?

Karl Palmskog (Apr 24 2022 at 15:09):

this is something that HOL4 can't do, since the logic can't support sigma types...

Meven Lennon-Bertrand (Apr 24 2022 at 15:11):

It’s definitely on rails! You’d have to ask @Matthieu Sozeau or @Yannick Forster for the exact state of the formalization, but if it’s not there yet it is going to be very soon.

Karl Palmskog (Apr 24 2022 at 15:17):

but just so we are talking about the same thing. Let's say I have this type:

Definition accept_t (rs : r char * list char) : Type :=
{ accept_p rs }+{ ~ accept_p rs }.

where r is a regexp and accept_p means the given sequence is in the language defined by r. And now I define:

Equations acc (rs : r char * list char) : accept_t rs by wf rs (* ... *) :=  (* ... *)

Does this mean I can get a version acc_ex of acc which returns only, say, Left or Right, and a generated proof that acc and acc_ex are related?

Meven Lennon-Bertrand (Apr 24 2022 at 15:21):

Not exactly, because most of this lives at the meta-level.
Or rather, your definition would be reified to some inhabitant of the type term as defined in MetaCoq, and you can then run extraction on that, to get another term in an AST that has a special box constructor, and all the propositional content is transformed to that box constructor.

Meven Lennon-Bertrand (Apr 24 2022 at 15:22):

I don’t think there is support yet to unquote that extracted term back to Coq, but up to mapping box to unit this should not be too hard (there’s already an unquoting for the standard AST).

Karl Palmskog (Apr 24 2022 at 15:24):

OK, at the moment, I think I would settle for a version I can run that doesn't have the propositional content. The main drawback of sigma-types is arguably that they can't be efficiently computed with inside Coq when proofs are big.

Meven Lennon-Bertrand (Apr 24 2022 at 15:24):

But even if unquoting was there, this does not give you a proof term acc_rel relating acc to the unquoted erasure (your acc_ex). This is because that proof currently lives at the meta-level.

Karl Palmskog (Apr 24 2022 at 15:25):

but can't I do some trick to propagate the meta-level proof for my instance?

Meven Lennon-Bertrand (Apr 24 2022 at 15:25):

Karl Palmskog said:

OK, at the moment, I think I would settle for a version I can run that doesn't have the propositional content. The main drawback of sigma-types is arguably that they can't be efficiently computed with inside Coq when proofs are big.

Then I think that we are not too far from having a command MetaCoq extract acc into acc_rel. that generates acc_rel.

Meven Lennon-Bertrand (Apr 24 2022 at 15:27):

Karl Palmskog said:

but can't I do some trick to propagate the meta-level proof for my instance?

I am not completely sure, because that meta-level proof is really about evaluation, and since everything in Coq is up-to conversion, I think it would be hard to state.

Karl Palmskog (Apr 24 2022 at 15:27):

I think I could live with adding the meta level proof as an axiom, if I at least knew exactly what the property looked like

Meven Lennon-Bertrand (Apr 24 2022 at 15:27):

If acc and acc_rel were both booleans, then the property would say that this must be the same boolean

Meven Lennon-Bertrand (Apr 24 2022 at 15:28):

Same goes for any hereditarily inductive type

Meven Lennon-Bertrand (Apr 24 2022 at 15:28):

If you get to functions, things get hairier, I guess some fashion of parametricity enters the game

Meven Lennon-Bertrand (Apr 24 2022 at 15:29):

But I guess in your case you would probably get something like "the two functions take equal inputs to either both left or both right".

Karl Palmskog (Apr 24 2022 at 15:30):

all the functions I'm interested in to extract inside Coq either return sumbool or sig. For sumbools I guess one just wants a version that instead returns sum or bool, and for sig it should be obvious, just throw out the exist

Meven Lennon-Bertrand (Apr 24 2022 at 15:32):

I am not completely sure how this would fare if you have also sig as inputs, but yeah, that should be the spec

Meven Lennon-Bertrand (Apr 24 2022 at 15:35):

And as to generating the proof, now that I think about it I am not even completely sure how this would do, because those really are on the syntax of your terms, something that does not even make sense in Coq (again, everything you can express is up to conversion)

Meven Lennon-Bertrand (Apr 24 2022 at 15:36):

Plus, there’s 100k lines of Coq proving confluence, subject reduction and whatnot before you can get to the proof you are into. Not sure how to account for that

Meven Lennon-Bertrand (Apr 24 2022 at 15:37):

(deleted)

Karl Palmskog (Apr 24 2022 at 15:37):

for some context, there was the advice here to never use sigma types, since they don't compute well: https://www.cs.princeton.edu/~appel/papers/ecosystem.pdf

However, I think MetaCoq could rehabilitate them a bit, but I guess meta questions abound.

Karl Palmskog (Apr 24 2022 at 15:38):

I spun off the topic a bit so as to hopefully avoid some confusion

Meven Lennon-Bertrand (Apr 24 2022 at 15:41):

Yes, I think once the proofs have matured a bit we can think about what we want to do with them, and indeed think about all the meta-stuff…

Meven Lennon-Bertrand (Apr 24 2022 at 15:44):

As for sigma-types, maybe extraction inside of Coq is a solution, but there might be others: a good notion of opaqueness would probably help, and maybe replacing Prop by strict propositions might also be helpful to ensure proofs are really irrelevant and can be safely ignored

Paolo Giarrusso (Apr 24 2022 at 15:46):

naive question: is conversion really such a big problem? Maybe it complicates stating what we want, but I’m not even sure how…

Meven Lennon-Bertrand (Apr 24 2022 at 15:46):

I don’t know, but you can’t really formulate in Coq "this term t reduces to a t' such that…"

Meven Lennon-Bertrand (Apr 24 2022 at 15:47):

Ofc you can replace that by propositional equality, but t = t' is much weaker

Paolo Giarrusso (Apr 24 2022 at 15:48):

exactly — probably something like erase_result (original_function inputs) = erased_function (erase_inputs inputs)

Paolo Giarrusso (Apr 24 2022 at 15:49):

probably a logical relation is needed, so that “=“ becomes “maps equal inputs to equal outputs” etc as appropriate

Karl Palmskog (Apr 24 2022 at 15:50):

yes, for many use cases "extensional equivalence" is enough to get work done

Meven Lennon-Bertrand (Apr 24 2022 at 15:50):

Yeah, maybe that would work, plus the knowledge that by canonicity if b = true then b actually evaluates to true

Paolo Giarrusso (Apr 24 2022 at 15:50):

and “propositional equality is weaker” seems only half-true. Internally, you cannot even state anything that you’d lose. Externally, I’d think the generic metatheory lets you recover everything you might want.

Meven Lennon-Bertrand (Apr 24 2022 at 15:50):

Yep, fair enough

Meven Lennon-Bertrand (Apr 24 2022 at 15:51):

Maybe I’m too pessimistic :)

Paolo Giarrusso (Apr 24 2022 at 15:51):

yeah that use of canonicity is an example, there could be more.

Meven Lennon-Bertrand (Apr 24 2022 at 15:52):

So maybe we can hope to have MetaCoq Extract foo to foo_ex related by foo_rel. with foo_rel mirroring the result of the meta-proof!

Meven Lennon-Bertrand (Apr 24 2022 at 15:53):

That would be really neat indeed

Meven Lennon-Bertrand (Apr 24 2022 at 15:54):

Meven Lennon-Bertrand said:

As for sigma-types, maybe extraction inside of Coq is a solution, but there might be others: a good notion of opaqueness would probably help, and maybe replacing Prop by strict propositions might also be helpful to ensure proofs are really irrelevant and can be safely ignored

Ok, these are exactly the two solutions proposed in the paper :grinning:

Paolo Giarrusso (Apr 24 2022 at 15:55):

Just to take apart my argument that won’t cover, e.g., execution traces or computational complexity (but you can’t just talk about those internally); does this cover normalization on open inputs?

Karl Palmskog (Apr 24 2022 at 15:55):

let's be real: regular Coq users are not going to jump into using SProp anytime soon, especially with lacking library support

Karl Palmskog (Apr 24 2022 at 15:57):

I don't know if opaqueness related stuff are also going to change anytime soon for Coq itself?

Karl Palmskog (Apr 24 2022 at 15:57):

SProp is great, but MetaCoq Extract foo to foo_ex related by foo_rel. would apply to millions of lines of Coq already written

Meven Lennon-Bertrand (Apr 24 2022 at 15:58):

Paolo Giarrusso said:

does this cover normalization on open inputs?

You mean, the current proof in MetaCoq?

Karl Palmskog (Apr 24 2022 at 16:00):

I meant more like: if you implement the command (possibly via the current proof in MetaCoq), it could be run in practice on a ton of code

Karl Palmskog (Apr 24 2022 at 16:01):

in contrast to using SProp, which appears to require structural changes (compared to regular Prop idioms) to apply well

Meven Lennon-Bertrand (Apr 24 2022 at 16:02):

For sure, we are very far from a good integration of SProp on so many levels… Even before adapting libraries, already the higher layers of Coq are completely broken on it currently

Paolo Giarrusso (Apr 24 2022 at 16:03):

this command would also let you compute past irrelevant Prop axioms etc? We had discussed here how to do this with PMP, but extraction would be more powerful

Paolo Giarrusso (Apr 24 2022 at 16:04):

re SProp, the only attempt to use it I’ve seen close got reverted for performance regressions (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/322)

Meven Lennon-Bertrand (Apr 24 2022 at 16:05):

Paolo Giarrusso said:

this command would also let you compute past irrelevant Prop axioms etc? We had discussed here how to do this with PMP, but extraction would be more powerful

Now that you say it, I’m not sure exactly what would be the computational behaviour of such a thing

Meven Lennon-Bertrand (Apr 24 2022 at 16:06):

In particular, erasure might get rid of proofs of termination, and so the extracted term might be non-terminating

Paolo Giarrusso (Apr 24 2022 at 16:07):

But you did say Gallina -> Gallina?

Meven Lennon-Bertrand (Apr 24 2022 at 16:07):

So I might have been too eager when saying you could unquote back by just mapping box to unit…

Meven Lennon-Bertrand (Apr 24 2022 at 16:08):

Actually, it takes a Gallina term to a language with one extra primitive (box), representing all that’s been erased

Paolo Giarrusso (Apr 24 2022 at 16:09):

So Acc erases to box, but operations on box are axiomatized?

Meven Lennon-Bertrand (Apr 24 2022 at 16:10):

Actually, I don’t know exactly what happens

Meven Lennon-Bertrand (Apr 24 2022 at 16:10):

The Ast is here

Paolo Giarrusso (Apr 24 2022 at 16:10):

Either way, it makes some sense; for Gallina to Gallina, you might not be able to erase subsingletons (at least Acc) as you’d do when erasing to non-Gallina…

Gaëtan Gilbert (Apr 24 2022 at 16:11):

Paolo Giarrusso said:

re SProp, the only attempt to use it I’ve seen close got reverted for performance regressions (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/322)

did the perf issue ever get investigated?

Meven Lennon-Bertrand (Apr 24 2022 at 16:12):

Yes, I’m not sure exactly how elimination of former Prop inductives (eg equality and acc) is treated, but there’s probably something hidden there

Paolo Giarrusso (Apr 24 2022 at 16:12):

https://github.com/MetaCoq/metacoq/blob/d012c811048fafb3ef81cd6dcf6066fc7326e9e7/erasure/theories/EWcbvEval.v#L113

Paolo Giarrusso (Apr 24 2022 at 16:13):

https://github.com/MetaCoq/metacoq/blob/d012c811048fafb3ef81cd6dcf6066fc7326e9e7/erasure/theories/EWcbvEval.v#L86

Meven Lennon-Bertrand (Apr 24 2022 at 16:13):

Like, we know the extracted term should be terminating because it is related to the original one that we know to be terminating, but all information as to why the term is indeed terminating is erased, so probably that erased term would not be typeable in Coq without some hackery

Paolo Giarrusso (Apr 24 2022 at 16:14):

also dunno how it’s used, but that reduction relation is not Gallina’s :-(

Meven Lennon-Bertrand (Apr 24 2022 at 16:14):

Yes, it’s weak-call-by-value

Meven Lennon-Bertrand (Apr 24 2022 at 16:14):

And indeed a hard part of the proof is to relate that strategy to iterated weak-head normalization

Paolo Giarrusso (Apr 24 2022 at 16:15):

that’s legal for gallina, but my links suggest it does reduce through box instead of getting stuck.

Meven Lennon-Bertrand (Apr 24 2022 at 16:15):

Yep, I just looked at it and it’s definitely not something you could get in vanilla Gallina

Meven Lennon-Bertrand (Apr 24 2022 at 16:16):

I over-sold this, sorry about it :grimacing:

Karl Palmskog (Apr 24 2022 at 16:17):

even getting lots of boxes would be an improvement compared to waiting minutes just to compute some Prop stuff

Meven Lennon-Bertrand (Apr 24 2022 at 16:17):

Probably the best you could get is something like MetaCoq erase_and_compute foo.

Paolo Giarrusso (Apr 24 2022 at 16:18):

alternatively, not easy, but could one plug in some partiality monad to fix the termination problem?

Meven Lennon-Bertrand (Apr 24 2022 at 16:20):

Mmmmmmm… I’m not sure: if you really want the extracted term back to Gallina, you’d need some termination witness. But if you’re getting rid of acc, that’s exactly what you erased in the first place?

Meven Lennon-Bertrand (Apr 24 2022 at 16:20):

I’m not an expert of the termination fiddling, so maybe there’s a trick there

Paolo Giarrusso (Apr 24 2022 at 16:21):

I mean, Partial Int would represent a monadic computation that gives an Int or diverges — because of infinite loops, or because some cast failed.

Paolo Giarrusso (Apr 24 2022 at 16:22):

if you obtain it by erasing an Int expression, you have a metalevel proof that your Partial Int always succeeds, without a way to internalize it. But it might be appropriate sometimes?

Paolo Giarrusso (Apr 24 2022 at 16:24):

No I don’t have a good use-case — and I don’t know a generic translation to this, I only have partial ideas for eq and Acc.

Paolo Giarrusso (Apr 24 2022 at 16:24):

@Gaëtan Gilbert not AFAICT

Paolo Giarrusso (Apr 24 2022 at 16:25):

among other signs, the tracking issue is https://gitlab.mpi-sws.org/iris/stdpp/-/issues/85 and has nothing.

Meven Lennon-Bertrand (Apr 24 2022 at 16:25):

There’s another issue: take a function foo (b : {b' : bool | b' = true} : unit which uses the proof of equality for termination. Then you’d erase this to some foo' : bool -> unit, but now you can feed it false and get a diverging computation, because this is not in the fragment related to the original function

Paolo Giarrusso (Apr 24 2022 at 16:28):

So not just casts: any erased equality would have to become a runtime test :-(

Meven Lennon-Bertrand (Apr 24 2022 at 16:29):

I think you’d see this the moment you try to eliminate your equality, which you could replace with a cast?

Paolo Giarrusso (Apr 24 2022 at 16:30):

Yep

Meven Lennon-Bertrand (Apr 24 2022 at 16:30):

(But in the sense of a cast that can fail, and you’re getting pretty close to gradual typing)

Paolo Giarrusso (Apr 24 2022 at 16:30):

Anyway, at best, erased_function (erase_inputs inputs) = return (erase_result (original_function inputs)) could still hold in principle, but it’d take a much more complex translation if it exists, so I’ll stop speculating. EraseAndCompute seems nicer.

Meven Lennon-Bertrand (Apr 24 2022 at 16:30):

Which is yet another can of worms

Paolo Giarrusso (Apr 24 2022 at 16:36):

Wait, which can of worms? EraseAndCompute?? Oh, must be gradual typing...

Notification Bot (Apr 24 2022 at 16:40):

Meven Lennon-Bertrand has marked this topic as resolved.

Notification Bot (Apr 24 2022 at 16:40):

Meven Lennon-Bertrand has marked this topic as unresolved.

Matthieu Sozeau (Apr 25 2022 at 09:21):

Paolo Giarrusso said:

Anyway, at best, erased_function (erase_inputs inputs) = return (erase_result (original_function inputs)) could still hold in principle, but it’d take a much more complex translation if it exists, so I’ll stop speculating. EraseAndCompute seems nicer.

On (closed) terms of first-order inductive type (i.e no proofs or types should appear in the return value), you do get a meta-proof of that, but indeed it's talking about erased terms which you can't really manipulate. I think a better interface for using MetaCoq's erasure would be to have a new conversion test (certicoq_compute) that checks that the conversion problem falls into the precondition of erasure (closed, first-order inductive value) and calls erasure+evaluation to get to a constructor on both sides of the conversion problem and check that they are equal.

Last updated: Sep 23 2023 at 08:01 UTC