| Commit message (Expand) | Author | Age |
... | |
| * | leibniz equal version of topdown rewriting of sigma types | Andres Erbsen | 2016-06-01 |
| * | E impl: proper morphisms are hard to dow without setoids | Andres Erbsen | 2016-05-30 |
| * | ERep add | Andres Erbsen | 2016-05-29 |
| * | --amend | Andres Erbsen | 2016-05-28 |
| * | verify derivation, EdDSA layer: allow arbitrary equivalence relation for ERep... | Andres Erbsen | 2016-05-28 |
| * | verify derivation, EdDSA layer: remove unused context variables | Andres Erbsen | 2016-05-28 |
| * | verify derivation: EdDSA layer | Andres Erbsen | 2016-05-28 |
| * | right after scalars to F l | Andres Erbsen | 2016-05-27 |
| * | before changing SRep from N to F l | Andres Erbsen | 2016-05-27 |
|/ |
|
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-05-25 |
|\ |
|
* | | Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ... | jadep | 2016-05-25 |
| * | ed25519: indentation fix | Andres Erbsen | 2016-05-24 |
| * | ed25519: integrate FRepPow and FRepInv | Andres Erbsen | 2016-05-24 |
| * | ed25519: continue refactor | Andres Erbsen | 2016-05-24 |
| * | PrimeFieldTheorems fermat inverse lemma: prove admit | Andres Erbsen | 2016-05-24 |
| * | Factor some rewrites into a single [autorewrite] | Jason Gross | 2016-05-24 |
| * | Remove unfolding, rewrite -> setoid_rewrite | Jason Gross | 2016-05-24 |
| * | Fix some issues in Ed25519 tactics | Jason Gross | 2016-05-24 |
| * | F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok... | Andres Erbsen | 2016-05-24 |
* | | First stage of canonicalization proofs complete; proved 3 carry loops reduce ... | jadep | 2016-05-20 |
| * | F: pow_nat_iter_op_correct | Andres Erbsen | 2016-05-18 |
| * | F: fermat inversion lemma refactor | Andres Erbsen | 2016-05-18 |
| * | unifiedAddM1Rep_sig: almost there | Andres Erbsen | 2016-05-18 |
| * | slightly nicer edwards curve extended coordinates addition | Andres Erbsen | 2016-05-18 |
|/ |
|
* | Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ... | jadep | 2016-05-09 |
* | Changed name of Encoding to CanonicalEncoding, and changed notation to match. | jadep | 2016-04-29 |
* | Moved sign_bit definition to Spec. | jadep | 2016-04-29 |
* | Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to | jadep | 2016-04-29 |
* | Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener... | jadep | 2016-04-28 |
* | Completed encoding reorganization; factored sign_bit out of PointEncodings an... | jadep | 2016-04-28 |
* | ed25519: solve elliptic curve math admits | Andres Erbsen | 2016-04-25 |
* | consolidate and rename Edwards curve lemmas | Andres Erbsen | 2016-04-25 |
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-04-25 |
|\ |
|
* | | Reorganization and revision of Encoding code and redefinition of sign_bit fun... | jadep | 2016-04-25 |
| * | refactor field lemmas out of ed25519 | Andres Erbsen | 2016-04-25 |
| * | reduce admits related to point negation | Andres Erbsen | 2016-04-25 |
|/ |
|
* | point_eq_dec | Andres Erbsen | 2016-04-22 |
* | finished last cases of nonzero proofs for associativity | jadep | 2016-04-21 |
* | added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ... | jadep | 2016-04-21 |
* | automated most of the code in GF25519 | jadep | 2016-04-21 |
* | Cleanup of GF25519 | jadep | 2016-04-20 |
* | Pulled generalized code out of GF25519 so that it can be used for other moduli | jadep | 2016-04-20 |
* | moved lemmas from ModularBaseSystemProofs to various Util files | jadep | 2016-04-20 |
* | GF25519 addition | jadep | 2016-04-20 |
* | GF25519: boring stuff -- fixed indentation and removed commented-out code | jadep | 2016-04-20 |
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-04-19 |
|\ |
|
* | | Defined a testbit variant for BaseSystem vectors and proved equivalence to Z.... | jadep | 2016-04-19 |
* | | Added lemmas to Util/ that are needed for testbit. | jadep | 2016-04-19 |
| * | Add a tactic for field inequalities | Jason Gross | 2016-04-19 |
| * | ed25519 derivation: down to final encoding | Andres Erbsen | 2016-04-17 |