| Commit message (Expand) | Author | Age |
|---|
| * | Fix for Coq 8.4 |  Jason Gross | 2016-10-13 |
| * | Add src/BoundedArithmetic/Eta.v | Jason Gross | 2016-10-13 |
| * | refactor scalar multiplication thoery, implement SRepERepMul |  Andres Erbsen | 2016-10-12 |
| * | Fixed naming issue |  jadep | 2016-10-12 |
| * | defined sign operation on field elements | jadep | 2016-10-12 |
| * | Fixing merge conflict | jadep | 2016-10-12 |
| * | Clean up ge_modulus definition in Specific | jadep | 2016-10-12 |
| * | Added top-level modulus comparison operation so field-element decoding can re... | jadep | 2016-10-12 |
| * | integrate bitwise operations | Andres Erbsen | 2016-10-12 |
| * | generalize equiv relations in Util.Option and EdDSARepChange | Andres Erbsen | 2016-10-12 |
| * | remove Experiments.EncodingLemmas (superseded by Jade's recent work) | Andres Erbsen | 2016-10-12 |
| * | Add Ed25519 to _CoqProject | Jason Gross | 2016-10-12 |
| * | Generalize and simplify cast_word_refl | Jason Gross | 2016-10-12 |
| * | word manipulation functions for secret key formatting (#74) | Andres Erbsen | 2016-10-12 |
| * | Fix for missing Nat.log2 in 8.4 | Jason Gross | 2016-10-11 |
| * | Fix for missing Nat.log2 in 8.4 | Jason Gross | 2016-10-11 |
| * | specialize_by: only specialize arguments of type [Prop] | Andres Erbsen | 2016-10-10 |
| * | specialize_by: explicitly maintain transparency | Andres Erbsen | 2016-10-10 |
| * | Starting to fill in Ed25519 context variables | jadep | 2016-10-10 |
| * | Filled in point/scalar encoding definitions. | jadep | 2016-10-10 |
| * | Added helper lemma to Algebra. | jadep | 2016-10-10 |
| * | Bundle arguments to Barrett Reduction | Jason Gross | 2016-10-10 |
| * | Ed25519: add basepoint and prove most EdDSA preconditions | Andres Erbsen | 2016-10-10 |
| * | Add some admitted x86->ZLike proofs | Jason Gross | 2016-10-10 |
| * | Work around bug 5003 (broken omega on projections) | Jason Gross | 2016-10-10 |
| * | Spec.Ed25519: prove that Curve25519 is an elliptic curve | Andres Erbsen | 2016-10-10 |
| * | Decidable: add [Z] and [nat] inequalities | Andres Erbsen | 2016-10-10 |
| * | Fix compatibility with sigT notation | Jason Gross | 2016-10-10 |
| * | Spec.Ed25519: fix exponent field modulus | Andres Erbsen | 2016-10-10 |
| * | Add definitions for x86 | Jason Gross | 2016-10-10 |
| * | Add repeated multiple | Jason Gross | 2016-10-10 |
| * | Add shl,shr,shrd to repeated doubling | Jason Gross | 2016-10-09 |
| * | Add proofs for doubling shl,shr,shrd | Jason Gross | 2016-10-09 |
| * | Make Ztestbit_full | Jason Gross | 2016-10-09 |
| * | Fix Ztestbit_full database | Jason Gross | 2016-10-09 |
| * | Fix shiftr_spec_full | Jason Gross | 2016-10-09 |
| * | Add more to Ztestbit_full | Jason Gross | 2016-10-09 |
| * | Add a Ztestbit_full database | Jason Gross | 2016-10-09 |
| * | Some work on x86 and bounded repeated things | Jason Gross | 2016-10-09 |
| * | Add some bounded decode/and things | Jason Gross | 2016-10-09 |
| * | Split up DoubleBoundedProofs, add proofs | Jason Gross | 2016-10-07 |
| * | Stronger Ztestbit, convert_to_ztestbit | Jason Gross | 2016-10-07 |
| * | More zsimplify lemmas, stronger Ztestbit | Jason Gross | 2016-10-07 |
| * | Add eta_expand to Prod.v | Jason Gross | 2016-10-07 |
| * | Add a variant of [map] on reflective things that changes the interp function | Jason Gross | 2016-10-07 |
| * | Weaken hyps of lor_range, add it to zarith | Jason Gross | 2016-10-07 |
| * | Moved lemma to ZUtil and added an extra lemma jgross needed | jadep | 2016-10-06 |
| * | Add testbit_add_shiftl_full | Jason Gross | 2016-10-06 |
| * | Use zutil_arith for side-conditions in testbit | Jason Gross | 2016-10-06 |
| * | Add Z.pow_le_mono_{r,l} to zarith | Jason Gross | 2016-10-06 |
Jason Gross
Andres Erbsen
jadep