| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Translating to 'pre-fancy' form now works on Montgomery |  Jade Philipoom | 2018-05-07 |
| | | |||
| * | move depth to a more sensible location | Jade Philipoom | 2018-05-07 |
| | | |||
| * | Translation to straightline code now works correctly on montgomery256 | Jade Philipoom | 2018-05-07 |
| | | |||
| * | Translation to straightline code (first attempts, mostly working) | Jade Philipoom | 2018-05-07 |
| | | |||
| * | fix the placement of a dlet to make more sense | Jade Philipoom | 2018-05-07 |
| | | |||
| * | Backtrack on moving a notation to Notations.v, to fix conflict |  Jason Gross | 2018-05-06 |
| | | |||
| * | Fix notations to not conflict with bbv | Jason Gross | 2018-05-06 |
| | | |||
| * | More reserved notations | Jason Gross | 2018-05-06 |
| | | |||
| * | Add another notation | Jason Gross | 2018-05-06 |
| | | |||
| * | Fix a typo in last commit | Jason Gross | 2018-05-06 |
| | | |||
| * | Add a reserved notation for #v | Jason Gross | 2018-05-06 |
| | | |||
| * | Don't use vm_compute with existentials | Jason Gross | 2018-05-05 |
| | | |||
| * | Update comment | Jason Gross | 2018-05-05 |
| | | |||
| * | Fully finish flat_map | Jason Gross | 2018-05-05 |
| | | |||
| * | Fix flat_map | Jason Gross | 2018-05-05 |
| | | |||
| * | WIP on lists as cons cells | Jason Gross | 2018-05-05 |
| | | |||
| * | Remove vinterp_arrow function | Jason Gross | 2018-05-05 |
| | | |||
| * | Revert "WIP on inductive base_value" | Jason Gross | 2018-05-05 |
| | | | | | This reverts commit e38faaac1d3996c61d396144e20b8bb41809a253. | ||
| * | WIP on inductive base_value | Jason Gross | 2018-05-05 |
| | | |||
| * | Revert "WIP with andres, not working pattern language" | Jason Gross | 2018-05-05 |
| | | | | | This reverts commit 2fcf4cd6aabebb3b68cc0a807e5d7c78e9142cb5. | ||
| * | WIP with andres, not working pattern language | Jason Gross | 2018-05-05 |
| | | |||
| * | Add comment about leaky abstraction | Jason Gross | 2018-05-05 |
| | | |||
| * | Split off specialization to base types from specialization to idents | Jason Gross | 2018-05-05 |
| | | |||
| * | make update-_CoqProject | Jason Gross | 2018-05-05 |
| | | |||
| * | Add type variables / substitutions | Jason Gross | 2018-05-05 |
| | | | | | This allows more genericness in the ident-specific code | ||
| * | Change some notations for more readability by Andres | Jason Gross | 2018-05-05 |
| | | |||
| * | Update cast -> annotate | Jason Gross | 2018-05-05 |
| | | |||
| * | Parameterize over types and identifiers | Jason Gross | 2018-05-05 |
| | | |||
| * | Add notes | Jason Gross | 2018-05-05 |
| | | |||
| * | Add partial evaluation | Jason Gross | 2018-05-05 |
| | | |||
| * | Some experiments with partial evaluation with letin without cps | Jason Gross | 2018-05-05 |
| | | | | | Jason & Andres | ||
| * | Bump versions of Coq we test on travis | Jason Gross | 2018-05-02 |
| | | | | | | Now we test master, v8.8.dev, v8.7.dev, 8.8.0, and 8.7.2, instead of master, v8.7.dev, and 8.7.1. | ||
| * | un-hardcode # of reductions | Jade Philipoom | 2018-04-30 |
| | | |||
| * | print saturated mulmod for p192 on 32-bit, add note about p256 | Jade Philipoom | 2018-04-30 |
| | | |||
| * | fixed too-many-additions problem by fixing number of limbs in from_associational | Jade Philipoom | 2018-04-30 |
| | | |||
| * | Fix some carry logic | Jade Philipoom | 2018-04-30 |
| | | |||
| * | First stab at generating code for saturated solinas modular | Jade Philipoom | 2018-04-30 |
| | | | | | | multiplication (currently produces way too many expressions because 1*x and -1*x are not simplified for two-output mul) | ||
| * | fix comment | Jade Philipoom | 2018-04-30 |
| | | |||
| * | Fix bounds analysis for saturated ops and remove unneeded comment | Jade Philipoom | 2018-04-30 |
| | | |||
| * | first stab at reifying barrett | Jade Philipoom | 2018-04-30 |
| | | |||
| * | fix definitions of saturated operations to avoid unnecessary work, and make ↵ | Jade Philipoom | 2018-04-30 |
| | | | | | Montgomery use them | ||
| * | tweak definition of flatten to use an index rather than check the length of ↵ | Jade Philipoom | 2018-04-30 |
| | | | | | the output accumulator--this prevents the accumulator from repeatedly showing up in the expression and making the term huge | ||
| * | fix the placement of a dlet to make more sense | Jade Philipoom | 2018-04-30 |
| | | |||
| * | Don't allow coqprime and coqprime-all to run in parallel | Jason Gross | 2018-04-30 |
| | | | | | We only want one invocation of submake at a time. | ||
| * | Only install files built by the coq target | Jason Gross | 2018-04-30 |
| | | |||
| * | Add a coqprime-all target to build all of coqprime | Jason Gross | 2018-04-30 |
| | | |||
| * | In reassocation, don't reassociate additions | Jason Gross | 2018-04-26 |
| | | | | | | | | | | It was serving no purpose, and was messing up the associativity of balance on sub. I believe it was originally there because I thought I had to handle 19 * (a * b + c * d) -> (19 * a) * b + (19 * c) * d, but this case doesn't show up, and so I never wrote the code to handle it, but also never removed the code to parse additions into lists (thereby losing associativity information). | ||
| * | Fix a printout | Jason Gross | 2018-04-26 |
| | | |||
| * | Revert most of "Make reassociation optional" | Jason Gross | 2018-04-26 |
| | | | | | | | This reverts most of commit f776eb5815166f1ff648808231794dee01a4683c. We'll do it a different way. | ||
| * | Make reassociation optional | Jason Gross | 2018-04-26 |
| | | | | | It was messing up the associativity of balance on sub. | ||
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |