fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	rename-everything	Andres Erbsen	2017-04-06
\|
*	Remove stuff from Reflection/Named/Syntax	Jason Gross	2017-03-08
\|
*	Switch to fully uncurried form for reflection	Jason Gross	2017-03-01
\| \| \| \| \| \| \| \| \| \| \|	This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.
*	Remove the Const constructor of exprf	Jason Gross	2017-01-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We instead use the [Op] constructor for constants. This allows [exprf] to not depend on the interpretation function; this means we don't need to map over it to change the interpretation function. This saves us about 300 lines of code and about 30s of build time, total. After \| File Name \| Before \|\| Change ----------------------------------------------------------------------------------------------------------- 18m11.34s \| Total \| 18m46.86s \|\| -0m35.52s ----------------------------------------------------------------------------------------------------------- 0m19.99s \| Specific/GF25519ReflectiveAddCoordinates \| 0m31.78s \|\| -0m11.79s 1m53.69s \| Specific/GF25519Reflective/Reified/LadderStep \| 2m01.32s \|\| -0m07.62s 1m27.74s \| Specific/GF25519Reflective/Reified/AddCoordinates \| 1m34.03s \|\| -0m06.29s 0m01.45s \| Specific/GF25519Reflective \| 0m06.31s \|\| -0m04.85s 0m04.62s \| Reflection/InlineInterp \| 0m01.52s \|\| +0m03.10s 1m19.68s \| CompleteEdwardsCurve/ExtendedCoordinates \| 1m21.19s \|\| -0m01.50s 0m02.90s \| Reflection/InlineWf \| 0m01.80s \|\| +0m01.09s N/A \| Reflection/MapWithInterpInfo \| 0m01.70s \|\| -0m01.70s 1m32.32s \| Test/Curve25519SpecTestVectors \| 1m32.25s \|\| +0m00.06s 1m12.79s \| Experiments/Ed25519 \| 1m13.17s \|\| -0m00.38s 0m40.52s \| ModularArithmetic/Conversion \| 0m40.44s \|\| +0m00.08s 0m34.57s \| Spec/Ed25519 \| 0m34.53s \|\| +0m00.03s 0m30.82s \| ModularArithmetic/ModularBaseSystemProofs \| 0m30.89s \|\| -0m00.07s 0m30.11s \| Specific/GF25519Bounded \| 0m30.21s \|\| -0m00.10s 0m23.20s \| Experiments/MontgomeryCurve \| 0m23.26s \|\| -0m00.06s 0m22.16s \| Reflection/Z/Interpretations128/Relations \| 0m21.72s \|\| +0m00.44s 0m21.69s \| ModularArithmetic/Pow2BaseProofs \| 0m21.58s \|\| +0m00.11s 0m20.25s \| Algebra \| 0m20.27s \|\| -0m00.01s 0m19.81s \| Specific/GF25519 \| 0m19.83s \|\| -0m00.01s 0m18.82s \| Reflection/Z/Interpretations64/Relations \| 0m18.50s \|\| +0m00.32s 0m18.19s \| EdDSARepChange \| 0m18.26s \|\| -0m00.07s 0m17.08s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m17.16s \|\| -0m00.08s 0m14.10s \| Util/ZUtil \| 0m14.03s \|\| +0m00.07s 0m10.05s \| Testbit \| 0m10.02s \|\| +0m00.03s 0m08.95s \| Specific/GF25519BoundedCommon \| 0m08.90s \|\| +0m00.04s 0m08.87s \| BoundedArithmetic/ArchitectureToZLikeProofs \| 0m08.81s \|\| +0m00.05s 0m08.80s \| Assembly/GF25519 \| 0m08.82s \|\| -0m00.01s 0m08.80s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.87s \|\| -0m00.06s 0m08.51s \| Encoding/PointEncoding \| 0m08.53s \|\| -0m00.01s 0m08.37s \| BoundedArithmetic/Double/Proofs/Multiply \| 0m08.39s \|\| -0m00.02s 0m08.34s \| Specific/GF1305 \| 0m08.31s \|\| +0m00.02s 0m07.85s \| BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate \| 0m07.86s \|\| -0m00.01s 0m07.60s \| Specific/GF25519Reflective/Reified/Mul \| 0m07.52s \|\| +0m00.08s 0m07.13s \| MxDHRepChange \| 0m07.08s \|\| +0m00.04s 0m06.85s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate \| 0m06.77s \|\| +0m00.08s 0m06.62s \| Reflection/Z/InterpretationsGen \| 0m06.62s \|\| +0m00.00s 0m05.69s \| Reflection/Z/Interpretations64/RelationsCombinations \| 0m05.60s \|\| +0m00.09s 0m05.68s \| Reflection/Z/Interpretations128/RelationsCombinations \| 0m05.67s \|\| +0m00.00s 0m05.48s \| Specific/SC25519 \| 0m05.38s \|\| +0m00.10s 0m05.40s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub \| 0m05.36s \|\| +0m00.04s 0m04.93s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m04.96s \|\| -0m00.03s 0m04.87s \| WeierstrassCurve/Pre \| 0m04.83s \|\| +0m00.04s 0m04.45s \| Specific/GF25519Reflective/Reified/PreFreeze \| 0m04.56s \|\| -0m00.10s 0m04.33s \| Specific/GF25519Reflective/CommonBinOp \| 0m04.55s \|\| -0m00.21s 0m03.95s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.98s \|\| -0m00.02s 0m03.87s \| Specific/GF25519Reflective/CommonUnOp \| 0m04.08s \|\| -0m00.20s 0m03.86s \| Encoding/PointEncodingPre \| 0m03.88s \|\| -0m00.02s 0m03.84s \| BaseSystemProofs \| 0m03.88s \|\| -0m00.04s 0m03.75s \| Specific/GF25519Reflective/CommonUnOpWireToFE \| 0m03.96s \|\| -0m00.20s 0m03.64s \| CompleteEdwardsCurve/Pre \| 0m03.60s \|\| +0m00.04s 0m03.51s \| BoundedArithmetic/InterfaceProofs \| 0m03.42s \|\| +0m00.08s 0m03.41s \| ModularArithmetic/Tutorial \| 0m03.38s \|\| +0m00.03s 0m03.30s \| Reflection/LinearizeWf \| 0m04.24s \|\| -0m00.94s 0m03.20s \| Specific/GF25519Reflective/Reified/CarrySub \| 0m03.28s \|\| -0m00.07s 0m03.14s \| ModularArithmetic/ZBoundedZ \| 0m03.14s \|\| +0m00.00s 0m03.14s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.14s \|\| +0m00.00s 0m02.95s \| Specific/GF25519Reflective/Reified/CarryAdd \| 0m02.93s \|\| +0m00.02s 0m02.92s \| Specific/GF25519Reflective/Common9_4Op \| 0m02.89s \|\| +0m00.02s 0m02.82s \| Specific/GF25519Reflective/Reified/CarryOpp \| 0m02.95s \|\| -0m00.13s 0m02.82s \| BoundedArithmetic/Double/Proofs/Decode \| 0m02.90s \|\| -0m00.08s 0m02.69s \| BoundedArithmetic/Double/Proofs/ShiftRight \| 0m02.69s \|\| +0m00.00s 0m02.66s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.67s \|\| -0m00.00s 0m02.63s \| Specific/FancyMachine256/Montgomery \| 0m02.24s \|\| +0m00.38s 0m02.61s \| Specific/GF25519Reflective/CommonUnOpFEToWire \| 0m02.76s \|\| -0m00.14s 0m02.58s \| BoundedArithmetic/Double/Proofs/ShiftLeft \| 0m02.58s \|\| +0m00.00s 0m02.56s \| Specific/GF25519Reflective/Common \| 0m02.60s \|\| -0m00.04s 0m02.52s \| Specific/FancyMachine256/Barrett \| 0m02.20s \|\| +0m00.31s 0m02.50s \| Specific/GF25519BoundedAddCoordinates \| 0m02.60s \|\| -0m00.10s 0m02.39s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.31s \|\| +0m00.08s 0m02.34s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.31s \|\| +0m00.02s 0m02.02s \| Specific/GF25519Reflective/Reified/Sub \| 0m02.01s \|\| +0m00.01s 0m01.98s \| Reflection/WfReflective \| 0m02.54s \|\| -0m00.56s 0m01.94s \| Specific/GF25519Reflective/Reified/Pack \| 0m02.07s \|\| -0m00.12s 0m01.93s \| Assembly/Evaluables \| 0m01.93s \|\| +0m00.00s 0m01.92s \| Specific/GF25519Reflective/Reified/Unpack \| 0m02.04s \|\| -0m00.12s 0m01.90s \| Specific/FancyMachine256/Core \| 0m01.79s \|\| +0m00.10s 0m01.79s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.86s \|\| -0m00.07s 0m01.77s \| Specific/GF25519ExtendedAddCoordinates \| 0m01.76s \|\| +0m00.01s 0m01.68s \| Specific/GF25519Reflective/Reified/Add \| 0m01.69s \|\| -0m00.01s 0m01.67s \| Specific/GF25519BoundedExtendedAddCoordinates \| 0m01.79s \|\| -0m00.12s 0m01.63s \| Experiments/Ed25519Extraction \| 0m01.66s \|\| -0m00.03s 0m01.62s \| Specific/GF25519Reflective/Reified/Opp \| 0m01.72s \|\| -0m00.09s 0m01.54s \| Specific/GF25519Reflective/Reified/GeModulus \| 0m01.59s \|\| -0m00.05s 0m01.50s \| Reflection/TestCase \| 0m01.42s \|\| +0m00.08s 0m01.47s \| ModularArithmetic/BarrettReduction/Z \| 0m01.47s \|\| +0m00.00s 0m01.43s \| Assembly/Compile \| 0m01.46s \|\| -0m00.03s 0m01.33s \| Reflection/WfProofs \| 0m01.95s \|\| -0m00.61s 0m01.26s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.28s \|\| -0m00.02s 0m01.20s \| Assembly/Conversions \| 0m01.19s \|\| +0m00.01s 0m01.16s \| ModularArithmetic/ExtendedBaseVector \| 0m01.22s \|\| -0m00.06s 0m01.16s \| BaseSystem \| 0m01.15s \|\| +0m00.01s 0m01.09s \| BoundedArithmetic/Double/Repeated/Proofs/Decode \| 0m01.11s \|\| -0m00.02s 0m00.99s \| Util/NumTheoryUtil \| 0m00.96s \|\| +0m00.03s 0m00.96s \| Assembly/HL \| 0m00.96s \|\| +0m00.00s 0m00.94s \| Assembly/LL \| 0m00.99s \|\| -0m00.05s 0m00.94s \| Assembly/Pipeline \| 0m00.92s \|\| +0m00.01s 0m00.88s \| Reflection/WfInversion \| 0m01.21s \|\| -0m00.32s 0m00.86s \| Assembly/PhoasCommon \| 0m00.91s \|\| -0m00.05s 0m00.86s \| Specific/GF25519Reflective/CommonUnOpFEToZ \| 0m01.02s \|\| -0m00.16s 0m00.85s \| BoundedArithmetic/Double/Proofs/LoadImmediate \| 0m00.86s \|\| -0m00.01s 0m00.84s \| BoundedArithmetic/Double/Proofs/BitwiseOr \| 0m00.91s \|\| -0m00.07s 0m00.82s \| BoundedArithmetic/X86ToZLikeProofs \| 0m00.85s \|\| -0m00.03s 0m00.79s \| Util/IterAssocOp \| 0m00.82s \|\| -0m00.02s 0m00.75s \| Reflection/Z/Syntax \| 0m00.67s \|\| +0m00.07s 0m00.73s \| Util/PartiallyReifiedProp \| 0m00.73s \|\| +0m00.00s 0m00.70s \| Encoding/ModularWordEncodingTheorems \| 0m00.76s \|\| -0m00.06s 0m00.70s \| Specific/GF25519Reflective/Reified \| 0m00.72s \|\| -0m00.02s 0m00.66s \| BoundedArithmetic/Double/Repeated/Proofs/Multiply \| 0m00.62s \|\| +0m00.04s 0m00.66s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.66s \|\| +0m00.00s 0m00.64s \| Encoding/ModularWordEncodingPre \| 0m00.63s \|\| +0m00.01s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.66s \|\| -0m00.05s 0m00.61s \| Util/AdditionChainExponentiation \| 0m00.64s \|\| -0m00.03s 0m00.60s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.64s \|\| -0m00.04s 0m00.60s \| Reflection/MultiSizeTest2 \| 0m00.71s \|\| -0m00.10s 0m00.60s \| Spec/EdDSA \| 0m00.65s \|\| -0m00.05s 0m00.59s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub \| 0m00.51s \|\| +0m00.07s 0m00.58s \| BoundedArithmetic/Interface \| 0m00.60s \|\| -0m00.02s 0m00.58s \| ModularArithmetic/ModularBaseSystemList \| 0m00.61s \|\| -0m00.03s 0m00.55s \| Spec/ModularWordEncoding \| 0m00.63s \|\| -0m00.07s 0m00.55s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight \| 0m00.50s \|\| +0m00.05s 0m00.55s \| Reflection/InterpWfRel \| 0m00.58s \|\| -0m00.02s 0m00.54s \| BoundedArithmetic/X86ToZLike \| 0m00.55s \|\| -0m00.01s 0m00.54s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional \| 0m00.53s \|\| +0m00.01s 0m00.54s \| BoundedArithmetic/Double/Proofs/SelectConditional \| 0m00.62s \|\| -0m00.07s 0m00.54s \| Reflection/WfReflectiveGen \| 0m00.58s \|\| -0m00.03s 0m00.52s \| BoundedArithmetic/ArchitectureToZLike \| 0m00.41s \|\| +0m00.11s 0m00.51s \| BoundedArithmetic/Double/Core \| 0m00.48s \|\| +0m00.03s 0m00.50s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr \| 0m00.51s \|\| -0m00.01s 0m00.49s \| Spec/WeierstrassCurve \| 0m00.42s \|\| +0m00.07s 0m00.48s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate \| 0m00.54s \|\| -0m00.06s 0m00.47s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate \| 0m00.58s \|\| -0m00.10s 0m00.47s \| Reflection/InterpWf \| 0m00.50s \|\| -0m00.03s 0m00.47s \| ModularArithmetic/Pre \| 0m00.48s \|\| -0m00.01s 0m00.47s \| BoundedArithmetic/Double/Repeated/Core \| 0m00.46s \|\| +0m00.00s 0m00.46s \| Reflection/Z/Interpretations64 \| 0m00.49s \|\| -0m00.02s 0m00.45s \| Reflection/InputSyntax \| 0m00.42s \|\| +0m00.03s N/A \| Reflection/MapInterpWf \| 0m00.44s \|\| -0m00.44s 0m00.44s \| Spec/CompleteEdwardsCurve \| 0m00.39s \|\| +0m00.04s 0m00.44s \| BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic \| 0m00.42s \|\| +0m00.02s 0m00.44s \| Reflection/Z/Interpretations128 \| 0m00.52s \|\| -0m00.08s 0m00.44s \| ModularArithmetic/ZBounded \| 0m00.45s \|\| -0m00.01s 0m00.42s \| BoundedArithmetic/StripCF \| 0m00.42s \|\| +0m00.00s 0m00.42s \| Reflection/Z/Reify \| 0m00.43s \|\| -0m00.01s 0m00.42s \| ModularArithmetic/ModularBaseSystemListZOperationsProofs \| 0m00.47s \|\| -0m00.04s 0m00.41s \| Reflection/Named/DeadCodeElimination \| 0m00.43s \|\| -0m00.02s 0m00.41s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.38s \|\| +0m00.02s 0m00.41s \| Spec/ModularArithmetic \| 0m00.34s \|\| +0m00.06s 0m00.41s \| Reflection/Named/RegisterAssign \| 0m00.37s \|\| +0m00.03s 0m00.41s \| Reflection/Reify \| 0m00.39s \|\| +0m00.01s 0m00.40s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| -0m00.01s 0m00.40s \| Reflection/Named/EstablishLiveness \| 0m00.33s \|\| +0m00.07s 0m00.40s \| Reflection/ExprInversion \| 0m00.57s \|\| -0m00.16s 0m00.40s \| Reflection/Named/Syntax \| 0m00.40s \|\| +0m00.00s 0m00.38s \| Reflection/Named/Compile \| 0m00.34s \|\| +0m00.03s N/A \| Reflection/MapInterp \| 0m00.38s \|\| -0m00.38s 0m00.38s \| ModularArithmetic/Montgomery/Z \| 0m00.39s \|\| -0m00.01s 0m00.38s \| ModularArithmetic/ModularBaseSystemWord \| 0m00.36s \|\| +0m00.02s N/A \| Reflection/WfRel \| 0m00.38s \|\| -0m00.38s 0m00.38s \| Reflection/Tuple \| N/A \|\| +0m00.38s 0m00.37s \| Spec/MxDH \| 0m00.39s \|\| -0m00.02s 0m00.37s \| BoundedArithmetic/Eta \| 0m00.36s \|\| +0m00.01s 0m00.36s \| Reflection/Named/ContextOn \| 0m00.37s \|\| -0m00.01s 0m00.34s \| Reflection/FilterLive \| 0m00.34s \|\| +0m00.00s 0m00.34s \| Reflection/LinearizeInterp \| 0m00.53s \|\| -0m00.19s 0m00.33s \| Reflection/Relations \| N/A \|\| +0m00.33s 0m00.32s \| Reflection/Equality \| 0m00.41s \|\| -0m00.08s 0m00.30s \| Reflection/Syntax \| 0m00.52s \|\| -0m00.22s 0m00.30s \| Reflection/InterpProofs \| 0m00.47s \|\| -0m00.17s 0m00.30s \| Reflection/ApplicationLemmas \| 0m00.43s \|\| -0m00.13s 0m00.30s \| Reflection/CommonSubexpressionElimination \| 0m00.50s \|\| -0m00.20s 0m00.28s \| Reflection/Inline \| 0m00.37s \|\| -0m00.08s 0m00.28s \| Reflection/Conversion \| 0m00.44s \|\| -0m00.15s 0m00.27s \| Reflection/MapCastWithCastOp \| 0m00.38s \|\| -0m00.10s 0m00.26s \| Reflection/MapCast \| 0m00.40s \|\| -0m00.14s 0m00.26s \| Reflection/ApplicationRelations \| 0m00.35s \|\| -0m00.08s 0m00.24s \| Reflection/Application \| 0m00.38s \|\| -0m00.14s 0m00.23s \| Reflection/Linearize \| 0m00.35s \|\| -0m00.11s 0m00.20s \| Reflection/CountLets \| 0m00.33s \|\| -0m00.13s 0m00.20s \| Reflection/Named/NameUtil \| 0m00.36s \|\| -0m00.15s 0m00.09s \| Util/PointedProp \| 0m00.08s \|\| +0m00.00s 0m00.05s \| Util/LetIn \| 0m00.06s \|\| -0m00.00s 0m00.03s \| Util/Notations \| 0m00.03s \|\| +0m00.00s 0m00.03s \| Util/AutoRewrite \| 0m00.03s \|\| +0m00.00s
*	Add interp_type_gen_rel_pointwise2, _gen =>	Jason Gross	2016-10-28
\|
*	Make use of named syntax, do reg assign for fancy	Jason Gross	2016-09-22
\|
*	Add a non-higher-order syntax, and reg assignment	Jason Gross	2016-09-22
	The register assigner will return [None] if you give it an invalid assignment (too short, attempting to eliminate live code, attempting to merge registers that can't be merged). No correctness proofs yet, nor any sort of automatic register assignment. I'm planning to write a dead-code-eliminator register assigner next. It should also be moderately straight-forward to write a default register allocator, or perhaps a register post-allocator, that takes a manual register allocation, and renumbers variables in a greedy way. (This would let you pre-specify that some registers should be merged, but leave the rest of the assignment up to the algorithm.)

|

| | | | | | | | | | |

This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

We instead use the [Op] constructor for constants. This allows [exprf] to not depend on the interpretation function; this means we don't need to map over it to change the interpretation function. This saves us about 300 lines of code and about 30s of build time, total. After | File Name | Before || Change ----------------------------------------------------------------------------------------------------------- 18m11.34s | Total | 18m46.86s || -0m35.52s ----------------------------------------------------------------------------------------------------------- 0m19.99s | Specific/GF25519ReflectiveAddCoordinates | 0m31.78s || -0m11.79s 1m53.69s | Specific/GF25519Reflective/Reified/LadderStep | 2m01.32s || -0m07.62s 1m27.74s | Specific/GF25519Reflective/Reified/AddCoordinates | 1m34.03s || -0m06.29s 0m01.45s | Specific/GF25519Reflective | 0m06.31s || -0m04.85s 0m04.62s | Reflection/InlineInterp | 0m01.52s || +0m03.10s 1m19.68s | CompleteEdwardsCurve/ExtendedCoordinates | 1m21.19s || -0m01.50s 0m02.90s | Reflection/InlineWf | 0m01.80s || +0m01.09s N/A | Reflection/MapWithInterpInfo | 0m01.70s || -0m01.70s 1m32.32s | Test/Curve25519SpecTestVectors | 1m32.25s || +0m00.06s 1m12.79s | Experiments/Ed25519 | 1m13.17s || -0m00.38s 0m40.52s | ModularArithmetic/Conversion | 0m40.44s || +0m00.08s 0m34.57s | Spec/Ed25519 | 0m34.53s || +0m00.03s 0m30.82s | ModularArithmetic/ModularBaseSystemProofs | 0m30.89s || -0m00.07s 0m30.11s | Specific/GF25519Bounded | 0m30.21s || -0m00.10s 0m23.20s | Experiments/MontgomeryCurve | 0m23.26s || -0m00.06s 0m22.16s | Reflection/Z/Interpretations128/Relations | 0m21.72s || +0m00.44s 0m21.69s | ModularArithmetic/Pow2BaseProofs | 0m21.58s || +0m00.11s 0m20.25s | Algebra | 0m20.27s || -0m00.01s 0m19.81s | Specific/GF25519 | 0m19.83s || -0m00.01s 0m18.82s | Reflection/Z/Interpretations64/Relations | 0m18.50s || +0m00.32s 0m18.19s | EdDSARepChange | 0m18.26s || -0m00.07s 0m17.08s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m17.16s || -0m00.08s 0m14.10s | Util/ZUtil | 0m14.03s || +0m00.07s 0m10.05s | Testbit | 0m10.02s || +0m00.03s 0m08.95s | Specific/GF25519BoundedCommon | 0m08.90s || +0m00.04s 0m08.87s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.81s || +0m00.05s 0m08.80s | Assembly/GF25519 | 0m08.82s || -0m00.01s 0m08.80s | ModularArithmetic/Montgomery/ZProofs | 0m08.87s || -0m00.06s 0m08.51s | Encoding/PointEncoding | 0m08.53s || -0m00.01s 0m08.37s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.39s || -0m00.02s 0m08.34s | Specific/GF1305 | 0m08.31s || +0m00.02s 0m07.85s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m07.86s || -0m00.01s 0m07.60s | Specific/GF25519Reflective/Reified/Mul | 0m07.52s || +0m00.08s 0m07.13s | MxDHRepChange | 0m07.08s || +0m00.04s 0m06.85s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m06.77s || +0m00.08s 0m06.62s | Reflection/Z/InterpretationsGen | 0m06.62s || +0m00.00s 0m05.69s | Reflection/Z/Interpretations64/RelationsCombinations | 0m05.60s || +0m00.09s 0m05.68s | Reflection/Z/Interpretations128/RelationsCombinations | 0m05.67s || +0m00.00s 0m05.48s | Specific/SC25519 | 0m05.38s || +0m00.10s 0m05.40s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.36s || +0m00.04s 0m04.93s | ModularArithmetic/ModularBaseSystemListProofs | 0m04.96s || -0m00.03s 0m04.87s | WeierstrassCurve/Pre | 0m04.83s || +0m00.04s 0m04.45s | Specific/GF25519Reflective/Reified/PreFreeze | 0m04.56s || -0m00.10s 0m04.33s | Specific/GF25519Reflective/CommonBinOp | 0m04.55s || -0m00.21s 0m03.95s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.98s || -0m00.02s 0m03.87s | Specific/GF25519Reflective/CommonUnOp | 0m04.08s || -0m00.20s 0m03.86s | Encoding/PointEncodingPre | 0m03.88s || -0m00.02s 0m03.84s | BaseSystemProofs | 0m03.88s || -0m00.04s 0m03.75s | Specific/GF25519Reflective/CommonUnOpWireToFE | 0m03.96s || -0m00.20s 0m03.64s | CompleteEdwardsCurve/Pre | 0m03.60s || +0m00.04s 0m03.51s | BoundedArithmetic/InterfaceProofs | 0m03.42s || +0m00.08s 0m03.41s | ModularArithmetic/Tutorial | 0m03.38s || +0m00.03s 0m03.30s | Reflection/LinearizeWf | 0m04.24s || -0m00.94s 0m03.20s | Specific/GF25519Reflective/Reified/CarrySub | 0m03.28s || -0m00.07s 0m03.14s | ModularArithmetic/ZBoundedZ | 0m03.14s || +0m00.00s 0m03.14s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.14s || +0m00.00s 0m02.95s | Specific/GF25519Reflective/Reified/CarryAdd | 0m02.93s || +0m00.02s 0m02.92s | Specific/GF25519Reflective/Common9_4Op | 0m02.89s || +0m00.02s 0m02.82s | Specific/GF25519Reflective/Reified/CarryOpp | 0m02.95s || -0m00.13s 0m02.82s | BoundedArithmetic/Double/Proofs/Decode | 0m02.90s || -0m00.08s 0m02.69s | BoundedArithmetic/Double/Proofs/ShiftRight | 0m02.69s || +0m00.00s 0m02.66s | ModularArithmetic/ModularArithmeticTheorems | 0m02.67s || -0m00.00s 0m02.63s | Specific/FancyMachine256/Montgomery | 0m02.24s || +0m00.38s 0m02.61s | Specific/GF25519Reflective/CommonUnOpFEToWire | 0m02.76s || -0m00.14s 0m02.58s | BoundedArithmetic/Double/Proofs/ShiftLeft | 0m02.58s || +0m00.00s 0m02.56s | Specific/GF25519Reflective/Common | 0m02.60s || -0m00.04s 0m02.52s | Specific/FancyMachine256/Barrett | 0m02.20s || +0m00.31s 0m02.50s | Specific/GF25519BoundedAddCoordinates | 0m02.60s || -0m00.10s 0m02.39s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.31s || +0m00.08s 0m02.34s | ModularArithmetic/ModularBaseSystemOpt | 0m02.31s || +0m00.02s 0m02.02s | Specific/GF25519Reflective/Reified/Sub | 0m02.01s || +0m00.01s 0m01.98s | Reflection/WfReflective | 0m02.54s || -0m00.56s 0m01.94s | Specific/GF25519Reflective/Reified/Pack | 0m02.07s || -0m00.12s 0m01.93s | Assembly/Evaluables | 0m01.93s || +0m00.00s 0m01.92s | Specific/GF25519Reflective/Reified/Unpack | 0m02.04s || -0m00.12s 0m01.90s | Specific/FancyMachine256/Core | 0m01.79s || +0m00.10s 0m01.79s | ModularArithmetic/Montgomery/ZBounded | 0m01.86s || -0m00.07s 0m01.77s | Specific/GF25519ExtendedAddCoordinates | 0m01.76s || +0m00.01s 0m01.68s | Specific/GF25519Reflective/Reified/Add | 0m01.69s || -0m00.01s 0m01.67s | Specific/GF25519BoundedExtendedAddCoordinates | 0m01.79s || -0m00.12s 0m01.63s | Experiments/Ed25519Extraction | 0m01.66s || -0m00.03s 0m01.62s | Specific/GF25519Reflective/Reified/Opp | 0m01.72s || -0m00.09s 0m01.54s | Specific/GF25519Reflective/Reified/GeModulus | 0m01.59s || -0m00.05s 0m01.50s | Reflection/TestCase | 0m01.42s || +0m00.08s 0m01.47s | ModularArithmetic/BarrettReduction/Z | 0m01.47s || +0m00.00s 0m01.43s | Assembly/Compile | 0m01.46s || -0m00.03s 0m01.33s | Reflection/WfProofs | 0m01.95s || -0m00.61s 0m01.26s | ModularArithmetic/PrimeFieldTheorems | 0m01.28s || -0m00.02s 0m01.20s | Assembly/Conversions | 0m01.19s || +0m00.01s 0m01.16s | ModularArithmetic/ExtendedBaseVector | 0m01.22s || -0m00.06s 0m01.16s | BaseSystem | 0m01.15s || +0m00.01s 0m01.09s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.11s || -0m00.02s 0m00.99s | Util/NumTheoryUtil | 0m00.96s || +0m00.03s 0m00.96s | Assembly/HL | 0m00.96s || +0m00.00s 0m00.94s | Assembly/LL | 0m00.99s || -0m00.05s 0m00.94s | Assembly/Pipeline | 0m00.92s || +0m00.01s 0m00.88s | Reflection/WfInversion | 0m01.21s || -0m00.32s 0m00.86s | Assembly/PhoasCommon | 0m00.91s || -0m00.05s 0m00.86s | Specific/GF25519Reflective/CommonUnOpFEToZ | 0m01.02s || -0m00.16s 0m00.85s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.86s || -0m00.01s 0m00.84s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.91s || -0m00.07s 0m00.82s | BoundedArithmetic/X86ToZLikeProofs | 0m00.85s || -0m00.03s 0m00.79s | Util/IterAssocOp | 0m00.82s || -0m00.02s 0m00.75s | Reflection/Z/Syntax | 0m00.67s || +0m00.07s 0m00.73s | Util/PartiallyReifiedProp | 0m00.73s || +0m00.00s 0m00.70s | Encoding/ModularWordEncodingTheorems | 0m00.76s || -0m00.06s 0m00.70s | Specific/GF25519Reflective/Reified | 0m00.72s || -0m00.02s 0m00.66s | BoundedArithmetic/Double/Repeated/Proofs/Multiply | 0m00.62s || +0m00.04s 0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.66s || +0m00.00s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.63s || +0m00.01s 0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.66s || -0m00.05s 0m00.61s | Util/AdditionChainExponentiation | 0m00.64s || -0m00.03s 0m00.60s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || -0m00.04s 0m00.60s | Reflection/MultiSizeTest2 | 0m00.71s || -0m00.10s 0m00.60s | Spec/EdDSA | 0m00.65s || -0m00.05s 0m00.59s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.51s || +0m00.07s 0m00.58s | BoundedArithmetic/Interface | 0m00.60s || -0m00.02s 0m00.58s | ModularArithmetic/ModularBaseSystemList | 0m00.61s || -0m00.03s 0m00.55s | Spec/ModularWordEncoding | 0m00.63s || -0m00.07s 0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | 0m00.50s || +0m00.05s 0m00.55s | Reflection/InterpWfRel | 0m00.58s || -0m00.02s 0m00.54s | BoundedArithmetic/X86ToZLike | 0m00.55s || -0m00.01s 0m00.54s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.53s || +0m00.01s 0m00.54s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.62s || -0m00.07s 0m00.54s | Reflection/WfReflectiveGen | 0m00.58s || -0m00.03s 0m00.52s | BoundedArithmetic/ArchitectureToZLike | 0m00.41s || +0m00.11s 0m00.51s | BoundedArithmetic/Double/Core | 0m00.48s || +0m00.03s 0m00.50s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.51s || -0m00.01s 0m00.49s | Spec/WeierstrassCurve | 0m00.42s || +0m00.07s 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.54s || -0m00.06s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.58s || -0m00.10s 0m00.47s | Reflection/InterpWf | 0m00.50s || -0m00.03s 0m00.47s | ModularArithmetic/Pre | 0m00.48s || -0m00.01s 0m00.47s | BoundedArithmetic/Double/Repeated/Core | 0m00.46s || +0m00.00s 0m00.46s | Reflection/Z/Interpretations64 | 0m00.49s || -0m00.02s 0m00.45s | Reflection/InputSyntax | 0m00.42s || +0m00.03s N/A | Reflection/MapInterpWf | 0m00.44s || -0m00.44s 0m00.44s | Spec/CompleteEdwardsCurve | 0m00.39s || +0m00.04s 0m00.44s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.42s || +0m00.02s 0m00.44s | Reflection/Z/Interpretations128 | 0m00.52s || -0m00.08s 0m00.44s | ModularArithmetic/ZBounded | 0m00.45s || -0m00.01s 0m00.42s | BoundedArithmetic/StripCF | 0m00.42s || +0m00.00s 0m00.42s | Reflection/Z/Reify | 0m00.43s || -0m00.01s 0m00.42s | ModularArithmetic/ModularBaseSystemListZOperationsProofs | 0m00.47s || -0m00.04s 0m00.41s | Reflection/Named/DeadCodeElimination | 0m00.43s || -0m00.02s 0m00.41s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.38s || +0m00.02s 0m00.41s | Spec/ModularArithmetic | 0m00.34s || +0m00.06s 0m00.41s | Reflection/Named/RegisterAssign | 0m00.37s || +0m00.03s 0m00.41s | Reflection/Reify | 0m00.39s || +0m00.01s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.42s || -0m00.01s 0m00.40s | Reflection/Named/EstablishLiveness | 0m00.33s || +0m00.07s 0m00.40s | Reflection/ExprInversion | 0m00.57s || -0m00.16s 0m00.40s | Reflection/Named/Syntax | 0m00.40s || +0m00.00s 0m00.38s | Reflection/Named/Compile | 0m00.34s || +0m00.03s N/A | Reflection/MapInterp | 0m00.38s || -0m00.38s 0m00.38s | ModularArithmetic/Montgomery/Z | 0m00.39s || -0m00.01s 0m00.38s | ModularArithmetic/ModularBaseSystemWord | 0m00.36s || +0m00.02s N/A | Reflection/WfRel | 0m00.38s || -0m00.38s 0m00.38s | Reflection/Tuple | N/A || +0m00.38s 0m00.37s | Spec/MxDH | 0m00.39s || -0m00.02s 0m00.37s | BoundedArithmetic/Eta | 0m00.36s || +0m00.01s 0m00.36s | Reflection/Named/ContextOn | 0m00.37s || -0m00.01s 0m00.34s | Reflection/FilterLive | 0m00.34s || +0m00.00s 0m00.34s | Reflection/LinearizeInterp | 0m00.53s || -0m00.19s 0m00.33s | Reflection/Relations | N/A || +0m00.33s 0m00.32s | Reflection/Equality | 0m00.41s || -0m00.08s 0m00.30s | Reflection/Syntax | 0m00.52s || -0m00.22s 0m00.30s | Reflection/InterpProofs | 0m00.47s || -0m00.17s 0m00.30s | Reflection/ApplicationLemmas | 0m00.43s || -0m00.13s 0m00.30s | Reflection/CommonSubexpressionElimination | 0m00.50s || -0m00.20s 0m00.28s | Reflection/Inline | 0m00.37s || -0m00.08s 0m00.28s | Reflection/Conversion | 0m00.44s || -0m00.15s 0m00.27s | Reflection/MapCastWithCastOp | 0m00.38s || -0m00.10s 0m00.26s | Reflection/MapCast | 0m00.40s || -0m00.14s 0m00.26s | Reflection/ApplicationRelations | 0m00.35s || -0m00.08s 0m00.24s | Reflection/Application | 0m00.38s || -0m00.14s 0m00.23s | Reflection/Linearize | 0m00.35s || -0m00.11s 0m00.20s | Reflection/CountLets | 0m00.33s || -0m00.13s 0m00.20s | Reflection/Named/NameUtil | 0m00.36s || -0m00.15s 0m00.09s | Util/PointedProp | 0m00.08s || +0m00.00s 0m00.05s | Util/LetIn | 0m00.06s || -0m00.00s 0m00.03s | Util/Notations | 0m00.03s || +0m00.00s 0m00.03s | Util/AutoRewrite | 0m00.03s || +0m00.00s

|

The register assigner will return [None] if you give it an invalid assignment (too short, attempting to eliminate live code, attempting to merge registers that can't be merged). No correctness proofs yet, nor any sort of automatic register assignment. I'm planning to write a dead-code-eliminator register assigner next. It should also be moderately straight-forward to write a default register allocator, or perhaps a register post-allocator, that takes a manual register allocation, and renumbers variables in a greedy way. (This would let you pre-specify that some registers should be merged, but leave the rest of the assignment up to the algorithm.)