fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Minor refactoring	Jason Gross	2018-06-13
\| \| \| \|	Note that List.repeat (ListUtil.List.repeat) rather than repeat (Coq.Lists.List.repeat) was interfering with extraction
*	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
\|
*	Add Option.List.map	Jason Gross	2018-06-04
\|
*	Move cps notations into a scope	Jason Gross	2018-06-01
\|
*	Add more bind reserved notations	Jason Gross	2018-05-31
\|
*	fix over-indented line	Jade Philipoom	2018-05-31
\|
*	prove prefancy->fancy for barrett special case	Jade Philipoom	2018-05-31
\|
*	move around some Lets so that 8.8 doesn't error	Jade Philipoom	2018-05-31
\|
*	relocate ok_expr tactics and fix an admit with a silly bounds relaxation hack	Jade Philipoom	2018-05-31
\|
*	Proved pre-fancy barrett reduction correct (except 1 admit for bounds	Jade Philipoom	2018-05-31
\| \| \| \| \|	that are correct but for which bounds relaxation loses necessary information) and add explanatory comments.
*	temporary workaround for #352	Jade Philipoom	2018-05-31
\|
*	Define machine model, write prefancy->fancy pass, and prove Montgomery code ↵	Jade Philipoom	2018-05-31
\| \| \| \|	correct
*	[WIP] shifting adds	Jade Philipoom	2018-05-31
\|
*	change order of additions so that they a) make more sense and b) are more ↵	Jade Philipoom	2018-05-31
\| \| \| \|	suited to shifting adds
*	tweak binders so that shifts from base conversion get inlined	Jade Philipoom	2018-05-31
\|
*	remove unneeded comment and extra whitespace	Jade Philipoom	2018-05-31
\|
*	end-to-end proof for montgomery	Jade Philipoom	2018-05-31
\|
*	Proofs for pre-fancy pass (could use cleanup)	Jade Philipoom	2018-05-31
\|
*	proofs for straightline pass (with admits for some depth stuff that should ↵	Jade Philipoom	2018-05-31
\| \| \| \|	be unneeded soon)
*	Move function argument out of fixpoint of List.map2	Jason Gross	2018-05-21
\| \| \| \| \|	This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now.
*	Compatibility after Coq PR#262.	Hugo Herbelin	2018-05-14
\| \| \| \| \| \| \| \| \|	Coq PR#262 makes the inference of return clauses more uniform and general but unification is sometimes not strong enough to deal with this generality. See #5107 for details. One reduces the search space for a return clause by forbidding it to be obtained by small inversion.
*	finish pushing through changes to dummy and factor out identifier match	Jade Philipoom	2018-05-07
\|
*	replace dummy_var with dummy_arrow and change style of straightline tests to ↵	Jade Philipoom	2018-05-07
\| \| \| \|	be more robust
*	clean up shared notations and constant-rewriting logic for prefancy	Jade Philipoom	2018-05-07
\|
*	prefancy now works on barrett (modulo add-opp=>sub)	Jade Philipoom	2018-05-07
\|
*	Move straightline and prefancy stuff above barrett reduction	Jade Philipoom	2018-05-07
\|
*	Translating to 'pre-fancy' form now works on Montgomery	Jade Philipoom	2018-05-07
\|
*	move depth to a more sensible location	Jade Philipoom	2018-05-07
\|
*	Translation to straightline code now works correctly on montgomery256	Jade Philipoom	2018-05-07
\|
*	Translation to straightline code (first attempts, mostly working)	Jade Philipoom	2018-05-07
\|
*	fix the placement of a dlet to make more sense	Jade Philipoom	2018-05-07
\|
*	Backtrack on moving a notation to Notations.v, to fix conflict	Jason Gross	2018-05-06
\|
*	Fix notations to not conflict with bbv	Jason Gross	2018-05-06
\|
*	More reserved notations	Jason Gross	2018-05-06
\|
*	Add another notation	Jason Gross	2018-05-06
\|
*	Fix a typo in last commit	Jason Gross	2018-05-06
\|
*	Add a reserved notation for #v	Jason Gross	2018-05-06
\|
*	Don't use vm_compute with existentials	Jason Gross	2018-05-05
\|
*	Update comment	Jason Gross	2018-05-05
\|
*	Fully finish flat_map	Jason Gross	2018-05-05
\|
*	Fix flat_map	Jason Gross	2018-05-05
\|
*	WIP on lists as cons cells	Jason Gross	2018-05-05
\|
*	Remove vinterp_arrow function	Jason Gross	2018-05-05
\|
*	Revert "WIP on inductive base_value"	Jason Gross	2018-05-05
\| \| \| \|	This reverts commit e38faaac1d3996c61d396144e20b8bb41809a253.
*	WIP on inductive base_value	Jason Gross	2018-05-05
\|
*	Revert "WIP with andres, not working pattern language"	Jason Gross	2018-05-05
\| \| \| \|	This reverts commit 2fcf4cd6aabebb3b68cc0a807e5d7c78e9142cb5.
*	WIP with andres, not working pattern language	Jason Gross	2018-05-05
\|
*	Add comment about leaky abstraction	Jason Gross	2018-05-05
\|
*	Split off specialization to base types from specialization to idents	Jason Gross	2018-05-05
\|