Jonathan Protzenko
Jonathan Protzenko
The noextract should remain -- this function cannot be compiled safely to C. Note that the commit that added the strict on args is ``` commit bb981031e609b37e4a5fd63b040357eb16ab9277 Author: Guido Martínez...
Do you think you could try to dump either an OCaml, or use krml's `-dmonomorphization` for the WASM target (`make dist/wasm/Makefile.basic`) to figure out what the arguments to this particular...
Can I help with this in any way?
First look at this: Hacl.Impl.SHA3.Vec.fst does not type-check on my machine. ``` Verified module: Hacl.Impl.SHA3.Vec 56 errors were reported (see above) ``` is this expected? @mamonet for the record I'm...
> No, I updated FStar repo in order to get type-check failing. I am looking at the errors now and trying to make more reliable code. So these were all...
Ok this is starting to look pretty good! For me, everything in code/sha3 is now good. Let's focus on the changes required in code/hash, which I believe are rather small....
Here's what remains to be done. - @karthikbhargavan we need your review. There seems to be excessive inlining in Hacl_Hash_SHA3.c -- please assess and advise Mamone. - Missing primitive from...
@mamonet please regenerate dist/test/c/Hacl_Test_SHA3.c and push
(after you upgrade krml to the latest version, I pushed a fix for your issue)
``` * Error 19 at /build/source/code/sha3/Hacl.Impl.SHA3.Vec.fst(1201,42-1201,52): hacl-star> - Assertion failed hacl-star> - See also prims.fst(420,83-420,96) ``` @mamonet can you please strengthen this proof?