Matthew Dempsky

@JasonGross Defining a `uint1` type is fine by me. Shouldn't affect code generation at all. (You can also generate type declarations unconditionally if you want. Go only disallows importing unused...

Last night I was playing with making use of fiat-crypto's NIST P-224 code. The fiat-crypto 32-bit code seems marginally slower than Go's existing [constant-time P-224 implementation](https://golang.org/src/crypto/elliptic/p224.go) on 386 (caveat: I...

> However, I was under the impression that Montgomery reduction was only efficient when using saturated limbs, and that unsaturated Solinas should be used instead for unsaturated primes (unfortunately, unsaturated...

I think these would be nice improvements if they're easy and don't add complexity to fiat-crypto's output routines (which aren't verified), but I don't think any of these affect the...

FWIW, the syntax rules for Go documentation are described at: https://golang.org/pkg/go/doc/#ToHTML I think the main noteworthy things for fiat-go code are that blank lines separate paragraphs, and runs of indented...

> Which indented lines become `` blocks? It looks like lines 3 and 4, 6 and 7, and 9 and 10 become pre blocks: testing with `go doc` ``` mdempsky@mdempsky:/tmp/test$...

Makes sense. So we just need a formally verified implementation of gofmt in Coq? :)

Thanks, that was quick! Let me benchmark to confirm the new code is actually faster than repeated additions.

Unfortunately, in my benchmarking, these scmul routines are slower than repeated additions. fiat_p224_add takes about 12ns; tripling and quadrupling take about 25ns; and octupling takes about 38ns. The generated scmul...

@JasonGross I haven't benchmarked it specifically, but I assume the bitshifting is faster if only because it's fewer instructions. I can measure though if it would be helpful. Here's an...