Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WebAssembly backend #103

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

WebAssembly backend #103

wants to merge 2 commits into from

Conversation

womeier
Copy link

@womeier womeier commented Nov 1, 2024

This PR adds our Wasm backend, as dicussed with Zoe.
It's not ready to be merged. (The proofs need some cleanup, see also below.)

However, you could already take a look at the main statement.
We extended the plugin with CertiCoq Compile Wasm <definition>.. Benchmarks are in benchmarks/wasm.

We'd like to do at least the following before merging:

  • depend on upstream WasmCert instead of our fork
  • use Disjoint and bound_var instead of NoDup (for end-to-end statement)
  • general cleanup of the proofs (we'll probably do that in January 25)
  • these helper lemmas are copied from the C backend and belong somewhere else I think
  • don't depend on the coqprime package (we use it for testing only, is there a way to specify development dependencies for opam?)

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

@womeier womeier marked this pull request as draft November 3, 2024 20:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant