fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock ↵	Samuel Gruetter	2018-02-05
\| \| \| \|	directory
*	Add wneg_inj	Jason Gross	2017-10-31
\|
*	Fix ZToWord, add wring_eq_ext, speed up some proofs	Jason Gross	2017-10-31
\|
*	Add Bedrock.Word.ZToWord	Jason Gross	2017-10-31
\|
*	Don't rely on autogenerated names	Jason Gross	2017-06-05
\| \| \| \| \| \|	This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
*	Revert "Fix a missing qualification"	Jason Gross	2017-01-21
\| \| \| \| \| \| \| \| \| \|	This reverts commit 3c4ff8fe8d2154addcf440690d315c58a529c1f6. Revert "Move weqb_hetero to Bedrock.Word" This reverts commit c83cb07f1477de33ce9eb43eea6a4f2720a94763. We probably shouldn't modify Bedrock.Word
*	Move weqb_hetero to Bedrock.Word	Jason Gross	2017-01-21
\|
*	Revert "Add Bedrock.Word.{wordToZ,ZToWord}"	Jason Gross	2017-01-03
\| \| \| \|	This reverts commit a66ba3e5202adcc436c3a1fcf6433261e7bdd158.
*	Add Bedrock.Word.{wordToZ,ZToWord}	Jason Gross	2017-01-03
\|
*	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.