aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Add update_by_tac_if_not_existsGravatar Jason Gross2017-10-10
|
* TagList: make get error, and fix bugsGravatar Jason Gross2017-10-10
|
* Add TagListGravatar Jason Gross2017-10-10
| | | | | List of dynamically-typed key-value pairs, and some helper definitions and tactics.
* Add notationsGravatar Jason Gross2017-10-10
|
* Add UniformWeightInstancesGravatar Jason Gross2017-10-09
|
* Generalize phisGravatar Jason Gross2017-10-07
| | | | | | | | | | | | | | | | After | File Name | Before || Change ----------------------------------------------------------------------- 3m56.20s | Total | 4m14.86s || -0m18.66s ----------------------------------------------------------------------- 0m02.44s | Specific/X25519/C32/ReificationTypes | 0m19.48s || -0m17.03s 2m00.12s | Specific/X25519/C64/ladderstep | 1m55.72s || +0m04.40s 0m01.16s | Specific/X25519/C64/ReificationTypes | 0m05.17s || -0m04.00s 0m26.27s | Specific/X25519/C32/fesquare | 0m27.76s || -0m01.49s 0m52.60s | Specific/X25519/C32/femul | 0m52.46s || +0m00.14s 0m10.35s | Specific/X25519/C64/femul | 0m10.28s || +0m00.07s 0m08.30s | Specific/IntegrationTestSub | 0m08.69s || -0m00.38s 0m07.97s | Specific/IntegrationTestFreeze | 0m08.00s || -0m00.03s 0m06.99s | Specific/X25519/C64/fesquare | 0m07.31s || -0m00.31s
* Factor out the compute bit of the compute notation in curve paramsGravatar Jason Gross2017-10-07
| | | | This will let us call it from Ltac; notations with tactics don't internalize identifiers correctly at tactic definition time
* 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
* Coq 8.5 can't handle symbol-free notationsGravatar Jason Gross2017-10-06
|
* Fix display logGravatar Jason Gross2017-10-06
|
* Clean up TestCase a bitGravatar Jason Gross2017-10-06
|
* Add another constantGravatar Jason Gross2017-10-06
|
* Add pow_ceil_mul_nat_nonnegGravatar Jason Gross2017-10-05
|
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
|
* Factor out some bits of ladderstep preglueGravatar Jason Gross2017-10-05
| | | | | This requires some changes to nonzero, which now needs to unfold proj1_sig itself.
* Add some ZUtil lemmasGravatar Jason Gross2017-10-03
|
* Make some typeclasses opaqueGravatar Jason Gross2017-10-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Not sure if it actually does anything in this case... The intent is to prevent tc resolution from unfolding [reify] and [reify_internal] / picking up one when looking for the other. After | File Name | Before || Change --------------------------------------------------------------------------------------- 13m02.51s | Total | 13m01.90s || +0m00.60s --------------------------------------------------------------------------------------- 1m30.27s | Specific/IntegrationTestKaratsubaMul | 1m25.34s || +0m04.92s 2m50.80s | Specific/X25519/C64/ladderstep | 2m53.74s || -0m02.93s 2m21.34s | Specific/NISTP256/AMD64/femul | 2m21.37s || -0m00.03s 1m12.30s | Specific/X25519/C32/femul | 1m12.04s || +0m00.26s 1m09.50s | Specific/IntegrationTestLadderstep130 | 1m09.66s || -0m00.15s 0m41.30s | Specific/X25519/C32/fesquare | 0m41.27s || +0m00.02s 0m27.08s | Specific/IntegrationTestMontgomeryP256_128 | 0m27.13s || -0m00.05s 0m17.64s | Specific/NISTP256/AMD64/fesub | 0m18.06s || -0m00.41s 0m16.45s | Specific/IntegrationTestFreeze | 0m17.36s || -0m00.91s 0m15.94s | Specific/NISTP256/AMD64/feadd | 0m16.02s || -0m00.08s 0m14.74s | Specific/NISTP256/AMD64/feopp | 0m14.42s || +0m00.32s 0m14.33s | Specific/X25519/C64/femul | 0m13.97s || +0m00.35s 0m12.41s | Specific/IntegrationTestSub | 0m12.44s || -0m00.02s 0m11.91s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.06s || -0m00.15s 0m11.61s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.00s || -0m00.39s 0m10.95s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.82s || +0m00.12s 0m10.28s | Specific/X25519/C64/fesquare | 0m10.46s || -0m00.18s 0m09.68s | Specific/NISTP256/AMD64/fenz | 0m09.76s || -0m00.08s 0m09.28s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.30s || -0m00.02s 0m03.54s | Compilers/TestCase | 0m03.41s || +0m00.12s 0m03.04s | Specific/NISTP256/FancyMachine256/Montgomery | 0m03.20s || -0m00.16s 0m02.99s | Specific/NISTP256/FancyMachine256/Barrett | 0m02.99s || +0m00.00s 0m02.16s | Specific/NISTP256/FancyMachine256/Core | 0m02.20s || -0m00.04s 0m00.82s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || +0m00.01s 0m00.70s | Compilers/Z/Bounds/Pipeline | 0m00.66s || +0m00.03s 0m00.57s | Compilers/Z/Reify | 0m00.53s || +0m00.03s 0m00.50s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.54s || -0m00.04s 0m00.38s | Compilers/Reify | 0m00.36s || +0m00.02s
* Speed up reification a little bitGravatar Jason Gross2017-10-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This helps a lot more in C32 ladderstep; we eliminate useless typeclass unification against hypotheses by separating out the typeclass used for external overloading and posing hypotheses, and the typeclass used for recursion under binders. After | File Name | Before || Change --------------------------------------------------------------------------------------- 12m49.58s | Total | 13m04.75s || -0m15.16s --------------------------------------------------------------------------------------- 2m48.67s | Specific/X25519/C64/ladderstep | 2m58.05s || -0m09.37s 2m21.65s | Specific/NISTP256/AMD64/femul | 2m16.64s || +0m05.01s 1m25.60s | Specific/IntegrationTestKaratsubaMul | 1m30.00s || -0m04.40s 1m08.01s | Specific/X25519/C32/femul | 1m12.17s || -0m04.15s 1m08.25s | Specific/IntegrationTestLadderstep130 | 1m11.61s || -0m03.35s 0m39.67s | Specific/X25519/C32/fesquare | 0m39.16s || +0m00.51s 0m27.09s | Specific/IntegrationTestMontgomeryP256_128 | 0m27.02s || +0m00.07s 0m17.74s | Specific/NISTP256/AMD64/fesub | 0m18.34s || -0m00.60s 0m17.21s | Specific/IntegrationTestFreeze | 0m16.37s || +0m00.83s 0m15.89s | Specific/NISTP256/AMD64/feadd | 0m15.31s || +0m00.58s 0m14.78s | Specific/NISTP256/AMD64/feopp | 0m14.73s || +0m00.04s 0m14.47s | Specific/X25519/C64/femul | 0m14.39s || +0m00.08s 0m12.07s | Specific/IntegrationTestSub | 0m11.76s || +0m00.31s 0m12.07s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.93s || +0m00.14s 0m11.79s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.00s || -0m00.21s 0m10.84s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.90s || -0m00.06s 0m10.08s | Specific/X25519/C64/fesquare | 0m10.61s || -0m00.52s 0m09.66s | Specific/NISTP256/AMD64/fenz | 0m09.68s || -0m00.01s 0m09.27s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.28s || -0m00.00s 0m03.51s | Compilers/TestCase | 0m03.49s || +0m00.01s 0m03.08s | Specific/NISTP256/FancyMachine256/Montgomery | 0m03.23s || -0m00.14s 0m02.99s | Specific/NISTP256/FancyMachine256/Barrett | 0m03.00s || -0m00.00s 0m02.16s | Specific/NISTP256/FancyMachine256/Core | 0m02.15s || +0m00.01s 0m00.86s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.84s || +0m00.02s 0m00.68s | Compilers/Z/Bounds/Pipeline | 0m00.61s || +0m00.07s 0m00.56s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.54s || +0m00.02s 0m00.54s | Compilers/Z/Reify | 0m00.54s || +0m00.00s 0m00.40s | Compilers/Reify | 0m00.41s || -0m00.00s
* Add missing tactic in comment in ladderstepGravatar Jason Gross2017-09-27
|
* Add src/Specific/X25519/C32/compiler.sh, update ↵Gravatar Jason Gross2017-09-27
| | | | src/Specific/X25519/C64/scalarmult.c
* Add curve25519-donna-c64 to etc/third_partyGravatar Jason Gross2017-09-27
|
* Add missing fileGravatar Jason Gross2017-09-21
|
* Add femul,fesqure for C32Gravatar Jason Gross2017-09-21
| | | | | 32-bit ladderstep takes way too long (at least on Coq 8.6), so we don't add it yet
* Update constants filesGravatar Jason Gross2017-09-21
|
* Add extract_ExprGravatar Jason Gross2017-09-21
|
* Split off tactics in IntegrationTestDisplayCommonGravatar Jason Gross2017-09-21
|
* make benchGravatar Jason Gross2017-09-12
|
* fsatz tests: 1/(1/x) = xGravatar Andres Erbsen2017-09-11
|
* Fix more commented out alternativesGravatar Jason Gross2017-09-05
|
* Fix commented out alternate version in ladderstepGravatar Jason Gross2017-09-05
|
* Add decidable equality with nilGravatar Jason Gross2017-08-13
|
* Factor out some of the preglue synthesis codeGravatar Jason Gross2017-07-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes it a bit more uniform, and hopefully more automatable and packageable. Unfortunately, there's still no spec for this part of the pipeline, so the tactics simply aggregate common patterns. Alas, this also makes things a bit slower; I suspect that [Defined] is the place where things are slower. After | File Name | Before || Change --------------------------------------------------------------------------------------- 13m51.14s | Total | 12m59.29s || +0m51.84s --------------------------------------------------------------------------------------- 1m54.18s | Specific/IntegrationTestKaratsubaMul | 1m43.12s || +0m11.06s 1m38.97s | Specific/IntegrationTestLadderstep130 | 1m30.26s || +0m08.70s 2m19.75s | Specific/NISTP256/AMD64/femul | 2m14.08s || +0m05.66s 0m39.90s | Specific/IntegrationTestMontgomeryP256_128 | 0m34.21s || +0m05.68s 0m21.95s | Specific/NISTP256/AMD64/fesub | 0m19.23s || +0m02.71s 0m21.37s | Specific/NISTP256/AMD64/feadd | 0m18.82s || +0m02.55s 0m21.02s | Specific/X25519/C64/femul | 0m18.32s || +0m02.69s 0m20.53s | Specific/IntegrationTestFreeze | 0m23.26s || -0m02.73s 0m18.28s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m15.32s || +0m02.96s 0m18.20s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m15.52s || +0m02.67s 0m16.35s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m13.52s || +0m02.83s 0m13.92s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s || +0m02.08s 0m18.23s | Specific/NISTP256/AMD64/MontgomeryP256 | 0m16.62s || +0m01.60s 0m15.54s | Specific/IntegrationTestSub | 0m14.53s || +0m01.00s 0m14.78s | Specific/X25519/C64/fesquare | 0m13.13s || +0m01.64s 0m13.71s | Specific/NISTP256/AMD64/fenz | 0m12.69s || +0m01.02s 3m14.34s | Specific/X25519/C64/ladderstep | 3m14.32s || +0m00.02s 0m16.54s | Specific/NISTP256/AMD64/feopp | 0m16.48s || +0m00.05s 0m12.21s | Specific/MontgomeryP256_128 | 0m12.70s || -0m00.48s 0m00.73s | Specific/IntegrationTestTemporaryMiscCommon | 0m00.72s || +0m00.01s 0m00.64s | Specific/IntegrationTestDisplayCommon | 0m00.60s || +0m00.04s
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This closes #239 After | File Name | Before || Change --------------------------------------------------------------------------------------- 10m04.12s | Total | 10m05.68s || -0m01.55s --------------------------------------------------------------------------------------- 2m45.12s | Specific/X25519/C64/ladderstep | 2m48.45s || -0m03.32s 1m06.06s | Specific/IntegrationTestLadderstep130 | 1m04.76s || +0m01.29s 2m03.02s | Specific/NISTP256/AMD64/femul | 2m02.29s || +0m00.72s 1m20.35s | Specific/IntegrationTestKaratsubaMul | 1m20.10s || +0m00.25s 0m25.29s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.17s || +0m00.11s 0m16.66s | Specific/IntegrationTestFreeze | 0m16.18s || +0m00.48s 0m14.81s | Specific/NISTP256/AMD64/feadd | 0m15.09s || -0m00.27s 0m14.58s | Specific/NISTP256/AMD64/fesub | 0m14.48s || +0m00.09s 0m13.23s | Specific/X25519/C64/femul | 0m13.54s || -0m00.30s 0m12.00s | Specific/NISTP256/AMD64/feopp | 0m12.07s || -0m00.07s 0m11.25s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.44s || -0m00.18s 0m11.23s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.19s || +0m00.04s 0m11.06s | Specific/IntegrationTestSub | 0m11.24s || -0m00.17s 0m10.39s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.41s || -0m00.01s 0m09.85s | Specific/X25519/C64/fesquare | 0m09.75s || +0m00.09s 0m09.19s | Specific/NISTP256/AMD64/fenz | 0m09.04s || +0m00.15s 0m08.76s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.11s || -0m00.34s 0m00.69s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.11s 0m00.59s | Compilers/Z/Bounds/Pipeline | 0m00.57s || +0m00.02s
* Add cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
| | | | This way, files importing Core don't have to keep track of the list of runtime operations, for unfoling.
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
|
* Fix Demo.vGravatar Jason Gross2017-07-08
|
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
|
* More fine-grained importsGravatar Jason Gross2017-07-08
|
* Add UnfoldArgGravatar Jason Gross2017-07-08
|
* Fix CSE_sym denoteGravatar Jason Gross2017-07-07
|
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
|
* Stronger contextsGravatar Jason Gross2017-07-07
|
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
|
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
|
* prove ModularArithmeticTheorems admitsGravatar Andres Erbsen2017-07-06
|
* Curves/Edwards/Affine: prove point compression admitsGravatar Andres Erbsen2017-07-06
|
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
|
* make benchGravatar Andres Erbsen2017-07-06
|
* make benchGravatar Jason Gross2017-07-06
| | | | | | | | | | | | | | | ``` make -j test make -j -k bench touch capture.sh make -k bench sudo etc/turboboost.sh off sudo etc/hyperthreading.sh off touch capture.sh make -k bench sudo etc/turboboost.sh on sudo etc/hyperthreading.sh on ```
* Fix a typo that ends up not matteringGravatar Jason Gross2017-07-06
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 20:32:03 +0000