fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add Tuple.map_Proper	Jason Gross	2017-04-03
\|
*	Use a more robust way of saving context definitions in IntegrationTest	Jason Gross	2017-04-03
\|
*	Use dlet in MontgomeryX	Jason Gross	2017-04-03
\|
*	More fine-grained tactic imports	Jason Gross	2017-04-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Most files no longer import Crypto.Util.Tactics. We remove an unused lemma depending on classical axioms; closes #143. After \| File Name \| Before \|\| Change ----------------------------------------------------------------------------------------------------------- 28m38.18s \| Total \| 29m04.51s \|\| -0m26.32s ----------------------------------------------------------------------------------------------------------- 0m41.70s \| ModularArithmetic/ModularBaseSystemProofs \| 0m32.66s \|\| +0m09.04s 1m39.88s \| MontgomeryX \| 1m46.07s \|\| -0m06.18s 1m56.52s \| WeierstrassCurve/Projective \| 2m00.76s \|\| -0m04.23s 10m36.85s \| WeierstrassCurve/WeierstrassCurveTheorems \| 10m40.14s \|\| -0m03.28s 0m21.35s \| ModularArithmetic/Pow2BaseProofs \| 0m22.54s \|\| -0m01.18s 0m20.24s \| Reflection/Named/MapCastWf \| 0m21.41s \|\| -0m01.17s 1m30.28s \| Test/Curve25519SpecTestVectors \| 1m31.19s \|\| -0m00.90s 0m49.53s \| Specific/IntegrationTest \| 0m50.01s \|\| -0m00.47s 0m42.19s \| MontgomeryCurveTheorems \| 0m42.18s \|\| +0m00.00s 0m41.08s \| ModularArithmetic/Conversion \| 0m41.84s \|\| -0m00.76s 0m36.62s \| Spec/Ed25519 \| 0m37.13s \|\| -0m00.51s 0m23.64s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m24.44s \|\| -0m00.80s 0m19.94s \| Specific/GF25519 \| 0m20.12s \|\| -0m00.17s 0m19.59s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m19.83s \|\| -0m00.23s 0m19.14s \| Reflection/Z/Bounds/InterpretationLemmas \| 0m19.90s \|\| -0m00.75s 0m18.65s \| EdDSARepChange \| 0m18.74s \|\| -0m00.08s 0m16.24s \| Reflection/Z/ArithmeticSimplifierWf \| 0m17.11s \|\| -0m00.87s 0m15.03s \| Util/ZUtil \| 0m15.93s \|\| -0m00.90s 0m14.74s \| Reflection/Named/ContextProperties/NameUtil \| 0m15.11s \|\| -0m00.36s 0m14.62s \| Reflection/Named/ContextProperties/SmartMap \| 0m14.93s \|\| -0m00.31s 0m12.96s \| Specific/NewBaseSystemTest \| 0m13.24s \|\| -0m00.27s 0m11.84s \| Algebra/Field \| 0m12.49s \|\| -0m00.65s 0m10.21s \| Testbit \| 0m09.86s \|\| +0m00.35s 0m09.86s \| Reflection/Z/ArithmeticSimplifierInterp \| 0m10.69s \|\| -0m00.83s 0m09.44s \| Reflection/Named/MapCastInterp \| 0m09.82s \|\| -0m00.38s 0m08.81s \| BoundedArithmetic/ArchitectureToZLikeProofs \| 0m09.37s \|\| -0m00.55s 0m08.60s \| Assembly/GF25519 \| 0m08.66s \|\| -0m00.06s 0m08.58s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.77s \|\| -0m00.18s 0m08.53s \| BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate \| 0m08.34s \|\| +0m00.18s 0m08.41s \| BoundedArithmetic/Double/Proofs/Multiply \| 0m08.77s \|\| -0m00.35s 0m08.26s \| Reflection/InlineWf \| 0m08.59s \|\| -0m00.33s 0m07.54s \| Algebra/Ring \| 0m08.04s \|\| -0m00.49s 0m07.43s \| MxDHRepChange \| 0m07.10s \|\| +0m00.33s 0m07.15s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate \| 0m07.09s \|\| +0m00.06s 0m07.00s \| NewBaseSystem \| 0m07.16s \|\| -0m00.16s 0m06.51s \| Specific/GF1305 \| 0m06.52s \|\| -0m00.00s 0m06.09s \| Util/FixedWordSizesEquality \| 0m06.37s \|\| -0m00.28s 0m05.56s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub \| 0m05.51s \|\| +0m00.04s 0m05.38s \| CompleteEdwardsCurve/Pre \| 0m05.38s \|\| +0m00.00s 0m05.28s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m05.15s \|\| +0m00.12s 0m05.24s \| Experiments/GenericFieldPow \| 0m05.54s \|\| -0m00.29s 0m05.01s \| Specific/SC25519 \| 0m05.38s \|\| -0m00.37s 0m04.93s \| Algebra/Field_test \| 0m04.81s \|\| +0m00.12s 0m04.78s \| Reflection/InlineCastWf \| 0m04.94s \|\| -0m00.16s 0m04.10s \| Reflection/Z/Syntax/Equality \| 0m04.28s \|\| -0m00.18s 0m03.92s \| BaseSystemProofs \| 0m03.90s \|\| +0m00.02s 0m03.75s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.94s \|\| -0m00.18s 0m03.72s \| CompleteEdwardsCurve/EdwardsMontgomery \| 0m03.69s \|\| +0m00.03s 0m03.72s \| Reflection/EtaWf \| 0m03.71s \|\| +0m00.01s 0m03.60s \| Reflection/Named/CompileWf \| 0m04.01s \|\| -0m00.40s 0m03.58s \| SaturatedBaseSystem \| 0m03.76s \|\| -0m00.17s 0m03.33s \| BoundedArithmetic/InterfaceProofs \| 0m03.72s \|\| -0m00.39s 0m03.16s \| Reflection/LinearizeWf \| 0m03.26s \|\| -0m00.09s 0m03.08s \| ModularArithmetic/ZBoundedZ \| 0m03.16s \|\| -0m00.08s 0m03.01s \| Specific/FancyMachine256/Montgomery \| 0m03.16s \|\| -0m00.15s 0m02.99s \| Reflection/Named/CompileInterp \| 0m03.24s \|\| -0m00.25s 0m02.92s \| ModularArithmetic/ModularArithmeticTheorems \| 0m03.06s \|\| -0m00.14s 0m02.92s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.15s \|\| -0m00.23s 0m02.90s \| Specific/FancyMachine256/Barrett \| 0m03.18s \|\| -0m00.28s 0m02.80s \| Spec/MontgomeryCurve \| 0m03.05s \|\| -0m00.25s 0m02.77s \| BoundedArithmetic/Double/Proofs/ShiftRight \| 0m02.75s \|\| +0m00.02s 0m02.75s \| BoundedArithmetic/Double/Proofs/Decode \| 0m02.81s \|\| -0m00.06s 0m02.64s \| BoundedArithmetic/Double/Proofs/ShiftLeft \| 0m02.62s \|\| +0m00.02s 0m02.54s \| Reflection/InlineInterp \| 0m02.60s \|\| -0m00.06s 0m02.48s \| Reflection/Named/ContextProperties \| 0m02.58s \|\| -0m00.10s 0m02.47s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.39s \|\| +0m00.08s 0m02.40s \| Reflection/TestCase \| 0m02.60s \|\| -0m00.20s 0m02.35s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.40s \|\| -0m00.04s 0m02.35s \| Reflection/Z/Bounds/Relax \| 0m02.46s \|\| -0m00.10s 0m02.33s \| Reflection/Named/NameUtilProperties \| 0m02.40s \|\| -0m00.06s 0m02.15s \| Reflection/WfProofs \| 0m02.26s \|\| -0m00.10s 0m02.00s \| Reflection/WfReflective \| 0m02.04s \|\| -0m00.04s 0m01.97s \| ModularArithmetic/Montgomery/ZBounded \| 0m02.14s \|\| -0m00.17s 0m01.90s \| Specific/FancyMachine256/Core \| 0m01.98s \|\| -0m00.08s 0m01.89s \| Util/WordUtil \| 0m01.96s \|\| -0m00.07s 0m01.88s \| Assembly/Evaluables \| 0m01.82s \|\| +0m00.05s 0m01.62s \| WeierstrassCurve/Pre \| 0m01.64s \|\| -0m00.01s 0m01.56s \| Reflection/Named/InterpretToPHOASWf \| 0m01.61s \|\| -0m00.05s 0m01.46s \| Assembly/Compile \| 0m01.51s \|\| -0m00.05s 0m01.44s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.43s \|\| +0m00.01s 0m01.44s \| ModularArithmetic/BarrettReduction/Z \| 0m01.57s \|\| -0m00.13s 0m01.41s \| Algebra/Group \| 0m01.87s \|\| -0m00.46s 0m01.40s \| Util/Tuple \| 0m01.46s \|\| -0m00.06s 0m01.38s \| Reflection/MapCastInterp \| 0m01.38s \|\| +0m00.00s 0m01.31s \| BoundedArithmetic/Double/Repeated/Proofs/Decode \| 0m01.05s \|\| +0m00.26s 0m01.26s \| ModularArithmetic/ExtendedBaseVector \| 0m01.28s \|\| -0m00.02s 0m01.16s \| Assembly/Conversions \| 0m01.13s \|\| +0m00.03s 0m01.14s \| Reflection/Z/Bounds/Pipeline/Definition \| 0m01.15s \|\| -0m00.01s 0m01.13s \| BaseSystem \| 0m01.14s \|\| -0m00.01s 0m01.06s \| Reflection/SmartBoundInterp \| 0m01.07s \|\| -0m00.01s 0m01.04s \| Reflection/Named/InterpretToPHOASInterp \| 0m00.99s \|\| +0m00.05s 0m01.01s \| Reflection/SmartCastWf \| 0m00.94s \|\| +0m00.07s 0m01.01s \| Assembly/Pipeline \| 0m01.02s \|\| -0m00.01s 0m01.01s \| Reflection/Relations \| 0m01.06s \|\| -0m00.05s 0m00.97s \| Assembly/HL \| 0m00.99s \|\| -0m00.02s 0m00.96s \| Algebra/IntegralDomain \| 0m01.00s \|\| -0m00.04s 0m00.94s \| Assembly/LL \| 0m01.02s \|\| -0m00.08s 0m00.92s \| BoundedArithmetic/Double/Proofs/BitwiseOr \| 0m00.91s \|\| +0m00.01s 0m00.90s \| Assembly/PhoasCommon \| 0m00.87s \|\| +0m00.03s 0m00.89s \| Util/NumTheoryUtil \| 0m00.92s \|\| -0m00.03s 0m00.87s \| BoundedArithmetic/Double/Proofs/LoadImmediate \| 0m00.96s \|\| -0m00.08s 0m00.84s \| Reflection/WfInversion \| 0m00.88s \|\| -0m00.04s 0m00.83s \| Reflection/InlineCastInterp \| 0m00.85s \|\| -0m00.02s 0m00.81s \| Reflection/Named/CompileProperties \| 0m00.87s \|\| -0m00.05s 0m00.80s \| BoundedArithmetic/X86ToZLikeProofs \| 0m00.86s \|\| -0m00.05s 0m00.78s \| Karatsuba \| 0m00.84s \|\| -0m00.05s 0m00.72s \| Util/PartiallyReifiedProp \| 0m00.73s \|\| -0m00.01s 0m00.72s \| Reflection/MultiSizeTest \| 0m00.72s \|\| +0m00.00s 0m00.69s \| ModularArithmetic/ModularBaseSystem \| 0m00.72s \|\| -0m00.03s 0m00.68s \| BoundedArithmetic/Double/Repeated/Proofs/Multiply \| 0m00.61s \|\| +0m00.07s 0m00.68s \| Reflection/MapCastByDeBruijnInterp \| 0m00.76s \|\| -0m00.07s 0m00.68s \| Encoding/ModularWordEncodingTheorems \| 0m00.80s \|\| -0m00.12s 0m00.68s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.72s \|\| -0m00.03s 0m00.67s \| Spec/EdDSA \| 0m00.66s \|\| +0m00.01s 0m00.67s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.74s \|\| -0m00.06s 0m00.66s \| Reflection/Z/Bounds/Pipeline/ReflectiveTactics \| 0m00.62s \|\| +0m00.04s 0m00.66s \| Util/IterAssocOp \| 0m00.94s \|\| -0m00.27s 0m00.64s \| Encoding/ModularWordEncodingPre \| 0m00.73s \|\| -0m00.08s 0m00.63s \| ModularArithmetic/ModularBaseSystemList \| 0m00.77s \|\| -0m00.14s 0m00.62s \| Spec/ModularWordEncoding \| 0m00.66s \|\| -0m00.04s 0m00.61s \| Reflection/MapCastByDeBruijnWf \| 0m00.61s \|\| +0m00.00s 0m00.58s \| BoundedArithmetic/X86ToZLike \| 0m00.57s \|\| +0m00.01s 0m00.58s \| Reflection/Z/CNotations \| 0m00.56s \|\| +0m00.01s 0m00.57s \| Spec/WeierstrassCurve \| 0m00.57s \|\| +0m00.00s 0m00.56s \| Spec/CompleteEdwardsCurve \| 0m00.59s \|\| -0m00.02s 0m00.56s \| BoundedArithmetic/Double/Proofs/SelectConditional \| 0m00.58s \|\| -0m00.01s 0m00.56s \| Reflection/InterpByIsoProofs \| 0m00.60s \|\| -0m00.03s 0m00.55s \| Reflection/Named/WfInterp \| 0m00.57s \|\| -0m00.01s 0m00.55s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight \| 0m00.57s \|\| -0m00.01s 0m00.54s \| Reflection/Named/FMapContext \| 0m00.70s \|\| -0m00.15s 0m00.54s \| Util/AdditionChainExponentiation \| 0m00.62s \|\| -0m00.07s 0m00.54s \| Reflection/SmartBoundWf \| 0m00.55s \|\| -0m00.01s 0m00.54s \| Reflection/WfReflectiveGen \| 0m00.54s \|\| +0m00.00s 0m00.54s \| BoundedArithmetic/Interface \| 0m00.56s \|\| -0m00.02s 0m00.52s \| BoundedArithmetic/ArchitectureToZLike \| 0m00.46s \|\| +0m00.06s 0m00.52s \| Reflection/Z/JavaNotations \| 0m00.58s \|\| -0m00.05s 0m00.52s \| Reflection/Z/Syntax/Util \| 0m00.53s \|\| -0m00.01s 0m00.52s \| Util/CPSUtil \| 0m00.57s \|\| -0m00.04s 0m00.51s \| Reflection/BoundByCastInterp \| 0m00.51s \|\| +0m00.00s 0m00.50s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate \| 0m00.53s \|\| -0m00.03s 0m00.50s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub \| 0m00.57s \|\| -0m00.06s 0m00.50s \| Reflection/InterpWfRel \| 0m00.54s \|\| -0m00.04s 0m00.49s \| Reflection/Z/InlineInterp \| 0m00.37s \|\| +0m00.12s 0m00.49s \| Reflection/InputSyntax \| 0m00.55s \|\| -0m00.06s 0m00.49s \| Util/Decidable \| 0m00.48s \|\| +0m00.01s 0m00.48s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.39s \|\| +0m00.08s 0m00.48s \| BoundedArithmetic/Double/Repeated/Core \| 0m00.48s \|\| +0m00.00s 0m00.47s \| BoundedArithmetic/Double/Core \| 0m00.50s \|\| -0m00.03s 0m00.47s \| Reflection/Z/Bounds/Pipeline \| 0m00.46s \|\| +0m00.00s 0m00.47s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional \| 0m00.54s \|\| -0m00.07s 0m00.47s \| ModularArithmetic/ModularBaseSystemListZOperationsProofs \| 0m00.42s \|\| +0m00.04s 0m00.47s \| Util/NUtil \| 0m00.50s \|\| -0m00.03s 0m00.47s \| Reflection/Z/Bounds/Interpretation \| 0m00.42s \|\| +0m00.04s 0m00.47s \| Reflection/Z/Reify \| 0m00.49s \|\| -0m00.02s 0m00.46s \| BoundedArithmetic/StripCF \| 0m00.44s \|\| +0m00.02s 0m00.46s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr \| 0m00.51s \|\| -0m00.04s 0m00.46s \| Reflection/Z/MapCastByDeBruijn \| 0m00.50s \|\| -0m00.03s 0m00.46s \| Reflection/Z/Bounds/MapCastByDeBruijnWf \| 0m00.42s \|\| +0m00.04s 0m00.46s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate \| 0m00.55s \|\| -0m00.09s 0m00.45s \| Util/HList \| 0m00.50s \|\| -0m00.04s 0m00.44s \| Reflection/Z/Inline \| 0m00.39s \|\| +0m00.04s 0m00.44s \| Reflection/InterpWf \| 0m00.55s \|\| -0m00.11s 0m00.44s \| Reflection/Z/Syntax \| 0m00.46s \|\| -0m00.02s 0m00.44s \| Reflection/Z/ArithmeticSimplifier \| 0m00.47s \|\| -0m00.02s 0m00.44s \| Reflection/Named/DeadCodeElimination \| 0m00.36s \|\| +0m00.08s 0m00.44s \| ModularArithmetic/ZBounded \| 0m00.49s \|\| -0m00.04s 0m00.43s \| ModularArithmetic/Pre \| 0m00.44s \|\| -0m00.01s 0m00.42s \| ModularArithmetic/Montgomery/Z \| 0m00.39s \|\| +0m00.02s 0m00.42s \| Reflection/Z/Bounds/MapCastByDeBruijnInterp \| 0m00.43s \|\| -0m00.01s 0m00.42s \| Util/ZRange \| 0m00.42s \|\| +0m00.00s 0m00.42s \| Reflection/Z/MapCastByDeBruijnInterp \| 0m00.46s \|\| -0m00.04s 0m00.41s \| BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic \| 0m00.45s \|\| -0m00.04s 0m00.41s \| Reflection/Z/Bounds/MapCastByDeBruijn \| 0m00.50s \|\| -0m00.09s 0m00.40s \| Reflection/Z/MapCastByDeBruijnWf \| 0m00.50s \|\| -0m00.09s 0m00.40s \| Reflection/Z/InlineWf \| 0m00.42s \|\| -0m00.01s 0m00.40s \| Reflection/Z/Bounds/Pipeline/OutputType \| 0m00.38s \|\| +0m00.02s 0m00.40s \| ModularArithmetic/Pow2Base \| 0m00.43s \|\| -0m00.02s 0m00.40s \| Reflection/Named/PositiveContext/DefaultsProperties \| 0m00.52s \|\| -0m00.12s 0m00.40s \| Reflection/MapCastByDeBruijn \| 0m00.39s \|\| +0m00.01s 0m00.39s \| Reflection/Z/Bounds/Pipeline/Glue \| 0m00.46s \|\| -0m00.07s 0m00.39s \| Reflection/Named/PositiveContext/Defaults \| 0m00.40s \|\| -0m00.01s 0m00.39s \| Reflection/Named/ContextDefinitions \| 0m00.37s \|\| +0m00.02s 0m00.38s \| Reflection/Z/FoldTypes \| 0m00.38s \|\| +0m00.00s 0m00.38s \| Reflection/Z/HexNotationConstants \| 0m00.42s \|\| -0m00.03s 0m00.38s \| Reflection/Z/OpInversion \| 0m00.37s \|\| +0m00.01s 0m00.38s \| ModularArithmetic/ModularBaseSystemListZOperations \| 0m00.41s \|\| -0m00.02s 0m00.38s \| Reflection/Named/EstablishLiveness \| 0m00.38s \|\| +0m00.00s 0m00.38s \| Reflection/Named/RegisterAssign \| 0m00.38s \|\| +0m00.00s 0m00.38s \| Reflection/Reify \| 0m00.40s \|\| -0m00.02s 0m00.37s \| ModularArithmetic/ModularBaseSystemWord \| 0m00.38s \|\| -0m00.01s 0m00.36s \| Reflection/Named/InterpretToPHOAS \| 0m00.45s \|\| -0m00.09s 0m00.36s \| Reflection/Named/Syntax \| 0m00.35s \|\| +0m00.01s 0m00.36s \| BoundedArithmetic/Eta \| 0m00.42s \|\| -0m00.06s 0m00.35s \| Reflection/Named/Compile \| 0m00.34s \|\| +0m00.00s 0m00.35s \| Reflection/MapCastWf \| 0m00.31s \|\| +0m00.03s 0m00.35s \| Reflection/Named/SmartMap \| 0m00.36s \|\| -0m00.01s 0m00.35s \| Util/BoundedWord \| 0m00.40s \|\| -0m00.05s 0m00.35s \| Spec/ModularArithmetic \| 0m00.36s \|\| -0m00.01s 0m00.34s \| Reflection/Named/ContextOn \| 0m00.34s \|\| +0m00.00s 0m00.34s \| Reflection/FilterLive \| 0m00.32s \|\| +0m00.02s 0m00.34s \| Reflection/Named/MapCast \| 0m00.37s \|\| -0m00.02s 0m00.33s \| Reflection/Named/PositiveContext \| 0m00.39s \|\| -0m00.06s 0m00.33s \| Algebra/ScalarMult \| 0m00.56s \|\| -0m00.23s 0m00.32s \| Reflection/Z/BinaryNotationConstants \| 0m00.35s \|\| -0m00.02s 0m00.32s \| Reflection/Tuple \| 0m00.38s \|\| -0m00.06s 0m00.32s \| Reflection/Named/ContextProperties/Tactics \| 0m00.48s \|\| -0m00.15s 0m00.32s \| Reflection/Named/IdContext \| 0m00.33s \|\| -0m00.01s 0m00.31s \| Reflection/Named/Wf \| 0m00.38s \|\| -0m00.07s 0m00.30s \| Reflection/MultiSizeTest2 \| 0m00.34s \|\| -0m00.04s 0m00.29s \| Reflection/ExprInversion \| 0m00.26s \|\| +0m00.02s 0m00.29s \| Spec/MxDH \| 0m00.43s \|\| -0m00.14s 0m00.26s \| Algebra/Monoid \| 0m00.51s \|\| -0m00.25s 0m00.26s \| Util/Sum \| 0m00.34s \|\| -0m00.08s 0m00.24s \| Algebra \| 0m00.43s \|\| -0m00.19s 0m00.23s \| Reflection/Equality \| 0m00.25s \|\| -0m00.01s 0m00.22s \| Reflection/CommonSubexpressionElimination \| 0m00.17s \|\| +0m00.04s 0m00.21s \| Reflection/SmartMap \| 0m00.23s \|\| -0m00.02s 0m00.20s \| Reflection/EtaInterp \| 0m00.22s \|\| -0m00.01s 0m00.20s \| Reflection/BoundByCastWf \| 0m00.12s \|\| +0m00.08s 0m00.20s \| Reflection/LinearizeInterp \| 0m00.23s \|\| -0m00.03s 0m00.18s \| Util/LetInMonad \| 0m00.19s \|\| -0m00.01s 0m00.16s \| Reflection/InterpProofs \| 0m00.18s \|\| -0m00.01s 0m00.13s \| Util/Option \| 0m00.14s \|\| -0m00.01s 0m00.13s \| Reflection/Wf \| 0m00.12s \|\| +0m00.01s 0m00.12s \| Reflection/RewriterWf \| 0m00.19s \|\| -0m00.07s 0m00.08s \| Reflection/Conversion \| 0m00.08s \|\| +0m00.00s 0m00.08s \| Reflection/Named/NameUtil \| 0m00.12s \|\| -0m00.03s 0m00.07s \| Reflection/Inline \| 0m00.04s \|\| +0m00.03s 0m00.06s \| Reflection/TypeInversion \| 0m00.08s \|\| -0m00.02s 0m00.06s \| Reflection/SmartBound \| 0m00.06s \|\| +0m00.00s 0m00.06s \| Reflection/InlineCast \| 0m00.06s \|\| +0m00.00s 0m00.06s \| Util/Tactics \| 0m00.07s \|\| -0m00.01s 0m00.06s \| Reflection/RewriterInterp \| 0m00.05s \|\| +0m00.00s 0m00.06s \| Reflection/MapCast \| 0m00.06s \|\| +0m00.00s 0m00.05s \| Reflection/TypeUtil \| 0m00.04s \|\| +0m00.01s 0m00.04s \| Reflection/Syntax \| 0m00.09s \|\| -0m00.05s 0m00.04s \| Reflection/FoldTypes \| 0m00.05s \|\| -0m00.01s 0m00.04s \| Reflection/Linearize \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Reflection/Rewriter \| 0m00.03s \|\| +0m00.01s 0m00.04s \| Reflection/Map \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Util/Tactics/OnSubterms \| N/A \|\| +0m00.04s 0m00.04s \| Reflection/CountLets \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Reflection/SmartCast \| 0m00.04s \|\| +0m00.00s 0m00.04s \| Util/LetIn \| 0m00.07s \|\| -0m00.03s 0m00.04s \| Reflection/Eta \| 0m00.05s \|\| -0m00.01s 0m00.04s \| Reflection/BoundByCast \| 0m00.06s \|\| -0m00.01s 0m00.03s \| Reflection/SmartCastInterp \| 0m00.05s \|\| -0m00.02s 0m00.03s \| Util/Tactics/SubstEvars \| N/A \|\| +0m00.03s 0m00.03s \| Reflection/InterpByIso \| 0m00.04s \|\| -0m00.01s 0m00.03s \| Util/Tactics/Forward \| N/A \|\| +0m00.03s 0m00.03s \| Util/Tactics/BreakMatch \| 0m00.02s \|\| +0m00.00s 0m00.03s \| Reflection/RenameBinders \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Util/Tactics/ConvoyDestruct \| N/A \|\| +0m00.03s 0m00.02s \| Util/Tactics/SideConditionsBeforeToAfter \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/Revert \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/Test \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/SetEvars \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/SetoidSubst \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/DestructTrivial \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/ESpecialize \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/SimplifyProjections \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/Not \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/Contains \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/SimplifyRepeatedIfs \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/ClearDuplicates \| N/A \|\| +0m00.02s 0m00.02s \| Util/Tactics/DebugPrint \| N/A \|\| +0m00.02s 0m00.01s \| Util/Tactics/GetGoal \| N/A \|\| +0m00.01s
*	Be more fine-grained in WeierstrassCurveTheorems imports	Jason Gross	2017-04-03
\| \| \| \|	We don't need to rebuild it every time we add a new Tactics/ file
*	Split off liftn_sig, add lift{3,4}_sig	Jason Gross	2017-04-03
\|
*	Synthesize mul instead of add	Jason Gross	2017-04-03
\|
*	Work around an anomaly in pretyping/constr_matching	Jason Gross	2017-04-03
\|
*	Document some tactics from Jade's pipleine side	Jason Gross	2017-04-03
\| \| \| \| \|	Also use more definitions and fewer tactics, and more general definitions.
*	Fuse Pipeline.{Composition,ReflectiveTactics}	Jason Gross	2017-04-03
\| \| \| \| \|	They need to be modified together to keep track of the ordering of side-conditions.
*	Fix missing unfold in proof	Jason Gross	2017-04-03
\|
*	Add missing parentheses	Jason Gross	2017-04-03
\|
*	Use projT2_map	Jason Gross	2017-04-03
\|
*	Finally, a fully working IntegrationTest	Jason Gross	2017-04-03
\|
*	WIP	Jason Gross	2017-04-03
\|
*	WIP on integration	Jason Gross	2017-04-03
\|
*	Rework and doc reflective pipeline (more Gallina)	Jason Gross	2017-04-03
\|
*	Add an initial stab at doing the pipeline mostly in Gallina	Jason Gross	2017-04-03
\|
*	Add a bit more documentation	Jason Gross	2017-04-03
\|
*	Pipeline: reduce away reflective constants	Jason Gross	2017-04-03
\| \| \| \| \|	This makes it so that the term that shows up when the reflective subgoal is solved doesn't include things like [Interp]
*	Start adding comments to Pipeline/ReflectiveTactics.v	Jason Gross	2017-04-03
\|
*	Rename PreDefinitions to OutputType	Jason Gross	2017-04-03
\| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/pull/141#discussion_r109312653
*	Add and update documentation in Pipeline/Glue.v	Jason Gross	2017-04-03
\|
*	An approximately first stab DeBruijn word-size-sel	Jason Gross	2017-04-03
\|
*	Remove old reflective pipeline, making way the new	Jason Gross	2017-04-03
\|
*	Remove everything after the individual reified ops	Jason Gross	2017-04-03
\| \| \| \| \|	This includes extraction and associated targets. I've left the .hs files lying around, currently unused.
*	Fix parsing issue	Jason Gross	2017-04-03
\|
*	Add proj2_sig_map	Jason Gross	2017-04-03
\|
*	Don't require keeping track of which goals have evars; check that in tactics	Jason Gross	2017-04-03
\|
*	Add UnifyAbstractReflexivity tactics	Jason Gross	2017-04-03
\|
*	Fix a typo	Jason Gross	2017-04-02
\|
*	Add projT2_map	Jason Gross	2017-04-02
\|
*	Add Tactics.EvarExists	Jason Gross	2017-04-02
\|
*	Add Util.SigmaAssoc	Jason Gross	2017-04-02
\|
*	clear before abstract so we can handle existentials	Jason Gross	2017-04-02
\|
*	Add ap_transport to Equality.v	Jason Gross	2017-04-02
\|
*	Add InterpEta	Jason Gross	2017-04-02
\| \| \| \|	It's a version of [Interp] that works even when there are destructuring lets.
*	Remove the bits of the new reflective pipeline in master	Jason Gross	2017-04-02
\| \| \| \|	This way, we can keep all of new pipeline code together in the PR
*	Remove all the .v files in SpecificGen	Jason Gross	2017-04-02
\| \| \| \|	This gets most of the way to 10 in #14.
*	More extensive comment in NewBaseSystem	Jason Gross	2017-04-02
\| \| \| \|	As per Andres' request on #138.
*	Work around bug #5434	Jason Gross	2017-04-02
\| \| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5434, [vm_compute] breaks an invariant asserted on line 115 of pretyping/constr_matching.ml. This was triggering whenever we tried to reify one of the operations.
*	Coalesce Tuple.pointwise2 and Tuple.fieldwise	Jason Gross	2017-04-02
\| \| \| \| \| \|	We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137.
*	Generalize Z.InterpInlineConst	Jason Gross	2017-04-02
\|
*	Better version of inversion_ProcessedReflectivePackage	Jason Gross	2017-04-02
\| \| \| \|	Now it doesn't introduce needless dependencies
*	Add inversion_ProcessedReflectivePackage	Jason Gross	2017-04-02
\|
*	Add PreDefinitions pipeline file	Jason Gross	2017-04-02
\|
*	Add Z instantiations of InlineConst	Jason Gross	2017-04-02
\|
*	Add Z.Bounds.MapCastByDeBruijn instantiation	Jason Gross	2017-04-02
\|
*	Add Z instantiation of MapCastByDeBruijnInterp	Jason Gross	2017-04-02
\|
*	Add reflective_interp rewrite db	Jason Gross	2017-04-02
\|