Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 GF*Reflective/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 |