fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Move most notation level declarations into Util	Jason Gross	2016-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reveals and prevents notation clashes. Notable breakage: - `x {{ y }}` breaks `Context {forall x, {P x} + {~P x}}.` (@jadephilipoom) - `x [[ y ]]` breaks `destruct x as [[a]\|[b]].` (@jadephilipoom) - `O :( A , B ): :?: L ::: R` breaks `((1):nat)` and `constr:(nat)` (@varomodt) After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 3m16.07s \| Total \| 3m23.63s \|\| -0m07.55s ------------------------------------------------------------------------------------ 0m16.90s \| ModularArithmetic/ModularBaseSystemProofs \| 0m19.02s \|\| -0m02.12s 0m03.29s \| ModularArithmetic/ModularBaseSystemOpt \| 0m05.30s \|\| -0m02.00s 0m12.04s \| Experiments/SpecEd25519 \| 0m13.89s \|\| -0m01.85s 0m36.02s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m36.12s \|\| -0m00.09s 0m34.48s \| Specific/GF25519 \| 0m34.27s \|\| +0m00.20s 0m15.62s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m15.76s \|\| -0m00.14s 0m07.36s \| Specific/GF1305 \| 0m07.34s \|\| +0m00.02s 0m06.64s \| Algebra \| 0m06.14s \|\| +0m00.50s 0m05.12s \| WeierstrassCurve/Pre \| 0m05.09s \|\| +0m00.03s 0m04.58s \| ModularArithmetic/Tutorial \| 0m03.83s \|\| +0m00.75s 0m04.46s \| BaseSystemProofs \| 0m04.33s \|\| +0m00.12s 0m04.26s \| ModularArithmetic/Pow2BaseProofs \| 0m05.16s \|\| -0m00.90s 0m03.91s \| CompleteEdwardsCurve/Pre \| 0m04.62s \|\| -0m00.71s 0m02.75s \| Assembly/State \| 0m03.12s \|\| -0m00.37s 0m02.55s \| Experiments/EdDSARefinement \| 0m01.85s \|\| +0m00.69s 0m02.46s \| Util/ZUtil \| 0m02.45s \|\| +0m00.00s 0m01.86s \| Assembly/Wordize \| 0m02.02s \|\| -0m00.15s 0m01.68s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.68s \|\| +0m00.00s 0m01.67s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.96s \|\| -0m00.29s 0m01.50s \| Encoding/PointEncodingPre \| 0m02.20s \|\| -0m00.70s 0m01.46s \| ModularArithmetic/BarrettReduction/Z \| 0m01.02s \|\| +0m00.43s 0m01.26s \| BaseSystem \| 0m01.21s \|\| +0m00.05s 0m01.24s \| Assembly/Pseudize \| 0m01.22s \|\| +0m00.02s 0m01.20s \| ModularArithmetic/ExtendedBaseVector \| 0m01.86s \|\| -0m00.66s 0m01.04s \| Util/IterAssocOp \| 0m00.74s \|\| +0m00.30s 0m00.96s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.67s \|\| +0m00.28s 0m00.96s \| Assembly/Pipeline \| 0m00.65s \|\| +0m00.30s 0m00.93s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.98s \|\| -0m00.04s 0m00.93s \| ModularArithmetic/ModularBaseSystemField \| 0m00.95s \|\| -0m00.01s 0m00.92s \| Util/NumTheoryUtil \| 0m01.19s \|\| -0m00.26s 0m00.90s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.89s \|\| +0m00.01s 0m00.82s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.95s \|\| -0m00.13s 0m00.81s \| Assembly/QhasmEvalCommon \| 0m00.86s \|\| -0m00.04s 0m00.80s \| Assembly/StringConversion \| 0m00.60s \|\| +0m00.20s 0m00.79s \| Assembly/Qhasm \| 0m00.54s \|\| +0m00.25s 0m00.73s \| Assembly/Pseudo \| 0m00.98s \|\| -0m00.25s 0m00.72s \| Util/AdditionChainExponentiation \| 0m00.92s \|\| -0m00.20s 0m00.69s \| Experiments/SpecificCurve25519 \| 0m00.72s \|\| -0m00.03s 0m00.65s \| Spec/ModularWordEncoding \| 0m00.85s \|\| -0m00.19s 0m00.65s \| ModularArithmetic/ModularBaseSystemList \| 0m00.68s \|\| -0m00.03s 0m00.65s \| Assembly/PseudoConversion \| 0m00.67s \|\| -0m00.02s 0m00.64s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| +0m00.02s 0m00.64s \| Spec/EdDSA \| 0m00.93s \|\| -0m00.29s 0m00.64s \| Testbit \| 0m00.94s \|\| -0m00.29s 0m00.63s \| Encoding/ModularWordEncodingTheorems \| 0m00.66s \|\| -0m00.03s 0m00.62s \| Assembly/AlmostQhasm \| 0m00.49s \|\| +0m00.13s 0m00.59s \| ModularArithmetic/ModularBaseSystem \| 0m00.61s \|\| -0m00.02s 0m00.49s \| Spec/WeierstrassCurve \| 0m00.43s \|\| +0m00.06s 0m00.49s \| Assembly/QhasmUtil \| 0m00.51s \|\| -0m00.02s 0m00.49s \| ModularArithmetic/Pre \| 0m00.47s \|\| +0m00.02s 0m00.47s \| Assembly/Vectorize \| 0m00.51s \|\| -0m00.04s 0m00.46s \| Assembly/AlmostConversion \| 0m00.44s \|\| +0m00.02s 0m00.42s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| +0m00.00s 0m00.41s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.45s \|\| -0m00.04s 0m00.41s \| Spec/ModularArithmetic \| 0m00.41s \|\| +0m00.00s 0m00.39s \| Spec/CompleteEdwardsCurve \| 0m00.41s \|\| -0m00.01s 0m00.03s \| Util/Notations \| 0m00.03s \|\| +0m00.00s
*	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I do hereby revoke the privilege of [intuition] to grab random hints from random databases. This privilege is reserved for [debug_intuition], which comes with a warning about not being used in production code. This tactic is useful in conjunction with `Print Hint *`, to discover what hint databases the hints were grabbed from. (Suggestions for renaming [debug_intuition] welcome.) Any file using [intuition] must [Require Export Crypto.Util.FixCoqMistakes.]. It's possible we could lift this restriction by compiling [FixCoqMistakes] separately, and passing along `-require FixCoqMistakes` to Coq. Should we do this? After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 3m29.54s \| Total \| 4m33.13s \|\| -1m03.59s ------------------------------------------------------------------------------------ 0m03.75s \| BaseSystemProofs \| 0m43.84s \|\| -0m40.09s 0m42.57s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m34.48s \|\| +0m08.09s 0m03.04s \| Util/ListUtil \| 0m11.18s \|\| -0m08.14s 0m01.62s \| ModularArithmetic/PrimeFieldTheorems \| 0m09.53s \|\| -0m07.90s 0m00.87s \| Util/NumTheoryUtil \| 0m07.61s \|\| -0m06.74s 0m01.61s \| Encoding/PointEncodingPre \| 0m06.93s \|\| -0m05.31s 0m51.95s \| Specific/GF25519 \| 0m47.52s \|\| +0m04.42s 0m12.30s \| Experiments/SpecEd25519 \| 0m11.29s \|\| +0m01.01s 0m09.22s \| Specific/GF1305 \| 0m08.17s \|\| +0m01.05s 0m03.48s \| CompleteEdwardsCurve/Pre \| 0m04.77s \|\| -0m01.28s 0m02.70s \| Assembly/State \| 0m04.09s \|\| -0m01.38s 0m01.55s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.93s \|\| -0m01.38s 0m01.16s \| Assembly/Pseudize \| 0m02.34s \|\| -0m01.17s 0m15.67s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m16.37s \|\| -0m00.70s 0m06.02s \| Algebra \| 0m06.67s \|\| -0m00.65s 0m05.90s \| Experiments/GenericFieldPow \| 0m06.68s \|\| -0m00.77s 0m04.65s \| WeierstrassCurve/Pre \| 0m05.27s \|\| -0m00.61s 0m03.93s \| ModularArithmetic/Pow2BaseProofs \| 0m03.94s \|\| -0m00.00s 0m03.70s \| ModularArithmetic/Tutorial \| 0m03.85s \|\| -0m00.14s 0m02.83s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.84s \|\| -0m00.00s 0m02.74s \| Experiments/EdDSARefinement \| 0m01.80s \|\| +0m00.94s 0m02.35s \| Util/ZUtil \| 0m02.51s \|\| -0m00.15s 0m01.86s \| Assembly/Wordize \| 0m02.32s \|\| -0m00.45s 0m01.23s \| ModularArithmetic/ExtendedBaseVector \| 0m01.20s \|\| +0m00.03s 0m01.21s \| BaseSystem \| 0m01.63s \|\| -0m00.41s 0m01.03s \| Experiments/SpecificCurve25519 \| 0m00.98s \|\| +0m00.05s 0m01.01s \| ModularArithmetic/ModularBaseSystemProofs \| 0m01.11s \|\| -0m00.10s 0m00.95s \| ModularArithmetic/BarrettReduction/Z \| 0m01.38s \|\| -0m00.42s 0m00.92s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.81s \|\| -0m00.89s 0m00.85s \| ModularArithmetic/ModularBaseSystemField \| 0m00.86s \|\| -0m00.01s 0m00.82s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.79s \|\| +0m00.02s 0m00.80s \| Assembly/QhasmEvalCommon \| 0m00.93s \|\| -0m00.13s 0m00.73s \| Spec/EdDSA \| 0m00.59s \|\| +0m00.14s 0m00.72s \| Util/Tuple \| 0m00.71s \|\| +0m00.01s 0m00.70s \| Util/IterAssocOp \| 0m00.72s \|\| -0m00.02s 0m00.67s \| Encoding/ModularWordEncodingTheorems \| 0m00.71s \|\| -0m00.03s 0m00.66s \| Assembly/Pipeline \| 0m00.64s \|\| +0m00.02s 0m00.65s \| Testbit \| 0m00.65s \|\| +0m00.00s 0m00.65s \| Assembly/PseudoConversion \| 0m00.65s \|\| +0m00.00s 0m00.64s \| Util/AdditionChainExponentiation \| 0m00.63s \|\| +0m00.01s 0m00.63s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.64s \|\| -0m00.01s 0m00.63s \| Assembly/Pseudo \| 0m00.65s \|\| -0m00.02s 0m00.62s \| ModularArithmetic/ModularBaseSystem \| 0m00.57s \|\| +0m00.05s 0m00.61s \| ModularArithmetic/ModularBaseSystemList \| 0m00.57s \|\| +0m00.04s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.69s \|\| -0m00.08s 0m00.60s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.59s \|\| +0m00.01s 0m00.56s \| Assembly/StringConversion \| 0m00.56s \|\| +0m00.00s 0m00.54s \| Spec/ModularWordEncoding \| 0m00.61s \|\| -0m00.06s 0m00.54s \| Assembly/QhasmUtil \| 0m00.46s \|\| +0m00.08s 0m00.52s \| Assembly/Qhasm \| 0m00.53s \|\| -0m00.01s 0m00.48s \| Assembly/AlmostQhasm \| 0m00.52s \|\| -0m00.04s 0m00.48s \| ModularArithmetic/Pre \| 0m00.48s \|\| +0m00.00s 0m00.46s \| Assembly/Vectorize \| 0m00.72s \|\| -0m00.25s 0m00.45s \| Spec/WeierstrassCurve \| 0m00.44s \|\| +0m00.01s 0m00.44s \| Assembly/AlmostConversion \| 0m00.44s \|\| +0m00.00s 0m00.43s \| ModularArithmetic/Pow2Base \| 0m00.51s \|\| -0m00.08s 0m00.42s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.38s \|\| +0m00.03s 0m00.41s \| Spec/CompleteEdwardsCurve \| 0m00.43s \|\| -0m00.02s 0m00.34s \| Spec/ModularArithmetic \| 0m00.36s \|\| -0m00.01s 0m00.03s \| Util/FixCoqMistakes \| N/A \|\| +0m00.03s 0m00.02s \| Util/Notations \| 0m00.04s \|\| -0m00.02s 0m00.02s \| Util/Tactics \| 0m00.02s \|\| +0m00.00s
*	port CompleteEdwardsCurveTheorems (builds again)	Andres Erbsen	2016-07-11
\|
*	Proved lingering lemmas in PointEncodingPre.	jadep	2016-07-06
\|
*	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\|\
\| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The standard library uses Z., and Z and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
* \|	merging point encoding port	jadep	2016-06-24
\|\\|
* \|	Ported PointEncodings to parameterize over field rather than modulus.	jadep	2016-06-24
\| \|
\| *	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\| \|
\| *	Remove anything incompatible with new algebraic hierarcy	Andres Erbsen	2016-06-20
\|/ \| \| \| \| \|	- PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway
*	Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ↵	jadep	2016-05-25
\| \| \| \|	reason I wasn't affected. Also updated the same file to use E module.
*	Changed name of Encoding to CanonicalEncoding, and changed notation to match.	jadep	2016-04-29
\|
*	Moved sign_bit definition to Spec.	jadep	2016-04-29
\|
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	Completed encoding reorganization; factored sign_bit out of PointEncodings ↵	jadep	2016-04-28
\| \| \| \|	and finished encoding admits.
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
\|
*	Reorganization and revision of Encoding code and redefinition of sign_bit ↵	jadep	2016-04-25
\| \| \| \|	function.
*	proved most of point encoding admits, fixed some build system issues (dead ↵	Jade Philipoom	2016-02-16
	imports of PointFormats and Galois things)