aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystemProofs.v
Commit message (Collapse)AuthorAge
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reveals and prevents notation clashes. Notable breakage: - `x {{ y }}` breaks `Context {forall x, {P x} + {~P x}}.` (@jadephilipoom) - `x [[ y ]]` breaks `destruct x as [[a]|[b]].` (@jadephilipoom) - `O :( A , B ): :?: L ::: R` breaks `((1):nat)` and `constr:(nat)` (@varomodt) After | File Name | Before || Change ------------------------------------------------------------------------------------ 3m16.07s | Total | 3m23.63s || -0m07.55s ------------------------------------------------------------------------------------ 0m16.90s | ModularArithmetic/ModularBaseSystemProofs | 0m19.02s || -0m02.12s 0m03.29s | ModularArithmetic/ModularBaseSystemOpt | 0m05.30s || -0m02.00s 0m12.04s | Experiments/SpecEd25519 | 0m13.89s || -0m01.85s 0m36.02s | CompleteEdwardsCurve/ExtendedCoordinates | 0m36.12s || -0m00.09s 0m34.48s | Specific/GF25519 | 0m34.27s || +0m00.20s 0m15.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.76s || -0m00.14s 0m07.36s | Specific/GF1305 | 0m07.34s || +0m00.02s 0m06.64s | Algebra | 0m06.14s || +0m00.50s 0m05.12s | WeierstrassCurve/Pre | 0m05.09s || +0m00.03s 0m04.58s | ModularArithmetic/Tutorial | 0m03.83s || +0m00.75s 0m04.46s | BaseSystemProofs | 0m04.33s || +0m00.12s 0m04.26s | ModularArithmetic/Pow2BaseProofs | 0m05.16s || -0m00.90s 0m03.91s | CompleteEdwardsCurve/Pre | 0m04.62s || -0m00.71s 0m02.75s | Assembly/State | 0m03.12s || -0m00.37s 0m02.55s | Experiments/EdDSARefinement | 0m01.85s || +0m00.69s 0m02.46s | Util/ZUtil | 0m02.45s || +0m00.00s 0m01.86s | Assembly/Wordize | 0m02.02s || -0m00.15s 0m01.68s | ModularArithmetic/ModularArithmeticTheorems | 0m01.68s || +0m00.00s 0m01.67s | ModularArithmetic/PrimeFieldTheorems | 0m01.96s || -0m00.29s 0m01.50s | Encoding/PointEncodingPre | 0m02.20s || -0m00.70s 0m01.46s | ModularArithmetic/BarrettReduction/Z | 0m01.02s || +0m00.43s 0m01.26s | BaseSystem | 0m01.21s || +0m00.05s 0m01.24s | Assembly/Pseudize | 0m01.22s || +0m00.02s 0m01.20s | ModularArithmetic/ExtendedBaseVector | 0m01.86s || -0m00.66s 0m01.04s | Util/IterAssocOp | 0m00.74s || +0m00.30s 0m00.96s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.67s || +0m00.28s 0m00.96s | Assembly/Pipeline | 0m00.65s || +0m00.30s 0m00.93s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.98s || -0m00.04s 0m00.93s | ModularArithmetic/ModularBaseSystemField | 0m00.95s || -0m00.01s 0m00.92s | Util/NumTheoryUtil | 0m01.19s || -0m00.26s 0m00.90s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.89s || +0m00.01s 0m00.82s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.95s || -0m00.13s 0m00.81s | Assembly/QhasmEvalCommon | 0m00.86s || -0m00.04s 0m00.80s | Assembly/StringConversion | 0m00.60s || +0m00.20s 0m00.79s | Assembly/Qhasm | 0m00.54s || +0m00.25s 0m00.73s | Assembly/Pseudo | 0m00.98s || -0m00.25s 0m00.72s | Util/AdditionChainExponentiation | 0m00.92s || -0m00.20s 0m00.69s | Experiments/SpecificCurve25519 | 0m00.72s || -0m00.03s 0m00.65s | Spec/ModularWordEncoding | 0m00.85s || -0m00.19s 0m00.65s | ModularArithmetic/ModularBaseSystemList | 0m00.68s || -0m00.03s 0m00.65s | Assembly/PseudoConversion | 0m00.67s || -0m00.02s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.62s || +0m00.02s 0m00.64s | Spec/EdDSA | 0m00.93s || -0m00.29s 0m00.64s | Testbit | 0m00.94s || -0m00.29s 0m00.63s | Encoding/ModularWordEncodingTheorems | 0m00.66s || -0m00.03s 0m00.62s | Assembly/AlmostQhasm | 0m00.49s || +0m00.13s 0m00.59s | ModularArithmetic/ModularBaseSystem | 0m00.61s || -0m00.02s 0m00.49s | Spec/WeierstrassCurve | 0m00.43s || +0m00.06s 0m00.49s | Assembly/QhasmUtil | 0m00.51s || -0m00.02s 0m00.49s | ModularArithmetic/Pre | 0m00.47s || +0m00.02s 0m00.47s | Assembly/Vectorize | 0m00.51s || -0m00.04s 0m00.46s | Assembly/AlmostConversion | 0m00.44s || +0m00.02s 0m00.42s | ModularArithmetic/Pow2Base | 0m00.42s || +0m00.00s 0m00.41s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.45s || -0m00.04s 0m00.41s | Spec/ModularArithmetic | 0m00.41s || +0m00.00s 0m00.39s | Spec/CompleteEdwardsCurve | 0m00.41s || -0m00.01s 0m00.03s | Util/Notations | 0m00.03s || +0m00.00s
* Fix 8.6 buildGravatar Jason Gross2016-07-26
| | | | | Terrible, horrible, no good, very bad bugs in Coq. https://coq.inria.fr/bugs/show_bug.cgi?id=4966
* Fix 8.4 build.Gravatar jadep2016-07-25
|
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-25
|\
* | Put ModularBaseSystem carries in terms of [carry_gen], and pushed this ↵Gravatar jadep2016-07-25
| | | | | | | | change through the pipeline. Also began the process of redoing canonicalization proofs, attempting to put the messy case analysis in theorem statements rather than separate lemmas.
| * 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
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-20
|\
* \ mergeGravatar jadep2016-07-20
|\ \
| | * Move mul_rep_extended (do we actually care about this?)Gravatar Jason Gross2016-07-20
| |/
| * Don't use auto with *Gravatar Jason Gross2016-07-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It's fragile and slow. Now we're 45 seconds faster. After | File Name | Before || Change ------------------------------------------------------------------------------- 1m03.42s | Total | 1m49.00s || -0m45.57s ------------------------------------------------------------------------------- 0m20.01s | ModularArithmetic/ModularBaseSystemProofs | 1m05.69s || -0m45.67s 0m32.14s | Specific/GF25519 | 0m31.92s || +0m00.21s 0m07.05s | Specific/GF1305 | 0m07.07s || -0m00.02s 0m02.84s | ModularArithmetic/ModularBaseSystemOpt | 0m02.90s || -0m00.06s 0m00.69s | Experiments/SpecificCurve25519 | 0m00.69s || +0m00.00s 0m00.69s | ModularArithmetic/ModularBaseSystemInterface | 0m00.73s || -0m00.04s
| * Remove dependency of ext_base on pseudomersenneGravatar Jason Gross2016-07-20
| |
| * Work around bad design in CoqGravatar Jason Gross2016-07-19
| | | | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=4949, [intuition] should not use [auto with *] by default
| * Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
| |
* | mergeGravatar jadep2016-07-19
|\|
* | Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.Gravatar jadep2016-07-19
| |
| * ext_base: now defined in terms of ext_limb_widthsGravatar Jason Gross2016-07-18
| |
| * Move more proofs earlierGravatar Jason Gross2016-07-18
| |
| * Express carry_simple in terms of carry_genGravatar Jason Gross2016-07-18
|/ | | | | | Also make much of the remaining code outside of Pow2BaseProofs independent of the precise definition of carry_simple. (We use [Local Opaque] to enforce this modularity.
* Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
| | | | | | | | | * Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
* rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ↵Gravatar jadep2016-07-18
| | | | (bases that are repeats of the same power of 2) into Pow2Base
* pushing through a tweak to the arguments of [sub], and defining a field over ↵Gravatar jadep2016-07-12
| | | | ModularBaseSystemInterface using some placeholder operations.
* Make [base] and [log_cap] notationsGravatar Jason Gross2016-07-11
| | | | | | | | Also use [ZUtil.Z.pow2_mod]. This lets us remove the dependency of ModularBaseSystem on ModularArithmetic.PseudoMersenneBaseParamProofs. This is a small part of reorganizing and factoring ModularBaseSystem for use with Barrett reduction.
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
* | added a few length proofs to ModularBaseSystemProofs to help with tuple ↵Gravatar jadep2016-07-08
| | | | | | | | conversion
| * Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.Gravatar jadep2016-07-07
| |
| * 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
| | |
| | * Make ZUtil more uniformGravatar Jason Gross2016-07-02
| |/ |/| | | | | | | | | | | | | The standard library uses Z.*, and Z* and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
| * added and proved shift/or decode operation 'decode_bitwise'Gravatar jadep2016-06-30
| |
| * encode operation in ModularBaseSystem now uses bitwise operators, taking ↵Gravatar jadep2016-06-29
| | | | | | | | advantage of the fact that base elements are required to be powers of 2
| * BaseSystem encode function is no longer naive; it does a mod/div loop rather ↵Gravatar jadep2016-06-28
|/ | | | than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
| | | | | This prevents notation conflicts (see comment in Notations.v for more explanation).
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
|
* PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵Gravatar jadep2016-06-15
| | | | base-length digit vectors)
* changed representation definition to require digits vector to be the exact ↵Gravatar jadep2016-06-15
| | | | length of the base vector
* Added canonicalization to ModularBaseSystemOpt.Gravatar jadep2016-06-15
|
* MergeGravatar jadep2016-06-14
|\
* | Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
| |
* | reversed modulus_digits and proved a few admitsGravatar jadep2016-06-13
| |
* | progress on second stage (conditional constant-time subtraction) of ↵Gravatar jadep2016-06-13
| | | | | | | | canonicalization proofs
| * More Coq 8.4pl2 fixesGravatar Jason Gross2016-06-11
| |
* | starting rewrite using different definition of mapGravatar jadep2016-06-11
|/
* First stage of canonicalization proofs complete; proved 3 carry loops reduce ↵Gravatar jadep2016-05-20
| | | | input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵Gravatar jadep2016-05-09
| | | | unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵Gravatar jadep2016-04-28
| | | | general contexts.
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
|
* Merge and refactor of GF25519Gravatar jadep2016-04-11
|
* made BaseVector instance globalGravatar Jade Philipoom2016-03-20
|
* refactor of Basesystem and ModularBaseSystem; includes general code ↵Gravatar Jade Philipoom2016-03-20
organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 14:07:54 +0000