aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tuple.v
Commit message (Collapse)AuthorAge
* Coalesce Tuple.pointwise2 and Tuple.fieldwiseGravatar Jason Gross2017-04-02
| | | | | | We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137.
* Add Tuple.etaGravatar Jason Gross2017-04-01
|
* added tuple [repeat]Gravatar jadep2017-03-30
|
* Get rid of list-based Tuple.mapGravatar Jason Gross2017-03-30
|
* Add Tuple.pointwise2, Tuple.map_fixGravatar Jason Gross2017-03-30
| | | | These are for definining boundedness and lining up judgmentally with reflective things
* change map_with to mapi_with, a version that handles the index explicitlyGravatar jadep2017-03-29
|
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
|
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
|
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
|
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
| | | | | These are for getting nicely reduced forms of, e.g., Tuple.map, without knowing exactly what the tuple is
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
| | | | Also, add [split_and]
* More universe fixesGravatar Jason Gross2017-01-15
|
* Fix an issue with universesGravatar Jason Gross2017-01-15
| | | | | | We don't want to force the universe of [option] below other universes; to get template polymorphism to refresh universes, we need to eta-expand [option].
* Add tuple lemmasGravatar Jason Gross2016-11-22
|
* Add fieldwise_mapGravatar Jason Gross2016-11-17
|
* use @implicits in rewrite (8.4)Gravatar Andres Erbsen2016-11-11
|
* prove admits in Util.TupleGravatar Andres Erbsen2016-11-11
|
* Add Tuple and HList lemmasGravatar Jason Gross2016-11-10
|
* Fix bug in 8.4Gravatar Jason Gross2016-11-09
|
* Add assoc_rightGravatar Jason Gross2016-11-09
|
* Fix Tuple.map2_SGravatar Jason Gross2016-11-09
|
* Add Tuple.map2_SGravatar Jason Gross2016-11-08
|
* Add map2_map{,_fst,_snd}Gravatar Jason Gross2016-11-08
|
* Rename iffT, add some lemmas about tuple and hlistGravatar Jason Gross2016-11-08
| | | | Some lemmas admitted
* Work around bug in 8.4Gravatar Jason Gross2016-11-08
|
* Add push_lift_optionGravatar Jason Gross2016-11-07
|
* Add tuple hd and tlGravatar Jason Gross2016-11-07
|
* Add more admitted tuple lemmasGravatar Jason Gross2016-11-06
|
* Add more admitted tuple lemmasGravatar Jason Gross2016-11-06
|
* Add Tuple.map_map2 (admitted)Gravatar Jason Gross2016-11-06
|
* Add admitted lemma about tuple map, add hlist lemGravatar Jason Gross2016-11-06
|
* Add Tuple lift pushGravatar Jason Gross2016-11-06
|
* Add functions for [tuple (option _) _]Gravatar Jason Gross2016-11-06
|
* Move hlist to new fileGravatar Jason Gross2016-11-01
|
* Fix a typo in the previous commitGravatar Jason Gross2016-11-01
|
* Generalize hlistGravatar Jason Gross2016-11-01
|
* Add hlist to tupleGravatar Jason Gross2016-11-01
|
* Fix implicit status of curryGravatar Jason Gross2016-10-27
|
* Add curry and uncurry to tupleGravatar Jason Gross2016-10-27
|
* Fix for Coq 8.4Gravatar Jason Gross2016-10-24
|
* Add more relations about fieldwiseGravatar Jason Gross2016-10-24
|
* Add Tuple.map2Gravatar Jason Gross2016-10-19
|
* Ed25519: add basepoint and prove most EdDSA preconditionsGravatar Andres Erbsen2016-10-10
|
* Add Tuple.mapGravatar Jason Gross2016-09-29
|
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
|
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
| | | | This way they won't become ambiguous if we add new files
* Defined an equality comparison for tuples that uses bool instead of Prop ↵Gravatar jadep2016-08-31
| | | | (like Z.eqb). This is necessary for the runtime equality comparison on tuples that will appear in square root calculations during point-decoding.
* Add length lemmasGravatar Jason Gross2016-08-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------------ 2m21.44s | Total | 2m18.90s || +0m02.54s ------------------------------------------------------------------------------------ 0m35.19s | CompleteEdwardsCurve/ExtendedCoordinates | 0m34.60s || +0m00.58s 0m17.20s | ModularArithmetic/ModularBaseSystemProofs | 0m16.72s || +0m00.48s 0m15.34s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.21s || +0m00.12s 0m14.89s | Specific/GF25519 | 0m14.38s || +0m00.50s 0m14.03s | Experiments/SpecEd25519 | 0m13.67s || +0m00.35s 0m08.57s | ModularArithmetic/Pow2BaseProofs | 0m08.67s || -0m00.09s 0m04.32s | Testbit | 0m04.28s || +0m00.04s 0m03.73s | BaseSystemProofs | 0m03.75s || -0m00.02s 0m03.30s | Experiments/SpecificCurve25519 | 0m03.24s || +0m00.05s 0m02.92s | Util/ListUtil | 0m02.98s || -0m00.06s 0m02.15s | Specific/GF1305 | 0m02.11s || +0m00.04s 0m02.11s | ModularArithmetic/ModularBaseSystemOpt | 0m02.16s || -0m00.05s 0m01.77s | Experiments/EdDSARefinement | 0m01.76s || +0m00.01s 0m01.67s | ModularArithmetic/BarrettReduction/ZBounded | 0m01.64s || +0m00.03s 0m01.54s | Encoding/PointEncodingPre | 0m01.50s || +0m00.04s 0m01.52s | Util/Tuple | 0m01.31s || +0m00.20s 0m01.20s | BaseSystem | 0m01.19s || +0m00.01s 0m01.19s | ModularArithmetic/ExtendedBaseVector | 0m01.17s || +0m00.02s 0m00.97s | ModularArithmetic/ModularBaseSystemField | 0m00.90s || +0m00.06s 0m00.93s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.88s || +0m00.05s 0m00.84s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.87s || -0m00.03s 0m00.82s | ModularArithmetic/Montgomery/ZBounded | 0m00.83s || -0m00.01s 0m00.68s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || +0m00.04s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.61s || +0m00.06s 0m00.64s | Util/AdditionChainExponentiation | 0m00.68s || -0m00.04s 0m00.64s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.07s 0m00.62s | Spec/EdDSA | 0m00.58s || +0m00.04s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.62s || -0m00.01s 0m00.56s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.57s || -0m00.00s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.42s || +0m00.01s 0m00.40s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.39s || +0m00.01s
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I do hereby revoke the privilege of [intuition] to grab random hints from random databases. This privilege is reserved for [debug_intuition], which comes with a warning about not being used in production code. This tactic is useful in conjunction with `Print Hint *`, to discover what hint databases the hints were grabbed from. (Suggestions for renaming [debug_intuition] welcome.) Any file using [intuition] must [Require Export Crypto.Util.FixCoqMistakes.]. It's possible we could lift this restriction by compiling [FixCoqMistakes] separately, and passing along `-require FixCoqMistakes` to Coq. Should we do this? After | File Name | Before || Change ------------------------------------------------------------------------------------ 3m29.54s | Total | 4m33.13s || -1m03.59s ------------------------------------------------------------------------------------ 0m03.75s | BaseSystemProofs | 0m43.84s || -0m40.09s 0m42.57s | CompleteEdwardsCurve/ExtendedCoordinates | 0m34.48s || +0m08.09s 0m03.04s | Util/ListUtil | 0m11.18s || -0m08.14s 0m01.62s | ModularArithmetic/PrimeFieldTheorems | 0m09.53s || -0m07.90s 0m00.87s | Util/NumTheoryUtil | 0m07.61s || -0m06.74s 0m01.61s | Encoding/PointEncodingPre | 0m06.93s || -0m05.31s 0m51.95s | Specific/GF25519 | 0m47.52s || +0m04.42s 0m12.30s | Experiments/SpecEd25519 | 0m11.29s || +0m01.01s 0m09.22s | Specific/GF1305 | 0m08.17s || +0m01.05s 0m03.48s | CompleteEdwardsCurve/Pre | 0m04.77s || -0m01.28s 0m02.70s | Assembly/State | 0m04.09s || -0m01.38s 0m01.55s | ModularArithmetic/ModularArithmeticTheorems | 0m02.93s || -0m01.38s 0m01.16s | Assembly/Pseudize | 0m02.34s || -0m01.17s 0m15.67s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.37s || -0m00.70s 0m06.02s | Algebra | 0m06.67s || -0m00.65s 0m05.90s | Experiments/GenericFieldPow | 0m06.68s || -0m00.77s 0m04.65s | WeierstrassCurve/Pre | 0m05.27s || -0m00.61s 0m03.93s | ModularArithmetic/Pow2BaseProofs | 0m03.94s || -0m00.00s 0m03.70s | ModularArithmetic/Tutorial | 0m03.85s || -0m00.14s 0m02.83s | ModularArithmetic/ModularBaseSystemOpt | 0m02.84s || -0m00.00s 0m02.74s | Experiments/EdDSARefinement | 0m01.80s || +0m00.94s 0m02.35s | Util/ZUtil | 0m02.51s || -0m00.15s 0m01.86s | Assembly/Wordize | 0m02.32s || -0m00.45s 0m01.23s | ModularArithmetic/ExtendedBaseVector | 0m01.20s || +0m00.03s 0m01.21s | BaseSystem | 0m01.63s || -0m00.41s 0m01.03s | Experiments/SpecificCurve25519 | 0m00.98s || +0m00.05s 0m01.01s | ModularArithmetic/ModularBaseSystemProofs | 0m01.11s || -0m00.10s 0m00.95s | ModularArithmetic/BarrettReduction/Z | 0m01.38s || -0m00.42s 0m00.92s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.81s || -0m00.89s 0m00.85s | ModularArithmetic/ModularBaseSystemField | 0m00.86s || -0m00.01s 0m00.82s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.79s || +0m00.02s 0m00.80s | Assembly/QhasmEvalCommon | 0m00.93s || -0m00.13s 0m00.73s | Spec/EdDSA | 0m00.59s || +0m00.14s 0m00.72s | Util/Tuple | 0m00.71s || +0m00.01s 0m00.70s | Util/IterAssocOp | 0m00.72s || -0m00.02s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.71s || -0m00.03s 0m00.66s | Assembly/Pipeline | 0m00.64s || +0m00.02s 0m00.65s | Testbit | 0m00.65s || +0m00.00s 0m00.65s | Assembly/PseudoConversion | 0m00.65s || +0m00.00s 0m00.64s | Util/AdditionChainExponentiation | 0m00.63s || +0m00.01s 0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || -0m00.01s 0m00.63s | Assembly/Pseudo | 0m00.65s || -0m00.02s 0m00.62s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.05s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.57s || +0m00.04s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.69s || -0m00.08s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.59s || +0m00.01s 0m00.56s | Assembly/StringConversion | 0m00.56s || +0m00.00s 0m00.54s | Spec/ModularWordEncoding | 0m00.61s || -0m00.06s 0m00.54s | Assembly/QhasmUtil | 0m00.46s || +0m00.08s 0m00.52s | Assembly/Qhasm | 0m00.53s || -0m00.01s 0m00.48s | Assembly/AlmostQhasm | 0m00.52s || -0m00.04s 0m00.48s | ModularArithmetic/Pre | 0m00.48s || +0m00.00s 0m00.46s | Assembly/Vectorize | 0m00.72s || -0m00.25s 0m00.45s | Spec/WeierstrassCurve | 0m00.44s || +0m00.01s 0m00.44s | Assembly/AlmostConversion | 0m00.44s || +0m00.00s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.51s || -0m00.08s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.38s || +0m00.03s 0m00.41s | Spec/CompleteEdwardsCurve | 0m00.43s || -0m00.02s 0m00.34s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s 0m00.03s | Util/FixCoqMistakes | N/A || +0m00.03s 0m00.02s | Util/Notations | 0m00.04s || -0m00.02s 0m00.02s | Util/Tactics | 0m00.02s || +0m00.00s
* tuple: applying functions to tuples of arbitrary lengthGravatar Andres Erbsen2016-07-12
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 10:57:24 +0000