aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Synthesize selectznzGravatar Jason Gross2018-07-03
|
* Correctly reify match on prodGravatar Jason Gross2018-07-03
|
* Add selectGravatar Jason Gross2018-07-03
|
* Comment out some code that's too slowGravatar 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
|
* 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
|
* 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
|
* New pipeline, split among filesGravatar Jason Gross2018-06-17
|
* Reserve a notatoin for ;;Gravatar Jason Gross2018-06-16
|
* Add zrange equalityGravatar Jason Gross2018-06-15
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 04:39:44 +0000