Bas Spitters
Bas Spitters
@andres-erbsen I think it's a great start to move such lemmas to the stdlib. Since you mention using modulo arithmetic for machine integers, it might be worth having a peek...
What is the status of this? We have updated SSProve to MC2.0 and would also like to update the jasmin part.
> Is the performance regression still unacceptable with hierarchy-builder 1.7? @cmester0 mentioned that HB 1.7 still has similar timings on his machine :-(
@andres-erbsen has anything happened on the plan to add extension-field support to Arithmetic and Curves?
@andres-erbsen Did they get back to you?
@mattam82 I could not directly find the answer in the code. How are Int63 translated to C? Are you using 64 bit integers? Did you prove correctness of this translation,...
Thanks! I wasn't aware of: https://github.com/CertiCoq/VeriFFI It seems somewhat related to https://gallium.inria.fr/~agueneau/publis/melocoton.pdf , which treats the ocaml-C FFI.
What is the status of this? We'd like to use it here: https://github.com/cryspen/libcrux/issues/225 for ElectionGuard integration.
These failures should not be connected to the README. Maybe we should just restart the CI?
fiat-crypto can generate wasm via rust. For F* there is [this](https://github.com/Inria-Prosecco/libsignal-protocol-wasm-fstar) library. Did you consider those?