fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Make arguments of InterpLinearize more implicit	Jason Gross	2017-11-17
\|
*	Add Interp{ExprEta,Linearize}_ind	Jason Gross	2017-11-17
\|
*	Update display logs and c files	Jason Gross	2017-11-17
\|
*	Add native_compute evar packages	Jason Gross	2017-11-16
\|
*	Add vm_compute_cbv_evar_package	Jason Gross	2017-11-16
\|
*	Add ModInv autosolver	Jason Gross	2017-11-16
\|
*	Update display logs and c files	Jason Gross	2017-11-16
\|
*	build src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.c	Andres Erbsen	2017-11-16
\|
*	Update display logs and c files	Jason Gross	2017-11-16
\|
*	Delete .gitignore	Jason Gross	2017-11-15
\|
*	Update display logs and c files	Jason Gross	2017-11-15
\|
*	Add a bunch of missing fesquare files	Jason Gross	2017-11-15
\| \| \| \| \|	I (or someone else?) forgot to `git add` them when invoking remake_curves.
*	build two montgomery files, including 32-bit p256	Andres Erbsen	2017-11-15
\|
*	Add MontgomeryAPI.encode and two lemmas about it	Jason Gross	2017-11-14
\| \| \| \|	One of them is Admitted.
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Add more constant notations	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-14
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update GeneralizeVar to ensure Wf	Jason Gross	2017-11-13
\| \| \| \| \|	This will hopefully pave the way for not needing to prove Wf anywhere in the bounds pipeline.
*	Add some convenience notations in Z.Syntax.Equality	Jason Gross	2017-11-13
\|
*	Revert "first batch benchmarks stash"	Andres Erbsen	2017-11-13
\| \| \| \|	This reverts commit b4a574666c0b7e9a761f95cfdafc7bb2f5e50cfc.
*	first batch benchmarks stash	Andres Erbsen	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Remove dead code for renaming binders	Jason Gross	2017-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change \| % Change ---------------------------------------------------------------------------------------------- 19m16.05s \| Total \| 21m25.28s \|\| -2m09.23s \| -10.05% ---------------------------------------------------------------------------------------------- 4m01.34s \| Specific/X25519/C64/ladderstep \| 4m59.49s \|\| -0m58.15s \| -19.41% 2m48.52s \| Specific/solinas32_2e255m765_13limbs/femul \| 3m12.95s \|\| -0m24.42s \| -12.66% 2m23.70s \| Specific/solinas32_2e255m765_12limbs/femul \| 2m44.11s \|\| -0m20.41s \| -12.43% 3m09.62s \| Specific/NISTP256/AMD64/femul \| 3m22.52s \|\| -0m12.90s \| -6.36% 0m36.32s \| Specific/X25519/C64/femul \| 0m39.50s \|\| -0m03.17s \| -8.05% 0m30.13s \| Specific/X25519/C64/fesquare \| 0m32.24s \|\| -0m02.11s \| -6.54% 0m35.40s \| Specific/NISTP256/AMD64/feadd \| 0m37.21s \|\| -0m01.81s \| -4.86% 0m31.50s \| Specific/X25519/C64/freeze \| 0m33.24s \|\| -0m01.74s \| -5.23% 0m24.99s \| Specific/X25519/C64/fecarry \| 0m26.31s \|\| -0m01.32s \| -5.01% 0m22.65s \| Specific/X25519/C64/fesub \| 0m23.72s \|\| -0m01.07s \| -4.51% 0m45.75s \| Specific/solinas32_2e255m765_13limbs/Synthesis \| 0m45.58s \|\| +0m00.17s \| +0.37% 0m39.59s \| Specific/NISTP256/AMD64/fesub \| 0m40.09s \|\| -0m00.50s \| -1.24% 0m36.92s \| Specific/solinas32_2e255m765_12limbs/Synthesis \| 0m36.64s \|\| +0m00.28s \| +0.76% 0m28.51s \| Specific/NISTP256/AMD64/feopp \| 0m29.46s \|\| -0m00.94s \| -3.22% 0m25.50s \| Specific/NISTP256/AMD64/fenz \| 0m26.41s \|\| -0m00.91s \| -3.44% 0m20.93s \| Specific/X25519/C64/feadd \| 0m21.41s \|\| -0m00.48s \| -2.24% 0m12.55s \| Specific/NISTP256/AMD64/Synthesis \| 0m12.54s \|\| +0m00.01s \| +0.07% 0m10.37s \| Specific/X25519/C64/Synthesis \| 0m10.30s \|\| +0m00.06s \| +0.67% 0m07.18s \| Compilers/Z/Bounds/Pipeline/Definition \| 0m07.22s \|\| -0m00.04s \| -0.55% 0m01.72s \| Compilers/Z/Bounds/Pipeline/ReflectiveTactics \| 0m01.58s \|\| +0m00.13s \| +8.86% 0m01.67s \| Specific/Framework/SynthesisFramework \| 0m01.72s \|\| -0m00.05s \| -2.90% 0m01.19s \| Compilers/Z/Bounds/Pipeline \| 0m01.04s \|\| +0m00.14s \| +14.42%
*	Make pipeline options more easily extensible	Jason Gross	2017-11-13
\| \| \| \| \|	Also add a dummy option about renaming binders, to be used in an upcoming commit.
*	Reflow comment	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|
*	Update display logs and c files	Jason Gross	2017-11-13
\|