fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add λn reserved notation	Jason Gross	2016-09-16
\|
*	Fix for Coq 8.5	Jason Gross	2016-09-16
\|
*	Add more prop_of_option	Jason Gross	2016-09-16
\|
*	Derive EdDSA.verify from equational specification	Andres Erbsen	2016-09-16
\| \| \| \|	Experiments/SpecEd25519 will come back soon
*	Algebra: prove an admit, add eq_r_opp_r_inv	Andres Erbsen	2016-09-16
\|
*	IterAssocOp: parameters before arguments	Andres Erbsen	2016-09-16
\|
*	ModularArithmetic: conversions between [F] and [nat]	Andres Erbsen	2016-09-16
\|
*	Generalize InlineConst	Jason Gross	2016-09-16
\| \| \| \| \|	Should now support constant subexpression evaluation (removing things like (_ + 0)).
*	Split off lemmas about [InlineConst]	Jason Gross	2016-09-16
\|
*	Equality for nat in natutil	Jason Gross	2016-09-16
\|
*	Add arguments for smartval	Jason Gross	2016-09-16
\|
*	Fix a bad line	Jason Gross	2016-09-16
\|
*	Add SmartVal	Jason Gross	2016-09-16
\|
*	Add generalized version of Wf parameterized on rel	Jason Gross	2016-09-15
\| \| \| \| \| \|	This should allow a nice elegant abstract way of doing bounds analysis. It's possible that wf should be redefined in terms of rel_wf.
*	More 8.4 compatibility	jadep	2016-09-14
\|
*	Tweaked automation for 8.4 compatibility	jadep	2016-09-14
\|
*	Automated and cleaned up [freeze] carry-loop proofs	jadep	2016-09-13
\|
*	Update old carry loop bounds proof; now is automated and also has analogous ↵	jadep	2016-09-13
\| \| \| \|	structure to subsequent carry loop proofs
*	Moved lemmas to ZUtil	jadep	2016-09-13
\|
*	Finished off last admits for proofs of bounds after 3 carry loops.	jadep	2016-09-13
\|
*	[freeze] proofs : Mostly-complete proofs of bounds after 3 carry loops	jadep	2016-09-13
\|
*	[freeze] proofs : proved bounds for second carry loop.	jadep	2016-09-13
\|
*	Merge pull request #63 from JasonGross/fancy-barrett-montgomery	Jason Gross	2016-09-08
\|\ \| \| \| \|	Add Barrett and Montgomery for the 256-bit machine
* \|	Fully qualify [Require]s	Jason Gross	2016-09-08
\| \| \| \| \| \| \| \|	This way they won't become ambiguous if we add new files
\| *	Move FancyMachine from Experiments to Specific	Jason Gross	2016-09-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Quoting Andres: > I am leaning towards putting this in Specifc instead of Experiments -- it > seems like complete result on its own, these files are unlikely to be reused > for something else, and I don't think we are expecting to need to remove it > any time soon. Currently, `Specific` code does not quantify over anything (no > context variables), but this seems secondary. We could make versions of this > with the curve constants plugged in, though.
\| *	Address code review, add come comments and cleanup	Jason Gross	2016-09-08
\| \|
\| *	Add Barrett and Montgomery for the 256-bit machine	Jason Gross	2016-09-07
\|/ \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------ 0m12.69s \| Total \| 0m00.00s \|\| +0m12.69s ------------------------------------------------------------------------ 0m06.96s \| Experiments/FancyMachineMontgomery256 \| N/A \|\| +0m06.96s 0m03.07s \| Experiments/FancyMachineBarrett256 \| N/A \|\| +0m03.06s 0m02.67s \| Experiments/FancyMachine256 \| N/A \|\| +0m02.67s
*	Fixes for Coq 8.4	Jason Gross	2016-09-07
\|
*	Remove the need for coercions in well-typing of Reify	Jason Gross	2016-09-07
\|
*	Add fastpath to reify, add coercions	Jason Gross	2016-09-07
\| \| \| \|	The lack of exported coercions broke some automation.
*	Work around bug #5073 (lia)	Jason Gross	2016-09-07
\| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5073, lia got weaker in the past few days (sometimes can't handle biconditionals)
*	Better spec in Montgomery.ZBounded	Jason Gross	2016-09-07
\|
*	Key on the head of the operation in reification	Jason Gross	2016-09-07
\| \| \| \| \| \|	Hopefully fixes #62 Also, don't export InputSyntax in Reify
*	Add Common Subexpression Elimination	Jason Gross	2016-09-06
\|
*	Fix for 8.4's type inferencer being broken	Jason Gross	2016-09-06
\|
*	Fix for changes in 8.4/8.5 behavior of [intro] w.r.t. refolding	Jason Gross	2016-09-06
\|
*	Fix for 8.6 (context (correctly) no longer defaults to type_scope)	Jason Gross	2016-09-06
\|
*	make 8.4 happier	jadep	2016-09-06
\|
*	Finished sqrt in GF25519	jadep	2016-09-06
\|
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], ↵	jadep	2016-09-06
\| \| \| \|	cleaning up freeze-related organization and definitions along the way
*	Add interp_flat_type_gen_rel_pointwise	Jason Gross	2016-09-05
\|
*	Add correctness of interpretation of linearize and inline_const	Jason Gross	2016-09-05
\|
*	Add instances for interp_type_gen_rel_pointwise	Jason Gross	2016-09-05
\|
*	Better implicits for interp_type_gen_rel_pointwise	Jason Gross	2016-09-05
\|
*	Better implicits for interpf, pointwise-lifting of rels over interp_type_gen	Jason Gross	2016-09-05
\|
*	Better implicits for interpf	Jason Gross	2016-09-05
\|
*	Better implicits for interp	Jason Gross	2016-09-05
\|
*	Better implicits for Interp	Jason Gross	2016-09-05
\|
*	Add LinearizeWf	Jason Gross	2016-09-05
\| \| \| \|	The proof of wf-preservation for inline_const isn't finished yet, though...
*	Reorder WfProofs arguments	Jason Gross	2016-09-05
\|