Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add curve25519-donna-c64 to etc/third_party | Jason Gross | 2017-09-27 |
| | |||
* | Add femul,fesqure for C32 | Jason Gross | 2017-09-21 |
| | | | | | 32-bit ladderstep takes way too long (at least on Coq 8.6), so we don't add it yet | ||
* | Update extract-function.sh for inline asm | Jason Gross | 2017-09-12 |
| | | | | | It needs to use printf rather than echo to not interpret \n, \t, and it needs to not insert { and } everywhere. | ||
* | benchmark NISTZ256 with and without adx | Andres Erbsen | 2017-07-05 |
| | |||
* | fix .h dependencies in makefile (closes #235) | Andres Erbsen | 2017-07-05 |
| | |||
* | benchmarking: correct for differences in CPU and TSC frequency | Andres Erbsen | 2017-07-05 |
| | |||
* | use att style assembly with icc, test it | Andres Erbsen | 2017-07-04 |
| | |||
* | test p256 mixed addition | Andres Erbsen | 2017-07-04 |
| | | | | | passed after fixing some stupid typos in glue code -- no conceptual issues. | ||
* | fix mulx argument order using sed, test feadd, femul (fails due to #234) | Andres Erbsen | 2017-07-03 |
| | |||
* | X25519 test (passed on first try) | Andres Erbsen | 2017-07-02 |
| | |||
* | automate P256 integration | Andres Erbsen | 2017-07-02 |
| | |||
* | make bench: include all benchmarks | Andres Erbsen | 2017-07-01 |
| | |||
* | benchmark OpenSSL p256 C code | Andres Erbsen | 2017-07-01 |
| | |||
* | benchmark OpenSSL curve25519 | Andres Erbsen | 2017-07-01 |
| | |||
* | Add proper dependencies on .h file in Makefile | Jason Gross | 2017-06-29 |
| | |||
* | Make the same display on windows and linux | Jason Gross | 2017-06-28 |
| | | | | Do this by removing windows line endings via sed | ||
* | p256 compilation and benchmarks with manual kludges | Andres Erbsen | 2017-06-27 |
| | |||
* | Drop the two slowest files from the lite target | Jason Gross | 2017-06-26 |
| | |||
* | add openssl nistz256 for benchmarking | Andres Erbsen | 2017-06-23 |
| | |||
* | Makefile: c: h | Andres Erbsen | 2017-06-20 |
| | |||
* | don't key benchmarks on cpu frequency | Andres Erbsen | 2017-06-18 |
| | |||
* | measurements.txt depends on scripts that generate it | Andres Erbsen | 2017-06-18 |
| | |||
* | "make bench", currently just X25519-C64 (closes #185) | Andres Erbsen | 2017-06-18 |
| | |||
* | compile X25519 C code from Makefile | Andres Erbsen | 2017-06-18 |
| | |||
* | Don't make curves proofs on travis (hopefully fast enough build) | Jason Gross | 2017-06-17 |
| | |||
* | Fix notation-overriden warning issues | Jason Gross | 2017-06-15 |
| | | | | This change is necessary because we've added -compat 8.6. | ||
* | Add -compat 8.6 to _CoqProject | Jason Gross | 2017-06-15 |
| | | | | | | This allows fiat-crypto to continue working with trunk, after the merge of https://github.com/coq/coq/pull/220. We will remove this when we migrate to requiring 8.6.1 or 8.7 (neither of which is released yet). | ||
* | Add a printlite target to display lite files | Jason Gross | 2017-06-14 |
| | |||
* | Error if Makefile.vo_closure doesn't exist and we need it | Jason Gross | 2017-06-14 |
| | |||
* | Handle multiple lite-unmade-vofiles | Jason Gross | 2017-06-12 |
| | |||
* | Fix lite target (typo in makefile fn call) | Jason Gross | 2017-06-12 |
| | |||
* | Better support for coq_makefile2 with fewer warnings | Jason Gross | 2017-06-12 |
| | |||
* | Don't print directory when entering coqprime folder | Jason Gross | 2017-06-11 |
| | |||
* | Remove Karatsuba from the lite target | Jason Gross | 2017-06-09 |
| | | | | It was pretty slow. | ||
* | Compatibility with coq_makefile2 | Jason Gross | 2017-06-01 |
| | | | | Work harder to overwrite OTHERFLAGS if there's nothing there | ||
* | Add only-heavy target | Jason Gross | 2017-05-18 |
| | |||
* | specialize squaring earlier | Andres Erbsen | 2017-05-14 |
| | |||
* | s/appcontext/context/ | Jason Gross | 2017-05-11 |
| | | | | They mean the same thing since 8.5, and appcontext is deprecated. | ||
* | Track .dir-locals.el rather than generating it | Jason Gross | 2017-04-24 |
| | | | | | Since we're only using one version of coqprime, we no longer need to generate .dir-locals.el | ||
* | X25519: wrap synthesized code in donna-c64, run SUPERCOP benchmarks | Andres Erbsen | 2017-04-13 |
| | | | | | | | | | | | | | | | | 21% slower than donna 36% slower than assembly with saturated limbs. cycles impl compiler 593072 crypto_scalarmult/curve25519/amd64-64 gcc_-m64_-march=core-avx2_-O3_-fomit-frame-pointer 636660 crypto_scalarmult/curve25519/amd64-51 gcc_-funroll-loops_-fno-schedule-insns_-O2_-fomit-frame-pointer 660220 crypto_scalarmult/curve25519/donna_c64 gcc_-m64_-march=native_-mtune=native_-O3_-fomit-frame-pointer 804684 crypto_scalarmult/curve25519/fiat_c64 clang_-march=native_-O3_-fomit-frame-pointer_-fwrapv_-Qunused-arguments 815716 crypto_scalarmult/curve25519/fiat_c64 gcc_-m64_-march=core-avx2_-O3_-fomit-frame-pointer Setup: Broadwell i7-5600U 2.60GHz in an X1C3. no HT, no TB, wall power. Journalctl did not record any thermal throttling, idk if trustworthy. Cc: @achlipala @JasonGross @jadephilipoom | ||
* | Makefile fixes | Jason Gross | 2017-04-09 |
| | | | | | | | Fix the lite target to remove all transitive (reverse) dependencies. Don't run `coqtop` to get the version unless we're actually going to use it to build things | ||
* | Fix printreversedeps | Jason Gross | 2017-04-09 |
| | |||
* | Add printreversedeps | Jason Gross | 2017-04-09 |
| | |||
* | Display un-interped C code | Jason Gross | 2017-04-07 |
| | |||
* | Add Display files and targets | Jason Gross | 2017-04-07 |
| | |||
* | Ladderstep isn't *that* heavy | Jason Gross | 2017-04-07 |
| | |||
* | Add IntegrationTestLadderstep.v | Jason Gross | 2017-04-07 |
| | |||
* | Don't duplicate entries when updating _CoqProject | Jason Gross | 2017-04-07 |
| | | | | This can happen if you're in the middle of resolving a merge conflict (git ls-files will list some files twice). | ||
* | Clean up coq_makefile invocation | Jason Gross | 2017-04-06 |
| | | | | | We don't need that part of the `sed` command anymore, now that we no longer support 8.4. | ||
* | Add note to makefile | Jason Gross | 2017-04-03 |
| |