fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	use [positive] for [F] modulus, char_ge_C instead of char_gt_C	Andres Erbsen	2017-03-02
\|
*	[F] has its own module now	Andres Erbsen	2016-08-05
\| \| \| \| \| \|	[ZToField] -> [F.of_Z] [FieldToZ] -> [F.to_Z] [Zmod.lem] -> [F.lem]
*	address code review comments	Andres Erbsen	2016-08-04
\|
*	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1
*	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.
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	Moved sign_bit definition to Spec.	jadep	2016-04-29
\|
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	Completed encoding reorganization; factored sign_bit out of PointEncodings ↵	jadep	2016-04-28
	and finished encoding admits.