Andres Erbsen

Looks like a clever solution that didn't need expanding fiat-crypto was found: https://words.filippo.io/dispatches/wide-reduction/ :)

`propext` may be used in bedrock2 (though maybe just in the compiler?). My suspects for reals and `classic` are coqprime and tauto.

The main reason for connecting to bedrock2 is that other projects in our group are connecting to bedrock2, which we intentionally designed as "common denominator" language. Other existing developments include...

Thanks for the benchmarks and analysis! We have indeed been attributing the slowness of our Montgomery multiplication code to inefficient spilling by C compilers. The differences you describe are compelling...

Yeah, ++ everything Jade said. This is a feature that we'd in principle want, but the pre-existing level of technical debt in that class hierarchy makes it too perilous to...

I think the main question is how to get the high part of a 64-by-64 multiplication. Does Java have int128?

what we do for bedrock2 is mulHigh.

In the idiomatic C translation of these constructs, storing using "store8" and then loading using "loadword" is a strict aliasing violation. And the code that would be calling bedrock2-printed-as-C sure...

Another thought: we could just play safe and stupid with strict aliasing and load larger words in 8-bit chunks in the C back-end... or perhaps have two back-ends, "sane C"...

Yes, we could. Using the wrong one could lead to really awkward bugs.