Jason Gross
Jason Gross
Maybe we can clone BoringSSL and compile it's test-suite? Or probably there's a better way? Maybe? cc @andres-erbsen @davidben
The standard way that things here fail to reify is that we don't support `Q`, and some of the weight stuff uses `Q`, iirc. We could just add support for...
Java has neither unsigned types nor uint128. Currently, we are generating 32-bit-targeted code for Java, but if I understand correctly, all of the operations (`+`, `-`, `*`, `>`, `&`, `|`)...
The panic [in Rust], as far as I can tell, isn't on the 128 bit numbers, but on the way we negate a signed number to turn it into an...
This is causing issues in the Go output (which doesn't support 128-bit integer infix arithmetic), which I'm basing on Rust. Consider the difference in `subborrowx_u51` between C and Rust: https://github.com/mit-plv/fiat-crypto/blob/ec9a757aba9ebafc43f069d2eeeeb623eb342d4d/curve25519_64.c#L59...
Since https://github.com/mit-plv/fiat-crypto/pull/664, we now sometimes strip casts out. After discussion with Andres, we decided that this should probably be mandatory, rather than taking a boolean. This issue is mostly for...
For 2^224 - 2^96 + 1, 128-bit words, we get the synthesized code ```coq mulmod = fun var : type -> Type => λ x x0 : var (type.base (base.type.list...
I'm concerned stackcollapse-perf.pl is going to blow through my available RAM; is there any way for it to be more streaming?  My perf.data file is almost 9GB, the output...
I'm not sure if this is the right place to report this, but there seems to be a nondeterministic issue with the setup of OCaml/opam on Windows: ``` Processing actions...
It would be nice if I could set some variable to `true` to have the opam environment added to path, so I don't need to `opam exec` everything. (It might...