| Commit message (Collapse) | Author | Age |
... | |
|
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/pull/332#discussion_r176415846
|
| |
|
|
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176417396
|
| |
|
|
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176417542
|
|
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176414627
|
|
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176422391
|
|
|
|
|
|
| |
By passing through a type of expression trees without any Gallina
functions in the AST, we achieve good performance (even faster than
before) on the pipeline with a cbv strategy.
|
| |
|
|
|
|
|
| |
This makes the pipeline faster to run under vm_compute than under lazy.
I suspect mainly because I've replaced [bool_rect] with [if].
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
This allows vm_compute to run in 300 seconds on the from_associational
pipeline.
|
|
|
|
|
| |
This allows us to remove the special case for `bool_rect`, and is a
step towards targeting `vm_compute` rather than `lazy`.
|
| |
|
| |
|
| |
|
|
|
|
| |
It was too slow to do `lazy -[Let_In]` in montgomery reduction.
|
|
|
|
| |
Also adapt to the lack of `'` notation in master for `Z.pos`.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Still need to insert casts for operations returning two values
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As the comment says, doing `lazy` is twice as slow as doing `lazy
-[Let_In]; lazy`. This is because the bounds pipeline does `dlet E :
Expr := (reduced thing) in let b := extract_bounds E in ...`. If we
allow `lazy` to unfold `Let_In` before it fully reduces the function
(function, because `Expr := forall var, @expr var`), then there is no
sharing between the partial reduction in bounds extraction and the
partial reduction in the return value. So we force `lazy` to fully
reduce the argument first, and only then permit `lazy` to inline it.
This is slightly slower than doing bounds analysis in a non-PHOAS
representation; we spend about 3%-5% of the overall time doing bounds
extraction, and fully reducing the bounds extraction expression before
plugging in arguments costs a bit more. However, it's still reasonably
fast, and the code is much simpler when `Interp` always succeeds rather
than returning `option`.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
- Update the style of montred snythesis to match the changes in the
pipeline
- Bring back non-quadratic dead code elimination and make use of it for
montgomery reduction
- Update partial reduction to inline "var-like" things (fst, snd, pair
applied to var)
|
|
|
|
| |
Unfortunately, the ring proofs are a bit messy.
|
|
|
|
|
| |
We can't actually prove the previous okness lemmas in
SimplyTypedArithmetic, so we instead ask for exactly what we need.
|
| |
|
|
|
|
|
|
|
| |
Major change is porting everything to Z and using Z.div_mod_to_quot_rem
which is a handy sledgehammer. Z is also a nice simplification. Dealing
with subtraction is tidier, though I do have 0 <= x goals everywhere as
a result.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This variant comes from
http://www.ridiculousfish.com/blog/posts/labor-of-division-episode-i.html.
It was useful for
https://boringssl-review.googlesource.com/#/c/boringssl/+/25887.
TODO - Talk to Andres to figure out all the ways this could be done more
cleanly. It was originally a standalone file.
|
| |
|
| |
|
|
|
|
| |
been in last commit
|
| |
|
| |
|