fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Moved sign_bit definition to Spec.	jadep	2016-06-22
\|
*	Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to	jadep	2016-06-22
\| \| \| \|	comparing points).
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-06-22
\| \| \| \|	general contexts.
*	Completed encoding reorganization; factored sign_bit out of PointEncodings ↵	jadep	2016-06-22
\| \| \| \|	and finished encoding admits.
*	ed25519: solve elliptic curve math admits	Andres Erbsen	2016-06-22
\|
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-06-22
\|
*	refactor field lemmas out of ed25519	Andres Erbsen	2016-06-22
\|
*	reduce admits related to point negation	Andres Erbsen	2016-06-22
\|
*	Reorganization and revision of Encoding code and redefinition of sign_bit ↵	jadep	2016-06-22
\| \| \| \|	function.
*	Update to_gallina.md	jadep	2016-06-22
\|
*	point_eq_dec	Andres Erbsen	2016-06-22
\|
*	finished last cases of nonzero proofs for associativity	jadep	2016-06-22
\|
*	wrote up remaining tasks needed for Gallina code (from board at 04/19 meeting)	jadep	2016-06-22
\|
*	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵	jadep	2016-06-22
\| \| \| \|	weight 2^26)
*	automated most of the code in GF25519	jadep	2016-06-22
\|
*	Cleanup of GF25519	jadep	2016-06-22
\|
*	Pulled generalized code out of GF25519 so that it can be used for other moduli	jadep	2016-06-22
\|
*	moved lemmas from ModularBaseSystemProofs to various Util files	jadep	2016-06-22
\|
*	GF25519 addition	jadep	2016-06-22
\|
*	GF25519: boring stuff -- fixed indentation and removed commented-out code	jadep	2016-06-22
\|
*	Add a tactic for field inequalities	Jason Gross	2016-06-22
\| \| \| \| \|	Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.
*	ed25519 derivation: down to final encoding	Andres Erbsen	2016-06-22
\|
*	ed25519 derivation: use representation of F	Andres Erbsen	2016-06-22
\|
*	ed25519 derivation: wrangle non-unique representations	Andres Erbsen	2016-06-22
\|
*	ed25519 derivation: stuck at main loop	Andres Erbsen	2016-06-22
\|
*	ed25519 derivation down to word until main equation	Andres Erbsen	2016-06-22
\|
*	Defined a testbit variant for BaseSystem vectors and proved equivalence to ↵	jadep	2016-06-22
\| \| \| \|	Z.testbit.
*	Added lemmas to Util/ that are needed for testbit.	jadep	2016-06-22
\|
*	Cleaned up and revised DoubleAndAdd.	jadep	2016-06-22
\|
*	Removed old iter_op version and its last dependency.	jadep	2016-06-22
\|
*	Retrieved updated version of Util/IterAssocOp and modified ↵	jadep	2016-06-22
\| \| \| \|	ExtendedCoordinates and Ed25519 to use it.
*	Fixed syntax error (missing bracket) in Ed25519 to make merge build	jadep	2016-06-22
\|
*	Fix freshen-bedrock-files.sh	Jason Gross	2016-06-22
\| \| \| \|	Previously, it was not actually recording when it found things.
*	ed25519: continue derivation	Andres Erbsen	2016-06-22
\|
*	Finished refactor of GF25519 (partial evaluation); code builds but needs to ↵	jadep	2016-06-22
\| \| \| \|	be reorganized, since many of the theorems in GF25519 are now generalized and do not need to be in Specific/.
*	Reverting Util/IterAssocOp to an earlier version for compatibility with ↵	jadep	2016-06-22
\| \| \| \|	CompleteEdwardsCurve/ExtendedCoordinates (we don't have testbit defined yet)
*	Merge and refactor of GF25519	jadep	2016-06-22
\|
*	Drop second projections in Ed25519	Jason Gross	2016-06-22
\|
*	fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParams	Jade Philipoom	2016-06-22
\|
*	made BaseVector instance global	Jade Philipoom	2016-06-22
\|
*	refactor of Basesystem and ModularBaseSystem; includes general code ↵	Jade Philipoom	2016-06-22
\| \| \| \|	organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division
*	Refactored BaseSystem and ModularBaseSystem.	Jade Philipoom	2016-06-22
\|
*	IterAssocOp: now uses arbitrary representation of scalar that implements testbit	Jade Philipoom	2016-06-22
\|
*	IterAssocOp : now takes a bound argument instead of just using size of exponent	Jade Philipoom	2016-06-22
\|
*	Full pipeline working again	Robert Sloan	2016-06-22
\|
*	Huge Language / Conversion refactors	Robert Sloan	2016-06-22
\|
*	More refactors that will make this whole thing very unstable	Robert Sloan	2016-06-22
\|
*	Running PipelineExample	Robert Sloan	2016-06-22
\|
*	Parsing portion of StringConversion	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \|	Running PipelineExample Running PipelineExample Running PipelineExample
*	AlmostConversion and part of StringConversion	Robert Sloan	2016-06-22
\| \| \| \|	Parsing portion of StringConversion