| Commit message (Expand) | Author | Age |
|---|
| * | rename-everything |  Andres Erbsen | 2017-04-06 |
| * | do not use VerdiTactics in files we plan to keep | Andres Erbsen | 2017-04-06 |
| * | Add [Proof using] to most proofs |  Jason Gross | 2017-04-04 |
| * | More fine-grained tactic imports | Jason Gross | 2017-04-03 |
| * | make fsatz recurse when proving nonzero-ness, undo Weierstrass workaround | Andres Erbsen | 2017-03-30 |
| * | CompleteEdwardsCurveTheorems: point compression | Andres Erbsen | 2017-03-02 |
| * | use [positive] for [F] modulus, char_ge_C instead of char_gt_C | Andres Erbsen | 2017-03-02 |
| * | rewrite ExtendedCoordinates, fix Ed25519 | Andres Erbsen | 2017-03-02 |
| * | edwards curves over isomorphic fields | Andres Erbsen | 2017-03-02 |
| * | WIP | Andres Erbsen | 2017-03-02 |
| * | split the algebra library; use fsatz more | Andres Erbsen | 2017-03-02 |
| * | fsatz, nsatz_solve_nonzero | Andres Erbsen | 2017-03-02 |
| * | use field_nsatz in CompleteEdwardsCurve.Pre | Andres Erbsen | 2017-03-02 |
| * | refactor scalar multiplication thoery, implement SRepERepMul | Andres Erbsen | 2016-10-12 |
| * | remove eq_dec from Monoid | Andres Erbsen | 2016-08-23 |
| * | Refactor ModularArithmetic into Zmod, expand Decidable | Andres Erbsen | 2016-08-04 |
| * | Move most notation level declarations into Util |  Jason Gross | 2016-07-27 |
| * | Make the library 20% faster: [auto with *] is evil | Jason Gross | 2016-07-22 |
| * | proved an admit in field homomorphisms that turned out to be unprovable; I ad... |  jadep | 2016-07-15 |
| * | s/conservative_common_denominator/common_denominator/g | Andres Erbsen | 2016-07-11 |
| * | port CompleteEdwardsCurveTheorems (builds again) | Andres Erbsen | 2016-07-11 |
| * | pose proof fails where specialize works (typeclass resolution / unification?) | Andres Erbsen | 2016-07-11 |
| * | wrap nsatz in Algebra | Andres Erbsen | 2016-07-11 |
| * | added proofs about addition chain exponentiation for later use in ModularBase... | jadep | 2016-07-10 |
| * | scalarmult support; EdDSA.sign produces valid signatures | Andres Erbsen | 2016-06-27 |
| * | Use Decidable machinery for is_eq_dec | Jason Gross | 2016-06-24 |
| * | Fix broken notations (hopefully) | Jason Gross | 2016-06-22 |
| * | Aggregate all level specifications not in Spec/* | Jason Gross | 2016-06-22 |
| * | Use Admitted, not Qed, when a proof has admit | Jason Gross | 2016-06-21 |
| * | Fix [Proper_add] in 8.5 | Jason Gross | 2016-06-21 |
| * | Make [bash] tactic easier to debug | Jason Gross | 2016-06-21 |
| * | use Local Obligation Tactic (8.5-compat) | Andres Erbsen | 2016-06-21 |
| * | remove trailing whitespace from src/ | Andres Erbsen | 2016-06-20 |
| * | move nsatz into tactics directory | Andres Erbsen | 2016-06-20 |
| * | tuple tooling | Andres Erbsen | 2016-06-20 |
| * | port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer... | Andres Erbsen | 2016-06-18 |
| * | move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems | Andres Erbsen | 2016-06-17 |
| * | verify derivation: EdDSA layer | Andres Erbsen | 2016-05-28 |
| * | consolidate and rename Edwards curve lemmas | 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 |
| * | Add a tactic for field inequalities | Jason Gross | 2016-04-19 |
| * | Finish absolutizing imports | Jason Gross | 2016-03-10 |
| * | Remove [Admitted]; [Qed] is now under a second | Jason Gross | 2016-03-08 |
| * | CompleteEdwardsCurveTheorems: associativity proof that times out on Qed | Andres Erbsen | 2016-03-03 |
| * | ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo... | Andres Erbsen | 2016-02-28 |
| * | moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ... |  Jade Philipoom | 2016-02-16 |
| * | cleaned up and ported definition to solve for x ^ 2 in the curve equation | Jade Philipoom | 2016-02-16 |
| * | remove Check | Andres Erbsen | 2016-02-15 |
| * | ported some of EdDSA25519 to new field framework | Jade Philipoom | 2016-02-15 |
Andres Erbsen
Jason Gross
Jason Gross
jadep
Jade Philipoom