aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Expand)AuthorAge
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* Add Common10_4OpGravatar Jason Gross2017-01-07
* Add Expr10_4OpGravatar Jason Gross2017-01-07
* Add i10top_correct_and_boundedGravatar Jason Gross2017-01-07
* Add appify10Gravatar Jason Gross2017-01-07
* Admit Common9_4Op.vGravatar Jason Gross2016-12-08
* Fix looping in Coq 8.4 in ExtendedAddCoordinates.vGravatar Jason Gross2016-12-02
* Minor change to inm_op_correct_and_bounded_prefixGravatar Jason Gross2016-11-25
* Fix a typoGravatar Jason Gross2016-11-25
* Add inm_op_correct_and_bounded_iff_prefixGravatar Jason Gross2016-11-25
* Add inm_op_correct_and_boundedGravatar Jason Gross2016-11-25
* uncurry_n_op_fe25519Gravatar Jason Gross2016-11-25
* Various application lemmasGravatar Jason Gross2016-11-23
* More GF25519ReflectiveCommon generalizationGravatar Jason Gross2016-11-22
* Copy bounds, fix a typoGravatar Jason Gross2016-11-22
* Start work on a faster version of GF*Reflective/Common*Gravatar Jason Gross2016-11-21
* Fix missing import for List.repeat in 8.4Gravatar Jason Gross2016-11-21
* Better extractionGravatar Jason Gross2016-11-17
* Finish proofs about eliminating useless carriesGravatar Jason Gross2016-11-17
* Add another admitted lemmaGravatar Jason Gross2016-11-17
* Add GF25519BoundedExtendedAddCoordinatesGravatar Jason Gross2016-11-17
* Add src/Specific/GF25519BoundedAddCoordinates.vGravatar Jason Gross2016-11-17
* Add ReflectiveAddCoordinatesGravatar Jason Gross2016-11-17
* Fix some problems with previous commitGravatar Jason Gross2016-11-17
* Remove admits, fill templates, copy boundsGravatar Jason Gross2016-11-17
* Update AddCoordinatesGravatar Jason Gross2016-11-17
* Minor change in AddCoordinatesGravatar Jason Gross2016-11-17
* Move util definitions to util folderGravatar Jason Gross2016-11-17
* Add reified mostly-bounds-checked add_coordinatesGravatar 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
* Work around bug #5205 (arguments naming weirdness)Gravatar Jason Gross2016-11-16
* Split fixedpoint in interpfGravatar Jason Gross2016-11-16
* Add more things to Reflective/CommonGravatar Jason Gross2016-11-16
* Fix for Coq 8.5 (more unfolding)Gravatar Jason Gross2016-11-15
* Handle both kinds of sqrtGravatar Jason Gross2016-11-14
* More generic sqrtGravatar Jason Gross2016-11-14
* Fix postfreezeW_correct_and_boundedGravatar Jason Gross2016-11-14
* Speed up some GF25519 tacticsGravatar Jason Gross2016-11-14
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* Fix some sqrt thingsGravatar Jason Gross2016-11-14
* Fix a missing unfoldGravatar Jason Gross2016-11-14
* Update bounds things with prefreezeGravatar Jason Gross2016-11-14
* Add mulW_noinlineGravatar Jason Gross2016-11-14
* Work around bug #5198 (broken tc resolution)Gravatar Jason Gross2016-11-12
* More 8.4pl2 fixesGravatar Jason Gross2016-11-12
* Fix for Coq 8.2Gravatar Jason Gross2016-11-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 18:44:27 +0000