fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix for Coq < 8.6	Jason Gross	2016-09-22
\|
*	Don't inline everything in Montgomery and Barrett	Jason Gross	2016-09-22
\| \| \| \| \| \|	We still use CSE in fancy machine, because we want to lift the ldi's above the rest of the code. However, on a quick inspection, the algorithm no longer needs CSE to be duplicate-free.
*	Make use of named syntax, do reg assign for fancy	Jason Gross	2016-09-22
\|
*	Add dead code elimination	Jason Gross	2016-09-22
\|
*	Add a non-higher-order syntax, and reg assignment	Jason Gross	2016-09-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The register assigner will return [None] if you give it an invalid assignment (too short, attempting to eliminate live code, attempting to merge registers that can't be merged). No correctness proofs yet, nor any sort of automatic register assignment. I'm planning to write a dead-code-eliminator register assigner next. It should also be moderately straight-forward to write a default register allocator, or perhaps a register post-allocator, that takes a manual register allocation, and renumbers variables in a greedy way. (This would let you pre-specify that some registers should be merged, but leave the rest of the assignment up to the algorithm.)
*	Revert "Add a locked version of [let] with fewer reductions"	Jason Gross	2016-09-22
\| \| \| \| \| \|	This reverts commit a4565d0c0c506a56a0db0ca09e9ac7af8b8eaee2. It's not needed.
*	Revert "Fix LockedLet"	Jason Gross	2016-09-22
\| \| \| \|	This reverts commit e9fb194f228321f9477a26bf18617047722fd42a.
*	Fix a typo	Jason Gross	2016-09-22
\|
*	Add a form of Let_In that carries a proof	Jason Gross	2016-09-22
\|
*	move eddsa rep change	Andres Erbsen	2016-09-22
\|
*	alternative signing derivation	Andres Erbsen	2016-09-22
\| \| \| \|	cleanup
*	Util.LetIn: fix proper instance	Andres Erbsen	2016-09-22
\|
*	Fix LockedLet	Jason Gross	2016-09-22
\| \| \| \| \|	We want beta-iota-delta to leave behind a zeta-redex (a let-in), even when unfolding locked_let.
*	Add a locked version of [let] with fewer reductions	Jason Gross	2016-09-22
\|
*	Generalize count_lets	Jason Gross	2016-09-21
\|
*	Deduplicate code	Jason Gross	2016-09-21
\|
*	Add some util files for reflective let bindings	Jason Gross	2016-09-21
\|
*	Reorganization, moving of lemmas to correct files, and 8.4 compatibility	jadep	2016-09-21
\|
*	Proved specification of constant-time modulus comparison (except for one ↵	jadep	2016-09-21
\| \| \| \|	ZUtil lemma)
*	Generalize InlineConst	Jason Gross	2016-09-20
\| \| \| \|	Now it can inline expressions as well as constants and variables
*	Change [Let ... in ...] to [dlet ... in ...] (#67)	Jason Gross	2016-09-19
\| \| \| \|	For "definition". This fixes #65; [Let] conflicts with the vernacular [Let] in Coq 8.4.
*	Make the example a function for reification	Jason Gross	2016-09-18
\|
*	Add dec eq for option, list	Jason Gross	2016-09-18
\|
*	Better arguments for SmartVarMap	Jason Gross	2016-09-18
\|
*	Arguments for SmartVarMap	Jason Gross	2016-09-18
\|
*	Generalize SmartVarVar	Jason Gross	2016-09-18
\|
*	Fix the 8.4 build by changing a couple standard library names	jadep	2016-09-18
\|
*	Util.Notations: change Let to match slet\	Andres Erbsen	2016-09-18
\|
*	Add reserved notation for Let, change #	Jason Gross	2016-09-17
\| \| \| \| \|	We reserve [a # b] in Notations.v, and make it's level compatible with the notation declared in the std lib for Q.
*	Move side lemmas to appropriate files	jadep	2016-09-17
\|
*	Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over ↵	jadep	2016-09-17
\| \| \| \|	implementations of [mul] and [pow] so bounds can be threaded through
*	Proved bounds for [encode] results; fleshed out some structure for [freeze] ↵	jadep	2016-09-17
\| \| \| \|	proofs; bundled [freeze] preconditions.
*	Fix missing parenthesis	jadep	2016-09-17
\|
*	Remove unused lemma and standardized use of notations for [freeze] proofs	jadep	2016-09-17
\|
*	deduplicate Let_In into src/Util/LetIn.v	Andres Erbsen	2016-09-17
\|
*	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
\|