fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Update redc algorithm	Jason Gross	2017-06-10
\| \| \| \| \| \| \|	Transcribe https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-301334813 Not sure if it's right, but now I'll try proofs.
*	Update word-by-word montgomery with ctx vars	Jason Gross	2017-06-10
\| \| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307212425
*	Finish proving loop invariant for wbw redc	Jason Gross	2017-06-09
\|
*	Make it clear that the combined definition/proof file is a work in progress	Jason Gross	2017-06-09
\|
*	Admit-free proof of cS3_mod_N	Jason Gross	2017-06-09
\| \| \| \| \| \|	Fix the algorithm to not talk about join, based on http://colinandmargaret.co.uk/Research/CDW_ELL_99.pdf (p2) and discussions over Signal with @andres-erbsen.
*	Fix open sections error	Jason Gross	2017-06-09
\|
*	More WIP on bounds for redc	Jason Gross	2017-06-09
\|
*	Minor progress on bounds	Jason Gross	2017-06-09
\|
*	Add pair-programmed wbw montgomery	Jason Gross	2017-06-09
\| \| \| \|	Partial progress with @andres-erbsen
*	Clean up implementation	Jason Gross	2017-05-01
\| \| \| \|	With help from Andres
*	Use columns rather than positional	Jason Gross	2017-05-01
\| \| \| \|	With help from Jade.
*	Use mod (weight (S i) / weight i), not mod (weight i)	Jason Gross	2017-05-01
\|
*	Initial stab at word-by-word montgomery	Jason Gross	2017-05-01
\| \| \| \| \| \| \| \| \| \| \| \|	I think I got the loop itself wrong, though: 1. I'm worried that it'll overflow off the end of the positional representation, since I'm not actually dividing by 2^s 2. I'm not carrying/reducing anywhere, so the getting the nth value might be wrong 3. I'm not sure if I got indexing right. But I want to submit this early version to get comments, before I put more effort into it.
*	rename-everything	Andres Erbsen	2017-04-06