aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519.v
Commit message (Expand)AuthorAge
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
* Make [freeze] proofs consider machine integer width and hard input bounds sep...Gravatar jadep2016-11-03
* Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...Gravatar jadep2016-11-02
* Add {un,}curry_wire_digitsGravatar Jason Gross2016-10-27
* Add {un,}curry_{bin,un}op_fe25519Gravatar Jason Gross2016-10-27
* Add length_fe25519Gravatar Jason Gross2016-10-27
* Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
* Created separate definitions for cmovne and cmovl for reificationGravatar jadep2016-10-23
* Finish twedprm_ERep proofGravatar Jason Gross2016-10-23
* Generalize field_from_redundant_representationGravatar Jason Gross2016-10-23
* final touches/fixes for freeze restructuringGravatar jadep2016-10-22
* add arguments that I forgotGravatar jadep2016-10-22
* Modified [freeze] to be more reifyableGravatar jadep2016-10-22
* pow, not pow_opt, in Specific/GF25519Gravatar Jason Gross2016-10-21
* Sane fieldwisebGravatar Jason Gross2016-10-21
* Make eqb sane (help from Jade)Gravatar Jason Gross2016-10-21
* Removed the lingering TODO and print statement that @JasonGross helpfully poi...Gravatar jadep2016-10-19
* Fill in admits for field with carry_add, carry_opp, and carry_subGravatar jadep2016-10-19
* Define carry_opp in terms of carry_subGravatar Jason Gross2016-10-19
* Add opt versions of add, sub, oppGravatar Jason Gross2016-10-19
* 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
* 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
* 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
* 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
* Speed up src/Specific/GF25519.v (#54)Gravatar Jason Gross2016-08-18
* Updated GF files to reflect change in [repeat]Gravatar 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
* 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
* 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
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
* remove obsolete rep mechanismGravatar Andres Erbsen2016-06-20
* GF25519: quietGravatar Andres Erbsen2016-06-20
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
|\
* | Canonicalization is now automated in GF25519 and added to GF1305.Gravatar jadep2016-06-17
* | Specific version of freeze for GF25519 (automation still needs a little work)Gravatar jadep2016-06-17
* | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...Gravatar jadep2016-06-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 01:36:53 +0000