Stream: Coq users

Topic: Soliciting feedback on kernel reduction primitives


view this post on Zulip Janno (Oct 10 2023 at 10:52):

BedRock Systems has been working on a Coq feature that allows fine-grained control over reduction during typechecking: https://github.com/coq/coq/pull/17839/. The PR is still in progress but it contains a design that we expect to be already quite useful to many people who have struggled with controlling reduction, e.g. having to maintain whitelists for calls to reduction tactics (usually in proofs by reflection) as well as slow Qed performance with computation-heavy function types.
The MR contains a description of the new primitives and also two examples of proofs by reflection using the new primitives (truelysimpl.v and realsimpl.v, the latter being a port of an example from the Metaprogramming Rosetta Stone which serves as very nice point of comparison). There is also a comment in the MR that shows how the MR allows to maintain sharing that is otherwise lost when typechecking repeated applications of functions whose types contain expensive computation.
There are countless open GitHub issues and even here on zulip there have been many questions related to reduction and Qed performance. We are hoping that some users affected by these problems would be willing to talk to us, describe their specific pain points, and work with us to see if our design can help address these issues. The following is a list of people that come to mind immediately but anyone suffering from these issues is welcome to respond (or send me a DM): @Jason Gross, @Michael Soegtrop, @Andres Erbsen, @Robbert Krebbers

/cc @Gregory Malecha, @Rodolphe Lepigre

view this post on Zulip Robbert Krebbers (Oct 11 2023 at 15:08):

We discussed in private with Janno and Rodolph. Based on that, Rodolph updated truelysimpl.v in the PR with comments. That might also be useful for others.

It seems this feature can be very useful in Iris to perform the computations of Iris Proof Mode environments. We need to figure out where to put the right uses of block and run once someone has the time for that :).

One thing that came up in our discussion is that vm_compute is not supported, and it might be very difficult to support. That is probably fine, but it's important to document that and give a clear error message.

view this post on Zulip Karl Palmskog (Oct 11 2023 at 15:10):

does this stuff increase the TCB in any way? Not sure I will use the new functionality, but it will have to be implemented in coqchk as well, no? (So non-users may have to "pay" in some sense)

view this post on Zulip Janno (Oct 11 2023 at 15:39):

Just to be extra precise here: vm_compute is currently not supported right now because it is missing code. It will likely never have special treatment for the new primitives, i.e. it is probably never going to stop reduction under block, but it will otherwise behave reasonably.

view this post on Zulip Janno (Oct 11 2023 at 15:46):

does this stuff increase the TCB in any way?

I am not an expert on that side of things but I'll try to answer:I think the change is technically an extension to the theory because we are extending coq with new primitive values. However, these primitives are treated as opaque constants by coq so we don't really extend types in an interesting way. And the way we give semantics to these new primitives in the kernel is compatible with an interpretation in which the primitives are defined in terms of existing concepts. We only change the order of evaluation which, AFAIU, is not specified.

view this post on Zulip Janno (Oct 11 2023 at 16:09):

It doesn't seem like coqchk will need special treatment outside of bumping a few hardocded values. It seems to re-use the kernel for typechecking so it automatically knows to how to handle the new primitives


Last updated: Jun 13 2024 at 19:02 UTC