fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Not quite done with WordUtil lemmas.	Robert Sloan	2016-11-08
\|\
* \|	More of jgross admits, less neg and the cmovs	Rob Sloan	2016-11-01
\| \|
* \|	most of jgross' admits	Rob Sloan	2016-10-31
\| \| \| \| \| \| \| \|	'
\| *	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
*	More of the Conversions.v correctness proofs	Robert Sloan	2016-10-14
\|
*	Making sub bounds actually tight	Robert Sloan	2016-10-14
\|
*	Removed nat arguments to Evaluable operations	Robert Sloan	2016-08-25
\|
*	Experimental requirements for rsloan-phoas	Robert Sloan	2016-08-23