Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update display logs and c files | 2017-11-12 | |
| | |||
* | Add more constant notations | 2017-11-12 | |
| | |||
* | Update display logs and c files | 2017-11-12 | |
| | |||
* | Add more constant notations | 2017-11-12 | |
| | |||
* | andres doesn't know what year it is | 2017-11-12 | |
| | |||
* | Add autosolve admit package | 2017-11-12 | |
| | |||
* | Remove outdated C128 files | 2017-11-12 | |
| | |||
* | add reflexivity to reify autosolve | 2017-11-12 | |
| | |||
* | Use abstract in ring autosolve | 2017-11-12 | |
| | |||
* | add back incorrectly deleted files | 2017-11-12 | |
| | |||
* | automatic modifications to _Coqproject with new files | 2017-11-12 | |
| | |||
* | new autogenerated files | 2017-11-12 | |
| | |||
* | update remake-curves.sh and Makefile | 2017-11-12 | |
| | |||
* | changes to parameter-generation script | 2017-11-12 | |
| | |||
* | fix comment | 2017-11-12 | |
| | |||
* | benchmark montgomery32, gmpvar, and gmpsec on 32-bit android | 2017-11-11 | |
| | | | | | | | | Despite significant effort, I did not manage to compiler gmpxx in a way that would allow it to be dynamically linked with the c++ standard library on android, or statically link the library in a way that would result in a file executable on Android. Somebody who understands C and Android dynamic linking might be able to do better. | ||
* | Add Decidable2Bool | 2017-11-11 | |
| | |||
* | Add ListUtil.Forall | 2017-11-11 | |
| | |||
* | First intro and split in Zring_prod_eq_tac, before cbv - | 2017-11-11 | |
| | |||
* | Also unfold tuple for reification | 2017-11-11 | |
| | |||
* | Update display logs and c files | 2017-11-10 | |
| | |||
* | Update display logs and c files | 2017-11-10 | |
| | |||
* | Update display logs and c files | 2017-11-10 | |
| | |||
* | Handle more base types in Z.Reify | 2017-11-10 | |
| | |||
* | Add more fine-grained cmovnz notations | 2017-11-10 | |
| | | | | | | Builds, but haven't tested the output This closes #265 | ||
* | benchmark solinas32 on a 32-bit processor | 2017-11-10 | |
| | |||
* | More modularity in autosolve | 2017-11-10 | |
| | |||
* | first benchmark on 32-bit Android | 2017-11-10 | |
| | |||
* | Handle tuples in reification | 2017-11-10 | |
| | |||
* | Add unfold_flat_interp_tuple | 2017-11-10 | |
| | |||
* | Use match in flat_interp_{,un}tuple' | 2017-11-10 | |
| | | | | | | This way, when we unfold them, we don't create multiple copies of the argument. This is needed for proper reification of x25519 alternate mul, square code in the new pipeline | ||
* | Separate case for handling option matches in autosolve | 2017-11-10 | |
| | |||
* | Add cbn [val] in autosolve | 2017-11-10 | |
| | |||
* | Update make_curve.py for python3 | 2017-11-10 | |
| | | | | | | In python2, we require unicode. In python3, "unicode" as a type doesn't exist. So we do a feature-check-kludge to set unicode to str if it doesn't exist. | ||
* | Revert "Update make_curve.py for python3" | 2017-11-10 | |
| | | | | | | This reverts commit a5fc7539c5688190f7622266c8e0959efbca80be. Didn't actually work | ||
* | Update make_curve.py for python3 | 2017-11-10 | |
| | | | | | | | | In python2, we require unicode. In python3, "unicode" as a type doesn't exist. In most places, we can replace the isinstance check for str/unicode with basestring. In one place where we need to output unicode, we do a terrible hack to set unicode to str if it doesn't exist. | ||
* | Fix opacity of dec_Forall, dec_Exists | 2017-11-10 | |
| | |||
* | Add dec_if_bool | 2017-11-10 | |
| | |||
* | Generalize Tuple.dec_fieldwise | 2017-11-09 | |
| | |||
* | Generalize Forall2_forall_iff | 2017-11-09 | |
| | |||
* | More generalization of fieldwise'_Proper to dependent types | 2017-11-09 | |
| | |||
* | Generalize fieldwise Proper lemmas | 2017-11-09 | |
| | |||
* | Remove from the lite target the slowest file currently in it | 2017-11-09 | |
| | | | | It takes 7m29.22s on Travis | ||
* | Add fieldwise_lift_and | 2017-11-09 | |
| | |||
* | Add more versions of fieldwise_Proper | 2017-11-09 | |
| | |||
* | Add fieldwise_Proper | 2017-11-09 | |
| | |||
* | Add fieldwise_eq_iff | 2017-11-09 | |
| | |||
* | Add dec_Forall, dec_Exists | 2017-11-09 | |
| | |||
* | Add fieldwise_map_from_list_iff | 2017-11-09 | |
| | |||
* | Fix another side condition issue | 2017-11-08 | |
| |