aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
Commit message (Collapse)AuthorAge
* Replaced placeholdeer [opp] operation in ModularBaseSystem with a real ↵Gravatar jadep2016-08-24
| | | | implementation, and pushed that up through Specific.
* Moved a tactic to Util/Tactics.vGravatar jadep2016-08-24
|
* Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6Gravatar jadep2016-08-24
|
* Removed now-obsolete ModularBaseSystemField.v; field lemmas for ↵Gravatar jadep2016-08-24
| | | | ModularBaseSystem are now in ModularBaseSystemProofs.v and Specific/
* Added optimized [inv] operation to Specific, and removed dependencies on ↵Gravatar jadep2016-08-24
| | | | ModularBaseSystemField.v
* Shifted around some of the proofs in ModularBaseSystemField.v and propagated ↵Gravatar jadep2016-08-23
| | | | field proof through GF1305.v as a proof of concept; working towards deleting that ModularBaseSystemField.v
* Defined real versions of [pow] and [inv] in ModularBaseSystem, replacing ↵Gravatar jadep2016-08-23
| | | | placeholders, and proved their correctness. In the process, reorganized early parts of ModularBaseSystemProofs.v by moving some lemmas to PseudoMersenneBaseParamProofs.v and introducing lemmas about the algebraic properties of ModularBaseSystem operations.
* Proved homomorphism between ModularBaseSystem field and F qGravatar jadep2016-08-22
|
* Merge.Gravatar jadep2016-08-21
|\
* | Proved some leftover admits in Pow2BaseProofs.vGravatar jadep2016-08-21
| |
* | Finished [split_index] proofs and reworked conversion proofs to match.Gravatar jadep2016-08-21
| |
| * More 8.4 Admitted fixesGravatar Jason Gross2016-08-17
| |
| * More fixes for 8.4Gravatar Jason Gross2016-08-17
|/ | | | | Use [assert] rather than [pose proof] because [Admitted] picks up section variables in 8.5 but not 8.4.
* More 8.4 compatGravatar Jason Gross2016-08-16
|
* Fixes for Coq 8.4Gravatar Jason Gross2016-08-16
|
* Add some list util, and decode'_map_mulGravatar Jason Gross2016-08-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------------ 3m41.37s | Total | 3m29.78s || +0m11.59s ------------------------------------------------------------------------------------ 0m49.73s | Specific/GF25519 | 0m31.66s || +0m18.06s 0m23.64s | ModularArithmetic/Pow2BaseProofs | 0m31.36s || -0m07.71s 0m42.29s | CompleteEdwardsCurve/ExtendedCoordinates | 0m44.80s || -0m02.50s 0m08.88s | Specific/GF1305 | 0m07.07s || +0m01.81s 0m19.09s | ModularArithmetic/ModularBaseSystemProofs | 0m19.86s || -0m00.76s 0m16.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.74s || -0m00.11s 0m15.31s | Experiments/SpecEd25519 | 0m14.40s || +0m00.91s 0m10.10s | Testbit | 0m10.15s || -0m00.05s 0m04.95s | BaseSystemProofs | 0m04.49s || +0m00.46s 0m03.96s | Util/ListUtil | 0m03.16s || +0m00.79s 0m03.40s | Experiments/SpecificCurve25519 | 0m03.31s || +0m00.08s 0m02.36s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.69s || -0m00.33s 0m02.23s | ModularArithmetic/ModularBaseSystemOpt | 0m02.24s || -0m00.01s 0m02.14s | Util/Tuple | 0m01.87s || +0m00.27s 0m01.92s | Experiments/EdDSARefinement | 0m01.85s || +0m00.06s 0m01.71s | Encoding/PointEncodingPre | 0m01.67s || +0m00.04s 0m01.71s | BaseSystem | 0m01.28s || +0m00.42s 0m01.28s | ModularArithmetic/Montgomery/ZBounded | 0m00.85s || +0m00.43s 0m01.16s | ModularArithmetic/ExtendedBaseVector | 0m01.65s || -0m00.49s 0m01.04s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.94s || +0m00.10s 0m00.95s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.96s || -0m00.01s 0m00.89s | ModularArithmetic/ModularBaseSystemField | 0m00.90s || -0m00.01s 0m00.87s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.77s || +0m00.09s 0m00.78s | Encoding/ModularWordEncodingTheorems | 0m00.69s || +0m00.09s 0m00.73s | Spec/EdDSA | 0m00.67s || +0m00.05s 0m00.69s | Util/AdditionChainExponentiation | 0m00.74s || -0m00.05s 0m00.68s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.73s || -0m00.04s 0m00.67s | ModularArithmetic/ModularBaseSystemList | 0m00.71s || -0m00.03s 0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.70s || -0m00.08s 0m00.52s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.45s || +0m00.07s 0m00.47s | ModularArithmetic/Pow2Base | 0m00.42s || +0m00.04s
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-08-16
|\
* \ Merge of conversion development branch with masterGravatar jadep2016-08-16
|\ \
| * | Added optimized versions of [pack] and [unpack] to ModularBaseSystemOpt. ↵Gravatar jadep2016-08-16
| | | | | | | | | | | | Further optimization, including the unrolling of the entire loop, can be done in Specific/ once limb widths of both ModularBaseSystem format and wire format are known.
| | * Add decode_shift_appGravatar Jason Gross2016-08-16
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m11.87s | Total | 1m10.99s || +0m00.87s ---------------------------------------------------------------------------------- 0m13.47s | ModularArithmetic/Pow2BaseProofs | 0m10.72s || +0m02.75s 0m17.00s | ModularArithmetic/ModularBaseSystemProofs | 0m18.39s || -0m01.39s 0m16.12s | Specific/GF25519 | 0m16.25s || -0m00.12s 0m08.65s | Testbit | 0m09.32s || -0m00.67s 0m03.31s | Experiments/SpecificCurve25519 | 0m03.35s || -0m00.04s 0m02.54s | Specific/GF1305 | 0m02.60s || -0m00.06s 0m02.23s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.16s || +0m00.06s 0m02.06s | ModularArithmetic/ModularBaseSystemOpt | 0m02.04s || +0m00.02s 0m01.18s | ModularArithmetic/ExtendedBaseVector | 0m01.17s || +0m00.01s 0m00.91s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.83s || +0m00.08s 0m00.90s | ModularArithmetic/ModularBaseSystemField | 0m00.87s || +0m00.03s 0m00.89s | ModularArithmetic/Montgomery/ZBounded | 0m00.84s || +0m00.05s 0m00.68s | ModularArithmetic/ModularBaseSystemList | 0m00.62s || +0m00.06s 0m00.67s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || +0m00.03s 0m00.65s | ModularArithmetic/ModularBaseSystem | 0m00.63s || +0m00.02s 0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.56s || +0m00.04s
| * Instantiated conversion both to (pack) and from (unpack) another set of limb ↵Gravatar jadep2016-08-16
| | | | | | | | widths in ModularBaseSystem
| * Pow2BaseProofs.v : removed Z lemmas that are now in ZUtil, updated the way ↵Gravatar jadep2016-08-16
| | | | | | | | [convert'] checks its termination condition, and added a convenience length proof about [convert] for later use in ModularBaseSystemListProofs.v
* | Factor decode_shift_uniformGravatar Jason Gross2016-08-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m01.14s | Total | 1m01.73s || -0m00.58s ---------------------------------------------------------------------------------- 0m16.84s | ModularArithmetic/ModularBaseSystemProofs | 0m17.09s || -0m00.25s 0m14.65s | Specific/GF25519 | 0m14.69s || -0m00.03s 0m08.99s | ModularArithmetic/Pow2BaseProofs | 0m09.03s || -0m00.03s 0m05.01s | Testbit | 0m04.98s || +0m00.02s 0m03.29s | Experiments/SpecificCurve25519 | 0m03.30s || -0m00.00s 0m02.12s | Specific/GF1305 | 0m02.12s || +0m00.00s 0m02.03s | ModularArithmetic/ModularBaseSystemOpt | 0m02.04s || -0m00.01s 0m01.84s | ModularArithmetic/BarrettReduction/ZBounded | 0m01.87s || -0m00.03s 0m01.19s | ModularArithmetic/ExtendedBaseVector | 0m01.16s || +0m00.03s 0m00.88s | ModularArithmetic/ModularBaseSystemField | 0m00.85s || +0m00.03s 0m00.86s | ModularArithmetic/Montgomery/ZBounded | 0m01.23s || -0m00.37s 0m00.85s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.88s || -0m00.03s 0m00.71s | ModularArithmetic/ModularBaseSystemList | 0m00.61s || +0m00.09s 0m00.69s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.65s || +0m00.03s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.63s || -0m00.03s 0m00.60s | ModularArithmetic/ModularBaseSystem | 0m00.61s || -0m00.01s
| * Proved remaining lemmas directly about conversion loop; still need to prove ↵Gravatar jadep2016-08-14
| | | | | | | | lemmas about [split_index]
| * Conversion: main step proof doneGravatar jadep2016-08-13
| |
* | Add decode_nonnegGravatar Jason Gross2016-08-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m00.69s | Total | 1m02.14s || -0m01.44s ---------------------------------------------------------------------------------- 0m16.79s | ModularArithmetic/ModularBaseSystemProofs | 0m16.90s || -0m00.10s 0m14.73s | Specific/GF25519 | 0m15.40s || -0m00.67s 0m08.77s | ModularArithmetic/Pow2BaseProofs | 0m08.62s || +0m00.15s 0m04.79s | Testbit | 0m05.11s || -0m00.32s 0m03.24s | Experiments/SpecificCurve25519 | 0m03.31s || -0m00.06s 0m02.13s | Specific/GF1305 | 0m02.46s || -0m00.33s 0m02.01s | ModularArithmetic/ModularBaseSystemOpt | 0m02.08s || -0m00.07s 0m01.78s | ModularArithmetic/BarrettReduction/ZBounded | 0m01.75s || +0m00.03s 0m01.17s | ModularArithmetic/ExtendedBaseVector | 0m01.14s || +0m00.03s 0m00.88s | ModularArithmetic/ModularBaseSystemField | 0m00.91s || -0m00.03s 0m00.88s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.83s || +0m00.05s 0m00.82s | ModularArithmetic/ModularBaseSystemList | 0m00.62s || +0m00.19s 0m00.81s | ModularArithmetic/Montgomery/ZBounded | 0m00.85s || -0m00.03s 0m00.73s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.95s || -0m00.21s 0m00.59s | ModularArithmetic/ModularBaseSystem | 0m00.62s || -0m00.03s 0m00.58s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.59s || -0m00.01s
* | Add upper_bound_uniformGravatar Jason Gross2016-08-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m53.61s | Total | 1m54.34s || -0m00.73s ---------------------------------------------------------------------------------- 0m16.96s | ModularArithmetic/ModularBaseSystemProofs | 0m16.86s || +0m00.10s 0m14.72s | Specific/GF25519 | 0m14.70s || +0m00.02s 0m14.03s | Experiments/SpecEd25519 | 0m14.53s || -0m00.50s 0m09.03s | ModularArithmetic/Pow2BaseProofs | 0m08.82s || +0m00.20s 0m06.64s | ModularArithmetic/Montgomery/ZProofs | 0m06.74s || -0m00.10s 0m06.10s | Testbit | 0m05.49s || +0m00.60s 0m03.84s | BaseSystemProofs | 0m04.04s || -0m00.20s 0m03.83s | ModularArithmetic/Tutorial | 0m03.53s || +0m00.30s 0m03.31s | Util/ZUtil | 0m03.31s || +0m00.00s 0m03.30s | Experiments/SpecificCurve25519 | 0m03.29s || +0m00.00s 0m02.81s | ModularArithmetic/BarrettReduction/ZHandbook | 0m02.78s || +0m00.03s 0m02.42s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.41s || +0m00.00s 0m02.05s | Specific/GF1305 | 0m02.10s || -0m00.05s 0m02.01s | ModularArithmetic/ModularBaseSystemOpt | 0m02.03s || -0m00.02s 0m01.99s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.05s || -0m00.05s 0m01.98s | ModularArithmetic/ModularArithmeticTheorems | 0m02.04s || -0m00.06s 0m01.76s | ModularArithmetic/ExtendedBaseVector | 0m01.50s || +0m00.26s 0m01.53s | Encoding/PointEncodingPre | 0m01.62s || -0m00.09s 0m01.41s | ModularArithmetic/BarrettReduction/Z | 0m01.39s || +0m00.02s 0m01.18s | BaseSystem | 0m01.22s || -0m00.04s 0m01.09s | Util/NumTheoryUtil | 0m00.88s || +0m00.21s 0m01.01s | ModularArithmetic/PrimeFieldTheorems | 0m01.05s || -0m00.04s 0m00.92s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.99s || -0m00.06s 0m00.88s | ModularArithmetic/Montgomery/ZBounded | 0m01.21s || -0m00.32s 0m00.87s | ModularArithmetic/ModularBaseSystemField | 0m00.89s || -0m00.02s 0m00.86s | Spec/ModularWordEncoding | 0m00.58s || +0m00.28s 0m00.82s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.95s || -0m00.13s 0m00.66s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || +0m00.02s 0m00.66s | Encoding/ModularWordEncodingTheorems | 0m00.71s || -0m00.04s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.64s || +0m00.00s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.89s || -0m00.28s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.84s || -0m00.24s 0m00.59s | ModularArithmetic/ModularBaseSystem | 0m00.66s || -0m00.07s 0m00.46s | ModularArithmetic/Pre | 0m00.48s || -0m00.01s 0m00.45s | ModularArithmetic/ZBounded | 0m00.45s || +0m00.00s 0m00.45s | ModularArithmetic/Pow2Base | 0m00.47s || -0m00.01s 0m00.40s | ModularArithmetic/Montgomery/Z | 0m00.58s || -0m00.17s 0m00.39s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.60s || -0m00.20s 0m00.35s | Spec/ModularArithmetic | 0m00.39s || -0m00.04s
* | Weaker UniformBase assumptionsGravatar Jason Gross2016-08-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 0m59.51s | Total | 0m59.14s || +0m00.37s ---------------------------------------------------------------------------------- 0m16.46s | ModularArithmetic/ModularBaseSystemProofs | 0m16.45s || +0m00.01s 0m14.41s | Specific/GF25519 | 0m14.36s || +0m00.05s 0m08.35s | ModularArithmetic/Pow2BaseProofs | 0m08.58s || -0m00.23s 0m04.71s | Testbit | 0m04.33s || +0m00.37s 0m03.41s | Experiments/SpecificCurve25519 | 0m03.31s || +0m00.10s 0m02.09s | Specific/GF1305 | 0m02.05s || +0m00.04s 0m02.02s | ModularArithmetic/ModularBaseSystemOpt | 0m02.09s || -0m00.06s 0m01.71s | ModularArithmetic/BarrettReduction/ZBounded | 0m01.70s || +0m00.01s 0m01.15s | ModularArithmetic/ExtendedBaseVector | 0m01.16s || -0m00.01s 0m00.91s | ModularArithmetic/Montgomery/ZBounded | 0m00.84s || +0m00.07s 0m00.90s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.92s || -0m00.02s 0m00.86s | ModularArithmetic/ModularBaseSystemField | 0m00.90s || -0m00.04s 0m00.69s | ModularArithmetic/ModularBaseSystemList | 0m00.61s || +0m00.07s 0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.66s || -0m00.01s 0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.04s 0m00.59s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.62s || -0m00.03s
* | 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
* | Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-08-12
|\ \
* | | added convenience lemma about [bounded] and [upper_bound] in Pow2BaseProofs.vGravatar jadep2016-08-12
| | |
| | * New and improved conversion proofs (final conditions proven, invariant step ↵Gravatar jadep2016-08-12
| |/ |/| | | | | unproven)
| * Fix build for Coq < 8.6Gravatar Jason Gross2016-08-12
| |
| * Don't take advantage of design flaws (auto with *)Gravatar Jason Gross2016-08-11
|/ | | | See bug #4966, https://coq.inria.fr/bugs/show_bug.cgi?id=4966.
* mergeGravatar jadep2016-08-11
|\
* \ Merge conversion development branch to give jgross better lemmasGravatar jadep2016-08-11
|\ \
| * | Tweaks for 8.4 compatibilityGravatar jadep2016-08-11
| | |
| * | Removed old conversion cruft and fixed Testbit to fit new decode_bitwise proofsGravatar jadep2016-08-11
| | |
| | * Merge pull request #49 from JasonGross/bounded-z-likeGravatar Jason Gross2016-08-10
| | |\ | | | | | | | | Specify a type of bounded integers for modular arithmetic
| * | | removed defunct lemmas/admits, proved helper function for conversion is correctGravatar jadep2016-08-10
| | | |
| | * | Add ext_limb_widths_upper_boundGravatar Jason Gross2016-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m00.15s | Total | 1m00.12s || +0m00.03s ---------------------------------------------------------------------------------- 0m14.85s | Specific/GF25519 | 0m16.44s || -0m01.59s 0m16.98s | ModularArithmetic/ModularBaseSystemProofs | 0m16.66s || +0m00.32s 0m04.21s | ModularArithmetic/Pow2BaseProofs | 0m04.23s || -0m00.02s 0m03.81s | BaseSystemProofs | 0m03.96s || -0m00.14s 0m03.33s | Experiments/SpecificCurve25519 | 0m03.33s || +0m00.00s 0m03.01s | Util/ListUtil | 0m02.98s || +0m00.02s 0m02.43s | Specific/GF1305 | 0m02.00s || +0m00.43s 0m02.11s | ModularArithmetic/ModularBaseSystemOpt | 0m02.05s || +0m00.06s 0m01.45s | BaseSystem | 0m01.16s || +0m00.29s 0m01.21s | ModularArithmetic/ExtendedBaseVector | 0m01.17s || +0m00.04s 0m00.91s | ModularArithmetic/ModularBaseSystemField | 0m00.90s || +0m00.01s 0m00.83s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.76s || +0m00.06s 0m00.70s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.58s || +0m00.12s 0m00.66s | Testbit | 0m00.63s || +0m00.03s 0m00.64s | ModularArithmetic/ModularBaseSystemList | 0m00.58s || +0m00.06s 0m00.62s | Util/AdditionChainExponentiation | 0m00.62s || +0m00.00s 0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.55s || +0m00.05s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.60s || +0m00.00s 0m00.60s | ModularArithmetic/ModularBaseSystem | 0m00.55s || +0m00.04s 0m00.60s | ModularArithmetic/Pow2Base | 0m00.38s || +0m00.21s
| | * | Add ext_limb_widths_nonnegGravatar Jason Gross2016-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change -------------------------------------------------------------------------------- 0m42.93s | Total | 0m43.10s || -0m00.16s -------------------------------------------------------------------------------- 0m16.42s | ModularArithmetic/ModularBaseSystemProofs | 0m16.26s || +0m00.16s 0m14.44s | Specific/GF25519 | 0m14.68s || -0m00.24s 0m03.30s | Experiments/SpecificCurve25519 | 0m03.24s || +0m00.05s 0m02.13s | ModularArithmetic/ModularBaseSystemOpt | 0m02.10s || +0m00.02s 0m02.09s | Specific/GF1305 | 0m02.06s || +0m00.02s 0m01.08s | ModularArithmetic/ExtendedBaseVector | 0m01.19s || -0m00.10s 0m00.89s | ModularArithmetic/ModularBaseSystemField | 0m00.87s || +0m00.02s 0m00.81s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.85s || -0m00.03s 0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || -0m00.01s 0m00.60s | ModularArithmetic/ModularBaseSystemList | 0m00.63s || -0m00.03s 0m00.55s | ModularArithmetic/ModularBaseSystem | 0m00.58s || -0m00.02s
| | * | Add carry_simple_subGravatar Jason Gross2016-08-10
| | | |
| | | * Work around bug #4165 (broken context) in 8.4Gravatar Jason Gross2016-08-10
| | | | | | | | | | | | | | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=4165, context replacement is broken (in the presence of [let]).
| * | | Made decode_bitwise proofs go away, and proved sane lemmas about Z.testbit ↵Gravatar jadep2016-08-10
| | | | | | | | | | | | | | | | (BaseSystem.decode _ _)
| | | * Remove unused code (still in vcs history, in case we want it later)Gravatar Jason Gross2016-08-09
| | | |
| | | * Specify a type of bounded integers for mod arithGravatar Jason Gross2016-08-09
| | |/ | | | | | | | | | Also use it to implement Montgomery reduction and Barrett reduction.
| | * Work around broken lia in 8.4Gravatar Jason Gross2016-08-09
| | |
| | * Add alternate form of Montgomery, which does better about boundsGravatar Jason Gross2016-08-09
| |/ |/| | | | | | | | | | | | | | | After | File Name | Before || Change ----------------------------------------------------------------------- 0m06.96s | Total | 0m04.29s || +0m02.67s ----------------------------------------------------------------------- 0m06.56s | ModularArithmetic/Montgomery/ZProofs | 0m03.82s || +0m02.73s 0m00.40s | ModularArithmetic/Montgomery/Z | 0m00.47s || -0m00.06s
* | Tweaked structure of GF [carry_mul] so that carry chain is specified in ↵Gravatar jadep2016-08-09
| | | | | | | | Specific.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 05:20:23 +0000