fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
\| \| *	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
\| * \|	Make use of named syntax, do reg assign for fancy	Jason Gross	2016-09-22
\| * \|	Add dead code elimination	Jason Gross	2016-09-22
\| * \|	Add a non-higher-order syntax, and reg assignment	Jason Gross	2016-09-22
\|/ /
* \|	Revert "Update _CoqProject"	Jason Gross	2016-09-22
* \|	move eddsa rep change	Andres Erbsen	2016-09-22
* \|	Update _CoqProject	Jason Gross	2016-09-22
* \|	Add some util files for reflective let bindings	Jason Gross	2016-09-21
* \|	deduplicate Let_In into src/Util/LetIn.v	Andres Erbsen	2016-09-17
* \|	Derive EdDSA.verify from equational specification	Andres Erbsen	2016-09-16
* \|	Split off lemmas about [InlineConst]	Jason Gross	2016-09-16
* \|	Add generalized version of Wf parameterized on rel	Jason Gross	2016-09-15
* \|	Move FancyMachine from Experiments to Specific	Jason Gross	2016-09-08
* \|	Add Barrett and Montgomery for the 256-bit machine	Jason Gross	2016-09-07
* \|	Add Common Subexpression Elimination	Jason Gross	2016-09-06
* \|	Add correctness of interpretation of linearize and inline_const	Jason Gross	2016-09-05
* \|	Add LinearizeWf	Jason Gross	2016-09-05
* \|	Fix order of binders, and add WfProofs	Jason Gross	2016-09-05
* \|	Fix _CoqProject	Jason Gross	2016-09-05
* \|	Remove ReifyDirect	Jason Gross	2016-09-05
* \|	A helper lemma for [Wf]	Jason Gross	2016-09-05
* \|	PHOAS syntax	Jason Gross	2016-09-05
* \|	Add a file about pointed Props	Jason Gross	2016-09-05
* \|	Rename congrunce_option to inversion_option, add [inversion_prod]	Jason Gross	2016-08-31
* \|	Integrate suggestions from Andres	Jason Gross	2016-08-25
* \|	Rework bounded proofs	Jason Gross	2016-08-24
* \|	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\|\ \
\| * \|	Removed now-obsolete ModularBaseSystemField.v; field lemmas for ModularBaseSy...	jadep	2016-08-24
\| \| *	Type requirements for in-place AST conversion in SpecificCurve25519	Robert Sloan	2016-08-23
* \| \|	Update _CoqProject	Jason Gross	2016-08-23
* \| \|	Hook up the bounded interface, finish proofs	Jason Gross	2016-08-23
* \| \|	Initial work on an architecture interface for ℤ/nℤ	Jason Gross	2016-08-23
\|/ /
\| *	Experimental requirements for rsloan-phoas	Robert Sloan	2016-08-23
* \|	Specify a type of bounded integers for mod arith	Jason Gross	2016-08-09
\| *	PHOAS-based reflective simplification of specific code	Andres Erbsen	2016-08-08
\| *	remove dependency on hprop stuff	Andres Erbsen	2016-08-08
\|/
*	Define Montgomery reduction / multiplication on Z (#42)	Jason Gross	2016-08-05
*	Implement Barrett Reduction following HAC 14.42 (#45)	Jason Gross	2016-08-04
*	Add a generalized version of Barrett Reduction (#44)	Jason Gross	2016-08-04