aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/WeierstrassCurve.v
Commit message (Collapse)AuthorAge
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
| | | | | | | | | | | | ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1
* Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03
Define the spec of Weierstrass curves This is the start of work on P256.