fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add ring_simplify_subterms	Jason Gross	2016-07-22
\|
*	Generalize div_sub_small a bit	Jason Gross	2016-07-22
\|
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-21
\|\
* \|	Fix 8.4{pl1,pl2} builds	jadep	2016-07-21
\| \|
\| *	Add another lemma to zarith	Jason Gross	2016-07-21
\| \|
* \|	Changed name of [carry_and_reduce_single] to [carry_single], since it does ↵	jadep	2016-07-21
\| \| \| \| \| \| \| \|	not perform reduction
\| *	Split up proof in BarrettReduction.Z	Jason Gross	2016-07-21
\| \| \| \| \| \| \| \| \| \| \| \|	In particular, we do equality reasoning in one place and inequality reasoning in another. This makes it very clear how the inequality reasoning follows from the equality reasoning.
\| *	Add another ZUtil lemma	Jason Gross	2016-07-21
\| \|
\| *	Another ZUtil lemma	Jason Gross	2016-07-21
\| \|
\| *	Fix broken proofs	Jason Gross	2016-07-21
\| \|
\| *	Add more ZUtil	Jason Gross	2016-07-21
\| \|
\| *	More ZUtil helper lemmas	Jason Gross	2016-07-21
\| \|
\| *	Add more ZUtil lemmas	Jason Gross	2016-07-21
\| \| \| \| \| \| \| \|	We really want rewrite mod AC here...
\| *	Update .mailmap	Jason Gross	2016-07-21
\| \|
\| *	Add ZUtil lemmas	Jason Gross	2016-07-21
\|/
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-21
\|\
* \|	Removed lingering print statement.	jadep	2016-07-21
\| \|
\| *	Faster update-_CoqProject target	Jason Gross	2016-07-21
\| \|
\| *	Fix clean target	Jason Gross	2016-07-21
\| \| \| \| \| \| \| \|	This is the problem with copy-paste solutions. (Thanks @jadephilipoom)
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-21
\|\\|
* \|	Fixes #29	jadep	2016-07-21
\| \|
* \|	re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵	jadep	2016-07-21
\| \| \| \| \| \| \| \|	organization of reasoning.
\| *	ed25519 spec: small cleanup	Andres Erbsen	2016-07-21
\| \|
\| *	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!
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-20
\|\\|
* \|	merge	jadep	2016-07-20
\|\ \
\| \| *	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
* \|	restructured ModularBaseSystem pipeline to put tuple conversion before ↵	jadep	2016-07-20
\| \| \| \| \| \| \| \|	ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
\| *	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
\| \|