aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* tuple toolingGravatar Andres Erbsen2016-06-20
* port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...Gravatar Andres Erbsen2016-06-18
* move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
* Z is integral domainGravatar Andres Erbsen2016-06-16
* port edwards curve specGravatar Andres Erbsen2016-06-16
* edwards curve addition respects field homomorphismGravatar Andres Erbsen2016-06-16
* algebra: add homomorphismsGravatar Andres Erbsen2016-06-16
* prove ring admitsGravatar Andres Erbsen2016-06-16
* edwards curve preliminaries: replace oncurve proof with nsatzGravatar Andres Erbsen2016-06-16
* nsatz: reimplement, integrate, demonstrateGravatar Andres Erbsen2016-06-15
* refactor nsatz wrappers into algebra fileGravatar Andres Erbsen2016-06-14
* [field] and [nsatz] do things now againGravatar Andres Erbsen2016-06-14
* stuck because overloading-by-typeclasses sucksGravatar Andres Erbsen2016-06-13
* indentGravatar Andres Erbsen2016-06-12
* improved generic field libraryGravatar Andres Erbsen2016-06-10
* improve generic field libraryGravatar Andres Erbsen2016-06-10
* experimentGravatar Andres Erbsen2016-06-07
* generic field definitionGravatar Andres Erbsen2016-06-07
* ed25519: refactor some ProperGravatar Andres Erbsen2016-06-06
* rewrite in Let_In binder by tacticGravatar Andres Erbsen2016-06-04
* Let_In rewritingGravatar Andres Erbsen2016-06-03
* leibniz equal version of topdown rewriting of sigma types: nicerGravatar Andres Erbsen2016-06-01
* leibniz equal version of topdown rewriting of sigma typesGravatar Andres Erbsen2016-06-01
* E impl: proper morphisms are hard to dow without setoidsGravatar Andres Erbsen2016-05-30
* ERep addGravatar Andres Erbsen2016-05-29
* --amendGravatar Andres Erbsen2016-05-28
* verify derivation, EdDSA layer: allow arbitrary equivalence relation for ERep...Gravatar Andres Erbsen2016-05-28
* verify derivation, EdDSA layer: remove unused context variablesGravatar Andres Erbsen2016-05-28
* verify derivation: EdDSA layerGravatar Andres Erbsen2016-05-28
* right after scalars to F lGravatar Andres Erbsen2016-05-27
* before changing SRep from N to F lGravatar Andres Erbsen2016-05-27
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-05-25
|\
* | Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ...Gravatar jadep2016-05-25
| * ed25519: indentation fixGravatar Andres Erbsen2016-05-24
| * ed25519: integrate FRepPow and FRepInvGravatar Andres Erbsen2016-05-24
| * ed25519: continue refactorGravatar Andres Erbsen2016-05-24
| * PrimeFieldTheorems fermat inverse lemma: prove admitGravatar Andres Erbsen2016-05-24
| * Factor some rewrites into a single [autorewrite]Gravatar Jason Gross2016-05-24
| * Remove unfolding, rewrite -> setoid_rewriteGravatar Jason Gross2016-05-24
| * Fix some issues in Ed25519 tacticsGravatar Jason Gross2016-05-24
| * F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...Gravatar Andres Erbsen2016-05-24
* | First stage of canonicalization proofs complete; proved 3 carry loops reduce ...Gravatar jadep2016-05-20
| * F: pow_nat_iter_op_correctGravatar Andres Erbsen2016-05-18
| * F: fermat inversion lemma refactorGravatar Andres Erbsen2016-05-18
| * unifiedAddM1Rep_sig: almost thereGravatar Andres Erbsen2016-05-18
| * slightly nicer edwards curve extended coordinates additionGravatar Andres Erbsen2016-05-18
|/
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...Gravatar jadep2016-05-09
* 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
* Proved decode_point_eq in Ed25519 (comparing encodings is equivalent toGravatar jadep2016-04-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 08:05:36 +0000