[rfc] Introduce a new ERASEcast kind for evaluation using verified erasure …

[mattam82]

…(to be linked to the kernel through the rocq-verified-extraction plugin)

For Rocq proper, this just adds a new parsing rule for c <<<: t which binds to a new cast kind.
kernel/eraseconv.ml is then in charge of transmitting the values to evaluate to a plugin which
provides a Environ.env -> Constr.t -> (Constr.t, unit) result. This is what the
PR MetaRocq/rocq-verified-extraction#34 provides.

The interface might seem a bit convoluted but the typing rule is the following, informally:
When typechecking c <<<: t, we infer the type c : cty and call eraseconv with cty and t.
t has to be an inductive type applied to parameters and indices. We evaluate all the indices using
erasure evaluation and then call back regular conversion betwee cty and the new t. If this succeeds,
it is dimmed type correct. Outside this fragment, it is a type error. For pretyping, we can hence allow
cty to still contain metavariables and fall back to regular evarconv for the final cty ~= t' test, hence
one does not need to know the value computed by erased evaluation beforehand, it can just be used to fill
an evar.

We could work on making this plugin more standalone. Right now it needs all of MetaRocq + Malfunction/VerifiedExtraction to produce the .cmxs but we could also make a standalone plugin based on the generated (verified) .mlf file and wrapper ML files.

• Added / updated test-suite.
  Without an installed erasure function, x <<<: t is an error.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

[SkySkimmer]

I guess the checker would install the identity function as a "reduction"? we could also have a checker version linked with the plugin

[SkySkimmer]

this check is incomplete, the env may contain evars too

[mattam82]

Yup, and we should check for a closed env as well.

[SkySkimmer]

how about allow returning a message (Pp.t) in the error case?

[mattam82]

Indeed that will be done :)

[mattam82]

For sure one could install the identity without endangering anything

[Janno]

I am very excited about this PR both because of the progress on verified extraction and also because it is giving me ideas related to casts in general. I suppose the amount of < in <<<: already hints at a problem of extensibility and modularity. So I wonder if Rocq shouldn't have a more generic mechanism to hook into the typechecker through casts. That mechanism could let plugins register as many different casts as they want¹.

For example, people could experiment with casts that perform limited reduction (with blacklists of whitelists for specific constants), or even manually traverse cty and reduce certain parts with vm_compute and keep other parts intact. Is this a useful idea?

If this needs to go in without being delayed by discussions about a more generic mechanism I can move my suggestion into a separate RFC.

Footnotes

1. Ideally this would use properly namespaced identifiers for these casts.. but that might be hard to do. So unique strings could suffice? ↩

[mattam82]

Just FTR, the nix CI for MetaRocq/rocq-verified-extraction#34 is green, using a slightly patched metarocq that handles ERASEcast. E.g. Check (eq_refl <<<: true = negb false) can check there by computing negb false in malfunction/ocaml.

[SkySkimmer]

I don't see the point in having this function here instead of in the plugin. Why not call the cast eg CustomCast and directly install custom_conv : conv_pb -> types kernel_conversion_function?

[silene]

Before, to produce a proof of False, a plugin had to corrupt memory somehow. Now, it can just invoke install_erase_conv. While I am all for replacing/improving parts of Rocq with MetaRocq-derived code, I really do not think that plugins are the way to go. (Let us not give even more arguments for ANSSI to say that one should disable plugins in Coq.)

Since you write that you would be able to make a standalone plugin that would embed the generated malfunction code, why not go a step further? Just push this generated code directly to this repository, so that it gets statically linked to Rocq. Sure, having some generated code in a repository is frowned upon, but there is some prior art, e.g., OCaml's boot/ocamlc, or even Rocq itself (that is, micromega.ml).

[SkySkimmer]

Before, to produce a proof of False, a plugin had to corrupt memory somehow.

not true, there are much easier ways to prove False from plugins

[mattam82]

Before, to produce a proof of False, a plugin had to corrupt memory somehow. Now, it can just invoke install_erase_conv. While I am all for replacing/improving parts of Rocq with MetaRocq-derived code, I really do not think that plugins are the way to go. (Let us not give even more arguments for ANSSI to say that one should disable plugins in Coq.)

I agree this is very unsafe in the current presentation. We could explicitly taint definitions requiring a use_eraseconv typing flag as a first safeguard?

Since you write that you would be able to make a standalone plugin that would embed the generated malfunction code, why not go a step further? Just push this generated code directly to this repository, so that it gets statically linked to Rocq. Sure, having some generated code in a repository is frowned upon, but there is some prior art, e.g., OCaml's boot/ocamlc, or even Rocq itself (that is, micromega.ml).

That's possible indeed, I don't know what @ppedrot and @SkySkimmer would say about this. That's basically adding a dependency on malfunction and a 2Mb source file to the repo. Plus integrating the OCaml quoting part of MetaRocq/template-rocq.

[mattam82]

I am very excited about this PR both because of the progress on verified extraction and also because it is giving me ideas related to casts in general. I suppose the amount of < in <<<: already hints at a problem of extensibility and modularity. So I wonder if Rocq shouldn't have a more generic mechanism to hook into the typechecker through casts. That mechanism could let plugins register as many different casts as they want1.

For example, people could experiment with casts that perform limited reduction (with blacklists of whitelists for specific constants), or even manually traverse cty and reduce certain parts with vm_compute and keep other parts intact. Is this a useful idea?

If this needs to go in without being delayed by discussions about a more generic mechanism I can move my suggestion into a separate RFC.

I think we want some agreed upon customCast interface anyway before we merge this, unless we directly integrate it as @silene proposes. Anyway, +1 for a separate RFC on that interface.