aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Add SmartFlatTypeMap_PairGravatar Jason Gross2017-10-14
|
* Fix a bug in CommonSubexpressionEliminationProperties.vGravatar Jason Gross2017-10-13
| | | | I'm very confused about how and when it was introduced...
* Add pow_ceil_mul_nat_divide_upperboundGravatar Jason Gross2017-10-13
|
* Support machines without controllable cpu speedGravatar Jason Gross2017-10-13
|
* Update smithers scriptGravatar Jason Gross2017-10-13
|
* add primes list andres scraped from curves at moderncrypto dot orgGravatar jadep2017-10-13
|
* add file input/output to json-generating scriptGravatar jadep2017-10-13
|
* add support for unsaturated limbs in json-generationGravatar jadep2017-10-13
|
* add examples to json-generation file for referenceGravatar jadep2017-10-13
|
* add script to generate json files given a primeGravatar jadep2017-10-13
|
* Add some SmartMap tuple lemmasGravatar Jason Gross2017-10-13
|
* Fix a spelling errorGravatar Jason Gross2017-10-13
|
* Factor out truncation_boundsGravatar Jason Gross2017-10-13
| | | | This makes it easier to extend the bounds analysis framework.
* Add comment to Compilers/Z/Bounds/Interpretation.vGravatar Jason Gross2017-10-13
| | | | | Hopefully this will help with extending the framework. Also remove [t_map4]; it was unused and didn't match the types of the other [t_mapn]s.
* Add some helper compilation lemmasGravatar Jason Gross2017-10-13
|
* Add reflective compose, notation for Z.Syntax.{Expr,Interp}Gravatar Jason Gross2017-10-12
|
* Allow test and bench to fail on travisGravatar Jason Gross2017-10-11
| | | | | | | | We now only build selected-test and selected-bench with one version of Coq (picked 8.7+beta2, because hopefully it'll be faster than 8.6.1). Previously, some travis builds failed because some travis machines don't support adc, adcx, mulx, etc.
* Add targets for no-curves-proofs-non-specific, and selected-specific,Gravatar Jason Gross2017-10-11
| | | | Also hopefully fix travis
* Smithers doesn't support -o pipefailGravatar Jason Gross2017-10-11
|
* Factor out -w "-notation-overridden" in MakefileGravatar Jason Gross2017-10-10
|
* Add etc/ci/smithers.sh for smithers testingGravatar Jason Gross2017-10-10
|
* More Makefile factoringGravatar Jason Gross2017-10-10
|
* Update Makefile by deduplicating some file listsGravatar Jason Gross2017-10-10
|
* Hopefully fix travisGravatar Jason Gross2017-10-10
| | | | | | Travis was too slow to run all of the coq target, so we split off the no-curves-proofs and the curves-proofs targets, and, while we're at it, also add 8.7+beta1 tests.
* 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
|
* Fix .dir-locals.el to work on WindowsGravatar Jason Gross2017-10-07
| | | | Previously, it was splitting on : and adding extra paths with, e.g., c:/
* 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
* [travis] trunk is now called masterGravatar Jason Gross2017-10-06
|
* Switch Coq {8.6 => 8.6.1} on travisGravatar Jason Gross2017-10-06
|
* Drop 8.5 travis buildGravatar Jason Gross2017-10-06
| | | | It's not useful, since we pass -compat 8.6
* Fix printenv sed script in Makefile for Windows supportGravatar Jason Gross2017-10-06
|
* 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
|
* Fix the printlite targetGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 22:04:37 +0000