Jason Gross
Jason Gross
This is how we get a binary for Barrett reduction. Unfortunately it doesn't really work well because we require 2 ^ (machine_wordsize - 1) < M < 2 ^ machine_wordsize....
We were asked over email by @huitseeker: > I'm wondering if there is a reason why fiat is not generating the scalar arithmetic files by default, since every standard parameter...
There are a number of issues, some more major than others: - The function call format is incompatible; we've been doing outputs, then inputs, in the C code, but bedrock2...
#887 added translation support for pairs, but did not update the validity function. @jadephilipoom how should the validity condition be updated (should it be split into "valid anywhere" (expr), "valid...
On Coq master, [`coqchk` successfully runs on fiat-crypto and the parts of bedrock and the rewriter that fiat-crypto uses](https://github.com/mit-plv/fiat-crypto/runs/574704310?check_suite_focus=true) (I'm working on adding it to the CI in https://github.com/mit-plv/fiat-crypto/pull/724). However,...
(3) The bounds analysis rule for `Z.land` rounds the bounds to one less than the nearest power of two. This results in too-loose bounds on expressions involving `Z.land`. In particular,...
Synthesis fails on ``` ./src/ExtractionOCaml/unsaturated_solinas 'p224' '4' '2^224 - 2^96 + 1' '64' ``` With a couple of issues: - bounds analysis cannot prove that the lower bound on carry...
> I should footnote, those numbers are for x86_64. They also include the following patch: > > static void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) { > fiat_p256_uint1...