Jason Gross
Jason Gross
We now compute the loose bounds to be as tight as possible given the tight bounds: they are the tightest bounds that will let us add two tightly-bounded field elements,...
As requested by @zx2c4, this version now does reduction Questions for @jadephilipoom / @andres-erbsen : 1. Should we name the functions `convert_bases_no_reduce` and `convert_bases` to align with `chained_carries_no_reduce`, or should...
As per https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657787914 cc @mdempsky
> As a start, looking at the Selectznz in curve25519.go, shortening the lifetimes of the variables will help. I'll aim to add a flag that allows this shortly. If it's...
> Some primitives (e.g., add-with-carry, sub-with-borrow) are used both in functions that permit bytes, and in functions that do not permit bytes sizes. _Originally posted by @JasonGross in https://github.com/mit-plv/fiat-crypto/issues/706#issuecomment-657157869_ I'm...
> Just one thing: there is a single instruction for changing the size of a value (`Z_static_cast`), no matter if it extends or reduces the size. Ah, I should be...
Should we remove `par:`? It doesn't play well with `make -j` (https://github.com/coq/coq/issues/14203) and seems to make it impossible to install fiat-crypto on Windows via opam (https://github.com/mit-plv/fiat-crypto/pull/966/checks?check_run_id=2521992149)
There's no transitivity lemma for `list_Z_bounded_by` as far as I can tell. In the interests of merging the PR sooner to unblock other things, I'm leaving a TODO there instead....
Armando has requested the ability to see bounds info as a sort-of intermediate output. I think the easiest way to do this is just to add a rewriting pass that...