Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Also git add in copy_bounds | 2016-11-25 | |
| | |||
* | uncurry_n_op_fe25519 | 2016-11-25 | |
| | |||
* | Various application lemmas | 2016-11-23 | |
| | |||
* | More GF25519ReflectiveCommon generalization | 2016-11-22 | |
| | |||
* | Add tuple lemmas | 2016-11-22 | |
| | |||
* | Add lemmas about application | 2016-11-22 | |
| | |||
* | Add impl_under_tower | 2016-11-22 | |
| | |||
* | Add hlistP | 2016-11-22 | |
| | |||
* | Add rhlist | 2016-11-22 | |
| | |||
* | Add interp_all_binders_for' | 2016-11-22 | |
| | |||
* | Add tower_nd | 2016-11-22 | |
| | |||
* | Fix for 8.6 | 2016-11-22 | |
| | |||
* | Copy bounds, fix a typo | 2016-11-22 | |
| | |||
* | Start work on a faster version of GF*Reflective/Common* | 2016-11-21 | |
| | |||
* | Fix for Coq 8.4 | 2016-11-21 | |
| | |||
* | Fix missing import for List.repeat in 8.4 | 2016-11-21 | |
| | |||
* | Don't let travis kill us in 10 minutes of silence | 2016-11-18 | |
| | |||
* | Better extraction | 2016-11-17 | |
| | |||
* | Copy bounds | 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 | 2016-11-17 | |
| | |||
* | Add add_coordinates_respectful_hetero | 2016-11-17 | |
| | |||
* | Remove an admit | 2016-11-17 | |
| | |||
* | Add fieldwise_map | 2016-11-17 | |
| | |||
* | Add another admitted lemma | 2016-11-17 | |
| | |||
* | Generalize add_coordinates | 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 | 2016-11-17 | |
| | | | | The lemma is currently admitted | ||
* | Add src/Specific/GF25519BoundedAddCoordinates.v | 2016-11-17 | |
| | |||
* | Add HList.mapt_Proper | 2016-11-17 | |
| | |||
* | Add ReflectiveAddCoordinates | 2016-11-17 | |
| | |||
* | Add some missing files | 2016-11-17 | |
| | |||
* | Fix some problems with previous commit | 2016-11-17 | |
| | |||
* | Remove admits, fill templates, copy bounds | 2016-11-17 | |
| | |||
* | Update AddCoordinates | 2016-11-17 | |
| | | | | Now the _correct_and_bounded lemma goes through | ||
* | Minor change in AddCoordinates | 2016-11-17 | |
| | |||
* | Add interpf_LetIn | 2016-11-17 | |
| | |||
* | Move util definitions to util folder | 2016-11-17 | |
| | |||
* | Copy reified add coordinates to various versions of curves | 2016-11-17 | |
| | |||
* | Add reified mostly-bounds-checked add_coordinates | 2016-11-17 | |
| | |||
* | Don't build 8.5pl{1,2} on travis | 2016-11-17 | |
| | | | | | | This will cancel out the timing increase of adding v8.5, v8.6. I've never seen 8.5 and 8.5pl3 succeed, while either 8.5pl1, or 8.5pl2 failed | ||
* | Add tip of 8.5, 8.6 to travis | 2016-11-17 | |
| | | | | Allow them to fail, though | ||
* | Update field names in SpecificGen | 2016-11-17 | |
| | |||
* | Move ExtendedAddCoordinates to new file, SpecGen | 2016-11-17 | |
| | |||
* | Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry | 2016-11-17 | |
| | |||
* | : assert is not valid 8.4 syntax | 2016-11-17 | |
| | |||
* | Work around bug #5205 (arguments naming weirdness) | 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 | 2016-11-16 | |
| | |||
* | Add Un{Return,Abs}_eta | 2016-11-16 | |
| | |||
* | Add : assert to a bunch of arguments | 2016-11-16 | |
| | | | | See https://coq.inria.fr/bugs/show_bug.cgi?id=5181#c3 | ||
* | Split fixedpoint in interpf | 2016-11-16 | |
| | |||
* | Add more things to Reflective/Common | 2016-11-16 | |
| | | | | Preparation for reflective add_coordinates |