Jason Gross
Jason Gross
I had hoped this would speed things up, but it doesn't. Sister PR to https://github.com/mit-plv/rewriter/pull/48 Timing Diff ``` After | Peak Mem | File Name | Before | Peak Mem...
This reverts commit de47c096b0f0bbee3763ab6293ed8e8e41413147. They are not actually more efficient, though; I'm creating this PR as a placeholder to remind me to work on this / #1293
This reverts commit d9f123fd330dab3fab551d69cd144a15dd0a77c5 It did not work for fixing the extraction, so no need to slow down compilation.
It would be nice to build statically-linked portable binaries for Windows, Mac, and Linux (c.f. [this blog post](https://www.ocamlpro.com/blog/2021_09_02_generating_static_and_portable_executables_with_ocaml), for example), and include them, as well as the generated OCaml source...
It's only present on OCaml >= 4.06, but might help with compile times?
Towards better equivalence checking cc @davidben @andres-erbsen We don't support these instructions yet: ``` $ src/ExtractionOCaml/word_by_word_montgomery p256 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' mul --no-wide-int --shiftr-avoid-uint1...
We should consider how to get better asymptotics on the equivalence checker, given that we now have invocations that take nearly an hour to run. For example, in [p448-mul-callgrind-with-source.7z.zip](https://github.com/mit-plv/fiat-crypto/files/8521862/p448-mul-callgrind-with-source.7z.zip), we...
On top of #1202
https://github.com/mit-plv/fiat-crypto/blob/bb756e43d1a819d41d0a3ca0f32be2870f83067c/src/Assembly/WithBedrock/Semantics.v#L246-L253 According to https://stackoverflow.com/questions/45495711/should-i-use-mul-or-imul-when-multiplying-a-signed-number-to-an-unsigned-num#comment105736478_59796786, "[mul](https://www.felixcloutier.com/x86/mul) sets CF and OF if the upper half is non-zero. [imul](https://www.felixcloutier.com/x86/imul) sets CF and OF if the upper half isn't the sign-extension of the low...
Do we want to use some version of https://github.com/benchmark-action/github-action-benchmark ?