Jason Gross

Montgomery: support rolled loops

2

We can actually support very large primes with minimal changes: 1. Export redc_step 2. Thunk synthesis so that when mul is not requested it's not computed 3. Write a wrapper...

Vectorizing Montgomery multiplication might require leaving free the top bits of each limb so we don't need carry bits. We should support, e.g., p256 51-ish-bit limbs in Montgomery form. This...

Two improvements that came from debugging https://github.com/mit-plv/fiat-crypto/pull/1187 - Annotate each line in the dag with the assembly lines / PHOAS lines that first generated it; or, annotate each line of...

Add Java tests to the CI and fix buggy Java output

3

We should test the Java code. I'm not sure where to find Java tests, though. cc @peterdettman @dghgit,

Windows CI is too slow

3

Since we added a couple more AMD64 tests, the Windows build has been timing out. Current CI Build times are: Stage \ Version | [Windows (8.12.0, no bedrock)](https://github.com/mit-plv/fiat-crypto/runs/5656129903?check_suite_focus=true) | [MacOS...

There are a bunch of "Command exited with non-zero status 2" errors at https://github.com/mit-plv/fiat-crypto/runs/5656130024?check_suite_focus=true#step:7:56 which is maybe because we set up some bash scripts wrong? The subsequent make works fine...

> This is not setoid_rewrite, though, because I'm not using at anywhere, only in Indeed, you're right. That said, the Leibniz rewrite also sets `modulo_conv_on_closed_terms` to `Some` so it will...

Tracking uses of fiat-crypto

21

Maybe we should create a wiki page tracking uses of fiat-crypto? The ones I'm aware of: - BoringSSL / https://boringssl.googlesource.com/boringssl/+/refs/heads/master/third_party/fiat/ / https://boringssl.googlesource.com/boringssl/+/47b1e39042bc3208771a8d947f1a1ed2fe5f3d8b/third_party/fiat/ / https://web.archive.org/web/20201218200341/https://boringssl.googlesource.com/boringssl/+/refs/heads/master/third_party/fiat/ - Chrome via BoringSSL - Facebook...

I am also happy to provide my types which look like this: Maybe we can add this in a file and refer to it from the Readme (instead of describing...

Use operator precedence to print C code

2

I'm attempting to make the printing code more uniform and factor out common patterns a bit more, in part to decrease the likelihood of transcription errors, but I'm afraid I...