fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	use improved fsatz on various elliptic curve things	Andres Erbsen	2017-03-31
\| \| \| \| \| \| \| \|	partial correctness of projective addition stronger projective addition proof fixup
*	make fsatz recurse when proving nonzero-ness, undo Weierstrass workaround	Andres Erbsen	2017-03-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ----------------------------------------------------------------------------------------------------------- 29m00.03s \| Total \| 33m00.88s \|\| -4m00.84s ----------------------------------------------------------------------------------------------------------- 11m48.99s \| WeierstrassCurve/WeierstrassCurveTheorems \| 16m37.07s \|\| -4m00.08s 1m46.82s \| Test/Curve25519SpecTestVectors \| 1m47.06s \|\| -0m00.24s 1m18.46s \| Spec/MontgomeryCurve \| 0m43.03s \|\| +0m00.43s 0m50.03s \| Specific/GF25519Reflective/Reified/LadderStep \| 0m50.00s \|\| +0m00.03s 0m43.21s \| Spec/Ed25519 \| 0m42.48s \|\| +0m00.73s 0m37.78s \| ModularArithmetic/Conversion \| 0m40.14s \|\| -0m00.35s 0m34.92s \| Specific/GF25519Reflective/Reified/AddCoordinates \| 0m36.07s \|\| -0m00.14s 0m32.14s \| Specific/GF25519Bounded \| 0m31.64s \|\| +0m00.50s 0m29.53s \| ModularArithmetic/ModularBaseSystemProofs \| 0m29.72s \|\| -0m00.18s 0m24.83s \| Reflection/Z/Interpretations128/Relations \| 0m23.35s \|\| +0m00.47s 0m23.51s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m23.57s \|\| -0m00.05s 0m20.51s \| ModularArithmetic/Pow2BaseProofs \| 0m22.19s \|\| -0m00.67s 0m20.13s \| Specific/GF25519 \| 0m22.72s \|\| -0m00.58s 0m19.08s \| Reflection/Named/MapCastWf \| 0m19.60s \|\| -0m00.52s 0m18.74s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m17.30s \|\| +0m00.43s 0m18.47s \| Reflection/Z/Interpretations64/Relations \| 0m19.28s \|\| -0m00.81s 0m18.12s \| EdDSARepChange \| 0m18.55s \|\| -0m00.42s 0m14.69s \| Util/ZUtil \| 0m15.19s \|\| -0m00.50s 0m13.86s \| Reflection/Named/ContextProperties/SmartMap \| 0m14.23s \|\| -0m00.37s 0m13.65s \| Reflection/Named/ContextProperties/NameUtil \| 0m15.92s \|\| -0m00.26s 0m11.98s \| Specific/GF25519Reflective/Reified/Mul \| 0m12.53s \|\| -0m00.54s 0m11.84s \| Experiments/Ed25519 \| 0m11.87s \|\| -0m00.02s 0m11.64s \| Specific/NewBaseSystemTest \| 0m11.70s \|\| -0m00.05s 0m11.28s \| Algebra/Field \| 0m11.55s \|\| -0m00.27s 0m09.04s \| Reflection/Named/MapCastInterp \| 0m09.25s \|\| -0m00.21s 0m09.02s \| Assembly/GF25519 \| 0m09.52s \|\| -0m00.50s 0m08.92s \| Specific/GF25519BoundedCommon \| 0m08.75s \|\| +0m00.16s 0m08.88s \| Testbit \| 0m10.14s \|\| -0m00.25s 0m08.25s \| BoundedArithmetic/Double/Proofs/Multiply \| 0m08.14s \|\| +0m00.10s 0m08.16s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.50s \|\| -0m00.33s 0m08.02s \| BoundedArithmetic/ArchitectureToZLikeProofs \| 0m08.18s \|\| -0m00.16s 0m07.94s \| Reflection/InlineWf \| 0m08.34s \|\| -0m00.39s 0m07.48s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate \| 0m06.54s \|\| +0m00.94s 0m07.47s \| Algebra/Ring \| 0m07.50s \|\| -0m00.03s 0m07.41s \| BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate \| 0m07.65s \|\| -0m00.24s 0m07.10s \| MxDHRepChange \| 0m07.48s \|\| -0m00.38s 0m06.48s \| Specific/GF1305 \| 0m06.40s \|\| +0m00.08s 0m06.33s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub \| 0m05.14s \|\| +0m00.19s 0m06.27s \| Reflection/Z/InterpretationsGen \| 0m06.42s \|\| -0m00.15s 0m06.01s \| Specific/GF25519Reflective/Reified/PreFreeze \| 0m05.91s \|\| +0m00.09s 0m05.96s \| Bedrock/Word \| 0m05.77s \|\| +0m00.19s 0m05.90s \| NewBaseSystem \| 0m06.06s \|\| -0m00.15s 0m05.76s \| Util/FixedWordSizesEquality \| 0m05.98s \|\| -0m00.22s 0m05.49s \| Specific/GF25519Reflective/Reified/CarrySub \| 0m05.42s \|\| +0m00.07s 0m05.38s \| CompleteEdwardsCurve/Pre \| 0m04.22s \|\| +0m00.16s 0m05.17s \| Specific/SC25519 \| 0m05.31s \|\| -0m00.13s 0m05.08s \| Util/ListUtil \| 0m05.16s \|\| -0m00.08s 0m05.04s \| Experiments/GenericFieldPow \| 0m05.20s \|\| -0m00.16s 0m05.01s \| Specific/GF25519Reflective/Reified/CarryAdd \| 0m05.04s \|\| -0m00.03s 0m04.98s \| Specific/GF25519Reflective/CommonBinOp \| 0m05.18s \|\| -0m00.19s 0m04.75s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m04.81s \|\| -0m00.05s 0m04.59s \| Algebra/Field_test \| 0m12.12s \|\| -0m00.52s 0m04.48s \| Reflection/InlineCastWf \| 0m04.72s \|\| -0m00.23s 0m03.97s \| Specific/GF25519Reflective/CommonUnOp \| 0m04.16s \|\| -0m00.18s 0m03.97s \| Specific/GF25519Reflective/Common9_4Op \| 0m04.11s \|\| -0m00.14s 0m03.96s \| Specific/GF25519Reflective/CommonUnOpWireToFE \| 0m03.91s \|\| +0m00.04s 0m03.70s \| Specific/GF25519Reflective/Reified/CarryOpp \| 0m03.73s \|\| -0m00.02s 0m03.53s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.71s \|\| -0m00.18s 0m03.51s \| BaseSystemProofs \| 0m03.52s \|\| -0m00.01s 0m03.39s \| Reflection/EtaWf \| 0m03.45s \|\| -0m00.06s 0m03.37s \| Reflection/Named/CompileWf \| 0m03.81s \|\| -0m00.43s 0m03.34s \| Specific/GF25519Reflective/Reified/Sub \| 0m03.47s \|\| -0m00.13s 0m03.16s \| BoundedArithmetic/InterfaceProofs \| 0m03.14s \|\| +0m00.02s 0m02.99s \| Reflection/LinearizeWf \| 0m03.09s \|\| -0m00.09s 0m02.90s \| Specific/GF25519Reflective/Reified/Add \| 0m03.02s \|\| -0m00.12s 0m02.84s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m02.88s \|\| -0m00.04s 0m02.79s \| Specific/FancyMachine256/Montgomery \| 0m02.77s \|\| +0m00.02s 0m02.77s \| ModularArithmetic/ZBoundedZ \| 0m02.91s \|\| -0m00.14s 0m02.74s \| Reflection/Named/CompileInterp \| 0m03.65s \|\| -0m00.90s 0m02.68s \| BoundedArithmetic/Double/Proofs/Decode \| 0m02.62s \|\| +0m00.06s 0m02.68s \| Specific/GF25519Reflective/CommonUnOpFEToWire \| 0m02.72s \|\| -0m00.04s 0m02.63s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.65s \|\| -0m00.02s 0m02.62s \| Specific/FancyMachine256/Barrett \| 0m02.58s \|\| +0m00.04s 0m02.58s \| Specific/GF25519Reflective/Reified/Pack \| 0m02.56s \|\| +0m00.02s 0m02.54s \| Reflection/InlineInterp \| 0m02.53s \|\| +0m00.01s 0m02.46s \| BoundedArithmetic/Double/Proofs/ShiftRight \| 0m02.52s \|\| -0m00.06s 0m02.42s \| Specific/GF25519Reflective/Reified/Unpack \| 0m02.42s \|\| +0m00.00s 0m02.40s \| Specific/GF25519ReflectiveAddCoordinates \| 0m02.33s \|\| +0m00.06s 0m02.39s \| Reflection/Named/ContextProperties \| 0m02.42s \|\| -0m00.02s 0m02.38s \| BoundedArithmetic/Double/Proofs/ShiftLeft \| 0m02.40s \|\| -0m00.02s 0m02.34s \| Assembly/State \| 0m02.44s \|\| -0m00.10s 0m02.22s \| Specific/GF25519Reflective/Reified/Opp \| 0m02.23s \|\| -0m00.00s 0m02.22s \| Reflection/Named/NameUtilProperties \| 0m02.31s \|\| -0m00.08s 0m02.18s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.19s \|\| -0m00.00s 0m02.16s \| Reflection/WfProofs \| 0m02.15s \|\| +0m00.01s 0m02.14s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.19s \|\| -0m00.04s 0m02.12s \| Reflection/TestCase \| 0m02.23s \|\| -0m00.10s 0m01.99s \| Specific/GF25519Reflective/Reified/GeModulus \| 0m01.96s \|\| +0m00.03s 0m01.90s \| WeierstrassCurve/Pre \| 0m01.55s \|\| +0m00.34s 0m01.87s \| Reflection/WfReflective \| 0m01.83s \|\| +0m00.04s 0m01.79s \| Util/WordUtil \| 0m01.82s \|\| -0m00.03s 0m01.76s \| Specific/FancyMachine256/Core \| 0m01.75s \|\| +0m00.01s 0m01.71s \| SaturatedBaseSystem \| 0m01.92s \|\| -0m00.20s 0m01.68s \| Algebra/Group \| 0m01.72s \|\| -0m00.04s 0m01.67s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.68s \|\| -0m00.01s 0m01.63s \| Assembly/Evaluables \| 0m01.68s \|\| -0m00.05s 0m01.45s \| Specific/GF25519Reflective/Common \| 0m01.39s \|\| +0m00.06s 0m01.43s \| Reflection/Z/Interpretations128/RelationsCombinations \| 0m01.16s \|\| +0m00.27s 0m01.42s \| Reflection/Named/InterpretToPHOASWf \| 0m01.51s \|\| -0m00.09s 0m01.32s \| Util/NatUtil \| 0m01.32s \|\| +0m00.00s 0m01.30s \| Util/Tuple \| 0m01.30s \|\| +0m00.00s 0m01.30s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.29s \|\| +0m00.01s 0m01.30s \| Assembly/WordizeUtil \| 0m01.46s \|\| -0m00.15s 0m01.30s \| ModularArithmetic/BarrettReduction/Z \| 0m01.34s \|\| -0m00.04s 0m01.30s \| Reflection/MapCastInterp \| 0m01.30s \|\| +0m00.00s 0m01.26s \| Specific/GF25519Reflective \| 0m01.30s \|\| -0m00.04s 0m01.22s \| Assembly/Compile \| 0m01.26s \|\| -0m00.04s 0m01.21s \| Reflection/Z/Interpretations64/RelationsCombinations \| 0m01.19s \|\| +0m00.02s 0m01.20s \| Reflection/Z/Syntax/Equality \| 0m01.17s \|\| +0m00.03s 0m01.18s \| Assembly/Bounds \| 0m01.35s \|\| -0m00.17s 0m01.06s \| BaseSystem \| 0m01.05s \|\| +0m00.01s 0m01.01s \| Experiments/Ed25519Extraction \| 0m00.98s \|\| +0m00.03s 0m01.00s \| Reflection/SmartBoundInterp \| 0m01.02s \|\| -0m00.02s 0m00.99s \| BoundedArithmetic/Double/Repeated/Proofs/Decode \| 0m01.02s \|\| -0m00.03s 0m00.99s \| Reflection/Relations \| 0m00.96s \|\| +0m00.03s 0m00.96s \| ModularArithmetic/ExtendedBaseVector \| 0m01.03s \|\| -0m00.07s 0m00.89s \| Assembly/Conversions \| 0m00.89s \|\| +0m00.00s 0m00.89s \| Reflection/Named/InterpretToPHOASInterp \| 0m00.92s \|\| -0m00.03s 0m00.88s \| Reflection/SmartCastWf \| 0m00.89s \|\| -0m00.01s 0m00.84s \| Algebra/IntegralDomain \| 0m00.86s \|\| -0m00.02s 0m00.84s \| Reflection/InlineCastInterp \| 0m00.89s \|\| -0m00.05s 0m00.80s \| Specific/GF25519Reflective/CommonUnOpFEToZ \| 0m00.87s \|\| -0m00.06s 0m00.79s \| Util/NumTheoryUtil \| 0m00.94s \|\| -0m00.14s 0m00.78s \| BoundedArithmetic/Double/Proofs/BitwiseOr \| 0m00.76s \|\| +0m00.02s 0m00.76s \| Reflection/MapCastByDeBruijnInterp \| 0m00.72s \|\| +0m00.04s 0m00.75s \| BoundedArithmetic/Double/Proofs/LoadImmediate \| 0m00.76s \|\| -0m00.01s 0m00.74s \| BoundedArithmetic/X86ToZLikeProofs \| 0m00.73s \|\| +0m00.01s 0m00.74s \| Reflection/WfInversion \| 0m00.78s \|\| -0m00.04s 0m00.73s \| Reflection/Named/CompileProperties \| 0m00.77s \|\| -0m00.04s 0m00.71s \| Assembly/LL \| 0m00.73s \|\| -0m00.02s 0m00.69s \| Assembly/Pipeline \| 0m00.69s \|\| +0m00.00s 0m00.69s \| Util/IterAssocOp \| 0m00.74s \|\| -0m00.05s 0m00.68s \| Assembly/HL \| 0m00.70s \|\| -0m00.01s 0m00.68s \| Util/PartiallyReifiedProp \| 0m00.70s \|\| -0m00.01s 0m00.67s \| Karatsuba \| 0m00.71s \|\| -0m00.03s 0m00.67s \| Assembly/QhasmEvalCommon \| 0m00.67s \|\| +0m00.00s 0m00.66s \| Specific/GF25519BoundedAddCoordinates \| 0m00.63s \|\| +0m00.03s 0m00.65s \| Assembly/PhoasCommon \| 0m00.62s \|\| +0m00.03s 0m00.62s \| Specific/GF25519Reflective/Reified \| 0m00.62s \|\| +0m00.00s 0m00.62s \| Reflection/MultiSizeTest \| 0m00.65s \|\| -0m00.03s 0m00.58s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.58s \|\| +0m00.00s 0m00.58s \| Reflection/MapCastByDeBruijnWf \| 0m00.57s \|\| +0m00.01s 0m00.58s \| Spec/WeierstrassCurve \| 0m00.48s \|\| +0m00.09s 0m00.55s \| Encoding/ModularWordEncodingTheorems \| 0m00.58s \|\| -0m00.02s 0m00.54s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.53s \|\| +0m00.01s 0m00.53s \| Spec/EdDSA \| 0m00.53s \|\| +0m00.00s 0m00.53s \| Util/AdditionChainExponentiation \| 0m00.56s \|\| -0m00.03s 0m00.53s \| BoundedArithmetic/Double/Repeated/Proofs/Multiply \| 0m00.53s \|\| +0m00.00s 0m00.52s \| Reflection/InterpByIsoProofs \| 0m00.53s \|\| -0m00.01s 0m00.52s \| Reflection/Named/WfInterp \| 0m00.52s \|\| +0m00.00s 0m00.51s \| ModularArithmetic/ModularBaseSystemList \| 0m00.51s \|\| +0m00.00s 0m00.51s \| BoundedArithmetic/Interface \| 0m00.51s \|\| +0m00.00s 0m00.51s \| BoundedArithmetic/X86ToZLike \| 0m00.53s \|\| -0m00.02s 0m00.51s \| Encoding/ModularWordEncodingPre \| 0m00.53s \|\| -0m00.02s 0m00.51s \| Reflection/WfReflectiveGen \| 0m00.48s \|\| +0m00.03s 0m00.50s \| ModularArithmetic/ModularBaseSystem \| 0m00.54s \|\| -0m00.04s 0m00.50s \| Reflection/Named/FMapContext \| 0m00.52s \|\| -0m00.02s 0m00.49s \| BoundedArithmetic/Double/Proofs/SelectConditional \| 0m00.48s \|\| +0m00.01s 0m00.48s \| Spec/ModularWordEncoding \| 0m00.50s \|\| -0m00.02s 0m00.47s \| Spec/CompleteEdwardsCurve \| 0m00.48s \|\| -0m00.01s 0m00.47s \| Assembly/StringConversion \| 0m00.42s \|\| +0m00.04s 0m00.47s \| Reflection/InterpWfRel \| 0m00.47s \|\| +0m00.00s 0m00.47s \| Reflection/BoundByCastInterp \| 0m00.45s \|\| +0m00.01s 0m00.46s \| Util/CPSUtil \| 0m00.51s \|\| -0m00.04s 0m00.45s \| Algebra/ScalarMult \| 0m00.47s \|\| -0m00.01s 0m00.44s \| Util/Decidable \| 0m00.43s \|\| +0m00.01s 0m00.44s \| BoundedArithmetic/Double/Core \| 0m00.41s \|\| +0m00.03s 0m00.44s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub \| 0m00.42s \|\| +0m00.02s 0m00.44s \| Reflection/SmartBoundWf \| 0m00.45s \|\| -0m00.01s 0m00.43s \| BoundedArithmetic/Double/Repeated/Core \| 0m00.43s \|\| +0m00.00s 0m00.43s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight \| 0m00.44s \|\| -0m00.01s 0m00.43s \| Util/HList \| 0m00.43s \|\| +0m00.00s 0m00.43s \| Reflection/InputSyntax \| 0m00.42s \|\| +0m00.01s 0m00.42s \| Algebra/Monoid \| 0m00.46s \|\| -0m00.04s 0m00.42s \| Assembly/Qhasm \| 0m00.43s \|\| -0m00.01s 0m00.42s \| Util/NUtil \| 0m00.43s \|\| -0m00.01s 0m00.41s \| ModularArithmetic/ZBounded \| 0m00.40s \|\| +0m00.00s 0m00.41s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate \| 0m00.39s \|\| +0m00.01s 0m00.41s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional \| 0m00.41s \|\| +0m00.00s 0m00.41s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate \| 0m00.42s \|\| -0m00.01s 0m00.41s \| Reflection/Named/PositiveContext/DefaultsProperties \| 0m00.36s \|\| +0m00.04s 0m00.40s \| ModularArithmetic/Pre \| 0m00.43s \|\| -0m00.02s 0m00.40s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr \| 0m00.44s \|\| -0m00.03s 0m00.40s \| Reflection/Z/Interpretations64 \| 0m00.40s \|\| +0m00.00s 0m00.40s \| Reflection/Z/Reify \| 0m00.40s \|\| +0m00.00s 0m00.40s \| Reflection/InterpWf \| 0m00.41s \|\| -0m00.00s 0m00.39s \| BoundedArithmetic/ArchitectureToZLike \| 0m00.41s \|\| -0m00.01s 0m00.39s \| BoundedArithmetic/StripCF \| 0m00.41s \|\| -0m00.01s 0m00.39s \| BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic \| 0m00.39s \|\| +0m00.00s 0m00.39s \| Reflection/Z/BoundsInterpretations \| 0m00.38s \|\| +0m00.01s 0m00.39s \| Reflection/Z/Interpretations128 \| 0m00.41s \|\| -0m00.01s 0m00.38s \| Algebra \| 0m00.35s \|\| +0m00.03s 0m00.38s \| Reflection/Z/Syntax \| 0m00.37s \|\| +0m00.01s 0m00.38s \| Reflection/Z/Syntax/Util \| 0m00.35s \|\| +0m00.03s 0m00.36s \| Reflection/MapCastByDeBruijn \| 0m00.35s \|\| +0m00.01s 0m00.35s \| ModularArithmetic/ModularBaseSystemListZOperations \| 0m00.33s \|\| +0m00.01s 0m00.35s \| ModularArithmetic/ModularBaseSystemListZOperationsProofs \| 0m00.34s \|\| +0m00.00s 0m00.35s \| Reflection/Z/HexNotationConstants \| 0m00.35s \|\| +0m00.00s 0m00.34s \| Spec/MxDH \| 0m00.34s \|\| +0m00.00s 0m00.34s \| ModularArithmetic/Pow2Base \| 0m00.39s \|\| -0m00.04s 0m00.34s \| Assembly/QhasmUtil \| 0m00.36s \|\| -0m00.01s 0m00.34s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.42s \|\| -0m00.07s 0m00.34s \| ModularArithmetic/Montgomery/Z \| 0m00.33s \|\| +0m00.01s 0m00.34s \| Reflection/Named/PositiveContext/Defaults \| 0m00.33s \|\| +0m00.01s 0m00.34s \| Reflection/Named/RegisterAssign \| 0m00.36s \|\| -0m00.01s 0m00.34s \| Reflection/Named/DeadCodeElimination \| 0m00.35s \|\| -0m00.00s 0m00.33s \| BoundedArithmetic/Eta \| 0m00.37s \|\| -0m00.03s 0m00.33s \| Reflection/Tuple \| 0m00.33s \|\| +0m00.00s 0m00.33s \| ModularArithmetic/ModularBaseSystemWord \| 0m00.32s \|\| +0m00.01s 0m00.33s \| Reflection/Named/Syntax \| 0m00.35s \|\| -0m00.01s 0m00.33s \| Reflection/Z/CNotations \| 0m00.34s \|\| -0m00.01s 0m00.32s \| Tactics/Algebra_syntax/Nsatz \| 0m00.34s \|\| -0m00.02s 0m00.32s \| Reflection/Reify \| 0m00.34s \|\| -0m00.02s 0m00.32s \| Reflection/Named/MapCast \| 0m00.32s \|\| +0m00.00s 0m00.32s \| Reflection/Named/Wf \| 0m00.30s \|\| +0m00.02s 0m00.32s \| Reflection/Named/Compile \| 0m00.30s \|\| +0m00.02s 0m00.32s \| Reflection/Named/PositiveContext \| 0m00.33s \|\| -0m00.01s 0m00.32s \| Reflection/Named/ContextProperties/Tactics \| 0m00.30s \|\| +0m00.02s 0m00.32s \| Reflection/Named/IdContext \| 0m00.31s \|\| +0m00.01s 0m00.32s \| Reflection/Z/BinaryNotationConstants \| 0m00.31s \|\| +0m00.01s 0m00.32s \| Reflection/Z/FoldTypes \| 0m00.34s \|\| -0m00.02s 0m00.32s \| Reflection/Z/JavaNotations \| 0m00.32s \|\| +0m00.00s 0m00.31s \| Util/Factorize \| 0m00.32s \|\| -0m00.01s 0m00.31s \| Reflection/Named/EstablishLiveness \| 0m00.32s \|\| -0m00.01s 0m00.31s \| Reflection/Named/SmartMap \| 0m00.32s \|\| -0m00.01s 0m00.30s \| Reflection/Named/InterpretToPHOAS \| 0m00.29s \|\| +0m00.01s 0m00.29s \| Spec/ModularArithmetic \| 0m00.34s \|\| -0m00.05s 0m00.29s \| Reflection/FilterLive \| 0m00.29s \|\| +0m00.00s 0m00.29s \| Reflection/Named/ContextDefinitions \| 0m00.33s \|\| -0m00.04s 0m00.29s \| Reflection/MultiSizeTest2 \| 0m00.30s \|\| -0m00.01s 0m00.28s \| Reflection/Named/ContextOn \| 0m00.31s \|\| -0m00.02s 0m00.27s \| Bedrock/Nomega \| 0m00.26s \|\| +0m00.01s 0m00.27s \| Util/FixedWordSizes \| 0m00.28s \|\| -0m00.01s 0m00.27s \| Reflection/Z/OpInversion \| 0m00.31s \|\| -0m00.03s 0m00.26s \| Reflection/MapCastWf \| 0m00.29s \|\| -0m00.02s 0m00.25s \| Reflection/ExprInversion \| 0m00.26s \|\| -0m00.01s 0m00.24s \| Assembly/QhasmCommon \| 0m00.26s \|\| -0m00.02s 0m00.23s \| Reflection/Equality \| 0m00.23s \|\| +0m00.00s 0m00.22s \| Util/Sum \| 0m00.22s \|\| +0m00.00s 0m00.21s \| Reflection/SmartMap \| 0m00.23s \|\| -0m00.02s 0m00.19s \| Util/CaseUtil \| 0m00.18s \|\| +0m00.01s 0m00.19s \| Reflection/LinearizeInterp \| 0m00.22s \|\| -0m00.03s 0m00.18s \| Util/LetInMonad \| 0m00.16s \|\| +0m00.01s 0m00.17s \| Reflection/EtaInterp \| 0m00.17s \|\| +0m00.00s 0m00.17s \| Reflection/CommonSubexpressionElimination \| 0m00.16s \|\| +0m00.01s 0m00.16s \| Reflection/InterpProofs \| 0m00.17s \|\| -0m00.01s 0m00.16s \| Experiments/ExtrHaskellNats \| 0m00.16s \|\| +0m00.00s 0m00.13s \| Reflection/Wf \| 0m00.11s \|\| +0m00.02s 0m00.11s \| Reflection/BoundByCastWf \| 0m00.11s \|\| +0m00.00s 0m00.11s \| Reflection/Named/NameUtil \| 0m00.10s \|\| +0m00.00s 0m00.10s \| Util/Option \| 0m00.12s \|\| -0m00.01s 0m00.09s \| Util/Sigma \| 0m00.08s \|\| +0m00.00s 0m00.09s \| Util/Relations \| 0m00.09s \|\| +0m00.00s 0m00.08s \| Reflection/Conversion \| 0m00.09s \|\| -0m00.00s 0m00.08s \| Util/PointedProp \| 0m00.08s \|\| +0m00.00s 0m00.07s \| Util/Prod \| 0m00.07s \|\| +0m00.00s 0m00.07s \| Reflection/TypeInversion \| 0m00.08s \|\| -0m00.00s 0m00.06s \| Util/Equality \| 0m00.06s \|\| +0m00.00s 0m00.05s \| Util/Tactics \| 0m00.04s \|\| +0m00.01s 0m00.05s \| Reflection/Inline \| 0m00.06s \|\| -0m00.00s 0m00.05s \| Reflection/SmartBound \| 0m00.07s \|\| -0m00.02s 0m00.05s \| Reflection/MapCast \| 0m00.05s \|\| +0m00.00s 0m00.05s \| Reflection/BoundByCast \| 0m00.05s \|\| +0m00.00s 0m00.04s \| Util/HProp \| 0m00.03s \|\| +0m00.01s 0m00.04s \| Util/Tactics/DestructHyps \| 0m00.01s \|\| +0m00.03s 0m00.04s \| Util/Bool \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Util/LetIn \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Reflection/Syntax \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Reflection/Eta \| 0m00.06s \|\| -0m00.01s 0m00.04s \| Reflection/Linearize \| 0m00.03s \|\| +0m00.01s 0m00.04s \| Reflection/InlineCast \| 0m00.06s \|\| -0m00.01s 0m00.04s \| Reflection/SmartCastInterp \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Reflection/CountLets \| 0m00.03s \|\| +0m00.01s 0m00.04s \| Reflection/FoldTypes \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Reflection/InterpByIso \| 0m00.04s \|\| +0m00.00s 0m00.03s \| Util/GlobalSettings \| 0m00.02s \|\| +0m00.00s 0m00.03s \| Util/Tactics/DoWithHyp \| 0m00.02s \|\| +0m00.00s 0m00.03s \| Util/Tactics/SpecializeBy \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Util/Tactics/UniquePose \| 0m00.02s \|\| +0m00.00s 0m00.03s \| Util/Logic \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Util/IffT \| 0m00.04s \|\| -0m00.01s 0m00.03s \| Reflection/Map \| 0m00.02s \|\| +0m00.00s 0m00.03s \| Reflection/TypeUtil \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Reflection/SmartCast \| 0m00.04s \|\| -0m00.01s 0m00.03s \| Util/Sumbool \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Util/Unit \| 0m00.03s \|\| +0m00.00s 0m00.02s \| Util/FixCoqMistakes \| 0m00.01s \|\| +0m00.01s 0m00.02s \| Util/Isomorphism \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/Tactics/Head \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/Tactics/BreakMatch \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Util/Tactics/RewriteHyp \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/Tactics/SplitInContext \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/Tactics/VM \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/Notations \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Tactics/VerdiTactics \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Util/Tower \| 0m00.04s \|\| -0m00.02s 0m00.02s \| Util/AutoRewrite \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Spec/Encoding \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Encoding/EncodingTheorems \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Util/Curry \| 0m00.01s \|\| +0m00.01s 0m00.01s \| Util/Tactics/DestructHead \| 0m00.02s \|\| -0m00.01s
*	CompleteEdwardsCurveTheorems: point compression	Andres Erbsen	2017-03-02
\|
*	use [positive] for [F] modulus, char_ge_C instead of char_gt_C	Andres Erbsen	2017-03-02
\|
*	rewrite ExtendedCoordinates, fix Ed25519	Andres Erbsen	2017-03-02
\|
*	edwards curves over isomorphic fields	Andres Erbsen	2017-03-02
\|
*	WIP	Andres Erbsen	2017-03-02
\|
*	split the algebra library; use fsatz more	Andres Erbsen	2017-03-02
\|
*	fsatz, nsatz_solve_nonzero	Andres Erbsen	2017-03-02
\|
*	use field_nsatz in CompleteEdwardsCurve.Pre	Andres Erbsen	2017-03-02
\|
*	Fix for 8.6	Jason Gross	2016-11-22
\|
*	Fix for Coq 8.4	Jason Gross	2016-11-21
\|
*	Add add_coordinates_respectful_hetero	Jason Gross	2016-11-17
\|
*	Generalize add_coordinates	Jason Gross	2016-11-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is in preparation for dropping extra carries. What remains to be done, after this and #106, is to finish packaging up the reified [add_coordinates] so that it can operate on [Tuple.tuple GF25519BoundedCommon.fe25519 4], and then to prove ```coq forall twice_d P1 P2, Tuple.fieldwise GF25519BoundedCommon.eq (<reflected add_coordinates> twice_d P1 P2) (@ExtendedCoordinates.Extended.add_coordinates GF25519BoundedCommon.fe25519 GF25519Bounded.add GF25519Bounded.sub GF25519Bounded.mul twice_d P1 P2) ``` I'm not sure how to do this, or even what the right structure for the proof is.
*	Add add_coordinates_gen	Jason Gross	2016-11-16
\| \| \| \|	This in preparation for reifying add_coordinates
*	framework for l_order_B	Andres Erbsen	2016-10-30
\|
*	CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism ↵	Andres Erbsen	2016-10-27
\| \| \| \|	lemma that did not turn out to be necessary
*	fiddle with [rewrite <-!(field_div_definition)], maybe fix build	Andres Erbsen	2016-10-21
\|
*	Edwards.Extended.to_twisted: only one inversion, improve extraction	Andres Erbsen	2016-10-21
\|
*	Be more hesitant to [pose proof E.char_gt_2]	Jason Gross	2016-10-17
\| \| \| \|	This makes progress towards #75, #57, and compatiblity between versions of Coq
*	refactor scalar multiplication thoery, implement SRepERepMul	Andres Erbsen	2016-10-12
\|
*	remove eq_dec from Monoid	Andres Erbsen	2016-08-23
\|
*	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1
*	Move most notation level declarations into Util	Jason Gross	2016-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
*	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-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
*	proved an admit in field homomorphisms that turned out to be unprovable; I ↵	jadep	2016-07-15
\| \| \| \|	added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck.
*	s/conservative_common_denominator/common_denominator/g	Andres Erbsen	2016-07-11
\|
*	remove field_algebra	Andres Erbsen	2016-07-11
\|
*	port CompleteEdwardsCurveTheorems (builds again)	Andres Erbsen	2016-07-11
\|
*	pose proof fails where specialize works (typeclass resolution / unification?)	Andres Erbsen	2016-07-11
\|
*	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\|
*	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
\| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-06-27
\|\
\| *	scalarmult support; EdDSA.sign produces valid signatures	Andres Erbsen	2016-06-27
\| \|
* \|	update new lemma in CompleteEdwardsCurve/Pre to match other changes to that file	jadep	2016-06-25
\| \|
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_port	jadep	2016-06-24
\|\\|
* \|	merging point encoding port	jadep	2016-06-24
\|\ \
* \| \|	Ported PointEncodings to parameterize over field rather than modulus.	jadep	2016-06-24
\| \| \|
\| \| *	Remove a useless intro	Jason Gross	2016-06-24
\| \|/
\| *	ExtendedCoordinates: group.	Andres Erbsen	2016-06-24
\| \|
\| *	Use Decidable machinery for is_eq_dec	Jason Gross	2016-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows us to rely entirely on typeclass resolution to resolve these instances, without having to do ad-hoc things for [and]. After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 2m21.71s \| Total \| 2m22.59s \|\| -0m00.87s ------------------------------------------------------------------------------------ 0m28.82s \| Specific/GF25519 \| 0m29.86s \|\| -0m01.03s 0m29.60s \| ModularArithmetic/ModularBaseSystemProofs \| 0m29.40s \|\| +0m00.20s 0m21.25s \| Experiments/SpecEd25519 \| 0m21.28s \|\| -0m00.03s 0m18.15s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m18.14s \|\| +0m00.00s 0m11.95s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m11.94s \|\| +0m00.00s 0m07.26s \| Specific/GF1305 \| 0m07.28s \|\| -0m00.02s 0m03.77s \| ModularArithmetic/Tutorial \| 0m03.75s \|\| +0m00.02s 0m03.76s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.75s \|\| +0m00.00s 0m03.61s \| CompleteEdwardsCurve/Pre \| 0m03.63s \|\| -0m00.02s 0m02.15s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.12s \|\| +0m00.02s 0m01.88s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.89s \|\| -0m00.01s 0m01.75s \| Algebra \| 0m01.73s \|\| +0m00.02s 0m01.21s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.17s \|\| +0m00.04s 0m01.14s \| ModularArithmetic/ExtendedBaseVector \| 0m01.14s \|\| +0m00.00s 0m01.01s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.98s \|\| +0m00.03s 0m00.62s \| Encoding/ModularWordEncodingTheorems \| 0m00.63s \|\| -0m00.01s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.61s \|\| -0m00.01s 0m00.59s \| Util/Decidable \| 0m00.64s \|\| -0m00.05s 0m00.58s \| Spec/EdDSA \| 0m00.61s \|\| -0m00.03s 0m00.57s \| ModularArithmetic/ModularBaseSystem \| 0m00.61s \|\| -0m00.04s 0m00.56s \| Spec/ModularWordEncoding \| 0m00.56s \|\| +0m00.00s 0m00.51s \| ModularArithmetic/PseudoMersenneBaseRep \| 0m00.53s \|\| -0m00.02s 0m00.37s \| Spec/CompleteEdwardsCurve \| 0m00.34s \|\| +0m00.02s
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Pseudize Let_In	Robert Sloan	2016-06-23
\| \|
\| *	Fix broken notations (hopefully)	Jason Gross	2016-06-22
\| \|
\| *	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \| \| \|	This prevents notation conflicts (see comment in Notations.v for more explanation).
\| *	Use Admitted, not Qed, when a proof has admit	Jason Gross	2016-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[admit] is the same as [shelve] / [give_up] in Coq 8.5. Error: Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed. (in proof edwards_acurve_abelian_group)
\| *	Fix [Proper_add] in 8.5	Jason Gross	2016-06-21
\| \| \| \| \| \| \| \|	Not sure why eauto depth matters...
\| *	Make [bash] tactic easier to debug	Jason Gross	2016-06-21
\| \| \| \| \| \| \| \|	Now you don't have to copy/paste the [match goal with ... end].
\| *	use Local Obligation Tactic (8.5-compat)	Andres Erbsen	2016-06-21
\| \|
\| *	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\| \|