fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	montgomery-curve	Andres Erbsen	2016-09-28
\|
*	Merge pull request #69 from JasonGross/scalable-scalars	Jason Gross	2016-09-26
\|\ \| \| \| \|	Scalable Scalars, Dead Code Removal, Register Assignment
\| *	Add a comment with an example	Jason Gross	2016-09-26
\| \|
* \|	MxDH: do not depend on implicit import of list notations	Andres Erbsen	2016-09-26
\| \|
* \|	add Montgomery x-coordinate Diffie-Hellman and Curve25519	Andres Erbsen	2016-09-26
\| \|
* \|	Finished remaining admits in [freeze] proofs	jadep	2016-09-23
\| \|
\| *	Drop CSE from Fancy Machine	Jason Gross	2016-09-22
\| \| \| \| \| \| \| \| \| \|	By being careful about building the expressions in the first place, we no longer need it, and can rely on dead code elimination.
\| *	Use dlet, not llet	Jason Gross	2016-09-22
\| \|
\| *	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 "Update _CoqProject"	Jason Gross	2016-09-22
\| \| \| \|	This reverts commit 1628cb14799db7af9eb13e49ae89f50d8f527301.
*	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.
*	Update _CoqProject	Jason Gross	2016-09-22
\|
*	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
*	Allow passing PROFILE=1 to make for -profile-ltac	Jason Gross	2016-09-20
\|
*	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
\|
*	Update .gitignore for Coq 8.6	Jason Gross	2016-09-16
\|
*	Update .gitignore for Coq 8.6	Jason Gross	2016-09-16
\|
*	Add λn reserved notation	Jason Gross	2016-09-16
\|
*	Fix for Coq 8.5	Jason Gross	2016-09-16
\|