aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve
Commit message (Collapse)AuthorAge
* proved an admit in field homomorphisms that turned out to be unprovable; I ↵Gravatar jadep2016-07-15
| | | | added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck.
* s/conservative_common_denominator/common_denominator/gGravatar Andres Erbsen2016-07-11
|
* remove field_algebraGravatar Andres Erbsen2016-07-11
|
* port CompleteEdwardsCurveTheorems (builds again)Gravatar Andres Erbsen2016-07-11
|
* pose proof fails where specialize works (typeclass resolution / unification?)Gravatar Andres Erbsen2016-07-11
|
* wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
|
* added proofs about addition chain exponentiation for later use in ↵Gravatar jadep2016-07-10
| | | | ModularBaseSystem [pow], which we need for sqrt and inversion.
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-06-27
|\
| * scalarmult support; EdDSA.sign produces valid signaturesGravatar Andres Erbsen2016-06-27
| |
* | update new lemma in CompleteEdwardsCurve/Pre to match other changes to that fileGravatar jadep2016-06-25
| |
* | Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_portGravatar jadep2016-06-24
|\|
* | merging point encoding portGravatar jadep2016-06-24
|\ \
* | | Ported PointEncodings to parameterize over field rather than modulus.Gravatar jadep2016-06-24
| | |
| | * Remove a useless introGravatar Jason Gross2016-06-24
| |/
| * ExtendedCoordinates: group.Gravatar Andres Erbsen2016-06-24
| |
| * Use Decidable machinery for is_eq_decGravatar Jason Gross2016-06-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows us to rely entirely on typeclass resolution to resolve these instances, without having to do ad-hoc things for [and]. After | File Name | Before || Change ------------------------------------------------------------------------------------ 2m21.71s | Total | 2m22.59s || -0m00.87s ------------------------------------------------------------------------------------ 0m28.82s | Specific/GF25519 | 0m29.86s || -0m01.03s 0m29.60s | ModularArithmetic/ModularBaseSystemProofs | 0m29.40s || +0m00.20s 0m21.25s | Experiments/SpecEd25519 | 0m21.28s || -0m00.03s 0m18.15s | CompleteEdwardsCurve/ExtendedCoordinates | 0m18.14s || +0m00.00s 0m11.95s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m11.94s || +0m00.00s 0m07.26s | Specific/GF1305 | 0m07.28s || -0m00.02s 0m03.77s | ModularArithmetic/Tutorial | 0m03.75s || +0m00.02s 0m03.76s | ModularArithmetic/ModularBaseSystemOpt | 0m03.75s || +0m00.00s 0m03.61s | CompleteEdwardsCurve/Pre | 0m03.63s || -0m00.02s 0m02.15s | ModularArithmetic/ModularArithmeticTheorems | 0m02.12s || +0m00.02s 0m01.88s | ModularArithmetic/PrimeFieldTheorems | 0m01.89s || -0m00.01s 0m01.75s | Algebra | 0m01.73s || +0m00.02s 0m01.21s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.17s || +0m00.04s 0m01.14s | ModularArithmetic/ExtendedBaseVector | 0m01.14s || +0m00.00s 0m01.01s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.98s || +0m00.03s 0m00.62s | Encoding/ModularWordEncodingTheorems | 0m00.63s || -0m00.01s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.61s || -0m00.01s 0m00.59s | Util/Decidable | 0m00.64s || -0m00.05s 0m00.58s | Spec/EdDSA | 0m00.61s || -0m00.03s 0m00.57s | ModularArithmetic/ModularBaseSystem | 0m00.61s || -0m00.04s 0m00.56s | Spec/ModularWordEncoding | 0m00.56s || +0m00.00s 0m00.51s | ModularArithmetic/PseudoMersenneBaseRep | 0m00.53s || -0m00.02s 0m00.37s | Spec/CompleteEdwardsCurve | 0m00.34s || +0m00.02s
| * Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
| |
| * Pseudize Let_InGravatar Robert Sloan2016-06-23
| |
| * Fix broken notations (hopefully)Gravatar Jason Gross2016-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).
| * Use Admitted, not Qed, when a proof has admitGravatar Jason Gross2016-06-21
| | | | | | | | | | | | | | | | [admit] is the same as [shelve] / [give_up] in Coq 8.5. Error: Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed. (in proof edwards_acurve_abelian_group)
| * Fix [Proper_add] in 8.5Gravatar Jason Gross2016-06-21
| | | | | | | | Not sure why eauto depth matters...
| * Make [bash] tactic easier to debugGravatar Jason Gross2016-06-21
| | | | | | | | Now you don't have to copy/paste the [match goal with ... end].
| * use Local Obligation Tactic (8.5-compat)Gravatar Andres Erbsen2016-06-21
| |
| * remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
| |
| * move nsatz into tactics directoryGravatar 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
| * 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
| |
| * edwards curve addition respects field homomorphismGravatar Andres Erbsen2016-06-16
| |
| * prove ring admitsGravatar Andres Erbsen2016-06-16
| |
| * edwards curve preliminaries: replace oncurve proof with nsatzGravatar Andres Erbsen2016-06-16
| |
| * nsatz: reimplement, integrate, demonstrateGravatar Andres Erbsen2016-06-15
| |
| * refactor nsatz wrappers into algebra fileGravatar Andres Erbsen2016-06-14
| |
| * [field] and [nsatz] do things now againGravatar Andres Erbsen2016-06-14
| |
| * stuck because overloading-by-typeclasses sucksGravatar Andres Erbsen2016-06-13
| | | | | | | | | | | | | | | | | | | | | | Using typeclasses for overloading clutters all users of the typeclass with an extra layer of indirection that would need to be unfolded in all proofs. Condemning all downstream Ltac to handling a new layer of definitions that have no semantic dignificance is suboptimal design (and encourages even worse design decisions like unfolding during rewriting). Overloading should be fully resolved during type inference, the resulting code must not be distinguishable from having the overloading resolved manually before entering the code.
* | Minor 8.5 changesGravatar Jason Gross2016-06-10
| |
* | More changes for 8.5Gravatar Jason Gross2016-06-10
| | | | | | | | [Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
| * generic field definitionGravatar Andres Erbsen2016-06-07
| |
| * ERep addGravatar Andres Erbsen2016-05-29
| |
| * verify derivation: EdDSA layerGravatar Andres Erbsen2016-05-28
| |
| * before changing SRep from N to F lGravatar Andres Erbsen2016-05-27
|/
* slightly nicer edwards curve extended coordinates additionGravatar Andres Erbsen2016-05-18
|
* ed25519: solve elliptic curve math admitsGravatar Andres Erbsen2016-04-25
|
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
|
* point_eq_decGravatar Andres Erbsen2016-04-22
|
* finished last cases of nonzero proofs for associativityGravatar jadep2016-04-21
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-19
|\
| * 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-06-26 09:19:12 +0000