diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-04-04 01:02:17 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-05 18:30:46 -0400 |
commit | f578406dd028f3d8d2afb16fb5d8e7d15b9a022c (patch) | |
tree | e5a2db1aa39f05116254a865a2f1e8f0d95fd175 | |
parent | 15b9797fba579e38c6e97f0677be82b14e7924f2 (diff) |
make elliptic curve proofs faster and split them into files
fix EdwardsMontgomery
try to speed up Weierstrass proof
--amend
Conflicts fixed by Jason Gross; timing diff added by Jason Gross
After | File Name | Before || Change
-----------------------------------------------------------------------------------------------------------
35m50.76s | Total | 33m10.99s || +2m39.77s
-----------------------------------------------------------------------------------------------------------
2m07.08s | MontgomeryXProofs | N/A || +2m07.07s
0m00.72s | MontgomeryX | 1m39.97s || -1m39.25s
12m47.53s | WeierstrassCurve/WeierstrassCurveTheorems | 11m33.56s || +1m13.97s
2m35.44s | WeierstrassCurve/Projective | 2m26.24s || +0m09.19s
0m58.83s | Specific/IntegrationTest | 0m51.09s || +0m07.73s
0m50.02s | ModularArithmetic/ModularBaseSystemProofs | 0m42.63s || +0m07.39s
0m24.81s | EdDSARepChange | 0m18.72s || +0m06.08s
0m26.89s | CompleteEdwardsCurve/ExtendedCoordinates | 0m21.82s || +0m05.07s
0m47.18s | MontgomeryCurveTheorems | 0m42.44s || +0m04.74s
0m41.62s | Spec/Ed25519 | 0m37.32s || +0m04.29s
0m18.06s | Specific/NewBaseSystemTest | 0m13.09s || +0m04.96s
0m21.56s | Reflection/Z/ArithmeticSimplifierWf | 0m17.61s || +0m03.94s
0m12.12s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.28s || +0m03.83s
0m08.58s | Reflection/InlineWf | 0m11.71s || -0m03.13s
0m07.66s | Algebra/Ring | 0m10.68s || -0m03.01s
0m03.98s | MontgomeryCurve | N/A || +0m03.98s
0m54.83s | ModularArithmetic/Conversion | 0m56.89s || -0m02.06s
0m14.94s | Algebra/Field | 0m12.60s || +0m02.33s
0m11.18s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m09.07s || +0m02.10s
0m08.33s | Util/FixedWordSizesEquality | 0m06.16s || +0m02.16s
1m44.81s | Test/Curve25519SpecTestVectors | 1m46.63s || -0m01.81s
0m27.28s | Reflection/Named/MapCastWf | 0m28.30s || -0m01.01s
0m11.27s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m09.99s || +0m01.27s
0m08.72s | MxDHRepChange | 0m09.76s || -0m01.03s
0m04.74s | BoundedArithmetic/InterfaceProofs | 0m03.38s || +0m01.36s
0m04.71s | SaturatedBaseSystem | 0m03.70s || +0m01.00s
0m03.85s | ModularArithmetic/BarrettReduction/ZHandbook | 0m05.55s || -0m01.69s
0m03.17s | Reflection/LinearizeWf | 0m04.62s || -0m01.45s
0m32.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m33.15s || -0m00.53s
0m28.02s | ModularArithmetic/Pow2BaseProofs | 0m28.89s || -0m00.87s
0m27.30s | Reflection/Z/Bounds/InterpretationLemmas | 0m26.88s || +0m00.42s
0m21.01s | Specific/GF25519 | 0m20.88s || +0m00.13s
0m19.39s | Reflection/Named/ContextProperties/NameUtil | 0m20.12s || -0m00.73s
0m18.99s | Reflection/Named/ContextProperties/SmartMap | 0m19.90s || -0m00.91s
0m15.32s | Util/ZUtil | 0m16.14s || -0m00.82s
0m14.19s | Reflection/Z/ArithmeticSimplifierInterp | 0m13.86s || +0m00.33s
0m13.42s | Testbit | 0m12.97s || +0m00.44s
0m12.74s | Reflection/Named/MapCastInterp | 0m12.39s || +0m00.34s
0m10.83s | ModularArithmetic/Montgomery/ZProofs | 0m11.19s || -0m00.35s
0m10.36s | NewBaseSystem | 0m10.53s || -0m00.16s
0m09.47s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m10.15s || -0m00.67s
0m09.22s | Assembly/GF25519 | 0m08.77s || +0m00.45s
0m07.82s | CompleteEdwardsCurve/Pre | 0m07.86s || -0m00.04s
0m07.60s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m08.19s || -0m00.58s
0m07.08s | Algebra/Field_test | 0m06.51s || +0m00.57s
0m06.92s | Specific/GF1305 | 0m06.83s || +0m00.08s
0m06.29s | Specific/SC25519 | 0m05.46s || +0m00.83s
0m06.23s | Bedrock/Word | 0m06.80s || -0m00.56s
0m06.01s | ModularArithmetic/ModularBaseSystemListProofs | 0m05.24s || +0m00.76s
0m05.75s | Reflection/Z/Syntax/Equality | 0m05.64s || +0m00.11s
0m05.66s | Util/ListUtil | 0m05.91s || -0m00.25s
0m05.63s | Reflection/InlineCastWf | 0m05.46s || +0m00.16s
0m05.47s | Experiments/GenericFieldPow | 0m05.84s || -0m00.37s
0m04.96s | BaseSystemProofs | 0m03.98s || +0m00.98s
0m04.93s | Reflection/Named/CompileWf | 0m05.12s || -0m00.19s
0m04.38s | ModularArithmetic/ModularArithmeticTheorems | 0m04.29s || +0m00.08s
0m04.25s | Spec/MontgomeryCurve | 0m04.22s || +0m00.03s
0m04.19s | Reflection/Named/CompileInterp | 0m04.26s || -0m00.06s
0m04.13s | Specific/FancyMachine256/Montgomery | 0m03.25s || +0m00.87s
0m04.11s | CompleteEdwardsCurve/EdwardsMontgomery | 0m03.67s || +0m00.44s
0m03.95s | BoundedArithmetic/Double/Proofs/ShiftLeft | 0m04.14s || -0m00.18s
0m03.86s | ModularArithmetic/ZBoundedZ | 0m03.16s || +0m00.69s
0m03.85s | Reflection/EtaWf | 0m03.74s || +0m00.10s
0m03.79s | BoundedArithmetic/Double/Proofs/ShiftRight | 0m03.53s || +0m00.26s
0m03.76s | Specific/FancyMachine256/Barrett | 0m02.99s || +0m00.76s
0m03.74s | BoundedArithmetic/Double/Proofs/Decode | 0m03.47s || +0m00.27s
0m03.66s | Reflection/TestCase | 0m03.34s || +0m00.32s
0m03.40s | Reflection/Z/Bounds/Relax | 0m02.86s || +0m00.54s
0m03.34s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.38s || +0m00.96s
0m03.30s | Reflection/Named/ContextProperties | 0m02.60s || +0m00.69s
0m02.94s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.86s || -0m00.92s
0m02.82s | Specific/FancyMachine256/Core | 0m01.97s || +0m00.84s
0m02.68s | ModularArithmetic/ModularBaseSystemOpt | 0m02.49s || +0m00.18s
0m02.63s | Reflection/InlineInterp | 0m03.57s || -0m00.94s
0m02.58s | Assembly/State | 0m02.60s || -0m00.02s
0m02.43s | Reflection/Named/NameUtilProperties | 0m02.36s || +0m00.07s
0m02.43s | ModularArithmetic/Montgomery/ZBounded | 0m01.84s || +0m00.59s
0m02.21s | Reflection/WfProofs | 0m02.17s || +0m00.04s
0m02.20s | ModularArithmetic/PrimeFieldTheorems | 0m02.06s || +0m00.14s
0m02.12s | WeierstrassCurve/Pre | 0m01.91s || +0m00.21s
0m02.03s | Util/WordUtil | 0m02.64s || -0m00.61s
0m02.00s | Assembly/Evaluables | 0m01.98s || +0m00.02s
0m01.95s | Reflection/Named/InterpretToPHOASWf | 0m02.21s || -0m00.26s
0m01.94s | Reflection/WfReflective | 0m02.74s || -0m00.80s
0m01.84s | Assembly/Bounds | 0m01.40s || +0m00.44s
0m01.78s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.72s || +0m00.06s
0m01.54s | Assembly/Compile | 0m01.53s || +0m00.01s
0m01.46s | Assembly/WordizeUtil | 0m02.12s || -0m00.66s
0m01.44s | ModularArithmetic/BarrettReduction/Z | 0m02.31s || -0m00.87s
0m01.44s | Reflection/Named/InterpretToPHOASInterp | 0m01.30s || +0m00.13s
0m01.42s | Util/NatUtil | 0m02.15s || -0m00.73s
0m01.40s | Reflection/Z/Bounds/Pipeline/Definition | 0m01.09s || +0m00.30s
0m01.40s | Util/Tuple | 0m01.45s || -0m00.05s
0m01.36s | ModularArithmetic/ExtendedBaseVector | 0m01.84s || -0m00.48s
0m01.36s | Algebra/Group | 0m01.40s || -0m00.03s
0m01.35s | Assembly/Conversions | 0m01.21s || +0m00.14s
0m01.34s | BoundedArithmetic/X86ToZLikeProofs | 0m00.83s || +0m00.51s
0m01.34s | Reflection/MapCastInterp | 0m01.62s || -0m00.28s
0m01.30s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m01.25s || +0m00.05s
0m01.20s | BaseSystem | 0m01.56s || -0m00.36s
0m01.19s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.97s || +0m00.21s
0m01.15s | Reflection/InlineCastInterp | 0m00.86s || +0m00.28s
0m01.12s | Reflection/SmartBoundInterp | 0m01.04s || +0m00.08s
0m01.06s | Reflection/Relations | 0m01.05s || +0m00.01s
0m01.04s | ModularArithmetic/ModularBaseSystemList | 0m00.65s || +0m00.39s
0m01.04s | Assembly/PhoasCommon | 0m00.87s || +0m00.17s
0m01.03s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.72s || +0m00.31s
0m01.03s | Assembly/HL | 0m01.18s || -0m00.14s
0m01.02s | Assembly/LL | 0m01.02s || +0m00.00s
0m01.02s | Assembly/Pipeline | 0m00.92s || +0m00.09s
0m01.02s | ModularArithmetic/ModularBaseSystem | 0m00.76s || +0m00.26s
0m01.01s | Algebra/IntegralDomain | 0m01.12s || -0m00.11s
0m01.00s | Util/IterAssocOp | 0m00.78s || +0m00.21s
0m00.96s | Util/NumTheoryUtil | 0m01.34s || -0m00.38s
0m00.95s | Reflection/MapCastByDeBruijnInterp | 0m00.83s || +0m00.12s
0m00.95s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.76s || +0m00.18s
0m00.90s | Reflection/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.66s || +0m00.24s
0m00.90s | Reflection/SmartCastWf | 0m00.97s || -0m00.06s
0m00.89s | Encoding/ModularWordEncodingTheorems | 0m00.71s || +0m00.18s
0m00.88s | Spec/CompleteEdwardsCurve | 0m00.83s || +0m00.05s
0m00.87s | BoundedArithmetic/X86ToZLike | 0m00.88s || -0m00.01s
0m00.86s | Spec/ModularWordEncoding | 0m00.60s || +0m00.26s
0m00.83s | Reflection/Named/CompileProperties | 0m00.88s || -0m00.05s
0m00.83s | Reflection/WfInversion | 0m00.82s || +0m00.01s
0m00.82s | Karatsuba | 0m01.20s || -0m00.38s
0m00.82s | WeierstrassCurve/Definitions | N/A || +0m00.82s
0m00.81s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.80s || +0m00.01s
0m00.80s | Encoding/ModularWordEncodingPre | 0m00.66s || +0m00.14s
0m00.80s | Reflection/MapCastByDeBruijnWf | 0m00.91s || -0m00.10s
0m00.78s | BoundedArithmetic/Double/Core | 0m00.69s || +0m00.09s
0m00.78s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | 0m00.48s || +0m00.30s
0m00.78s | Assembly/QhasmEvalCommon | 0m00.80s || -0m00.02s
0m00.75s | Util/PartiallyReifiedProp | 0m00.73s || +0m00.02s
0m00.74s | Spec/EdDSA | 0m00.67s || +0m00.06s
0m00.71s | Reflection/BoundByCastInterp | 0m00.77s || -0m00.06s
0m00.71s | Reflection/Z/Syntax/Util | 0m00.80s || -0m00.09s
0m00.71s | Reflection/Z/Reify | 0m00.57s || +0m00.14s
0m00.70s | Util/NUtil | 0m00.52s || +0m00.17s
0m00.70s | Reflection/Z/CNotations | 0m00.56s || +0m00.13s
0m00.70s | Spec/WeierstrassCurve | 0m00.84s || -0m00.14s
0m00.69s | Assembly/StringConversion | 0m00.50s || +0m00.18s
0m00.69s | Reflection/Z/JavaNotations | 0m00.54s || +0m00.14s
0m00.68s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.47s || +0m00.21s
0m00.67s | Reflection/MultiSizeTest | 0m00.70s || -0m00.02s
0m00.67s | BoundedArithmetic/Double/Repeated/Proofs/Multiply | 0m00.68s || -0m00.01s
0m00.66s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.46s || +0m00.20s
0m00.65s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.53s || +0m00.12s
0m00.64s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.49s || +0m00.15s
0m00.62s | Reflection/Z/Bounds/Pipeline/Glue | 0m00.69s || -0m00.06s
0m00.62s | Reflection/Z/Bounds/MapCastByDeBruijn | 0m00.57s || +0m00.05s
0m00.62s | Reflection/Z/Bounds/Pipeline | 0m00.51s || +0m00.10s
0m00.62s | BoundedArithmetic/Double/Repeated/Core | 0m00.77s || -0m00.15s
0m00.61s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.42s || +0m00.19s
0m00.60s | BoundedArithmetic/Interface | 0m00.78s || -0m00.18s
0m00.60s | Reflection/Z/MapCastByDeBruijnWf | 0m00.46s || +0m00.13s
0m00.57s | Reflection/Named/WfInterp | 0m00.60s || -0m00.03s
0m00.57s | Reflection/Named/DeadCodeElimination | 0m00.45s || +0m00.11s
0m00.56s | Util/AdditionChainExponentiation | 0m00.48s || +0m00.08s
0m00.55s | Reflection/Named/PositiveContext/DefaultsProperties | 0m00.58s || -0m00.02s
0m00.54s | Reflection/InterpByIsoProofs | 0m00.80s || -0m00.26s
0m00.54s | BoundedArithmetic/ArchitectureToZLike | 0m00.70s || -0m00.15s
0m00.54s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.47s || +0m00.07s
0m00.54s | Reflection/Z/InlineWf | 0m00.57s || -0m00.02s
0m00.54s | Reflection/Named/FMapContext | 0m00.73s || -0m00.18s
0m00.54s | BoundedArithmetic/StripCF | 0m00.48s || +0m00.06s
0m00.54s | Reflection/Z/MapCastByDeBruijn | 0m00.58s || -0m00.03s
0m00.53s | Reflection/Z/MapCastByDeBruijnInterp | 0m00.66s || -0m00.13s
0m00.53s | Reflection/Z/FoldTypes | 0m00.56s || -0m00.03s
0m00.53s | Reflection/Z/Bounds/MapCastByDeBruijnInterp | 0m00.40s || +0m00.13s
0m00.53s | Reflection/Z/Bounds/MapCastByDeBruijnWf | 0m00.40s || +0m00.13s
0m00.53s | Reflection/WfReflectiveGen | 0m00.56s || -0m00.03s
0m00.52s | Reflection/Z/HexNotationConstants | 0m00.53s || -0m00.01s
0m00.52s | Util/CPSUtil | 0m00.49s || +0m00.03s
0m00.52s | Reflection/Z/Inline | 0m00.58s || -0m00.05s
0m00.52s | ModularArithmetic/Pre | 0m00.42s || +0m00.10s
0m00.52s | Reflection/Z/Bounds/Pipeline/OutputType | 0m00.35s || +0m00.17s
0m00.50s | Util/Decidable | 0m00.51s || -0m00.01s
0m00.50s | Reflection/InterpWf | 0m00.46s || +0m00.03s
0m00.49s | Reflection/Z/ArithmeticSimplifier | 0m00.65s || -0m00.16s
0m00.49s | Reflection/SmartBoundWf | 0m00.56s || -0m00.07s
0m00.48s | Reflection/Named/PositiveContext | 0m00.47s || +0m00.01s
0m00.48s | Reflection/Named/PositiveContext/Defaults | 0m00.60s || -0m00.12s
0m00.48s | Reflection/MapCastByDeBruijn | 0m00.44s || +0m00.03s
0m00.48s | Spec/ModularArithmetic | 0m00.44s || +0m00.03s
0m00.48s | Reflection/InputSyntax | 0m00.59s || -0m00.10s
0m00.48s | Reflection/InterpWfRel | 0m00.50s || -0m00.02s
0m00.47s | ModularArithmetic/Pow2Base | 0m00.56s || -0m00.09s
0m00.46s | BoundedArithmetic/Eta | 0m00.39s || +0m00.07s
0m00.45s | Reflection/Z/Syntax | 0m00.50s || -0m00.04s
0m00.44s | Reflection/Z/Bounds/Interpretation | 0m00.60s || -0m00.15s
0m00.44s | Assembly/Qhasm | 0m00.72s || -0m00.27s
0m00.44s | Util/HList | 0m00.47s || -0m00.02s
0m00.44s | Reflection/Named/RegisterAssign | 0m00.40s || +0m00.03s
0m00.42s | ModularArithmetic/ModularBaseSystemListZOperations | 0m00.38s || +0m00.03s
0m00.42s | ModularArithmetic/ModularBaseSystemWord | 0m00.37s || +0m00.04s
0m00.42s | ModularArithmetic/ZBounded | 0m00.64s || -0m00.22s
0m00.41s | Reflection/Z/InlineInterp | 0m00.58s || -0m00.17s
0m00.41s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.55s || -0m00.14s
0m00.40s | Assembly/QhasmUtil | 0m00.42s || -0m00.01s
0m00.40s | Util/ZRange | 0m00.43s || -0m00.02s
0m00.40s | ModularArithmetic/ModularBaseSystemListZOperationsProofs | 0m00.59s || -0m00.18s
0m00.39s | Util/BoundedWord | 0m00.40s || -0m00.01s
0m00.38s | Reflection/Named/Wf | 0m00.38s || +0m00.00s
0m00.38s | Reflection/FilterLive | 0m00.32s || +0m00.06s
0m00.38s | Reflection/Named/EstablishLiveness | 0m00.34s || +0m00.03s
0m00.38s | Reflection/MultiSizeTest2 | 0m00.44s || -0m00.06s
0m00.38s | Reflection/Tuple | 0m00.40s || -0m00.02s
0m00.38s | ModularArithmetic/Montgomery/Z | 0m00.58s || -0m00.19s
0m00.37s | Reflection/Named/ContextDefinitions | 0m00.34s || +0m00.02s
0m00.37s | Reflection/Reify | 0m00.51s || -0m00.14s
0m00.37s | Reflection/Named/ContextProperties/Tactics | 0m00.43s || -0m00.06s
0m00.36s | Tactics/Algebra_syntax/Nsatz | 0m00.58s || -0m00.21s
0m00.36s | Reflection/Named/Syntax | 0m00.38s || -0m00.02s
0m00.36s | Reflection/Named/InterpretToPHOAS | 0m00.46s || -0m00.10s
0m00.36s | Reflection/Named/Compile | 0m00.35s || +0m00.01s
0m00.35s | Util/Factorize | 0m00.46s || -0m00.11s
0m00.34s | Reflection/Named/MapCast | 0m00.33s || +0m00.01s
0m00.34s | Reflection/Named/IdContext | 0m00.35s || -0m00.00s
0m00.34s | Reflection/Named/SmartMap | 0m00.35s || -0m00.00s
0m00.34s | Reflection/Z/BinaryNotationConstants | 0m00.53s || -0m00.19s
0m00.33s | Reflection/Z/OpInversion | 0m00.44s || -0m00.10s
0m00.32s | Algebra/ScalarMult | 0m00.27s || +0m00.04s
0m00.32s | Reflection/MapCastWf | 0m00.50s || -0m00.18s
0m00.32s | Util/FixedWordSizes | 0m00.34s || -0m00.02s
0m00.32s | Reflection/Named/ContextOn | 0m00.36s || -0m00.03s
0m00.31s | Assembly/QhasmCommon | 0m00.29s || +0m00.02s
0m00.31s | Reflection/ExprInversion | 0m00.27s || +0m00.03s
0m00.28s | Bedrock/Nomega | 0m00.40s || -0m00.12s
0m00.28s | Reflection/SmartMap | 0m00.22s || +0m00.06s
0m00.26s | Reflection/Equality | 0m00.26s || +0m00.00s
0m00.26s | Util/Sum | 0m00.24s || +0m00.02s
0m00.26s | Algebra/Monoid | 0m00.26s || +0m00.00s
0m00.26s | Reflection/LinearizeInterp | 0m00.24s || +0m00.02s
0m00.26s | Algebra | 0m00.30s || -0m00.03s
0m00.24s | Reflection/EtaInterp | 0m00.20s || +0m00.03s
0m00.23s | Util/CaseUtil | 0m00.33s || -0m00.10s
0m00.21s | Spec/MxDH | 0m00.27s || -0m00.06s
0m00.19s | Util/LetInMonad | 0m00.28s || -0m00.09s
0m00.19s | Reflection/CommonSubexpressionElimination | 0m00.18s || +0m00.01s
0m00.18s | Reflection/InterpProofs | 0m00.19s || -0m00.01s
0m00.18s | Util/Option | 0m00.12s || +0m00.06s
0m00.17s | Reflection/BoundByCastWf | 0m00.21s || -0m00.03s
0m00.16s | Experiments/ExtrHaskellNats | 0m00.27s || -0m00.11s
0m00.14s | Reflection/RewriterWf | 0m00.18s || -0m00.03s
0m00.13s | Reflection/Conversion | 0m00.08s || +0m00.05s
0m00.13s | Reflection/Wf | 0m00.15s || -0m00.01s
0m00.12s | Reflection/Named/NameUtil | 0m00.14s || -0m00.02s
0m00.11s | Reflection/TypeInversion | 0m00.07s || +0m00.03s
0m00.10s | Util/Sigma | 0m00.13s || -0m00.03s
0m00.10s | Reflection/RewriterInterp | 0m00.10s || +0m00.00s
0m00.09s | Util/Relations | 0m00.10s || -0m00.01s
0m00.08s | Util/Prod | 0m00.13s || -0m00.05s
0m00.08s | Util/PointedProp | 0m00.13s || -0m00.05s
0m00.07s | Reflection/InlineCast | 0m00.04s || +0m00.03s
0m00.06s | Reflection/BoundByCast | 0m00.04s || +0m00.01s
0m00.06s | Util/Equality | 0m00.08s || -0m00.02s
0m00.05s | Reflection/SmartCastInterp | 0m00.04s || +0m00.01s
0m00.05s | Reflection/Inline | 0m00.06s || -0m00.00s
0m00.05s | Reflection/Syntax | 0m00.08s || -0m00.03s
0m00.05s | Reflection/FoldTypes | 0m00.04s || +0m00.01s
0m00.05s | Reflection/SmartBound | 0m00.08s || -0m00.03s
0m00.05s | Reflection/MapCast | 0m00.09s || -0m00.03s
0m00.05s | Util/Tactics | 0m00.04s || +0m00.01s
0m00.04s | Reflection/CountLets | 0m00.05s || -0m00.01s
0m00.04s | Util/HProp | 0m00.06s || -0m00.01s
0m00.04s | Util/Bool | 0m00.02s || +0m00.02s
0m00.04s | Reflection/TypeUtil | 0m00.05s || -0m00.01s
0m00.04s | Util/Tactics/BreakMatch | 0m00.04s || +0m00.00s
0m00.04s | Reflection/RenameBinders | 0m00.03s || +0m00.01s
0m00.04s | Reflection/InterpByIso | 0m00.04s || +0m00.00s
0m00.04s | Util/Sumbool | 0m00.05s || -0m00.01s
0m00.04s | Reflection/Linearize | 0m00.04s || +0m00.00s
0m00.04s | Reflection/Map | 0m00.05s || -0m00.01s
0m00.04s | Util/Tower | 0m00.04s || +0m00.00s
0m00.04s | Reflection/SmartCast | 0m00.03s || +0m00.01s
0m00.04s | Util/AutoRewrite | 0m00.04s || +0m00.00s
0m00.04s | Reflection/Eta | 0m00.05s || -0m00.01s
0m00.03s | Util/Tactics/RewriteHyp | 0m00.03s || +0m00.00s
0m00.03s | Reflection/Rewriter | 0m00.05s || -0m00.02s
0m00.03s | Util/Tactics/SplitInContext | 0m00.04s || -0m00.01s
0m00.03s | Util/Tactics/DestructHead | 0m00.03s || +0m00.00s
0m00.03s | Util/Tactics/ETransitivity | 0m00.04s || -0m00.01s
0m00.03s | Util/Tactics/Test | 0m00.02s || +0m00.00s
0m00.03s | Util/Sigma/Lift | 0m00.04s || -0m00.01s
0m00.03s | Util/IffT | 0m00.03s || +0m00.00s
0m00.03s | Util/Tactics/SetEvars | 0m00.02s || +0m00.00s
0m00.03s | Util/Tactics/PrintContext | 0m00.03s || +0m00.00s
0m00.03s | Encoding/EncodingTheorems | 0m00.04s || -0m00.01s
0m00.03s | Util/Tactics/Contains | 0m00.02s || +0m00.00s
0m00.03s | Util/GlobalSettings | 0m00.02s || +0m00.00s
0m00.03s | Util/Tactics/SetoidSubst | 0m00.03s || +0m00.00s
0m00.03s | Util/Sigma/MapProjections | 0m00.02s || +0m00.00s
0m00.03s | Util/Logic | 0m00.03s || +0m00.00s
0m00.03s | Util/Tactics/DebugPrint | 0m00.04s || -0m00.01s
0m00.02s | Tactics/VerdiTactics | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/Head | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/SideConditionsBeforeToAfter | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics/Forward | 0m00.03s || -0m00.00s
0m00.02s | Util/LetIn | 0m00.08s || -0m00.06s
0m00.02s | Util/Tactics/EvarExists | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/ChangeInAll | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/TransparentAssert | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/VM | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/DestructTrivial | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/Revert | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/DoWithHyp | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/MoveLetIn | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/SimplifyProjections | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics/SubstEvars | 0m00.03s || -0m00.00s
0m00.02s | Util/Notations | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics/GetGoal | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/Not | 0m00.04s || -0m00.02s
0m00.02s | Util/ChangeInAll | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/ConvoyDestruct | 0m00.05s || -0m00.03s
0m00.02s | Util/Curry | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/SimplifyRepeatedIfs | 0m00.03s || -0m00.00s
0m00.02s | Util/Isomorphism | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics/SpecializeBy | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/OnSubterms | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/UniquePose | 0m00.04s || -0m00.02s
0m00.02s | Util/Unit | 0m00.05s || -0m00.03s
0m00.02s | Spec/Encoding | 0m00.02s || +0m00.00s
0m00.02s | Util/FixCoqMistakes | 0m00.03s || -0m00.00s
0m00.02s | Util/Tactics/ClearDuplicates | 0m00.04s || -0m00.02s
0m00.02s | Util/Sigma/Associativity | 0m00.05s || -0m00.03s
0m00.02s | Util/Tactics/UnifyAbstractReflexivity | 0m00.02s || +0m00.00s
0m00.02s | Util/Tactics/DestructHyps | 0m00.05s || -0m00.03s
0m00.01s | Util/Tactics/SubstLet | 0m00.03s || -0m00.01s
0m00.00s | Util/Tactics/ESpecialize | 0m00.02s || -0m00.02s
-rw-r--r-- | _CoqProject | 3 | ||||
-rw-r--r-- | src/Algebra.v | 9 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/EdwardsMontgomery.v | 27 | ||||
-rw-r--r-- | src/MontgomeryCurve.v | 67 | ||||
-rw-r--r-- | src/MontgomeryCurveTheorems.v | 99 | ||||
-rw-r--r-- | src/MontgomeryX.v | 34 | ||||
-rw-r--r-- | src/MontgomeryXProofs.v | 57 | ||||
-rw-r--r-- | src/Util/Decidable.v | 16 | ||||
-rw-r--r-- | src/WeierstrassCurve/Definitions.v | 18 | ||||
-rw-r--r-- | src/WeierstrassCurve/WeierstrassCurveTheorems.v | 209 |
10 files changed, 394 insertions, 145 deletions
diff --git a/_CoqProject b/_CoqProject index c0d87b646..0406fecf5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -7,8 +7,10 @@ src/BaseSystem.v src/BaseSystemProofs.v src/EdDSARepChange.v src/Karatsuba.v +src/MontgomeryCurve.v src/MontgomeryCurveTheorems.v src/MontgomeryX.v +src/MontgomeryXProofs.v src/MxDHRepChange.v src/NewBaseSystem.v src/SaturatedBaseSystem.v @@ -323,6 +325,7 @@ src/Util/Tactics/TransparentAssert.v src/Util/Tactics/UnifyAbstractReflexivity.v src/Util/Tactics/UniquePose.v src/Util/Tactics/VM.v +src/WeierstrassCurve/Definitions.v src/WeierstrassCurve/Pre.v src/WeierstrassCurve/Projective.v src/WeierstrassCurve/WeierstrassCurveTheorems.v diff --git a/src/Algebra.v b/src/Algebra.v index ca86b54e4..342e9feaa 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -140,8 +140,15 @@ Section Algebra. Global Existing Instance field_div_Proper. End AddMul. - Definition char_ge {T} (eq:T->T->Prop) (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.lt p C -> not (eq (inj p) zero). + Definition char_ge (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.lt p C -> not (eq (inj p) zero). Existing Class char_ge. + Lemma char_ge_weaken id of_pos C + (HC:@char_ge id of_pos C) c (Hc:BinPos.Pos.le c C) + : @char_ge id of_pos c. + Proof. intros ??; eauto using BinPos.Pos.lt_le_trans. Qed. + (* TODO: make a typeclass instance that applies this lemma + automatically using [vm_decide] for the inequality if both + characteristics are literal constants. *) End Algebra. Section ZeroNeqOne. diff --git a/src/CompleteEdwardsCurve/EdwardsMontgomery.v b/src/CompleteEdwardsCurve/EdwardsMontgomery.v index c02e833ac..f5a30ff88 100644 --- a/src/CompleteEdwardsCurve/EdwardsMontgomery.v +++ b/src/CompleteEdwardsCurve/EdwardsMontgomery.v @@ -1,15 +1,17 @@ Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems. +Require Import Crypto.MontgomeryCurve. Require Import Crypto.Util.Notations Crypto.Util.Decidable. Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod. Require Import Crypto.Algebra Crypto.Algebra.Field. +Import BinNums. Module E. Section EdwardsMontgomery. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} + {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28} {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. @@ -17,13 +19,18 @@ Module E. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^ 2" := (x*x). + Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12. + Proof. eapply char_ge_weaken; eauto. vm_decide. Qed. + Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3. + Proof. eapply char_ge_weaken; eauto. vm_decide. Qed. + Context {a d: F} {nonzero_a : a <> 0} {square_a : exists sqrt_a, sqrt_a^2 = a} {nonsquare_d : forall x, x^2 <> d}. Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). Local Notation Ezero := (E.zero(nonzero_a:=nonzero_a)(d:=d)). - Local Notation Eadd := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). + Local Notation Eadd := (E.add(char_ge_3:=char_ge_3)(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). Local Notation Eopp := (E.opp(nonzero_a:=nonzero_a)(d:=d)). Let a_neq_d : a <> d. @@ -86,28 +93,22 @@ Module E. assert (f1 <> Fopp 1) by admit (* ad, d are nonsero *); fsatz. Admitted. - Import BinNums. - (* TODO: characteristic weakening lemmas *) - Context {char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}. - Context {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. - - Program Definition _EM : _ /\ _ /\ _ := + Program Definition _EM (discr_nonzero:id _) : _ /\ _ /\ _ := @Group.group_from_redundant_representation Mpoint M.eq Madd M.zero M.opp - (M.group(discr_nonzero:=_)) + (M.group discr_nonzero) Epoint E.eq Eadd Ezero Eopp of_Montgomery to_Montgomery _ _ _ _ _ . - Next Obligation. Proof. Admitted. (* discriminant nonzero *) - Next Obligation. Proof. Admitted. (* M->E->M *) Next Obligation. Proof. Admitted. (* M->E->M *) + Next Obligation. Proof. Admitted. (* equivalences match *) Next Obligation. Proof. Admitted. (* add *) Next Obligation. Proof. Admitted. (* opp *) Next Obligation. Proof. cbv [of_Montgomery to_Montgomery]; t; fsatz. Qed. - Global Instance homomorphism_of_Montgomery : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 _EM). - Global Instance homomorphism_to_Montgomery : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 _EM). + Global Instance homomorphism_of_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 (_EM discr_nonzero)). + Global Instance homomorphism_to_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 (_EM discr_nonzero)). End EdwardsMontgomery. End E. diff --git a/src/MontgomeryCurve.v b/src/MontgomeryCurve.v new file mode 100644 index 000000000..a04701ed5 --- /dev/null +++ b/src/MontgomeryCurve.v @@ -0,0 +1,67 @@ +Require Import Crypto.Algebra Crypto.Algebra.Field. +Require Import Crypto.Util.GlobalSettings. +Require Import Crypto.Util.Sum Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve. + +Module M. + Section MontgomeryCurve. + Import BinNat. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:Decidable.DecidableRel Feq} + {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "- x" := (Fopp x). + Local Notation "x ^ 2" := (x*x) (at level 30). + Local Notation "x ^ 3" := (x*x^2) (at level 30). + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "( x , y )" := (inl (pair x y)). + Local Open Scope core_scope. + + Context {a b: F} {b_nonzero:b <> 0}. + + Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b := + match P return F*F+∞ with + | (x, y) => (x, -y) + | ∞ => ∞ + end. + Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + + Local Notation add := (M.add(b_nonzero:=b_nonzero)). + Local Notation point := (@M.point F Feq Fadd Fmul a b). + + Section MontgomeryWeierstrass. + Local Notation "2" := (1+1). + Local Notation "3" := (1+2). + Local Notation "4" := (1+3). + Local Notation "16" := (4*4). + Local Notation "9" := (3*3). + Local Notation "27" := (3*9). + Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. + + + Local Notation WeierstrassA := ((3-a^2)/(3*b^2)). + Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)). + Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). + Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB). + Program Definition to_Weierstrass (P:@point) : Wpoint := + match M.coordinates P return F*F+∞ with + | (x, y) => ((x + a/3)/b, y/b) + | _ => ∞ + end. + Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + + Program Definition of_Weierstrass (P:Wpoint) : point := + match W.coordinates P return F*F+∞ with + | (x,y) => (b*x-a/3, b*y) + | _ => ∞ + end. + Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + End MontgomeryWeierstrass. + End MontgomeryCurve. +End M.
\ No newline at end of file diff --git a/src/MontgomeryCurveTheorems.v b/src/MontgomeryCurveTheorems.v index 61eb5f880..7f7ad5bdf 100644 --- a/src/MontgomeryCurveTheorems.v +++ b/src/MontgomeryCurveTheorems.v @@ -2,7 +2,8 @@ Require Import Crypto.Algebra Crypto.Algebra.Field. Require Import Crypto.Util.GlobalSettings. Require Import Crypto.Util.Sum Crypto.Util.Prod. Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve. +Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve. +Require Import Crypto.Spec.WeierstrassCurve Crypto.WeierstrassCurve.Definitions. Require Import Crypto.WeierstrassCurve.WeierstrassCurveTheorems. Module M. @@ -11,7 +12,12 @@ Module M. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} - {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. + Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12. + Proof. eapply char_ge_weaken; eauto. vm_decide. Qed. + Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3. + Proof. eapply char_ge_weaken; eauto; vm_decide. Qed. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. @@ -20,6 +26,7 @@ Module M. Local Notation "x ^ 3" := (x*x^2) (at level 30). Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Local Notation "9" := (3*3). Local Notation "27" := (3*9). Local Notation "'∞'" := unit : type_scope. Local Notation "'∞'" := (inr tt) : core_scope. Local Notation "( x , y )" := (inl (pair x y)). @@ -27,12 +34,11 @@ Module M. Context {a b: F} {b_nonzero:b <> 0}. - Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b := - match P return F*F+∞ with - | (x, y) => (x, -y) - | ∞ => ∞ - end. - Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + Local Notation WeierstrassA := ((3-a^2)/(3*b^2)). + Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)). + Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). + Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB). + Local Notation Wopp := (@W.opp F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec). Ltac t := repeat @@ -48,66 +54,29 @@ Module M. | _ => progress Prod.inversion_prod | _ => progress Tactics.BreakMatch.break_match_hyps | _ => progress Tactics.BreakMatch.break_match - | _ => progress cbv [M.coordinates M.add M.zero M.eq opp proj1_sig] in * - | _ => progress cbv [W.coordinates W.add W.zero W.eq W.inv proj1_sig] in * + | _ => progress cbv [M.coordinates M.add M.zero M.eq M.opp proj1_sig + W.coordinates W.add W.zero W.eq W.opp + M.of_Weierstrass M.to_Weierstrass] in * | |- _ /\ _ => split | |- _ <-> _ => split end. - Local Notation add := (M.add(b_nonzero:=b_nonzero)). - Local Notation point := (@M.point F Feq Fadd Fmul a b). + Program Definition _MW (discr_nonzero:id _) : _ /\ _ /\ _ := + @Group.group_from_redundant_representation + Wpoint W.eq Wadd W.zero Wopp + (abelian_group_group (W.commutative_group(char_ge_12:=char_ge_12)(discriminant_nonzero:=discr_nonzero))) + (@M.point F Feq Fadd Fmul a b) M.eq (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero)) M.zero (M.opp(b_nonzero:=b_nonzero)) + (M.of_Weierstrass(b_nonzero:=b_nonzero)) + (M.to_Weierstrass(b_nonzero:=b_nonzero)) + _ _ _ _ _ + . + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. - Section MontgomeryWeierstrass. - Local Notation "4" := (1+3). - Local Notation "16" := (4*4). - Local Notation "9" := (3*3). - Local Notation "27" := (3*9). - Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. - - - Local Notation WeierstrassA := ((3-a^2)/(3*b^2)). - Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)). - Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). - Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB). - Program Definition to_Weierstrass (P:@point) : Wpoint := - match M.coordinates P return F*F+∞ with - | (x, y) => ((x + a/3)/b, y/b) - | _ => ∞ - end. - Next Obligation. Proof. t; fsatz. Qed. - - Program Definition of_Weierstrass (P:Wpoint) : point := - match W.coordinates P return F*F+∞ with - | (x,y) => (b*x-a/3, b*y) - | _ => ∞ - end. - Next Obligation. Proof. t. fsatz. Qed. - - (*TODO: rename inv to opp, make it not require [discr_nonzero] *) - Context {discr_nonzero : (2 + 1 + 1) * WeierstrassA * WeierstrassA * WeierstrassA + - ((2 + 1 + 1) ^ 2 + (2 + 1 + 1) + (2 + 1 + 1) + 1 + 1 + 1) * - WeierstrassB * WeierstrassB <> 0}. - (* TODO: weakening lemma for characteristic *) - Context {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}. - Local Notation Wopp := (@W.inv F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec discr_nonzero). - - Program Definition _MW : _ /\ _ /\ _ := - @Group.group_from_redundant_representation - Wpoint W.eq Wadd W.zero Wopp - (abelian_group_group (W.commutative_group(discriminant_nonzero:=discr_nonzero))) - point M.eq (M.add(b_nonzero:=b_nonzero)) M.zero opp - of_Weierstrass - to_Weierstrass - _ _ _ _ _ - . - Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. - Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. - Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. - Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. - Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. - - Global Instance group : Algebra.group := proj1 _MW. - Global Instance homomorphism_of_Weierstrass : Monoid.is_homomorphism(phi:=of_Weierstrass) := proj1 (proj2 _MW). - Global Instance homomorphism_to_Weierstrass : Monoid.is_homomorphism(phi:=to_Weierstrass) := proj2 (proj2 _MW). - End MontgomeryWeierstrass. + Global Instance group discr_nonzero : Algebra.group := proj1 (_MW discr_nonzero). + Global Instance homomorphism_of_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.of_Weierstrass) := proj1 (proj2 (_MW discr_nonzero)). + Global Instance homomorphism_to_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.to_Weierstrass) := proj2 (proj2 (_MW discr_nonzero)). End MontgomeryCurve. End M. diff --git a/src/MontgomeryX.v b/src/MontgomeryX.v index a9cbd8836..6cb5b2387 100644 --- a/src/MontgomeryX.v +++ b/src/MontgomeryX.v @@ -1,7 +1,7 @@ Require Import Crypto.Algebra Crypto.Algebra.Field. Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations. Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems. +Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve. Module M. Section MontgomeryCurve. @@ -9,7 +9,6 @@ Module M. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} - {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. @@ -30,6 +29,9 @@ Module M. | ∞ => pair 1 0 end. + Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)). + Proof. eapply char_ge_weaken; eauto; vm_decide. Qed. + (* From Curve25519 paper by djb, appendix B. Credited to Montgomery *) Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}. Definition xzladderstep (x1:F) (Q Q':F*F) : ((F*F)*(F*F)) := @@ -50,33 +52,5 @@ Module M. dlet z3 := x1*(DA-CB)^2 in (pair (pair x2 z2) (pair x3 z3)) end. - - Ltac t := - repeat - match goal with - | _ => solve [ contradiction | trivial ] - | _ => progress intros - | _ => progress subst - | _ => progress Tactics.DestructHead.destruct_head' @M.point - | _ => progress Tactics.DestructHead.destruct_head' @prod - | _ => progress Tactics.DestructHead.destruct_head' @sum - | _ => progress Tactics.DestructHead.destruct_head' @and - | _ => progress Sum.inversion_sum - | _ => progress Prod.inversion_prod - | _ => progress Tactics.BreakMatch.break_match_hyps - | _ => progress Tactics.BreakMatch.break_match - | _ => progress cbv [fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig xzladderstep to_xz Let_In] in * - | |- _ /\ _ => split - end. - - Lemma xzladderstep_correct - (Q Q':point) x z x' z' x1 x2 z2 x3 z3 - (Hl:Logic.eq (pair(pair x2 z2)(pair x3 z3)) (xzladderstep x1 (pair x z) (pair x' z'))) - (H:match M.coordinates Q with∞=>z=0/\x<>0|(xQ,y)=>xQ=x/z/\z<>0 (* TODO *) /\ y <> 0 (* TODO: prove this from non-squareness of a^2 - 4 *) end) - (H':match M.coordinates Q' with∞=>z'=0/\x'<>0|(xQ',_)=>xQ'=x'/z'/\z'<>0 end) - (H1:match M.coordinates (add Q (opp Q')) with∞=>False|(x,y)=>x=x1/\x<>0 end): - match M.coordinates (add Q Q) with∞=>z2=0/\x2<>0|(xQQ,_)=>xQQ=x2/z2/\z2<>0 end /\ - match M.coordinates (add Q Q') with∞=>z3=0/\x3<>0|(xQQ',_)=>xQQ'=x3/z3/\z3<>0 end. - Proof using a24_correct char_ge_5. t; abstract fsatz. Qed. End MontgomeryCurve. End M. diff --git a/src/MontgomeryXProofs.v b/src/MontgomeryXProofs.v new file mode 100644 index 000000000..f3f0346c9 --- /dev/null +++ b/src/MontgomeryXProofs.v @@ -0,0 +1,57 @@ +Require Import Crypto.Algebra Crypto.Algebra.Field. +Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn. +Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve. +Require Import Crypto.MontgomeryX BinPos. + +Module M. + Section MontgomeryCurve. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:Decidable.DecidableRel Feq} + {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "( x , y )" := (inl (pair x y)). + + Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)). + Proof. eapply char_ge_weaken; eauto; vm_decide. Qed. + + Context {a b: F} {b_nonzero:b <> 0}. + Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}. + Local Notation add := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)). + Local Notation opp := (M.opp(a:=a)(b_nonzero:=b_nonzero)). + Local Notation point := (@M.point F Feq Fadd Fmul a b). + Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)). + + Ltac t := + repeat + match goal with + | _ => solve [ contradiction | trivial ] + | _ => progress intros + | _ => progress subst + | _ => progress Tactics.DestructHead.destruct_head' @M.point + | _ => progress Tactics.DestructHead.destruct_head' @prod + | _ => progress Tactics.DestructHead.destruct_head' @sum + | _ => progress Tactics.DestructHead.destruct_head' @and + | _ => progress Sum.inversion_sum + | _ => progress Prod.inversion_prod + | _ => progress Tactics.BreakMatch.break_match_hyps + | _ => progress Tactics.BreakMatch.break_match + | _ => progress cbv [fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig M.xzladderstep M.to_xz Let_In] in * + | |- _ /\ _ => split + end. + + Lemma xzladderstep_correct + (Q Q':point) x z x' z' x1 x2 z2 x3 z3 + (Hl:Logic.eq (pair(pair x2 z2)(pair x3 z3)) (xzladderstep x1 (pair x z) (pair x' z'))) + (H:match M.coordinates Q with∞=>z=0/\x<>0|(xQ,y)=>xQ=x/z/\z<>0 (* TODO *) /\ y <> 0 (* TODO: prove this from non-squareness of a^2 - 4 *) end) + (H':match M.coordinates Q' with∞=>z'=0/\x'<>0|(xQ',_)=>xQ'=x'/z'/\z'<>0 end) + (H1:match M.coordinates (add Q (opp Q')) with∞=>False|(x,y)=>x=x1/\x<>0 end): + match M.coordinates (add Q Q) with∞=>z2=0/\x2<>0|(xQQ,_)=>xQQ=x2/z2/\z2<>0 end /\ + match M.coordinates (add Q Q') with∞=>z3=0/\x3<>0|(xQQ',_)=>xQQ'=x3/z3/\z3<>0 end. + Proof using a24_correct char_ge_5. t; abstract fsatz. Qed. + End MontgomeryCurve. +End M. diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index e7e8ce471..2703ef108 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -11,7 +11,6 @@ Local Open Scope type_scope. Class Decidable (P : Prop) := dec : {P} + {~P}. Arguments dec _%type_scope {_}. - Notation DecidableRel R := (forall x y, Decidable (R x y)). Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10. @@ -85,7 +84,6 @@ Lemma dec_not {A} `{Decidable A} : Decidable (~A). Proof. solve_decidable_transparent. Defined. (** Disallow infinite loops of dec_not *) Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances. - Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined. Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined. Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined. @@ -110,8 +108,6 @@ Global Instance dec_le_Z : DecidableRel BinInt.Z.le := ZArith_dec.Z_le_dec. Global Instance dec_gt_Z : DecidableRel BinInt.Z.gt := ZArith_dec.Z_gt_dec. Global Instance dec_ge_Z : DecidableRel BinInt.Z.ge := ZArith_dec.Z_ge_dec. -Global Instance dec_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec. - Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B} {HD : Decidable (P (fst x) (snd x))} : Decidable (let '(a, b) := x in P a b) | 1. @@ -139,6 +135,16 @@ Proof. solve_decidable_transparent. Defined. Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A. Proof. solve_decidable_transparent. Defined. +Global Instance dec_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec. +Global Instance dec_lt_positive : DecidableRel BinPos.Pos.lt. +Proof. eauto using Decidable_iff_to_impl, Pos.ltb_lt with typeclass_instances. Defined. +Global Instance dec_le_positive : DecidableRel BinPos.Pos.le. +Proof. eauto using Decidable_iff_to_impl, Pos.leb_le with typeclass_instances. Defined. +Global Instance dec_gt_positive : DecidableRel BinPos.Pos.gt. +Proof. eauto using Decidable_iff_to_flip_impl, Pos.gt_lt_iff with typeclass_instances. Defined. +Global Instance dec_ge_positive : DecidableRel BinPos.Pos.ge. +Proof. eauto using Decidable_iff_to_flip_impl, Pos.ge_le_iff with typeclass_instances. Defined. + Lemma dec_of_semidec {P : Prop} (H : option P) (H_complete : H = None -> ~P) : Decidable P. Proof. destruct H; [ left; assumption | right; apply H_complete, eq_refl ]. Defined. @@ -169,4 +175,4 @@ Lemma cast_if_eq_refl {T H P} t v : @cast_if_eq T H P t t v = Some v. Proof. compute; clear; destruct (H t t) as [ [] |e]; [ reflexivity | destruct (e eq_refl) ]. -Qed. +Qed.
\ No newline at end of file diff --git a/src/WeierstrassCurve/Definitions.v b/src/WeierstrassCurve/Definitions.v new file mode 100644 index 000000000..fb400d8c8 --- /dev/null +++ b/src/WeierstrassCurve/Definitions.v @@ -0,0 +1,18 @@ +Require Import Crypto.Spec.WeierstrassCurve. +Require Import Crypto.Algebra Crypto.Algebra.Field. +Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch. + +Module W. + Section W. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} + {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:DecidableRel Feq}. + + Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b + := match W.coordinates P return F*F+_ with + | inl (x1, y1) => inl (x1, Fopp y1) + | _ => P + end. + Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed. + End W. +End W.
\ No newline at end of file diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v index 38dda01d6..7547eb147 100644 --- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v +++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v @@ -1,6 +1,6 @@ Require Import Coq.Numbers.BinNums. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Spec.WeierstrassCurve. +Require Import Crypto.Spec.WeierstrassCurve Crypto.WeierstrassCurve.Definitions. Require Import Crypto.Algebra Crypto.Algebra.Field. Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch. Require Import Coq.PArith.BinPos. @@ -9,41 +9,188 @@ Module W. Section W. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} - {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: shouldn't need we need 4, not 12? *) - {Feq_dec:DecidableRel Feq}. + {Feq_dec:DecidableRel Feq} + {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}. (* FIXME: shouldn't need we need 4, not 12? *) + Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3. + Proof. eapply char_ge_weaken; eauto; vm_decide. Qed. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Infix "+" := Fadd. Local Infix "-" := Fsub. Local Infix "*" := Fmul. Local Notation "4" := (1+1+1+1). Local Notation "27" := (4*4 + 4+4 +1+1+1). - Context {discriminant_nonzero:4*a*a*a + 27*b*b <> 0}. - Program Definition inv (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b - := match W.coordinates P return F*F+_ with - | inl (x1, y1) => inl (x1, Fopp y1) - | _ => P - end. - Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed. + Global Instance commutative_group {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} : abelian_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp). + Proof using Type. + Time + repeat match goal with + | _ => solve [ contradiction | trivial | exact _ ] + | _ => intro + | |- Equivalence _ => split + | |- abelian_group => split | |- group => split | |- monoid => split + | |- is_associative => split | |- is_commutative => split + | |- is_left_inverse => split | |- is_right_inverse => split + | |- is_left_identity => split | |- is_right_identity => split + | _ => progress destruct_head' @W.point + | _ => progress destruct_head' sum + | _ => progress destruct_head' prod + | _ => progress destruct_head' unit + | _ => progress destruct_head' and + | _ => progress cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig]in* + | _ => progress break_match + end. + (* Finished transaction in 2.098 secs (2.099u,0.s) (successful) *) + all: try split. + (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *) - Global Instance commutative_group : abelian_group(eq:=W.eq)(op:=W.add)(id:=W.zero)(inv:=inv). - Proof using Feq_dec discriminant_nonzero field char_ge_12. - repeat match goal with - | _ => solve [ contradiction | trivial | exact _ ] - | _ => intro - | |- Equivalence _ => split - | |- abelian_group => split | |- group => split | |- monoid => split - | |- is_associative => split | |- is_commutative => split - | |- is_left_inverse => split | |- is_right_inverse => split - | |- is_left_identity => split | |- is_right_identity => split - | _ => progress destruct_head' @W.point - | _ => progress destruct_head' sum - | _ => progress destruct_head' prod - | _ => progress destruct_head' unit - | _ => progress destruct_head' and - | _ => progress cbv [inv W.eq W.zero W.add W.coordinates proj1_sig]in* - | _ => progress break_match - end. - all: try abstract(fsatz_prepare_hyps; repeat split; fsatz_solve). - Qed. + (* The [discriminant_nonzero] hypothesis makes [fsatz] slow but + is necessary in some cases. Thus, we wrap it in [id] by detault + to hide it from [nsatz] but unfold it when normal [fsatz] fails. *) + (* Variable re-ordering is a micro-optimization *) + (* TODO: why does par not work here? *) + Ltac s := abstract ( + match goal with [H:id _ |- _] => move H at bottom end; + move b at bottom; + move a at bottom; + repeat match goal with [H: ?x = Fopp ?y |- _] => is_var x; is_var y; revert H end; intros; + repeat match goal with [H: ?x = ?y |- _] => is_var x; is_var y; revert H end; intros; + repeat split; + solve + [ fsatz + | cbv [id] in *; fsatz] + ). + Time s. (* Finished transaction in 0.099 secs (0.096u,0.003s) (successful) *) + Time s. (* Finished transaction in 0.094 secs (0.093u,0.s) (successful) *) + Time s. (* Finished transaction in 0.48 secs (0.48u,0.s) (successful) *) + Time s. (* Finished transaction in 2.229 secs (2.226u,0.003s) (successful) *) + Time s. (* Finished transaction in 3.164 secs (3.153u,0.01s) (successful) *) + Time s. (* Finished transaction in 2.218 secs (2.199u,0.019s) (successful) *) + Time s. (* Finished transaction in 3.499 secs (3.486u,0.01s) (successful) *) + Time s. (* Finished transaction in 1.164 secs (1.16u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.971 secs (1.953u,0.016s) (successful) *) + Time s. (* Finished transaction in 2.344 secs (2.343u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.287 secs (1.286u,0.s) (successful) *) + Time s. (* Finished transaction in 1.781 secs (1.783u,0.s) (successful) *) + Time s. (* Finished transaction in 0.497 secs (0.496u,0.s) (successful) *) + Time s. (* Finished transaction in 1.859 secs (1.856u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.499 secs (1.499u,0.s) (successful) *) + Time s. (* Finished transaction in 1.6 secs (1.6u,0.s) (successful) *) + Time s. (* Finished transaction in 1.446 secs (1.443u,0.s) (successful) *) + Time s. (* Finished transaction in 1.56 secs (1.563u,0.s) (successful) *) + Time s. (* Finished transaction in 1.62 secs (1.616u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.973 secs (1.966u,0.006s) (successful) *) + Time s. (* Finished transaction in 7.66 secs (7.663u,0.s) (successful) *) + Time s. (* Finished transaction in 7.645 secs (7.643u,0.003s) (successful) *) + Time s. (* Finished transaction in 5.956 secs (5.949u,0.006s) (successful) *) + Time s. (* Finished transaction in 7.835 secs (7.803u,0.s) (successful) *) + Time s. (* Finished transaction in 1.893 secs (1.893u,0.s) (successful) *) + Time s. (* Finished transaction in 10.23 secs (10.229u,0.003s) (successful) *) + Time s. (* Finished transaction in 11.059 secs (11.036u,0.02s) (successful) *) + Time s. (* Finished transaction in 8.965 secs (8.963u,0.s) (successful) *) + Time s. (* Finished transaction in 9.539 secs (9.539u,0.003s) (successful) *) + Time s. (* Finished transaction in 2.019 secs (2.013u,0.003s) (successful) *) + Time s. (* Finished transaction in 2.907 secs (2.9u,0.01s) (successful) *) + Time s. (* Finished transaction in 1.622 secs (1.613u,0.01s) (successful) *) + Time s. (* Finished transaction in 13.205 secs (13.203u,0.003s) (successful) *) + Time s. (* Finished transaction in 14.689 secs (14.686u,0.s) (successful) *) + Time s. (* Finished transaction in 10.672 secs (10.673u,0.s) (successful) *) + Time s. (* Finished transaction in 13.509 secs (13.509u,0.s) (successful) *) + Time s. (* Finished transaction in 1.389 secs (1.386u,0.003s) (successful) *) + Time s. (* Finished transaction in 10.331 secs (10.329u,0.003s) (successful) *) + Time s. (* Finished transaction in 12.182 secs (12.176u,0.006s) (successful) *) + Time s. (* Finished transaction in 9.826 secs (9.829u,0.s) (successful) *) + Time s. (* Finished transaction in 13.709 secs (13.703u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.059 secs (1.06u,0.s) (successful) *) + Time s. (* Finished transaction in 1.894 secs (1.896u,0.s) (successful) *) + Time s. (* Finished transaction in 1.358 secs (1.356u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.537 secs (1.536u,0.s) (successful) *) + Time s. (* Finished transaction in 1.342 secs (1.343u,0.s) (successful) *) + Time s. (* Finished transaction in 1.095 secs (1.096u,0.s) (successful) *) + Time s. (* Finished transaction in 1.157 secs (1.153u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.603 secs (1.603u,0.s) (successful) *) + Time s. (* Finished transaction in 6.196 secs (6.196u,0.s) (successful) *) + Time s. (* Finished transaction in 6.949 secs (6.949u,0.s) (successful) *) + Time s. (* Finished transaction in 4.685 secs (4.68u,0.006s) (successful) *) + Time s. (* Finished transaction in 6.483 secs (6.483u,0.s) (successful) *) + Time s. (* Finished transaction in 1.451 secs (1.453u,0.s) (successful) *) + Time s. (* Finished transaction in 13.648 secs (13.646u,0.s) (successful) *) + Time s. (* Finished transaction in 18.053 secs (18.056u,0.s) (successful) *) + Time s. (* Finished transaction in 7.186 secs (7.186u,0.s) (successful) *) + Time s. (* Finished transaction in 8.817 secs (8.819u,0.s) (successful) *) + Time s. (* Finished transaction in 1.251 secs (1.25u,0.s) (successful) *) + Time s. (* Finished transaction in 1.569 secs (1.569u,0.s) (successful) *) + Time s. (* Finished transaction in 1.356 secs (1.356u,0.s) (successful) *) + Time s. (* Finished transaction in 11.45 secs (11.446u,0.003s) (successful) *) + Time s. (* Finished transaction in 17.968 secs (17.969u,0.003s) (successful) *) + Time s. (* Finished transaction in 12.418 secs (12.366u,0.046s) (successful) *) + Time s. (* Finished transaction in 15.323 secs (15.316u,0.01s) (successful) *) + Time s. (* Finished transaction in 1.589 secs (1.586u,0.003s) (successful) *) + Time s. (* Finished transaction in 10.22 secs (10.223u,0.s) (successful) *) + Time s. (* Finished transaction in 11.887 secs (11.889u,0.s) (successful) *) + Time s. (* Finished transaction in 7.284 secs (7.283u,0.003s) (successful) *) + Time s. (* Finished transaction in 8.75 secs (8.753u,0.s) (successful) *) + Time s. (* Finished transaction in 0.291 secs (0.29u,0.s) (successful) *) + Time s. (* Finished transaction in 0.348 secs (0.346u,0.s) (successful) *) + Time s. (* Finished transaction in 0.222 secs (0.223u,0.s) (successful) *) + Time s. (* Finished transaction in 0.266 secs (0.266u,0.s) (successful) *) + Time s. (* Finished transaction in 0.296 secs (0.296u,0.s) (successful) *) + Time s. (* Finished transaction in 0.737 secs (0.736u,0.s) (successful) *) + Time s. (* Finished transaction in 0.227 secs (0.226u,0.s) (successful) *) + Time s. (* Finished transaction in 0.269 secs (0.269u,0.s) (successful) *) + Time s. (* Finished transaction in 0.054 secs (0.056u,0.s) (successful) *) + Time s. (* Finished transaction in 0.057 secs (0.056u,0.s) (successful) *) + Time s. (* Finished transaction in 0.308 secs (0.309u,0.s) (successful) *) + Time s. (* Finished transaction in 0.362 secs (0.363u,0.s) (successful) *) + Time s. (* Finished transaction in 0.226 secs (0.226u,0.s) (successful) *) + Time s. (* Finished transaction in 0.279 secs (0.279u,0.s) (successful) *) + Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.057 secs (0.06u,0.s) (successful) *) + Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.052 secs (0.049u,0.s) (successful) *) + Time s. (* Finished transaction in 0.053 secs (0.056u,0.s) (successful) *) + Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.2 secs (0.203u,0.s) (successful) *) + Time s. (* Finished transaction in 0.21 secs (0.21u,0.s) (successful) *) + Time s. (* Finished transaction in 0.208 secs (0.206u,0.s) (successful) *) + Time s. (* Finished transaction in 1.162 secs (1.163u,0.s) (successful) *) + Time s. (* Finished transaction in 1.256 secs (1.256u,0.s) (successful) *) + Time s. (* Finished transaction in 0.994 secs (0.996u,0.s) (successful) *) + Time s. (* Finished transaction in 1.017 secs (1.016u,0.s) (successful) *) + Time s. (* Finished transaction in 0.186 secs (0.186u,0.s) (successful) *) + Time s. (* Finished transaction in 1.044 secs (1.043u,0.s) (successful) *) + Time s. (* Finished transaction in 1.123 secs (1.123u,0.s) (successful) *) + Time s. (* Finished transaction in 0.892 secs (0.889u,0.s) (successful) *) + Time s. (* Finished transaction in 0.961 secs (0.963u,0.s) (successful) *) + Time s. (* Finished transaction in 0.051 secs (0.05u,0.s) (successful) *) + Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.085 secs (0.086u,0.s) (successful) *) + Time s. (* Finished transaction in 0.081 secs (0.08u,0.s) (successful) *) + Time s. (* Finished transaction in 0.12 secs (0.119u,0.s) (successful) *) + Time s. (* Finished transaction in 0.116 secs (0.12u,0.s) (successful) *) + Time s. (* Finished transaction in 0.074 secs (0.073u,0.s) (successful) *) + Time s. (* Finished transaction in 0.067 secs (0.066u,0.s) (successful) *) + Time s. (* Finished transaction in 0.07 secs (0.073u,0.s) (successful) *) + Time s. (* Finished transaction in 0.063 secs (0.063u,0.s) (successful) *) + Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *) + Time s. (* Finished transaction in 0.084 secs (0.083u,0.s) (successful) *) + Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *) + Time s. (* Finished transaction in 0.097 secs (0.096u,0.s) (successful) *) + Time s. (* Finished transaction in 0.108 secs (0.106u,0.s) (successful) *) + Time s. (* Finished transaction in 0.658 secs (0.66u,0.s) (successful) *) + Time s. (* Finished transaction in 0.775 secs (0.773u,0.s) (successful) *) + Time s. (* Finished transaction in 0.527 secs (0.526u,0.s) (successful) *) + Time s. (* Finished transaction in 0.625 secs (0.623u,0.003s) (successful) *) + Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *) + Time s. (* Finished transaction in 0.586 secs (0.586u,0.s) (successful) *) + Time s. (* Finished transaction in 0.687 secs (0.686u,0.s) (successful) *) + Time s. (* Finished transaction in 0.189 secs (0.189u,0.s) (successful) *) + Time s. (* Finished transaction in 0.21 secs (0.209u,0.s) (successful) *) + Time s. (* Finished transaction in 0.066 secs (0.066u,0.s) (successful) *) + Time s. (* Finished transaction in 0.078 secs (0.08u,0.s) (successful) *) + Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *) + Time s. (* Finished transaction in 0.068 secs (0.066u,0.s) (successful) *) + (* Total: 414.396 seconds, roughly 7 minutes*) + + Time Qed. End W. End W. |