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/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/Ed25519.v
src/Experiments/Ed25519Extraction.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/Interpretations128.v
src/Reflection/Z/Interpretations64.v
src/Reflection/Z/InterpretationsGen.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/MapCastByDeBruijn.v
src/Reflection/Z/Bounds/Relax.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/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/GF25519Bounded.v
src/Specific/GF25519BoundedAddCoordinates.v
src/Specific/GF25519BoundedCommon.v
src/Specific/GF25519Reflective.v
src/Specific/GF25519ReflectiveAddCoordinates.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/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/AddDisplay.v
src/Specific/GF25519Reflective/Reified/AddJavaDisplay.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/LadderStepDisplay.v
src/Specific/GF25519Reflective/Reified/LadderStepJavaDisplay.v
src/Specific/GF25519Reflective/Reified/Mul.v
src/Specific/GF25519Reflective/Reified/MulDisplay.v
src/Specific/GF25519Reflective/Reified/MulJavaDisplay.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/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/Tactics/BreakMatch.v
src/Util/Tactics/DestructHead.v
src/Util/Tactics/DestructHyps.v
src/Util/Tactics/DoWithHyp.v
src/Util/Tactics/ETransitivity.v
src/Util/Tactics/Head.v
src/Util/Tactics/RewriteHyp.v
src/Util/Tactics/SpecializeBy.v
src/Util/Tactics/SplitInContext.v
src/Util/Tactics/SubstLet.v
src/Util/Tactics/UniquePose.v
src/Util/Tactics/VM.v
src/WeierstrassCurve/Pre.v
src/WeierstrassCurve/Projective.v
src/WeierstrassCurve/WeierstrassCurveTheorems.v