aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Expand)AuthorAge
* Fix out of memory error for 8.5,8.5pl1Gravatar Jason Gross2016-10-19
* Fix for Coq 8.4 evar propogationGravatar Jason Gross2016-10-18
* Fix missing importsGravatar Jason Gross2016-10-17
* Remove broken importsGravatar Jason Gross2016-10-17
* Rename and clean up exponent codeGravatar Jason Gross2016-10-17
* Remove admits with the help of AndresGravatar Jason Gross2016-10-17
* Fill in more proofsGravatar Jason Gross2016-10-17
* Initial work on exponent field as ZGravatar Jason Gross2016-10-17
* Clean up ge_modulus definition in SpecificGravatar jadep2016-10-12
* Added top-level modulus comparison operation so field-element decoding can re...Gravatar jadep2016-10-12
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
* Add bitwise and, remove mkl from fancyGravatar Jason Gross2016-10-03
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-10-03
* Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
* Use dlet, not lletGravatar Jason Gross2016-09-22
* Don't inline everything in Montgomery and BarrettGravatar Jason Gross2016-09-22
* Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Move FancyMachine from Experiments to SpecificGravatar Jason Gross2016-09-08
* make 8.4 happierGravatar jadep2016-09-06
* Finished sqrt in GF25519Gravatar jadep2016-09-06
* Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...Gravatar jadep2016-09-06
* updated GF25519 to match new exponentiation chain codeGravatar jadep2016-08-31
* 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
* Speed up src/Specific/GF25519.v (#54)Gravatar Jason Gross2016-08-18
* 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
* Merge of conversion development branch with masterGravatar jadep2016-08-16
|\
| * Added specific versions of [pack] and [unpack] to GF25519Gravatar 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
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
* remove obsolete rep mechanismGravatar Andres Erbsen2016-06-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:39:36 +0000