fiat-crypto
fiat-crypto copied to clipboard
mit-plv
Cryptographic Primitive Code Generation by Fiat
Opening a pull request for the changes suggested in #1215
More of a discussion than an issue. I was talking with @FiloSottile at HACS about the possibility of generating code for curve25519's scalar field using fiat-crypto. My first answer was...
If anyone cared, we could make a verified clone of Mike Hamburg's scalar multiplication synthesis. It accepts descriptions along the lines of: > The key generation algorithm uses the signed...
Currently, the assembly-checker generates annotated output like the following: ` add rcx, rax ; #572, #574, #576, #578, #583, #584, #585, #589, #590, #591, #595, #596, #597, #601, #602, #603,...
I had hoped this would speed things up, but it doesn't. Sister PR to https://github.com/mit-plv/rewriter/pull/48 Timing Diff ``` After | Peak Mem | File Name | Before | Peak Mem...
This reverts commit de47c096b0f0bbee3763ab6293ed8e8e41413147. They are not actually more efficient, though; I'm creating this PR as a placeholder to remind me to work on this / #1293
This reverts commit d9f123fd330dab3fab551d69cd144a15dd0a77c5 It did not work for fixing the extraction, so no need to slow down compilation.
I've started work integrating the Rust output from fiat-crypto into the [RustCrypto `p384` crate](https://github.com/RustCrypto/elliptic-curves/tree/master/p384). One of the biggest hurdles I've encountered is that in our other elliptic curve crates we...
It would be nice to build statically-linked portable binaries for Windows, Mac, and Linux (c.f. [this blog post](https://www.ocamlpro.com/blog/2021_09_02_generating_static_and_portable_executables_with_ocaml), for example), and include them, as well as the generated OCaml source...
It's only present on OCaml >= 4.06, but might help with compile times?