Jonathan Protzenko
Jonathan Protzenko
Thanks. @polubelova wrote this code so she (might) be able to tell us whether it's an easy fix or a more complex one I can take care of adding something...
If I understand correctly what you're suggesting, you ended up with the same conclusion I came to. The code is not public yet, but essentially here's what I did locally...
Oh so you don't want to use what is in `bindings/js` but rather you want to provide an *identical* api to the high-level OCaml bindings (`hacl-star` OPAM package), except you...
So you would basically like to add some branching somewhere in the ocaml bindings code that either calls to ctypes or to wasm directly with a minimal amount of glue?...
I see. Then in that case I'd be quite curious to see how you implement it. If you have a proof of concept I'd be quite keen to see it....
Per the discussion in FStarLang/FStar#2072, let's way for a complete set of changes that i) establishes mt_safe when deserializing and ii) checks that the API is sound via a Low*...
I thought we fought really hard with @tahina-pro to make this work... does it no longer work?
There used to be this in the Makefile: + if $(HAS_CL); then USE_CL=true $(MAKE) extract-c ; fi^M And then, a while ago, `extract-c` would also compile and run the tests....
Yes, as part of the Everest-wide Windows builds, we gather all the sources from Everest and recompile them with MSVC and run a few tests. We don't have local HACL...
@Chris-Hawblitzel is the Vale tool expert, here... Chris, any thoughts?