WebAssembly backend

[womeier]

This PR adds our Wasm backend, as dicussed with Zoe.

We extended the plugin with CertiCoq Compile Wasm <definition>..
Benchmarks are in benchmarks/wasm.

Some considerations (before merge or follow-up):

• Refactoring: use Disjoint and bound_var instead of NoDup in correctness statement (relevant for linking to earlier pipeline, to obtain an end-to-end statement at some point)
• these helper lemmas are copied from the proof of the C backend (that doesn't compile currently) and belong somewhere else I think
• The current Docker image has old versions, we need at least compcert 3.14, (see the temporary workaround in the GH actions config)
• one of our benchmarks requires the coqprime package. We probably don't want this as a general dependency. It seems there is no way to specify development dependencies for opam? (The benchmark tests the 63-bit primitive integer operations.)

This PR has our backend in a single commit, we'll keep the full history at gh/womeier/certicoqwasm.

[spitters]

Depends on #115

[womeier]

could someone trigger the CI? (and possibly take a look at the PR)

[spitters]

@yforster @zoep ?

[womeier]

could someone take a look at this? @zoep maybe
(I also texted you on the CertiCoq slack a while back @zoep)

thanks!

[spitters]

@womeier what should be reviewed?
Is the PR ready to merge, or do you feedback before you can address the todos you list above?

[womeier]

The last three todos are really small things. I was just hoping for feedback/another opinion.
The first one about using Disjoint will take a bit of work, I thought it could make sense to merge the PR before that.
(the Wasm backend is fully usable as is now; the change will be necessary for the end-to-end statement)

The diff is already quite large, so I'm a little hesitant to include more changes...
It'd just be nice if so. could take a look first.

[womeier]

Thanks for the merge.
Unrelated to this, we also have a Nix-based setup for CertiCoq with the coq-nix-toolbox.
Would you care to have that @yforster?
If so I can open a PR.

[mattam82]

@womeier yes please, for the nix setup!