fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
*	Add reification of various operations	Jason Gross	2016-10-30
*	Add initial work on reifying GF25519 stuff	Jason Gross	2016-10-30
*	Add InterpWf	Jason Gross	2016-10-28
*	Add InterpWfRel	Jason Gross	2016-10-28
*	Add beginnings of various interpretations of expression trees	Jason Gross	2016-10-27
*	Merge pull request #84 from mit-plv/rsloan-phoas	Jason Gross	2016-10-27
\|\
* \|	Add syntax and reification for the ops in GF25519	Jason Gross	2016-10-27
* \|	Factor out cmov{l,ne} and neg	Jason Gross	2016-10-27
* \|	Add WfRelReflective	Jason Gross	2016-10-27
* \|	Add WfReflectiveGen	Jason Gross	2016-10-27
* \|	Add Wf proofs about MapInterp	Jason Gross	2016-10-27
\| *	Merge branch 'master' into rsloan-phoas	Jason Gross	2016-10-27
\| \|\ \| \|/ \|/\|
* \|	Switch to bounded Z	Jason Gross	2016-10-25
\| *	Fix 8.4 build	Jason Gross	2016-10-22
\| *	Merge branch 'master' into pr/84	Jason Gross	2016-10-22
\| \|\ \| \|/ \|/\|
* \|	Fix src/Experiments/Ed25519.v for Coq 8.4	Jason Gross	2016-10-22
\| *	merge rsloan-phoas refactors into master	Robert Sloan	2016-10-21
\| \|\ \| \|/ \|/\|
\| *	committing unstable refactors to patch master	Robert Sloan	2016-10-21
* \|	Split up GF25519Bounded to avoid circular dependencies	Jason Gross	2016-10-20
* \|	Merge branch 'master' into instantiation-rsloan-phoas	Jason Gross	2016-10-20
\|\ \
\| * \|	First pass at bounded version of GF25519	Jason Gross	2016-10-19
* \| \|	Start instantiating boundedness things	Jason Gross	2016-10-19
\| \|/ \|/\|
\| *	Rename and clean up exponent code	Jason Gross	2016-10-17
\| *	Initial work on exponent field as Z	Jason Gross	2016-10-17
\| *	Add Z as ZBounded	Jason Gross	2016-10-16
* \|	Making sub bounds actually tight	Robert Sloan	2016-10-14
* \|	Minor refactors waiting for the code generation to finish	Robert Sloan	2016-10-13
\| *	Add src/BoundedArithmetic/Eta.v	Jason Gross	2016-10-13
\| *	remove EncodingLemmas from _CoqProject (file deleted by Andres in commit 9379...	jadep	2016-10-12
\| *	Add Ed25519 to _CoqProject	Jason Gross	2016-10-12
\| *	Add some admitted x86->ZLike proofs	Jason Gross	2016-10-10
\| *	Update _CoqProject	Jason Gross	2016-10-10
\| *	Add shl,shr,shrd to repeated doubling	Jason Gross	2016-10-09
\| *	Add proofs for doubling shl,shr,shrd	Jason Gross	2016-10-09
\| *	Some work on x86 and bounded repeated things	Jason Gross	2016-10-09
\| *	Split up DoubleBoundedProofs, add proofs	Jason Gross	2016-10-07
\| *	Add a variant of [map] on reflective things that changes the interp function	Jason Gross	2016-10-07
* \|	Merge _CoqProject	Rob Sloan	2016-10-06
\|\ \
\| \| *	Moved PointEncoding out of Spec	jadep	2016-10-06
\| \| *	Moved conversion logic out of Pow2BaseProofs into its own file	jadep	2016-10-06
\| \| *	Add some more instructions	Jason Gross	2016-10-04
\| \|/ \|/\|
* \|	Wrote proofs necessary to fill in all point-encoding related context variable...	jadep	2016-10-03
* \|	Spec: add ed25519	Andres Erbsen	2016-10-03
\| *	Complete example + GF25519 outline in Pipeline.v	Robert Sloan	2016-10-02
* \|	Small example of bounds-calculation with dependent types (#61)	Jason Gross	2016-09-29
* \|	montgomery-curve	Andres Erbsen	2016-09-28
* \|	Merge pull request #69 from JasonGross/scalable-scalars	Jason Gross	2016-09-26
\|\ \
* \| \|	add Montgomery x-coordinate Diffie-Hellman and Curve25519	Andres Erbsen	2016-09-26
\| \| *	Fix merge with master	Robert Sloan	2016-09-24
\| \| \|\ \| \|_\|/ \|/\| \|
\| \| *	Large-scale refactoring of src/Assembly	Robert Sloan	2016-09-24