aboutsummaryrefslogtreecommitdiff
path: root/src/Encoding
Commit message (Expand)AuthorAge
* remove PointEncodingGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* improve some fragile proofs (built on 8.4)Gravatar Andres Erbsen2016-11-02
* Fix some subtleties with equalities in point encodingsGravatar jadep2016-10-30
* Modify point_phi (from PointEncodings) to use ref_phiGravatar jadep2016-10-23
* Don't let [tauto] destruct [Equivalence] in PEGravatar Jason Gross2016-10-17
* refactor scalar multiplication thoery, implement SRepERepMulGravatar Andres Erbsen2016-10-12
* Moved PointEncoding out of SpecGravatar jadep2016-10-06
* Wrote proofs necessary to fill in all point-encoding related context variable...Gravatar jadep2016-10-03
* remove eq_dec from MonoidGravatar Andres Erbsen2016-08-23
* [F] has its own module nowGravatar Andres Erbsen2016-08-05
* address code review commentsGravatar Andres Erbsen2016-08-04
* 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
* port CompleteEdwardsCurveTheorems (builds again)Gravatar Andres Erbsen2016-07-11
* Proved lingering lemmas in PointEncodingPre.Gravatar jadep2016-07-06
* Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
|\
| * Make ZUtil more uniformGravatar Jason Gross2016-07-02
* | merging point encoding portGravatar jadep2016-06-24
|\|
* | Ported PointEncodings to parameterize over field rather than modulus.Gravatar jadep2016-06-24
| * remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
| * Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-06-20
|/
* Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ...Gravatar jadep2016-05-25
* Changed name of Encoding to CanonicalEncoding, and changed notation to match.Gravatar jadep2016-04-29
* Moved sign_bit definition to Spec.Gravatar jadep2016-04-29
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* Completed encoding reorganization; factored sign_bit out of PointEncodings an...Gravatar jadep2016-04-28
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
* Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-04-25
* proved most of point encoding admits, fixed some build system issues (dead im...Gravatar Jade Philipoom2016-02-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-09 21:16:37 +0000