Alix Trieu

On macOS and BSD, `cp` does not have the `-T` option, so `finch` fails with the following message `cp: illegal option -- T`. The issue comes from https://github.com/roddyyaga/finch/blob/685b661b987c7b57fe07e1e67b0ce4f688d87d67/bin/finch.ml#L102

Joye double-add ladder for short Weierstrass curves in co-Z arithmetic

6

Not sure if this is of interest for inclusion, feel free to close if not. I have proved correctness of an implementation of Joye's double-add ladder for short Weierstrass curves...

Bedrock2 End2End field and co-Z operations for secp256k1

3

This PR contains verified Bedrock2 code for - secp256k1 field operations (using Montgomery representation? Not sure about the terminology, is there any literature about saturated/unsaturated Solinas representation ? A quick...

This is a new version of #1997 using the suggestions given there for specifying the NTT. Specifically, this provides - a theory of univariate polynomials (`src/NTT/Polynomial.v`) - the algebraic form...

Field operations for small prime moduli

4

I'm trying to use fiat-crypto to synthesize (bedrock2) C code for NTT operations as used in some PQ lattice-based cryptography, where the prime modulus fits in one word. How difficult...