aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Collapse)AuthorAge
* Add HProp, IsomorphismGravatar Jason Gross2016-07-29
|
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29
|
* 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
* re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵Gravatar jadep2016-07-21
| | | | organization of reasoning.
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-20
|\
| * Move mul_rep_extended (do we actually care about this?)Gravatar Jason Gross2016-07-20
| |
* | restructured ModularBaseSystem pipeline to put tuple conversion before ↵Gravatar jadep2016-07-20
| | | | | | | | ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
* | Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.Gravatar jadep2016-07-19
|/
* Experiments/SpecificCurve25519.v: curve25519 addition using small Z-sGravatar Andres Erbsen2016-07-13
|
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
| * wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
| |
| * Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
| |\
| * | Factored out some proofs that rely only on base being powers of two, and ↵Gravatar jadep2016-07-06
| | | | | | | | | | | | defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
* | | add new interface to ModularBaseSystemGravatar Andres Erbsen2016-07-03
|/ /
| * Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03
| | | | | | | | | | Define the spec of Weierstrass curves This is the start of work on P256.
| * Implement and prove Barrett reduction on Z (#18)Gravatar Jason Gross2016-07-03
|/ | | | | | | | Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia).
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25
|
* Update _CoqProjectGravatar Jason Gross2016-06-23
|
* Remove vestigal BoundedWord machineryGravatar Robert Sloan2016-06-23
|
* Update _CoqProjectGravatar Robert Sloan2016-06-23
|
* Remove unstable Pipeline.v examples from _CoqProjectGravatar Robert Sloan2016-06-23
|
* Add Language.v, Conversion.v to _CoqProjectGravatar Robert Sloan2016-06-23
|
* Add Pseudize, Vectorize, Wordize to the build processGravatar Robert Sloan2016-06-22
|
* Merge with public masterGravatar Robert Sloan2016-06-22
|\
| * Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
| | | | | | | | | | This prevents notation conflicts (see comment in Notations.v for more explanation).
| * Update _CoqProjectGravatar Jason Gross2016-06-22
| |
* | Merge with plv/masterGravatar Robert Sloan2016-06-22
|\|
| * move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
| |
| * remove obsolete rep mechanismGravatar Andres Erbsen2016-06-20
| |
| * Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-06-20
| | | | | | | | | | | | - PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway
| * Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
| |\ | | | | | | | | | includes broken files to be removed in next commit
| | * tuple toolingGravatar Andres Erbsen2016-06-20
| | |
| | * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵Gravatar Andres Erbsen2016-06-18
| | | | | | | | | | | | fewer nonzero ports. remove FField and FNsatz
| | * move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
| | |
| | * nsatz: reimplement, integrate, demonstrateGravatar Andres Erbsen2016-06-15
| | |
| | * [field] and [nsatz] do things now againGravatar Andres Erbsen2016-06-14
| | |
| * | Add coqprime that works with 8.5, bundle bedrockGravatar Jason Gross2016-06-10
| | | | | | | | | | | | | | | | | | This simplifes the build process, and also allows us to try to build with 8.5. We autodetect the version of Coq in the Makefile to decide which version of coqprime to build.
| | * generic field definitionGravatar Andres Erbsen2016-06-07
| |/
* | Meshing Assembly machinery into the MakefileGravatar Robert Sloan2016-06-06
| |
* | merging with masterGravatar Robert Sloan2016-06-06
|\|
* | merging with masterGravatar Robert Sloan2016-06-06
|\ \
* | | PseudoMedialConversion doneGravatar Robert Sloan2016-05-31
| | |
| | * F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵Gravatar Andres Erbsen2016-05-24
| | | | | | | | | | | | broken...
| | * Completed encoding reorganization; factored sign_bit out of PointEncodings ↵Gravatar jadep2016-04-28
| | | | | | | | | | | | and finished encoding admits.
| | * Reorganization and revision of Encoding code and redefinition of sign_bit ↵Gravatar jadep2016-04-25
| | | | | | | | | | | | function.
| | * added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵Gravatar jadep2016-04-21
| | | | | | | | | | | | weight 2^26)
| | * Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-04-20
| | |
| | * Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-19
| | |\
| | * | Defined a testbit variant for BaseSystem vectors and proved equivalence to ↵Gravatar jadep2016-04-19
| | | | | | | | | | | | | | | | Z.testbit.
| | | * Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
| | | | | | | | | | | | | | | | | | | | Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 12:22:59 +0000