Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | tuple tooling | 2016-06-20 | ||
| | | ||||
| * | port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵ | 2016-06-18 | ||
| | | | | | | | | fewer nonzero ports. remove FField and FNsatz | |||
| * | move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems | 2016-06-17 | ||
| | | ||||
| * | edwards curve addition respects field homomorphism | 2016-06-16 | ||
| | | ||||
| * | prove ring admits | 2016-06-16 | ||
| | | ||||
| * | edwards curve preliminaries: replace oncurve proof with nsatz | 2016-06-16 | ||
| | | ||||
| * | nsatz: reimplement, integrate, demonstrate | 2016-06-15 | ||
| | | ||||
| * | refactor nsatz wrappers into algebra file | 2016-06-14 | ||
| | | ||||
| * | [field] and [nsatz] do things now again | 2016-06-14 | ||
| | | ||||
| * | stuck because overloading-by-typeclasses sucks | 2016-06-13 | ||
| | | | | | | | | | | | | | | | | | | | | | | Using typeclasses for overloading clutters all users of the typeclass with an extra layer of indirection that would need to be unfolded in all proofs. Condemning all downstream Ltac to handling a new layer of definitions that have no semantic dignificance is suboptimal design (and encourages even worse design decisions like unfolding during rewriting). Overloading should be fully resolved during type inference, the resulting code must not be distinguishable from having the overloading resolved manually before entering the code. | |||
* | | Minor 8.5 changes | 2016-06-10 | ||
| | | ||||
* | | More changes for 8.5 | 2016-06-10 | ||
| | | | | | | | | [Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior | |||
| * | generic field definition | 2016-06-07 | ||
| | | ||||
| * | ERep add | 2016-05-29 | ||
| | | ||||
| * | verify derivation: EdDSA layer | 2016-05-28 | ||
| | | ||||
| * | before changing SRep from N to F l | 2016-05-27 | ||
|/ | ||||
* | slightly nicer edwards curve extended coordinates addition | 2016-05-18 | ||
| | ||||
* | ed25519: solve elliptic curve math admits | 2016-04-25 | ||
| | ||||
* | consolidate and rename Edwards curve lemmas | 2016-04-25 | ||
| | ||||
* | point_eq_dec | 2016-04-22 | ||
| | ||||
* | finished last cases of nonzero proofs for associativity | 2016-04-21 | ||
| | ||||
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | 2016-04-19 | ||
|\ | ||||
| * | Add a tactic for field inequalities | 2016-04-19 | ||
| | | | | | | | | | | Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc. | |||
* | | Cleaned up and revised DoubleAndAdd. | 2016-04-15 | ||
| | | ||||
* | | Removed old iter_op version and its last dependency. | 2016-04-15 | ||
|/ | ||||
* | Retrieved updated version of Util/IterAssocOp and modified ↵ | 2016-04-14 | ||
| | | | | ExtendedCoordinates and Ed25519 to use it. | |||
* | extended coordinates setoid boilerplate | 2016-03-20 | ||
| | ||||
* | Finish absolutizing imports | 2016-03-10 | ||
| | | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ``` | |||
* | Remove [Admitted]; [Qed] is now under a second | 2016-03-08 | ||
| | ||||
* | CompleteEdwardsCurveTheorems: associativity proof that times out on Qed | 2016-03-03 | ||
| | ||||
* | ModularArithmetic: [field] tactic that respects opacity, prettify ↵ | 2016-02-28 | ||
| | | | | ExtendedCoordinates, outline Edwards curve associativity | |||
* | moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵ | 2016-02-16 | ||
| | | | | CompleteEdwardsCurve, where the precondition is not in scope. | |||
* | cleaned up and ported definition to solve for x ^ 2 in the curve equation | 2016-02-16 | ||
| | ||||
* | remove Check | 2016-02-15 | ||
| | ||||
* | Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec | 2016-02-15 | ||
|\ | ||||
* | | ported some of EdDSA25519 to new field framework | 2016-02-15 | ||
| | | ||||
| * | port bounded iter_op and Edwards doubleAndAdd | 2016-02-15 | ||
| | | ||||
| * | CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context | 2016-02-15 | ||
|/ | ||||
* | EdDSA spec ported over to new field implementation | 2016-02-13 | ||
| | ||||
* | workaround field with typeclass modulus | 2016-02-12 | ||
| | ||||
* | fix imports | 2016-02-12 | ||
| | ||||
* | document field issue re-appearing | 2016-02-12 | ||
| | ||||
* | port some edwards curve theorems | 2016-02-12 | ||