fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
* \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
\|/
*	Add [specialize_by] tactic	Jason Gross	2016-07-01
\|
*	Fix field_algebra in 8.4	Jason Gross	2016-06-28
\|
*	Fix super_nsatz tactic to be better about ordering	Jason Gross	2016-06-28
\| \| \| \|	See also #13.
*	Add [destruct_head] tactics	Jason Gross	2016-06-27
\|
*	Add [break_match] for hypotheses	Jason Gross	2016-06-27
\|
*	Various nsatz and field tactic improvements	Jason Gross	2016-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 2m29.81s \| Total \| 2m34.05s \|\| -0m04.23s ------------------------------------------------------------------------------------ 0m11.98s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m15.22s \|\| -0m03.24s 0m29.71s \| ModularArithmetic/ModularBaseSystemProofs \| 0m30.05s \|\| -0m00.33s 0m29.12s \| Specific/GF25519 \| 0m29.12s \|\| +0m00.00s 0m21.50s \| Experiments/SpecEd25519 \| 0m21.43s \|\| +0m00.07s 0m18.20s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m18.24s \|\| -0m00.03s 0m07.36s \| Specific/GF1305 \| 0m07.33s \|\| +0m00.03s 0m06.66s \| Experiments/GenericFieldPow \| 0m06.89s \|\| -0m00.22s 0m03.84s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.84s \|\| +0m00.00s 0m03.82s \| ModularArithmetic/Tutorial \| 0m03.88s \|\| -0m00.06s 0m03.74s \| CompleteEdwardsCurve/Pre \| 0m03.81s \|\| -0m00.06s 0m02.30s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.27s \|\| +0m00.02s 0m02.11s \| ModularArithmetic/PrimeFieldTheorems \| 0m02.05s \|\| +0m00.06s 0m01.93s \| Algebra \| 0m02.06s \|\| -0m00.13s 0m01.17s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.19s \|\| -0m00.02s 0m01.13s \| ModularArithmetic/ExtendedBaseVector \| 0m01.18s \|\| -0m00.05s 0m01.01s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m01.07s \|\| -0m00.06s 0m00.61s \| Encoding/ModularWordEncodingTheorems \| 0m00.64s \|\| -0m00.03s 0m00.61s \| Spec/EdDSA \| 0m00.62s \|\| -0m00.01s 0m00.57s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| -0m00.05s 0m00.56s \| Spec/ModularWordEncoding \| 0m00.59s \|\| -0m00.02s 0m00.55s \| ModularArithmetic/ModularBaseSystem \| 0m00.59s \|\| -0m00.03s 0m00.52s \| ModularArithmetic/PseudoMersenneBaseRep \| 0m00.52s \|\| +0m00.00s 0m00.41s \| Tactics/Nsatz \| 0m00.41s \|\| +0m00.00s 0m00.38s \| Spec/CompleteEdwardsCurve \| 0m00.40s \|\| -0m00.02s 0m00.03s \| Util/Tactics \| 0m00.03s \|\| +0m00.00s
*	Improve some tactics and lemmas	Jason Gross	2016-06-23
\|
*	[break_match] should not be local	Jason Gross	2016-06-23
\|
*	Add tactics to Tactics, at most 2 sq-roots to Algebra	Jason Gross	2016-06-23
\|
*	Add a tactic for field inequalities	Jason Gross	2016-04-19
	Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.