fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix side-condition from previous commit	Jason Gross	2016-07-19
\|
*	Add another lemma to distr_length	Jason Gross	2016-07-19
\|
*	Use update_nth in add_to_nth (#26)	Jason Gross	2016-07-19
\| \| \| \| \| \|	It leads to a slightly more transparent and clearer definition. If I got everything right, nothing should depend on the judgmental definition of [add_to_nth] anymore.
*	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
\|
*	Add a lemma about base_from_limb_widths and app	Jason Gross	2016-07-18
\|
*	Move more proofs earlier	Jason Gross	2016-07-18
\|
*	Make Pow2BaseProofs independent of the def of add_to_nth	Jason Gross	2016-07-18
\|
*	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
\| \| \| \| \| \|	Also make much of the remaining code outside of Pow2BaseProofs independent of the precise definition of carry_simple. (We use [Local Opaque] to enforce this modularity.
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
\| \| \| \| \| \| \| \| \|	* Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
*	ported IterAssocOp to use monoid rather than a billion context variables ↵	jadep	2016-07-18
\| \| \| \|	that add up to a monoid
*	rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ↵	jadep	2016-07-18
\| \| \| \|	(bases that are repeats of the same power of 2) into Pow2Base
*	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
\|
*	removing experimental file accidentally included in last commit	jadep	2016-07-12
\|
*	pushing through a tweak to the arguments of [sub], and defining a field over ↵	jadep	2016-07-12
\| \| \| \|	ModularBaseSystemInterface using some placeholder operations.
*	Make [base] and [log_cap] notations	Jason Gross	2016-07-11
\| \| \| \| \| \| \| \|	Also use [ZUtil.Z.pow2_mod]. This lets us remove the dependency of ModularBaseSystem on ModularArithmetic.PseudoMersenneBaseParamProofs. This is a small part of reorganizing and factoring ModularBaseSystem for use with Barrett reduction.
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
* \|	ported Specific files to use ModularBaseSystemInterface	jadep	2016-07-11
\| \|
* \|	proved correctness of [add] operation in ModularBaseSystemInterface	jadep	2016-07-08
\| \|
* \|	defined some group operations, stated group lemma for tuple-based [add] (in ↵	jadep	2016-07-08
\| \| \| \| \| \| \| \|	terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor
* \|	added a few length proofs to ModularBaseSystemProofs to help with tuple ↵	jadep	2016-07-08
\| \| \| \| \| \| \| \|	conversion
* \|	unstuck carry_mul_opt_cps using from_list_default	jadep	2016-07-08
\| \|
\| *	Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.	jadep	2016-07-07
\| \|
\| *	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\| \|\
\| * \|	Factored out some proofs that rely only on base being powers of two, and ↵	jadep	2016-07-06
\| \| \| \| \| \| \| \| \| \| \| \|	defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
* \| \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
\| \| \|
* \| \|	add new interface to ModularBaseSystem	Andres Erbsen	2016-07-03
\| \| \|
* \| \|	remove PseudoMersenneRep	Andres Erbsen	2016-07-03
\| \| \|
\| \| *	Implement and prove Barrett reduction on Z (#18)	Jason Gross	2016-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia).
\| \| *	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.
\| *	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
\| \|
\| *	encode operation in ModularBaseSystem now uses bitwise operators, taking ↵	jadep	2016-06-29
\| \| \| \| \| \| \| \|	advantage of the fact that base elements are required to be powers of 2
\| *	BaseSystem encode function is no longer naive; it does a mod/div loop rather ↵	jadep	2016-06-28
\|/ \| \| \|	than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| \| \| \| \|	This prevents notation conflicts (see comment in Notations.v for more explanation).
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\ \| \| \| \| \| \|	includes broken files to be removed in next commit
\| *	[F q] is [Algebra.field]	Andres Erbsen	2016-06-20
\| \|
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵	Andres Erbsen	2016-06-18
\| \| \| \| \| \| \| \|	fewer nonzero ports. remove FField and FNsatz
* \|	Canonicalization is now automated in GF25519 and added to GF1305.	jadep	2016-06-17
\| \|
* \|	Specific version of freeze for GF25519 (automation still needs a little work)	jadep	2016-06-17
\| \|
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| \|
\| *	Z is integral domain	Andres Erbsen	2016-06-16
\| \|
* \|	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵	jadep	2016-06-15
\| \| \| \| \| \| \| \|	base-length digit vectors)
* \|	changed representation definition to require digits vector to be the exact ↵	jadep	2016-06-15
\| \| \| \| \| \| \| \|	length of the base vector
* \|	Added canonicalization to ModularBaseSystemOpt.	jadep	2016-06-15
\| \|
* \|	Merge	jadep	2016-06-14
\|\ \
* \| \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
\| \| \|
* \| \|	reversed modulus_digits and proved a few admits	jadep	2016-06-13
\| \| \|
* \| \|	progress on second stage (conditional constant-time subtraction) of ↵	jadep	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \|	canonicalization proofs
\| * \|	More Coq 8.4pl2 fixes	Jason Gross	2016-06-11
\| \| \|
* \| \|	starting rewrite using different definition of map	jadep	2016-06-11
\| \|/ \|/\|