| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/pull/315#discussion_r169085799
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Apparently using `refine eq_refl` rather than `subst <name for evar>;
reflexivity` was resulting in βδ reduction of `chained_carries` in
`carry_mulmod`. The β reduction resulted in us getting a different
cps'd term.
I do not know why this particular β reduction resulted in a 3x slowdown
in partial reduction; it seems like anything that cared about sharing
should either get sharing from the top-level in `carry_mulmod`, or
should have no difference in sharing between the terms
```coq
(fun n s c p idxs
=> fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs))
n s c p idxs
```
and
```coq
fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs))
```
This feels fragile, and I am mystified.
Note for the future: I went about debugging this by integrating little
bits of this PR one by one, seeing which one caused the slowdown, and
then, when I realized it was use of `carry_mulmod`, I took the reified
terms and made a goal asserting their equality, and then took the terms
apart with `f_equal` and `extensionality` until I found the difference.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This is required for reification to work, it seems
|
| | |
|
| |
|
|
| |
For filling in default values
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The proper cps transform of
```
if b then (let x := y in z) else w
```
is
```
cps b (fun b' =>
if b'
then cps y (fun y'
=> let x := y' in cps z k)
else cps w k
```
not
```
cps b (fun b' =>
cps y (fun y' =>
let x := y' in
cps z (fun z' =>
cps w (fun w' =>
if b' then k z' else k w')
```
So we fix the cps transform, and remove the now useless dead code
elimination. The partial reduction pipeline is now 2x faster.
|
| |
|
|
| |
Preparation for following commit
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
See also #300.
We take the simple path of pulling all of the constant multiplication of
sufficiently small size to the end of any expression like a * b * c * d
* ..., and then we associate all addition and multiplication all the way
to the right. This might be very much the wrong choice in some cases;
I invite suggestions that don't require knowing any bounds, which
perform better. (Doing things that require bounds would complicate this
significantly.)
I have no idea why this reassociation results in this part of the diff:
```diff
expr_let 15 := (uint64)(x_14 >> 51) in
expr_let 16 := ((uint64)x_14 & 2251799813685247) in
- expr_let 17 := x_4 +₆₄₋₆₄₋₆₄ (19) *₃₂₋₆₄₋₆₄ x_15 in
- expr_let 18 := (uint32)(x_17 >> 51) in
+ expr_let 17 := x_4 +₆₄ x_15 *₆₄₋₆₄₋₆₄ (19) in
+ expr_let 18 := (uint64)(x_17 >> 51) in
expr_let 19 := ((uint64)x_17 & 2251799813685247) in
- expr_let 20 := x_18 +₃₂₋₆₄₋₆₄ x_7 in
- expr_let 21 := (uint32)(x_20 >> 51) in
+ expr_let 20 := x_18 +₆₄ x_7 in
+ expr_let 21 := (uint64)(x_20 >> 51) in
```
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Initial work
* Respond to code review comments
* Add x25519_32, commented out for speed
* Remove outdated comment
* Add another unfolding thing to make 2^127-1 with (_ + 1/3)%Q work
* Use vm_compute in one place where it's faster
|
| |
|
|
| |
Previously the vo_reverse_closure logic was not working correctly
|
| | |
|
| | |
|
| |
|
|
| |
The older ones don't have --recurse-submodules
|
| | |
|
| |
|
|
| |
developers will clone the submodule via ssh, while travis will clone it via https
|
| | |
|
| |
|
|
| |
removing lemma wordToNat_wzero is ok because it's already in bbv
|
| |
|
|
| |
directory
|
| |
|
|
|
|
|
| |
https://github.com/travis-ci/travis-ci/issues/8507
We use a script and travis_retry to work around "failed to fetch" with
launchpad
|
| | |
|
| |
|
|
| |
This allows us to remove some manual unfolding
|
| | |
|
| |
|
|
|
|
|
|
| |
Rather than always inline, we now introduce one let-bound node per
non-var list element.
Not sure this is the right thing to do, so maybe we should revert this
commit.
|
Jason Gross
Andres Erbsen
Jason Gross
Samuel Gruetter