aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* 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
* Update constants filesGravatar Jason Gross2017-09-21
|
* Add extract_ExprGravatar Jason Gross2017-09-21
|
* Split off tactics in IntegrationTestDisplayCommonGravatar Jason Gross2017-09-21
|
* Check if /sys/devices/system/cpu/intel_pstate/no_turbo exists before ↵Gravatar Jason Gross2017-09-16
| | | | searching it
* Drop test target on travisGravatar Jason Gross2017-09-16
| | | | It gives "illegal instruction" on p256
* Test `make bench` on travis.Gravatar Jason Gross2017-09-15
|
* Don't inline measure_helperGravatar Jason Gross2017-09-15
| | | | It breaks the ability to use bp in inline asm
* Allow bp in inline asm by tweaking measureGravatar Jason Gross2017-09-15
|
* Merge remote-tracking branch 'origin/master'Gravatar Jason Gross2017-09-15
|\
| * Use imul (not sure if it's better...)Gravatar Jason Gross2017-09-12
| | | | | | | | | | ... but that's what shows up on supercop: https://github.com/floodyberry/supercop/blob/master/crypto_scalarmult/curve25519/amd64-51/fe25519_mul.s#L164
* | Use imul (not sure if it's better...)Gravatar Jason Gross2017-09-12
|/
* make benchGravatar Jason Gross2017-09-12
|
* Preserved rbp, not rspGravatar Jason Gross2017-09-12
| | | | Apparently gcc accessess memory via rbp, according to objdump -D
* Don't claim to clobber rbpGravatar Jason Gross2017-09-12
| | | | gcc complains if we claim to clobber it
* Be better about asm syntax dialectsGravatar Jason Gross2017-09-12
| | | | | | | With some help from stackoverflow, https://stackoverflow.com/questions/46186592/how-do-i-refer-to-literal-registers-in-gcc-inline-assembly-in-att-syntax and https://stackoverflow.com/questions/46185788/how-can-i-pass-an-immediate-value-to-shr-in-assembly-in-intel-syntax
* Update register allocation moreGravatar Jason Gross2017-09-12
| | | | | Switch over to intel syntax, because I can't figure out how to name registers in AT&T / GAS.
* Update reg allocGravatar Jason Gross2017-09-12
|
* Update extract-function.sh for inline asmGravatar Jason Gross2017-09-12
| | | | | It needs to use printf rather than echo to not interpret \n, \t, and it needs to not insert { and } everywhere.
* Add reg alloc to rootGravatar Jason Gross2017-09-12
|
* Fix assemblyGravatar Jason Gross2017-09-12
|
* WIP on reg alloc for asm outputGravatar Jason Gross2017-09-11
|
* 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
|
* Fix (hopefully) overlap in regGravatar Jason Gross2017-09-05
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 10:34:39 +0000