Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Don't subst01 in square | 2018-07-03 | |
| | |||
* | synthesize square | 2018-07-03 | |
| | |||
* | static in c | 2018-07-03 | |
| | |||
* | static void | 2018-07-03 | |
| | |||
* | WIP | 2018-07-03 | |
| | |||
* | Add ZUtil, list lemmas | 2018-07-02 | |
| | |||
* | Fix a notation issue in previous commit | 2018-07-02 | |
| | |||
* | Add more ListUtil proofs | 2018-07-02 | |
| | |||
* | Add some list lemmas | 2018-07-02 | |
| | |||
* | Make all parameters implicit | 2018-07-02 | |
| | |||
* | Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoids | 2018-07-01 | |
| | | | | Also make it easy to redeclare such instances. | ||
* | Add useful list lemmas | 2018-06-29 | |
| | |||
* | Add ZUtil.Sorting | 2018-06-29 | |
| | |||
* | Revert "Add more schemes for prod" | 2018-06-28 | |
| | | | | | | This reverts commit 5d38a03f5a9f69a78a582cc9cc1c350dc6596cd3. Some of these already exist in Datatypes | ||
* | Add more schemes for prod | 2018-06-28 | |
| | |||
* | Remove useless Requires | 2018-06-28 | |
| | |||
* | Fix sed scripts in Makefile | 2018-06-28 | |
| | |||
* | Try out stronger land, lor bounds | 2018-06-27 | |
| | |||
* | Add is_tighter_than_bool lemmas | 2018-06-27 | |
| | |||
* | Add lnot mod pull/push lemmas | 2018-06-27 | |
| | |||
* | Add missing Z.lnot_0 hints | 2018-06-27 | |
| | |||
* | Add more Z const hints | 2018-06-27 | |
| | |||
* | Remove lneg in favor of lnot_modulo (lneg was wrong) | 2018-06-27 | |
| | |||
* | Add some Z.land, Z.lor hints | 2018-06-27 | |
| | |||
* | Add a couple of zrange lemmas | 2018-06-26 | |
| | |||
* | Add specialize_all_ways, fix a proof in ↵ | 2018-06-26 | |
| | | | | src/Compilers/Z/ArithmeticSimplifierInterp.v | ||
* | Add Z.bneg, Z.lneg | 2018-06-26 | |
| | |||
* | Slightly better definitions of some ZUtil functions | 2018-06-26 | |
| | | | | | This way we can just directly reify most of the primitives we care about. | ||
* | Add list_beq | 2018-06-22 | |
| | |||
* | Add Option.List.bind_list | 2018-06-21 | |
| | |||
* | Add [freeze] to Arithmetic | 2018-06-21 | |
| | |||
* | Add extend_to_length for non-uniform-length add, sub | 2018-06-19 | |
| | |||
* | Be more aggressive about removing \r | 2018-06-19 | |
| | |||
* | Fix issue with Travis network | 2018-06-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | Sometimes we get logs like [this](https://travis-ci.org/mit-plv/fiat-crypto/jobs/393628098), where we have ``` Reading package lists... W: GPG error: http://ppa.launchpad.net/jgross-h/many-coq-versions/ubuntu trusty InRelease: The following signatures couldn't be verified because the public key is not available: NO_PUBKEY E58B19DAA454A7D9 W: The repository 'http://ppa.launchpad.net/jgross-h/many-coq-versions/ubuntu trusty InRelease' is not signed. W: There is no public key available for the following key IDs: E58B19DAA454A7D9 W: http://ppa.launchpad.net/couchdb/stable/ubuntu/dists/trusty/Release.gpg: Signature by key 15866BAFD9BCC4F3C1E0DFC7D69548E1C17EAB57 uses weak digest algorithm (SHA1) ``` and then ``` WARNING: The following packages cannot be authenticated! ocaml-base-nox ocaml-compiler-libs ocaml-interp ocaml-nox libcamlp4-ocaml-dev camlp4 coq-8.7.2-theories liblablgtk2-ocaml liblablgtksourceview2-ocaml libcoq-8.7.2-ocaml ocaml-native-compilers coq-8.7.2 coq-8.7.2ide libfindlib-ocaml libfindlib-ocaml-dev ocaml-findlib E: There were unauthenticated packages and -y was used without --allow-unauthenticated ``` I'm not sure if this is the right way to fix this... | ||
* | Make COQPATH in Makefile work on Windows / cygwin | 2018-06-19 | |
| | |||
* | Add seq_add, seq_len_0 | 2018-06-19 | |
| | |||
* | Add a comment about sub | 2018-06-18 | |
| | |||
* | More compact printing of ASTs in errors | 2018-06-18 | |
| | |||
* | Add another prime example | 2018-06-18 | |
| | |||
* | Fix a typo in to-C shifts | 2018-06-18 | |
| | |||
* | Don't duplicate error message printing in OCaml | 2018-06-18 | |
| | |||
* | Pass around lists of strings for error messages | 2018-06-17 | |
| | | | | | | | | | | This allows us to get back an error message in Saturated Solinas in OCaml on P256 x32 in reasonable time without blowing the stack. There's the slight oddity that the list of string in the success case is joined by the empty string, but the list of string in the error case is joined by newline. Probably meanas that I chose the wrong abstraction barrier somewhere. | ||
* | Add ShowLines | 2018-06-17 | |
| | |||
* | New pipeline, split among files | 2018-06-17 | |
| | |||
* | Update .gitignore with *.pyc for various helper scripts | 2018-06-16 | |
| | |||
* | Reserve a notatoin for ;; | 2018-06-16 | |
| | |||
* | Add zrange equality | 2018-06-15 | |
| | |||
* | Add ErrorT monad, and Show class | 2018-06-15 | |
| | |||
* | Add decimal_string_of_Z | 2018-06-15 | |
| | |||
* | Add some lemmas and defs to ListUtil.FoldBool | 2018-06-14 | |
| |