fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Make [freeze] proofs consider machine integer width and hard input bounds sep...	jadep	2016-11-03
*	Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...	jadep	2016-11-02
*	Fix a missing import in previous commit	Jason Gross	2016-10-27
*	Modified [freeze] to be more reifyable	jadep	2016-10-22
*	Define carry_opp in terms of carry_sub	Jason Gross	2016-10-19
*	Add opt versions of add, sub, opp	Jason Gross	2016-10-19
*	Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl...	jadep	2016-09-17
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...	jadep	2016-09-06
*	fixed typo; extra argument	jadep	2016-08-31
*	Add runtime equality comparison and square root functions to ModularBaseSystem.	jadep	2016-08-31
*	Changed definition of [sub] to require proof that the modulus multiple actual...	jadep	2016-08-25
*	Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem...	jadep	2016-08-24
*	Defined real versions of [pow] and [inv] in ModularBaseSystem, replacing plac...	jadep	2016-08-23
*	Instantiated conversion both to (pack) and from (unpack) another set of limb ...	jadep	2016-08-16
*	Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci...	jadep	2016-08-09
*	[F] has its own module now	Andres Erbsen	2016-08-05
*	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
*	Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...	jadep	2016-07-25
*	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
*	Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.	jadep	2016-07-19
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
*	pushing through a tweak to the arguments of [sub], and defining a field over ...	jadep	2016-07-12
*	Make [base] and [log_cap] notations	Jason Gross	2016-07-11
*	Factored out some proofs that rely only on base being powers of two, and defi...	jadep	2016-07-06
*	encode operation in ModularBaseSystem now uses bitwise operators, taking adva...	jadep	2016-06-29
*	BaseSystem encode function is no longer naive; it does a mod/div loop rather ...	jadep	2016-06-28
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
*	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...	jadep	2016-06-15
*	changed representation definition to require digits vector to be the exact le...	jadep	2016-06-15
*	Added canonicalization to ModularBaseSystemOpt.	jadep	2016-06-15
*	reversed modulus_digits and proved a few admits	jadep	2016-06-13
*	starting rewrite using different definition of map	jadep	2016-06-11
*	First stage of canonicalization proofs complete; proved 3 carry loops reduce ...	jadep	2016-05-20
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...	jadep	2016-05-09
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\
* \|	made BaseVector instance global	Jade Philipoom	2016-03-20
* \|	refactor of Basesystem and ModularBaseSystem; includes general code organizat...	Jade Philipoom	2016-03-20
* \|	Refactored BaseSystem and ModularBaseSystem.	Jade Philipoom	2016-03-11
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
\|/
*	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15