Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add more constant notations | 2017-11-13 | |
| | |||
* | More granularity in src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 2017-11-13 | |
| | |||
* | Split up reflective side condition tactics | 2017-11-13 | |
| | | | | Now we no longer bundle the side-condition solver with the reifier | ||
* | Add InterpCompose | 2017-11-13 | |
| | |||
* | 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 | |
| | |||
* | 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 | |
| | |||
* | 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 | |
| | |||
* | 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 | ||
* | 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 | |
| | |||
* | Add fieldwise_lift_and | 2017-11-09 | |
| | |||
* | Add more versions of fieldwise_Proper | 2017-11-09 | |
| | |||
* | Add fieldwise_Proper | 2017-11-09 | |
| |