| Commit message (Expand) | Author | Age |
* | 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 |
* | Add more Z-notations | Jason Gross | 2017-06-20 |
* | make display | Jason Gross | 2017-06-20 |
* | Add another fusion to adc-fusion | Jason Gross | 2017-06-20 |
* | changed number of limbs partway through conditional_sub; was n, now S n | jadep | 2017-06-20 |
* | Add fold_left_orb_true, fold_left_orb_pull | Jason Gross | 2017-06-20 |
* | Use solve_wf_side_condition to synch the depth of auto with wf | Jason Gross | 2017-06-20 |
* | make display | Jason Gross | 2017-06-20 |
* | make display (new conditional_sub) | Jason Gross | 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 |
* | Add more constant notations | Jason Gross | 2017-06-20 |
* | Add is_bounded_by_None_repeat_In_iff | Jason Gross | 2017-06-20 |
* | make bench | Jason Gross | 2017-06-20 |
* | check in icc-compiled IntegrationTestMontgomeryP256.s | Andres Erbsen | 2017-06-20 |
* | sed mulx appropriately | Andres Erbsen | 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 |