aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystem.v
Commit message (Expand)AuthorAge
* Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...Gravatar jadep2016-07-25
* restructured ModularBaseSystem pipeline to put tuple conversion before Modula...Gravatar jadep2016-07-20
* Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.Gravatar jadep2016-07-19
* Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
* pushing through a tweak to the arguments of [sub], and defining a field over ...Gravatar jadep2016-07-12
* Make [base] and [log_cap] notationsGravatar Jason Gross2016-07-11
* Factored out some proofs that rely only on base being powers of two, and defi...Gravatar jadep2016-07-06
* encode operation in ModularBaseSystem now uses bitwise operators, taking adva...Gravatar jadep2016-06-29
* BaseSystem encode function is no longer naive; it does a mod/div loop rather ...Gravatar jadep2016-06-28
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...Gravatar jadep2016-06-15
* changed representation definition to require digits vector to be the exact le...Gravatar jadep2016-06-15
* Added canonicalization to ModularBaseSystemOpt.Gravatar jadep2016-06-15
* reversed modulus_digits and proved a few admitsGravatar jadep2016-06-13
* starting rewrite using different definition of mapGravatar jadep2016-06-11
* First stage of canonicalization proofs complete; proved 3 carry loops reduce ...Gravatar jadep2016-05-20
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...Gravatar jadep2016-05-09
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
|\
* | made BaseVector instance globalGravatar Jade Philipoom2016-03-20
* | refactor of Basesystem and ModularBaseSystem; includes general code organizat...Gravatar Jade Philipoom2016-03-20
* | Refactored BaseSystem and ModularBaseSystem.Gravatar Jade Philipoom2016-03-11
| * Finish absolutizing importsGravatar Jason Gross2016-03-10
|/
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15