| Commit message (Collapse) | Author | Age |
|
|
|
| |
This reverts commit 131f341f368b606fd50b57f135e602e40e132b46.
|
|
|
|
|
| |
This is a faster version of [autorewrite with reflective_interp] on
large chains of expressions.
|
|
|
|
|
| |
The real use of this is with the 8.7-only transparent_abstract, but we
can do some things even when we can only cache proofs.
|
| |
|
| |
|
|
|
|
|
| |
List of dynamically-typed key-value pairs, and some helper definitions
and tactics.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change
------------------------------------------------------------------------------
6m08.27s | Total | 6m25.95s || -0m17.68s
------------------------------------------------------------------------------
N/A | Specific/ArithmeticSynthesisTest32 | 0m39.62s || -0m39.61s
0m38.34s | Specific/X25519/C32/ArithmeticSynthesisTest | N/A || +0m38.34s
0m20.46s | Specific/X25519/C32/ReificationTypes | N/A || +0m20.46s
2m31.97s | Specific/X25519/C64/ladderstep | 2m51.10s || -0m19.12s
N/A | Specific/ArithmeticSynthesisTest | 0m09.54s || -0m09.53s
0m09.50s | Specific/X25519/C64/ArithmeticSynthesisTest | N/A || +0m09.50s
1m03.72s | Specific/X25519/C32/femul | 1m11.22s || -0m07.50s
0m10.44s | Specific/IntegrationTestFreeze | 0m17.29s || -0m06.84s
0m34.55s | Specific/X25519/C32/fesquare | 0m40.47s || -0m05.92s
0m05.50s | Specific/X25519/C64/ReificationTypes | N/A || +0m05.50s
0m12.47s | Specific/X25519/C64/femul | 0m13.98s || -0m01.50s
0m08.93s | Specific/X25519/C64/fesquare | 0m10.67s || -0m01.74s
0m11.14s | Specific/IntegrationTestSub | 0m12.06s || -0m00.92s
0m00.50s | Specific/X25519/C32/CurveParameters | N/A || +0m00.50s
0m00.38s | Specific/CurveParameters | N/A || +0m00.38s
0m00.37s | Specific/X25519/C64/CurveParameters | N/A || +0m00.37s
|
| |
|
| |
|
| |
|
|
|
|
|
| |
32-bit ladderstep takes way too long (at least on Coq 8.6), so we don't
add it yet
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This closes #209.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
The new parameterized definitions and proofs are in
WordByWord/Abstract/Dependent/*; the old ones are untouched (and unused)
in WordByWord/Abstract/*. I replaced definitions I didn't know how to
write in the Saturated API with the use of an axiom.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309060964
and
https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309101747
Revert "update ocq2C sed script"
This reverts commit 4a39f39e195b9b7273810a83de78dfd1d150783e.
Revert "make display"
This reverts commit cbf6d013c533d5165d749d0f9405a15d1ff0b43e.
Revert "Make use of CArrayNotations"
This reverts commit cae0e80ae76b76091e7fb86fcd794358a4fe55bb.
Revert "Fix CArrayNotations"
This reverts commit d0d0fbd4499296a2164e209466227892671556f0.
Revert "Revert "Revert "Add CArrayNotations"""
This reverts commit b2b8403ca76f6fd461d9a71ac2e9add4359bba8c.
|
|
|
|
| |
This reverts commit 29ad742d76dca90ec9c8d03ab6f4359ccf053a90.
|
|
|
|
|
|
|
| |
This reverts commit 44359b29d99ab52154dcfdf2b2b16bca7dbaf339.
It triggers [bug #5469](https://coq.inria.fr/bugs/show_bug.cgi?id=5469),
which is present in 8.6, but not v8.6 (nor 8.6.1, once it comes out).
|
|
|
| |
This closes #182.
|
| |
|
|
|
|
|
|
| |
This allows fiat-crypto to continue working with trunk, after the merge
of https://github.com/coq/coq/pull/220. We will remove this when we
migrate to requiring 8.6.1 or 8.7 (neither of which is released yet).
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Now it can handle ops that return (Tbase TZ)
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|