aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/ArithmeticSynthesisTest.v
Commit message (Collapse)AuthorAge
* Factor out parameter-specific codeGravatar Jason Gross2017-10-07
| | | | | | | | | | | | | | | | | | | | | | | 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
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
|
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
|
* Reorganization of saturated arithmeticGravatar jadep2017-06-29
|
* start saturated-arithmetic API for use in Montgomery (see discussion in #157)Gravatar jadep2017-06-08
|
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
| | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
| | | | | | | With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
* fix last wide mul in curve25519-51Gravatar Andres Erbsen2017-05-20
|
* Make proj1_sig square_sig take only one argumentGravatar Jason Gross2017-05-14
|
* specialize squaring earlierGravatar Andres Erbsen2017-05-14
|
* preserve common subexpressions in donna-derived codeGravatar Andres Erbsen2017-05-14
|
* applied micro-optimizations from donna with [transitivity] and [ring] (as ↵Gravatar jadep2017-05-14
| | | | per #176)
* remove lingering [About]Gravatar jadephilipoom2017-05-14
|
* make freeze use the correct versions of add_get_carry and zselectGravatar jadep2017-05-14
|
* plug in tuple-select rather than using context variablesGravatar jadep2017-05-01
|
* move hints and context outside section (this is what happens when you ↵Gravatar jadep2017-05-01
| | | | 'organize' code last-minute and don't check that it still works)
* first synthesis of freeze codeGravatar jadep2017-05-01
|
* Construct a24_sigGravatar Jason Gross2017-04-17
|
* Merge branch 'rename-everything'. Closes #14.Gravatar Andres Erbsen2017-04-06
|
* rename-everythingGravatar Andres Erbsen2017-04-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 03:29:15 +0000