fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	tweak to NumTheoryUtil so it builds on older Coq versions	Jade Philipoom	2016-06-22
\|
*	CompleteEdwardsCurveTheorems: associativity proof that times out on Qed	Andres Erbsen	2016-06-22
\|
*	Instance Fq_Integral_domain : @Integral_domain (F q) ...	Andres Erbsen	2016-06-22
\|
*	ModularArithmetic: [field] tactic that respects opacity, prettify ↵	Andres Erbsen	2016-06-22
\| \| \| \|	ExtendedCoordinates, outline Edwards curve associativity
*	Makefile: single-quotes for shell globbing	Andres Erbsen	2016-06-22
\|
*	generic binary exponentiation correctness proof in 3 one-liners	Andres Erbsen	2016-06-22
\|
*	ModularArithmetic: reasonable-time FieldToZ inv implementation	Andres Erbsen	2016-06-22
\|
*	Automate a UList proof a bit so it builds with 8.5	Jason Gross	2016-06-22
\| \| \| \|	It still builds with 8.4
*	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-06-22
\| \| \| \|	Also move a definition about words, with a TODO about location, into WordUtil.
*	Update Coqprime/UList	Jason Gross	2016-06-22
\| \| \| \| \|	Ambiguous imports, oh joy! (Coqprime failed to build when Bedrock was in COQPATH.)
*	Add etc/freshen-bedrock-files.sh	Jason Gross	2016-06-22
\| \| \| \| \| \|	It is used on smithers to remove .vo files which are older than relevant Bedrock .vo files. This prevents version mismatches when updating Bedrock on smithers.
*	cleanup of bounded iter_op	Jade Philipoom	2016-06-22
\|
*	reasonable version	Robert Sloan	2016-06-22
\|
*	remove bedrock from COQ_ARGS because we all use COQPATH	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \|	BoundedWord2 Factor out a tactic and add more examples BoundedWord2: add test cases intermediate stage simple
*	efficient powmod	Andres Erbsen	2016-06-22
\|
*	update ModularArithmetic tutorial	Andres Erbsen	2016-06-22
\|
*	removed Print Assumptions	Jade Philipoom	2016-06-22
\|
*	proved sqrt_solutions, the last remaining admit for point encodings	Jade Philipoom	2016-06-22
\|
*	moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵	Jade Philipoom	2016-06-22
\| \| \| \|	CompleteEdwardsCurve, where the precondition is not in scope.
*	proved most of point encoding admits, fixed some build system issues (dead ↵	Jade Philipoom	2016-06-22
\| \| \| \|	imports of PointFormats and Galois things)
*	added point encodings; some admits remain	Jade Philipoom	2016-06-22
\|
*	cleaned up and ported definition to solve for x ^ 2 in the curve equation	Jade Philipoom	2016-06-22
\|
*	EdDSA: tweaked l_bound	Jade Philipoom	2016-06-22
\|
*	fixed renamed files and added imports for encodings	Jade Philipoom	2016-06-22
\|
*	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-06-22
\|
*	remove Check	Andres Erbsen	2016-06-22
\|
*	instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ↵	Jade Philipoom	2016-06-22
\| \| \| \|	the commit looks huge)
*	added generic encoding spec	Jade Philipoom	2016-06-22
\|
*	moved two non-primality-dependent lemmas to ModularArithmeticTheorems from ↵	Jade Philipoom	2016-06-22
\| \| \| \|	PrimeFieldTheorems
*	a few lemmas in util about powers of 2 in Bedrock's various rewritten forms	Jade Philipoom	2016-06-22
\|
*	port bounded iter_op and Edwards doubleAndAdd	Andres Erbsen	2016-06-22
\|
*	CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context	Andres Erbsen	2016-06-22
\|
*	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-06-22
\|
*	added square roots and an assortment of lemmas about prime fields/rings	Jade Philipoom	2016-06-22
\|
*	changed the name of the ring to ring, not field	Jade Philipoom	2016-06-22
\|
*	tweaks to util files, including automation for proving ↵	Jade Philipoom	2016-06-22
\| \| \| \|	positivity/nonnegativity in Z
*	update F Coercions and tutorial	Andres Erbsen	2016-06-22
\|
*	port ModularBaseSystem.v and GF25519.v to F m	Andres Erbsen	2016-06-22
\|
*	Spec/EdDSA: comments, remove prehashing	Andres Erbsen	2016-06-22
\|
*	Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v	Andres Erbsen	2016-06-22
\|
*	prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd ↵	Andres Erbsen	2016-06-22
\| \| \| \|	Closed Under Global Context
*	EdDSA spec ported over to new field implementation	Jade Philipoom	2016-06-22
\|
*	EdDSA25519: progress on proving PointEncoding admits; code still unorganized	Jade Philipoom	2016-06-22
\|
*	implement F_opp	Andres Erbsen	2016-06-22
\|
*	workaround field with typeclass modulus	Andres Erbsen	2016-06-22
\|
*	fix imports	Andres Erbsen	2016-06-22
\|
*	document field issue re-appearing	Andres Erbsen	2016-06-22
\|
*	port some edwards curve theorems	Andres Erbsen	2016-06-22
\|
*	make field on F automatically clean up the constant-vomit it expands	Andres Erbsen	2016-06-22
\|
*	port some Edwards curve stuff from GF to F	Andres Erbsen	2016-06-22
\|