fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Also git add in copy_bounds	Jason Gross	2016-11-25
\|
*	uncurry_n_op_fe25519	Jason Gross	2016-11-25
\|
*	Various application lemmas	Jason Gross	2016-11-23
\|
*	More GF25519ReflectiveCommon generalization	Jason Gross	2016-11-22
\|
*	Add tuple lemmas	Jason Gross	2016-11-22
\|
*	Add lemmas about application	Jason Gross	2016-11-22
\|
*	Add impl_under_tower	Jason Gross	2016-11-22
\|
*	Add hlistP	Jason Gross	2016-11-22
\|
*	Add rhlist	Jason Gross	2016-11-22
\|
*	Add interp_all_binders_for'	Jason Gross	2016-11-22
\|
*	Add tower_nd	Jason Gross	2016-11-22
\|
*	Fix for 8.6	Jason Gross	2016-11-22
\|
*	Copy bounds, fix a typo	Jason Gross	2016-11-22
\|
*	Start work on a faster version of GFReflective/Common	Jason Gross	2016-11-21
\|
*	Fix for Coq 8.4	Jason Gross	2016-11-21
\|
*	Fix missing import for List.repeat in 8.4	Jason Gross	2016-11-21
\|
*	Better extraction	Jason Gross	2016-11-17
\|
*	Copy bounds	Jason Gross	2016-11-17
\| \| \| \| \| \| \|	```bash $ pushd src/SpecificGen; pushd $ pushd && for i in *.json; do ./copy_bounds.sh $i; done && pushd ```
*	Finish proofs about eliminating useless carries	Jason Gross	2016-11-17
\|
*	Add add_coordinates_respectful_hetero	Jason Gross	2016-11-17
\|
*	Remove an admit	Jason Gross	2016-11-17
\|
*	Add fieldwise_map	Jason Gross	2016-11-17
\|
*	Add another admitted lemma	Jason Gross	2016-11-17
\|
*	Generalize add_coordinates	Jason Gross	2016-11-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is in preparation for dropping extra carries. What remains to be done, after this and #106, is to finish packaging up the reified [add_coordinates] so that it can operate on [Tuple.tuple GF25519BoundedCommon.fe25519 4], and then to prove ```coq forall twice_d P1 P2, Tuple.fieldwise GF25519BoundedCommon.eq (<reflected add_coordinates> twice_d P1 P2) (@ExtendedCoordinates.Extended.add_coordinates GF25519BoundedCommon.fe25519 GF25519Bounded.add GF25519Bounded.sub GF25519Bounded.mul twice_d P1 P2) ``` I'm not sure how to do this, or even what the right structure for the proof is.
*	Add GF25519BoundedExtendedAddCoordinates	Jason Gross	2016-11-17
\| \| \| \|	The lemma is currently admitted
*	Add src/Specific/GF25519BoundedAddCoordinates.v	Jason Gross	2016-11-17
\|
*	Add HList.mapt_Proper	Jason Gross	2016-11-17
\|
*	Add ReflectiveAddCoordinates	Jason Gross	2016-11-17
\|
*	Add some missing files	Jason Gross	2016-11-17
\|
*	Fix some problems with previous commit	Jason Gross	2016-11-17
\|
*	Remove admits, fill templates, copy bounds	Jason Gross	2016-11-17
\|
*	Update AddCoordinates	Jason Gross	2016-11-17
\| \| \| \|	Now the _correct_and_bounded lemma goes through
*	Minor change in AddCoordinates	Jason Gross	2016-11-17
\|
*	Add interpf_LetIn	Jason Gross	2016-11-17
\|
*	Move util definitions to util folder	Jason Gross	2016-11-17
\|
*	Copy reified add coordinates to various versions of curves	Jason Gross	2016-11-17
\|
*	Add reified mostly-bounds-checked add_coordinates	Jason Gross	2016-11-17
\|
*	Update field names in SpecificGen	Jason Gross	2016-11-17
\|
*	Move ExtendedAddCoordinates to new file, SpecGen	Jason Gross	2016-11-17
\|
*	Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry	Jason Gross	2016-11-17
\|
*	: assert is not valid 8.4 syntax	Jason Gross	2016-11-17
\|
*	Work around bug #5205 (arguments naming weirdness)	Jason Gross	2016-11-16
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5205, Bogus "Error: Wrong argument name: n." error message in 8.4, 8.5
*	Copy bounds to specific_gen	Jason Gross	2016-11-16
\|
*	Add Un{Return,Abs}_eta	Jason Gross	2016-11-16
\|
*	Add : assert to a bunch of arguments	Jason Gross	2016-11-16
\| \| \| \|	See https://coq.inria.fr/bugs/show_bug.cgi?id=5181#c3
*	Split fixedpoint in interpf	Jason Gross	2016-11-16
\|
*	Add more things to Reflective/Common	Jason Gross	2016-11-16
\| \| \| \|	Preparation for reflective add_coordinates
*	Arguments for Un{Return,Abs}	Jason Gross	2016-11-16
\|
*	Add add_coordinates_gen	Jason Gross	2016-11-16
\| \| \| \|	This in preparation for reifying add_coordinates
*	Add UnReturn, UnAbs	Jason Gross	2016-11-16
\|