| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
| |
Jason & Andres
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
multiplication (currently produces way too many expressions because 1*x
and -1*x are not simplified for two-output mul)
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Montgomery use them
|
| |
|
|
| |
the output accumulator--this prevents the accumulator from repeatedly showing up in the expression and making the term huge
|
| | |
|
| |
|
|
|
|
|
|
|
| |
It was serving no purpose, and was messing up the associativity of
balance on sub. I believe it was originally there because I thought I
had to handle 19 * (a * b + c * d) -> (19 * a) * b + (19 * c) * d, but
this case doesn't show up, and so I never wrote the code to handle it,
but also never removed the code to parse additions into lists (thereby
losing associativity information).
|
| | |
|
| |
|
|
|
|
| |
This reverts most of commit f776eb5815166f1ff648808231794dee01a4683c.
We'll do it a different way.
|
| |
|
|
| |
It was messing up the associativity of balance on sub.
|
| |
|
|
|
|
| |
We compute them as 1.1*(s-1), which is a simpler way to express that
they vary across limbs for nonuniform bases. This allows 32-bit 25519
sub to boundscheck.
|
| |
|
|
|
|
|
|
|
| |
Previously I was trying to make the proof easier by using the same var
type for input and output (which would allow a
correctness-of-interpretation proof which doesn't depend on
well-formedness). We now no longer do that, and instead go from `@expr
(@expr var)` to `@expr var`, and avoid introducing useless `Abs` and
`App` nodes.
|
| |
|
|
|
| |
They disappear after the end of the section, but I want them to stay in
distr_length for later proofs.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The immediate motivation is BoringSSL's generic EC code is sadly stuck
with supporting arbitrary curves, including those where a <> -3, but it
may be more generally useful.
This makes the file slightly more general:
- It now proves that the addition formula works independent of a = -3.
- It proves a generic doubling implementation, based on
http://www.hyperelliptic.org/EFD/g1p/auto-shortw-jacobian.html#doubling-dbl-2007-bl
- There's a place to stick in other specializations should someone want
them. (I hear some folks are interested in secp256k1 for some reason.)
|
| | |
|
| |
|
|
| |
preparation for reifying barrett; tweaked definition of cc_l
|
| |
|
|
| |
This will be required to correctly stringify the syntax tree for the error message
|
| | |
|
| |
|
|
|
|
| |
This was causing issues with bug minimization because some hints seem to
follow [Require], not [Import], and so when [eauto] got stronger, this
proof was failing.
|
| |\
| |
| | |
comprehensive loops framework with complete proof theory
|
| | |
| |
| |
| |
| | |
See https://github.com/coq/coq/issues/7291 and
https://github.com/mit-plv/fiat-crypto/issues/349#issuecomment-382180578
|
| | | |
|
| | |
| |
| |
| | |
This should fix #349 (or at least most of it).
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
To updated version of https://github.com/coq/coq/pull/6597
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
After in-person discussion with Andres, we decided that, because the
previous form of uncurrying was only half-uncurried (not including
identifiers nor lambdas passed to other lambdas), and the strongest
driver of a full uncurrying pass would be having an easier-to-visualize
intermediate representation / knowing more clearly what the pipeline is
doing, and the changes required for making this a full uncurrying pass
would be global to the pipeline (require changing the type of
identifiers), we would instead go back the version of uncurrying that I
initially proposed, where we only uncurry the top-level function.
Note that we create a slightly more complicated term (with more
application nodes) than we have to; if we instead took in `@expr (@expr
var) t` rather than `@expr var t`, we wouldn't introduce needless
abstractions. However, the current form admits an extremely simple
proof of correctness, which doesn't even require well-formedness of the
expression tree.
|
| | |
| |
| |
| |
| | |
This allows us to (a) consolidate the constant and non-constant
pipelines and (b) vastly simplify the call-with-id-continuation logic.
|
| | |
| |
| |
| |
| | |
This pass uncurries all applied lambdas. Care is taken to not do beta
reduction and to not introduce spurious `Abs` or `App` nodes.
|
| | | |
|
Jason Gross
Jade Philipoom
Andres Erbsen
David Benjamin