aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystemListProofs.v
Commit message (Expand)AuthorAge
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
* Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
* Created separate definitions for cmovne and cmovl for reificationGravatar jadep2016-10-23
* Modified [freeze] to be more reifyableGravatar jadep2016-10-22
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
* Finished remaining admits in [freeze] proofsGravatar jadep2016-09-23
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
* Proved specification of constant-time modulus comparison (except for one ZUti...Gravatar jadep2016-09-21
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
* Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...Gravatar jadep2016-09-06
* Instantiated conversion both to (pack) and from (unpack) another set of limb ...Gravatar jadep2016-08-16
* Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...Gravatar jadep2016-07-25
* mergeGravatar jadep2016-07-20
* restructured ModularBaseSystem pipeline to put tuple conversion before Modula...Gravatar jadep2016-07-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 16:10:05 +0000