Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Removed lingering print statement. | jadep | 2016-07-21 |
| | |||
* | re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵ | jadep | 2016-07-21 |
| | | | | organization of reasoning. | ||
* | restructured ModularBaseSystem pipeline to put tuple conversion before ↵ | jadep | 2016-07-20 |
| | | | | ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt | ||
* | Fixed unsimplified multiplication definitions in Specific by separating out ↵ | jadep | 2016-07-18 |
| | | | | the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions. | ||
* | more changes to Specific for 8.4 compatibility | jadep | 2016-07-15 |
| | |||
* | re-cleaned operations in Specific and updated GF25519 to match GF1305 | jadep | 2016-07-12 |
| | |||
* | cleaned Specific operations so they produce code without proof terms, and ↵ | jadep | 2016-07-12 |
| | | | | proved that GF1305 is a field | ||
* | pushing through a tweak to the arguments of [sub], and defining a field over ↵ | jadep | 2016-07-12 |
| | | | | ModularBaseSystemInterface using some placeholder operations. | ||
* | ported Specific files to use ModularBaseSystemInterface | jadep | 2016-07-11 |
| | |||
* | defined some group operations, stated group lemma for tuple-based [add] (in ↵ | jadep | 2016-07-08 |
| | | | | terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor | ||
* | stuck trying to figure out dependently typed continuation passing style | Andres Erbsen | 2016-07-06 |
| | |||
* | Aggregate all level specifications not in Spec/* | Jason Gross | 2016-06-22 |
| | | | | | This prevents notation conflicts (see comment in Notations.v for more explanation). | ||
* | remove obsolete rep mechanism | Andres Erbsen | 2016-06-20 |
| | |||
* | GF25519: quiet | Andres Erbsen | 2016-06-20 |
| | |||
* | Merge branch 'field-experiment' | Andres Erbsen | 2016-06-20 |
|\ | | | | | | | includes broken files to be removed in next commit | ||
* | | Canonicalization is now automated in GF25519 and added to GF1305. | jadep | 2016-06-17 |
| | | |||
* | | Specific version of freeze for GF25519 (automation still needs a little work) | jadep | 2016-06-17 |
| | | |||
* | | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵ | jadep | 2016-06-15 |
| | | | | | | | | base-length digit vectors) | ||
* | | Another fix for an anomaly in 8.4pl2 | Jason Gross | 2016-06-11 |
| | | |||
* | | Work around bug #4811 (slow f_equal) | Jason Gross | 2016-06-11 |
| | | | | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal] loops(?) in 8.5pl1 (fixed already in 8.5.dev) | ||
| * | ed25519: refactor some Proper | Andres Erbsen | 2016-06-06 |
| | | |||
| * | rewrite in Let_In binder by tactic | Andres Erbsen | 2016-06-04 |
| | | |||
| * | Let_In rewriting | Andres Erbsen | 2016-06-03 |
| | | |||
| * | leibniz equal version of topdown rewriting of sigma types: nicer | Andres Erbsen | 2016-06-01 |
| | | |||
| * | 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 ↵ | Andres Erbsen | 2016-05-28 |
| | | | | | | | | ERep and SRep | ||
| * | 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 |
|/ | |||
* | 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 |
| | |||
* | 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... | ||
* | unifiedAddM1Rep_sig: almost there | 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. | ||
* | 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). | ||
* | 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 |
| | |