fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	PointFormats: extended coordinates equivalence proofs	Andres Erbsen	2016-01-16
\|
*	fix merge conflicts + PointFormats proofs	Robert Sloan	2016-01-14
\|\
* \|	assumption lemmas in PointFormats	Rob Sloan	2016-01-11
\| \|
* \|	simple refactor of makefile; comments	varomodt	2016-01-09
\| \|
\| *	cleanup	Andres Erbsen	2016-01-08
\|/
*	PointFormats: factor out admits	Andres Erbsen	2016-01-08
\|
*	PointFormats: no zero denominators in Edwards addition	Andres Erbsen	2016-01-08
\|
*	PointFormats: addition produces points on curve	Andres Erbsen	2016-01-07
\|
*	Start writing PointFormats field proofs	Andres Erbsen	2016-01-07
\|
*	PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of ↵	Jade Philipoom	2016-01-05
\| \| \| \|	phrasing in EdDSA to make proofs more convenient.
*	PointFormats : removed reliance on Pos.size_nat; doubleAndAdd now takes an ↵	Jade Philipoom	2015-12-28
\| \| \| \|	argument that serves as an upper bound on bit length.
*	PointFormats : changed iter_op to allow overestimating bitlength of argument.	Jade Philipoom	2015-12-26
\|
*	Removed OpWithZero typeclass in favor of explicit arguments.	Jade Philipoom	2015-12-25
\|
*	PointFormats: completed remaining admits for non-destruction doubleAndAdd.	Jade Philipoom	2015-12-24
\|
*	PointFormats: implemented doubleAndAdd without destructing scalar and proved ↵	Jade Philipoom	2015-12-24
\| \| \| \|	equivalence with scalarMult; several small admits remain.
*	PointFormats: wrote and proved equivalent a double-and-add implementation of ↵	Jade Philipoom	2015-12-20
\| \| \| \|	scalar-point multiplication; standardized EdDSA to use nat instead of Z.
*	PointFormats: all Edwards25519 points are onCurve	Andres Erbsen	2015-12-15
\|
*	EdDSA: mostly-complete spec and preliminary structure.	Jade Philipoom	2015-12-12
\|
*	More improved structure for EdDSA and PointFormats.	Jade Philipoom	2015-12-10
\|
*	More refacoring PointFormats.	Jade Philipoom	2015-12-09
\|
*	Rewrote PointFormats to be parameterized by modulus; reformatting of EdDSA.	Jade Philipoom	2015-12-09
\|
*	scalar multiplication	Andres Erbsen	2015-11-25
\|
*	remove resolved todo	Andres Erbsen	2015-10-28
\|
*	Tiny module-system tweaks in PointFormats	Adam Chlipala	2015-10-28
\|
*	fix the makefile to not rebuild + module renaming	Robert Sloan	2015-10-22
\|\
* \|	fix the makefile to not rebuild + module renaming	Robert Sloan	2015-10-22
\| \|
\| *	disable Curve25519 until PointFormats is parametric or we give up and retry	Andres Erbsen	2015-10-22
\| \|
\| *	refactor pointformats to use have a module type of correct implementations	Andres Erbsen	2015-10-22
\|/
*	pull changes from desktop	Robert Sloan	2015-10-19
\|
*	pull changes from desktop	Robert Sloan	2015-10-19
\|
*	Small PointFormats tweaks while reading through	Adam Chlipala	2015-10-12
\|
*	comment out edwards<->montgomery conversion	Andres Erbsen	2015-10-08
\|
*	refactor point formats to use modules and prove some lemmas	Andres Erbsen	2015-10-07
\|
*	in case of not-on-curve points, extended coordinate addition and twisted ↵	Andres Erbsen	2015-09-21
\| \| \| \|	coordinate addition may have different behavior
*	montgomery ladder definition	Andres Erbsen	2015-09-21
\|
*	make ring decidable + define constants	Robert Sloan	2015-09-19
\|
*	Curves: elliptic curve point format record declarations and some invariants	Andres Erbsen	2015-09-18
\|
*	fix module structure + add assembly placeholder	Robert Sloan	2015-09-17
\|
*	redo module structure + init curve25519	Robert Sloan	2015-09-16
\|
*	init our centralized repo	Robert Sloan	2015-09-10