fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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.
*	Support for 128-bit words	Jason Gross	2016-11-14
\| \| \| \| \|	I haven't found a good way to genericize the proofs of relatedness things, mostly because Modules and functors are annoying.
*	extraction: inline field operations into group operations	Andres Erbsen	2016-11-14
\|
*	Add mulW_noinline	Jason Gross	2016-11-14
\|
*	Proper_sqrt	Andres Erbsen	2016-11-13
\|
*	Remove extra admitted lemmas in 8.4	Jason Gross	2016-11-12
\|
*	GF25519: add ErepAdd	Andres Erbsen	2016-11-11
\|
*	[cbn] is 8.5 only	Jason Gross	2016-11-11
\|
*	Fix proofs broken by stronger preconditions	Jason Gross	2016-11-11
\|
*	Most of the admits in Ed25519.v	Rob Sloan	2016-11-11
\|
*	extraction less slow	Andres Erbsen	2016-11-11
\|
*	Work around looping in 8.4	Jason Gross	2016-11-10
\| \| \| \|	This fixes #96
*	Rewrite cast_word so that it's extracted better	Jason Gross	2016-11-09
\| \| \| \| \| \| \| \|	It will now be extracted as the identity function automatically, so we don't need to manually extract it as the empty string. This should also fix #93. (I think the issue was that this was an instance of https://coq.inria.fr/bugs/show_bug.cgi?id=4243.)
*	implement X25519	Andres Erbsen	2016-11-06
\|
*	move B_order_l and prime_q	Andres Erbsen	2016-11-06
\|
*	Connect [is_bounded] to [bounded_by]	Jason Gross	2016-11-06
\| \| \| \| \|	This hooks up the boundedness constraints on [freeze] in GF25519Bounded to those in Ed25519.
*	Work around a bug in 8.4 vm_compute	Jason Gross	2016-11-05
\|
*	put EdDSA encoding sign bit at the MSB	Andres Erbsen	2016-11-04
\|
*	fix extraction directives -- tested enc((l+1)B)=enc(B)	Andres Erbsen	2016-11-03
\|
*	separate Ed25519Extraction.v, add extraction to Makefile	Andres Erbsen	2016-11-03
\| \| \| \| \|	@JasonGross: src/Specific/GF25519Bounded.v has another constant that I think needs a extraction-friendly version, I added a comment
*	fix Word64 constants for extraction, check in more extraction directives	Andres Erbsen	2016-11-03
\|
*	Make [freeze] proofs consider machine integer width and hard input bounds ↵	jadep	2016-11-03
\| \| \| \|	separately
*	fix and prove ERepDec_correct	Andres Erbsen	2016-11-02
\|
*	Fix diverging Qed in 8.5{,pl1} ([f_equal] is broken)	Jason Gross	2016-11-02
\|
*	Fix broken proof	Jason Gross	2016-11-02
\| \| \| \|	See https://github.com/mit-plv/fiat-crypto/commit/254aa1f3ce33dd190f7fee8946fb3c950142aa4c#commitcomment-19671361
*	Fix a possibly-diverging Qed in 8.4 (feEnc_correct)	Jason Gross	2016-11-02
\|
*	Ed25519: use fully qualified names for [a] and [d]	Andres Erbsen	2016-11-02
\|
*	almost fix Ed25519 for 8.4	Andres Erbsen	2016-11-02
\|
*	even less fragile proofs	Andres Erbsen	2016-11-02
\|
*	improve some fragile proofs (built on 8.4)	Andres Erbsen	2016-11-02
\|
*	Proved feDec_correct modulo a few admits about Z	jadep	2016-11-02
\|
*	feDec_correct in progress, fully converted to Z operations	jadep	2016-11-02
\|
*	use correct version of WToZ_ZToW lemma	jadep	2016-11-02
\|
*	sqrt_correct reduced to a few admits	jadep	2016-11-02
\|
*	Progress proving ERepDec_correct (included tweaking preconditions for ↵	jadep	2016-11-02
\| \| \| \|	ModularBaseSystem sqrt_5mod8 proofs)
*	Fixed reversed tuple in feDec	jadep	2016-11-02
\|
*	Parameterize bounded things over the limb length	Jason Gross	2016-11-01
\| \| \| \| \| \| \| \| \| \|	It should now be possible to use sed to change to other limbs. Alas, there are a lot of files that need to be copied over (including about 5-10 in src/Specific/GF25519Reflective/Refied/) cc @jadep cc @andres-erbsen @jadep about my change to feDec
*	Add some interpretations things, speed up proofs in Ed25519	Jason Gross	2016-10-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ----------------------------------------------------------------------------------------------------------- 13m02.08s \| Total \| 15m13.67s \|\| -2m11.59s ----------------------------------------------------------------------------------------------------------- 0m34.08s \| Experiments/Ed25519 \| 3m15.96s \|\| -2m41.87s 1m27.34s \| CompleteEdwardsCurve/ExtendedCoordinates \| 1m18.08s \|\| +0m09.26s 0m47.66s \| ModularArithmetic/Conversion \| 0m40.15s \|\| +0m07.50s 1m37.25s \| Test/Curve25519SpecTestVectors \| 1m32.28s \|\| +0m04.96s 0m38.79s \| Spec/Ed25519 \| 0m34.76s \|\| +0m04.03s 0m30.44s \| ModularArithmetic/ModularBaseSystemProofs \| 0m30.30s \|\| +0m00.14s 0m23.38s \| Experiments/MontgomeryCurve \| 0m23.03s \|\| +0m00.34s 0m22.34s \| ModularArithmetic/Pow2BaseProofs \| 0m22.08s \|\| +0m00.26s 0m22.30s \| Specific/GF25519 \| 0m22.27s \|\| +0m00.03s 0m19.90s \| Algebra \| 0m20.14s \|\| -0m00.24s 0m17.70s \| EdDSARepChange \| 0m17.18s \|\| +0m00.51s 0m17.18s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m16.92s \|\| +0m00.25s 0m13.88s \| Util/ZUtil \| 0m13.76s \|\| +0m00.12s 0m10.20s \| Testbit \| 0m09.88s \|\| +0m00.31s 0m09.78s \| Specific/GF25519BoundedCommon \| 0m09.79s \|\| -0m00.00s 0m08.85s \| Assembly/GF25519 \| 0m08.92s \|\| -0m00.07s 0m08.80s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.67s \|\| +0m00.13s 0m08.69s \| BoundedArithmetic/ArchitectureToZLikeProofs \| 0m08.56s \|\| +0m00.12s 0m08.64s \| Encoding/PointEncoding \| 0m08.52s \|\| +0m00.12s 0m08.43s \| BoundedArithmetic/Double/Proofs/Multiply \| 0m08.30s \|\| +0m00.12s 0m08.38s \| Specific/GF1305 \| 0m08.44s \|\| -0m00.05s 0m07.85s \| BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate \| 0m07.80s \|\| +0m00.04s 0m07.74s \| Specific/GF25519Reflective/Reified/Mul \| 0m07.78s \|\| -0m00.04s 0m07.45s \| Specific/GF25519Bounded \| 0m07.66s \|\| -0m00.20s 0m07.38s \| Specific/GF25519Reflective \| 0m07.49s \|\| -0m00.11s 0m06.88s \| Specific/GF25519Reflective/Reified/Freeze \| 0m06.87s \|\| +0m00.00s 0m06.79s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate \| 0m06.78s \|\| +0m00.00s 0m06.31s \| Bedrock/Word \| 0m06.10s \|\| +0m00.20s 0m05.98s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub \| 0m05.40s \|\| +0m00.58s 0m05.52s \| Specific/SC25519 \| 0m05.46s \|\| +0m00.05s 0m05.40s \| Util/ListUtil \| 0m05.42s \|\| -0m00.01s 0m05.38s \| Experiments/GenericFieldPow \| 0m05.33s \|\| +0m00.04s 0m04.90s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m04.80s \|\| +0m00.10s 0m04.85s \| WeierstrassCurve/Pre \| 0m04.75s \|\| +0m00.09s 0m04.65s \| Reflection/Z/Interpretations \| 0m04.68s \|\| -0m00.02s 0m04.58s \| Encoding/PointEncodingPre \| 0m04.24s \|\| +0m00.33s 0m04.31s \| Reflection/LinearizeWf \| 0m04.32s \|\| -0m00.01s 0m03.96s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.92s \|\| +0m00.04s 0m03.92s \| BaseSystemProofs \| 0m04.00s \|\| -0m00.08s 0m03.52s \| CompleteEdwardsCurve/Pre \| 0m03.52s \|\| +0m00.00s 0m03.46s \| ModularArithmetic/Tutorial \| 0m03.40s \|\| +0m00.06s 0m03.46s \| BoundedArithmetic/InterfaceProofs \| 0m03.31s \|\| +0m00.14s 0m03.37s \| BoundedArithmetic/Double/Proofs/Decode \| 0m02.84s \|\| +0m00.53s 0m03.33s \| Specific/GF25519Reflective/Reified/CarrySub \| 0m03.26s \|\| +0m00.07s 0m03.28s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.15s \|\| +0m00.12s 0m02.91s \| Specific/GF25519Reflective/Reified/CarryOpp \| 0m03.02s \|\| -0m00.10s 0m02.88s \| Specific/GF25519Reflective/Reified/CarryAdd \| 0m02.88s \|\| +0m00.00s 0m02.86s \| ModularArithmetic/ZBoundedZ \| 0m02.86s \|\| +0m00.00s 0m02.68s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.64s \|\| +0m00.04s 0m02.67s \| Assembly/State \| 0m02.70s \|\| -0m00.03s 0m02.67s \| BoundedArithmetic/Double/Proofs/ShiftLeft \| 0m02.60s \|\| +0m00.06s 0m02.62s \| BoundedArithmetic/Double/Proofs/ShiftRight \| 0m02.50s \|\| +0m00.12s 0m02.38s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.36s \|\| +0m00.02s 0m02.24s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.20s \|\| +0m00.04s 0m02.17s \| Specific/FancyMachine256/Barrett \| 0m02.14s \|\| +0m00.02s 0m02.16s \| Specific/FancyMachine256/Montgomery \| 0m02.06s \|\| +0m00.10s 0m02.05s \| Reflection/WfReflective \| 0m01.98s \|\| +0m00.06s 0m02.04s \| Assembly/Evaluables \| 0m01.98s \|\| +0m00.06s 0m02.04s \| Specific/GF25519Reflective/Reified/Unpack \| 0m02.02s \|\| +0m00.02s 0m02.04s \| Specific/GF25519Reflective/Reified/Sub \| 0m02.01s \|\| +0m00.03s 0m02.02s \| Specific/GF25519Reflective/Reified/Pack \| 0m02.00s \|\| +0m00.02s 0m01.93s \| Specific/FancyMachine256/Core \| 0m01.81s \|\| +0m00.11s 0m01.91s \| Reflection/WfProofs \| 0m01.98s \|\| -0m00.07s 0m01.88s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.86s \|\| +0m00.01s 0m01.74s \| Specific/GF25519Reflective/Reified/Add \| 0m01.72s \|\| +0m00.02s 0m01.72s \| Reflection/InlineWf \| 0m01.71s \|\| +0m00.01s 0m01.67s \| Specific/GF25519Reflective/Reified/GeModulus \| 0m01.59s \|\| +0m00.07s 0m01.66s \| Specific/GF25519Reflective/Reified/Opp \| 0m01.73s \|\| -0m00.07s 0m01.63s \| ModularArithmetic/BarrettReduction/Z \| 0m01.47s \|\| +0m00.15s 0m01.57s \| Reflection/InlineInterp \| 0m01.55s \|\| +0m00.02s 0m01.52s \| Assembly/WordizeUtil \| 0m01.48s \|\| +0m00.04s 0m01.44s \| Assembly/Compile \| 0m01.46s \|\| -0m00.02s 0m01.41s \| Util/NatUtil \| 0m01.41s \|\| +0m00.00s 0m01.37s \| Reflection/TestCase \| 0m01.42s \|\| -0m00.04s 0m01.32s \| Assembly/Bounds \| 0m01.35s \|\| -0m00.03s 0m01.26s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.29s \|\| -0m00.03s 0m01.25s \| BaseSystem \| 0m01.18s \|\| +0m00.07s 0m01.18s \| BoundedArithmetic/Double/Repeated/Proofs/Decode \| 0m01.02s \|\| +0m00.15s 0m01.16s \| Assembly/Conversions \| 0m01.18s \|\| -0m00.02s 0m01.11s \| ModularArithmetic/ExtendedBaseVector \| 0m01.23s \|\| -0m00.11s 0m01.07s \| Assembly/LL \| 0m00.92s \|\| +0m00.15s 0m01.00s \| BoundedArithmetic/Double/Proofs/LoadImmediate \| 0m00.81s \|\| +0m00.18s 0m00.99s \| Util/WordUtil \| 0m00.99s \|\| +0m00.00s 0m00.97s \| Assembly/HL \| 0m01.01s \|\| -0m00.04s 0m00.95s \| Assembly/Pipeline \| 0m00.92s \|\| +0m00.02s 0m00.92s \| Util/NumTheoryUtil \| 0m00.90s \|\| +0m00.02s 0m00.92s \| BoundedArithmetic/Double/Proofs/BitwiseOr \| 0m00.83s \|\| +0m00.09s 0m00.84s \| Assembly/PhoasCommon \| 0m00.88s \|\| -0m00.04s 0m00.81s \| BoundedArithmetic/X86ToZLikeProofs \| 0m00.87s \|\| -0m00.05s 0m00.80s \| Specific/GF25519Reflective/Reified \| 0m00.81s \|\| -0m00.01s 0m00.80s \| Util/IterAssocOp \| 0m00.80s \|\| +0m00.00s 0m00.76s \| Util/Tuple \| 0m00.72s \|\| +0m00.04s 0m00.75s \| Assembly/QhasmEvalCommon \| 0m00.78s \|\| -0m00.03s 0m00.74s \| Util/PartiallyReifiedProp \| 0m00.74s \|\| +0m00.00s 0m00.72s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.70s \|\| +0m00.02s 0m00.70s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.72s \|\| -0m00.02s 0m00.68s \| Specific/GF25519Reflective/Common \| 0m00.74s \|\| -0m00.05s 0m00.68s \| Encoding/ModularWordEncodingTheorems \| 0m00.67s \|\| +0m00.01s 0m00.66s \| BoundedArithmetic/Double/Repeated/Proofs/Multiply \| 0m00.61s \|\| +0m00.05s 0m00.64s \| Spec/ModularWordEncoding \| 0m00.60s \|\| +0m00.04s 0m00.63s \| ModularArithmetic/ModularBaseSystem \| 0m00.68s \|\| -0m00.05s 0m00.62s \| Spec/EdDSA \| 0m00.64s \|\| -0m00.02s 0m00.61s \| ModularArithmetic/ModularBaseSystemList \| 0m00.68s \|\| -0m00.07s 0m00.61s \| Util/AdditionChainExponentiation \| 0m00.72s \|\| -0m00.10s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.68s \|\| -0m00.08s 0m00.58s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr \| 0m00.47s \|\| +0m00.10s 0m00.58s \| Reflection/WfReflectiveGen \| 0m00.54s \|\| +0m00.03s 0m00.57s \| BoundedArithmetic/X86ToZLike \| 0m00.57s \|\| +0m00.00s 0m00.57s \| Reflection/LinearizeInterp \| 0m00.63s \|\| -0m00.06s 0m00.56s \| BoundedArithmetic/Interface \| 0m00.58s \|\| -0m00.01s 0m00.54s \| Reflection/InterpWfRel \| 0m00.57s \|\| -0m00.02s 0m00.53s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate \| 0m00.53s \|\| +0m00.00s 0m00.53s \| BoundedArithmetic/Double/Proofs/SelectConditional \| 0m00.58s \|\| -0m00.04s 0m00.53s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub \| 0m00.54s \|\| -0m00.01s 0m00.52s \| Reflection/Z/Reify \| 0m00.48s \|\| +0m00.04s 0m00.52s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional \| 0m00.48s \|\| +0m00.04s 0m00.51s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight \| 0m00.52s \|\| -0m00.01s 0m00.51s \| Assembly/StringConversion \| 0m00.52s \|\| -0m00.01s 0m00.49s \| BoundedArithmetic/Double/Core \| 0m00.47s \|\| +0m00.02s 0m00.49s \| Util/Decidable \| 0m00.48s \|\| +0m00.01s 0m00.49s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.40s \|\| +0m00.08s 0m00.49s \| Reflection/InputSyntax \| 0m00.51s \|\| -0m00.02s 0m00.49s \| BoundedArithmetic/Double/Repeated/Core \| 0m00.48s \|\| +0m00.01s 0m00.48s \| Reflection/Syntax \| 0m00.43s \|\| +0m00.04s 0m00.48s \| Assembly/Qhasm \| 0m00.52s \|\| -0m00.04s 0m00.48s \| Reflection/Z/Syntax \| 0m00.47s \|\| +0m00.01s 0m00.47s \| ModularArithmetic/Pow2Base \| 0m00.48s \|\| -0m00.01s 0m00.47s \| BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic \| 0m00.44s \|\| +0m00.02s 0m00.47s \| ModularArithmetic/Pre \| 0m00.54s \|\| -0m00.07s 0m00.47s \| BoundedArithmetic/ArchitectureToZLike \| 0m00.45s \|\| +0m00.01s 0m00.47s \| Spec/MxDH \| 0m00.41s \|\| +0m00.06s 0m00.46s \| Reflection/InterpWf \| 0m00.45s \|\| +0m00.01s 0m00.46s \| ModularArithmetic/ZBounded \| 0m00.47s \|\| -0m00.00s 0m00.46s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate \| 0m00.50s \|\| -0m00.03s 0m00.46s \| Reflection/CommonSubexpressionElimination \| 0m00.50s \|\| -0m00.03s 0m00.43s \| Reflection/Named/DeadCodeElimination \| 0m00.45s \|\| -0m00.02s 0m00.43s \| Reflection/InterpProofs \| 0m00.52s \|\| -0m00.09s 0m00.42s \| Spec/WeierstrassCurve \| 0m00.46s \|\| -0m00.04s 0m00.42s \| BoundedArithmetic/StripCF \| 0m00.42s \|\| +0m00.00s 0m00.42s \| Reflection/Named/Syntax \| 0m00.41s \|\| +0m00.01s 0m00.41s \| Reflection/FilterLive \| 0m00.36s \|\| +0m00.04s 0m00.41s \| Reflection/Conversion \| 0m00.43s \|\| -0m00.02s 0m00.40s \| Reflection/MapInterp \| 0m00.42s \|\| -0m00.01s 0m00.40s \| BoundedArithmetic/Eta \| 0m00.46s \|\| -0m00.06s 0m00.39s \| Reflection/MapInterpWf \| 0m00.39s \|\| +0m00.00s 0m00.39s \| Reflection/Inline \| 0m00.40s \|\| -0m00.01s 0m00.38s \| Reflection/Named/EstablishLiveness \| 0m00.39s \|\| -0m00.01s 0m00.38s \| Tactics/Algebra_syntax/Nsatz \| 0m00.37s \|\| +0m00.01s 0m00.38s \| Reflection/Named/RegisterAssign \| 0m00.44s \|\| -0m00.06s 0m00.37s \| Reflection/Reify \| 0m00.37s \|\| +0m00.00s 0m00.37s \| Reflection/WfRel \| 0m00.38s \|\| -0m00.01s 0m00.36s \| Spec/CompleteEdwardsCurve \| 0m00.38s \|\| -0m00.02s 0m00.36s \| Assembly/QhasmUtil \| 0m00.55s \|\| -0m00.19s 0m00.36s \| ModularArithmetic/Montgomery/Z \| 0m00.48s \|\| -0m00.12s 0m00.35s \| Reflection/Named/Compile \| 0m00.35s \|\| +0m00.00s 0m00.35s \| Reflection/Linearize \| 0m00.37s \|\| -0m00.02s 0m00.35s \| Spec/ModularArithmetic \| 0m00.35s \|\| +0m00.00s 0m00.34s \| Reflection/CountLets \| 0m00.33s \|\| +0m00.01s 0m00.34s \| Reflection/Named/NameUtil \| 0m00.36s \|\| -0m00.01s 0m00.32s \| Util/Sum \| 0m00.22s \|\| +0m00.10s 0m00.32s \| Reflection/Named/ContextOn \| 0m00.35s \|\| -0m00.02s 0m00.31s \| Assembly/QhasmCommon \| 0m00.31s \|\| +0m00.00s 0m00.27s \| Bedrock/Nomega \| 0m00.26s \|\| +0m00.01s 0m00.26s \| ModularArithmetic/ModularBaseSystemListZOperations \| 0m00.26s \|\| +0m00.00s 0m00.19s \| Util/CaseUtil \| 0m00.24s \|\| -0m00.04s 0m00.18s \| Experiments/ExtrHaskellNats \| 0m00.18s \|\| +0m00.00s 0m00.14s \| Util/PointedProp \| 0m00.10s \|\| +0m00.04s 0m00.10s \| Util/Sigma \| 0m00.08s \|\| +0m00.02s 0m00.09s \| Util/Option \| 0m00.12s \|\| -0m00.03s 0m00.09s \| Util/Relations \| 0m00.12s \|\| -0m00.03s 0m00.07s \| Util/Equality \| 0m00.04s \|\| +0m00.03s 0m00.06s \| Util/Tactics \| 0m00.05s \|\| +0m00.00s 0m00.05s \| Util/Prod \| 0m00.06s \|\| -0m00.00s 0m00.05s \| Util/HProp \| 0m00.03s \|\| +0m00.02s 0m00.05s \| Util/LetIn \| 0m00.04s \|\| +0m00.01s 0m00.04s \| Util/Notations \| 0m00.03s \|\| +0m00.01s 0m00.03s \| Tactics/VerdiTactics \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Encoding/EncodingTheorems \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Util/Unit \| 0m00.04s \|\| -0m00.01s 0m00.03s \| Util/AutoRewrite \| 0m00.02s \|\| +0m00.00s 0m00.03s \| Util/FixCoqMistakes \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/Isomorphism \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/GlobalSettings \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Spec/Encoding \| 0m00.02s \|\| +0m00.00s 0m00.02s \| Util/Logic \| 0m00.03s \|\| -0m00.00s 0m00.02s \| Util/Bool \| 0m00.02s \|\| +0m00.00s
*	Switch to reflective bounded word in Ed25519	Jason Gross	2016-10-31
\| \| \| \|	(cc @andres-erbsen)
*	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)
*	Proved eq_enc_E_iff	jadep	2016-10-30
\|
*	framework for l_order_B	Andres Erbsen	2016-10-30
\|
*	proved feSign_correct	jadep	2016-10-29
\|
*	proved Proper_feSign	jadep	2016-10-29
\|
*	prove Proper_SRepERepMul	Andres Erbsen	2016-10-29
\|
*	proved last admit (Proper_feEnc) in Experiments/Ed25519	jadep	2016-10-27
\|
*	proved an admit (eq_enc_S_iff) in Ed25519.v	jadep	2016-10-27
\|
*	removed now irrelevant commented-out code	jadep	2016-10-27
\|
*	convert feEnc correctness proof to bounded type	jadep	2016-10-27
\|
*	finished feEnc correctness	jadep	2016-10-27
\|