path: root/_CoqProject

-R src Crypto
-R Bedrock Bedrock
Bedrock/Nomega.v
Bedrock/Word.v
src/Algebra.v
src/BaseSystem.v
src/BaseSystemProofs.v
src/EdDSARepChange.v
src/MxDHRepChange.v
src/Testbit.v
src/Assembly/Bounds.v
src/Assembly/Compile.v
src/Assembly/Conversions.v
src/Assembly/Evaluables.v
src/Assembly/GF25519.v
src/Assembly/HL.v
src/Assembly/LL.v
src/Assembly/PhoasCommon.v
src/Assembly/Pipeline.v
src/Assembly/Qhasm.v
src/Assembly/QhasmCommon.v
src/Assembly/QhasmEvalCommon.v
src/Assembly/QhasmUtil.v
src/Assembly/State.v
src/Assembly/StringConversion.v
src/Assembly/WordizeUtil.v
src/BoundedArithmetic/ArchitectureToZLike.v
src/BoundedArithmetic/ArchitectureToZLikeProofs.v
src/BoundedArithmetic/Eta.v
src/BoundedArithmetic/Interface.v
src/BoundedArithmetic/InterfaceProofs.v
src/BoundedArithmetic/StripCF.v
src/BoundedArithmetic/X86ToZLike.v
src/BoundedArithmetic/X86ToZLikeProofs.v
src/BoundedArithmetic/Double/Core.v
src/BoundedArithmetic/Double/Proofs/BitwiseOr.v
src/BoundedArithmetic/Double/Proofs/Decode.v
src/BoundedArithmetic/Double/Proofs/LoadImmediate.v
src/BoundedArithmetic/Double/Proofs/Multiply.v
src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v
src/BoundedArithmetic/Double/Proofs/SelectConditional.v
src/BoundedArithmetic/Double/Proofs/ShiftLeft.v
src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v
src/BoundedArithmetic/Double/Proofs/ShiftRight.v
src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v
src/BoundedArithmetic/Double/Repeated/Core.v
src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v
src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v
src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v
src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v
src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v
src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v
src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v
src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
src/CompleteEdwardsCurve/ExtendedCoordinates.v
src/CompleteEdwardsCurve/Pre.v
src/Encoding/EncodingTheorems.v
src/Encoding/ModularWordEncodingPre.v
src/Encoding/ModularWordEncodingTheorems.v
src/Encoding/PointEncoding.v
src/Encoding/PointEncodingPre.v
src/Experiments/Ed25519.v
src/Experiments/Ed25519Extraction.v
src/Experiments/ExtrHaskellNats.v
src/Experiments/GenericFieldPow.v
src/Experiments/MontgomeryCurve.v
src/ModularArithmetic/Conversion.v
src/ModularArithmetic/ExtPow2BaseMulProofs.v
src/ModularArithmetic/ExtendedBaseVector.v
src/ModularArithmetic/ModularArithmeticTheorems.v
src/ModularArithmetic/ModularBaseSystem.v
src/ModularArithmetic/ModularBaseSystemList.v
src/ModularArithmetic/ModularBaseSystemListProofs.v
src/ModularArithmetic/ModularBaseSystemListZOperations.v
src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
src/ModularArithmetic/ModularBaseSystemOpt.v
src/ModularArithmetic/ModularBaseSystemProofs.v
src/ModularArithmetic/ModularBaseSystemWord.v
src/ModularArithmetic/Pow2Base.v
src/ModularArithmetic/Pow2BaseProofs.v
src/ModularArithmetic/Pre.v
src/ModularArithmetic/PrimeFieldTheorems.v
src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
src/ModularArithmetic/PseudoMersenneBaseParams.v
src/ModularArithmetic/Tutorial.v
src/ModularArithmetic/ZBounded.v
src/ModularArithmetic/ZBoundedZ.v
src/ModularArithmetic/BarrettReduction/Z.v
src/ModularArithmetic/BarrettReduction/ZBounded.v
src/ModularArithmetic/BarrettReduction/ZGeneralized.v
src/ModularArithmetic/BarrettReduction/ZHandbook.v
src/ModularArithmetic/Montgomery/Z.v
src/ModularArithmetic/Montgomery/ZBounded.v
src/ModularArithmetic/Montgomery/ZProofs.v
src/Reflection/Application.v
src/Reflection/ApplicationLemmas.v
src/Reflection/ApplicationRelations.v
src/Reflection/CommonSubexpressionElimination.v
src/Reflection/Conversion.v
src/Reflection/CountLets.v
src/Reflection/Equality.v
src/Reflection/ExprInversion.v
src/Reflection/FilterLive.v
src/Reflection/Inline.v
src/Reflection/InlineInterp.v
src/Reflection/InlineWf.v
src/Reflection/InputSyntax.v
src/Reflection/InterpProofs.v
src/Reflection/InterpWf.v
src/Reflection/InterpWfRel.v
src/Reflection/Linearize.v
src/Reflection/LinearizeInterp.v
src/Reflection/LinearizeWf.v
src/Reflection/MapCast.v
src/Reflection/MapCastWithCastOp.v
src/Reflection/MultiSizeTest.v
src/Reflection/MultiSizeTest2.v
src/Reflection/Reify.v
src/Reflection/Relations.v
src/Reflection/Syntax.v
src/Reflection/TestCase.v
src/Reflection/Tuple.v
src/Reflection/WfInversion.v
src/Reflection/WfProofs.v
src/Reflection/WfReflective.v
src/Reflection/WfReflectiveGen.v
src/Reflection/Named/Compile.v
src/Reflection/Named/ContextOn.v
src/Reflection/Named/DeadCodeElimination.v
src/Reflection/Named/EstablishLiveness.v
src/Reflection/Named/NameUtil.v
src/Reflection/Named/RegisterAssign.v
src/Reflection/Named/Syntax.v
src/Reflection/Z/Interpretations128.v
src/Reflection/Z/Interpretations64.v
src/Reflection/Z/InterpretationsGen.v
src/Reflection/Z/Reify.v
src/Reflection/Z/Syntax.v
src/Reflection/Z/Interpretations128/Relations.v
src/Reflection/Z/Interpretations128/RelationsCombinations.v
src/Reflection/Z/Interpretations64/Relations.v
src/Reflection/Z/Interpretations64/RelationsCombinations.v
src/Spec/CompleteEdwardsCurve.v
src/Spec/Ed25519.v
src/Spec/EdDSA.v
src/Spec/Encoding.v
src/Spec/ModularArithmetic.v
src/Spec/ModularWordEncoding.v
src/Spec/MxDH.v
src/Spec/WeierstrassCurve.v
src/Specific/GF1305.v
src/Specific/GF25519.v
src/Specific/GF25519Bounded.v
src/Specific/GF25519BoundedAddCoordinates.v
src/Specific/GF25519BoundedCommon.v
src/Specific/GF25519BoundedExtendedAddCoordinates.v
src/Specific/GF25519ExtendedAddCoordinates.v
src/Specific/GF25519Reflective.v
src/Specific/GF25519ReflectiveAddCoordinates.v
src/Specific/SC25519.v
src/Specific/FancyMachine256/Barrett.v
src/Specific/FancyMachine256/Core.v
src/Specific/FancyMachine256/Montgomery.v
src/Specific/GF25519Reflective/Common.v
src/Specific/GF25519Reflective/Common9_4Op.v
src/Specific/GF25519Reflective/CommonBinOp.v
src/Specific/GF25519Reflective/CommonUnOp.v
src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
src/Specific/GF25519Reflective/Reified.v
src/Specific/GF25519Reflective/Reified/Add.v
src/Specific/GF25519Reflective/Reified/AddCoordinates.v
src/Specific/GF25519Reflective/Reified/CarryAdd.v
src/Specific/GF25519Reflective/Reified/CarryOpp.v
src/Specific/GF25519Reflective/Reified/CarrySub.v
src/Specific/GF25519Reflective/Reified/GeModulus.v
src/Specific/GF25519Reflective/Reified/LadderStep.v
src/Specific/GF25519Reflective/Reified/Mul.v
src/Specific/GF25519Reflective/Reified/Opp.v
src/Specific/GF25519Reflective/Reified/Pack.v
src/Specific/GF25519Reflective/Reified/PreFreeze.v
src/Specific/GF25519Reflective/Reified/Sub.v
src/Specific/GF25519Reflective/Reified/Unpack.v
src/SpecificGen/GF2213_32.v
src/SpecificGen/GF2213_32Bounded.v
src/SpecificGen/GF2213_32BoundedAddCoordinates.v
src/SpecificGen/GF2213_32BoundedCommon.v
src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v
src/SpecificGen/GF2213_32ExtendedAddCoordinates.v
src/SpecificGen/GF2213_32Reflective.v
src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v
src/SpecificGen/GF2519_32.v
src/SpecificGen/GF2519_32Bounded.v
src/SpecificGen/GF2519_32BoundedAddCoordinates.v
src/SpecificGen/GF2519_32BoundedCommon.v
src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v
src/SpecificGen/GF2519_32ExtendedAddCoordinates.v
src/SpecificGen/GF2519_32Reflective.v
src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v
src/SpecificGen/GF25519_32.v
src/SpecificGen/GF25519_32Bounded.v
src/SpecificGen/GF25519_32BoundedAddCoordinates.v
src/SpecificGen/GF25519_32BoundedCommon.v
src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v
src/SpecificGen/GF25519_32ExtendedAddCoordinates.v
src/SpecificGen/GF25519_32Reflective.v
src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v
src/SpecificGen/GF25519_64.v
src/SpecificGen/GF25519_64Bounded.v
src/SpecificGen/GF25519_64BoundedAddCoordinates.v
src/SpecificGen/GF25519_64BoundedCommon.v
src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v
src/SpecificGen/GF25519_64ExtendedAddCoordinates.v
src/SpecificGen/GF25519_64Reflective.v
src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v
src/SpecificGen/GF41417_32.v
src/SpecificGen/GF41417_32Bounded.v
src/SpecificGen/GF41417_32BoundedAddCoordinates.v
src/SpecificGen/GF41417_32BoundedCommon.v
src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v
src/SpecificGen/GF41417_32ExtendedAddCoordinates.v
src/SpecificGen/GF41417_32Reflective.v
src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v
src/SpecificGen/GF5211_32.v
src/SpecificGen/GF5211_32Bounded.v
src/SpecificGen/GF5211_32BoundedAddCoordinates.v
src/SpecificGen/GF5211_32BoundedCommon.v
src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v
src/SpecificGen/GF5211_32ExtendedAddCoordinates.v
src/SpecificGen/GF5211_32Reflective.v
src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v
src/SpecificGen/GF2213_32Reflective/Common.v
src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v
src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v
src/SpecificGen/GF2213_32Reflective/Reified.v
src/SpecificGen/GF2213_32Reflective/Reified/Add.v
src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
src/SpecificGen/GF2213_32Reflective/Reified/CarryAdd.v
src/SpecificGen/GF2213_32Reflective/Reified/CarryOpp.v
src/SpecificGen/GF2213_32Reflective/Reified/CarrySub.v
src/SpecificGen/GF2213_32Reflective/Reified/GeModulus.v
src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v
src/SpecificGen/GF2213_32Reflective/Reified/Mul.v
src/SpecificGen/GF2213_32Reflective/Reified/Opp.v
src/SpecificGen/GF2213_32Reflective/Reified/Pack.v
src/SpecificGen/GF2213_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF2213_32Reflective/Reified/Sub.v
src/SpecificGen/GF2213_32Reflective/Reified/Unpack.v
src/SpecificGen/GF2519_32Reflective/Common.v
src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v
src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v
src/SpecificGen/GF2519_32Reflective/Reified.v
src/SpecificGen/GF2519_32Reflective/Reified/Add.v
src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v
src/SpecificGen/GF2519_32Reflective/Reified/CarryAdd.v
src/SpecificGen/GF2519_32Reflective/Reified/CarryOpp.v
src/SpecificGen/GF2519_32Reflective/Reified/CarrySub.v
src/SpecificGen/GF2519_32Reflective/Reified/GeModulus.v
src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v
src/SpecificGen/GF2519_32Reflective/Reified/Mul.v
src/SpecificGen/GF2519_32Reflective/Reified/Opp.v
src/SpecificGen/GF2519_32Reflective/Reified/Pack.v
src/SpecificGen/GF2519_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF2519_32Reflective/Reified/Sub.v
src/SpecificGen/GF2519_32Reflective/Reified/Unpack.v
src/SpecificGen/GF25519_32Reflective/Common.v
src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v
src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v
src/SpecificGen/GF25519_32Reflective/Reified.v
src/SpecificGen/GF25519_32Reflective/Reified/Add.v
src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
src/SpecificGen/GF25519_32Reflective/Reified/CarryAdd.v
src/SpecificGen/GF25519_32Reflective/Reified/CarryOpp.v
src/SpecificGen/GF25519_32Reflective/Reified/CarrySub.v
src/SpecificGen/GF25519_32Reflective/Reified/GeModulus.v
src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v
src/SpecificGen/GF25519_32Reflective/Reified/Mul.v
src/SpecificGen/GF25519_32Reflective/Reified/Opp.v
src/SpecificGen/GF25519_32Reflective/Reified/Pack.v
src/SpecificGen/GF25519_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF25519_32Reflective/Reified/Sub.v
src/SpecificGen/GF25519_32Reflective/Reified/Unpack.v
src/SpecificGen/GF25519_64Reflective/Common.v
src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v
src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v
src/SpecificGen/GF25519_64Reflective/Reified.v
src/SpecificGen/GF25519_64Reflective/Reified/Add.v
src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v
src/SpecificGen/GF25519_64Reflective/Reified/CarryAdd.v
src/SpecificGen/GF25519_64Reflective/Reified/CarryOpp.v
src/SpecificGen/GF25519_64Reflective/Reified/CarrySub.v
src/SpecificGen/GF25519_64Reflective/Reified/GeModulus.v
src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v
src/SpecificGen/GF25519_64Reflective/Reified/Mul.v
src/SpecificGen/GF25519_64Reflective/Reified/Opp.v
src/SpecificGen/GF25519_64Reflective/Reified/Pack.v
src/SpecificGen/GF25519_64Reflective/Reified/PreFreeze.v
src/SpecificGen/GF25519_64Reflective/Reified/Sub.v
src/SpecificGen/GF25519_64Reflective/Reified/Unpack.v
src/SpecificGen/GF41417_32Reflective/Common.v
src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v
src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v
src/SpecificGen/GF41417_32Reflective/Reified.v
src/SpecificGen/GF41417_32Reflective/Reified/Add.v
src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v
src/SpecificGen/GF41417_32Reflective/Reified/CarryAdd.v
src/SpecificGen/GF41417_32Reflective/Reified/CarryOpp.v
src/SpecificGen/GF41417_32Reflective/Reified/CarrySub.v
src/SpecificGen/GF41417_32Reflective/Reified/GeModulus.v
src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v
src/SpecificGen/GF41417_32Reflective/Reified/Mul.v
src/SpecificGen/GF41417_32Reflective/Reified/Opp.v
src/SpecificGen/GF41417_32Reflective/Reified/Pack.v
src/SpecificGen/GF41417_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF41417_32Reflective/Reified/Sub.v
src/SpecificGen/GF41417_32Reflective/Reified/Unpack.v
src/SpecificGen/GF5211_32Reflective/Common.v
src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v
src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v
src/SpecificGen/GF5211_32Reflective/Reified.v
src/SpecificGen/GF5211_32Reflective/Reified/Add.v
src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v
src/SpecificGen/GF5211_32Reflective/Reified/CarryAdd.v
src/SpecificGen/GF5211_32Reflective/Reified/CarryOpp.v
src/SpecificGen/GF5211_32Reflective/Reified/CarrySub.v
src/SpecificGen/GF5211_32Reflective/Reified/GeModulus.v
src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v
src/SpecificGen/GF5211_32Reflective/Reified/Mul.v
src/SpecificGen/GF5211_32Reflective/Reified/Opp.v
src/SpecificGen/GF5211_32Reflective/Reified/Pack.v
src/SpecificGen/GF5211_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF5211_32Reflective/Reified/Sub.v
src/SpecificGen/GF5211_32Reflective/Reified/Unpack.v
src/Tactics/VerdiTactics.v
src/Tactics/Algebra_syntax/Nsatz.v
src/Test/Curve25519SpecTestVectors.v
src/Util/AdditionChainExponentiation.v
src/Util/AutoRewrite.v
src/Util/Bool.v
src/Util/CaseUtil.v
src/Util/Curry.v
src/Util/Decidable.v
src/Util/Equality.v
src/Util/FixCoqMistakes.v
src/Util/FixedWordSizes.v
src/Util/FixedWordSizesEquality.v
src/Util/GlobalSettings.v
src/Util/HList.v
src/Util/HProp.v
src/Util/IffT.v
src/Util/Isomorphism.v
src/Util/IterAssocOp.v
src/Util/LetIn.v
src/Util/LetInMonad.v
src/Util/ListUtil.v
src/Util/Logic.v
src/Util/NatUtil.v
src/Util/Notations.v
src/Util/NumTheoryUtil.v
src/Util/Option.v
src/Util/PartiallyReifiedProp.v
src/Util/PointedProp.v
src/Util/Prod.v
src/Util/Relations.v
src/Util/Sigma.v
src/Util/Sum.v
src/Util/Tactics.v
src/Util/Tower.v
src/Util/Tuple.v
src/Util/Unit.v
src/Util/WordUtil.v
src/Util/ZUtil.v
src/Util/Tactics/BreakMatch.v
src/Util/Tactics/DestructHead.v
src/Util/Tactics/DestructHyps.v
src/Util/Tactics/Head.v
src/Util/Tactics/SpecializeBy.v
src/Util/Tactics/SplitInContext.v
src/WeierstrassCurve/Pre.v