Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add transparent equality proofs for fixed wordT | Jason Gross | 2017-01-21 |
| | | | | Such a pain to make proofs compute | ||
* | Revert "Fix a missing qualification" | Jason Gross | 2017-01-21 |
| | | | | | | | | | | This reverts commit 3c4ff8fe8d2154addcf440690d315c58a529c1f6. Revert "Move weqb_hetero to Bedrock.Word" This reverts commit c83cb07f1477de33ce9eb43eea6a4f2720a94763. We probably shouldn't modify Bedrock.Word | ||
* | Fix a missing qualification | Jason Gross | 2017-01-21 |
| | |||
* | Move weqb_hetero to Bedrock.Word | Jason Gross | 2017-01-21 |
| | |||
* | Add weqb_hetero | Jason Gross | 2017-01-21 |
| | |||
* | Lemmas about winit, wlast | Rob Sloan | 2016-11-11 |
| | |||
* | Fix for Coq 8.4 | Jason Gross | 2016-11-11 |
| | | | | Tactic notations in sections are automatically local | ||
* | Most of the admits in Ed25519.v | Rob Sloan | 2016-11-11 |
| | |||
* | Fix for 8.4 | Jason Gross | 2016-11-10 |
| | |||
* | Hint Rewrite is section-local; move to top-level | Jason Gross | 2016-11-10 |
| | |||
* | Remove WordizeUtil dependency from WordUtil | Rob Sloan | 2016-11-09 |
| | |||
* | Rebase + remove WordizeUtil dependency from Z/Interpretations | Rob Sloan | 2016-11-09 |
|\ | |||
| * | Rewrite cast_word so that it's extracted better | Jason Gross | 2016-11-09 |
| | | | | | | | | | | | | | | | | It will now be extracted as the identity function automatically, so we don't need to manually extract it as the empty string. This should also fix #93. (I think the issue was that this was an instance of https://coq.inria.fr/bugs/show_bug.cgi?id=4243.) | ||
* | | Finished WordUtil, word operations in Z/Interpretation | Rob Sloan | 2016-11-09 |
| | | |||
* | | Not quite done with WordUtil lemmas. | Robert Sloan | 2016-11-08 |
|\| | |||
| * | put EdDSA encoding sign bit at the MSB | Andres Erbsen | 2016-11-04 |
| | | |||
* | | More of jgross admits, less neg and the cmovs | Rob Sloan | 2016-11-01 |
| | | |||
* | | most of jgross' admits | Rob Sloan | 2016-10-31 |
|/ | | | | ' | ||
* | Some work on proofs in src/Reflection/Z/Interpretations.v | Jason Gross | 2016-10-27 |
| | |||
* | Add some rewrites and admitted lemmas | Jason Gross | 2016-10-27 |
| | |||
* | Add beginnings of various interpretations of expression trees | Jason Gross | 2016-10-27 |
| | |||
* | More 8.4 fixes | Jason Gross | 2016-10-23 |
| | |||
* | Prove more things in WordUtil | Jason Gross | 2016-10-23 |
| | | | | The proofs should be automated eventually... | ||
* | Fill in some word util admitted lemmas | Jason Gross | 2016-10-23 |
| | |||
* | Add word64eqb_Zeqb | Jason Gross | 2016-10-21 |
| | |||
* | integrate bitwise operations | Andres Erbsen | 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 |
| | | | | | | | | | | * wordsize automation hooks and examples * wordToNat_cast_word * WordUtil: make [wordsize_eq] transparent * address code review comments | ||
* | Derive EdDSA.verify from equational specification | Andres Erbsen | 2016-09-16 |
| | | | | Experiments/SpecEd25519 will come back soon | ||
* | Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to | jadep | 2016-04-29 |
| | | | | comparing points). | ||
* | Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵ | jadep | 2016-04-28 |
| | | | | general contexts. | ||
* | Finish absolutizing imports | Jason Gross | 2016-03-10 |
| | | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ``` | ||
* | Factor out some bedrock dependencies into WordUtil | Jason Gross | 2016-02-25 |
Also move a definition about words, with a TODO about location, into WordUtil. |