-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/Karatsuba.v
src/MontgomeryCurveTheorems.v
src/MontgomeryX.v
src/MxDHRepChange.v
src/NewBaseSystem.v
src/SaturatedBaseSystem.v
src/Testbit.v
src/Algebra/Field.v
src/Algebra/Field_test.v
src/Algebra/Group.v
src/Algebra/IntegralDomain.v
src/Algebra/Monoid.v
src/Algebra/Ring.v
src/Algebra/ScalarMult.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/EdwardsMontgomery.v
src/CompleteEdwardsCurve/ExtendedCoordinates.v
src/CompleteEdwardsCurve/Pre.v
src/Encoding/EncodingTheorems.v
src/Encoding/ModularWordEncodingPre.v
src/Encoding/ModularWordEncodingTheorems.v
src/Experiments/ExtrHaskellNats.v
src/Experiments/GenericFieldPow.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/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/BoundByCast.v
src/Reflection/BoundByCastInterp.v
src/Reflection/BoundByCastWf.v
src/Reflection/CommonSubexpressionElimination.v
src/Reflection/Conversion.v
src/Reflection/CountLets.v
src/Reflection/Equality.v
src/Reflection/Eta.v
src/Reflection/EtaInterp.v
src/Reflection/EtaWf.v
src/Reflection/ExprInversion.v
src/Reflection/FilterLive.v
src/Reflection/FoldTypes.v
src/Reflection/Inline.v
src/Reflection/InlineCast.v
src/Reflection/InlineCastInterp.v
src/Reflection/InlineCastWf.v
src/Reflection/InlineInterp.v
src/Reflection/InlineWf.v
src/Reflection/InputSyntax.v
src/Reflection/InterpByIso.v
src/Reflection/InterpByIsoProofs.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/Map.v
src/Reflection/MapCast.v
src/Reflection/MapCastByDeBruijn.v
src/Reflection/MapCastByDeBruijnInterp.v
src/Reflection/MapCastByDeBruijnWf.v
src/Reflection/MapCastInterp.v
src/Reflection/MapCastWf.v
src/Reflection/MultiSizeTest.v
src/Reflection/MultiSizeTest2.v
src/Reflection/Reify.v
src/Reflection/Relations.v
src/Reflection/RenameBinders.v
src/Reflection/Rewriter.v
src/Reflection/RewriterInterp.v
src/Reflection/RewriterWf.v
src/Reflection/SmartBound.v
src/Reflection/SmartBoundInterp.v
src/Reflection/SmartBoundWf.v
src/Reflection/SmartCast.v
src/Reflection/SmartCastInterp.v
src/Reflection/SmartCastWf.v
src/Reflection/SmartMap.v
src/Reflection/Syntax.v
src/Reflection/TestCase.v
src/Reflection/Tuple.v
src/Reflection/TypeInversion.v
src/Reflection/TypeUtil.v
src/Reflection/Wf.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/CompileInterp.v
src/Reflection/Named/CompileProperties.v
src/Reflection/Named/CompileWf.v
src/Reflection/Named/ContextDefinitions.v
src/Reflection/Named/ContextOn.v
src/Reflection/Named/ContextProperties.v
src/Reflection/Named/DeadCodeElimination.v
src/Reflection/Named/EstablishLiveness.v
src/Reflection/Named/FMapContext.v
src/Reflection/Named/IdContext.v
src/Reflection/Named/InterpretToPHOAS.v
src/Reflection/Named/InterpretToPHOASInterp.v
src/Reflection/Named/InterpretToPHOASWf.v
src/Reflection/Named/MapCast.v
src/Reflection/Named/MapCastInterp.v
src/Reflection/Named/MapCastWf.v
src/Reflection/Named/NameUtil.v
src/Reflection/Named/NameUtilProperties.v
src/Reflection/Named/PositiveContext.v
src/Reflection/Named/RegisterAssign.v
src/Reflection/Named/SmartMap.v
src/Reflection/Named/Syntax.v
src/Reflection/Named/Wf.v
src/Reflection/Named/WfInterp.v
src/Reflection/Named/ContextProperties/NameUtil.v
src/Reflection/Named/ContextProperties/SmartMap.v
src/Reflection/Named/ContextProperties/Tactics.v
src/Reflection/Named/PositiveContext/Defaults.v
src/Reflection/Named/PositiveContext/DefaultsProperties.v
src/Reflection/Z/ArithmeticSimplifier.v
src/Reflection/Z/ArithmeticSimplifierInterp.v
src/Reflection/Z/ArithmeticSimplifierWf.v
src/Reflection/Z/BinaryNotationConstants.v
src/Reflection/Z/CNotations.v
src/Reflection/Z/FoldTypes.v
src/Reflection/Z/HexNotationConstants.v
src/Reflection/Z/Inline.v
src/Reflection/Z/InlineInterp.v
src/Reflection/Z/InlineWf.v
src/Reflection/Z/JavaNotations.v
src/Reflection/Z/MapCastByDeBruijn.v
src/Reflection/Z/MapCastByDeBruijnInterp.v
src/Reflection/Z/MapCastByDeBruijnWf.v
src/Reflection/Z/OpInversion.v
src/Reflection/Z/Reify.v
src/Reflection/Z/Syntax.v
src/Reflection/Z/Bounds/Interpretation.v
src/Reflection/Z/Bounds/InterpretationLemmas.v
src/Reflection/Z/Bounds/MapCastByDeBruijn.v
src/Reflection/Z/Bounds/MapCastByDeBruijnInterp.v
src/Reflection/Z/Bounds/MapCastByDeBruijnWf.v
src/Reflection/Z/Bounds/Pipeline.v
src/Reflection/Z/Bounds/Relax.v
src/Reflection/Z/Bounds/Pipeline/Definition.v
src/Reflection/Z/Bounds/Pipeline/Glue.v
src/Reflection/Z/Bounds/Pipeline/OutputType.v
src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
src/Reflection/Z/Syntax/Equality.v
src/Reflection/Z/Syntax/Util.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/MontgomeryCurve.v
src/Spec/MxDH.v
src/Spec/WeierstrassCurve.v
src/Specific/GF1305.v
src/Specific/GF25519.v
src/Specific/IntegrationTest.v
src/Specific/NewBaseSystemTest.v
src/Specific/SC25519.v
src/Specific/FancyMachine256/Barrett.v
src/Specific/FancyMachine256/Core.v
src/Specific/FancyMachine256/Montgomery.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/BoundedWord.v
src/Util/CPSUtil.v
src/Util/CaseUtil.v
src/Util/Curry.v
src/Util/Decidable.v
src/Util/Equality.v
src/Util/Factorize.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/NUtil.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/Sumbool.v
src/Util/Tactics.v
src/Util/Tower.v
src/Util/Tuple.v
src/Util/Unit.v
src/Util/WordUtil.v
src/Util/ZRange.v
src/Util/ZUtil.v
src/Util/Sigma/Associativity.v
src/Util/Sigma/Lift.v
src/Util/Tactics/BreakMatch.v
src/Util/Tactics/ClearDuplicates.v
src/Util/Tactics/Contains.v
src/Util/Tactics/ConvoyDestruct.v
src/Util/Tactics/DebugPrint.v
src/Util/Tactics/DestructHead.v
src/Util/Tactics/DestructHyps.v
src/Util/Tactics/DestructTrivial.v
src/Util/Tactics/DoWithHyp.v
src/Util/Tactics/ESpecialize.v
src/Util/Tactics/ETransitivity.v
src/Util/Tactics/EvarExists.v
src/Util/Tactics/Forward.v
src/Util/Tactics/GetGoal.v
src/Util/Tactics/Head.v
src/Util/Tactics/Not.v
src/Util/Tactics/OnSubterms.v
src/Util/Tactics/Revert.v
src/Util/Tactics/RewriteHyp.v
src/Util/Tactics/SetEvars.v
src/Util/Tactics/SetoidSubst.v
src/Util/Tactics/SideConditionsBeforeToAfter.v
src/Util/Tactics/SimplifyProjections.v
src/Util/Tactics/SimplifyRepeatedIfs.v
src/Util/Tactics/SpecializeBy.v
src/Util/Tactics/SplitInContext.v
src/Util/Tactics/SubstEvars.v
src/Util/Tactics/SubstLet.v
src/Util/Tactics/Test.v
src/Util/Tactics/UnifyAbstractReflexivity.v
src/Util/Tactics/UniquePose.v
src/Util/Tactics/VM.v
src/WeierstrassCurve/Pre.v
src/WeierstrassCurve/Projective.v
src/WeierstrassCurve/WeierstrassCurveTheorems.v