fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Add Z.lt_le_incl to zarith	Jason Gross	2016-07-20
\|
*	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\|
*	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
*	merge	jadep	2016-07-10
\|\
\| *	Add Z.div_0_l to ZUtil	Jason Gross	2016-07-08
\| \|
* \|	Added mod case to zero_bounds	jadep	2016-07-08
\| \|
\| *	Add pow2_mod to ZUtil	Jason Gross	2016-07-07
\|/
*	Fix notations, add &	Jason Gross	2016-07-06
\|
*	Add notations for Z.shift{r,l} to ZUtil	Jason Gross	2016-07-06
\|
*	fixed indentation for new lemmas in ZUtil	jadep	2016-07-06
\|
*	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\|\
* \|	Factored out some proofs that rely only on base being powers of two, and ↵	jadep	2016-07-06
\| \| \| \| \| \| \| \|	defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
\| *	Indentation in ZUtil	Jason Gross	2016-07-02
\| \|
\| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The standard library uses Z., and Z and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
\| *	Fix for 8.4 evars	Jason Gross	2016-07-01
\| \|
\| *	Add ZUtil hints	Jason Gross	2016-07-01
\| \|
\| *	Add more hints to ZUtil	Jason Gross	2016-07-01
\| \|
\| *	Add more hints in ZUtil	Jason Gross	2016-07-01
\| \|
\| *	Add more ZUtil hints	Jason Gross	2016-07-01
\| \|
\| *	Add more hints to ZUtil	Jason Gross	2016-07-01
\| \|
\| *	Add hint databases and a proof about Z.log2	Jason Gross	2016-07-01
\| \|
\| *	Add some proofs about Z.div and Z.mul	Jason Gross	2016-07-01
\| \|
\| *	Fix a typo in Zsplit_sums	Jason Gross	2016-07-01
\| \|
\| *	Add tactic to split sums and differences in inequalities	Jason Gross	2016-07-01
\| \|
\| *	Add fraction inequality reasoning tactics to ZUtil	Jason Gross	2016-07-01
\| \|
\| *	Add a proof of 2 * x - x = x	Jason Gross	2016-06-30
\| \|
\| *	Add a classification of n / m < 0	Jason Gross	2016-06-30
\| \|
\| *	Add a tactic for making use of destructed <? in Z	Jason Gross	2016-06-30
\| \|
* \|	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
\| \|
\| *	Add pow_Zpow to Util.ZUtil	Jason Gross	2016-06-30
\|/ \| \| \|	I followed the naming scheme of things like div_Zdiv in the stdlib.
*	Merge	jadep	2016-06-14
\|\
* \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
\| \|
\| *	Fix for Coq 8.4pl2	Jason Gross	2016-06-11
\| \|
\| *	8.5 fixes	Jason Gross	2016-06-10
\|/
*	First stage of canonicalization proofs complete; proved 3 carry loops reduce ↵	jadep	2016-05-20
\| \| \| \|	input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	moved lemmas from ModularBaseSystemProofs to various Util files	jadep	2016-04-20
\|
*	Added lemmas to Util/ that are needed for testbit.	jadep	2016-04-19
\|
*	Finish absolutizing imports	Jason Gross	2016-03-10
\| \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-02-25
\| \| \| \|	Also move a definition about words, with a TODO about location, into WordUtil.
*	a few lemmas in util about powers of 2 in Bedrock's various rewritten forms	Jade Philipoom	2016-02-15
\|
*	tweaks to util files, including automation for proving ↵	Jade Philipoom	2016-02-15
\| \| \| \|	positivity/nonnegativity in Z
*	NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.	Jade Philipoom	2016-01-23
\|
*	Util: added util lemmas needed to instantiate EdDSA25519.	Jade Philipoom	2016-01-05
\|
*	reorganized lemmas; moved several to ListUtil and ZUtil.	Jade Philipoom	2015-11-24