| Commit message (Expand) | Author | Age |
* | Fix the s-adjustment for saturated solinas | Jason Gross | 2018-11-06 |
* | Revert "Factor out a common computation to fix n² behavior" | Jason Gross | 2018-11-06 |
* | Factor out a common computation to fix n² behavior | Jason Gross | 2018-11-06 |
* | Use a better strategy in Rows.sat_reduce | Jason Gross | 2018-11-06 |
* | Compatibility with coq PR #8457 | Frédéric Besson | 2018-09-25 |
* | remove unneeded proof | jadep | 2018-09-17 |
* | redo all Rows correctness proofs using partition and sanity, remove now-unuse... | jadep | 2018-09-17 |
* | remove now-unused nth_default hints | jadep | 2018-09-17 |
* | fix up flatten partitioning proofs so that they don't use nth_default | jadep | 2018-09-17 |
* | remove commented-out code that is now clearly unneeded | jadep | 2018-09-17 |
* | re-fix syntax so it works on older Coq versions | jadep | 2018-09-17 |
* | prove small_div axiom | jadep | 2018-09-17 |
* | prove eval_mod axiom and clean up eval_div proof | jadep | 2018-09-17 |
* | use recursive partition to prove eval_div axiom | jadep | 2018-09-17 |
* | add a recursive definition of partition and prove it equivalent | jadep | 2018-09-17 |
* | move partition and its proofs to a new module and use it for correctness of C... | jadep | 2018-09-17 |
* | change deprecated 'Focus 2' to '2:' | jadep | 2018-09-17 |
* | Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil | Jason Gross | 2018-08-23 |
* | Add Proof using to arithmetic proofs | Jason Gross | 2018-08-07 |
* | Montgomery reduction in new pipeline | Jason Gross | 2018-07-21 |
* | Thunk nat_rect for better perf, list_{rect=>case} | Jason Gross | 2018-07-17 |
* | Remove a lemma that's been moved to NatUtil | Jason Gross | 2018-07-17 |
* | Add a stronger version of eval_reduce | Jason Gross | 2018-07-14 |
* | Make Z.div_mod_to_quot_rem stronger | Jason Gross | 2018-07-10 |
* | Prove that to_bytesmod partitions | Jason Gross | 2018-07-08 |
* | Shuffle some ZUtil lemmas around | Jason Gross | 2018-07-08 |
* | Factor eval_reduce_square_exact a bit differently | Jason Gross | 2018-07-03 |
* | Fix hints, hopefully | Jason Gross | 2018-07-03 |
* | clean | Jason Gross | 2018-07-03 |
* | Finish reduce_square proof | Jason Gross | 2018-07-03 |
* | Try to fix square again | Jason Gross | 2018-07-03 |
* | Fix a typo, start on proof | Jason Gross | 2018-07-03 |
* | Fix a reification issue | Jason Gross | 2018-07-03 |
* | Try a different reduce_square | Jason Gross | 2018-07-03 |
* | WIP better square | Jason Gross | 2018-07-03 |
* | Add select | Jason Gross | 2018-07-03 |
* | Allow passing functions to synthesize on the command line, and scmul for 25519 | Jason Gross | 2018-07-03 |
* | Pull out *2 in square, don't turn *2 into <<1 | Jason Gross | 2018-07-03 |
* | Start with a better template for carry_square | Jason Gross | 2018-07-03 |
* | WIP | Jason Gross | 2018-07-03 |
* | Remove useless Requires | Jason Gross | 2018-06-28 |
* | Add [freeze] to Arithmetic | Jason Gross | 2018-06-21 |
* | Add extend_to_length for non-uniform-length add, sub | Jason Gross | 2018-06-19 |
* | Add a comment about sub | Jason Gross | 2018-06-18 |
* | New pipeline, split among files | Jason Gross | 2018-06-17 |