| Commit message (Expand) | Author | Age |
|---|
| * | Factor out cmov{l,ne} and neg |  Jason Gross | 2016-10-27 |
| * | Simplify proof of proj1_fe25519_encode | Jason Gross | 2016-10-27 |
| * | Add lemmas about GF25519BoundedCommon.{encode,decode} | Jason Gross | 2016-10-27 |
| * | Switch to bounded Z | Jason Gross | 2016-10-25 |
| * | Adjust bound on final word in wire_digits to 31 | Jason Gross | 2016-10-24 |
| * | Fix bounds on wire_digits | Jason Gross | 2016-10-24 |
| * | Add pack, unpack, ge_modulus to axioms to be reified | Jason Gross | 2016-10-24 |
| * | Created separate definitions for cmovne and cmovl for reification |  jadep | 2016-10-23 |
| * | Finish twedprm_ERep proof | Jason Gross | 2016-10-23 |
| * | Make some things instances | Jason Gross | 2016-10-23 |
| * | Generalize field_from_redundant_representation | Jason Gross | 2016-10-23 |
| * | Add decode to GF25519BoundedCommon | Jason Gross | 2016-10-22 |
| * | Make [vm_compute] on Bounded word reasonable | Jason Gross | 2016-10-22 |
| * | Fix divergence in src/Specific/GF25519Bounded.v | Jason Gross | 2016-10-22 |
| * | Unfold interp stuff in Assembly/GF25519BoundedInstantiation | Jason Gross | 2016-10-22 |
| * | Add bounded sqrt | Jason Gross | 2016-10-22 |
| * | final touches/fixes for freeze restructuring | jadep | 2016-10-22 |
| * | add arguments that I forgot | jadep | 2016-10-22 |
| * | Modified [freeze] to be more reifyable | jadep | 2016-10-22 |
| * | pow, not pow_opt, in Specific/GF25519 | Jason Gross | 2016-10-21 |
| * | Add word64eqb_Zeqb | Jason Gross | 2016-10-21 |
| * | Sane fieldwiseb | Jason Gross | 2016-10-21 |
| * | Make eqb sane (help from Jade) | Jason Gross | 2016-10-21 |
| * | Remove axioms from src/Specific/GF25519Bounded.v, plug assembly | Jason Gross | 2016-10-21 |
| * | A bit of initial setup on correct_and_bounded proofs in GF25519BoundedInstant... | Jason Gross | 2016-10-20 |
| * | Plug bounded into assembly stuff | Jason Gross | 2016-10-20 |
| * | Remove code that should have been removed | Jason Gross | 2016-10-20 |
| * | Split up GF25519Bounded to avoid circular dependencies | Jason Gross | 2016-10-20 |
| * | Add todo | Jason Gross | 2016-10-20 |
| * | Switch from bounded Z to bounded word | Jason Gross | 2016-10-20 |
| * | More specific bounded requirements, implement inv | Jason Gross | 2016-10-19 |
| * | First pass at bounded version of GF25519 | Jason Gross | 2016-10-19 |
| * | Removed the lingering TODO and print statement that @JasonGross helpfully poi... | jadep | 2016-10-19 |
| * | Fill in admits for field with carry_add, carry_opp, and carry_sub | jadep | 2016-10-19 |
| * | Define carry_opp in terms of carry_sub | Jason Gross | 2016-10-19 |
| * | Add opt versions of add, sub, opp | Jason Gross | 2016-10-19 |
| * | Fix out of memory error for 8.5,8.5pl1 | Jason Gross | 2016-10-19 |
| * | Fix for Coq 8.4 evar propogation | Jason Gross | 2016-10-18 |
| * | Fix missing imports | Jason Gross | 2016-10-17 |
| * | Remove broken imports | Jason Gross | 2016-10-17 |
| * | Rename and clean up exponent code | Jason Gross | 2016-10-17 |
| * | Remove admits with the help of Andres | Jason Gross | 2016-10-17 |
| * | Fill in more proofs | Jason Gross | 2016-10-17 |
| * | Initial work on exponent field as Z | Jason Gross | 2016-10-17 |
| * | 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 |
| * | Split up DoubleBoundedProofs, add proofs | Jason Gross | 2016-10-07 |
| * | Moved conversion logic out of Pow2BaseProofs into its own file | jadep | 2016-10-06 |
| * | Add bitwise and, remove mkl from fancy | Jason Gross | 2016-10-03 |
| * | Work around bug #5112 ([Arguments id /] broken) | Jason Gross | 2016-10-03 |
Jason Gross
jadep