fiat-crypto - fast, formally verified cryptography

	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.