aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519.v
Commit message (Expand)AuthorAge
* change import order to avoid name-clash with [List.repeat] and [Tuple.repeat]Gravatar jadep2017-03-30
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add appify10Gravatar Jason Gross2017-01-07
* uncurry_n_op_fe25519Gravatar Jason Gross2016-11-25
* Update AddCoordinatesGravatar Jason Gross2016-11-17
* Move ExtendedAddCoordinates to new file, SpecGenGravatar Jason Gross2016-11-17
* Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarryGravatar Jason Gross2016-11-17
* Update bounds things with prefreezeGravatar Jason Gross2016-11-14
* GF25519: add ErepAddGravatar Andres Erbsen2016-11-11
* GF25519: add optimized addition chainGravatar Andres Erbsen2016-11-11
* separate freeze into two partsGravatar jadep2016-11-11
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 13:45:34 +0000