aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystemList.v
Commit message (Expand)AuthorAge
* 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
* Proved specification of constant-time modulus comparison (except for one ZUti...Gravatar jadep2016-09-21
* 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
* [F] has its own module nowGravatar Andres Erbsen2016-08-05
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Fix 8.4 build.Gravatar jadep2016-07-25
* 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-06-01 17:25:18 +0000