fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add support for TIMED=1 in Coq 8.4	Jason Gross	2016-07-20
\| \| \| \|	This should fix #34
*	Don't depend on the submodule; copy-paste instead	Jason Gross	2016-07-20
\|
*	Add a separate non-specific target	Jason Gross	2016-07-20
\| \| \| \| \| \| \| \|	This should fix #27. We depend on some files in the etc/coq-scripts submodule. Note that you need to either run `make cleanall -k` or `rm -f Makefile.coq` after pulling this to build the development.
*	Merge pull request #33 from JasonGross/dir-locals	Andres Erbsen	2016-07-20
\|\ \| \| \| \|	Add target for .dir-locals.el
* \|	automate a proof	Andres Erbsen	2016-07-20
\| \|
* \|	compute on [F q]!	Andres Erbsen	2016-07-20
\| \|
* \|	experiments wd25519: simplify proof for a	Andres Erbsen	2016-07-20
\| \|
\| *	Add target for .dir-locals.el	Jason Gross	2016-07-20
\|/ \| \| \| \| \|	This fixes #31 Thanks @cpitclaudel!
*	Move mul_rep_extended (do we actually care about this?)	Jason Gross	2016-07-20
\|
*	Don't use auto with *	Jason Gross	2016-07-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It's fragile and slow. Now we're 45 seconds faster. After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------- 1m03.42s \| Total \| 1m49.00s \|\| -0m45.57s ------------------------------------------------------------------------------- 0m20.01s \| ModularArithmetic/ModularBaseSystemProofs \| 1m05.69s \|\| -0m45.67s 0m32.14s \| Specific/GF25519 \| 0m31.92s \|\| +0m00.21s 0m07.05s \| Specific/GF1305 \| 0m07.07s \|\| -0m00.02s 0m02.84s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.90s \|\| -0m00.06s 0m00.69s \| Experiments/SpecificCurve25519 \| 0m00.69s \|\| +0m00.00s 0m00.69s \| ModularArithmetic/ModularBaseSystemInterface \| 0m00.73s \|\| -0m00.04s
*	Absolutize some imports	Jason Gross	2016-07-20
\|
*	Silence a deprecation warning	Jason Gross	2016-07-20
\|
*	Display pretty timing graph on travis	Jason Gross	2016-07-20
\|
*	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\|
*	Add Z.lt_le_incl to zarith	Jason Gross	2016-07-20
\|
*	Add another lemma about +, <= to arith	Jason Gross	2016-07-20
\|
*	Use a proof that doesn't require as many assumptions in extended_base_length	Jason Gross	2016-07-20
\|
*	Work around bad design in Coq	Jason Gross	2016-07-19
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=4949, [intuition] should not use [auto with *] by default
*	Add a distr_length database	Jason Gross	2016-07-19
\|
*	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\|
*	{base} -> base	Jason Gross	2016-07-19
\|
*	Move two_k_nonzero to PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\| \| \| \|	It has nothing to do with ext_base
*	Fix side-condition from previous commit	Jason Gross	2016-07-19
\|
*	Add another lemma to distr_length	Jason Gross	2016-07-19
\|
*	Use update_nth in add_to_nth (#26)	Jason Gross	2016-07-19
\| \| \| \| \| \|	It leads to a slightly more transparent and clearer definition. If I got everything right, nothing should depend on the judgmental definition of [add_to_nth] anymore.
*	Bump submodule	Jason Gross	2016-07-19
\|
*	Bump submodule	Jason Gross	2016-07-19
\|
*	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
\|
*	Add a lemma about base_from_limb_widths and app	Jason Gross	2016-07-18
\|
*	Add a lemma about sum_firstn	Jason Gross	2016-07-18
\|
*	Add a ListUtil lemma	Jason Gross	2016-07-18
\|
*	Move more proofs earlier	Jason Gross	2016-07-18
\|
*	Make Pow2BaseProofs independent of the def of add_to_nth	Jason Gross	2016-07-18
\|
*	Silence a warning	Jason Gross	2016-07-18
\| \| \| \| \| \| \| \| \|	File "./src/Experiments/GenericFieldPow.v", line 130, characters 4-471: Warning: Casts are ignored in patterns [cast-in-pattern,automation] @andres-erbsen Did you intend for the cast at https://github.com/mit-plv/fiat-crypto/commit/6823b63275333ebb11c7f84068894f76cdb06068#diff-078114b2627a38e74938989c7ca2f6d1R131 to have semantic meaning for some reason, performance or otherwise?
*	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
\| \| \| \| \| \|	Also make much of the remaining code outside of Pow2BaseProofs independent of the precise definition of carry_simple. (We use [Local Opaque] to enforce this modularity.
*	Fix for Coq 8.4 (missing lemmas)	Jason Gross	2016-07-18
\|
*	Fix for Coq 8.4 (omega used to be weaker)	Jason Gross	2016-07-18
\|
*	Add more distr_length proofs in BaseSystemProofs	Jason Gross	2016-07-18
\|
*	Add more natsimplify le_dec lemmas	Jason Gross	2016-07-18
\|
*	Add more NatUtil lemmas	Jason Gross	2016-07-18
\|
*	Add natsimplify lemmas about eq_nat_dec	Jason Gross	2016-07-18
\|
*	Fix some typos in the previous commit	Jason Gross	2016-07-18
\|
*	Add some lemmas about nth_default in bounds	Jason Gross	2016-07-18
\|
*	Remove a nested proof	Jason Gross	2016-07-18
\| \| \| \| \|	Fix for Warning: Nested proofs are deprecated and will stop working in a future Coq version [deprecated-nested-proofs,deprecated]
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
\| \| \| \| \| \| \| \| \|	* Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
*	ported IterAssocOp to use monoid rather than a billion context variables ↵	jadep	2016-07-18
\| \| \| \|	that add up to a monoid
*	rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ↵	jadep	2016-07-18
\| \| \| \|	(bases that are repeats of the same power of 2) into Pow2Base
*	Added lemmas to ZUtil and NatUtil (for Testbit)	jadep	2016-07-18
\|
*	Fixed unsimplified multiplication definitions in Specific by separating out ↵	jadep	2016-07-18
\| \| \| \|	the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions.
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-15
\|\