From fa027c4a37ed455a26a5bb12c6f3d54ae4bd8774 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 19 Jan 2017 19:35:24 -0500 Subject: Remove the Const constructor of exprf 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 --- src/SpecificGen/GF2213_32Reflective.v | 21 +++-- src/SpecificGen/GF2213_32Reflective/Common.v | 96 +++++++++++----------- src/SpecificGen/GF2213_32Reflective/Common9_4Op.v | 7 +- src/SpecificGen/GF2213_32Reflective/CommonBinOp.v | 7 +- src/SpecificGen/GF2213_32Reflective/CommonUnOp.v | 7 +- .../GF2213_32Reflective/CommonUnOpFEToWire.v | 7 +- .../GF2213_32Reflective/CommonUnOpFEToZ.v | 7 +- .../GF2213_32Reflective/CommonUnOpWireToFE.v | 7 +- .../GF2213_32Reflective/Reified/AddCoordinates.v | 36 ++++---- .../GF2213_32Reflective/Reified/LadderStep.v | 37 +++++---- .../GF2213_32ReflectiveAddCoordinates.v | 7 +- src/SpecificGen/GF2519_32Reflective.v | 21 +++-- src/SpecificGen/GF2519_32Reflective/Common.v | 96 +++++++++++----------- src/SpecificGen/GF2519_32Reflective/Common9_4Op.v | 7 +- src/SpecificGen/GF2519_32Reflective/CommonBinOp.v | 7 +- src/SpecificGen/GF2519_32Reflective/CommonUnOp.v | 7 +- .../GF2519_32Reflective/CommonUnOpFEToWire.v | 7 +- .../GF2519_32Reflective/CommonUnOpFEToZ.v | 7 +- .../GF2519_32Reflective/CommonUnOpWireToFE.v | 7 +- .../GF2519_32Reflective/Reified/AddCoordinates.v | 36 ++++---- .../GF2519_32Reflective/Reified/LadderStep.v | 37 +++++---- .../GF2519_32ReflectiveAddCoordinates.v | 7 +- src/SpecificGen/GF25519_32Reflective.v | 21 +++-- src/SpecificGen/GF25519_32Reflective/Common.v | 96 +++++++++++----------- src/SpecificGen/GF25519_32Reflective/Common9_4Op.v | 7 +- src/SpecificGen/GF25519_32Reflective/CommonBinOp.v | 7 +- src/SpecificGen/GF25519_32Reflective/CommonUnOp.v | 7 +- .../GF25519_32Reflective/CommonUnOpFEToWire.v | 7 +- .../GF25519_32Reflective/CommonUnOpFEToZ.v | 7 +- .../GF25519_32Reflective/CommonUnOpWireToFE.v | 7 +- .../GF25519_32Reflective/Reified/AddCoordinates.v | 36 ++++---- .../GF25519_32Reflective/Reified/LadderStep.v | 37 +++++---- .../GF25519_32ReflectiveAddCoordinates.v | 7 +- src/SpecificGen/GF25519_64Reflective.v | 21 +++-- src/SpecificGen/GF25519_64Reflective/Common.v | 96 +++++++++++----------- src/SpecificGen/GF25519_64Reflective/Common9_4Op.v | 7 +- src/SpecificGen/GF25519_64Reflective/CommonBinOp.v | 7 +- src/SpecificGen/GF25519_64Reflective/CommonUnOp.v | 7 +- .../GF25519_64Reflective/CommonUnOpFEToWire.v | 7 +- .../GF25519_64Reflective/CommonUnOpFEToZ.v | 7 +- .../GF25519_64Reflective/CommonUnOpWireToFE.v | 7 +- .../GF25519_64Reflective/Reified/AddCoordinates.v | 36 ++++---- .../GF25519_64Reflective/Reified/LadderStep.v | 37 +++++---- .../GF25519_64ReflectiveAddCoordinates.v | 7 +- src/SpecificGen/GF41417_32Reflective.v | 21 +++-- src/SpecificGen/GF41417_32Reflective/Common.v | 96 +++++++++++----------- src/SpecificGen/GF41417_32Reflective/Common9_4Op.v | 7 +- src/SpecificGen/GF41417_32Reflective/CommonBinOp.v | 7 +- src/SpecificGen/GF41417_32Reflective/CommonUnOp.v | 7 +- .../GF41417_32Reflective/CommonUnOpFEToWire.v | 7 +- .../GF41417_32Reflective/CommonUnOpFEToZ.v | 7 +- .../GF41417_32Reflective/CommonUnOpWireToFE.v | 7 +- .../GF41417_32Reflective/Reified/AddCoordinates.v | 36 ++++---- .../GF41417_32Reflective/Reified/LadderStep.v | 37 +++++---- .../GF41417_32ReflectiveAddCoordinates.v | 7 +- src/SpecificGen/GF5211_32Reflective.v | 21 +++-- src/SpecificGen/GF5211_32Reflective/Common.v | 96 +++++++++++----------- src/SpecificGen/GF5211_32Reflective/Common9_4Op.v | 7 +- src/SpecificGen/GF5211_32Reflective/CommonBinOp.v | 7 +- src/SpecificGen/GF5211_32Reflective/CommonUnOp.v | 7 +- .../GF5211_32Reflective/CommonUnOpFEToWire.v | 7 +- .../GF5211_32Reflective/CommonUnOpFEToZ.v | 7 +- .../GF5211_32Reflective/CommonUnOpWireToFE.v | 7 +- .../GF5211_32Reflective/Reified/AddCoordinates.v | 36 ++++---- .../GF5211_32Reflective/Reified/LadderStep.v | 37 +++++---- .../GF5211_32ReflectiveAddCoordinates.v | 7 +- 66 files changed, 690 insertions(+), 744 deletions(-) (limited to 'src/SpecificGen') diff --git a/src/SpecificGen/GF2213_32Reflective.v b/src/SpecificGen/GF2213_32Reflective.v index 8b09203e9..2f43e92fd 100644 --- a/src/SpecificGen/GF2213_32Reflective.v +++ b/src/SpecificGen/GF2213_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF2213_32BoundedCommon.wire_digitsW -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v index 56e4bc47c..977f47e69 100644 --- a/src/SpecificGen/GF2213_32Reflective/Common.v +++ b/src/SpecificGen/GF2213_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Export Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Util.Tower. Require Import Crypto.Util.LetIn. @@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type WordW.interp_base_type op). +Notation Expr := (Expr base_type op). Local Ltac make_type_from' T := let T := (eval compute in T) in @@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition expr_nm_Op count_in count_out interp_base_type var : Type - := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). -Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. -Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). -Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. -Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. -Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. -Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. -Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. -Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Definition expr_nm_Op count_in count_out var : Type + := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out). +Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT. +Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT. +Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT. +Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT. +Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ). +Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT. +Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET. +Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT. +Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT. +Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT. +Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT. +Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT. Local Ltac bounds_from_list_cps ls := lazymatch (eval hnf in ls) with @@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe2213_32 op)) Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in let ropZ_sig := ropZ_sigv in - let ropW := MapInterp (fun _ x => x) ropW' in - let ropZ := MapInterp WordW.to_Z ropW' in - let ropBounds := MapInterp ZBounds.of_wordW ropW' in - let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in + let ropW := ropW' in + let ropZ := ropW' in + let ropBounds := ropW' in + let ropBoundedWordW := ropW' in ropZ = proj1_sig ropZ_sig /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ) /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds) @@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in - refine (LetIn (UnReturn x) _); + let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in + refine (LetIn (invert_Return x) _); let x'' := fresh "x''" in intro x''; let xv := assoc_right_tuple x'' (@None) in refine (SmartVarf (xv : interp_flat_type _ t')). -Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var. +Definition unop_make_args {var} (x : exprArg var) : exprArgRev var. Proof. make_args x. Defined. -Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var. +Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var. Proof. make_args x. Defined. Local Ltac args_to_bounded x H := @@ -432,31 +432,31 @@ Defined. Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool. Proof. make_bounds_prop bounds Expr4Op_bounds. Defined. -Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var +Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe2213_32 f k)). -Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2213_32 f k)). +Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var := fun x y - => LetIn (UnReturn (unop_make_args x)) + => LetIn (invert_Return (unop_make_args x)) (fun x' - => LetIn (UnReturn (unop_make_args y)) + => LetIn (invert_Return (unop_make_args y)) (fun y' - => UnReturn (Apply length_fe2213_32 + => invert_Return (Apply length_fe2213_32 (Apply length_fe2213_32 f x') y'))). -Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var +Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe2213_32 f k)). -Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2213_32 f k)). +Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var := fun x - => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (List.length wire_widths) f k)). -Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var + => LetIn (invert_Return (unop_wire_make_args x)) + (fun k => invert_Return (Apply (List.length wire_widths) f k)). +Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe2213_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2213_32 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the @@ -545,17 +545,14 @@ Ltac rexpr_correct := assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); cbv zeta; repeat apply conj; [ vm_compute; reflexivity - | apply @InterpRelWf; - [ | apply @RelWfMapInterp, wf_ropW ].. ]; + | apply @InterpWf; + [ | apply wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). - -Definition rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize end) x. +Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds) (only parsing). @@ -586,6 +583,7 @@ Module Export PrettyPrinting. | in_range _ _ => no | enlargen _ => borked end + | Unit => fun _ => no | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no | yes, no | no, yes | yes, yes => yes diff --git a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v index d8d55ca04..49a4782eb 100644 --- a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. diff --git a/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v index 23becba34..0cdef8deb 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => binop_bounds_good bounds = true | None => False end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : binop_correct_and_bounded ropW op. Proof. intros x y Hx Hy. pose x as x'; pose y as y'. diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v index 250a64400..5df7f6c98 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded (Hx : is_bounded (fe2213_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unop_bounds_good bounds = true | None => False end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v index 2dcae7edd..0751754d7 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded (Hx : is_bounded (fe2213_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToWire_bounds_good bounds = true | None => False end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_FEToWire_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v index ef997e3f9..d6cf8653d 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe2213_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToZ_bounds_good bounds = true | None => False end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v index 4342ef865..15dc52517 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded let args := unopWireToFE_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopWireToFE_bounds_good bounds = true | None => False end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_WireToFE_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v index 76c119adc..c2fb547d0 100644 --- a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Export Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF2213_32.fe2213_32 -> GF2213_32.fe2213_32 -> GF2213_32.fe2213_32) (x' y' : GF2213_32.fe2213_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2213_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe2213_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe2213_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe2213_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v index 18bbd8289..51b07c4d6 100644 --- a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Export Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Add. @@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) a24 _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) x0 P1 P2. -Definition rladderstepZ'' : Syntax.Expr _ _ _ _ +Definition rladderstepZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF2213_32.fe2213_32 -> GF2213_32.fe2213_32 -> GF2213_32.fe2213_32) (x' y' : GF2213_32.fe2213_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2213_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe2213_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -107,14 +107,15 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe2213_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + let f := match goal with f : expr _ _ _ |- _ => f end in + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -125,7 +126,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe2213_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 ladderstep]. intros; cbv beta zeta. - unfold UnReturn at 14 15 16 17. + unfold invert_Return at 14 15 16 17. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -148,9 +149,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v index 3b95ae5c4..4dd4b8e9e 100644 --- a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF2213_32BoundedCommon.fe2 -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF2519_32Reflective.v b/src/SpecificGen/GF2519_32Reflective.v index 5ebb35b5e..f3c1d7c08 100644 --- a/src/SpecificGen/GF2519_32Reflective.v +++ b/src/SpecificGen/GF2519_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF2519_32BoundedCommon.wire_digitsW -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v index dd7be148a..6f6f607fb 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common.v +++ b/src/SpecificGen/GF2519_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Export Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Util.Tower. Require Import Crypto.Util.LetIn. @@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type WordW.interp_base_type op). +Notation Expr := (Expr base_type op). Local Ltac make_type_from' T := let T := (eval compute in T) in @@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition expr_nm_Op count_in count_out interp_base_type var : Type - := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). -Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. -Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). -Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. -Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. -Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. -Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. -Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. -Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Definition expr_nm_Op count_in count_out var : Type + := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out). +Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT. +Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT. +Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT. +Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT. +Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ). +Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT. +Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET. +Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT. +Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT. +Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT. +Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT. +Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT. Local Ltac bounds_from_list_cps ls := lazymatch (eval hnf in ls) with @@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe2519_32 op)) Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in let ropZ_sig := ropZ_sigv in - let ropW := MapInterp (fun _ x => x) ropW' in - let ropZ := MapInterp WordW.to_Z ropW' in - let ropBounds := MapInterp ZBounds.of_wordW ropW' in - let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in + let ropW := ropW' in + let ropZ := ropW' in + let ropBounds := ropW' in + let ropBoundedWordW := ropW' in ropZ = proj1_sig ropZ_sig /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ) /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds) @@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in - refine (LetIn (UnReturn x) _); + let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in + refine (LetIn (invert_Return x) _); let x'' := fresh "x''" in intro x''; let xv := assoc_right_tuple x'' (@None) in refine (SmartVarf (xv : interp_flat_type _ t')). -Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var. +Definition unop_make_args {var} (x : exprArg var) : exprArgRev var. Proof. make_args x. Defined. -Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var. +Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var. Proof. make_args x. Defined. Local Ltac args_to_bounded x H := @@ -432,31 +432,31 @@ Defined. Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool. Proof. make_bounds_prop bounds Expr4Op_bounds. Defined. -Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var +Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe2519_32 f k)). -Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2519_32 f k)). +Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var := fun x y - => LetIn (UnReturn (unop_make_args x)) + => LetIn (invert_Return (unop_make_args x)) (fun x' - => LetIn (UnReturn (unop_make_args y)) + => LetIn (invert_Return (unop_make_args y)) (fun y' - => UnReturn (Apply length_fe2519_32 + => invert_Return (Apply length_fe2519_32 (Apply length_fe2519_32 f x') y'))). -Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var +Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe2519_32 f k)). -Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2519_32 f k)). +Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var := fun x - => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (List.length wire_widths) f k)). -Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var + => LetIn (invert_Return (unop_wire_make_args x)) + (fun k => invert_Return (Apply (List.length wire_widths) f k)). +Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe2519_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2519_32 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the @@ -545,17 +545,14 @@ Ltac rexpr_correct := assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); cbv zeta; repeat apply conj; [ vm_compute; reflexivity - | apply @InterpRelWf; - [ | apply @RelWfMapInterp, wf_ropW ].. ]; + | apply @InterpWf; + [ | apply wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). - -Definition rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize end) x. +Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds) (only parsing). @@ -586,6 +583,7 @@ Module Export PrettyPrinting. | in_range _ _ => no | enlargen _ => borked end + | Unit => fun _ => no | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no | yes, no | no, yes | yes, yes => yes diff --git a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v index 1cedb55ac..6a07ae3cf 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. diff --git a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v index 095c7a8c6..e20ab88d1 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => binop_bounds_good bounds = true | None => False end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : binop_correct_and_bounded ropW op. Proof. intros x y Hx Hy. pose x as x'; pose y as y'. diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v index f2e091570..505a9a9ce 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded (Hx : is_bounded (fe2519_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unop_bounds_good bounds = true | None => False end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v index cf8a85d6f..e84df9be2 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded (Hx : is_bounded (fe2519_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToWire_bounds_good bounds = true | None => False end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_FEToWire_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v index 7d70c1234..054155d1f 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe2519_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToZ_bounds_good bounds = true | None => False end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v index 22e68fcf5..b22e73f6e 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded let args := unopWireToFE_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopWireToFE_bounds_good bounds = true | None => False end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_WireToFE_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v index 332178361..1e74a8cf5 100644 --- a/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Export Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF2519_32.fe2519_32 -> GF2519_32.fe2519_32 -> GF2519_32.fe2519_32) (x' y' : GF2519_32.fe2519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2519_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe2519_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe2519_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe2519_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2519_32 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v index e5ea0e52b..3a069c45c 100644 --- a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Export Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Add. @@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) a24 _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) x0 P1 P2. -Definition rladderstepZ'' : Syntax.Expr _ _ _ _ +Definition rladderstepZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF2519_32.fe2519_32 -> GF2519_32.fe2519_32 -> GF2519_32.fe2519_32) (x' y' : GF2519_32.fe2519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2519_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe2519_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -107,14 +107,15 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe2519_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + let f := match goal with f : expr _ _ _ |- _ => f end in + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -125,7 +126,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe2519_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2519_32 ladderstep]. intros; cbv beta zeta. - unfold UnReturn at 14 15 16 17. + unfold invert_Return at 14 15 16 17. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -148,9 +149,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v index a400a893a..e1f691607 100644 --- a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF2519_32BoundedCommon.fe2 -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> Tuple.tuple SpecificGen.GF2519_32BoundedCommon.fe2519_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF25519_32Reflective.v b/src/SpecificGen/GF25519_32Reflective.v index 92a1bdbf8..d3e45d36d 100644 --- a/src/SpecificGen/GF25519_32Reflective.v +++ b/src/SpecificGen/GF25519_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF25519_32BoundedCommon.wire_digitsW -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v index 644ed7c92..bd01c31a2 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common.v +++ b/src/SpecificGen/GF25519_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Export Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Util.Tower. Require Import Crypto.Util.LetIn. @@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type WordW.interp_base_type op). +Notation Expr := (Expr base_type op). Local Ltac make_type_from' T := let T := (eval compute in T) in @@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition expr_nm_Op count_in count_out interp_base_type var : Type - := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). -Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. -Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). -Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. -Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. -Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. -Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. -Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. -Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Definition expr_nm_Op count_in count_out var : Type + := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out). +Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT. +Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT. +Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT. +Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT. +Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ). +Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT. +Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET. +Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT. +Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT. +Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT. +Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT. +Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT. Local Ltac bounds_from_list_cps ls := lazymatch (eval hnf in ls) with @@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519_32 op) Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in let ropZ_sig := ropZ_sigv in - let ropW := MapInterp (fun _ x => x) ropW' in - let ropZ := MapInterp WordW.to_Z ropW' in - let ropBounds := MapInterp ZBounds.of_wordW ropW' in - let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in + let ropW := ropW' in + let ropZ := ropW' in + let ropBounds := ropW' in + let ropBoundedWordW := ropW' in ropZ = proj1_sig ropZ_sig /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ) /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds) @@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in - refine (LetIn (UnReturn x) _); + let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in + refine (LetIn (invert_Return x) _); let x'' := fresh "x''" in intro x''; let xv := assoc_right_tuple x'' (@None) in refine (SmartVarf (xv : interp_flat_type _ t')). -Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var. +Definition unop_make_args {var} (x : exprArg var) : exprArgRev var. Proof. make_args x. Defined. -Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var. +Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var. Proof. make_args x. Defined. Local Ltac args_to_bounded x H := @@ -432,31 +432,31 @@ Defined. Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool. Proof. make_bounds_prop bounds Expr4Op_bounds. Defined. -Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var +Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_32 f k)). -Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_32 f k)). +Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var := fun x y - => LetIn (UnReturn (unop_make_args x)) + => LetIn (invert_Return (unop_make_args x)) (fun x' - => LetIn (UnReturn (unop_make_args y)) + => LetIn (invert_Return (unop_make_args y)) (fun y' - => UnReturn (Apply length_fe25519_32 + => invert_Return (Apply length_fe25519_32 (Apply length_fe25519_32 f x') y'))). -Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var +Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_32 f k)). -Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_32 f k)). +Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var := fun x - => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (List.length wire_widths) f k)). -Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var + => LetIn (invert_Return (unop_wire_make_args x)) + (fun k => invert_Return (Apply (List.length wire_widths) f k)). +Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_32 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the @@ -545,17 +545,14 @@ Ltac rexpr_correct := assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); cbv zeta; repeat apply conj; [ vm_compute; reflexivity - | apply @InterpRelWf; - [ | apply @RelWfMapInterp, wf_ropW ].. ]; + | apply @InterpWf; + [ | apply wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). - -Definition rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize end) x. +Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds) (only parsing). @@ -586,6 +583,7 @@ Module Export PrettyPrinting. | in_range _ _ => no | enlargen _ => borked end + | Unit => fun _ => no | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no | yes, no | no, yes | yes, yes => yes diff --git a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v index c163fa18a..fc0bf3d0b 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. diff --git a/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v index f254a2d3a..3053b6d51 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => binop_bounds_good bounds = true | None => False end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : binop_correct_and_bounded ropW op. Proof. intros x y Hx Hy. pose x as x'; pose y as y'. diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v index 246dcbf70..dd7c392b1 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded (Hx : is_bounded (fe25519_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unop_bounds_good bounds = true | None => False end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v index a940a0c8b..f05bfdba4 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded (Hx : is_bounded (fe25519_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToWire_bounds_good bounds = true | None => False end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_FEToWire_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v index b7ec2c6a5..ea8f01446 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe25519_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToZ_bounds_good bounds = true | None => False end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v index 34e0896f1..2a19f9eb1 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded let args := unopWireToFE_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopWireToFE_bounds_good bounds = true | None => False end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_WireToFE_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v index 567ed1a01..c276df344 100644 --- a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Export Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF25519_32.fe25519_32 -> GF25519_32.fe25519_32 -> GF25519_32.fe25519_32) (x' y' : GF25519_32.fe25519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe25519_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_32 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v index 9fc865d98..33b232dc2 100644 --- a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Export Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Add. @@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) a24 _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) x0 P1 P2. -Definition rladderstepZ'' : Syntax.Expr _ _ _ _ +Definition rladderstepZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF25519_32.fe25519_32 -> GF25519_32.fe25519_32 -> GF25519_32.fe25519_32) (x' y' : GF25519_32.fe25519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -107,14 +107,15 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe25519_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + let f := match goal with f : expr _ _ _ |- _ => f end in + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -125,7 +126,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_32 ladderstep]. intros; cbv beta zeta. - unfold UnReturn at 14 15 16 17. + unfold invert_Return at 14 15 16 17. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -148,9 +149,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v index b13c07f44..b4840a4d2 100644 --- a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF25519_32BoundedCommon.fe -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> Tuple.tuple SpecificGen.GF25519_32BoundedCommon.fe25519_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF25519_64Reflective.v b/src/SpecificGen/GF25519_64Reflective.v index 86b8735d6..620c96713 100644 --- a/src/SpecificGen/GF25519_64Reflective.v +++ b/src/SpecificGen/GF25519_64Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations128. Require Crypto.Reflection.Z.Interpretations128.Relations. Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr (rword128ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr (rword128ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.word128 - := Eval asm_interp in interp_uexpr_FEToZ (rword128ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword128ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF25519_64BoundedCommon.wire_digitsW -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr_WireToFE (rword128ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v index c7b1a69fb..dd78063a8 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common.v +++ b/src/SpecificGen/GF25519_64Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Export Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Z.Interpretations128. Require Crypto.Reflection.Z.Interpretations128.Relations. Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. @@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Util.Tower. Require Import Crypto.Util.LetIn. @@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type WordW.interp_base_type op). +Notation Expr := (Expr base_type op). Local Ltac make_type_from' T := let T := (eval compute in T) in @@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition expr_nm_Op count_in count_out interp_base_type var : Type - := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). -Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. -Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). -Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. -Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. -Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. -Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. -Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. -Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Definition expr_nm_Op count_in count_out var : Type + := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out). +Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT. +Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT. +Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT. +Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT. +Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ). +Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT. +Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET. +Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT. +Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT. +Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT. +Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT. +Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT. Local Ltac bounds_from_list_cps ls := lazymatch (eval hnf in ls) with @@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519_64 op) Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in let ropZ_sig := ropZ_sigv in - let ropW := MapInterp (fun _ x => x) ropW' in - let ropZ := MapInterp WordW.to_Z ropW' in - let ropBounds := MapInterp ZBounds.of_wordW ropW' in - let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in + let ropW := ropW' in + let ropZ := ropW' in + let ropBounds := ropW' in + let ropBoundedWordW := ropW' in ropZ = proj1_sig ropZ_sig /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ) /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds) @@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in - refine (LetIn (UnReturn x) _); + let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in + refine (LetIn (invert_Return x) _); let x'' := fresh "x''" in intro x''; let xv := assoc_right_tuple x'' (@None) in refine (SmartVarf (xv : interp_flat_type _ t')). -Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var. +Definition unop_make_args {var} (x : exprArg var) : exprArgRev var. Proof. make_args x. Defined. -Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var. +Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var. Proof. make_args x. Defined. Local Ltac args_to_bounded x H := @@ -432,31 +432,31 @@ Defined. Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool. Proof. make_bounds_prop bounds Expr4Op_bounds. Defined. -Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var +Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_64 f k)). -Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_64 f k)). +Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var := fun x y - => LetIn (UnReturn (unop_make_args x)) + => LetIn (invert_Return (unop_make_args x)) (fun x' - => LetIn (UnReturn (unop_make_args y)) + => LetIn (invert_Return (unop_make_args y)) (fun y' - => UnReturn (Apply length_fe25519_64 + => invert_Return (Apply length_fe25519_64 (Apply length_fe25519_64 f x') y'))). -Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var +Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_64 f k)). -Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_64 f k)). +Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var := fun x - => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (List.length wire_widths) f k)). -Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var + => LetIn (invert_Return (unop_wire_make_args x)) + (fun k => invert_Return (Apply (List.length wire_widths) f k)). +Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_64 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_64 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the @@ -545,17 +545,14 @@ Ltac rexpr_correct := assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); cbv zeta; repeat apply conj; [ vm_compute; reflexivity - | apply @InterpRelWf; - [ | apply @RelWfMapInterp, wf_ropW ].. ]; + | apply @InterpWf; + [ | apply wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). - -Definition rword128ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word128ize end) x. +Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds) (only parsing). @@ -586,6 +583,7 @@ Module Export PrettyPrinting. | in_range _ _ => no | enlargen _ => borked end + | Unit => fun _ => no | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no | yes, no | no, yes | yes, yes => yes diff --git a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v index 634ec3388..9699d43b4 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v index c8872efc5..5ebff74a9 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => binop_bounds_good bounds = true | None => False end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : binop_correct_and_bounded ropW op. Proof. intros x y Hx Hy. pose x as x'; pose y as y'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v index f6a71740a..53b0c372f 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded (Hx : is_bounded (fe25519_64WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unop_bounds_good bounds = true | None => False end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v index 7bd176749..b9c642d43 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded (Hx : is_bounded (fe25519_64WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToWire_bounds_good bounds = true | None => False end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_FEToWire_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v index d6b8bb2c7..fcc07a651 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe25519_64WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToZ_bounds_good bounds = true | None => False end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v index baadad3c3..09292ea2c 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded let args := unopWireToFE_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopWireToFE_bounds_good bounds = true | None => False end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_WireToFE_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v index 4143ad79b..a109ec89b 100644 --- a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Export Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations128. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF25519_64.fe25519_64 -> GF25519_64.fe25519_64 -> GF25519_64.fe25519_64) (x' y' : GF25519_64.fe25519_64) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_64 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_64 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe25519_64 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519_64 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v index 38bd20c08..c105a2846 100644 --- a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Export Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations128. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add. @@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) a24 _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) x0 P1 P2. -Definition rladderstepZ'' : Syntax.Expr _ _ _ _ +Definition rladderstepZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF25519_64.fe25519_64 -> GF25519_64.fe25519_64 -> GF25519_64.fe25519_64) (x' y' : GF25519_64.fe25519_64) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_64 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_64 interp_flat_type] in H. simpl @interp_base_type in *. @@ -107,14 +107,15 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe25519_64 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + let f := match goal with f : expr _ _ _ |- _ => f end in + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -125,7 +126,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519_64 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 ladderstep]. intros; cbv beta zeta. - unfold UnReturn at 14 15 16 17. + unfold invert_Return at 14 15 16 17. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -148,9 +149,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v index e9067cee8..9050ee849 100644 --- a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations128. Require Crypto.Reflection.Z.Interpretations128.Relations. Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF25519_64BoundedCommon.fe -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword128ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF41417_32Reflective.v b/src/SpecificGen/GF41417_32Reflective.v index 5f37c51fa..efc54565e 100644 --- a/src/SpecificGen/GF41417_32Reflective.v +++ b/src/SpecificGen/GF41417_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF41417_32BoundedCommon.wire_digitsW -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v index b9f98cfba..9ab04a78f 100644 --- a/src/SpecificGen/GF41417_32Reflective/Common.v +++ b/src/SpecificGen/GF41417_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Export Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Util.Tower. Require Import Crypto.Util.LetIn. @@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type WordW.interp_base_type op). +Notation Expr := (Expr base_type op). Local Ltac make_type_from' T := let T := (eval compute in T) in @@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition expr_nm_Op count_in count_out interp_base_type var : Type - := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). -Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. -Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). -Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. -Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. -Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. -Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. -Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. -Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Definition expr_nm_Op count_in count_out var : Type + := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out). +Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT. +Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT. +Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT. +Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT. +Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ). +Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT. +Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET. +Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT. +Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT. +Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT. +Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT. +Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT. Local Ltac bounds_from_list_cps ls := lazymatch (eval hnf in ls) with @@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe41417_32 op) Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in let ropZ_sig := ropZ_sigv in - let ropW := MapInterp (fun _ x => x) ropW' in - let ropZ := MapInterp WordW.to_Z ropW' in - let ropBounds := MapInterp ZBounds.of_wordW ropW' in - let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in + let ropW := ropW' in + let ropZ := ropW' in + let ropBounds := ropW' in + let ropBoundedWordW := ropW' in ropZ = proj1_sig ropZ_sig /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ) /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds) @@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in - refine (LetIn (UnReturn x) _); + let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in + refine (LetIn (invert_Return x) _); let x'' := fresh "x''" in intro x''; let xv := assoc_right_tuple x'' (@None) in refine (SmartVarf (xv : interp_flat_type _ t')). -Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var. +Definition unop_make_args {var} (x : exprArg var) : exprArgRev var. Proof. make_args x. Defined. -Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var. +Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var. Proof. make_args x. Defined. Local Ltac args_to_bounded x H := @@ -432,31 +432,31 @@ Defined. Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool. Proof. make_bounds_prop bounds Expr4Op_bounds. Defined. -Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var +Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe41417_32 f k)). -Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe41417_32 f k)). +Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var := fun x y - => LetIn (UnReturn (unop_make_args x)) + => LetIn (invert_Return (unop_make_args x)) (fun x' - => LetIn (UnReturn (unop_make_args y)) + => LetIn (invert_Return (unop_make_args y)) (fun y' - => UnReturn (Apply length_fe41417_32 + => invert_Return (Apply length_fe41417_32 (Apply length_fe41417_32 f x') y'))). -Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var +Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe41417_32 f k)). -Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe41417_32 f k)). +Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var := fun x - => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (List.length wire_widths) f k)). -Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var + => LetIn (invert_Return (unop_wire_make_args x)) + (fun k => invert_Return (Apply (List.length wire_widths) f k)). +Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe41417_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe41417_32 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the @@ -545,17 +545,14 @@ Ltac rexpr_correct := assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); cbv zeta; repeat apply conj; [ vm_compute; reflexivity - | apply @InterpRelWf; - [ | apply @RelWfMapInterp, wf_ropW ].. ]; + | apply @InterpWf; + [ | apply wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). - -Definition rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize end) x. +Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds) (only parsing). @@ -586,6 +583,7 @@ Module Export PrettyPrinting. | in_range _ _ => no | enlargen _ => borked end + | Unit => fun _ => no | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no | yes, no | no, yes | yes, yes => yes diff --git a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v index d7916c957..f1230b04e 100644 --- a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. diff --git a/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v index 3542dc9cf..438110cb8 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => binop_bounds_good bounds = true | None => False end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : binop_correct_and_bounded ropW op. Proof. intros x y Hx Hy. pose x as x'; pose y as y'. diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v index 7d86a5e95..b3d00f8c9 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded (Hx : is_bounded (fe41417_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unop_bounds_good bounds = true | None => False end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v index a008c50bb..8a8075739 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded (Hx : is_bounded (fe41417_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToWire_bounds_good bounds = true | None => False end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_FEToWire_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v index 700581bad..19664d936 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe41417_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToZ_bounds_good bounds = true | None => False end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v index d04d44d32..7c23f3be8 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded let args := unopWireToFE_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopWireToFE_bounds_good bounds = true | None => False end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_WireToFE_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v index 8288d10e0..4c658f227 100644 --- a/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Export Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF41417_32.fe41417_32 -> GF41417_32.fe41417_32 -> GF41417_32.fe41417_32) (x' y' : GF41417_32.fe41417_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe41417_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe41417_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe41417_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe41417_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe41417_32 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v index 7384553a5..1f3516551 100644 --- a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Export Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Add. @@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) a24 _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) x0 P1 P2. -Definition rladderstepZ'' : Syntax.Expr _ _ _ _ +Definition rladderstepZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF41417_32.fe41417_32 -> GF41417_32.fe41417_32 -> GF41417_32.fe41417_32) (x' y' : GF41417_32.fe41417_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe41417_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe41417_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -107,14 +107,15 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe41417_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + let f := match goal with f : expr _ _ _ |- _ => f end in + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -125,7 +126,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe41417_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe41417_32 ladderstep]. intros; cbv beta zeta. - unfold UnReturn at 14 15 16 17. + unfold invert_Return at 14 15 16 17. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -148,9 +149,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v index 6d4dd60bb..82f159e25 100644 --- a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF41417_32BoundedCommon.fe -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> Tuple.tuple SpecificGen.GF41417_32BoundedCommon.fe41417_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF5211_32Reflective.v b/src/SpecificGen/GF5211_32Reflective.v index faf61f8c2..8c80562de 100644 --- a/src/SpecificGen/GF5211_32Reflective.v +++ b/src/SpecificGen/GF5211_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF5211_32BoundedCommon.wire_digitsW -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v index 396d2cd35..670234315 100644 --- a/src/SpecificGen/GF5211_32Reflective/Common.v +++ b/src/SpecificGen/GF5211_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Util.Tower. Require Import Crypto.Util.LetIn. @@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type WordW.interp_base_type op). +Notation Expr := (Expr base_type op). Local Ltac make_type_from' T := let T := (eval compute in T) in @@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition expr_nm_Op count_in count_out interp_base_type var : Type - := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). -Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. -Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). -Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. -Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. -Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. -Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. -Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. -Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Definition expr_nm_Op count_in count_out var : Type + := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out). +Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT. +Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT. +Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT. +Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT. +Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ). +Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT. +Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET. +Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT. +Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT. +Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT. +Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT. +Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT. Local Ltac bounds_from_list_cps ls := lazymatch (eval hnf in ls) with @@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe5211_32 op)) Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in let ropZ_sig := ropZ_sigv in - let ropW := MapInterp (fun _ x => x) ropW' in - let ropZ := MapInterp WordW.to_Z ropW' in - let ropBounds := MapInterp ZBounds.of_wordW ropW' in - let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in + let ropW := ropW' in + let ropZ := ropW' in + let ropBounds := ropW' in + let ropBoundedWordW := ropW' in ropZ = proj1_sig ropZ_sig /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ) /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds) @@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in - refine (LetIn (UnReturn x) _); + let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in + refine (LetIn (invert_Return x) _); let x'' := fresh "x''" in intro x''; let xv := assoc_right_tuple x'' (@None) in refine (SmartVarf (xv : interp_flat_type _ t')). -Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var. +Definition unop_make_args {var} (x : exprArg var) : exprArgRev var. Proof. make_args x. Defined. -Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var. +Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var. Proof. make_args x. Defined. Local Ltac args_to_bounded x H := @@ -432,31 +432,31 @@ Defined. Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool. Proof. make_bounds_prop bounds Expr4Op_bounds. Defined. -Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var +Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe5211_32 f k)). -Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe5211_32 f k)). +Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var := fun x y - => LetIn (UnReturn (unop_make_args x)) + => LetIn (invert_Return (unop_make_args x)) (fun x' - => LetIn (UnReturn (unop_make_args y)) + => LetIn (invert_Return (unop_make_args y)) (fun y' - => UnReturn (Apply length_fe5211_32 + => invert_Return (Apply length_fe5211_32 (Apply length_fe5211_32 f x') y'))). -Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var +Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe5211_32 f k)). -Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe5211_32 f k)). +Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var := fun x - => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (List.length wire_widths) f k)). -Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var + => LetIn (invert_Return (unop_wire_make_args x)) + (fun k => invert_Return (Apply (List.length wire_widths) f k)). +Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe5211_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe5211_32 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the @@ -545,17 +545,14 @@ Ltac rexpr_correct := assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); cbv zeta; repeat apply conj; [ vm_compute; reflexivity - | apply @InterpRelWf; - [ | apply @RelWfMapInterp, wf_ropW ].. ]; + | apply @InterpWf; + [ | apply wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). - -Definition rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize end) x. +Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds) (only parsing). @@ -586,6 +583,7 @@ Module Export PrettyPrinting. | in_range _ _ => no | enlargen _ => borked end + | Unit => fun _ => no | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no | yes, no | no, yes | yes, yes => yes diff --git a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v index 627b8849d..b1da3f12f 100644 --- a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v index ccaefeb38..2395d7c74 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => binop_bounds_good bounds = true | None => False end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : binop_correct_and_bounded ropW op. Proof. intros x y Hx Hy. pose x as x'; pose y as y'. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v index 4c8c024ef..29652a1e8 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded (Hx : is_bounded (fe5211_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unop_bounds_good bounds = true | None => False end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v index 4abf5e85f..9d37b910f 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded (Hx : is_bounded (fe5211_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToWire_bounds_good bounds = true | None => False end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_FEToWire_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v index 821f6529c..9dde1f276 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe5211_32WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopFEToZ_bounds_good bounds = true | None => False end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v index 9284bf40f..e20146853 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded let args := unopWireToFE_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => unopWireToFE_bounds_good bounds = true | None => False end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : unop_WireToFE_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v index 26fb59a04..85da73838 100644 --- a/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF5211_32.fe5211_32 -> GF5211_32.fe5211_32 -> GF5211_32.fe5211_32) (x' y' : GF5211_32.fe5211_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe5211_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe5211_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe5211_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe5211_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe5211_32 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v index 71cb965a9..b05fc64a6 100644 --- a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations64. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Add. @@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) a24 _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) x0 P1 P2. -Definition rladderstepZ'' : Syntax.Expr _ _ _ _ +Definition rladderstepZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF5211_32.fe5211_32 -> GF5211_32.fe5211_32 -> GF5211_32.fe5211_32) (x' y' : GF5211_32.fe5211_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe5211_32 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe5211_32 interp_flat_type] in H. simpl @interp_base_type in *. @@ -107,14 +107,15 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe5211_32 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + let f := match goal with f : expr _ _ _ |- _ => f end in + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -125,7 +126,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe5211_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe5211_32 ladderstep]. intros; cbv beta zeta. - unfold UnReturn at 14 15 16 17. + unfold invert_Return at 14 15 16 17. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -148,9 +149,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v index ddba2a199..5284ffbcd 100644 --- a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF5211_32BoundedCommon.fe5 -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> Tuple.tuple SpecificGen.GF5211_32BoundedCommon.fe5211_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. -- cgit v1.2.3