Typed extraction integration

[mattam82]

This finally updates the typed extraction correctness proof, including the dearging optimization, allowing it to use efficent environment representations.
We additionally prove that it preserves wellformedness and fixpoint eta-expansion, so it can be integrated in all existing pipelines. We generalize a bit the correctness theorem so that we have a simulation for all terms (it used to be restricted to constants that evaluate to constructors). This mainly required adding a bit more of invariants on valid masks in the environment. The transformation is partial in the sense that if the environment analysis does not produce valid masks for dearging, we will just use the identity transformation, to fit in the total erasure pipelines we have for now.
The new commands "MetaCoq (Bypass) Typed Erase" run the extracted verified extraction in OCaml.

[4ever2]

@mattam82 could you please elaborate a bit on what these changes to the valid masks are?

This PR breaks all our extraction examples in https://github.com/AU-COBRA/coq-elm-extraction and https://github.com/AU-COBRA/coq-rust-extraction when both the do_trim_ctor_masks and check_valid_masks flags are set to true in dearg_transform.

Those examples worked before and it is not clear to me if it is a bug or that is the expected behaviour after this PR.

[spitters]

@mattam82 pinging this issue, so it does not become stale...

[mattam82]

IIRC, I changed the default value of do_trim_ctor_masks as otherwise the valid mask check was always failing for me, but I might be wrong. In any case, we should probably make this configurable for the whole pipeline to debug this issue.

[mattam82]

The relevant part of the new invariant is this:

Definition check_oib_masks masks i oib :=
  forallbi (fun c cb => #|get_branch_mask masks i c| == cb.2) 0 oib.(ind_ctors) &&
  match oib.(ind_projs) with
  | [] => true
  | _ :: _ =>
    let mask := get_branch_mask masks i 0 in
    #|mask| == #|oib.(ind_projs)|
  end.

I guess previously we didn't consider primitive projections, but they have to be masked if some arguments are removed (and hence some projections are not defined anymore).

[4ever2]

Thanks for the help. I see now why it doesn't work anymore, the new check that you added to check_valid_masks assumes that the length of the masks will be equal to the number of constructor arguments. However, do_trim_ctor_masks trims trailing false values in the masks so when enabled the assumption might be broken.

I suppose we should change the check in check_oib_masks to <= instead or document that the two flags are incompatible.