| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | indentation |  Jason Gross | 2017-06-25 |
| * | Prove map2_zselect | Jason Gross | 2017-06-25 |
| * | Prove map2_append | Jason Gross | 2017-06-25 |
| * | Allow disabling adc-fusion | Jason Gross | 2017-06-25 |
| * | make display on p256 |  Andres Erbsen | 2017-06-25 |
| * | Fixes #219 |  jadep | 2017-06-25 |
| * | write and prove Tuple.map2_cps | jadep | 2017-06-25 |
| * | make display | Jason Gross | 2017-06-25 |
| * | Convert adc to sbb when doing [0 - x] | Jason Gross | 2017-06-25 |
| * | Revert "Convert adc to sbb when doing [0 - x]" | Jason Gross | 2017-06-25 |
| * | Convert adc to sbb when doing [0 - x] | Jason Gross | 2017-06-24 |
| * | make display | Jason Gross | 2017-06-24 |
| * | Fix some things not being unfolded | Jason Gross | 2017-06-24 |
| * | make display | Jason Gross | 2017-06-24 |
| * | Propogate neg through constant multiplication | Jason Gross | 2017-06-24 |
| * | Clean up some montgomery wbw instantiation, make display | Jason Gross | 2017-06-24 |
| * | Remove admits | 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 |
| * | make bench | Andres Erbsen | 2017-06-23 |
| * | Weierstrass Jacobian mixed addition | Andres Erbsen | 2017-06-23 |
| * | Fix an issue with notations | Jason Gross | 2017-06-22 |
| * | Add notation for logical or | Jason Gross | 2017-06-22 |
| * | make display | Jason Gross | 2017-06-22 |
| * | Add (partially admitted) integration tests for add, sub, opp | Jason Gross | 2017-06-22 |
| * | Fix a typo in push_Zmod that was causing looping | Jason Gross | 2017-06-22 |
| * | P256: Partial work on add, sub, opp | Jason Gross | 2017-06-22 |
| * | Fix an [sz] that shouldn't have been removed in the previous commit | Jason Gross | 2017-06-22 |
| * | P256: Keep around < eval N bounds | Jason Gross | 2017-06-22 |
| * | Add sig_conj_by_impl2 | Jason Gross | 2017-06-22 |
| * | Work around bug #5615 (constr not being updated) | Jason Gross | 2017-06-22 |
| * | move Specifi p256 files into their own directory | Andres Erbsen | 2017-06-22 |
| * | Fix some minor naming bugs in sig_assoc tactics | Jason Gross | 2017-06-22 |
| * | Add tighter bounds to MontgomeryP256{,_128} | Jason Gross | 2017-06-22 |
| * | Account for future changes of #219 | Jason Gross | 2017-06-22 |
| * | src/Demo.v: a 200-line introduction to BaseSystem ideas | Andres Erbsen | 2017-06-21 |
| * | 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 |
| * | compile src/Specific/IntegrationTestMontgomeryP256.s | Andres Erbsen | 2017-06-21 |
| * | Use is_bounded_by_None_repeat_In_iff_lt, remove axiom | Jason Gross | 2017-06-20 |
| * | Add is_bounded_by_None_repeat_In_iff_lt | Jason Gross | 2017-06-20 |
| * | make display | Jason Gross | 2017-06-20 |
| * | Also key adc->sbb on the carry-bit being negative | Jason Gross | 2017-06-20 |
| * | Add more simplification passes (de-doubling opp) | Jason Gross | 2017-06-20 |
| * | make display | Jason Gross | 2017-06-20 |
| * | Add more simplification passes (de-doubling opp) | Jason Gross | 2017-06-20 |
| * | make display | Jason Gross | 2017-06-20 |
| * | Enable a-nf for montgomery | Jason Gross | 2017-06-20 |
| * | make display | Jason Gross | 2017-06-20 |
Jason Gross
Andres Erbsen
jadep