| Commit message (Expand) | Author | Age |
|---|
| * | proved eval_mod and eval_div (last remaining eval_ admits in Saturated) |  jadep | 2017-06-27 |
| * | Add a comment for nonzero_cps |  Jason Gross | 2017-06-26 |
| * | Factor out admitted proof into admitted lemma | Jason Gross | 2017-06-26 |
| * | Add nonzero synthesis | Jason Gross | 2017-06-26 |
| * | Prove map2_zselect | Jason Gross | 2017-06-25 |
| * | Fixes #219 | jadep | 2017-06-25 |
| * | 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 |
| * | 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 |
| * | 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 |
| * | Weaken preconditions on small_add | Jason Gross | 2017-06-20 |
| * | Strip trailing whitespace | Jason Gross | 2017-06-20 |
| * | fixed precondition on small_add | jadep | 2017-06-19 |
| * | proved small_scmul | jadep | 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 |
| * | 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 |
| * | Fill in mul_split to wbw montgomery | Jason Gross | 2017-06-13 |
| * | finish computational portions of operations needed for Montgomery, and sketch... | jadep | 2017-06-12 |
| * | add zero (as per #157) | jadep | 2017-06-08 |
| * | start saturated-arithmetic API for use in Montgomery (see discussion in #157) | jadep | 2017-06-08 |
| * | Don't rely on autogenerated names | Jason Gross | 2017-06-05 |
| * | Strip trailing whitespace | Jason Gross | 2017-06-02 |
| * | remove redundant definition | jadep | 2017-05-14 |
| * | make freeze use the correct versions of add_get_carry and zselect | jadep | 2017-05-14 |
| * | move some lemmas to Core and define a tuple-select operation | jadep | 2017-05-01 |
| * | Fix base-case for compact_digit (for a list [x;y], we want to do div/mod on x... | jadep | 2017-05-01 |
| * | proved freeze, removed initial carry step (the correctness proof of that step... | jadep | 2017-05-01 |
| * | prove compact obeys div/mod rule | jadep | 2017-05-01 |
| * | prove compact_digit obeys div/mod rule | jadep | 2017-05-01 |
| * | first attempts at freeze | jadep | 2017-05-01 |
| * | More comment on Saturated.v, explaining representation and the [compact] oper... | jadep | 2017-04-11 |
| * | rename-everything |  Andres Erbsen | 2017-04-06 |
jadep
Jason Gross
Andres Erbsen