fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Start work on a faster version of GFReflective/Common	Jason Gross	2016-11-21
\|
*	Fix for Coq 8.4	Jason Gross	2016-11-21
\|
*	Fix missing import for List.repeat in 8.4	Jason Gross	2016-11-21
\|
*	Don't let travis kill us in 10 minutes of silence	Jason Gross	2016-11-18
\|
*	Better extraction	Jason Gross	2016-11-17
\|
*	Copy bounds	Jason Gross	2016-11-17
\| \| \| \| \| \| \|	```bash $ pushd src/SpecificGen; pushd $ pushd && for i in *.json; do ./copy_bounds.sh $i; done && pushd ```
*	Finish proofs about eliminating useless carries	Jason Gross	2016-11-17
\|
*	Add add_coordinates_respectful_hetero	Jason Gross	2016-11-17
\|
*	Remove an admit	Jason Gross	2016-11-17
\|
*	Add fieldwise_map	Jason Gross	2016-11-17
\|
*	Add another admitted lemma	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 GF25519BoundedExtendedAddCoordinates	Jason Gross	2016-11-17
\| \| \| \|	The lemma is currently admitted
*	Add src/Specific/GF25519BoundedAddCoordinates.v	Jason Gross	2016-11-17
\|
*	Add HList.mapt_Proper	Jason Gross	2016-11-17
\|
*	Add ReflectiveAddCoordinates	Jason Gross	2016-11-17
\|
*	Add some missing files	Jason Gross	2016-11-17
\|
*	Fix some problems with previous commit	Jason Gross	2016-11-17
\|
*	Remove admits, fill templates, copy bounds	Jason Gross	2016-11-17
\|
*	Update AddCoordinates	Jason Gross	2016-11-17
\| \| \| \|	Now the _correct_and_bounded lemma goes through
*	Minor change in AddCoordinates	Jason Gross	2016-11-17
\|
*	Add interpf_LetIn	Jason Gross	2016-11-17
\|
*	Move util definitions to util folder	Jason Gross	2016-11-17
\|
*	Copy reified add coordinates to various versions of curves	Jason Gross	2016-11-17
\|
*	Add reified mostly-bounds-checked add_coordinates	Jason Gross	2016-11-17
\|
*	Don't build 8.5pl{1,2} on travis	Jason Gross	2016-11-17
\| \| \| \| \| \|	This will cancel out the timing increase of adding v8.5, v8.6. I've never seen 8.5 and 8.5pl3 succeed, while either 8.5pl1, or 8.5pl2 failed
*	Add tip of 8.5, 8.6 to travis	Jason Gross	2016-11-17
\| \| \| \|	Allow them to fail, though
*	Update field names in SpecificGen	Jason Gross	2016-11-17
\|
*	Move ExtendedAddCoordinates to new file, SpecGen	Jason Gross	2016-11-17
\|
*	Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry	Jason Gross	2016-11-17
\|
*	: assert is not valid 8.4 syntax	Jason Gross	2016-11-17
\|
*	Work around bug #5205 (arguments naming weirdness)	Jason Gross	2016-11-16
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5205, Bogus "Error: Wrong argument name: n." error message in 8.4, 8.5
*	Copy bounds to specific_gen	Jason Gross	2016-11-16
\|
*	Add Un{Return,Abs}_eta	Jason Gross	2016-11-16
\|
*	Add : assert to a bunch of arguments	Jason Gross	2016-11-16
\| \| \| \|	See https://coq.inria.fr/bugs/show_bug.cgi?id=5181#c3
*	Split fixedpoint in interpf	Jason Gross	2016-11-16
\|
*	Add more things to Reflective/Common	Jason Gross	2016-11-16
\| \| \| \|	Preparation for reflective add_coordinates
*	Arguments for Un{Return,Abs}	Jason Gross	2016-11-16
\|
*	Add add_coordinates_gen	Jason Gross	2016-11-16
\| \| \| \|	This in preparation for reifying add_coordinates
*	Add UnReturn, UnAbs	Jason Gross	2016-11-16
\|
*	remove outdated files: roadmap and to_gallina	Andres Erbsen	2016-11-15
\|
*	Also redact mit-plv and fiat-crypto	Jason Gross	2016-11-15
\|
*	Add instructions on building to README	Jason Gross	2016-11-15
\|
*	Add medium-specific-gen	Jason Gross	2016-11-15
\|
*	Add a small-specific-gen target	Jason Gross	2016-11-15
\|
*	Fix for Coq 8.5 (more unfolding)	Jason Gross	2016-11-15
\|
*	Empty commit with timing log	Jason Gross	2016-11-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	So I have an easy reference if I want it Time \| File Name ---------------------------------------------------------------------------------- 46m09.90s \| Total ---------------------------------------------------------------------------------- 4m16.33s \| SpecificGen/GF5211_32Reflective/Reified/Mul 3m23.12s \| SpecificGen/GF5211_32Bounded 2m55.84s \| SpecificGen/GF5211_32 2m25.01s \| SpecificGen/GF41417_32Bounded 1m47.24s \| SpecificGen/GF41417_32 1m44.75s \| SpecificGen/GF5211_32BoundedCommon 1m32.33s \| Test/Curve25519SpecTestVectors 1m17.22s \| CompleteEdwardsCurve/ExtendedCoordinates 1m13.83s \| Experiments/Ed25519 1m06.12s \| SpecificGen/GF41417_32BoundedCommon 0m59.04s \| SpecificGen/GF41417_32Reflective/Reified/Mul 0m40.43s \| ModularArithmetic/Conversion 0m37.59s \| SpecificGen/GF5211_32Reflective/CommonBinOp 0m34.60s \| Spec/Ed25519 0m33.27s \| SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE 0m33.24s \| SpecificGen/GF5211_32Reflective/CommonUnOp 0m31.56s \| ModularArithmetic/ModularBaseSystemProofs 0m30.41s \| Specific/GF25519Bounded 0m30.21s \| SpecificGen/GF25519_32Bounded 0m30.18s \| SpecificGen/GF2519_32Bounded 0m25.95s \| SpecificGen/GF41417_32Reflective/CommonBinOp 0m23.36s \| Experiments/MontgomeryCurve 0m23.17s \| SpecificGen/GF41417_32Reflective/CommonUnOp 0m22.94s \| SpecificGen/GF2519_32 0m22.53s \| SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE 0m21.95s \| ModularArithmetic/Pow2BaseProofs 0m21.76s \| Reflection/Z/Interpretations128/Relations 0m21.61s \| Specific/GF25519 0m21.14s \| SpecificGen/GF25519_32 0m20.16s \| Algebra 0m19.94s \| SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire 0m18.70s \| SpecificGen/GF2213_32Bounded 0m18.52s \| Reflection/Z/Interpretations64/Relations 0m18.14s \| EdDSARepChange 0m17.27s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems 0m16.65s \| SpecificGen/GF5211_32Reflective 0m14.18s \| SpecificGen/GF2213_32 0m14.00s \| Util/ZUtil 0m12.74s \| SpecificGen/GF5211_32Reflective/Reified/PreFreeze 0m11.65s \| SpecificGen/GF41417_32Reflective 0m11.27s \| SpecificGen/GF25519_64Reflective 0m10.94s \| SpecificGen/GF25519_64Bounded 0m10.73s \| SpecificGen/GF25519_64 0m10.41s \| SpecificGen/GF41417_32Reflective/Reified/PreFreeze 0m10.09s \| Testbit 0m09.44s \| Specific/GF25519BoundedCommon 0m09.42s \| SpecificGen/GF25519_32BoundedCommon 0m09.40s \| SpecificGen/GF2519_32BoundedCommon 0m09.28s \| Assembly/GF25519 0m09.21s \| SpecificGen/GF2519_32Reflective/Reified/Mul 0m08.90s \| SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire 0m08.81s \| BoundedArithmetic/ArchitectureToZLikeProofs 0m08.78s \| ModularArithmetic/Montgomery/ZProofs 0m08.75s \| Encoding/PointEncoding 0m08.47s \| SpecificGen/GF5211_32Reflective/Reified/CarrySub 0m08.46s \| Specific/GF1305 0m08.43s \| BoundedArithmetic/Double/Proofs/Multiply 0m08.31s \| SpecificGen/GF25519_32Reflective/Reified/Mul 0m08.12s \| Specific/GF25519Reflective/Reified/Mul 0m08.00s \| BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate 0m07.67s \| SpecificGen/GF5211_32Reflective/Reified/CarryAdd 0m07.33s \| SpecificGen/GF41417_32Reflective/Reified/CarrySub 0m07.02s \| MxDHRepChange 0m06.82s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate 0m06.74s \| SpecificGen/GF5211_32Reflective/Reified/CarryOpp 0m06.68s \| SpecificGen/GF2519_32Reflective 0m06.61s \| Reflection/Z/InterpretationsGen 0m06.54s \| SpecificGen/GF25519_32Reflective 0m06.36s \| Specific/GF25519Reflective 0m06.34s \| SpecificGen/GF41417_32Reflective/Reified/CarryAdd 0m06.09s \| Bedrock/Word 0m05.85s \| SpecificGen/GF41417_32Reflective/Reified/CarryOpp 0m05.80s \| SpecificGen/GF2213_32BoundedCommon 0m05.70s \| SpecificGen/GF2213_32Reflective/Reified/Mul 0m05.50s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub 0m05.46s \| Reflection/Z/Interpretations128/RelationsCombinations 0m05.46s \| Reflection/Z/Interpretations64/RelationsCombinations 0m05.41s \| Experiments/GenericFieldPow 0m05.38s \| Specific/SC25519 0m05.34s \| Util/ListUtil 0m05.26s \| SpecificGen/GF2213_32Reflective 0m05.24s \| ModularArithmetic/ModularBaseSystemListProofs 0m05.06s \| SpecificGen/GF5211_32Reflective/Reified/Pack 0m04.88s \| SpecificGen/GF5211_32Reflective/Reified/Unpack 0m04.86s \| SpecificGen/GF5211_32Reflective/Reified/Sub 0m04.82s \| WeierstrassCurve/Pre 0m04.74s \| SpecificGen/GF25519_32Reflective/CommonBinOp 0m04.70s \| SpecificGen/GF2519_32Reflective/CommonBinOp 0m04.67s \| SpecificGen/GF5211_32Reflective/Common 0m04.61s \| SpecificGen/GF2519_32Reflective/Reified/PreFreeze 0m04.60s \| SpecificGen/GF25519_32Reflective/Reified/PreFreeze 0m04.58s \| Specific/GF25519Reflective/Reified/PreFreeze 0m04.54s \| Specific/GF25519Reflective/CommonBinOp 0m04.31s \| SpecificGen/GF25519_64BoundedCommon 0m04.19s \| Specific/GF25519Reflective/CommonUnOp 0m04.15s \| SpecificGen/GF25519_32Reflective/CommonUnOp 0m04.11s \| Reflection/LinearizeWf 0m04.10s \| SpecificGen/GF41417_32Reflective/Reified/Pack 0m04.10s \| SpecificGen/GF2519_32Reflective/CommonUnOp 0m04.04s \| SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE 0m04.01s \| Specific/GF25519Reflective/CommonUnOpWireToFE 0m04.01s \| SpecificGen/GF5211_32Reflective/Reified/Add 0m04.00s \| SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE 0m03.98s \| SpecificGen/GF41417_32Reflective/Reified/Sub 0m03.98s \| ModularArithmetic/BarrettReduction/ZHandbook 0m03.94s \| BaseSystemProofs 0m03.88s \| SpecificGen/GF41417_32Reflective/Reified/Unpack 0m03.79s \| Encoding/PointEncodingPre 0m03.70s \| SpecificGen/GF2213_32Reflective/Reified/PreFreeze 0m03.57s \| SpecificGen/GF5211_32Reflective/Reified/Opp 0m03.52s \| CompleteEdwardsCurve/Pre 0m03.46s \| SpecificGen/GF2519_32Reflective/Reified/CarrySub 0m03.45s \| SpecificGen/GF25519_32Reflective/Reified/CarrySub 0m03.42s \| ModularArithmetic/Tutorial 0m03.41s \| SpecificGen/GF41417_32Reflective/Reified/Add 0m03.41s \| BoundedArithmetic/InterfaceProofs 0m03.38s \| SpecificGen/GF41417_32Reflective/Common 0m03.36s \| Specific/GF25519Reflective/Reified/CarrySub 0m03.18s \| ModularArithmetic/BarrettReduction/ZGeneralized 0m03.16s \| SpecificGen/GF2519_32Reflective/Reified/CarryOpp 0m03.15s \| ModularArithmetic/ZBoundedZ 0m03.10s \| SpecificGen/GF25519_64Reflective/Reified/PreFreeze 0m03.10s \| SpecificGen/GF25519_32Reflective/Reified/CarryOpp 0m03.09s \| SpecificGen/GF25519_64Reflective/Reified/Mul 0m03.08s \| SpecificGen/GF2519_32Reflective/Reified/CarryAdd 0m03.07s \| SpecificGen/GF41417_32Reflective/Reified/Opp 0m03.06s \| Specific/GF25519Reflective/Reified/CarryOpp 0m03.05s \| Specific/GF25519Reflective/Reified/CarryAdd 0m03.04s \| SpecificGen/GF25519_32Reflective/Reified/CarryAdd 0m02.96s \| SpecificGen/GF5211_32Reflective/Reified/GeModulus 0m02.92s \| SpecificGen/GF2213_32Reflective/CommonBinOp 0m02.91s \| BoundedArithmetic/Double/Proofs/Decode 0m02.77s \| SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire 0m02.75s \| SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire 0m02.74s \| SpecificGen/GF2213_32Reflective/Reified/CarrySub 0m02.72s \| BoundedArithmetic/Double/Proofs/ShiftRight 0m02.71s \| Specific/GF25519Reflective/CommonUnOpFEToWire 0m02.66s \| ModularArithmetic/ModularArithmeticTheorems 0m02.63s \| Assembly/State 0m02.62s \| BoundedArithmetic/Double/Proofs/ShiftLeft 0m02.60s \| SpecificGen/GF2213_32Reflective/CommonUnOp 0m02.60s \| SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE 0m02.56s \| SpecificGen/GF2213_32Reflective/Reified/CarryOpp 0m02.54s \| SpecificGen/GF25519_64Reflective/Reified/CarrySub 0m02.54s \| SpecificGen/GF41417_32Reflective/Reified/GeModulus 0m02.46s \| SpecificGen/GF2213_32Reflective/Reified/CarryAdd 0m02.39s \| SpecificGen/GF25519_64Reflective/Reified/CarryOpp 0m02.36s \| ModularArithmetic/BarrettReduction/ZBounded 0m02.28s \| ModularArithmetic/ModularBaseSystemOpt 0m02.26s \| SpecificGen/GF2519_32Reflective/Reified/Unpack 0m02.25s \| SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire 0m02.20s \| SpecificGen/GF2519_32Reflective/Reified/Pack 0m02.19s \| SpecificGen/GF25519_64Reflective/Reified/CarryAdd 0m02.16s \| SpecificGen/GF25519_32Reflective/Reified/Unpack 0m02.16s \| Specific/FancyMachine256/Montgomery 0m02.14s \| Specific/GF25519Reflective/Reified/Pack 0m02.11s \| Specific/FancyMachine256/Barrett 0m02.08s \| Specific/GF25519Reflective/Reified/Unpack 0m02.08s \| SpecificGen/GF25519_32Reflective/Reified/Pack 0m02.05s \| SpecificGen/GF25519_32Reflective/Reified/Sub 0m02.02s \| Specific/GF25519Reflective/Reified/Sub 0m02.01s \| SpecificGen/GF2519_32Reflective/Reified/Sub 0m01.99s \| Reflection/WfReflective 0m01.96s \| SpecificGen/GF2213_32Reflective/Reified/Pack 0m01.94s \| Assembly/Evaluables 0m01.93s \| Reflection/WfProofs 0m01.92s \| SpecificGen/GF2213_32Reflective/Reified/Unpack 0m01.87s \| Specific/FancyMachine256/Core 0m01.86s \| Util/WordUtil 0m01.83s \| SpecificGen/GF2519_32Reflective/Reified/Opp 0m01.82s \| ModularArithmetic/Montgomery/ZBounded 0m01.79s \| Specific/GF25519Reflective/Reified/Add 0m01.78s \| Specific/GF25519Reflective/Reified/Opp 0m01.77s \| SpecificGen/GF25519_64Reflective/Reified/Pack 0m01.77s \| SpecificGen/GF2213_32Reflective/Reified/Sub 0m01.77s \| SpecificGen/GF2519_32Reflective/Reified/Add 0m01.76s \| SpecificGen/GF25519_32Reflective/Reified/Opp 0m01.70s \| SpecificGen/GF25519_64Reflective/Reified/Unpack 0m01.68s \| Reflection/InlineWf 0m01.67s \| SpecificGen/GF25519_32Reflective/Reified/Add 0m01.67s \| SpecificGen/GF25519_32Reflective/Reified/GeModulus 0m01.65s \| SpecificGen/GF25519_64Reflective/CommonBinOp 0m01.63s \| Reflection/InlineInterp 0m01.63s \| SpecificGen/GF2519_32Reflective/Reified/GeModulus 0m01.62s \| Assembly/Compile 0m01.61s \| Specific/GF25519Reflective/Reified/GeModulus 0m01.60s \| Experiments/Ed25519Extraction 0m01.59s \| SpecificGen/GF25519_32Reflective/Common 0m01.55s \| SpecificGen/GF2213_32Reflective/Reified/Opp 0m01.54s \| Specific/GF25519Reflective/Common 0m01.54s \| Assembly/WordizeUtil 0m01.52s \| SpecificGen/GF25519_64Reflective/Reified/GeModulus 0m01.52s \| SpecificGen/GF2519_32Reflective/Common 0m01.50s \| ModularArithmetic/BarrettReduction/Z 0m01.50s \| SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ 0m01.48s \| SpecificGen/GF2213_32Reflective/Reified/Add 0m01.46s \| SpecificGen/GF25519_64Reflective/CommonUnOp 0m01.45s \| SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE 0m01.42s \| SpecificGen/GF2213_32Reflective/Reified/GeModulus 0m01.40s \| SpecificGen/GF25519_64Reflective/Reified/Opp 0m01.40s \| SpecificGen/GF25519_64Reflective/Reified/Sub 0m01.39s \| Reflection/TestCase 0m01.39s \| Util/NatUtil 0m01.39s \| SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire 0m01.36s \| ModularArithmetic/PrimeFieldTheorems 0m01.32s \| Assembly/Bounds 0m01.32s \| SpecificGen/GF2213_32Reflective/Common 0m01.28s \| Assembly/Conversions 0m01.26s \| SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ 0m01.24s \| ModularArithmetic/ExtendedBaseVector 0m01.18s \| BaseSystem 0m01.16s \| SpecificGen/GF25519_64Reflective/Reified/Add 0m01.16s \| Util/Tuple 0m01.15s \| SpecificGen/GF25519_64Reflective/Common 0m01.15s \| BoundedArithmetic/Double/Repeated/Proofs/Decode 0m01.09s \| SpecificGen/GF5211_32Reflective/Reified 0m01.05s \| SpecificGen/GF41417_32Reflective/Reified 0m01.01s \| Assembly/LL 0m00.99s \| Specific/GF25519Reflective/CommonUnOpFEToZ 0m00.96s \| Assembly/Pipeline 0m00.94s \| SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ 0m00.94s \| SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ 0m00.89s \| Util/NumTheoryUtil 0m00.89s \| Assembly/HL 0m00.88s \| BoundedArithmetic/Double/Proofs/LoadImmediate 0m00.88s \| Assembly/PhoasCommon 0m00.88s \| BoundedArithmetic/Double/Proofs/BitwiseOr 0m00.88s \| SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ 0m00.86s \| Util/IterAssocOp 0m00.84s \| SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ 0m00.79s \| BoundedArithmetic/X86ToZLikeProofs 0m00.77s \| ModularArithmetic/ModularBaseSystem 0m00.75s \| Assembly/QhasmEvalCommon 0m00.75s \| SpecificGen/GF2519_32Reflective/Reified 0m00.73s \| Specific/GF25519Reflective/Reified 0m00.72s \| SpecificGen/GF25519_32Reflective/Reified 0m00.71s \| Util/PartiallyReifiedProp 0m00.70s \| SpecificGen/GF2213_32Reflective/Reified 0m00.70s \| SpecificGen/GF25519_64Reflective/Reified 0m00.69s \| ModularArithmetic/PseudoMersenneBaseParamProofs 0m00.68s \| Reflection/Z/Syntax 0m00.66s \| ModularArithmetic/ExtPow2BaseMulProofs 0m00.65s \| Reflection/InterpWfRel 0m00.64s \| Util/AdditionChainExponentiation 0m00.63s \| BoundedArithmetic/Double/Proofs/SelectConditional 0m00.62s \| Encoding/ModularWordEncodingTheorems 0m00.62s \| BoundedArithmetic/Double/Repeated/Proofs/Multiply 0m00.61s \| Encoding/ModularWordEncodingPre 0m00.60s \| ModularArithmetic/ModularBaseSystemList 0m00.60s \| Spec/EdDSA 0m00.60s \| Spec/ModularWordEncoding 0m00.58s \| BoundedArithmetic/Interface 0m00.58s \| BoundedArithmetic/X86ToZLike 0m00.57s \| Reflection/WfReflectiveGen 0m00.56s \| Assembly/Qhasm 0m00.55s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub 0m00.54s \| Reflection/Syntax 0m00.54s \| Reflection/LinearizeInterp 0m00.54s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr 0m00.50s \| BoundedArithmetic/ArchitectureToZLike 0m00.50s \| Assembly/StringConversion 0m00.48s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional 0m00.48s \| ModularArithmetic/Pow2Base 0m00.48s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight 0m00.48s \| Util/Decidable 0m00.48s \| Reflection/Z/Reify 0m00.48s \| Reflection/CommonSubexpressionElimination 0m00.47s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate 0m00.47s \| BoundedArithmetic/Double/Repeated/Core 0m00.47s \| Reflection/InterpProofs 0m00.47s \| Reflection/Z/Interpretations128 0m00.47s \| Reflection/InterpWf 0m00.46s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate 0m00.46s \| BoundedArithmetic/Double/Core 0m00.46s \| BoundedArithmetic/StripCF 0m00.46s \| Util/HList 0m00.46s \| BoundedArithmetic/Eta 0m00.45s \| Reflection/Z/Interpretations64 0m00.45s \| ModularArithmetic/ZBounded 0m00.45s \| Assembly/QhasmUtil 0m00.44s \| ModularArithmetic/Pre 0m00.44s \| BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic 0m00.44s \| Reflection/Conversion 0m00.44s \| Reflection/WfRel 0m00.44s \| ModularArithmetic/ModularBaseSystemListZOperationsProofs 0m00.43s \| Spec/CompleteEdwardsCurve 0m00.43s \| Reflection/FilterLive 0m00.42s \| Reflection/MapInterpWf 0m00.42s \| Reflection/Named/EstablishLiveness 0m00.42s \| Reflection/InputSyntax 0m00.42s \| Spec/WeierstrassCurve 0m00.42s \| Reflection/Application 0m00.42s \| ModularArithmetic/Montgomery/Z 0m00.41s \| Spec/ModularArithmetic 0m00.40s \| Reflection/Named/RegisterAssign 0m00.40s \| Reflection/Named/Compile 0m00.40s \| Reflection/Named/Syntax 0m00.40s \| Reflection/MapInterp 0m00.39s \| ModularArithmetic/ModularBaseSystemWord 0m00.39s \| ModularArithmetic/ModularBaseSystemListZOperations 0m00.38s \| Reflection/Linearize 0m00.38s \| Tactics/Algebra_syntax/Nsatz 0m00.38s \| Spec/MxDH 0m00.37s \| Reflection/Inline 0m00.37s \| Reflection/Reify 0m00.36s \| ModularArithmetic/PseudoMersenneBaseParams 0m00.36s \| Reflection/Named/DeadCodeElimination 0m00.35s \| Reflection/CountLets 0m00.34s \| Reflection/Named/ContextOn 0m00.33s \| Reflection/Named/NameUtil 0m00.29s \| Bedrock/Nomega 0m00.27s \| Assembly/QhasmCommon 0m00.22s \| Util/CaseUtil 0m00.22s \| Util/Sum 0m00.19s \| Experiments/ExtrHaskellNats 0m00.13s \| Util/Relations 0m00.11s \| Util/Sigma 0m00.09s \| Util/Prod 0m00.09s \| Util/Option 0m00.08s \| Util/PointedProp 0m00.06s \| Util/Equality 0m00.04s \| Util/LetIn 0m00.04s \| Util/HProp 0m00.04s \| Util/Bool 0m00.04s \| Util/IffT 0m00.04s \| Util/Tactics 0m00.03s \| Tactics/VerdiTactics 0m00.03s \| Util/Notations 0m00.03s \| Util/Unit 0m00.03s \| Util/Logic 0m00.02s \| Encoding/EncodingTheorems 0m00.02s \| Util/Isomorphism 0m00.02s \| Util/GlobalSettings 0m00.02s \| Spec/Encoding 0m00.02s \| Util/AutoRewrite 0m00.02s \| Util/FixCoqMistakes
*	Fix sqrt handling in specificgen	Jason Gross	2016-11-14
\|
*	Handle both kinds of sqrt	Jason Gross	2016-11-14
\|
*	More generic sqrt in SpecificGen	Jason Gross	2016-11-14
\|