Integrate elimination of useless carries #108
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JasonGross
force-pushed
the
eliminate-useless-carries
branch
3 times, most recently
from
db731dd
to
8cdea27
Compare
|
Updated; no more admitted proofs, and I've inspected the extraction and it looks fine, modulo doing lots of stuff with pairs/tuples, and calling |
|
Updated with timing: the core stuff takes about 20 minutes; the entire library with SpecificGen takes around 2 hours. The most expensive files, RAM-wise, are: The core things now need about 4 GB of RAM to build, and SpecificGen still needs around 27 GB of RAM to build. |
Timing info on make all: Time | File Name ----------------------------------------------------------------------------------- 147m20.79s | Total ----------------------------------------------------------------------------------- 33m56.77s | SpecificGen/GF5211_32Reflective/Reified/AddCoordinates 21m43.91s | SpecificGen/GF5211_32Reflective/Common9_4Op 15m06.36s | SpecificGen/GF41417_32Reflective/Common9_4Op 12m52.27s | SpecificGen/GF41417_32Reflective/Reified/AddCoordinates 4m30.01s | SpecificGen/GF5211_32Reflective/Reified/Mul 3m32.18s | SpecificGen/GF5211_32Bounded 2m52.34s | SpecificGen/GF5211_32 2m32.78s | SpecificGen/GF41417_32Bounded 2m27.71s | SpecificGen/GF2519_32Reflective/Common9_4Op 2m26.41s | SpecificGen/GF25519_32Reflective/Common9_4Op 2m24.50s | Specific/GF25519Reflective/Common9_4Op 1m53.18s | SpecificGen/GF2519_32Reflective/Reified/AddCoordinates 1m47.72s | SpecificGen/GF41417_32 1m45.36s | SpecificGen/GF5211_32BoundedCommon 1m38.02s | Specific/GF25519Reflective/Reified/AddCoordinates 1m36.31s | SpecificGen/GF25519_32Reflective/Reified/AddCoordinates 1m32.95s | Test/Curve25519SpecTestVectors 1m21.69s | Experiments/Ed25519 1m19.14s | SpecificGen/GF2213_32Reflective/Common9_4Op 1m18.13s | CompleteEdwardsCurve/ExtendedCoordinates 1m05.62s | SpecificGen/GF41417_32BoundedCommon 0m59.16s | SpecificGen/GF41417_32Reflective/Reified/Mul 0m52.14s | SpecificGen/GF2213_32Reflective/Reified/AddCoordinates 0m40.63s | ModularArithmetic/Conversion 0m37.91s | SpecificGen/GF5211_32Reflective/CommonBinOp 0m34.92s | Spec/Ed25519 0m33.29s | SpecificGen/GF5211_32Reflective/CommonUnOp 0m33.08s | Specific/GF25519ReflectiveAddCoordinates 0m32.95s | SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE 0m31.63s | ModularArithmetic/ModularBaseSystemProofs 0m30.20s | Specific/GF25519Bounded 0m30.18s | SpecificGen/GF25519_32Bounded 0m29.60s | SpecificGen/GF2519_32Bounded 0m26.31s | SpecificGen/GF41417_32Reflective/CommonBinOp 0m23.98s | Experiments/Ed25519Extraction 0m23.51s | SpecificGen/GF25519_64Reflective/Common9_4Op 0m23.24s | SpecificGen/GF41417_32Reflective/CommonUnOp 0m23.10s | Experiments/MontgomeryCurve 0m22.75s | SpecificGen/GF2519_32 0m22.66s | SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE 0m22.04s | ModularArithmetic/Pow2BaseProofs 0m21.68s | Reflection/Z/Interpretations128/Relations 0m21.19s | SpecificGen/GF25519_32 0m20.34s | Algebra 0m20.17s | SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire 0m20.16s | Specific/GF25519 0m19.82s | SpecificGen/GF25519_64Reflective/Reified/AddCoordinates 0m18.66s | SpecificGen/GF2213_32Bounded 0m18.44s | Reflection/Z/Interpretations64/Relations 0m18.22s | EdDSARepChange 0m17.19s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems 0m17.15s | SpecificGen/GF5211_32Reflective 0m14.16s | SpecificGen/GF2213_32 0m14.00s | Util/ZUtil 0m12.41s | SpecificGen/GF5211_32Reflective/Reified/PreFreeze 0m12.22s | SpecificGen/GF5211_32Reflective/Common 0m11.92s | SpecificGen/GF41417_32Reflective 0m11.16s | SpecificGen/GF25519_64Reflective 0m10.91s | SpecificGen/GF25519_64Bounded 0m10.75s | SpecificGen/GF25519_64 0m10.63s | SpecificGen/GF41417_32Reflective/Reified/PreFreeze 0m09.96s | Testbit 0m09.49s | SpecificGen/GF25519_32BoundedCommon 0m09.40s | Specific/GF25519BoundedCommon 0m09.36s | SpecificGen/GF2519_32BoundedCommon 0m09.09s | Assembly/GF25519 0m08.94s | SpecificGen/GF41417_32Reflective/Common 0m08.89s | SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire 0m08.83s | Encoding/PointEncoding 0m08.82s | SpecificGen/GF2519_32Reflective/Reified/Mul 0m08.78s | ModularArithmetic/Montgomery/ZProofs 0m08.75s | BoundedArithmetic/ArchitectureToZLikeProofs 0m08.51s | Specific/GF1305 0m08.40s | BoundedArithmetic/Double/Proofs/Multiply 0m08.28s | SpecificGen/GF5211_32Reflective/Reified/CarrySub 0m08.12s | SpecificGen/GF25519_32Reflective/Reified/Mul 0m08.11s | Specific/GF25519Reflective/Reified/Mul 0m07.91s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate 0m07.35s | SpecificGen/GF5211_32Reflective/Reified/CarryAdd 0m07.22s | SpecificGen/GF41417_32Reflective/Reified/CarrySub 0m07.08s | MxDHRepChange 0m06.85s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate 0m06.74s | SpecificGen/GF2519_32Reflective 0m06.59s | SpecificGen/GF5211_32Reflective/Reified/CarryOpp 0m06.56s | Reflection/Z/InterpretationsGen 0m06.38s | SpecificGen/GF41417_32Reflective/Reified/CarryAdd 0m06.33s | Specific/GF25519Reflective 0m06.26s | SpecificGen/GF25519_32Reflective 0m06.12s | Bedrock/Word 0m05.98s | SpecificGen/GF41417_32Reflective/Reified/CarryOpp 0m05.89s | SpecificGen/GF2213_32BoundedCommon 0m05.68s | SpecificGen/GF5211_32ExtendedAddCoordinates 0m05.64s | SpecificGen/GF2213_32Reflective/Reified/Mul 0m05.55s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub 0m05.53s | Reflection/Z/Interpretations128/RelationsCombinations 0m05.46s | Reflection/Z/Interpretations64/RelationsCombinations 0m05.39s | Util/ListUtil 0m05.36s | Specific/SC25519 0m05.32s | Experiments/GenericFieldPow 0m05.21s | ModularArithmetic/ModularBaseSystemListProofs 0m05.02s | SpecificGen/GF2213_32Reflective 0m04.84s | WeierstrassCurve/Pre 0m04.82s | SpecificGen/GF5211_32Reflective/Reified/Pack 0m04.70s | SpecificGen/GF5211_32Reflective/Reified/Unpack 0m04.68s | SpecificGen/GF5211_32Reflective/Reified/Sub 0m04.60s | SpecificGen/GF25519_32Reflective/CommonBinOp 0m04.58s | Specific/GF25519Reflective/CommonBinOp 0m04.57s | Specific/GF25519Reflective/Reified/PreFreeze 0m04.53s | SpecificGen/GF2519_32Reflective/CommonBinOp 0m04.50s | SpecificGen/GF25519_32Reflective/Reified/PreFreeze 0m04.50s | SpecificGen/GF2519_32Reflective/Reified/PreFreeze 0m04.37s | SpecificGen/GF25519_64BoundedCommon 0m04.13s | Specific/GF25519Reflective/CommonUnOp 0m04.10s | SpecificGen/GF41417_32Reflective/Reified/Sub 0m04.10s | Reflection/LinearizeWf 0m04.10s | SpecificGen/GF41417_32ExtendedAddCoordinates 0m04.07s | SpecificGen/GF41417_32Reflective/Reified/Pack 0m04.04s | SpecificGen/GF25519_32Reflective/CommonUnOp 0m04.03s | SpecificGen/GF2519_32Reflective/CommonUnOp 0m04.02s | ModularArithmetic/BarrettReduction/ZHandbook 0m03.98s | SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE 0m03.98s | SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE 0m03.94s | Specific/GF25519Reflective/CommonUnOpWireToFE 0m03.88s | BaseSystemProofs 0m03.87s | SpecificGen/GF41417_32Reflective/Reified/Unpack 0m03.85s | Encoding/PointEncodingPre 0m03.84s | SpecificGen/GF5211_32Reflective/Reified/Add 0m03.62s | CompleteEdwardsCurve/Pre 0m03.53s | SpecificGen/GF5211_32Reflective/Reified/Opp 0m03.52s | SpecificGen/GF2213_32Reflective/Reified/PreFreeze 0m03.50s | ModularArithmetic/Tutorial 0m03.43s | Specific/GF25519Reflective/Reified/CarrySub 0m03.42s | SpecificGen/GF41417_32Reflective/Reified/Add 0m03.39s | BoundedArithmetic/InterfaceProofs 0m03.38s | SpecificGen/GF2519_32Reflective/Reified/CarrySub 0m03.34s | SpecificGen/GF25519_32Reflective/Reified/CarrySub 0m03.16s | SpecificGen/GF41417_32Reflective/Reified/Opp 0m03.14s | ModularArithmetic/BarrettReduction/ZGeneralized 0m03.12s | ModularArithmetic/ZBoundedZ 0m03.08s | Specific/GF25519Reflective/Common 0m03.06s | SpecificGen/GF25519_64Reflective/Reified/PreFreeze 0m03.05s | SpecificGen/GF25519_32Reflective/Reified/CarryOpp 0m03.04s | SpecificGen/GF2519_32Reflective/Common 0m03.04s | Specific/GF25519Reflective/Reified/CarryOpp 0m03.03s | SpecificGen/GF25519_32Reflective/Common 0m03.03s | SpecificGen/GF2519_32Reflective/Reified/CarryAdd 0m03.02s | SpecificGen/GF25519_32Reflective/Reified/CarryAdd 0m03.00s | SpecificGen/GF2519_32Reflective/Reified/CarryOpp 0m03.00s | Specific/GF25519Reflective/Reified/CarryAdd 0m02.98s | SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE 0m02.96s | SpecificGen/GF25519_64Reflective/Reified/Mul 0m02.93s | BoundedArithmetic/Double/Proofs/Decode 0m02.86s | SpecificGen/GF2213_32Reflective/CommonBinOp 0m02.83s | SpecificGen/GF5211_32Reflective/Reified/GeModulus 0m02.80s | Specific/GF25519ExtendedAddCoordinates 0m02.73s | ModularArithmetic/ModularArithmeticTheorems 0m02.72s | SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire 0m02.72s | SpecificGen/GF2213_32Reflective/Reified/CarrySub 0m02.70s | Assembly/State 0m02.69s | Specific/GF25519Reflective/CommonUnOpFEToWire 0m02.68s | Specific/GF25519BoundedAddCoordinates 0m02.67s | SpecificGen/GF2213_32Reflective/CommonUnOp 0m02.66s | SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire 0m02.65s | BoundedArithmetic/Double/Proofs/ShiftRight 0m02.60s | BoundedArithmetic/Double/Proofs/ShiftLeft 0m02.55s | SpecificGen/GF2213_32Reflective/Reified/CarryOpp 0m02.51s | SpecificGen/GF41417_32Reflective/Reified/GeModulus 0m02.42s | SpecificGen/GF25519_32ExtendedAddCoordinates 0m02.42s | SpecificGen/GF2213_32Reflective/Reified/CarryAdd 0m02.40s | SpecificGen/GF25519_64Reflective/Reified/CarryOpp 0m02.38s | SpecificGen/GF25519_64Reflective/Reified/CarrySub 0m02.36s | SpecificGen/GF2519_32ExtendedAddCoordinates 0m02.33s | ModularArithmetic/BarrettReduction/ZBounded 0m02.30s | ModularArithmetic/ModularBaseSystemOpt 0m02.27s | SpecificGen/GF2519_32Reflective/Reified/Pack 0m02.25s | SpecificGen/GF2213_32Reflective/Common 0m02.20s | SpecificGen/GF2213_32ExtendedAddCoordinates 0m02.18s | SpecificGen/GF2519_32Reflective/Reified/Unpack 0m02.12s | Specific/FancyMachine256/Barrett 0m02.11s | SpecificGen/GF25519_64Reflective/Reified/CarryAdd 0m02.10s | Specific/FancyMachine256/Montgomery 0m02.10s | SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire 0m02.09s | Specific/GF25519Reflective/Reified/Unpack 0m02.08s | Specific/GF25519Reflective/Reified/Pack 0m02.07s | SpecificGen/GF25519_32Reflective/Reified/Unpack 0m02.06s | SpecificGen/GF25519_32Reflective/Reified/Sub 0m02.05s | SpecificGen/GF25519_32Reflective/Reified/Pack 0m02.03s | SpecificGen/GF2519_32Reflective/Reified/Sub 0m02.03s | Reflection/WfReflective 0m02.00s | SpecificGen/GF25519_64ExtendedAddCoordinates 0m01.99s | Specific/GF25519Reflective/Reified/Sub 0m01.96s | Reflection/WfProofs 0m01.92s | SpecificGen/GF2213_32Reflective/Reified/Pack 0m01.92s | Assembly/Evaluables 0m01.92s | Util/WordUtil 0m01.89s | ModularArithmetic/Montgomery/ZBounded 0m01.84s | SpecificGen/GF2213_32Reflective/Reified/Unpack 0m01.82s | Specific/FancyMachine256/Core 0m01.76s | SpecificGen/GF25519_32Reflective/Reified/Add 0m01.74s | Specific/GF25519Reflective/Reified/Opp 0m01.74s | SpecificGen/GF2519_32Reflective/Reified/Opp 0m01.73s | SpecificGen/GF2213_32Reflective/Reified/Sub 0m01.72s | Specific/GF25519BoundedExtendedAddCoordinates 0m01.72s | SpecificGen/GF2519_32Reflective/Reified/Add 0m01.70s | SpecificGen/GF25519_32Reflective/Reified/Opp 0m01.70s | Reflection/InlineWf 0m01.70s | SpecificGen/GF25519_64Reflective/Reified/Pack 0m01.68s | SpecificGen/GF25519_64Reflective/Reified/Unpack 0m01.68s | Assembly/Compile 0m01.67s | SpecificGen/GF25519_64Reflective/CommonBinOp 0m01.64s | Specific/GF25519Reflective/Reified/Add 0m01.64s | Reflection/InlineInterp 0m01.62s | Specific/GF25519Reflective/Reified/GeModulus 0m01.60s | SpecificGen/GF2519_32Reflective/Reified/GeModulus 0m01.60s | SpecificGen/GF25519_32Reflective/Reified/GeModulus 0m01.56s | SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE 0m01.53s | SpecificGen/GF25519_64Reflective/Common 0m01.53s | SpecificGen/GF25519_64Reflective/CommonUnOp 0m01.53s | SpecificGen/GF2213_32Reflective/Reified/Opp 0m01.52s | ModularArithmetic/BarrettReduction/Z 0m01.50s | SpecificGen/GF2213_32Reflective/Reified/Add 0m01.48s | Assembly/WordizeUtil 0m01.47s | SpecificGen/GF2213_32Reflective/Reified/GeModulus 0m01.46s | SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ 0m01.44s | Util/NatUtil 0m01.40s | SpecificGen/GF25519_64Reflective/Reified/Opp 0m01.39s | Reflection/TestCase 0m01.37s | SpecificGen/GF25519_64Reflective/Reified/Sub 0m01.36s | SpecificGen/GF25519_64Reflective/Reified/GeModulus 0m01.36s | Assembly/Bounds 0m01.31s | SpecificGen/GF5211_32Reflective/Reified 0m01.29s | Util/Tuple 0m01.28s | SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire 0m01.27s | ModularArithmetic/PrimeFieldTheorems 0m01.27s | SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ 0m01.20s | Assembly/Conversions 0m01.17s | BaseSystem 0m01.13s | ModularArithmetic/ExtendedBaseVector 0m01.09s | BoundedArithmetic/Double/Repeated/Proofs/Decode 0m01.08s | SpecificGen/GF25519_64Reflective/Reified/Add 0m01.05s | Assembly/LL 0m01.00s | Assembly/Pipeline 0m00.95s | SpecificGen/GF41417_32Reflective/Reified 0m00.92s | Assembly/HL 0m00.92s | Specific/GF25519Reflective/CommonUnOpFEToZ 0m00.91s | Util/NumTheoryUtil 0m00.91s | SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ 0m00.88s | SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ 0m00.88s | Assembly/PhoasCommon 0m00.87s | BoundedArithmetic/Double/Proofs/BitwiseOr 0m00.87s | SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ 0m00.86s | BoundedArithmetic/Double/Proofs/LoadImmediate 0m00.86s | SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ 0m00.81s | BoundedArithmetic/X86ToZLikeProofs 0m00.81s | Util/IterAssocOp 0m00.79s | Specific/GF25519Reflective/Reified 0m00.78s | Assembly/QhasmEvalCommon 0m00.76s | SpecificGen/GF2519_32Reflective/Reified 0m00.73s | Reflection/Z/Syntax 0m00.72s | SpecificGen/GF25519_64Reflective/Reified 0m00.71s | SpecificGen/GF2213_32Reflective/Reified 0m00.70s | Encoding/ModularWordEncodingTheorems 0m00.70s | SpecificGen/GF25519_32Reflective/Reified 0m00.69s | Util/PartiallyReifiedProp 0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs 0m00.64s | ModularArithmetic/ExtPow2BaseMulProofs 0m00.64s | Spec/EdDSA 0m00.63s | ModularArithmetic/ModularBaseSystem 0m00.62s | BoundedArithmetic/Double/Repeated/Proofs/Multiply 0m00.61s | Util/AdditionChainExponentiation 0m00.61s | Reflection/WfReflectiveGen 0m00.60s | ModularArithmetic/ModularBaseSystemList 0m00.60s | Encoding/ModularWordEncodingPre 0m00.58s | BoundedArithmetic/X86ToZLike 0m00.58s | Reflection/InterpWfRel 0m00.57s | Spec/ModularWordEncoding 0m00.55s | BoundedArithmetic/Double/Proofs/SelectConditional 0m00.55s | BoundedArithmetic/Interface 0m00.54s | Reflection/Syntax 0m00.53s | Util/Decidable 0m00.53s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub 0m00.52s | BoundedArithmetic/Double/Repeated/Core 0m00.52s | Reflection/LinearizeInterp 0m00.51s | Assembly/StringConversion 0m00.51s | BoundedArithmetic/ArchitectureToZLike 0m00.50s | BoundedArithmetic/Double/Core 0m00.50s | Util/HList 0m00.49s | Reflection/Named/Syntax 0m00.49s | Assembly/Qhasm 0m00.49s | ModularArithmetic/ZBounded 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr 0m00.48s | Reflection/CommonSubexpressionElimination 0m00.48s | ModularArithmetic/Pre 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional 0m00.46s | Reflection/InterpProofs 0m00.46s | Reflection/Z/Interpretations128 0m00.46s | Reflection/Z/Reify 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate 0m00.45s | Spec/CompleteEdwardsCurve 0m00.45s | Reflection/InterpWf 0m00.44s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate 0m00.44s | Reflection/Application 0m00.44s | Assembly/QhasmUtil 0m00.43s | Reflection/Conversion 0m00.43s | Reflection/InputSyntax 0m00.43s | Reflection/Z/Interpretations64 0m00.42s | Reflection/MapInterpWf 0m00.42s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic 0m00.42s | BoundedArithmetic/StripCF 0m00.42s | ModularArithmetic/ModularBaseSystemListZOperationsProofs 0m00.42s | Spec/WeierstrassCurve 0m00.41s | ModularArithmetic/PseudoMersenneBaseParams 0m00.41s | ModularArithmetic/Pow2Base 0m00.40s | Spec/MxDH 0m00.39s | Reflection/Named/RegisterAssign 0m00.39s | ModularArithmetic/ModularBaseSystemWord 0m00.39s | Reflection/CountLets 0m00.39s | ModularArithmetic/ModularBaseSystemListZOperations 0m00.38s | Reflection/MapInterp 0m00.38s | BoundedArithmetic/Eta 0m00.37s | Reflection/Inline 0m00.37s | Reflection/WfRel 0m00.37s | Tactics/Algebra_syntax/Nsatz 0m00.36s | ModularArithmetic/Montgomery/Z 0m00.36s | Reflection/Named/DeadCodeElimination 0m00.35s | Reflection/Named/Compile 0m00.35s | Reflection/Named/EstablishLiveness 0m00.34s | Reflection/FilterLive 0m00.34s | Spec/ModularArithmetic 0m00.33s | Reflection/Named/ContextOn 0m00.33s | Reflection/Linearize 0m00.32s | Reflection/Named/NameUtil 0m00.32s | Reflection/Reify 0m00.29s | Assembly/QhasmCommon 0m00.29s | Util/Sum 0m00.28s | Bedrock/Nomega 0m00.22s | Util/CaseUtil 0m00.17s | Experiments/ExtrHaskellNats 0m00.11s | Util/Option 0m00.10s | Util/Relations 0m00.09s | Util/PointedProp 0m00.09s | Util/Prod 0m00.08s | Util/Sigma 0m00.05s | Util/Bool 0m00.05s | Spec/Encoding 0m00.05s | Util/Equality 0m00.04s | Util/Logic 0m00.04s | Util/Tactics 0m00.04s | Util/LetIn 0m00.03s | Tactics/VerdiTactics 0m00.03s | Util/IffT 0m00.03s | Util/Notations 0m00.03s | Util/Isomorphism 0m00.03s | Util/AutoRewrite 0m00.03s | Util/FixCoqMistakes 0m00.03s | Encoding/EncodingTheorems 0m00.03s | Util/HProp 0m00.02s | Util/GlobalSettings 0m00.02s | Util/Tower 0m00.02s | Util/Unit
Timing info on make coq: Time | File Name ---------------------------------------------------------------------------------- 20m12.50s | Total ---------------------------------------------------------------------------------- 2m24.50s | Specific/GF25519Reflective/Common9_4Op 1m38.02s | Specific/GF25519Reflective/Reified/AddCoordinates 1m32.95s | Test/Curve25519SpecTestVectors 1m21.69s | Experiments/Ed25519 1m18.13s | CompleteEdwardsCurve/ExtendedCoordinates 0m40.63s | ModularArithmetic/Conversion 0m34.92s | Spec/Ed25519 0m33.08s | Specific/GF25519ReflectiveAddCoordinates 0m31.63s | ModularArithmetic/ModularBaseSystemProofs 0m30.20s | Specific/GF25519Bounded 0m23.98s | Experiments/Ed25519Extraction 0m23.10s | Experiments/MontgomeryCurve 0m22.04s | ModularArithmetic/Pow2BaseProofs 0m21.68s | Reflection/Z/Interpretations128/Relations 0m20.34s | Algebra 0m20.16s | Specific/GF25519 0m18.44s | Reflection/Z/Interpretations64/Relations 0m18.22s | EdDSARepChange 0m17.19s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems 0m14.00s | Util/ZUtil 0m09.96s | Testbit 0m09.40s | Specific/GF25519BoundedCommon 0m09.09s | Assembly/GF25519 0m08.83s | Encoding/PointEncoding 0m08.78s | ModularArithmetic/Montgomery/ZProofs 0m08.75s | BoundedArithmetic/ArchitectureToZLikeProofs 0m08.51s | Specific/GF1305 0m08.40s | BoundedArithmetic/Double/Proofs/Multiply 0m08.11s | Specific/GF25519Reflective/Reified/Mul 0m07.91s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate 0m07.08s | MxDHRepChange 0m06.85s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate 0m06.56s | Reflection/Z/InterpretationsGen 0m06.33s | Specific/GF25519Reflective 0m06.12s | Bedrock/Word 0m05.55s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub 0m05.53s | Reflection/Z/Interpretations128/RelationsCombinations 0m05.46s | Reflection/Z/Interpretations64/RelationsCombinations 0m05.39s | Util/ListUtil 0m05.36s | Specific/SC25519 0m05.32s | Experiments/GenericFieldPow 0m05.21s | ModularArithmetic/ModularBaseSystemListProofs 0m04.84s | WeierstrassCurve/Pre 0m04.58s | Specific/GF25519Reflective/CommonBinOp 0m04.57s | Specific/GF25519Reflective/Reified/PreFreeze 0m04.13s | Specific/GF25519Reflective/CommonUnOp 0m04.10s | Reflection/LinearizeWf 0m04.02s | ModularArithmetic/BarrettReduction/ZHandbook 0m03.94s | Specific/GF25519Reflective/CommonUnOpWireToFE 0m03.88s | BaseSystemProofs 0m03.85s | Encoding/PointEncodingPre 0m03.62s | CompleteEdwardsCurve/Pre 0m03.50s | ModularArithmetic/Tutorial 0m03.43s | Specific/GF25519Reflective/Reified/CarrySub 0m03.39s | BoundedArithmetic/InterfaceProofs 0m03.14s | ModularArithmetic/BarrettReduction/ZGeneralized 0m03.12s | ModularArithmetic/ZBoundedZ 0m03.08s | Specific/GF25519Reflective/Common 0m03.04s | Specific/GF25519Reflective/Reified/CarryOpp 0m03.00s | Specific/GF25519Reflective/Reified/CarryAdd 0m02.93s | BoundedArithmetic/Double/Proofs/Decode 0m02.80s | Specific/GF25519ExtendedAddCoordinates 0m02.73s | ModularArithmetic/ModularArithmeticTheorems 0m02.70s | Assembly/State 0m02.69s | Specific/GF25519Reflective/CommonUnOpFEToWire 0m02.68s | Specific/GF25519BoundedAddCoordinates 0m02.65s | BoundedArithmetic/Double/Proofs/ShiftRight 0m02.60s | BoundedArithmetic/Double/Proofs/ShiftLeft 0m02.33s | ModularArithmetic/BarrettReduction/ZBounded 0m02.30s | ModularArithmetic/ModularBaseSystemOpt 0m02.12s | Specific/FancyMachine256/Barrett 0m02.10s | Specific/FancyMachine256/Montgomery 0m02.09s | Specific/GF25519Reflective/Reified/Unpack 0m02.08s | Specific/GF25519Reflective/Reified/Pack 0m02.03s | Reflection/WfReflective 0m01.99s | Specific/GF25519Reflective/Reified/Sub 0m01.96s | Reflection/WfProofs 0m01.92s | Assembly/Evaluables 0m01.92s | Util/WordUtil 0m01.89s | ModularArithmetic/Montgomery/ZBounded 0m01.82s | Specific/FancyMachine256/Core 0m01.74s | Specific/GF25519Reflective/Reified/Opp 0m01.72s | Specific/GF25519BoundedExtendedAddCoordinates 0m01.70s | Reflection/InlineWf 0m01.68s | Assembly/Compile 0m01.64s | Reflection/InlineInterp 0m01.64s | Specific/GF25519Reflective/Reified/Add 0m01.62s | Specific/GF25519Reflective/Reified/GeModulus 0m01.52s | ModularArithmetic/BarrettReduction/Z 0m01.48s | Assembly/WordizeUtil 0m01.44s | Util/NatUtil 0m01.39s | Reflection/TestCase 0m01.36s | Assembly/Bounds 0m01.29s | Util/Tuple 0m01.27s | ModularArithmetic/PrimeFieldTheorems 0m01.20s | Assembly/Conversions 0m01.17s | BaseSystem 0m01.13s | ModularArithmetic/ExtendedBaseVector 0m01.09s | BoundedArithmetic/Double/Repeated/Proofs/Decode 0m01.05s | Assembly/LL 0m01.00s | Assembly/Pipeline 0m00.92s | Specific/GF25519Reflective/CommonUnOpFEToZ 0m00.92s | Assembly/HL 0m00.91s | Util/NumTheoryUtil 0m00.88s | Assembly/PhoasCommon 0m00.87s | BoundedArithmetic/Double/Proofs/BitwiseOr 0m00.86s | BoundedArithmetic/Double/Proofs/LoadImmediate 0m00.81s | BoundedArithmetic/X86ToZLikeProofs 0m00.81s | Util/IterAssocOp 0m00.79s | Specific/GF25519Reflective/Reified 0m00.78s | Assembly/QhasmEvalCommon 0m00.73s | Reflection/Z/Syntax 0m00.70s | Encoding/ModularWordEncodingTheorems 0m00.69s | Util/PartiallyReifiedProp 0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs 0m00.64s | ModularArithmetic/ExtPow2BaseMulProofs 0m00.64s | Spec/EdDSA 0m00.63s | ModularArithmetic/ModularBaseSystem 0m00.62s | BoundedArithmetic/Double/Repeated/Proofs/Multiply 0m00.61s | Util/AdditionChainExponentiation 0m00.61s | Reflection/WfReflectiveGen 0m00.60s | Encoding/ModularWordEncodingPre 0m00.60s | ModularArithmetic/ModularBaseSystemList 0m00.58s | Reflection/InterpWfRel 0m00.58s | BoundedArithmetic/X86ToZLike 0m00.57s | Spec/ModularWordEncoding 0m00.55s | BoundedArithmetic/Interface 0m00.55s | BoundedArithmetic/Double/Proofs/SelectConditional 0m00.54s | Reflection/Syntax 0m00.53s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub 0m00.53s | Util/Decidable 0m00.52s | BoundedArithmetic/Double/Repeated/Core 0m00.52s | Reflection/LinearizeInterp 0m00.51s | BoundedArithmetic/ArchitectureToZLike 0m00.51s | Assembly/StringConversion 0m00.50s | BoundedArithmetic/Double/Core 0m00.50s | Util/HList 0m00.49s | Assembly/Qhasm 0m00.49s | ModularArithmetic/ZBounded 0m00.49s | Reflection/Named/Syntax 0m00.48s | ModularArithmetic/Pre 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr 0m00.48s | Reflection/CommonSubexpressionElimination 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate 0m00.46s | Reflection/InterpProofs 0m00.46s | Reflection/Z/Interpretations128 0m00.46s | Reflection/Z/Reify 0m00.45s | Spec/CompleteEdwardsCurve 0m00.45s | Reflection/InterpWf 0m00.44s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate 0m00.44s | Reflection/Application 0m00.44s | Assembly/QhasmUtil 0m00.43s | Reflection/Z/Interpretations64 0m00.43s | Reflection/InputSyntax 0m00.43s | Reflection/Conversion 0m00.42s | Reflection/MapInterpWf 0m00.42s | BoundedArithmetic/StripCF 0m00.42s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic 0m00.42s | Spec/WeierstrassCurve 0m00.42s | ModularArithmetic/ModularBaseSystemListZOperationsProofs 0m00.41s | ModularArithmetic/Pow2Base 0m00.41s | ModularArithmetic/PseudoMersenneBaseParams 0m00.40s | Spec/MxDH 0m00.39s | Reflection/CountLets 0m00.39s | ModularArithmetic/ModularBaseSystemWord 0m00.39s | Reflection/Named/RegisterAssign 0m00.39s | ModularArithmetic/ModularBaseSystemListZOperations 0m00.38s | BoundedArithmetic/Eta 0m00.38s | Reflection/MapInterp 0m00.37s | Reflection/Inline 0m00.37s | Tactics/Algebra_syntax/Nsatz 0m00.37s | Reflection/WfRel 0m00.36s | Reflection/Named/DeadCodeElimination 0m00.36s | ModularArithmetic/Montgomery/Z 0m00.35s | Reflection/Named/EstablishLiveness 0m00.35s | Reflection/Named/Compile 0m00.34s | Reflection/FilterLive 0m00.34s | Spec/ModularArithmetic 0m00.33s | Reflection/Linearize 0m00.33s | Reflection/Named/ContextOn 0m00.32s | Reflection/Named/NameUtil 0m00.32s | Reflection/Reify 0m00.29s | Assembly/QhasmCommon 0m00.29s | Util/Sum 0m00.28s | Bedrock/Nomega 0m00.22s | Util/CaseUtil 0m00.17s | Experiments/ExtrHaskellNats 0m00.11s | Util/Option 0m00.10s | Util/Relations 0m00.09s | Util/Prod 0m00.09s | Util/PointedProp 0m00.08s | Util/Sigma 0m00.05s | Util/Bool 0m00.05s | Spec/Encoding 0m00.05s | Util/Equality 0m00.04s | Util/LetIn 0m00.04s | Util/Logic 0m00.04s | Util/Tactics 0m00.03s | Tactics/VerdiTactics 0m00.03s | Encoding/EncodingTheorems 0m00.03s | Util/Isomorphism 0m00.03s | Util/HProp 0m00.03s | Util/Notations 0m00.03s | Util/IffT 0m00.03s | Util/AutoRewrite 0m00.03s | Util/FixCoqMistakes 0m00.02s | Util/Tower 0m00.02s | Util/GlobalSettings 0m00.02s | Util/Unit
JasonGross
force-pushed
the
eliminate-useless-carries
branch
from
fae2a70
to
663253b
Compare
|
I assume this is stale and should be closed? |
|
Yes |
JasonGross
added a commit
to JasonGross/fiat-crypto
that referenced
this pull request
Feb 21, 2022
Probably if the lists are the same lengths, then we want to compare them element-wise rather than all at once. It's way too verbose to keep expanding them, so we only do that when lists are not the same length. We now get error messages such as ``` Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]] Could not unify the values at index 0: [mit-plv#378, mit-plv#381, mit-plv#384] != [mit-plv#101, mit-plv#106, mit-plv#108] index 0: mit-plv#378 != mit-plv#101 (slice 0 44, [mit-plv#377]) != (slice 0 44, [mit-plv#98]) index 0: mit-plv#377 != mit-plv#98 (add 64, [mit-plv#345, mit-plv#375]) != (add 64, [mit-plv#57, mit-plv#96]) index 0: mit-plv#345 != mit-plv#57 (slice 0 44, [mit-plv#337]) != (slice 0 44, [#44]) index 0: mit-plv#337 != #44 (add 64, [#41, mit-plv#334]) != (add 64, [#25, #41]) index 1: mit-plv#334 != #25 (mul 64, [#1, mit-plv#331]) != (mul 64, [#0, #1, #22]) [(add 64, [mit-plv#329, mit-plv#329])] != [#0, (const 20, [])] [(add 64, [(mul 64, [#7, mit-plv#328]), (mul 64, [#7, mit-plv#328])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])]), (mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])] ``` The second to last line is generally the one to look at; the last line adds a bit more detail to it. Perhaps we should instead list out the values of indices rather than expanding one additional level?
JasonGross
added a commit
to JasonGross/fiat-crypto
that referenced
this pull request
Feb 21, 2022
Probably if the lists are the same lengths, then we want to compare them element-wise rather than all at once. It's way too verbose to keep expanding them, so we only do that when lists are not the same length. We now get error messages such as ``` Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]] Could not unify the values at index 0: [mit-plv#378, mit-plv#381, mit-plv#384] != [mit-plv#101, mit-plv#106, mit-plv#108] index 0: mit-plv#378 != mit-plv#101 (slice 0 44, [mit-plv#377]) != (slice 0 44, [mit-plv#98]) index 0: mit-plv#377 != mit-plv#98 (add 64, [mit-plv#345, mit-plv#375]) != (add 64, [mit-plv#57, mit-plv#96]) index 0: mit-plv#345 != mit-plv#57 (slice 0 44, [mit-plv#337]) != (slice 0 44, [#44]) index 0: mit-plv#337 != #44 (add 64, [#41, mit-plv#334]) != (add 64, [#25, #41]) index 1: mit-plv#334 != #25 (mul 64, [#1, mit-plv#331]) != (mul 64, [#0, #1, #22]) [(add 64, [mit-plv#329, mit-plv#329])] != [#0, (const 20, [])] [(add 64, [(mul 64, [#7, mit-plv#328]), (mul 64, [#7, mit-plv#328])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])]), (mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])] ``` The second to last line is generally the one to look at; the last line adds a bit more detail to it. Perhaps we should instead list out the values of indices rather than expanding one additional level?
JasonGross
added a commit
that referenced
this pull request
Feb 22, 2022
Probably if the lists are the same lengths, then we want to compare them element-wise rather than all at once. It's way too verbose to keep expanding them, so we only do that when lists are not the same length. We now get error messages such as ``` Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]] Could not unify the values at index 0: [#378, #381, #384] != [#101, #106, #108] index 0: #378 != #101 (slice 0 44, [#377]) != (slice 0 44, [#98]) index 0: #377 != #98 (add 64, [#345, #375]) != (add 64, [#57, #96]) index 0: #345 != #57 (slice 0 44, [#337]) != (slice 0 44, [#44]) index 0: #337 != #44 (add 64, [#41, #334]) != (add 64, [#25, #41]) index 1: #334 != #25 (mul 64, [#1, #331]) != (mul 64, [#0, #1, #22]) [(add 64, [#329, #329])] != [#0, (const 20, [])] [(add 64, [(mul 64, [#7, #328]), (mul 64, [#7, #328])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, #327])]), (mul 64, [(const 2, []), (add 64, [#0, #327])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])] [(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])] ``` The second to last line is generally the one to look at; the last line adds a bit more detail to it. Perhaps we should instead list out the values of indices rather than expanding one additional level?
dderjoel
added a commit
to dderjoel/fiat-crypto
that referenced
this pull request
Mar 22, 2022
Unable to unify: [inr [351, 349, 350]] == [inr [103, 108, 110]] Could not unify the values at index 0: [mit-plv#351, mit-plv#349, mit-plv#350] != [mit-plv#103, mit-plv#108, mit-plv#110] index 0: mit-plv#351 != mit-plv#103 (slice 0 44, [mit-plv#345]) != (slice 0 44, [mit-plv#100]) index 0: mit-plv#345 != mit-plv#100 (add 64, [mit-plv#58, mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#58, mit-plv#98]) (add 64, [mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#98]) (add 64, [mit-plv#95, (mul 64, [mit-plv#95, mit-plv#331])]) != (add 64, [(mul 64, [#3, mit-plv#95])]) (add 64, [mit-plv#95, (mul 64, [mit-plv#95, (const 4, [])])]) != (add 64, [(mul 64, [#3, mit-plv#95])]) (add 64, [(or 64, [mit-plv#91, mit-plv#93]), (mul 64, [(or 64, [mit-plv#91, mit-plv#93]), (const 4, [])])]) != (add 64, [(mul 64, [(const 5, []), (or 64, [mit-plv#91, mit-plv#93])])])
JasonGross
pushed a commit
to dderjoel/fiat-crypto
that referenced
this pull request
Mar 22, 2022
Unable to unify: [inr [351, 349, 350]] == [inr [103, 108, 110]] Could not unify the values at index 0: [mit-plv#351, mit-plv#349, mit-plv#350] != [mit-plv#103, mit-plv#108, mit-plv#110] index 0: mit-plv#351 != mit-plv#103 (slice 0 44, [mit-plv#345]) != (slice 0 44, [mit-plv#100]) index 0: mit-plv#345 != mit-plv#100 (add 64, [mit-plv#58, mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#58, mit-plv#98]) (add 64, [mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#98]) (add 64, [mit-plv#95, (mul 64, [mit-plv#95, mit-plv#331])]) != (add 64, [(mul 64, [#3, mit-plv#95])]) (add 64, [mit-plv#95, (mul 64, [mit-plv#95, (const 4, [])])]) != (add 64, [(mul 64, [#3, mit-plv#95])]) (add 64, [(or 64, [mit-plv#91, mit-plv#93]), (mul 64, [(or 64, [mit-plv#91, mit-plv#93]), (const 4, [])])]) != (add 64, [(mul 64, [(const 5, []), (or 64, [mit-plv#91, mit-plv#93])])])
JasonGross
pushed a commit
that referenced
this pull request
Mar 23, 2022
Unable to unify: [inr [351, 349, 350]] == [inr [103, 108, 110]] Could not unify the values at index 0: [#351, #349, #350] != [#103, #108, #110] index 0: #351 != #103 (slice 0 44, [#345]) != (slice 0 44, [#100]) index 0: #345 != #100 (add 64, [#58, #95, #343]) != (add 64, [#58, #98]) (add 64, [#95, #343]) != (add 64, [#98]) (add 64, [#95, (mul 64, [#95, #331])]) != (add 64, [(mul 64, [#3, #95])]) (add 64, [#95, (mul 64, [#95, (const 4, [])])]) != (add 64, [(mul 64, [#3, #95])]) (add 64, [(or 64, [#91, #93]), (mul 64, [(or 64, [#91, #93]), (const 4, [])])]) != (add 64, [(mul 64, [(const 5, []), (or 64, [#91, #93])])])
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Alas, we are now too slow for Travis, I believe, even on 8.5. (Dealing with things with 90 binders is slow.)
Timing data coming soon.