fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add [f] to things that use [exprf] or [flat_type]	Jason Gross	2016-10-31
\|
*	Implicits for SmartVarMapT	Jason Gross	2016-10-31
\|
*	Make it so that changing the list of wire bounds doesn't break the build	Jason Gross	2016-10-31
\|
*	Add SmartVarMapT	Jason Gross	2016-10-31
\|
*	Revert "Switch from word to Z"	Jason Gross	2016-10-31
\| \| \| \|	This reverts commit ac46ff22a9f6a279068ebdb897498e8dd14b1916.
*	Switch from word to Z	Jason Gross	2016-10-31
\|
*	Switch to reflective bounded word in Ed25519	Jason Gross	2016-10-31
\| \| \| \|	(cc @andres-erbsen)
*	Safer definitions of shl, shr	Jason Gross	2016-10-31
\|
*	Fix a typo making word calculations wrong	Jason Gross	2016-10-31
\|
*	Use sigma types to fix extraction	Jason Gross	2016-10-31
\| \| \| \| \| \| \|	This should get rid of the extra data being carried around after extraction. (cc @andres-erbsen)
*	Silence a warning	Jason Gross	2016-10-31
\|
*	Significantly faster wordToN, I hope	Jason Gross	2016-10-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change -------------------------------------------------------------------------------------- 3m22.43s \| Total \| 3m22.13s \|\| +0m00.30s -------------------------------------------------------------------------------------- 0m34.51s \| Spec/Ed25519 \| 0m34.56s \|\| -0m00.05s 0m28.83s \| Experiments/Ed25519 \| 0m28.60s \|\| +0m00.22s 0m17.28s \| EdDSARepChange \| 0m17.25s \|\| +0m00.03s 0m08.66s \| [require-in-module,deprecated] src/Assembly/GF25519 \| 0m08.66s \|\| +0m00.00s 0m08.46s \| Encoding/PointEncoding \| 0m08.47s \|\| -0m00.00s 0m08.35s \| Specific/GF25519BoundedCommonWord \| 0m08.44s \|\| -0m00.08s 0m07.74s \| Specific/GF25519Reflective \| 0m07.69s \|\| +0m00.04s 0m07.59s \| Specific/GF25519Reflective/Reified/Mul \| 0m07.65s \|\| -0m00.06s 0m07.35s \| Specific/GF25519BoundedCommon \| 0m07.39s \|\| -0m00.04s 0m06.88s \| Specific/GF25519Reflective/Reified/Freeze \| 0m06.86s \|\| +0m00.01s 0m05.80s \| Bedrock/Word \| 0m05.74s \|\| +0m00.05s 0m05.43s \| Specific/SC25519 \| 0m05.32s \|\| +0m00.10s 0m04.76s \| Reflection/Z/Interpretations \| 0m04.65s \|\| +0m00.10s 0m04.27s \| Encoding/PointEncodingPre \| 0m04.31s \|\| -0m00.04s 0m03.72s \| Assembly/GF25519BoundedInstantiation \| 0m03.68s \|\| +0m00.04s 0m03.21s \| Specific/GF25519Reflective/Reified/CarrySub \| 0m03.34s \|\| -0m00.12s 0m02.91s \| Specific/GF25519Reflective/Reified/CarryOpp \| 0m02.86s \|\| +0m00.05s 0m02.84s \| Specific/GF25519Reflective/Reified/CarryAdd \| 0m02.87s \|\| -0m00.03s 0m02.70s \| Assembly/State \| 0m02.67s \|\| +0m00.03s 0m02.00s \| Specific/GF25519Reflective/Reified/Unpack \| 0m01.96s \|\| +0m00.04s 0m01.97s \| Specific/GF25519Reflective/Reified/Sub \| 0m01.95s \|\| +0m00.02s 0m01.95s \| Specific/GF25519Reflective/Reified/Pack \| 0m02.03s \|\| -0m00.07s 0m01.81s \| Assembly/Evaluables \| 0m01.88s \|\| -0m00.06s 0m01.78s \| Specific/GF25519Bounded \| 0m01.77s \|\| +0m00.01s 0m01.71s \| Specific/GF25519Reflective/Reified/Opp \| 0m01.68s \|\| +0m00.03s 0m01.66s \| Specific/GF25519Reflective/Reified/Add \| 0m01.66s \|\| +0m00.00s 0m01.52s \| Assembly/Compile \| 0m01.48s \|\| +0m00.04s 0m01.49s \| Specific/GF25519Reflective/Reified/GeModulus \| 0m01.48s \|\| +0m00.01s 0m01.44s \| Assembly/WordizeUtil \| 0m01.51s \|\| -0m00.07s 0m01.33s \| Assembly/Bounds \| 0m01.34s \|\| -0m00.01s 0m01.22s \| Assembly/Conversions \| 0m01.23s \|\| -0m00.01s 0m01.05s \| Util/WordUtil \| 0m01.03s \|\| +0m00.02s 0m00.94s \| Assembly/LL \| 0m00.94s \|\| +0m00.00s 0m00.94s \| Assembly/Pipeline \| 0m00.90s \|\| +0m00.03s 0m00.87s \| Assembly/HL \| 0m00.89s \|\| -0m00.02s 0m00.81s \| Assembly/PhoasCommon \| 0m00.77s \|\| +0m00.04s 0m00.79s \| Assembly/QhasmEvalCommon \| 0m00.83s \|\| -0m00.03s 0m00.75s \| Specific/GF25519Reflective/Reified \| 0m00.80s \|\| -0m00.05s 0m00.72s \| Specific/GF25519Reflective/Common \| 0m00.71s \|\| +0m00.01s 0m00.70s \| Encoding/ModularWordEncodingTheorems \| 0m00.65s \|\| +0m00.04s 0m00.66s \| Spec/EdDSA \| 0m00.66s \|\| +0m00.00s 0m00.61s \| Spec/ModularWordEncoding \| 0m00.58s \|\| +0m00.03s 0m00.61s \| Encoding/ModularWordEncodingPre \| 0m00.67s \|\| -0m00.06s 0m00.51s \| Assembly/Qhasm \| 0m00.51s \|\| +0m00.00s 0m00.48s \| Assembly/StringConversion \| 0m00.50s \|\| -0m00.02s 0m00.47s \| Assembly/QhasmUtil \| 0m00.40s \|\| +0m00.06s 0m00.36s \| Assembly/QhasmCommon \| 0m00.31s \|\| +0m00.04s
*	Add src/Specific/GF25519Reflective.v	Jason Gross	2016-10-31
\|
*	Interpret syntax with Let_In	Jason Gross	2016-10-31
\|
*	Also construct relatedness proofs in reified	Jason Gross	2016-10-30
\|
*	Fix tactic notation scope in the 8.5 build	Jason Gross	2016-10-30
\|
*	Fix for 8.5 build?	Jason Gross	2016-10-30
\|
*	Proved eq_enc_E_iff	jadep	2016-10-30
\|
*	Fix some subtleties with equalities in point encodings	jadep	2016-10-30
\|
*	Added new algebra lemma	jadep	2016-10-30
\|
*	Remove an [About]	Jason Gross	2016-10-30
\|
*	Renaming in Reflection/Z/Interpretations.v, admitted rel lemmas	Jason Gross	2016-10-30
\|
*	Switch to a faster way of proving wf	Jason Gross	2016-10-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	By keeping more data in the reified side-condition, we can reflectively replace all side conditions of the form [x = y] with [x = x], and check via vm_cast that this does not change the side condition. This is empirically a cheap check, and since we can prove that all propositions become true under this sort of replacement, we get most of our proof for free. After \| File Name \| Before \|\| Change ----------------------------------------------------------------------------------------------------------- 12m15.26s \| Total \| 12m34.17s \|\| -0m18.90s ----------------------------------------------------------------------------------------------------------- 0m06.92s \| Specific/GF25519Reflective/Reified/Mul \| 0m14.58s \|\| -0m07.66s 0m05.99s \| Specific/GF25519Reflective/Reified/Freeze \| 0m10.74s \|\| -0m04.75s N/A \| Reflection/WfRelReflective \| 0m04.05s \|\| -0m04.04s 0m02.00s \| Reflection/WfReflective \| 0m04.05s \|\| -0m02.04s 1m17.14s \| CompleteEdwardsCurve/ExtendedCoordinates \| 1m16.12s \|\| +0m01.01s 1m32.08s \| Test/Curve25519SpecTestVectors \| 1m32.06s \|\| +0m00.01s 0m40.68s \| ModularArithmetic/Conversion \| 0m40.54s \|\| +0m00.14s 0m34.50s \| Spec/Ed25519 \| 0m34.74s \|\| -0m00.24s 0m30.28s \| ModularArithmetic/ModularBaseSystemProofs \| 0m30.33s \|\| -0m00.04s 0m29.06s \| Experiments/Ed25519 \| 0m29.43s \|\| -0m00.37s 0m23.05s \| Experiments/MontgomeryCurve \| 0m22.85s \|\| +0m00.19s 0m22.37s \| Specific/GF25519 \| 0m22.28s \|\| +0m00.08s 0m22.06s \| ModularArithmetic/Pow2BaseProofs \| 0m22.08s \|\| -0m00.01s 0m20.17s \| Algebra \| 0m20.11s \|\| +0m00.06s 0m17.10s \| EdDSARepChange \| 0m17.21s \|\| -0m00.10s 0m16.85s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m17.03s \|\| -0m00.17s 0m13.86s \| Util/ZUtil \| 0m13.72s \|\| +0m00.13s 0m09.98s \| Testbit \| 0m10.03s \|\| -0m00.04s 0m08.94s \| [require-in-module,deprecated] src/Assembly/GF25519 \| 0m09.08s \|\| -0m00.14s 0m08.81s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.71s \|\| +0m00.09s 0m08.45s \| BoundedArithmetic/ArchitectureToZLikeProofs \| 0m08.46s \|\| -0m00.01s 0m08.39s \| Specific/GF25519BoundedCommonWord \| 0m08.41s \|\| -0m00.01s 0m08.39s \| Specific/GF1305 \| 0m08.44s \|\| -0m00.04s 0m08.35s \| Encoding/PointEncoding \| 0m08.41s \|\| -0m00.06s 0m08.22s \| BoundedArithmetic/Double/Proofs/Multiply \| 0m08.25s \|\| -0m00.02s 0m07.76s \| BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate \| 0m07.77s \|\| -0m00.00s 0m07.18s \| Specific/GF25519BoundedCommon \| 0m07.34s \|\| -0m00.16s 0m06.80s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate \| 0m07.03s \|\| -0m00.23s 0m06.10s \| Bedrock/Word \| 0m06.08s \|\| +0m00.01s 0m05.45s \| Specific/SC25519 \| 0m05.44s \|\| +0m00.00s 0m05.44s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub \| 0m05.49s \|\| -0m00.04s 0m05.40s \| Util/ListUtil \| 0m05.38s \|\| +0m00.02s 0m05.32s \| Experiments/GenericFieldPow \| 0m05.31s \|\| +0m00.01s 0m04.81s \| WeierstrassCurve/Pre \| 0m04.82s \|\| -0m00.01s 0m04.76s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m04.84s \|\| -0m00.08s 0m04.40s \| Reflection/Z/Interpretations \| 0m04.48s \|\| -0m00.08s 0m04.22s \| Reflection/LinearizeWf \| 0m04.21s \|\| +0m00.00s 0m03.92s \| BaseSystemProofs \| 0m03.88s \|\| +0m00.04s 0m03.91s \| Assembly/GF25519BoundedInstantiation \| 0m03.78s \|\| +0m00.13s 0m03.83s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.90s \|\| -0m00.06s 0m03.67s \| ModularArithmetic/Tutorial \| 0m03.53s \|\| +0m00.14s 0m03.56s \| CompleteEdwardsCurve/Pre \| 0m03.50s \|\| +0m00.06s 0m03.36s \| BoundedArithmetic/InterfaceProofs \| 0m03.30s \|\| +0m00.06s 0m03.03s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.12s \|\| -0m00.09s 0m02.92s \| BoundedArithmetic/Double/Proofs/Decode \| 0m02.90s \|\| +0m00.02s 0m02.89s \| ModularArithmetic/ZBoundedZ \| 0m02.84s \|\| +0m00.05s 0m02.86s \| Specific/GF25519Reflective/Reified/CarrySub \| 0m03.15s \|\| -0m00.29s 0m02.85s \| Encoding/PointEncodingPre \| 0m02.87s \|\| -0m00.02s 0m02.62s \| Assembly/State \| 0m02.71s \|\| -0m00.08s 0m02.61s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.60s \|\| +0m00.00s 0m02.54s \| BoundedArithmetic/Double/Proofs/ShiftLeft \| 0m02.60s \|\| -0m00.06s 0m02.53s \| BoundedArithmetic/Double/Proofs/ShiftRight \| 0m02.50s \|\| +0m00.02s 0m02.52s \| Specific/GF25519Reflective/Reified/CarryOpp \| 0m03.00s \|\| -0m00.48s 0m02.51s \| Specific/GF25519Reflective/Reified/CarryAdd \| 0m02.50s \|\| +0m00.00s 0m02.38s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.34s \|\| +0m00.04s 0m02.28s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.30s \|\| -0m00.02s 0m02.16s \| Specific/FancyMachine256/Montgomery \| 0m02.07s \|\| +0m00.09s 0m02.13s \| Specific/FancyMachine256/Barrett \| 0m02.18s \|\| -0m00.05s 0m01.93s \| Reflection/WfProofs \| 0m01.89s \|\| +0m00.04s 0m01.84s \| Assembly/Evaluables \| 0m02.00s \|\| -0m00.15s 0m01.84s \| Specific/FancyMachine256/Core \| 0m01.91s \|\| -0m00.06s 0m01.84s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.79s \|\| +0m00.05s 0m01.79s \| Specific/GF25519Bounded \| 0m01.74s \|\| +0m00.05s 0m01.79s \| Specific/GF25519Reflective/Reified/Sub \| 0m01.66s \|\| +0m00.13s 0m01.78s \| Specific/GF25519Reflective/Reified/Pack \| 0m01.80s \|\| -0m00.02s 0m01.76s \| Reflection/InlineWf \| 0m01.69s \|\| +0m00.07s 0m01.68s \| Specific/GF25519Reflective/Reified/Unpack \| 0m01.71s \|\| -0m00.03s 0m01.55s \| Reflection/InlineInterp \| 0m01.58s \|\| -0m00.03s 0m01.53s \| ModularArithmetic/BarrettReduction/Z \| 0m01.55s \|\| -0m00.02s 0m01.51s \| Specific/GF25519Reflective/Reified/Add \| 0m01.29s \|\| +0m00.21s 0m01.48s \| Specific/GF25519Reflective/Reified/Opp \| 0m01.49s \|\| -0m00.01s 0m01.47s \| Assembly/WordizeUtil \| 0m01.52s \|\| -0m00.05s 0m01.45s \| Assembly/Compile \| 0m01.45s \|\| +0m00.00s 0m01.43s \| Reflection/TestCase \| 0m01.44s \|\| -0m00.01s 0m01.42s \| Specific/GF25519Reflective/Reified/GeModulus \| 0m01.34s \|\| +0m00.07s 0m01.41s \| Util/NatUtil \| 0m01.39s \|\| +0m00.02s 0m01.32s \| Assembly/Bounds \| 0m01.33s \|\| -0m00.01s 0m01.31s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.27s \|\| +0m00.04s 0m01.18s \| ModularArithmetic/ExtendedBaseVector \| 0m01.11s \|\| +0m00.06s 0m01.17s \| BaseSystem \| 0m01.16s \|\| +0m00.01s 0m01.15s \| Assembly/Conversions \| 0m01.12s \|\| +0m00.02s 0m01.08s \| BoundedArithmetic/Double/Repeated/Proofs/Decode \| 0m01.11s \|\| -0m00.03s 0m01.00s \| Assembly/Pipeline \| 0m01.00s \|\| +0m00.00s 0m00.99s \| Util/WordUtil \| 0m01.07s \|\| -0m00.08s 0m00.98s \| Assembly/HL \| 0m01.04s \|\| -0m00.06s 0m00.98s \| Assembly/LL \| 0m01.00s \|\| -0m00.02s 0m00.98s \| BoundedArithmetic/Double/Proofs/BitwiseOr \| 0m00.91s \|\| +0m00.06s 0m00.97s \| Assembly/PhoasCommon \| 0m00.89s \|\| +0m00.07s 0m00.92s \| Util/NumTheoryUtil \| 0m00.91s \|\| +0m00.01s 0m00.87s \| BoundedArithmetic/X86ToZLikeProofs \| 0m00.80s \|\| +0m00.06s 0m00.83s \| BoundedArithmetic/Double/Proofs/LoadImmediate \| 0m00.86s \|\| -0m00.03s 0m00.78s \| Specific/GF25519Reflective/Reified \| 0m00.68s \|\| +0m00.09s 0m00.78s \| Util/IterAssocOp \| 0m00.78s \|\| +0m00.00s 0m00.77s \| Specific/GF25519Reflective/Common \| 0m00.70s \|\| +0m00.07s 0m00.76s \| Assembly/QhasmEvalCommon \| 0m00.78s \|\| -0m00.02s 0m00.75s \| Util/PartiallyReifiedProp \| 0m00.74s \|\| +0m00.01s 0m00.72s \| Encoding/ModularWordEncodingTheorems \| 0m00.62s \|\| +0m00.09s 0m00.72s \| Util/Tuple \| 0m00.72s \|\| +0m00.00s 0m00.66s \| ModularArithmetic/ModularBaseSystem \| 0m00.64s \|\| +0m00.02s 0m00.63s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.63s \|\| +0m00.00s 0m00.62s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.70s \|\| -0m00.07s 0m00.61s \| Util/AdditionChainExponentiation \| 0m00.60s \|\| +0m00.01s 0m00.61s \| Reflection/LinearizeInterp \| 0m00.51s \|\| +0m00.09s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.58s \|\| +0m00.02s 0m00.60s \| BoundedArithmetic/Double/Repeated/Proofs/Multiply \| 0m00.61s \|\| -0m00.01s 0m00.60s \| ModularArithmetic/ModularBaseSystemList \| 0m00.61s \|\| -0m00.01s 0m00.60s \| Spec/EdDSA \| 0m00.60s \|\| +0m00.00s 0m00.58s \| Reflection/InterpWfRel \| 0m00.57s \|\| +0m00.01s 0m00.57s \| Reflection/WfReflectiveGen \| 0m00.60s \|\| -0m00.03s 0m00.56s \| BoundedArithmetic/Interface \| 0m00.65s \|\| -0m00.08s 0m00.56s \| Spec/ModularWordEncoding \| 0m00.72s \|\| -0m00.15s 0m00.56s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight \| 0m00.62s \|\| -0m00.05s 0m00.56s \| BoundedArithmetic/X86ToZLike \| 0m00.63s \|\| -0m00.06s 0m00.55s \| BoundedArithmetic/Double/Proofs/SelectConditional \| 0m00.54s \|\| +0m00.01s 0m00.52s \| BoundedArithmetic/Double/Repeated/Core \| 0m00.52s \|\| +0m00.00s 0m00.51s \| BoundedArithmetic/ArchitectureToZLike \| 0m00.42s \|\| +0m00.09s 0m00.50s \| Assembly/StringConversion \| 0m00.54s \|\| -0m00.04s 0m00.50s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub \| 0m00.49s \|\| +0m00.01s 0m00.50s \| ModularArithmetic/ZBounded \| 0m00.51s \|\| -0m00.01s 0m00.49s \| Assembly/Qhasm \| 0m00.53s \|\| -0m00.04s 0m00.49s \| Reflection/Z/Syntax \| 0m00.50s \|\| -0m00.01s 0m00.48s \| BoundedArithmetic/Double/Core \| 0m00.47s \|\| +0m00.01s 0m00.48s \| Reflection/Z/Reify \| 0m00.41s \|\| +0m00.07s 0m00.48s \| ModularArithmetic/Pre \| 0m00.48s \|\| +0m00.00s 0m00.48s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional \| 0m00.46s \|\| +0m00.01s 0m00.47s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate \| 0m00.62s \|\| -0m00.15s 0m00.47s \| Reflection/InterpWf \| 0m00.47s \|\| +0m00.00s 0m00.47s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate \| 0m00.47s \|\| +0m00.00s 0m00.46s \| Assembly/QhasmUtil \| 0m00.45s \|\| +0m00.01s 0m00.46s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr \| 0m00.49s \|\| -0m00.02s 0m00.46s \| Reflection/CommonSubexpressionElimination \| 0m00.44s \|\| +0m00.02s 0m00.45s \| Util/Decidable \| 0m00.54s \|\| -0m00.09s 0m00.44s \| BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic \| 0m00.42s \|\| +0m00.02s 0m00.44s \| Reflection/Conversion \| 0m00.42s \|\| +0m00.02s 0m00.44s \| Reflection/InterpProofs \| 0m00.45s \|\| -0m00.01s 0m00.44s \| BoundedArithmetic/Eta \| 0m00.39s \|\| +0m00.04s 0m00.42s \| Reflection/MapInterpWf \| 0m00.41s \|\| +0m00.01s 0m00.42s \| Reflection/Syntax \| 0m00.44s \|\| -0m00.02s 0m00.42s \| Spec/WeierstrassCurve \| 0m00.43s \|\| -0m00.01s 0m00.42s \| Reflection/Named/NameUtil \| 0m00.35s \|\| +0m00.07s 0m00.42s \| BoundedArithmetic/StripCF \| 0m00.48s \|\| -0m00.06s 0m00.42s \| Reflection/Named/RegisterAssign \| 0m00.41s \|\| +0m00.01s 0m00.42s \| Reflection/InputSyntax \| 0m00.42s \|\| +0m00.00s 0m00.42s \| Spec/MxDH \| 0m00.40s \|\| +0m00.01s 0m00.41s \| Reflection/CountLets \| 0m00.36s \|\| +0m00.04s 0m00.41s \| Reflection/Named/EstablishLiveness \| 0m00.36s \|\| +0m00.04s 0m00.40s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| -0m00.01s 0m00.39s \| Reflection/MapInterp \| 0m00.35s \|\| +0m00.04s 0m00.39s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.45s \|\| -0m00.06s 0m00.39s \| Reflection/Named/Syntax \| 0m00.42s \|\| -0m00.02s 0m00.38s \| Reflection/FilterLive \| 0m00.35s \|\| +0m00.03s 0m00.38s \| Spec/CompleteEdwardsCurve \| 0m00.44s \|\| -0m00.06s 0m00.38s \| Reflection/Named/DeadCodeElimination \| 0m00.36s \|\| +0m00.02s 0m00.38s \| Reflection/Linearize \| 0m00.38s \|\| +0m00.00s 0m00.37s \| Reflection/Inline \| 0m00.38s \|\| -0m00.01s 0m00.37s \| ModularArithmetic/Montgomery/Z \| 0m00.36s \|\| +0m00.01s 0m00.37s \| Reflection/WfRel \| 0m00.37s \|\| +0m00.00s 0m00.36s \| Assembly/QhasmCommon \| 0m00.31s \|\| +0m00.04s 0m00.35s \| Tactics/Algebra_syntax/Nsatz \| 0m00.37s \|\| -0m00.02s 0m00.35s \| Spec/ModularArithmetic \| 0m00.36s \|\| -0m00.01s 0m00.34s \| Reflection/Named/Compile \| 0m00.36s \|\| -0m00.01s 0m00.34s \| Reflection/Named/ContextOn \| 0m00.34s \|\| +0m00.00s 0m00.34s \| Reflection/Reify \| 0m00.35s \|\| -0m00.00s 0m00.28s \| Bedrock/Nomega \| 0m00.28s \|\| +0m00.00s 0m00.24s \| ModularArithmetic/ModularBaseSystemListZOperations \| 0m00.26s \|\| -0m00.02s 0m00.21s \| Util/Sum \| 0m00.24s \|\| -0m00.03s 0m00.19s \| Util/CaseUtil \| 0m00.22s \|\| -0m00.03s 0m00.18s \| Experiments/ExtrHaskellNats \| 0m00.17s \|\| +0m00.00s 0m00.13s \| Util/Relations \| 0m00.14s \|\| -0m00.01s 0m00.10s \| Util/Option \| 0m00.14s \|\| -0m00.04s 0m00.09s \| Util/PointedProp \| 0m00.08s \|\| +0m00.00s 0m00.08s \| Util/Sigma \| 0m00.10s \|\| -0m00.02s 0m00.08s \| Util/LetIn \| 0m00.04s \|\| +0m00.04s 0m00.05s \| Util/HProp \| 0m00.04s \|\| +0m00.01s 0m00.05s \| Util/Tactics \| 0m00.04s \|\| +0m00.01s 0m00.05s \| Util/Equality \| 0m00.04s \|\| +0m00.01s 0m00.04s \| Util/Prod \| 0m00.05s \|\| -0m00.01s 0m00.04s \| Util/AutoRewrite \| 0m00.04s \|\| +0m00.00s 0m00.03s \| Util/Unit \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Spec/Encoding \| 0m00.02s \|\| +0m00.00s 0m00.03s \| Util/Logic \| 0m00.03s \|\| +0m00.00s 0m00.02s \| Tactics/VerdiTactics \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Util/Notations \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Encoding/EncodingTheorems \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Util/Isomorphism \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/GlobalSettings \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/FixCoqMistakes \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Util/Bool \| 0m00.02s \|\| +0m00.00s
*	Add trueify to src/Util/PartiallyReifiedProp.v	Jason Gross	2016-10-30
\|
*	Add to_prop_and_reified_Prop	Jason Gross	2016-10-30
\|
*	Add break_innermost_match	Jason Gross	2016-10-30
\|
*	Fix a loop in PartiallyReifiedProp	Jason Gross	2016-10-30
\|
*	Generalize interp_flat_type_rel_pointwise2 a bit	Jason Gross	2016-10-30
\|
*	Minor changes to GF25519 reflective	Jason Gross	2016-10-30
\|
*	Add PartiallyReifiedProp	Jason Gross	2016-10-30
\|
*	Add reification of various operations	Jason Gross	2016-10-30
\| \| \| \| \|	We split the reification up into separate files, one operation per file, so that we can run all the reification in parallel when building.
*	Add initial work on reifying GF25519 stuff	Jason Gross	2016-10-30
\|
*	Handle 4 arguments in Reify	Jason Gross	2016-10-30
\|
*	remove commented-out lemma	jadep	2016-10-30
\|
*	revived accidentally deleted lemma	jadep	2016-10-30
\|
*	Revert "Premature optimization of [Reify_rhs]"	Jason Gross	2016-10-30
\| \| \| \| \| \| \|	This reverts commit 6ebe0ff5b046658b198c645e72b6484d2342c4cf. Leave it in version control, but don't apply this common subexpression elimination to proof terms unless we see that we need it.
*	Premature optimization of [Reify_rhs]	Jason Gross	2016-10-30
\| \| \| \|	This might or might not actually speed up proving things.
*	Fix slowness in [Defined] after [Reify_rhs]	Jason Gross	2016-10-30
\| \| \| \|	Do this by removing simplify_projections, which was messing with kernel reduction
*	Make Z Reification handle correctness proofs	Jason Gross	2016-10-30
\|
*	Factor out prove_compile_correct	Jason Gross	2016-10-30
\|
*	Adjust arguments to InputSyntax.Compile	Jason Gross	2016-10-30
\|
*	Generalize Reify a bit	Jason Gross	2016-10-30
\|
*	Generalize InputSyntax.Compile_correct	Jason Gross	2016-10-30
\|
*	Factor Reify_rhs so that it's more reusable	Jason Gross	2016-10-30
\|
*	framework for l_order_B	Andres Erbsen	2016-10-30
\|
*	Minor reflective changes	Jason Gross	2016-10-30
\|
*	proved feSign_correct	jadep	2016-10-29
\|
*	proved Proper_feSign	jadep	2016-10-29
\|
*	Fix an infinite loop	Jason Gross	2016-10-29
\|
*	Add things like app_7 to GF25519BoundedCommonWord.v	Jason Gross	2016-10-29
\|