fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fill in admits for field with carry_add, carry_opp, and carry_sub	jadep	2016-10-19
\|
*	Add fold_right_andb_true_iff_fold_right_and_True	Jason Gross	2016-10-19
\|
*	Fix broken [firstorder auto with *] >:-(	Jason Gross	2016-10-19
\|
*	Add Tuple.map2	Jason Gross	2016-10-19
\|
*	Define carry_opp in terms of carry_sub	Jason Gross	2016-10-19
\|
*	Add opt versions of add, sub, opp	Jason Gross	2016-10-19
\|
*	Fix for change in precedence of <-> vs -> in 8.4/8.5	Jason Gross	2016-10-19
\|
*	Fix out of memory error for 8.5,8.5pl1	Jason Gross	2016-10-19
\|
*	Work around out of memory error in 8.5, 8.5pl1	Jason Gross	2016-10-18
\|
*	Work around bug #5149 in 8.6 (broken subst, evars)	Jason Gross	2016-10-18
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5149, [subst] breaks evars in 8.6 (regression in the past week or two)
*	Fix for Coq 8.5, 8.5pl1	Jason Gross	2016-10-18
\|
*	Fix for Coq 8.4 evar propogation	Jason Gross	2016-10-18
\|
*	Fix missing imports	Jason Gross	2016-10-17
\|
*	Remove broken imports	Jason Gross	2016-10-17
\|
*	Rename and clean up exponent code	Jason Gross	2016-10-17
\|
*	Remove admits with the help of Andres	Jason Gross	2016-10-17
\|
*	Fill in more proofs	Jason Gross	2016-10-17
\|
*	Initial work on exponent field as Z	Jason Gross	2016-10-17
\|
*	Be more hesitant to [pose proof E.char_gt_2]	Jason Gross	2016-10-17
\| \| \| \|	This makes progress towards #75, #57, and compatiblity between versions of Coq
*	Don't let [tauto] destruct [Equivalence] in PE	Jason Gross	2016-10-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This makes progress towards #75 (now src/Experiments/Ed25519.v builds with both 8.4 and 8.5). Quoting [the changelog](https://github.com/coq/coq/blob/trunk/CHANGES#L576): > - Tactic "tauto" was exceptionally able to destruct other connectives than the binary connectives "and", "or", "prod", "sum", "iff". This non-uniform behavior has been fixed (bug #2680) and tauto is slightly weaker (possible source of incompatibilities). On the opposite side, new tactic "dtauto" is able to destruct any record-like inductive types, superseding the old version of "tauto". There was an `Equivalence` in the context that `tauto` was destructing, but otherwise not using. This made the proof pick up an extra dependency from the context in 8.4, but not 8.5/8.6.
*	Fix for 8.4 unification being unhappy in Ed25519 (nats are terrible)	Jason Gross	2016-10-17
\|
*	Various Ed25519 8.4 fixes	Jason Gross	2016-10-17
\|
*	Fix location of code in previous commit	Jason Gross	2016-10-17
\|
*	Add field by isomorphism	Jason Gross	2016-10-17
\|
*	Add more simplify lemmas to ZUtil	Jason Gross	2016-10-17
\|
*	Add more simplify lemmas to ZUtil	Jason Gross	2016-10-17
\|
*	Add ZUtil lemma	Jason Gross	2016-10-17
\|
*	Fix a proof	Jason Gross	2016-10-16
\|
*	Don't inline as much in ZBoundedZ	Jason Gross	2016-10-16
\|
*	Add Z as ZBounded	Jason Gross	2016-10-16
\|
*	Actually fix the exponential blowup (hopefully)	Jason Gross	2016-10-14
\| \| \| \| \|	This is a case where a variable was used in two places, and thus duplicated. Not sure if the other cases actually trigger.
*	Fix a typo in the previous commit	Jason Gross	2016-10-14
\|
*	Fix exponential blowup in some doubling ops	Jason Gross	2016-10-14
\| \| \| \|	Thanks @andres-erbsen !
*	Work around bug 5401 (bad let '(x, y))	Jason Gross	2016-10-13
\| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5140, destructuring let under binders of a class with an argument gives "Anomaly: index to an anonymous variable. Please report at http://coq.inria.fr/bugs/."
*	Revert "Eta-expand pairs in Eta.v"	Jason Gross	2016-10-13
\| \| \| \| \| \| \| \| \|	This reverts commit 778c1906711f68bed5760710712bb16eeb9c2365. It's not particularly useful, I think, and might be counterproductive; most of the unfolded pair projections in x86 are applied to variables, not instructions, and some instructions don't have pair projections directly applied to them.
*	Eta-expand pairs in Eta.v	Jason Gross	2016-10-13
\|
*	Unfold more things in eta	Jason Gross	2016-10-13
\|
*	Fix for Coq 8.4	Jason Gross	2016-10-13
\|
*	Add src/BoundedArithmetic/Eta.v	Jason Gross	2016-10-13
\|
*	refactor scalar multiplication thoery, implement SRepERepMul	Andres Erbsen	2016-10-12
\|
*	Fixed naming issue	jadep	2016-10-12
\|
*	defined sign operation on field elements	jadep	2016-10-12
\|
*	Fixing merge conflict	jadep	2016-10-12
\|
*	Clean up ge_modulus definition in Specific	jadep	2016-10-12
\|
*	Added top-level modulus comparison operation so field-element decoding can ↵	jadep	2016-10-12
\| \| \| \|	return None if input is greater than modulus
*	integrate bitwise operations	Andres Erbsen	2016-10-12
\|
*	generalize equiv relations in Util.Option and EdDSARepChange	Andres Erbsen	2016-10-12
\|
*	remove Experiments.EncodingLemmas (superseded by Jade's recent work)	Andres Erbsen	2016-10-12
\|
*	Add Ed25519 to _CoqProject	Jason Gross	2016-10-12
\|
*	Generalize and simplify cast_word_refl	Jason Gross	2016-10-12
\|