Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Fill in axioms for sub_then_maybe_add; this required fiddling with updated ↵ | 2017-06-24 | ||
| | | | | arguments since more context variables were used in the definitions than in the placeholder axioms | |||
* | made conditional_add a wrapper, defined and proved sub_then_maybe_add | 2017-06-24 | ||
| | ||||
* | Make a 'conditionals' section in Columns, and move conditional_add there | 2017-06-24 | ||
| | ||||
* | make bench | 2017-06-23 | ||
| | ||||
* | Weierstrass Jacobian mixed addition | 2017-06-23 | ||
| | ||||
* | Fix an issue with notations | 2017-06-22 | ||
| | | | | | CNotations breaks writing of Gallina and Ltac `match`. So we need to import it very, very late. | |||
* | Add notation for logical or | 2017-06-22 | ||
| | ||||
* | make display | 2017-06-22 | ||
| | ||||
* | Add (partially admitted) integration tests for add, sub, opp | 2017-06-22 | ||
| | ||||
* | Fix a typo in push_Zmod that was causing looping | 2017-06-22 | ||
| | ||||
* | P256: Partial work on add, sub, opp | 2017-06-22 | ||
| | | | | Partial work towards #218 | |||
* | Fix an [sz] that shouldn't have been removed in the previous commit | 2017-06-22 | ||
| | ||||
* | P256: Keep around < eval N bounds | 2017-06-22 | ||
| | | | | | | This closes #220 The code before the glue part of the pipeline is getting kind-of ugly... | |||
* | Add sig_conj_by_impl2 | 2017-06-22 | ||
| | ||||
* | Work around bug #5615 (constr not being updated) | 2017-06-22 | ||
| | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5615, Ltac should be able to bind references and not just names, in which names are slippery, slippery objects. | |||
* | move Specifi p256 files into their own directory | 2017-06-22 | ||
| | ||||
* | Fix some minor naming bugs in sig_assoc tactics | 2017-06-22 | ||
| | ||||
* | Add tighter bounds to MontgomeryP256{,_128} | 2017-06-22 | ||
| | ||||
* | Account for future changes of #219 | 2017-06-22 | ||
| | | | | | Note that this makes the axiom we added false. It has a very long and descriptive name to account for this fact. | |||
* | src/Demo.v: a 200-line introduction to BaseSystem ideas | 2017-06-21 | ||
| | ||||
* | Prove In_to_list_left_tl, In_left_hd, to_list_left_append | 2017-06-21 | ||
| | ||||
* | Prove some admitted lemmas about uweight | 2017-06-21 | ||
| | | | | Not sure if locally adding hypotheses is the best way to do it. | |||
* | compile src/Specific/IntegrationTestMontgomeryP256.s | 2017-06-21 | ||
| | ||||
* | Use is_bounded_by_None_repeat_In_iff_lt, remove axiom | 2017-06-20 | ||
| | | | | This actually closes #211 | |||
* | Add is_bounded_by_None_repeat_In_iff_lt | 2017-06-20 | ||
| | ||||
* | make display | 2017-06-20 | ||
| | ||||
* | Also key adc->sbb on the carry-bit being negative | 2017-06-20 | ||
| | | | | This is needed when we're subtracting 0 >.> | |||
* | Add more simplification passes (de-doubling opp) | 2017-06-20 | ||
| | ||||
* | make display | 2017-06-20 | ||
| | ||||
* | Add more simplification passes (de-doubling opp) | 2017-06-20 | ||
| | ||||
* | make display | 2017-06-20 | ||
| | ||||
* | Enable a-nf for montgomery | 2017-06-20 | ||
| | | | | This fixes adc-fusion, and closes #214. | |||
* | make display | 2017-06-20 | ||
| | ||||
* | Add more Z-notations | 2017-06-20 | ||
| | ||||
* | make display | 2017-06-20 | ||
| | ||||
* | Add another fusion to adc-fusion | 2017-06-20 | ||
| | | | | | | | Might have something to do with #213. Also, RewriteAddToAdcInterp is now a bit more stable under changes to the rewriting strategy (the parts are now more separate). | |||
* | changed number of limbs partway through conditional_sub; was n, now S n | 2017-06-20 | ||
| | ||||
* | Add fold_left_orb_true, fold_left_orb_pull | 2017-06-20 | ||
| | ||||
* | Use solve_wf_side_condition to synch the depth of auto with wf | 2017-06-20 | ||
| | ||||
* | make display | 2017-06-20 | ||
| | ||||
* | make display (new conditional_sub) | 2017-06-20 | ||
| | ||||
* | Make use of new conditional_subtract | 2017-06-20 | ||
| | ||||
* | Remove duplicate [small p] hypothesis from small_conditional_sub | 2017-06-20 | ||
| | ||||
* | Add conditional_sub_id to uncps globally | 2017-06-20 | ||
| | ||||
* | Add more constant notations | 2017-06-20 | ||
| | ||||
* | Add is_bounded_by_None_repeat_In_iff | 2017-06-20 | ||
| | ||||
* | make bench | 2017-06-20 | ||
| | ||||
* | check in icc-compiled IntegrationTestMontgomeryP256.s | 2017-06-20 | ||
| | ||||
* | sed mulx appropriately | 2017-06-20 | ||
| | ||||
* | defined conditional_sub (see #207) -- small_conditional_sub admitted, ↵ | 2017-06-20 | ||
| | | | | eval_conditional_sub proven |