fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Significantly faster wordToN, I hope	Jason Gross	2016-10-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change -------------------------------------------------------------------------------------- 3m22.43s \| Total \| 3m22.13s \|\| +0m00.30s -------------------------------------------------------------------------------------- 0m34.51s \| Spec/Ed25519 \| 0m34.56s \|\| -0m00.05s 0m28.83s \| Experiments/Ed25519 \| 0m28.60s \|\| +0m00.22s 0m17.28s \| EdDSARepChange \| 0m17.25s \|\| +0m00.03s 0m08.66s \| [require-in-module,deprecated] src/Assembly/GF25519 \| 0m08.66s \|\| +0m00.00s 0m08.46s \| Encoding/PointEncoding \| 0m08.47s \|\| -0m00.00s 0m08.35s \| Specific/GF25519BoundedCommonWord \| 0m08.44s \|\| -0m00.08s 0m07.74s \| Specific/GF25519Reflective \| 0m07.69s \|\| +0m00.04s 0m07.59s \| Specific/GF25519Reflective/Reified/Mul \| 0m07.65s \|\| -0m00.06s 0m07.35s \| Specific/GF25519BoundedCommon \| 0m07.39s \|\| -0m00.04s 0m06.88s \| Specific/GF25519Reflective/Reified/Freeze \| 0m06.86s \|\| +0m00.01s 0m05.80s \| Bedrock/Word \| 0m05.74s \|\| +0m00.05s 0m05.43s \| Specific/SC25519 \| 0m05.32s \|\| +0m00.10s 0m04.76s \| Reflection/Z/Interpretations \| 0m04.65s \|\| +0m00.10s 0m04.27s \| Encoding/PointEncodingPre \| 0m04.31s \|\| -0m00.04s 0m03.72s \| Assembly/GF25519BoundedInstantiation \| 0m03.68s \|\| +0m00.04s 0m03.21s \| Specific/GF25519Reflective/Reified/CarrySub \| 0m03.34s \|\| -0m00.12s 0m02.91s \| Specific/GF25519Reflective/Reified/CarryOpp \| 0m02.86s \|\| +0m00.05s 0m02.84s \| Specific/GF25519Reflective/Reified/CarryAdd \| 0m02.87s \|\| -0m00.03s 0m02.70s \| Assembly/State \| 0m02.67s \|\| +0m00.03s 0m02.00s \| Specific/GF25519Reflective/Reified/Unpack \| 0m01.96s \|\| +0m00.04s 0m01.97s \| Specific/GF25519Reflective/Reified/Sub \| 0m01.95s \|\| +0m00.02s 0m01.95s \| Specific/GF25519Reflective/Reified/Pack \| 0m02.03s \|\| -0m00.07s 0m01.81s \| Assembly/Evaluables \| 0m01.88s \|\| -0m00.06s 0m01.78s \| Specific/GF25519Bounded \| 0m01.77s \|\| +0m00.01s 0m01.71s \| Specific/GF25519Reflective/Reified/Opp \| 0m01.68s \|\| +0m00.03s 0m01.66s \| Specific/GF25519Reflective/Reified/Add \| 0m01.66s \|\| +0m00.00s 0m01.52s \| Assembly/Compile \| 0m01.48s \|\| +0m00.04s 0m01.49s \| Specific/GF25519Reflective/Reified/GeModulus \| 0m01.48s \|\| +0m00.01s 0m01.44s \| Assembly/WordizeUtil \| 0m01.51s \|\| -0m00.07s 0m01.33s \| Assembly/Bounds \| 0m01.34s \|\| -0m00.01s 0m01.22s \| Assembly/Conversions \| 0m01.23s \|\| -0m00.01s 0m01.05s \| Util/WordUtil \| 0m01.03s \|\| +0m00.02s 0m00.94s \| Assembly/LL \| 0m00.94s \|\| +0m00.00s 0m00.94s \| Assembly/Pipeline \| 0m00.90s \|\| +0m00.03s 0m00.87s \| Assembly/HL \| 0m00.89s \|\| -0m00.02s 0m00.81s \| Assembly/PhoasCommon \| 0m00.77s \|\| +0m00.04s 0m00.79s \| Assembly/QhasmEvalCommon \| 0m00.83s \|\| -0m00.03s 0m00.75s \| Specific/GF25519Reflective/Reified \| 0m00.80s \|\| -0m00.05s 0m00.72s \| Specific/GF25519Reflective/Common \| 0m00.71s \|\| +0m00.01s 0m00.70s \| Encoding/ModularWordEncodingTheorems \| 0m00.65s \|\| +0m00.04s 0m00.66s \| Spec/EdDSA \| 0m00.66s \|\| +0m00.00s 0m00.61s \| Spec/ModularWordEncoding \| 0m00.58s \|\| +0m00.03s 0m00.61s \| Encoding/ModularWordEncodingPre \| 0m00.67s \|\| -0m00.06s 0m00.51s \| Assembly/Qhasm \| 0m00.51s \|\| +0m00.00s 0m00.48s \| Assembly/StringConversion \| 0m00.50s \|\| -0m00.02s 0m00.47s \| Assembly/QhasmUtil \| 0m00.40s \|\| +0m00.06s 0m00.36s \| Assembly/QhasmCommon \| 0m00.31s \|\| +0m00.04s
*	Silence a deprecation warning	Jason Gross	2016-07-20
\|
*	parenthesize Ltac [constr:] arguments	Andres Erbsen	2016-06-20
\|
*	Set Asymmetric Patterns	Jason Gross	2016-06-10
\|
*	Add coqprime that works with 8.5, bundle bedrock	Jason Gross	2016-06-10
	This simplifes the build process, and also allows us to try to build with 8.5. We autodetect the version of Coq in the Makefile to decide which version of coqprime to build.