aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Add selectGravatar Jason Gross2018-07-03
|
* Comment out some code that's too slowGravatar Jason Gross2018-07-03
|
* Synthesize moreGravatar Jason Gross2018-07-03
|
* Allow passing functions to synthesize on the command line, and scmul for 25519Gravatar Jason Gross2018-07-03
|
* Pull out *2 in square, don't turn *2 into <<1Gravatar Jason Gross2018-07-03
|
* No subst01 in mulmodGravatar Jason Gross2018-07-03
|
* Start with a better template for carry_squareGravatar Jason Gross2018-07-03
|
* Don't subst01 in squareGravatar Jason Gross2018-07-03
|
* synthesize squareGravatar Jason Gross2018-07-03
|
* static in cGravatar Jason Gross2018-07-03
|
* static voidGravatar Jason Gross2018-07-03
|
* WIPGravatar Jason Gross2018-07-03
|
* Add ZUtil, list lemmasGravatar Jason Gross2018-07-02
|
* Fix a notation issue in previous commitGravatar Jason Gross2018-07-02
|
* Add more ListUtil proofsGravatar Jason Gross2018-07-02
|
* Add some list lemmasGravatar Jason Gross2018-07-02
|
* Make all parameters implicitGravatar Jasper Hugunin2018-07-02
|
* Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoidsGravatar Jason Gross2018-07-01
| | | | Also make it easy to redeclare such instances.
* Add useful list lemmasGravatar Jason Gross2018-06-29
|
* Add ZUtil.SortingGravatar Jason Gross2018-06-29
|
* Revert "Add more schemes for prod"Gravatar Jason Gross2018-06-28
| | | | | | This reverts commit 5d38a03f5a9f69a78a582cc9cc1c350dc6596cd3. Some of these already exist in Datatypes
* Add more schemes for prodGravatar Jason Gross2018-06-28
|
* Remove useless RequiresGravatar Jason Gross2018-06-28
|
* Fix sed scripts in MakefileGravatar Jason Gross2018-06-28
|
* Try out stronger land, lor boundsGravatar Jason Gross2018-06-27
|
* Add is_tighter_than_bool lemmasGravatar Jason Gross2018-06-27
|
* Add lnot mod pull/push lemmasGravatar Jason Gross2018-06-27
|
* Add missing Z.lnot_0 hintsGravatar Jason Gross2018-06-27
|
* Add more Z const hintsGravatar Jason Gross2018-06-27
|
* Remove lneg in favor of lnot_modulo (lneg was wrong)Gravatar Jason Gross2018-06-27
|
* Add some Z.land, Z.lor hintsGravatar Jason Gross2018-06-27
|
* Add a couple of zrange lemmasGravatar Jason Gross2018-06-26
|
* Add specialize_all_ways, fix a proof in ↵Gravatar Jason Gross2018-06-26
| | | | src/Compilers/Z/ArithmeticSimplifierInterp.v
* Add Z.bneg, Z.lnegGravatar Jason Gross2018-06-26
|
* Slightly better definitions of some ZUtil functionsGravatar Jason Gross2018-06-26
| | | | | This way we can just directly reify most of the primitives we care about.
* Add list_beqGravatar Jason Gross2018-06-22
|
* Add Option.List.bind_listGravatar Jason Gross2018-06-21
|
* Add [freeze] to ArithmeticGravatar Jason Gross2018-06-21
|
* Add extend_to_length for non-uniform-length add, subGravatar Jason Gross2018-06-19
|
* Be more aggressive about removing \rGravatar Jason Gross2018-06-19
|
* Fix issue with Travis networkGravatar Jason Gross2018-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 / cygwinGravatar Jason Gross2018-06-19
|
* Add seq_add, seq_len_0Gravatar Jason Gross2018-06-19
|
* Add a comment about subGravatar Jason Gross2018-06-18
|
* More compact printing of ASTs in errorsGravatar Jason Gross2018-06-18
|
* Add another prime exampleGravatar Jason Gross2018-06-18
|
* Fix a typo in to-C shiftsGravatar Jason Gross2018-06-18
|
* Don't duplicate error message printing in OCamlGravatar Jason Gross2018-06-18
|
* Pass around lists of strings for error messagesGravatar Jason Gross2018-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 ShowLinesGravatar Jason Gross2018-06-17
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 03:03:47 +0000