| Commit message (Expand) | Author | Age |
... | |
* | Prove map2_zselect | Jason Gross | 2017-06-25 |
* | Fixes #219 | jadep | 2017-06-25 |
* | Clean up some montgomery wbw instantiation, make display | Jason Gross | 2017-06-24 |
* | Fill in axioms for sub_then_maybe_add; this required fiddling with updated ar... | jadep | 2017-06-24 |
* | made conditional_add a wrapper, defined and proved sub_then_maybe_add | jadep | 2017-06-24 |
* | Make a 'conditionals' section in Columns, and move conditional_add there | jadep | 2017-06-24 |
* | Add (partially admitted) integration tests for add, sub, opp | Jason Gross | 2017-06-22 |
* | P256: Partial work on add, sub, opp | Jason Gross | 2017-06-22 |
* | Account for future changes of #219 | Jason Gross | 2017-06-22 |
* | Prove In_to_list_left_tl, In_left_hd, to_list_left_append | Jason Gross | 2017-06-21 |
* | Prove some admitted lemmas about uweight | Jason Gross | 2017-06-21 |
* | changed number of limbs partway through conditional_sub; was n, now S n | jadep | 2017-06-20 |
* | Make use of new conditional_subtract | Jason Gross | 2017-06-20 |
* | Remove duplicate [small p] hypothesis from small_conditional_sub | Jason Gross | 2017-06-20 |
* | Add conditional_sub_id to uncps globally | Jason Gross | 2017-06-20 |
* | defined conditional_sub (see #207) -- small_conditional_sub admitted, eval_co... | jadep | 2017-06-20 |
* | rename Columns.sub_cps to make it clear that no balance is added | jadep | 2017-06-20 |
* | Don't depend on classical axioms for small_add | Jason Gross | 2017-06-20 |
* | Make use of new small_add | Jason Gross | 2017-06-20 |
* | Weaken preconditions on small_add | Jason Gross | 2017-06-20 |
* | Strip trailing whitespace | Jason Gross | 2017-06-20 |
* | Fix build error | Jason Gross | 2017-06-19 |
* | fixed precondition on small_add | jadep | 2017-06-19 |
* | mulmod: sig type in terms of equivalence modulo p | Jason Gross | 2017-06-18 |
* | Make use of new small_scmul | Jason Gross | 2017-06-18 |
* | proved small_scmul | jadep | 2017-06-18 |
* | Update wbw to work with new api | Jason Gross | 2017-06-18 |
* | proved eval_scmul | jadep | 2017-06-18 |
* | proved small_zero | jadep | 2017-06-18 |
* | proved small_drop_high | jadep | 2017-06-18 |
* | proved eval_drop_high | jadep | 2017-06-18 |
* | define strong small and re-prove small_add and small_compact with that defini... | jadep | 2017-06-18 |
* | make scmul discard its carry in a saner way; rather than concatenating it in ... | jadep | 2017-06-18 |
* | Drop the 0-carry bit before bounds analysis | Jason Gross | 2017-06-17 |
* | Fix scmul bounds issue | jadep | 2017-06-17 |
* | More eye-catching naming scheme for nm in saturated | Jason Gross | 2017-06-17 |
* | Make use of non-uniform tuple-based add | Jason Gross | 2017-06-17 |
* | fix WWMM partial evaluation | Andres Erbsen | 2017-06-16 |
* | finish tuple-ifying Montgomery API | jadep | 2017-06-16 |
* | Switch to using tuples for word-by-word montgomery | Jason Gross | 2017-06-16 |
* | CPSify montgomery wbw reduction | Jason Gross | 2017-06-15 |
* | CPSify Saturated API in preparation for CPSifying Montgomery (see #194) | jadep | 2017-06-15 |
* | Improve replace_match_with_destructuring_match | Jason Gross | 2017-06-15 |
* | Added reduce to karatsuba synthesis | jadep | 2017-06-15 |
* | fix goldilocks karatsuba; TODO implement reduce | Andres Erbsen | 2017-06-14 |
* | ScalarMult: Z -> G -> G (closes #193) | Andres Erbsen | 2017-06-14 |
* | Update WBW montgomery comments | Jason Gross | 2017-06-13 |
* | Fill in mul_split to wbw montgomery | Jason Gross | 2017-06-13 |
* | WBW-montgomery: Fill in most context variables | Jason Gross | 2017-06-13 |
* | finish computational portions of operations needed for Montgomery, and sketch... | jadep | 2017-06-12 |