aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519.v
Commit message (Collapse)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
| | | | | | | | | | | | | | | | | | | | | | | | This reverts commit fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b. Revert "copy_bounds" This reverts commit 4c395e83de3c0baf7f8639fa2fbe2b62ba509682. Revert "Add Common10_4Op" This reverts commit 677733838139ff09d4a2dd9ff82258492a9a5bab. Revert "Add Expr10_4Op" This reverts commit 540740e8a423d0ec9d1dddb173f772c441dc0a1a. Revert "Add i10top_correct_and_bounded" This reverts commit bc4184ce6086971799630a0419881c8d344811ca. Revert "Add appify10" This reverts commit 66b63b406d9c78a0cecbbf89e5baf282231215c5.
* Add appify10Gravatar Jason Gross2017-01-07
| | | | Grrrrrr, code duplication for ladderstep
* uncurry_n_op_fe25519Gravatar Jason Gross2016-11-25
|
* Update AddCoordinatesGravatar Jason Gross2016-11-17
| | | | Now the _correct_and_bounded lemma goes through
* 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 ↵Gravatar jadep2016-11-03
| | | | separately
* Changes to sqrt for easier bounds proofs; currently blocked on broken proof ↵Gravatar jadep2016-11-02
| | | | in GF25519Bounded
* 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
| | | | It'll be needed for generic reification and uncurrying
* Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
| | | | This way we will have a faster build of reification things
* Created separate definitions for cmovne and cmovl for reificationGravatar jadep2016-10-23
|
* Finish twedprm_ERep proofGravatar Jason Gross2016-10-23
| | | | (cc @andres-erbsen)
* Generalize field_from_redundant_representationGravatar Jason Gross2016-10-23
| | | | Note that the old version did not need phi', but the new version does
* 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 ↵Gravatar jadep2016-10-19
| | | | pointed out
* 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 ↵Gravatar jadep2016-10-12
| | | | return None if input is greater than modulus
* 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], ↵Gravatar jadep2016-09-06
| | | | cleaning up freeze-related organization and definitions along the way
* updated GF25519 to match new exponentiation chain codeGravatar jadep2016-08-31
|
* Replaced placeholdeer [opp] operation in ModularBaseSystem with a real ↵Gravatar jadep2016-08-24
| | | | implementation, and pushed that up through Specific.
* Added optimized [inv] operation to Specific, and removed dependencies on ↵Gravatar jadep2016-08-24
| | | | ModularBaseSystemField.v
* Speed up src/Specific/GF25519.v (#54)Gravatar Jason Gross2016-08-18
| | | | | | | | After | File Name | Before || Change ----------------------------------------------------------------- 0m13.37s | Total | 0m40.29s || -0m26.91s ----------------------------------------------------------------- 0m10.09s | Specific/GF25519 | 0m37.00s || -0m26.91s 0m03.29s | Experiments/SpecificCurve25519 | 0m03.30s || -0m00.00s
* 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 ↵Gravatar jadep2016-08-09
| | | | Specific.
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
| | | | | | | | | | | | ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1
* re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵Gravatar jadep2016-07-21
| | | | organization of reasoning.
* restructured ModularBaseSystem pipeline to put tuple conversion before ↵Gravatar jadep2016-07-20
| | | | ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 12:27:33 +0000