Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | ed448 mul: use two carry chains to fix bounds (still silly otherwise) | 2017-06-15 | |
| | |||
* | fix wrong number of limbs for square as well | 2017-06-15 | |
| | |||
* | fix wrong number of limbs | 2017-06-15 | |
| | |||
* | Added reduce to karatsuba synthesis | 2017-06-15 | |
| | |||
* | fix goldilocks karatsuba; TODO implement reduce | 2017-06-14 | |
| | |||
* | Don't unfold id_with_alt | 2017-06-13 | |
| | | | | Oops | ||
* | Remove use of id_tuple_with_alt_proof | 2017-06-12 | |
| | | | | We (@jadephilipoom?) should now remove the dead-code admits. | ||
* | Factor karatsuba through IdfunWithAlt, add test | 2017-06-11 | |
| | | | | | | | | | | | Currently the refinement is commented out. Also, we drop the proof of equality early (and probably won't use it in the first place); there's no way we can carry around such a proof in reflective-land, so we'll need to add an arithmetical-equality semi-decider to reflective-land that can prove the relevant equalities (or we'll need to leave them over as side-conditions). I expeect this may make things significantly easier on @jadephilipoom. | ||
* | Fix broken implicits | 2017-06-08 | |
| | | | | Closes #190 | ||
* | first stage of synthesis for karatsuba with alt-bounds hack, contains ↵ | 2017-06-07 | |
| | | | | several admitted lemmas | ||
* | Make Karatsuba depend on Arithmetic/Core to make calling it less of a pain | 2017-06-02 | |
| | |||
* | pulled in a CPS version of Karatsuba from another branch | 2017-06-02 | |