| Commit message (Collapse) | Author | Age |
... | |
| |
|
|
|
|
| |
This is the lighter-weight solution to #197.
|
|
|
|
| |
This closes #195
|
|
|
|
|
| |
Now it handles matches under binders, e.g., under dlet. This fixes
https://github.com/mit-plv/fiat-crypto/issues/195#issuecomment-308724129.
|
|
|
|
| |
It was previously trying to run constrs and erroring when we turned on debugging
|
| |
|
| |
|
|
|
|
| |
Don't require that the test be strict
|
| |
|
| |
|
|
|
|
| |
It unrolls a for-loop once at the head of the loop
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Induction is so much faster than brute force.
After | File Name | Before || Change
--------------------------------------------------------------------------------
6m15.02s | Total | 7m14.18s || -0m59.15s
--------------------------------------------------------------------------------
0m11.62s | Compilers/Z/ArithmeticSimplifierWf | 0m42.97s || -0m31.35s
0m06.52s | Compilers/Z/ArithmeticSimplifierInterp | 0m34.28s || -0m27.76s
2m47.55s | Specific/IntegrationTestLadderstep | 2m48.14s || -0m00.58s
1m09.50s | Specific/IntegrationTestKaratsubaMul | 1m08.86s || +0m00.64s
1m03.53s | Specific/IntegrationTestLadderstep130 | 1m04.05s || -0m00.51s
0m16.39s | Specific/IntegrationTestFreeze | 0m16.29s || +0m00.10s
0m13.60s | Specific/IntegrationTestMul | 0m13.60s || +0m00.00s
0m11.58s | Specific/IntegrationTestSub | 0m11.36s || +0m00.22s
0m09.79s | Specific/IntegrationTestSquare | 0m09.71s || +0m00.07s
0m03.64s | Compilers/Z/Bounds/Pipeline/Definition | 0m03.54s || +0m00.10s
0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.05s
0m00.55s | Compilers/Z/Bounds/Pipeline | 0m00.58s || -0m00.02s
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Now it can handle ops that return (Tbase TZ)
|
|
|
|
|
|
|
| |
Binary operations with casts were wrongly parenthesized. Luckily, this
impacted nothing in A-normal form, and it impacted nothing that is
currently displayed. It does, however, impact the display of karatsuba
mul.
|
|
|
|
| |
Oops
|
| |
|
| |
|
|
|
|
|
| |
This will make it easier on the reflective machinery, because it won't
have to carry around such large constants.
|
|
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/commit/b4b711cba32a21806c6c0aae53be40c04af60cb3#commitcomment-22521097
|
|
|
|
| |
This version provides hypotheses about the non{negativity,positivity} of the Z.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
sketch out some of the proofs as discussed in #157
|
|
|
|
| |
We (@jadephilipoom?) should now remove the dead-code admits.
|
| |
|
|
|
|
|
| |
It now knows how to deal with _ + 0 involving words, and also eliminates
IdWithAlt when both the first argument and the output are the same size word.
|