aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25
|
* Various nsatz and field tactic improvementsGravatar Jason Gross2016-06-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------------ 2m29.81s | Total | 2m34.05s || -0m04.23s ------------------------------------------------------------------------------------ 0m11.98s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.22s || -0m03.24s 0m29.71s | ModularArithmetic/ModularBaseSystemProofs | 0m30.05s || -0m00.33s 0m29.12s | Specific/GF25519 | 0m29.12s || +0m00.00s 0m21.50s | Experiments/SpecEd25519 | 0m21.43s || +0m00.07s 0m18.20s | CompleteEdwardsCurve/ExtendedCoordinates | 0m18.24s || -0m00.03s 0m07.36s | Specific/GF1305 | 0m07.33s || +0m00.03s 0m06.66s | Experiments/GenericFieldPow | 0m06.89s || -0m00.22s 0m03.84s | ModularArithmetic/ModularBaseSystemOpt | 0m03.84s || +0m00.00s 0m03.82s | ModularArithmetic/Tutorial | 0m03.88s || -0m00.06s 0m03.74s | CompleteEdwardsCurve/Pre | 0m03.81s || -0m00.06s 0m02.30s | ModularArithmetic/ModularArithmeticTheorems | 0m02.27s || +0m00.02s 0m02.11s | ModularArithmetic/PrimeFieldTheorems | 0m02.05s || +0m00.06s 0m01.93s | Algebra | 0m02.06s || -0m00.13s 0m01.17s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.19s || -0m00.02s 0m01.13s | ModularArithmetic/ExtendedBaseVector | 0m01.18s || -0m00.05s 0m01.01s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m01.07s || -0m00.06s 0m00.61s | Encoding/ModularWordEncodingTheorems | 0m00.64s || -0m00.03s 0m00.61s | Spec/EdDSA | 0m00.62s || -0m00.01s 0m00.57s | Encoding/ModularWordEncodingPre | 0m00.62s || -0m00.05s 0m00.56s | Spec/ModularWordEncoding | 0m00.59s || -0m00.02s 0m00.55s | ModularArithmetic/ModularBaseSystem | 0m00.59s || -0m00.03s 0m00.52s | ModularArithmetic/PseudoMersenneBaseRep | 0m00.52s || +0m00.00s 0m00.41s | Tactics/Nsatz | 0m00.41s || +0m00.00s 0m00.38s | Spec/CompleteEdwardsCurve | 0m00.40s || -0m00.02s 0m00.03s | Util/Tactics | 0m00.03s || +0m00.00s
* Add a version of common_denominator w/o oversimplGravatar Jason Gross2016-06-24
| | | | | | | It first [set]s anything not containing a division. Unfortunately, it's not a good drop-in replacement, because some code relies on exactly how [field_simplify] calls [field_simplify_eq] >.<
* Remove a useless introGravatar Jason Gross2016-06-24
|
* ExtendedCoordinates: group.Gravatar Andres Erbsen2016-06-24
|
* isomorphism_to_subgroup_groupGravatar 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
* nsatz_contradict can now handle invalid _ <> _ hypothesesGravatar Jason Gross2016-06-23
|
* Add Unit.vGravatar Jason Gross2016-06-23
|
* Add equality on sum typesGravatar Jason Gross2016-06-23
|
* Merge pull request #8 from mit-plv/rsloan-pipeline-example-initGravatar Jason Gross2016-06-23
|\ | | | | Make Pipeline.v Build on 8.4
| * Remove examples for 8.4 compatibilityGravatar Robert Sloan2016-06-23
| |
| * Remove vestigal BoundedWord machineryGravatar Robert Sloan2016-06-23
| |
* | Improve some tactics and lemmasGravatar Jason Gross2016-06-23
| |
* | [break_match] should not be localGravatar Jason Gross2016-06-23
| |
| * Remove vestigal GaloisField machineryGravatar Robert Sloan2016-06-23
| |
* | Add tactics to Tactics, at most 2 sq-roots to AlgebraGravatar Jason Gross2016-06-23
| |
| * Make Pipeline.v Build on 8.4Gravatar Robert Sloan2016-06-23
|/
* Merge pull request #7 from mit-plv/rsloan-unstableGravatar Rob Sloan2016-06-23
|\ | | | | Merge Assembly Machinery into Master
| * Add Language.v, Conversion.v to _CoqProjectGravatar Robert Sloan2016-06-23
| |
* | surjective homomorphism from group makes a groupGravatar Andres Erbsen2016-06-23
| |
| * Merge branch 'master' of github.com:mit-plv/fiat-crypto into ↵Gravatar Robert Sloan2016-06-23
| |\ | |/ |/| | | public/rsloan-unstable
| * QhasmUtil.v: Remove 8.4-incompatible intro nameGravatar Robert Sloan2016-06-23
| |
| * Pipeline: several new examplesGravatar Robert Sloan2016-06-23
| |
* | Make [nsatz_contradict] better at inequalitiesGravatar Jason Gross2016-06-23
| |
| * Pseudize Lemmas for Dual OperationsGravatar Robert Sloan2016-06-23
| |
* | [field_algebra] now knows that 0 <> -0 is falseGravatar Jason Gross2016-06-23
| |
* | Work around bug #4851 in nsatzGravatar Jason Gross2016-06-23
| | | | | | | | | | Now our [nsatz] does not barf when you have duplicate equations in the context.
* | Add tactics for canonicalizing field (in)equalitiesGravatar Jason Gross2016-06-23
| |
* | Rename the nonzero lemma to an iff lemmaGravatar Jason Gross2016-06-23
| |
* | Add mul_nonzero_nonzero_and to Algebra.vGravatar Jason Gross2016-06-23
| |
| * Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
| |
| * Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
| |
| * Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
| |
| * Pseudize Let_In with minor notationsGravatar Robert Sloan2016-06-23
| |
| * Pseudize Let_InGravatar Robert Sloan2016-06-23
| |
| * Add Pseudize, Vectorize, Wordize to the build processGravatar Robert Sloan2016-06-22
| |
| * Make Assembly modules 8.5-compatibleGravatar Robert Sloan2016-06-22
| |
| * Merge with public masterGravatar Robert Sloan2016-06-22
| |\ | |/ |/|
* | EdDSA.Notations: indentationGravatar Andres Erbsen2016-06-22
| |
* | Fix broken notations (hopefully)Gravatar Jason Gross2016-06-22
| |
* | Fix missing notationsGravatar 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).
* | Fix for broken abstractGravatar Jason Gross2016-06-22
| | | | | | | | It breaks when used in [Instance ... := _.]
| * Replace NPeano -> Nat in src/Spec/EdDSAGravatar Robert Sloan2016-06-22
| |
* | Add decidability util fileGravatar Jason Gross2016-06-22
| | | | | | | | | | This will be useful for the Weierstrass curves, which require case-splitting on field equality.
* | Handle renaming of NPeano.pow to Nat.pow (#3)Gravatar Jason Gross2016-06-22
| | | | | | | | We leave ambiguous which [pow] and [modulo] we refer to, so that this builds in both 8.4 and 8.5
| * Merge with plv/masterGravatar Robert Sloan2016-06-22
| |\ | |/ |/|
| * Merging Pipeline.vGravatar Robert Sloan2016-06-22
| |\
| * \ squash commits + revert makefileGravatar Robert Sloan2016-06-22
| |\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 18:59:03 +0000