fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add [freeze] to Arithmetic	Jason Gross	2018-06-21
\|
*	Add extend_to_length for non-uniform-length add, sub	Jason Gross	2018-06-19
\|
*	Add a comment about sub	Jason Gross	2018-06-18
\|
*	More compact printing of ASTs in errors	Jason Gross	2018-06-18
\|
*	Add another prime example	Jason Gross	2018-06-18
\|
*	Fix a typo in to-C shifts	Jason Gross	2018-06-18
\|
*	Don't duplicate error message printing in OCaml	Jason Gross	2018-06-18
\|
*	Pass around lists of strings for error messages	Jason Gross	2018-06-17
\| \| \| \| \| \| \| \| \| \|	This allows us to get back an error message in Saturated Solinas in OCaml on P256 x32 in reasonable time without blowing the stack. There's the slight oddity that the list of string in the success case is joined by the empty string, but the list of string in the error case is joined by newline. Probably meanas that I chose the wrong abstraction barrier somewhere.
*	New pipeline, split among files	Jason Gross	2018-06-17
\|
*	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
*	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)
*	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
\|
*	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
\|
*	Add type variables / substitutions	Jason Gross	2018-05-05
\| \| \| \|	This allows more genericness in the ident-specific code
*	Change some notations for more readability by Andres	Jason Gross	2018-05-05
\|