| Commit message (Expand) | Author | Age |
|---|
| * | move B_order_l and prime_q |  Andres Erbsen | 2016-11-06 |
| * | Refactor various reflective things |  Jason Gross | 2016-11-06 |
| * | Connect [is_bounded] to [bounded_by] | Jason Gross | 2016-11-06 |
| * | The fix in 8.4 broke 8.5/8.6, so we fix that | Jason Gross | 2016-11-06 |
| * | Add syntactic tuples | Jason Gross | 2016-11-06 |
| * | Add support for dependent reification | Jason Gross | 2016-11-06 |
| * | Work around broken evars in 8.4 | Jason Gross | 2016-11-06 |
| * | Plug in boundedness proofs | Jason Gross | 2016-11-05 |
| * | Add better bounded lemmas to reified things | Jason Gross | 2016-11-05 |
| * | Add eta-expansion in GF25519BoundedCommon.v | Jason Gross | 2016-11-05 |
| * | Add proofs about boundedness to GF25519Reflective/Common.v | Jason Gross | 2016-11-05 |
| * | Add unfold_is_bounded | Jason Gross | 2016-11-05 |
| * | Add code for overflow check (disabled bc freeze) | Jason Gross | 2016-11-05 |
| * | Split off some things from Interpretations | Jason Gross | 2016-11-05 |
| * | separate Ed25519Extraction.v, add extraction to Makefile | Andres Erbsen | 2016-11-03 |
| * | Shove Z.Interpretations into closer alignment | Jason Gross | 2016-11-03 |
| * | Fix build | Jason Gross | 2016-11-03 |
| * | Make [freeze] proofs consider machine integer width and hard input bounds sep... |  jadep | 2016-11-03 |
| * | Fix bounds that were reversed | Jason Gross | 2016-11-03 |
| * | Clean up fe25519_word64ize, give examples | Jason Gross | 2016-11-02 |
| * | GF25519BoundedCommon.v: require less higher order unification (8.4) | Andres Erbsen | 2016-11-02 |
| * | fix lingering reference to old name of renamed lemma | jadep | 2016-11-02 |
| * | Fix GF25519Bounded in a different way | Jason Gross | 2016-11-02 |
| * | Fix [sqrtW_sig] | Jason Gross | 2016-11-02 |
| * | Changes to sqrt for easier bounds proofs; currently blocked on broken proof i... | jadep | 2016-11-02 |
| * | Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBar | Jason Gross | 2016-11-01 |
| * | Export strings in GF25519Reflective/Common | Jason Gross | 2016-11-01 |
| * | Print out the computed bounds on the various ops | Jason Gross | 2016-11-01 |
| * | Parameterize bounded things over the limb length | Jason Gross | 2016-11-01 |
| * | Add fe25519WToZToW | Jason Gross | 2016-11-01 |
| * | Make it easier to extract word64 | Jason Gross | 2016-10-31 |
| * | Add bounds type in Specific/GF25519Reflective/Common.v | Jason Gross | 2016-10-31 |
| * | Make it so that changing the list of wire bounds doesn't break the build | Jason Gross | 2016-10-31 |
| * | Revert "Switch from word to Z" | Jason Gross | 2016-10-31 |
| * | Switch from word to Z | Jason Gross | 2016-10-31 |
| * | Switch to reflective bounded word in Ed25519 | Jason Gross | 2016-10-31 |
| * | Use sigma types to fix extraction | Jason Gross | 2016-10-31 |
| * | Add src/Specific/GF25519Reflective.v | Jason Gross | 2016-10-31 |
| * | Also construct relatedness proofs in reified | Jason Gross | 2016-10-30 |
| * | Minor changes to GF25519 reflective | Jason Gross | 2016-10-30 |
| * | Add reification of various operations | Jason Gross | 2016-10-30 |
| * | Add initial work on reifying GF25519 stuff | Jason Gross | 2016-10-30 |
| * | Add things like app_7 to GF25519BoundedCommonWord.v | Jason Gross | 2016-10-29 |
| * | Add interp_type_gen_rel_pointwise2, *_gen => * | Jason Gross | 2016-10-28 |
| * | Add {un,}curry_wire_digits | Jason Gross | 2016-10-27 |
| * | Add {un,}curry_{bin,un}op_fe25519 | Jason Gross | 2016-10-27 |
| * | Add length_fe25519 | Jason Gross | 2016-10-27 |
| * | 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 |
Andres Erbsen
Jason Gross
jadep