fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	EdDSARefinement: work around rewrite_strat for 8.4	Andres Erbsen	2016-06-28
\|
*	Tuple: from_list_to_list	Andres Erbsen	2016-06-28
\|
*	Try a faster way of solving some inequalities resulting from common_denominator	Jason Gross	2016-06-27
\|
*	Actual fix for super_nsatz	Jason Gross	2016-06-27
\|
*	Fix super_nstaz to not error	Jason Gross	2016-06-27
\|
*	Add a super_nsatz tactic	Jason Gross	2016-06-27
\|
*	eddsa refinement setup	Andres Erbsen	2016-06-27
\|
*	Add [destruct_head] tactics	Jason Gross	2016-06-27
\|
*	Update .mailmap with email from 3c36b589a01bce19063872544bca132f3daf947d	Jason Gross	2016-06-27
\|
*	Merge pull request #9 from mit-plv/folkwisdom	Andres Erbsen	2016-06-27
\|\ \| \| \| \|	Document "folk wisdom" tips that would have been good to know
\| *	Update folkwisdom.md	Andres Erbsen	2016-06-27
\| \|
* \|	Add [break_match] for hypotheses	Jason Gross	2016-06-27
\| \|
* \|	Update .gitignore	Jason Gross	2016-06-27
\| \|
* \|	Add decidable instances for sumwise and fieldwise	Jason Gross	2016-06-27
\| \|
* \|	Add a tactic for dealing with equalities of [sum]	Jason Gross	2016-06-27
\| \|
* \|	Fix notation level	Jason Gross	2016-06-27
\| \|
* \|	Add global notation for eq_dec	Jason Gross	2016-06-27
\| \|
* \|	scalarmult support; EdDSA.sign produces valid signatures	Andres Erbsen	2016-06-27
\| \|
* \|	first pass of scalarmult	Andres Erbsen	2016-06-27
\| \|
* \|	Add a tactic to handle "at most two square roots"	Jason Gross	2016-06-27
\| \|
* \|	Test 8.5 and 8.5pl1 on travis	Jason Gross	2016-06-27
\| \| \| \| \| \| \| \| \| \|	Now that I've finally managed to get packages built for both of these versions of Coq on my ppa...
\| *	actually fix pose proof	Andres Erbsen	2016-06-25
\| \|
\| *	s/fist/first/	Andres Erbsen	2016-06-25
\| \|
\| *	s/`proofgeneral`/Proof General/	Andres Erbsen	2016-06-25
\| \|
\| *	recommend pose proof instead of pose	Andres Erbsen	2016-06-25
\| \|
\| *	s/on//	Andres Erbsen	2016-06-25
\| \|
\| *	add closing parenthesis to "(and make"	Andres Erbsen	2016-06-25
\| \|
\| *	s/quality/equality/	Andres Erbsen	2016-06-25
\| \|
\| *	s/be//	Andres Erbsen	2016-06-25
\| \|
\| *	typo near "and make and"	Andres Erbsen	2016-06-25
\| \|
\| *	wording change near "split this up"	Andres Erbsen	2016-06-25
\| \|
\| *	add sigma type proof irrelevance wisdom from ssreflect	Andres Erbsen	2016-06-25
\| \|
* \|	Fix for Coq 8.4	Jason Gross	2016-06-25
\| \|
* \|	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
\| \|
* \|	Update mailmap	Jason Gross	2016-06-25
\| \|
* \|	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
* \|	Add a version of common_denominator w/o oversimpl	Jason Gross	2016-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	It first [set]s anything not containing a division. Unfortunately, it's not a good drop-in replacement, because some code relies on exactly how [field_simplify] calls [field_simplify_eq] >.<
* \|	Remove a useless intro	Jason Gross	2016-06-24
\| \|
* \|	ExtendedCoordinates: group.	Andres Erbsen	2016-06-24
\| \|
\| *	folkwisdom: remove redundant idtac	Andres Erbsen	2016-06-24
\| \|
* \|	isomorphism_to_subgroup_group	Andres Erbsen	2016-06-24
\| \|
* \|	Use Decidable machinery for is_eq_dec	Jason Gross	2016-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows us to rely entirely on typeclass resolution to resolve these instances, without having to do ad-hoc things for [and]. After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 2m21.71s \| Total \| 2m22.59s \|\| -0m00.87s ------------------------------------------------------------------------------------ 0m28.82s \| Specific/GF25519 \| 0m29.86s \|\| -0m01.03s 0m29.60s \| ModularArithmetic/ModularBaseSystemProofs \| 0m29.40s \|\| +0m00.20s 0m21.25s \| Experiments/SpecEd25519 \| 0m21.28s \|\| -0m00.03s 0m18.15s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m18.14s \|\| +0m00.00s 0m11.95s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m11.94s \|\| +0m00.00s 0m07.26s \| Specific/GF1305 \| 0m07.28s \|\| -0m00.02s 0m03.77s \| ModularArithmetic/Tutorial \| 0m03.75s \|\| +0m00.02s 0m03.76s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.75s \|\| +0m00.00s 0m03.61s \| CompleteEdwardsCurve/Pre \| 0m03.63s \|\| -0m00.02s 0m02.15s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.12s \|\| +0m00.02s 0m01.88s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.89s \|\| -0m00.01s 0m01.75s \| Algebra \| 0m01.73s \|\| +0m00.02s 0m01.21s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.17s \|\| +0m00.04s 0m01.14s \| ModularArithmetic/ExtendedBaseVector \| 0m01.14s \|\| +0m00.00s 0m01.01s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.98s \|\| +0m00.03s 0m00.62s \| Encoding/ModularWordEncodingTheorems \| 0m00.63s \|\| -0m00.01s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.61s \|\| -0m00.01s 0m00.59s \| Util/Decidable \| 0m00.64s \|\| -0m00.05s 0m00.58s \| Spec/EdDSA \| 0m00.61s \|\| -0m00.03s 0m00.57s \| ModularArithmetic/ModularBaseSystem \| 0m00.61s \|\| -0m00.04s 0m00.56s \| Spec/ModularWordEncoding \| 0m00.56s \|\| +0m00.00s 0m00.51s \| ModularArithmetic/PseudoMersenneBaseRep \| 0m00.53s \|\| -0m00.02s 0m00.37s \| Spec/CompleteEdwardsCurve \| 0m00.34s \|\| +0m00.02s
\| *	incorporate `Program Definition` match statement handling advice from @mattam82	Andres Erbsen	2016-06-24
\| \|
\| *	first draft of a "folk wisdom" document	Andres Erbsen	2016-06-24
\|/
*	nsatz_contradict can now handle invalid _ <> _ hypotheses	Jason Gross	2016-06-23
\|
*	Update _CoqProject	Jason Gross	2016-06-23
\|
*	Add Unit.v	Jason Gross	2016-06-23
\|
*	Add equality on sum types	Jason Gross	2016-06-23
\|
*	Merge pull request #8 from mit-plv/rsloan-pipeline-example-init	Jason Gross	2016-06-23
\|\ \| \| \| \|	Make Pipeline.v Build on 8.4
\| *	Remove examples for 8.4 compatibility	Robert Sloan	2016-06-23
\| \|