Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 |
| | | | | | | | | reason I wasn't affected. Also updated the same file to use E module. | ||
| * | 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 |
| | | | | | | | | Slightly less [apply f_equal] beforehand, more automation. | ||
| * | Remove unfolding, rewrite -> setoid_rewrite | Jason Gross | 2016-05-24 |
| | | | | | | | | | | | | | | | | | | | | Moving the [scalar] argument to the beginning of [iter_op] makes inference of the [Proper] lemmas a bit easier. Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows [setoid_rewrite] to work; since [setoid_rewrite] does more unfolding than [rewrite], we no longer need to unfold things to make the [rewrite] work. | ||
| * | Fix some issues in Ed25519 tactics | Jason Gross | 2016-05-24 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Use replace rather than refine to speed up [Defined] and make the tactics easier to read - Use [apply f_equal] in place of [reflexivity] for unknown presumably arcane reasons to satisfy Coq's unifier - Factor out some tactics into tactic scripts - Write a lemma to pull functions out of [Let_In] - Fix autoindentation in emacs by wrapping [Let_In_unRep] in parentheses (probably a ProofGeneral regexp gone wrong) - Write a kludgy tactic to unfold [proj1_sig] only when applied to [exist] (Pair programming with Andres) | ||
| * | F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵ | Andres Erbsen | 2016-05-24 |
| | | | | | | | | broken... | ||
* | | First stage of canonicalization proofs complete; proved 3 carry loops reduce ↵ | jadep | 2016-05-20 |
| | | | | | | | | input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1]) | ||
| * | 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 |
| | | | | unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want. | ||
* | 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 |
| | | | | comparing points). | ||
* | Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵ | jadep | 2016-04-28 |
| | | | | general contexts. | ||
* | Completed encoding reorganization; factored sign_bit out of PointEncodings ↵ | jadep | 2016-04-28 |
| | | | | and finished encoding admits. | ||
* | 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 ↵ | jadep | 2016-04-25 |
| | | | | | | | | function. | ||
| * | 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 |
| | | | | weight 2^26) | ||
* | 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 ↵ | jadep | 2016-04-19 |
| | | | | | | | | Z.testbit. | ||
* | | Added lemmas to Util/ that are needed for testbit. | jadep | 2016-04-19 |
| | | |||
| * | Add a tactic for field inequalities | Jason Gross | 2016-04-19 |
| | | | | | | | | | | Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc. | ||
| * | ed25519 derivation: down to final encoding | Andres Erbsen | 2016-04-17 |
| | | |||
| * | ed25519 derivation: use representation of F | Andres Erbsen | 2016-04-17 |
| | | |||
| * | ed25519 derivation: wrangle non-unique representations | Andres Erbsen | 2016-04-16 |
| | | |||
| * | ed25519 derivation: stuck at main loop | Andres Erbsen | 2016-04-16 |
| | | |||
| * | ed25519 derivation down to word until main equation | Andres Erbsen | 2016-04-16 |
| | | |||
* | | Cleaned up and revised DoubleAndAdd. | jadep | 2016-04-15 |
| | | |||
* | | Removed old iter_op version and its last dependency. | jadep | 2016-04-15 |
|/ | |||
* | Retrieved updated version of Util/IterAssocOp and modified ↵ | jadep | 2016-04-14 |
| | | | | ExtendedCoordinates and Ed25519 to use it. | ||
* | Fixed syntax error (missing bracket) in Ed25519 to make merge build | jadep | 2016-04-12 |
| | |||
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-04-12 |
|\ |