aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve
Commit message (Expand)AuthorAge
* use improved fsatz on various elliptic curve thingsGravatar Andres Erbsen2017-03-31
* make fsatz recurse when proving nonzero-ness, undo Weierstrass workaroundGravatar Andres Erbsen2017-03-30
* CompleteEdwardsCurveTheorems: point compressionGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* rewrite ExtendedCoordinates, fix Ed25519Gravatar Andres Erbsen2017-03-02
* edwards curves over isomorphic fieldsGravatar Andres Erbsen2017-03-02
* WIPGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* fsatz, nsatz_solve_nonzeroGravatar Andres Erbsen2017-03-02
* use field_nsatz in CompleteEdwardsCurve.PreGravatar Andres Erbsen2017-03-02
* Fix for 8.6Gravatar Jason Gross2016-11-22
* Fix for Coq 8.4Gravatar Jason Gross2016-11-21
* Add add_coordinates_respectful_heteroGravatar Jason Gross2016-11-17
* Generalize add_coordinatesGravatar Jason Gross2016-11-17
* Add add_coordinates_genGravatar Jason Gross2016-11-16
* framework for l_order_BGravatar Andres Erbsen2016-10-30
* CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism l...Gravatar Andres Erbsen2016-10-27
* fiddle with [rewrite <-!(field_div_definition)], maybe fix buildGravatar Andres Erbsen2016-10-21
* Edwards.Extended.to_twisted: only one inversion, improve extractionGravatar Andres Erbsen2016-10-21
* Be more hesitant to [pose proof E.char_gt_2]Gravatar Jason Gross2016-10-17
* refactor scalar multiplication thoery, implement SRepERepMulGravatar Andres Erbsen2016-10-12
* remove eq_dec from MonoidGravatar Andres Erbsen2016-08-23
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* proved an admit in field homomorphisms that turned out to be unprovable; I ad...Gravatar jadep2016-07-15
* s/conservative_common_denominator/common_denominator/gGravatar Andres Erbsen2016-07-11
* remove field_algebraGravatar Andres Erbsen2016-07-11
* port CompleteEdwardsCurveTheorems (builds again)Gravatar Andres Erbsen2016-07-11
* pose proof fails where specialize works (typeclass resolution / unification?)Gravatar Andres Erbsen2016-07-11
* wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
* added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-06-27
|\
| * scalarmult support; EdDSA.sign produces valid signaturesGravatar Andres Erbsen2016-06-27
* | update new lemma in CompleteEdwardsCurve/Pre to match other changes to that fileGravatar jadep2016-06-25
* | Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_portGravatar jadep2016-06-24
|\|
* | merging point encoding portGravatar jadep2016-06-24
|\ \
* | | Ported PointEncodings to parameterize over field rather than modulus.Gravatar jadep2016-06-24
| | * Remove a useless introGravatar Jason Gross2016-06-24
| |/
| * ExtendedCoordinates: group.Gravatar Andres Erbsen2016-06-24
| * Use Decidable machinery for is_eq_decGravatar Jason Gross2016-06-24
| * Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
| * Pseudize Let_InGravatar Robert Sloan2016-06-23
| * Fix broken notations (hopefully)Gravatar Jason Gross2016-06-22
| * Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
| * Use Admitted, not Qed, when a proof has admitGravatar Jason Gross2016-06-21
| * Fix [Proper_add] in 8.5Gravatar Jason Gross2016-06-21
| * Make [bash] tactic easier to debugGravatar Jason Gross2016-06-21
| * use Local Obligation Tactic (8.5-compat)Gravatar Andres Erbsen2016-06-21
| * remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 10:52:22 +0000