fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Admit Common9_4Op.v	Jason Gross	2016-12-08
\|
*	Don't use UIP in inversion_wff	Jason Gross	2016-12-03
\|
*	Add inversion_wff	Jason Gross	2016-12-03
\|
*	Add WfInversion	Jason Gross	2016-12-03
\|
*	More powerful inversion_option	Jason Gross	2016-12-03
\|
*	Move things to ExprInversion	Jason Gross	2016-12-03
\|
*	Add invert_Var	Jason Gross	2016-12-03
\|
*	Arguments for invert_Op	Jason Gross	2016-12-03
\|
*	Fewer autogenerated names	Jason Gross	2016-12-03
\|
*	Add invert_Op	Jason Gross	2016-12-03
\|
*	Change some default names	Jason Gross	2016-12-03
\|
*	copy_bounds.sh	Jason Gross	2016-12-02
\|
*	Fix looping in Coq 8.4 in ExtendedAddCoordinates.v	Jason Gross	2016-12-02
\|
*	Initial (not fully working) version of MapWithInterpInfo	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMapUnInterp	Jason Gross	2016-12-02
\|
*	Add invert_LetIn	Jason Gross	2016-12-02
\|
*	Arguments for invert_Pair	Jason Gross	2016-12-02
\|
*	Add invert_Pair	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMapInterp	Jason Gross	2016-12-02
\|
*	SmartFlatTypeMap arguments	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMap	Jason Gross	2016-12-02
\|
*	Minor change to inm_op_correct_and_bounded_prefix	Jason Gross	2016-11-25
\|
*	Fix a typo	Jason Gross	2016-11-25
\|
*	Add inm_op_correct_and_bounded_iff_prefix	Jason Gross	2016-11-25
\|
*	Add inm_op_correct_and_bounded	Jason Gross	2016-11-25
\|
*	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