aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
* Fix missing argGravatar Jason Gross2018-07-03
* Add missing spaceGravatar Jason Gross2018-07-03
* Add support for annotating generated C functions with commentsGravatar Jason Gross2018-07-03
* 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
* Make all parameters implicitGravatar Jasper Hugunin2018-07-02
* Remove useless RequiresGravatar Jason Gross2018-06-28
* Add [freeze] to ArithmeticGravatar Jason Gross2018-06-21
* Add extend_to_length for non-uniform-length add, subGravatar 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
* New pipeline, split among filesGravatar Jason Gross2018-06-17
* Minor refactoringGravatar Jason Gross2018-06-13
* fix over-indented lineGravatar Jade Philipoom2018-05-31
* prove prefancy->fancy for barrett special caseGravatar Jade Philipoom2018-05-31
* move around some Lets so that 8.8 doesn't errorGravatar Jade Philipoom2018-05-31
* relocate ok_expr tactics and fix an admit with a silly bounds relaxation hackGravatar Jade Philipoom2018-05-31
* Proved pre-fancy barrett reduction correct (except 1 admit for boundsGravatar Jade Philipoom2018-05-31
* temporary workaround for #352Gravatar Jade Philipoom2018-05-31
* Define machine model, write prefancy->fancy pass, and prove Montgomery code c...Gravatar Jade Philipoom2018-05-31
* [WIP] shifting addsGravatar Jade Philipoom2018-05-31
* change order of additions so that they a) make more sense and b) are more sui...Gravatar Jade Philipoom2018-05-31
* tweak binders so that shifts from base conversion get inlinedGravatar Jade Philipoom2018-05-31
* remove unneeded comment and extra whitespaceGravatar Jade Philipoom2018-05-31
* end-to-end proof for montgomeryGravatar Jade Philipoom2018-05-31
* Proofs for pre-fancy pass (could use cleanup)Gravatar Jade Philipoom2018-05-31
* proofs for straightline pass (with admits for some depth stuff that should be...Gravatar Jade Philipoom2018-05-31
* finish pushing through changes to dummy and factor out identifier matchGravatar Jade Philipoom2018-05-07
* replace dummy_var with dummy_arrow and change style of straightline tests to ...Gravatar Jade Philipoom2018-05-07
* clean up shared notations and constant-rewriting logic for prefancyGravatar Jade Philipoom2018-05-07
* prefancy now works on barrett (modulo add-opp=>sub)Gravatar Jade Philipoom2018-05-07
* Move straightline and prefancy stuff above barrett reductionGravatar Jade Philipoom2018-05-07
* Translating to 'pre-fancy' form now works on MontgomeryGravatar Jade Philipoom2018-05-07
* move depth to a more sensible locationGravatar Jade Philipoom2018-05-07
* Translation to straightline code now works correctly on montgomery256Gravatar Jade Philipoom2018-05-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 00:15:09 +0000