aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
| * | More Coq 8.4pl2 fixesGravatar Jason Gross2016-06-11
| * | Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-11
| * | Work around bug #4811 (slow f_equal)Gravatar Jason Gross2016-06-11
* | | starting rewrite using different definition of mapGravatar jadep2016-06-11
| * | Minor 8.5 changesGravatar Jason Gross2016-06-10
| * | More changes for 8.5Gravatar Jason Gross2016-06-10
| * | 8.5 fixesGravatar Jason Gross2016-06-10
|/ /
| * 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
* 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
* ed25519: solve elliptic curve math admitsGravatar Andres Erbsen2016-04-25
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-25
|\
* | Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-04-25
| * refactor field lemmas out of ed25519Gravatar Andres Erbsen2016-04-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 19:45:14 +0000