| Commit message (Expand) | Author | Age |
* | Not quite done with WordUtil lemmas. | Robert Sloan | 2016-11-08 |
|\ |
|
* | | More of jgross admits, less neg and the cmovs | Rob Sloan | 2016-11-01 |
| * | Switch to reflective bounded word in Ed25519 | Jason Gross | 2016-10-31 |
* | | most of jgross' admits | Rob Sloan | 2016-10-31 |
| * | Silence a warning | Jason Gross | 2016-10-31 |
| * | Significantly faster wordToN, I hope | Jason Gross | 2016-10-31 |
|/ |
|
* | Disable extraction in src/Assembly/GF25519.v | Jason Gross | 2016-10-29 |
* | Disable some printing | Jason Gross | 2016-10-29 |
* | Merge branch 'master' into rsloan-phoas | Jason Gross | 2016-10-27 |
|\ |
|
* | | Fixes for Coq 8.4 | Jason Gross | 2016-10-27 |
* | | Strip function extensionality, enable printing of sub, mul, opp, freeze | Jason Gross | 2016-10-27 |
* | | Tactics to manually remove Z.to/of_N and such | Robert Sloan | 2016-10-26 |
* | | Refactors to remove intermediate conversions | Robert Sloan | 2016-10-26 |
| * | Switch to bounded Z | Jason Gross | 2016-10-25 |
* | | Refactors to remove intermediate conversions in HLConversions | Robert Sloan | 2016-10-25 |
* | | Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoas | Robert Sloan | 2016-10-24 |
|\ \ |
|
* | | | Use HL conversions for all data types + Pipeline.v refactors | Robert Sloan | 2016-10-24 |
| | * | Add pack, unpack, ge_modulus to axioms to be reified | Jason Gross | 2016-10-24 |
| | * | Fix for weaker pattern matching in < 8.4pl4 | Jason Gross | 2016-10-22 |
| | * | Fix for weaker pattern matching in < 8.4pl4 | Jason Gross | 2016-10-22 |
| * | | More Coq 8.4 fixes | Jason Gross | 2016-10-22 |
| * | | Fix 8.4 build | Jason Gross | 2016-10-22 |
| * | | cbn does not exist in 8.4 | Jason Gross | 2016-10-22 |
| * | | Fix 8.4 build | Jason Gross | 2016-10-22 |
| * | | Fix build failure in 8.6 | Jason Gross | 2016-10-22 |
| * | | Merge branch 'master' into pr/84 | Jason Gross | 2016-10-22 |
|/| |
| |/ |
|
| * | Unfold interp stuff in Assembly/GF25519BoundedInstantiation | Jason Gross | 2016-10-22 |
| * | Interpret LetIn to Let_In for better control of interp | Jason Gross | 2016-10-22 |
* | | Make lower bounds work by using HL conversions | Robert Sloan | 2016-10-21 |
* | | merge rsloan-phoas refactors into master | Robert Sloan | 2016-10-21 |
|\ \ |
|
* \ \ | merge rsloan-phoas refactors into master | Robert Sloan | 2016-10-21 |
|\ \ \
| | |/
| |/| |
|
* | | | committing unstable refactors to patch master | Robert Sloan | 2016-10-21 |
| * | | Instantiate some things with bounded things | Jason Gross | 2016-10-21 |
| | * | committing unstable refactors to patch master | Robert Sloan | 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 |
| * | Adjust bounds in assembly | Jason Gross | 2016-10-20 |
| * | Split up GF25519Bounded to avoid circular dependencies | Jason Gross | 2016-10-20 |
| * | Various fixes for Coq 8.4 | Jason Gross | 2016-10-20 |
| * | Use carry versions of operations | Jason Gross | 2016-10-20 |
| * | rfreeze, not rinv; update to saner boundedness requirements | Jason Gross | 2016-10-20 |
| * | Start instantiating boundedness things | Jason Gross | 2016-10-19 |
|/ |
|
* | Fast bounds-checking machinery but lower-bounds are broken | Robert Sloan | 2016-10-18 |
* | Converting to bounded machinery | Robert Sloan | 2016-10-17 |
* | More of the Conversions.v correctness proofs | Robert Sloan | 2016-10-14 |
* | Use 64-bit limbs in Pipelines | Robert Sloan | 2016-10-14 |
* | Making sub bounds actually tight | Robert Sloan | 2016-10-14 |
* | Moved to non-extended operations + Extraction + Bounds-checking | Robert Sloan | 2016-10-14 |
* | Well, here's the program instance. The string conversion is still running. | Robert Sloan | 2016-10-13 |
* | More minor improvements in Conversions.v and Compile.v | Robert Sloan | 2016-10-13 |