fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix a proof	Jason Gross	2018-04-18
\|
*	Change a proof in src/Util/Option	Jason Gross	2018-04-18
\| \| \| \| \| \|	This was causing issues with bug minimization because some hints seem to follow [Require], not [Import], and so when [eauto] got stronger, this proof was failing.
*	Merge pull request #335 from mit-plv/cpsloops	Andres Erbsen	2018-04-18
\|\ \| \| \| \|	comprehensive loops framework with complete proof theory
* \|	Actually display the error messages from pipeline failures	Jason Gross	2018-04-18
\| \| \| \| \| \| \| \| \| \|	See https://github.com/coq/coq/issues/7291 and https://github.com/mit-plv/fiat-crypto/issues/349#issuecomment-382180578
* \|	Add a Z.cast2 case to bounds extraction	Jason Gross	2018-04-18
\| \|
* \|	Also include the syntax tree in bounds analysis errors	Jason Gross	2018-04-18
\| \| \| \| \| \| \| \|	This should fix #349 (or at least most of it).
* \|	move requires to top of file	Jade Philipoom	2018-04-11
\| \|
* \|	barrett reduction definition and proof	Jade Philipoom	2018-04-11
\| \|
* \|	add a list lemma	Jade Philipoom	2018-04-11
\| \|
* \|	add some lemmas aboud div and mod	Jade Philipoom	2018-04-11
\| \|
* \|	Add new assembly-mimicking operations rshi, cc_m, and cc_l	Jade Philipoom	2018-04-11
\| \|
* \|	fix trashed carry flag	Jade Philipoom	2018-04-11
\| \|
* \|	remove comment	Jade Philipoom	2018-04-11
\| \|
* \|	add a comment to rerun build	Jade Philipoom	2018-04-11
\| \|
* \|	Automate some proofs a bit more	Jason Gross	2018-04-11
\| \|
* \|	try to fix build on coq master	Jade Philipoom	2018-04-11
\| \|
* \|	prove stronger bound on quotient error for barrett reduction	Jade Philipoom	2018-04-11
\| \|
* \|	Update number/string conversions	Jason Gross	2018-04-09
\| \| \| \| \| \| \| \|	To updated version of https://github.com/coq/coq/pull/6597
* \|	package properties of weight functions into a record	Jade Philipoom	2018-04-09
\| \|
* \|	relocate and prove an admit	Jade Philipoom	2018-04-09
\| \|
* \|	reorganization: move more things into BaseConversion	Jade Philipoom	2018-04-09
\| \|
* \|	better factoring-out of mul_converted stuff, define saturated arith operations	Jade Philipoom	2018-04-06
\| \|
* \|	Use a simpler form of Uncurrying	Jason Gross	2018-04-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After in-person discussion with Andres, we decided that, because the previous form of uncurrying was only half-uncurried (not including identifiers nor lambdas passed to other lambdas), and the strongest driver of a full uncurrying pass would be having an easier-to-visualize intermediate representation / knowing more clearly what the pipeline is doing, and the changes required for making this a full uncurrying pass would be global to the pipeline (require changing the type of identifiers), we would instead go back the version of uncurrying that I initially proposed, where we only uncurry the top-level function. Note that we create a slightly more complicated term (with more application nodes) than we have to; if we instead took in `@expr (@expr var) t` rather than `@expr var t`, we wouldn't introduce needless abstractions. However, the current form admits an extremely simple proof of correctness, which doesn't even require well-formedness of the expression tree.
* \|	Stick an uncurry pass in the pipeline	Jason Gross	2018-04-04
\| \| \| \| \| \| \| \| \| \|	This allows us to (a) consolidate the constant and non-constant pipelines and (b) vastly simplify the call-with-id-continuation logic.
* \|	Add Uncurry	Jason Gross	2018-04-04
\| \| \| \| \| \| \| \| \| \|	This pass uncurries all applied lambdas. Care is taken to not do beta reduction and to not introduce spurious `Abs` or `App` nodes.
* \|	pass-through after Jason's review	Jade Philipoom	2018-04-03
\| \|
* \|	pass-through after Andres's review in #334	Jade Philipoom	2018-04-03
\| \|
* \|	move requires to the top of the file	Jade Philipoom	2018-04-03
\| \|
* \|	make montgomery not depend on intermediate weight for multiplication being ↵	Jade Philipoom	2018-04-03
\| \| \| \| \| \| \| \|	the sqrt of the usual weight
* \|	rename w_half to w_mul	Jade Philipoom	2018-04-03
\| \|
* \|	make a more general kind of mul_converted_halve that produces the correct ↵	Jade Philipoom	2018-04-03
\| \| \| \| \| \| \| \|	carries even in cases where w is not necessarily the square of w', but potentially some other power
* \|	move some lemmas to ZUtil/ListUtil	Jade Philipoom	2018-04-03
\| \|
* \|	move some shared lemmas between Columns/Rows into a Saturated module	Jade Philipoom	2018-04-03
\| \|
* \|	reprint Montgomery output (order of additions in Rows.flatten changed)	Jade Philipoom	2018-04-03
\| \|
* \|	more proof automation in Rows	Jade Philipoom	2018-04-03
\| \|
* \|	automate some Rows proofs	Jade Philipoom	2018-04-03
\| \|
* \|	organize Rows into sections	Jade Philipoom	2018-04-03
\| \|
* \|	organize proofs into sections	Jade Philipoom	2018-04-03
\| \|
* \|	more cleanup of flatten proofs	Jade Philipoom	2018-04-03
\| \|
* \|	clean up some [flatten] proofs	Jade Philipoom	2018-04-03
\| \|
* \|	move some lemmas/hints to ListUtil	Jade Philipoom	2018-04-03
\| \|
* \|	fix typo and add booleans for carries	Jade Philipoom	2018-04-03
\| \|
* \|	changing Montgomery notations	Jade Philipoom	2018-04-03
\| \|
* \|	make add_with_get_carry with a constant zero for the carry translate to ↵	Jade Philipoom	2018-04-03
\| \| \| \| \| \| \| \|	add_get_carry
* \|	inline shifts for Montgomery example	Jade Philipoom	2018-04-03
\| \|
* \|	Make Montgomery example use row-wise flatten (involves adding Nat.max, ↵	Jade Philipoom	2018-04-03
\| \| \| \| \| \| \| \|	List.tl, and List.hd to the pipeline)
* \|	add Rows.from_associational and some more length proofs that allow ↵	Jade Philipoom	2018-04-03
\| \| \| \| \| \| \| \|	Rows.length_from_associational
* \|	move mul_converted to its own module	Jade Philipoom	2018-04-03
\| \|
* \|	finish flatten_partitions and slightly change the format of _partitions ↵	Jade Philipoom	2018-04-03
\| \| \| \| \| \| \| \|	lemma statements
* \|	proved admits about sum_rows	Jade Philipoom	2018-04-03
\| \|