Jason Gross

Add Go tests to the CI

26

It would be nice to be able to verify that our Go code works. I'm not sure where to find Go tests, though. cc @andres-erbsen

Using .h rather than .c, and using `__attribute__((unused))`?

1

> Optional/follow-up/whatever: if you're outputting a file that's meant to be #included somewhere (given the symbols are `static` anyway), there may be something to be said for the files being...

With `ulimit -S -s 1000000`, it completed in just over an hour: [fiat_32.txt](https://github.com/mit-plv/fiat-crypto/files/4834869/fiat_32.txt) Perhaps we should document in the README how to increase the stack size? _Originally posted by @JasonGross...

Bench bedrock2 C code

1

We should see if it's really slower or not. While we're at it, maybe we should add a CI test that drops the newest version of our code into BoringSSL...

cc @andres-erbsen @davidben

p448 32-bit uses int128

10

There are a lot of Z.combine_at_bitwidth operations left over. Not sure why, I'll try to dig into this.

How to improve the synthesis experience

4

> > Thanks for setting this up for me. Our pipeline has come a long way since we first pushed stuff through it, I had an actually decent experience working...

Karatsuba Support?

7

Should we support karatsuba again? IIRC, the main issue was that we couldn't recognize that `x + y - x` had the same bounds as `y`. However, we should be...

Add support for signed cmov

2

Currently the analysis of what primitives we needs only looks at unsigned numbers. In implementing #679, we might want (for Java) the ability to emit, e.g., `cmovznz_64` rather than just...

[WIP] Add partial semantics for the C AST

1

This is definitely not ready for merge (though I believe it does build) I've left a bunch of `TODO`s for @davidben (or possible for me-in-the-future) to fill in the actual...