fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add PrimitiveHList, PrimitiveProd	Jason Gross	2018-06-13
\|
*	Move Option.List.map to OptionList.map to fix name clashes in Tuple	Jason Gross	2018-06-04
\|
*	make update-_CoqProject	Jason Gross	2018-05-05
\|
*	Merge pull request #335 from mit-plv/cpsloops	Andres Erbsen	2018-04-18
\|\ \| \| \| \|	comprehensive loops framework with complete proof theory
* \|	Add new assembly-mimicking operations rshi, cc_m, and cc_l	Jade Philipoom	2018-04-11
\| \|
* \|	Update number/string conversions	Jason Gross	2018-04-09
\| \| \| \| \| \| \| \|	To updated version of https://github.com/coq/coq/pull/6597
\| *	move Loops from Experiments to Util	Andres Erbsen	2018-03-27
\| \|
\| *	remove old loops code	Andres Erbsen	2018-03-27
\|/
*	Add Algebra.SubsetoidRing	Jason Gross	2018-03-12
\|
*	make update-_CoqProject	Jason Gross	2018-03-10
\|
*	Prove another Barrett reduction variant.	David Benjamin	2018-03-09
\| \| \| \| \| \| \| \| \| \|	This variant comes from http://www.ridiculousfish.com/blog/posts/labor-of-division-episode-i.html. It was useful for https://boringssl-review.googlesource.com/#/c/boringssl/+/25887. TODO - Talk to Andres to figure out all the ways this could be done more cleanly. It was originally a standalone file.
*	Add new modular addition operation on Z	Jade Philipoom	2018-02-23
\|
*	Add pointed types	Jason Gross	2018-02-18
\| \| \| \|	For filling in default values
*	Add a file to parse taps with Coq notations	Jason Gross	2018-02-14
\|
*	Add some string utility functions	Jason Gross	2018-02-13
\|
*	Add string conversions	Jason Gross	2018-02-11
\|
*	Split off ZRange lemmas	Jason Gross	2018-02-10
\|
*	Add some ZRange operations	Jason Gross	2018-02-10
\|
*	minor updates needed to make it compile with bbv	Samuel Gruetter	2018-02-05
\| \| \| \|	removing lemma wordToNat_wzero is ok because it's already in bbv
*	add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock ↵	Samuel Gruetter	2018-02-05
\| \| \| \|	directory
*	Add x25519 donna versions with the new way of generating C code	Jason Gross	2018-01-15
\|
*	Generate fecarry for solinas	Jason Gross	2018-01-10
\| \| \| \| \| \| \|	This is a one-line change in generate_parameters.py (plus some whitespace trimming), and running `make regenerate-curves` This handles part of #294
*	Factor out fsatz lemmas	Jason Gross	2018-01-09
\| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change \| % Change ------------------------------------------------------------------------- 1m11.42s \| Total \| 1m53.75s \|\| -0m42.33s \| -37.21% ------------------------------------------------------------------------- 1m06.02s \| Curves/Weierstrass/Jacobian \| 1m53.76s \|\| -0m47.73s \| -41.96% 0m05.40s \| Util/FsatzAutoLemmas \| N/A \|\| +0m05.40s \| ∞
*	@davidben merged Jacobian+affine into Jacobian+Jacobian	Andres Erbsen	2018-01-09
\|
*	Jacobian coordinates	Andres Erbsen	2018-01-09
\|
*	Add Tactics.RunTacticAsConstr	Jason Gross	2017-11-26
\|
*	Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.v	Jason Gross	2017-11-24
\| \| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/pull/271#discussion_r152720545
*	Make a copy of Demo.v	Jason Gross	2017-11-24
\|
*	Add ModInv autosolver	Jason Gross	2017-11-16
\|
*	Update GeneralizeVar to ensure Wf	Jason Gross	2017-11-13
\| \| \| \| \|	This will hopefully pave the way for not needing to prove Wf anywhere in the bounds pipeline.
*	Make pipeline options more easily extensible	Jason Gross	2017-11-13
\| \| \| \| \|	Also add a dummy option about renaming binders, to be used in an upcoming commit.
*	Add faster version of intros [a b] for reflective stuff	Jason Gross	2017-11-13
\|
*	Add autosolve admit package	Jason Gross	2017-11-12
\|
*	automatic modifications to _Coqproject with new files	jadep	2017-11-12
\|
*	Add Decidable2Bool	Jason Gross	2017-11-11
\|
*	Add ListUtil.Forall	Jason Gross	2017-11-11
\|
*	More modularity in autosolve	Jason Gross	2017-11-10
\|
*	Add HeadUnderBinders	Jason Gross	2017-11-07
\|
*	A bit more reorganization of autosolve	Jason Gross	2017-11-07
\| \| \| \|	This lets other files import evar_package without having to be rebuilt every time a new package alias is added to Autosolve
*	Move SideConditionFramework	Jason Gross	2017-11-07
\|
*	Add SideConditionFramework	Jason Gross	2017-11-07
\|
*	Add type of bounded Z	Jason Gross	2017-11-02
\|
*	make update-_CoqProject	Jason Gross	2017-11-02
\|
*	Add MapBaseType	Jason Gross	2017-10-31
\|
*	Add unextend_op	Jason Gross	2017-10-31
\|
*	make update-_CoqProject	Jason Gross	2017-10-29
\|
*	Add MapBaseTypeWf, generalize src/Compilers/MapBaseType.v a bit	Jason Gross	2017-10-24
\|
*	Add MapBaseType	Jason Gross	2017-10-23
\|
*	Add InlineConstAndOpByRewrite	Jason Gross	2017-10-23
\|
*	Add ZExtended/InlineConstAndOp.v	Jason Gross	2017-10-22
\|