Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove [Admitted]; [Qed] is now under a second | 2016-03-08 | |
| | |||
* | Use [rewrite] rather than [change] to speed up Qed | 2016-03-08 | |
| | | | | | | | | | | | | | [Opaque] tells kernel unification to defer unfolding a constant as long as possible. This is not a problem for [change], when the functions are small and directly convertible. It's disastrous for [Qed]/[Defined], which (if I understand correctly) try to unify [Opaquemul x' y'] with [mul x y] by fully unfolding [mul] and [x] and [y] before trying to unfold [Opaquemul]; when [x] and [y] are large, this takes a very long time. Rewrite avoids this by telling Coq *how* to unify [Opaquemul x' y'] with [mul x y] (namely, by unifying [Opaquemul] with [mul], and then [x] with [x'] and [y] with [y']). | ||
* | IterAssocOp : proved iter_op with function exponential | 2016-03-03 | |
| | |||
* | tweak to NumTheoryUtil so it builds on older Coq versions | 2016-03-03 | |
| | |||
* | CompleteEdwardsCurveTheorems: associativity proof that times out on Qed | 2016-03-03 | |
| | |||
* | Instance Fq_Integral_domain : @Integral_domain (F q) ... | 2016-02-28 | |
| | |||
* | ModularArithmetic: [field] tactic that respects opacity, prettify ↵ | 2016-02-28 | |
| | | | | ExtendedCoordinates, outline Edwards curve associativity | ||
* | Makefile: single-quotes for shell globbing | 2016-02-28 | |
| | |||
* | generic binary exponentiation correctness proof in 3 one-liners | 2016-02-26 | |
| | |||
* | ModularArithmetic: reasonable-time FieldToZ inv implementation | 2016-02-26 | |
| | |||
* | Factor out some bedrock dependencies into WordUtil | 2016-02-25 | |
| | | | | Also move a definition about words, with a TODO about location, into WordUtil. | ||
* | cleanup of bounded iter_op | 2016-02-25 | |
| | |||
* | efficient powmod | 2016-02-17 | |
| | |||
* | update ModularArithmetic tutorial | 2016-02-17 | |
| | |||
* | removed Print Assumptions | 2016-02-16 | |
| | |||
* | proved sqrt_solutions, the last remaining admit for point encodings | 2016-02-16 | |
| | |||
* | moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵ | 2016-02-16 | |
| | | | | CompleteEdwardsCurve, where the precondition is not in scope. | ||
* | proved most of point encoding admits, fixed some build system issues (dead ↵ | 2016-02-16 | |
| | | | | imports of PointFormats and Galois things) | ||
* | added point encodings; some admits remain | 2016-02-16 | |
| | |||
* | cleaned up and ported definition to solve for x ^ 2 in the curve equation | 2016-02-16 | |
| | |||
* | EdDSA: tweaked l_bound | 2016-02-15 | |
| | |||
* | fixed renamed files and added imports for encodings | 2016-02-15 | |
| | |||
* | merge | 2016-02-15 | |
|\ | |||
* | | instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ↵ | 2016-02-15 | |
| | | | | | | | | the commit looks huge) | ||
* | | added generic encoding spec | 2016-02-15 | |
| | | |||
* | | moved two non-primality-dependent lemmas to ModularArithmeticTheorems from ↵ | 2016-02-15 | |
| | | | | | | | | PrimeFieldTheorems | ||
* | | a few lemmas in util about powers of 2 in Bedrock's various rewritten forms | 2016-02-15 | |
| | | |||
| * | Finish seperating our specs: remove old non-specified code | 2016-02-15 | |
| | | |||
| * | 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 | |
| | | |||
* | | added square roots and an assortment of lemmas about prime fields/rings | 2016-02-15 | |
| | | |||
* | | changed the name of the ring to ring, not field | 2016-02-15 | |
| | | |||
* | | tweaks to util files, including automation for proving ↵ | 2016-02-15 | |
| | | | | | | | | positivity/nonnegativity in Z | ||
| * | port bounded iter_op and Edwards doubleAndAdd | 2016-02-15 | |
| | | |||
| * | CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context | 2016-02-15 | |
|/ | |||
* | update F Coercions and tutorial | 2016-02-14 | |
| | |||
* | port ModularBaseSystem.v and GF25519.v to F m | 2016-02-14 | |
| | |||
* | Spec/EdDSA: comments, remove prehashing | 2016-02-13 | |
| | |||
* | Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v | 2016-02-13 | |
| | |||
* | prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd ↵ | 2016-02-13 | |
| | | | | Closed Under Global Context | ||
* | Merge branch 'master' into spec | 2016-02-13 | |
|\ | |||
| * | EdDSA spec ported over to new field implementation | 2016-02-13 | |
| | | |||
* | | implement F_opp | 2016-02-12 | |
| | | |||
| * | Merge branch 'spec' of github.mit.edu:plv/fiat-crypto | 2016-02-12 | |
| |\ | |/ |/| | |||
| * | EdDSA25519: progress on proving PointEncoding admits; code still unorganized | 2016-02-12 | |
| | | |||
* | | 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 | |
| | |