aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* 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
* Add BITWIDTH=64 to extract-function.sh rule in MakefileGravatar Jason Gross2017-09-27
|
* Add example usageGravatar Jason Gross2017-09-27
|
* Update etc scripts to include governorGravatar Jason Gross2017-09-27
| | | | | | | | It needs to be in performance, not powersave, to work well on my machine. While we're at it, also have the scripts print usage if you pass no arguments, rather than giving an error message about $1 being unset.
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 08:16:12 +0000