fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	new add/carry chain logic with admitted proofs	jadep	2017-06-29
\|
*	Skeleton for add/subtract chains (see #222)	jadep	2017-06-29
\|
*	Add wrappers for subborrow and add_with_get_carry so they work when it is ↵	jadep	2017-06-29
\| \| \| \|	not known that they split on a power of 2
*	Update .gitignore with things from make bench	Jason Gross	2017-06-29
\|
*	Fix comment-in-string issues	Jason Gross	2017-06-29
\|
*	More C Notations for uin8_t-valued addcarryx	Jason Gross	2017-06-29
\|
*	Add proper dependencies on .h file in Makefile	Jason Gross	2017-06-29
\|
*	Remove a [Check]	Jason Gross	2017-06-29
\|
*	Use -std=gnu11 for older versions of gcc	Jason Gross	2017-06-28
\|
*	Make the same display on windows and linux	Jason Gross	2017-06-28
\| \| \| \|	Do this by removing windows line endings via sed
*	match C code in Jacobian addition	Andres Erbsen	2017-06-27
\|
*	p256 compilation and benchmarks with manual kludges	Andres Erbsen	2017-06-27
\|
*	proved eval_mod and eval_div (last remaining eval_ admits in Saturated)	jadep	2017-06-27
\|
*	Drop the two slowest files from the lite target	Jason Gross	2017-06-26
\|
*	Empty commit with timing log, for easy reference	Jason Gross	2017-06-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Time \| File Name ----------------------------------------------------------------------------------- 53m11.20s \| Total ----------------------------------------------------------------------------------- 11m29.79s \| Curves/Weierstrass/AffineProofs 5m49.40s \| Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256 2m59.82s \| Specific/X25519/C64/ladderstep 2m55.06s \| Curves/Montgomery/AffineProofs 2m06.89s \| Curves/Weierstrass/Projective 1m45.76s \| Curves/Weierstrass/Jacobian/Precomputed 1m41.31s \| Spec/Test/X25519 1m22.31s \| Specific/IntegrationTestKaratsubaMul 1m09.37s \| Specific/IntegrationTestLadderstep130 1m06.28s \| Specific/Karatsuba 1m03.94s \| Demo 0m56.63s \| Compilers/Z/Named/RewriteAddToAdcInterp 0m43.36s \| Compilers/Z/Bounds/Pipeline/Definition 0m41.07s \| Spec/Ed25519 0m39.40s \| Compilers/Z/ArithmeticSimplifierInterp 0m38.85s \| Compilers/Z/ArithmeticSimplifierWf 0m37.45s \| Specific/IntegrationTestMontgomeryP256_128 0m33.05s \| Curves/Montgomery/XZProofs 0m29.20s \| Compilers/CommonSubexpressionEliminationWf 0m28.70s \| Specific/NISTP256/AMD64/MontgomeryP256 0m27.41s \| Arithmetic/Saturated 0m25.22s \| Primitives/EdDSARepChange 0m24.91s \| Curves/Edwards/AffineProofs 0m24.23s \| Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs 0m21.97s \| Curves/Edwards/XYZT/Basic 0m20.95s \| Compilers/Named/MapCastWf 0m20.62s \| Arithmetic/Karatsuba 0m19.08s \| Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Sub 0m18.44s \| Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Add 0m17.40s \| Specific/IntegrationTestFreeze 0m16.71s \| Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Opp 0m16.24s \| Compilers/Named/MapCastInterp 0m15.48s \| Compilers/Named/ContextProperties/NameUtil 0m15.01s \| Compilers/Named/ContextProperties/SmartMap 0m14.89s \| Specific/MontgomeryP256_128 0m14.78s \| Compilers/Z/Syntax/Equality 0m14.04s \| Specific/X25519/C64/femul 0m13.57s \| Algebra/Field 0m13.44s \| Specific/IntegrationTestMontgomeryP256_128_Sub 0m12.97s \| Specific/IntegrationTestMontgomeryP256_128_Add 0m12.96s \| Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs 0m12.62s \| Specific/IntegrationTestMontgomeryP256_128_Opp 0m12.10s \| Specific/ArithmeticSynthesisTest 0m11.94s \| Specific/IntegrationTestSub 0m11.10s \| Primitives/MxDHRepChange 0m10.44s \| Specific/X25519/C64/fesquare 0m10.24s \| Util/ZUtil 0m09.92s \| Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero 0m09.91s \| Arithmetic/Core 0m09.52s \| LegacyArithmetic/Double/Proofs/Multiply 0m09.46s \| LegacyArithmetic/ArchitectureToZLikeProofs 0m09.23s \| Arithmetic/MontgomeryReduction/Proofs 0m09.19s \| Specific/IntegrationTestMontgomeryP256_128_Nonzero 0m09.12s \| Algebra/Ring 0m09.04s \| Compilers/Named/RegisterAssignInterp 0m08.86s \| LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate 0m08.39s \| Compilers/Named/CompileInterpSideConditions 0m08.28s \| Compilers/InlineWf 0m08.15s \| Util/ZUtil/ZSimplify/Autogenerated 0m07.33s \| LegacyArithmetic/Double/Proofs/SpreadLeftImmediate 0m06.94s \| Util/FixedWordSizesEquality 0m06.20s \| Bedrock/Word 0m06.14s \| Compilers/Z/Bounds/InterpretationLemmas/PullCast 0m05.98s \| Compilers/LinearizeWf 0m05.90s \| LegacyArithmetic/Double/Proofs/RippleCarryAddSub 0m05.80s \| Specific/ArithmeticSynthesisTest130 0m05.76s \| LegacyArithmetic/Pow2BaseProofs 0m05.76s \| Curves/Edwards/Pre 0m05.40s \| Util/ListUtil 0m05.02s \| Algebra/Field_test 0m04.64s \| Compilers/WfProofs 0m04.62s \| Util/ZUtil/Modulo 0m04.06s \| Arithmetic/BarrettReduction/HAC 0m04.06s \| Curves/Montgomery/Affine 0m03.96s \| Util/ForLoop/Unrolling 0m03.74s \| Compilers/EtaWf 0m03.68s \| LegacyArithmetic/InterfaceProofs 0m03.61s \| Compilers/Z/RewriteAddToAdcInterp 0m03.60s \| Compilers/Named/CompileWf 0m03.30s \| Compilers/TestCase 0m03.21s \| LegacyArithmetic/ZBoundedZ 0m03.20s \| Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy 0m03.19s \| Arithmetic/BarrettReduction/Generalized 0m03.06s \| LegacyArithmetic/Double/Proofs/ShiftRight 0m03.00s \| Specific/NISTP256/FancyMachine256/Montgomery 0m02.98s \| Compilers/Z/ArithmeticSimplifier 0m02.98s \| Arithmetic/MontgomeryReduction/WordByWord/Proofs 0m02.92s \| Compilers/Named/CompileInterp 0m02.90s \| LegacyArithmetic/Double/Proofs/Decode 0m02.87s \| LegacyArithmetic/Double/Proofs/ShiftLeft 0m02.86s \| Specific/NISTP256/FancyMachine256/Barrett 0m02.85s \| Spec/MontgomeryCurve 0m02.84s \| Arithmetic/ModularArithmeticTheorems 0m02.80s \| Algebra/Group 0m02.71s \| Compilers/Named/ContextProperties 0m02.57s \| Compilers/InlineInterp 0m02.56s \| Compilers/Z/Bounds/Relax 0m02.42s \| Compilers/Named/NameUtilProperties 0m02.42s \| LegacyArithmetic/BarretReduction 0m02.28s \| Util/WordUtil 0m02.26s \| Compilers/CommonSubexpressionEliminationProperties 0m02.12s \| Util/ForLoop/InvariantFramework 0m02.11s \| Compilers/WfReflective 0m02.05s \| Specific/NISTP256/FancyMachine256/Core 0m01.82s \| Spec/WeierstrassCurve 0m01.80s \| Compilers/Named/ContextProperties/Proper 0m01.67s \| LegacyArithmetic/MontgomeryReduction 0m01.65s \| Util/ZUtil/AddGetCarry 0m01.64s \| Util/Tuple 0m01.63s \| Arithmetic/BarrettReduction/Wikipedia 0m01.52s \| Arithmetic/PrimeFieldTheorems 0m01.50s \| Util/NatUtil 0m01.44s \| Compilers/Named/InterpretToPHOASWf 0m01.41s \| Util/Loop 0m01.40s \| Compilers/Named/WfFromUnit 0m01.38s \| Util/ZUtil/Quot 0m01.35s \| Curves/Edwards/XYZT/Precomputed 0m01.27s \| Compilers/Z/CNotations 0m01.20s \| Algebra/ScalarMult 0m01.17s \| Compilers/Z/RewriteAddToAdcWf 0m01.12s \| Curves/Montgomery/AffineInstances 0m01.08s \| Compilers/Relations 0m01.02s \| Util/ZUtil/Pow2Mod 0m01.01s \| LegacyArithmetic/Double/Proofs/BitwiseOr 0m00.99s \| Compilers/LinearizeInterp 0m00.98s \| LegacyArithmetic/Double/Proofs/LoadImmediate 0m00.98s \| Util/NumTheoryUtil 0m00.97s \| Algebra/IntegralDomain 0m00.94s \| LegacyArithmetic/BaseSystemProofs 0m00.89s \| Compilers/WfInversion 0m00.88s \| Compilers/Named/CompileProperties 0m00.88s \| Util/ZUtil/Div 0m00.88s \| Compilers/Named/InterpretToPHOASInterp 0m00.86s \| Compilers/MapCastByDeBruijnInterp 0m00.85s \| Compilers/Z/CommonSubexpressionElimination 0m00.82s \| Compilers/Z/Bounds/Pipeline/ReflectiveTactics 0m00.81s \| Compilers/Z/Syntax/Util 0m00.79s \| Util/ZUtil/Testbit 0m00.78s \| Util/ZUtil/Stabilization 0m00.77s \| Util/PartiallyReifiedProp 0m00.77s \| Arithmetic/MontgomeryReduction/WordByWord/Definition 0m00.73s \| Specific/IntegrationTestTemporaryMiscCommon 0m00.73s \| Compilers/MultiSizeTest 0m00.66s \| LegacyArithmetic/Interface 0m00.66s \| Compilers/MapCastByDeBruijnWf 0m00.64s \| LegacyArithmetic/Double/Proofs/SelectConditional 0m00.63s \| Util/CPSUtil 0m00.62s \| Compilers/Z/JavaNotations 0m00.61s \| Compilers/Z/Named/RewriteAddToAdc 0m00.61s \| Compilers/Z/Bounds/Pipeline 0m00.61s \| Curves/Montgomery/XZ 0m00.60s \| Spec/CompleteEdwardsCurve 0m00.60s \| Util/ZUtil/Modulo/PullPush 0m00.60s \| Compilers/CommonSubexpressionEliminationInterp 0m00.58s \| Compilers/InterpByIsoProofs 0m00.58s \| Compilers/WfReflectiveGen 0m00.58s \| Curves/Weierstrass/Affine 0m00.58s \| Util/ForLoop/Tests 0m00.56s \| Arithmetic/ModularArithmeticPre 0m00.55s \| Compilers/Z/Bounds/MapCastByDeBruijnInterp 0m00.54s \| Compilers/Z/Reify 0m00.54s \| LegacyArithmetic/Double/Core 0m00.53s \| Compilers/Z/Bounds/Pipeline/Glue 0m00.53s \| Compilers/InputSyntax 0m00.53s \| Util/Decidable 0m00.53s \| LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic 0m00.52s \| Compilers/Z/Bounds/InterpretationLemmas/Tactics 0m00.52s \| Compilers/Z/Bounds/RoundUpLemmas 0m00.51s \| Compilers/InterpWfRel 0m00.51s \| Util/HList 0m00.51s \| Compilers/CommonSubexpressionElimination 0m00.50s \| Compilers/Z/Syntax 0m00.50s \| Arithmetic/MontgomeryReduction/Definition 0m00.50s \| LegacyArithmetic/ZBounded 0m00.50s \| Compilers/Z/MapCastByDeBruijnWf 0m00.50s \| Util/NUtil 0m00.50s \| Compilers/Z/FoldTypes 0m00.50s \| Compilers/Named/AListContext 0m00.50s \| Compilers/Named/InterpSideConditionsInterp 0m00.50s \| Spec/EdDSA 0m00.49s \| Compilers/Z/Bounds/MapCastByDeBruijnWf 0m00.48s \| Compilers/Named/PositiveContext/DefaultsProperties 0m00.48s \| Compilers/Z/MapCastByDeBruijnInterp 0m00.48s \| Spec/ModularArithmetic 0m00.48s \| LegacyArithmetic/ArchitectureToZLike 0m00.47s \| Compilers/Z/CommonSubexpressionEliminationWf 0m00.47s \| Compilers/Z/ArithmeticSimplifierUtil 0m00.46s \| Util/ZRange 0m00.46s \| LegacyArithmetic/BaseSystem 0m00.46s \| Compilers/Named/FMapContext 0m00.46s \| Compilers/Z/RewriteAddToAdc 0m00.45s \| Compilers/Named/DeadCodeEliminationInterp 0m00.45s \| Compilers/Z/BinaryNotationConstants 0m00.45s \| LegacyArithmetic/Pow2Base 0m00.45s \| Compilers/Z/Inline 0m00.45s \| Compilers/Z/MapCastByDeBruijn 0m00.44s \| Compilers/Z/CommonSubexpressionEliminationInterp 0m00.44s \| Compilers/Z/HexNotationConstants 0m00.44s \| Compilers/InterpWf 0m00.44s \| Compilers/Z/Bounds/MapCastByDeBruijn 0m00.44s \| Compilers/Z/Bounds/Interpretation 0m00.44s \| Specific/IntegrationTestDisplayCommon 0m00.43s \| Compilers/Z/InterpSideConditions 0m00.42s \| Util/AdditionChainExponentiation 0m00.42s \| Util/ZUtil/ZSimplify/Simple 0m00.42s \| Compilers/Z/Named/DeadCodeEliminationInterp 0m00.41s \| Util/ZUtil/Peano 0m00.40s \| Compilers/Z/Named/DeadCodeElimination 0m00.39s \| Compilers/Reify 0m00.39s \| Compilers/Z/InlineInterp 0m00.39s \| Compilers/Named/DeadCodeElimination 0m00.39s \| Util/ZUtil/EquivModulo 0m00.39s \| Compilers/Z/InlineWf 0m00.38s \| Util/BoundedWord 0m00.38s \| Util/Factorize 0m00.38s \| Util/ZUtil/Tactics/Ztestbit 0m00.38s \| Algebra/Nsatz 0m00.38s \| Compilers/Z/TypeInversion 0m00.37s \| Compilers/Z/OpInversion 0m00.37s \| Compilers/Z/Bounds/Pipeline/OutputType 0m00.37s \| Util/ZUtil/Tactics/ZeroBounds 0m00.37s \| Compilers/Tuple 0m00.36s \| Util/ZUtil/Tactics/SimplifyFractionsLe 0m00.36s \| Util/ZUtil/MulSplit 0m00.36s \| Util/ZUtil/Tactics/DivModToQuotRem 0m00.36s \| Compilers/Named/WeakListContext 0m00.36s \| Util/ZUtil/Tactics/PullPush/Modulo 0m00.36s \| Util/ZUtil/Tactics 0m00.36s \| Util/ZUtil/Tactics/LtbToLt 0m00.36s \| Util/ZUtil/Morphisms 0m00.36s \| Util/ZUtil/ZSimplify/Core 0m00.36s \| Util/IdfunWithAlt 0m00.36s \| Util/FixedWordSizes 0m00.36s \| Util/ZUtil/Hints/PullPush 0m00.35s \| Util/ZUtil/Tactics/RewriteModSmall 0m00.35s \| Util/ZUtil/Tactics/PeelLe 0m00.35s \| Util/ZUtil/Hints/Ztestbit 0m00.34s \| Compilers/Named/RegisterAssign 0m00.34s \| Util/ForLoop/Instances 0m00.34s \| Util/ZUtil/Hints/ZArith 0m00.34s \| Util/ZUtil/Hints/Core 0m00.33s \| Compilers/FilterLive 0m00.32s \| Compilers/MapCastByDeBruijn 0m00.32s \| Util/ZUtil/Hints 0m00.32s \| Algebra/Monoid 0m00.32s \| Util/ZUtil/ZSimplify 0m00.32s \| Util/ZUtil/Zselect 0m00.31s \| Compilers/Equality 0m00.31s \| Util/ZUtil/Z2Nat 0m00.31s \| Util/ZUtil/Tactics/LinearSubstitute 0m00.31s \| Util/ZUtil/Sgn 0m00.31s \| Util/ZUtil/Land 0m00.31s \| Compilers/Named/EstablishLiveness 0m00.30s \| Util/ZUtil/Definitions 0m00.30s \| Util/ZUtil/Tactics/PullPush 0m00.30s \| Compilers/Named/PositiveContext 0m00.30s \| Util/Sum 0m00.30s \| Compilers/Named/PositiveContext/Defaults 0m00.29s \| Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition 0m00.29s \| Compilers/Named/WfInterp 0m00.29s \| Util/ZUtil/Tactics/ReplaceNegWithPos 0m00.28s \| Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition 0m00.28s \| Util/ZUtil/ModInv 0m00.28s \| Algebra/Hierarchy 0m00.28s \| Util/ZUtil/Tactics/DivideExistsMul 0m00.28s \| Util/QUtil 0m00.27s \| Compilers/ExprInversion 0m00.26s \| Compilers/CommonSubexpressionEliminationDenote 0m00.25s \| Util/Decidable/Bool2Prop 0m00.25s \| Spec/MxDH 0m00.24s \| Bedrock/Nomega 0m00.24s \| Compilers/Named/ContextOn 0m00.24s \| Compilers/SmartMap 0m00.23s \| Util/ZUtil/Tactics/PrimeBound 0m00.23s \| Util/ZUtil/Tactics/CompareToSgn 0m00.22s \| Util/ForLoop 0m00.22s \| Compilers/Named/ContextProperties/Tactics 0m00.21s \| Util/ZUtil/Notations 0m00.20s \| Compilers/EtaInterp 0m00.19s \| Compilers/InterpProofs 0m00.19s \| Compilers/Named/ContextDefinitions 0m00.18s \| Util/LetInMonad 0m00.18s \| Util/PointedProp 0m00.15s \| Util/Option 0m00.14s \| Compilers/Wf 0m00.13s \| Compilers/Named/NameUtil 0m00.12s \| Compilers/RewriterWf 0m00.11s \| Compilers/Named/IdContext 0m00.10s \| Compilers/Conversion 0m00.10s \| Util/ListUtil/FoldBool 0m00.10s \| Compilers/Named/GetNames 0m00.10s \| Util/Sigma 0m00.10s \| Compilers/Named/Compile 0m00.10s \| Util/Relations 0m00.09s \| Compilers/TypeInversion 0m00.08s \| Compilers/Named/MapCast 0m00.07s \| Compilers/Named/InterpSideConditions 0m00.07s \| Compilers/Named/InterpretToPHOAS 0m00.07s \| Compilers/Linearize 0m00.07s \| Util/Equality 0m00.06s \| Compilers/Named/Context 0m00.06s \| Util/Prod 0m00.06s \| Compilers/FoldTypes 0m00.06s \| Compilers/Named/Syntax 0m00.06s \| Compilers/Inline 0m00.05s \| Util/IffT 0m00.05s \| Compilers/RewriterInterp 0m00.05s \| Compilers/Named/Wf 0m00.05s \| Compilers/Named/SmartMap 0m00.05s \| Compilers/Syntax 0m00.05s \| Compilers/Map 0m00.05s \| Compilers/InterpByIso 0m00.05s \| Compilers/Named/CountLets 0m00.05s \| Util/HProp 0m00.05s \| Compilers/InterpSideConditions 0m00.04s \| Util/Tactics/Revert 0m00.04s \| Compilers/Eta 0m00.04s \| Util/Tactics/DestructHead 0m00.04s \| Compilers/CountLets 0m00.04s \| Util/Tactics/MoveLetIn 0m00.04s \| Util/Tactics 0m00.04s \| Util/Tower 0m00.04s \| Compilers/TypeUtil 0m00.04s \| Util/Tactics/DebugPrint 0m00.03s \| Util/Logic/ImplAnd 0m00.03s \| Util/Tactics/TransparentAssert 0m00.03s \| Compilers/Rewriter 0m00.03s \| Util/Notations 0m00.03s \| Util/GlobalSettings 0m00.03s \| Util/AutoRewrite 0m00.03s \| Util/FixCoqMistakes 0m00.03s \| Util/Sigma/MapProjections 0m00.03s \| Util/Logic 0m00.03s \| LegacyArithmetic/VerdiTactics 0m00.03s \| Compilers/RenameBinders 0m00.03s \| Util/Tactics/RewriteHyp 0m00.03s \| Util/Tactics/EvarExists 0m00.03s \| Compilers/Named/ExprInversion 0m00.03s \| Util/Bool 0m00.03s \| Util/Tactics/SplitInContext 0m00.03s \| Util/Sigma/Associativity 0m00.03s \| Util/Tactics/SetEvars 0m00.03s \| Util/LetIn 0m00.03s \| Util/Tactics/SubstLet 0m00.03s \| Util/Sumbool 0m00.03s \| Util/Tactics/DestructHyps 0m00.02s \| Util/Tactics/Head 0m00.02s \| Util/Tactics/ChangeInAll 0m00.02s \| Util/Tactics/Test 0m00.02s \| Util/Sigma/Lift 0m00.02s \| Util/Curry 0m00.02s \| Util/Tactics/PrintContext 0m00.02s \| Util/Isomorphism 0m00.02s \| Util/Tactics/SpecializeBy 0m00.02s \| Util/Tactics/SetoidSubst 0m00.02s \| Util/Tactics/ConvoyDestruct 0m00.02s \| Util/Tactics/UnifyAbstractReflexivity 0m00.02s \| Util/Tactics/Forward 0m00.02s \| Util/Tactics/VM 0m00.02s \| Util/Tactics/DestructTrivial 0m00.02s \| Util/Tactics/DoWithHyp 0m00.02s \| Util/Tactics/BreakMatch 0m00.02s \| Util/Tactics/ESpecialize 0m00.02s \| Util/Tactics/SimplifyProjections 0m00.02s \| Util/CPSNotations 0m00.02s \| Util/Tactics/GetGoal 0m00.02s \| Util/Tactics/Not 0m00.02s \| Util/ChangeInAll 0m00.02s \| Util/Tactics/Contains 0m00.02s \| Util/Tactics/OnSubterms 0m00.02s \| Util/Tactics/SideConditionsBeforeToAfter 0m00.02s \| Util/Tactics/ClearbodyAll 0m00.02s \| Util/Tactics/UniquePose 0m00.02s \| Util/Unit 0m00.02s \| Util/Tactics/ETransitivity 0m00.02s \| Util/Tactics/ClearDuplicates 0m00.01s \| Util/Tactics/SubstEvars 0m00.01s \| Util/Tactics/ClearAll 0m00.01s \| Util/Tactics/SimplifyRepeatedIfs
*	More proof fixing	Jason Gross	2017-06-26
\|
*	Add a comment for nonzero_cps	Jason Gross	2017-06-26
\|
*	Fix a broken proof	Jason Gross	2017-06-26
\|
*	Factor out admitted proof into admitted lemma	Jason Gross	2017-06-26
\|
*	Remove an admit	Jason Gross	2017-06-26
\| \| \| \|	This proof should possibly be factored out and go elsewhere.....
*	make display	Jason Gross	2017-06-26
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	remove unused admit (has been moved to Tuple.v)	jadep	2017-06-26
\|
*	indentation	Jason Gross	2017-06-25
\|
*	Prove map2_zselect	Jason Gross	2017-06-25
\|
*	Prove map2_append	Jason Gross	2017-06-25
\|
*	Allow disabling adc-fusion	Jason Gross	2017-06-25
\|
*	make display on p256	Andres Erbsen	2017-06-25
\|
*	Fixes #219	jadep	2017-06-25
\|
*	write and prove Tuple.map2_cps	jadep	2017-06-25
\|
*	make display	Jason Gross	2017-06-25
\|
*	Convert adc to sbb when doing [0 - x]	Jason Gross	2017-06-25
\| \| \| \|	Actually this time
*	Revert "Convert adc to sbb when doing [0 - x]"	Jason Gross	2017-06-25
\| \| \| \| \| \|	This reverts commit ecff47dbc867261b81c6e268eca99e5b5ab28805. It was wrong
*	Convert adc to sbb when doing [0 - x]	Jason Gross	2017-06-24
\|
*	make display	Jason Gross	2017-06-24
\|
*	Fix some things not being unfolded	Jason Gross	2017-06-24
\|
*	make display	Jason Gross	2017-06-24
\|
*	Propogate neg through constant multiplication	Jason Gross	2017-06-24
\|
*	Clean up some montgomery wbw instantiation, make display	Jason Gross	2017-06-24
\|
*	Remove admits	Jason Gross	2017-06-24
\|
*	Fill in axioms for sub_then_maybe_add; this required fiddling with updated ↵	jadep	2017-06-24
\| \| \| \|	arguments since more context variables were used in the definitions than in the placeholder axioms
*	made conditional_add a wrapper, defined and proved sub_then_maybe_add	jadep	2017-06-24
\|
*	Make a 'conditionals' section in Columns, and move conditional_add there	jadep	2017-06-24
\|
*	make bench	Andres Erbsen	2017-06-23
\|
*	add openssl nistz256 for benchmarking	Andres Erbsen	2017-06-23
\|
*	Weierstrass Jacobian mixed addition	Andres Erbsen	2017-06-23
\|
*	Fix an issue with notations	Jason Gross	2017-06-22
\| \| \| \| \|	CNotations breaks writing of Gallina and Ltac `match`. So we need to import it very, very late.
*	Add notation for logical or	Jason Gross	2017-06-22
\|
*	make display	Jason Gross	2017-06-22
\|
*	Add (partially admitted) integration tests for add, sub, opp	Jason Gross	2017-06-22
\|