aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF1305.v
Commit message (Expand)AuthorAge
* Make [freeze] proofs consider machine integer width and hard input bounds sep...Gravatar jadep2016-11-03
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
* Added square roots to GF1305, started reworking freeze_opt in preparation for...Gravatar jadep2016-08-31
* Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem...Gravatar jadep2016-08-24
* Added optimized [inv] operation to Specific, and removed dependencies on Modu...Gravatar jadep2016-08-24
* Shifted around some of the proofs in ModularBaseSystemField.v and propagated ...Gravatar jadep2016-08-23
* Updated GF files to reflect change in [repeat]Gravatar jadep2016-08-16
* Added specific versions of [pack] and [unpack] to GF1305.vGravatar jadep2016-08-16
* Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci...Gravatar jadep2016-08-09
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Removed lingering print statement.Gravatar jadep2016-07-21
* re-introduced extra field isomorphism layer for 8.4 compatibility and better ...Gravatar jadep2016-07-21
* restructured ModularBaseSystem pipeline to put tuple conversion before Modula...Gravatar jadep2016-07-20
* Fixed unsimplified multiplication definitions in Specific by separating out t...Gravatar jadep2016-07-18
* more changes to Specific for 8.4 compatibilityGravatar jadep2016-07-15
* re-cleaned operations in Specific and updated GF25519 to match GF1305Gravatar jadep2016-07-12
* cleaned Specific operations so they produce code without proof terms, and pro...Gravatar jadep2016-07-12
* pushing through a tweak to the arguments of [sub], and defining a field over ...Gravatar jadep2016-07-12
* ported Specific files to use ModularBaseSystemInterfaceGravatar jadep2016-07-11
* defined some group operations, stated group lemma for tuple-based [add] (in t...Gravatar jadep2016-07-08
* stuck trying to figure out dependently typed continuation passing styleGravatar Andres Erbsen2016-07-06
* Canonicalization is now automated in GF25519 and added to GF1305.Gravatar jadep2016-06-17
* PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...Gravatar jadep2016-06-15
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...Gravatar jadep2016-05-09
* added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...Gravatar jadep2016-04-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 03:43:17 +0000