fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	assumption lemmas in PointFormats	Rob Sloan	2016-01-11
\|
*	simple refactor of makefile; comments	varomodt	2016-01-09
\|
*	Specific/GF25519: explicit formula for multiplication	Andres Erbsen	2015-12-05
\|
*	reorganized lemmas; moved several to ListUtil and ZUtil.	Jade Philipoom	2015-11-24
\|
*	ModularBaseSystem: added definition to perform a specific sequence of ↵	Jade Philipoom	2015-11-24
\| \| \| \|	carries and proved that it preserves GF representation.
*	ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ↵	Jade Philipoom	2015-11-20
\| \| \| \|	carry_rep.
*	Added base_succ precondition to BaseSystem to help prove carrying.	Jade Philipoom	2015-11-19
\|
*	ModularBaseSystem: proving reduce case of carry_rep.	Jade Philipoom	2015-11-18
\|
*	ModularBaseSystem: carry_rep has boring modular arithmetic proofs	Andres Erbsen	2015-11-17
\|
*	ModularBaseSystem: introduced lemmas about breaking lists; working on ↵	Jade Philipoom	2015-11-17
\| \| \| \|	carry_rep_reduce.
*	ModularBaseSystem.carry: implement, state lemmas, some progress on proofs	Andres Erbsen	2015-11-17
\|
*	ModularBaseSystem: Implemented and proved subtraction, completing ↵	Jade Philipoom	2015-11-10
\| \| \| \|	implementation of GFrep interface.
*	ModularBaseSystem: implemented fromGF and proved correct, moved inline ↵	Jade Philipoom	2015-11-10
\| \| \| \|	admits about inject to GaloisTheory.
*	BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ↵	Jade Philipoom	2015-11-10
\| \| \| \|	(first element of base is 1).
*	ModularBaseSystem: finished most admits for addition and multiplication, ↵	Jade Philipoom	2015-11-09
\| \| \| \|	moved some lemmas to ListUtil.
*	ModularBaseSystem: proved addition and multiplication.	Jade Philipoom	2015-11-07
\|
*	ModularBaseSystem: finish base_good	Andres Erbsen	2015-11-07
\|
*	ModularBaseSystem: prove some admits in mase system extension	Andres Erbsen	2015-11-07
\|
*	ModularBaseSystem: continuing to prove base_good.	Jade Philipoom	2015-11-07
\|
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2015-11-06
\|\
* \|	Starting to prove base_good in ModularBaseSystem	Jade Philipoom	2015-11-06
\| \|
\| *	Specific: PseudoMersenneBaseParams for GF25519Base25Point5.	Andres Erbsen	2015-11-06
\| \|
\| *	Merge remote-tracking branch 'jadep/master'	Andres Erbsen	2015-11-06
\|/
*	ModularBaseSystem: finished proving all admits for reduce_rep; proved ↵	Jade Philipoom	2015-11-05
\| \| \| \|	base_positive for extended base system.
*	ModularBaseSystem: Implemented reduce and proved reduce_rep, currently ↵	Jade Philipoom	2015-11-05
\| \| \| \|	working on admits (extended_shiftadd and reduce_defn).
*	ModularBaseSystem: defined an extended base system to represent unreduced ↵	Jade Philipoom	2015-11-04
\| \| \| \|	products.
*	ModularBaseSystem skeleton	Andres Erbsen	2015-10-30