-R src Crypto
-arg -w -arg +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive
-arg -native-compiler -arg ondemand
src/BoundsPipeline.v
src/CLI.v
src/COperationSpecifications.v
src/CastLemmas.v
src/CompilersTestCases.v
src/Demo.v
src/MiscCompilerPasses.v
src/MiscCompilerPassesProofs.v
src/MiscCompilerPassesProofsExtra.v
src/SlowPrimeSynthesisExamples.v
src/StandaloneDebuggingExamples.v
src/StandaloneHaskellMain.v
src/StandaloneOCamlMain.v
src/TAPSort.v
src/UnsaturatedSolinasHeuristics.v
src/AbstractInterpretation/AbstractInterpretation.v
src/AbstractInterpretation/Proofs.v
src/AbstractInterpretation/Wf.v
src/AbstractInterpretation/WfExtra.v
src/AbstractInterpretation/ZRange.v
src/AbstractInterpretation/ZRangeProofs.v
src/Algebra/Field.v
src/Algebra/Field_test.v
src/Algebra/Group.v
src/Algebra/Hierarchy.v
src/Algebra/IntegralDomain.v
src/Algebra/Monoid.v
src/Algebra/Nsatz.v
src/Algebra/NsatzTactic.v
src/Algebra/Ring.v
src/Algebra/ScalarMult.v
src/Algebra/SubsetoidRing.v
src/Arithmetic/BYInv.v
src/Arithmetic/BarrettReduction.v
src/Arithmetic/BaseConversion.v
src/Arithmetic/Core.v
src/Arithmetic/FLia.v
src/Arithmetic/FancyMontgomeryReduction.v
src/Arithmetic/Freeze.v
src/Arithmetic/ModOps.v
src/Arithmetic/ModularArithmeticPre.v
src/Arithmetic/ModularArithmeticTheorems.v
src/Arithmetic/Partition.v
src/Arithmetic/PrimeFieldTheorems.v
src/Arithmetic/Primitives.v
src/Arithmetic/Saturated.v
src/Arithmetic/UniformWeight.v
src/Arithmetic/WordByWordMontgomery.v
src/Arithmetic/BarrettReduction/Generalized.v
src/Arithmetic/BarrettReduction/HAC.v
src/Arithmetic/BarrettReduction/RidiculousFish.v
src/Arithmetic/BarrettReduction/Wikipedia.v
src/Arithmetic/MontgomeryReduction/Definition.v
src/Arithmetic/MontgomeryReduction/Proofs.v
src/ArithmeticCPS/BaseConversion.v
src/ArithmeticCPS/Core.v
src/ArithmeticCPS/Freeze.v
src/ArithmeticCPS/ModOps.v
src/ArithmeticCPS/Saturated.v
src/ArithmeticCPS/WordByWordMontgomery.v
src/Assembly/Equality.v
src/Assembly/Equivalence.v
src/Assembly/EquivalenceProofs.v
src/Assembly/Parse.v
src/Assembly/Symbolic.v
src/Assembly/Syntax.v
src/Assembly/Parse/TestAsm.v
src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised.v
src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.v
src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.v
src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v
src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v
src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.v
src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.v
src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.v
src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.v
src/Assembly/WithBedrock/Proofs.v
src/Assembly/WithBedrock/Semantics.v
src/Assembly/WithBedrock/SymbolicProofs.v
src/Bedrock/End2End/Poly1305/Field1305.v
src/Bedrock/End2End/X25519/Field25519.v
src/Bedrock/End2End/X25519/MontgomeryLadder.v
src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
src/Bedrock/Field/Common/Tactics.v
src/Bedrock/Field/Common/Types.v
src/Bedrock/Field/Common/Util.v
src/Bedrock/Field/Common/Arrays/ByteBounds.v
src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v
src/Bedrock/Field/Common/Arrays/MakeListLengths.v
src/Bedrock/Field/Common/Arrays/MaxBounds.v
src/Bedrock/Field/Common/Names/MakeNames.v
src/Bedrock/Field/Common/Names/VarnameGenerator.v
src/Bedrock/Field/Interface/Compilation2.v
src/Bedrock/Field/Interface/Representation.v
src/Bedrock/Field/Stringification/FlattenVarData.v
src/Bedrock/Field/Stringification/LoadStoreListVarData.v
src/Bedrock/Field/Stringification/Stringification.v
src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v
src/Bedrock/Field/Synthesis/Examples/LadderStep.v
src/Bedrock/Field/Synthesis/Examples/MulTwice.v
src/Bedrock/Field/Synthesis/Examples/X1305_32.v
src/Bedrock/Field/Synthesis/Examples/X25519_64.v
src/Bedrock/Field/Synthesis/Examples/p224_64.v
src/Bedrock/Field/Synthesis/Examples/p256_64.v
src/Bedrock/Field/Synthesis/Generic/Bignum.v
src/Bedrock/Field/Synthesis/Generic/Operation.v
src/Bedrock/Field/Synthesis/Generic/Tactics.v
src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v
src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v
src/Bedrock/Field/Synthesis/New/ComputedOp.v
src/Bedrock/Field/Synthesis/New/Signature.v
src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v
src/Bedrock/Field/Synthesis/Specialized/ReifiedOperation.v
src/Bedrock/Field/Synthesis/Specialized/Tactics.v
src/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.v
src/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.v
src/Bedrock/Field/Translation/Cmd.v
src/Bedrock/Field/Translation/Expr.v
src/Bedrock/Field/Translation/Flatten.v
src/Bedrock/Field/Translation/Func.v
src/Bedrock/Field/Translation/LoadStoreList.v
src/Bedrock/Field/Translation/Parameters/Defaults.v
src/Bedrock/Field/Translation/Parameters/Defaults32.v
src/Bedrock/Field/Translation/Parameters/Defaults64.v
src/Bedrock/Field/Translation/Proofs/Cmd.v
src/Bedrock/Field/Translation/Proofs/Equivalence.v
src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v
src/Bedrock/Field/Translation/Proofs/Expr.v
src/Bedrock/Field/Translation/Proofs/Flatten.v
src/Bedrock/Field/Translation/Proofs/Func.v
src/Bedrock/Field/Translation/Proofs/LoadStoreList.v
src/Bedrock/Field/Translation/Proofs/UsedVarnames.v
src/Bedrock/Field/Translation/Proofs/VarnameSet.v
src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v
src/Bedrock/Group/AdditionChains.v
src/Bedrock/Group/Loops.v
src/Bedrock/Group/Point.v
src/Bedrock/Group/ScalarMult/CSwap.v
src/Bedrock/Group/ScalarMult/LadderStep.v
src/Bedrock/Group/ScalarMult/MontgomeryEquivalence.v
src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
src/Bedrock/Group/ScalarMult/ScalarMult.v
src/Bedrock/Specs/Field.v
src/Bedrock/Specs/Group.v
src/Bedrock/Standalone/StandaloneHaskellMain.v
src/Bedrock/Standalone/StandaloneOCamlMain.v
src/Curves/EdwardsMontgomery.v
src/Curves/Edwards/AffineProofs.v
src/Curves/Edwards/Pre.v
src/Curves/Edwards/XYZT/Basic.v
src/Curves/Edwards/XYZT/Precomputed.v
src/Curves/Montgomery/Affine.v
src/Curves/Montgomery/AffineInstances.v
src/Curves/Montgomery/AffineProofs.v
src/Curves/Montgomery/XZ.v
src/Curves/Montgomery/XZProofs.v
src/Curves/Weierstrass/Affine.v
src/Curves/Weierstrass/AffineProofs.v
src/Curves/Weierstrass/Jacobian.v
src/Curves/Weierstrass/Projective.v
src/Fancy/Barrett256.v
src/Fancy/Compiler.v
src/Fancy/Montgomery256.v
src/Fancy/Prod.v
src/Fancy/Spec.v
src/Language/API.v
src/Language/APINotations.v
src/Language/IdentifierParameters.v
src/Language/IdentifiersBasicGENERATED.v
src/Language/IdentifiersGENERATED.v
src/Language/IdentifiersGENERATEDProofs.v
src/Language/InversionExtra.v
src/Language/PreExtra.v
src/Language/UnderLetsProofsExtra.v
src/Language/WfExtra.v
src/Primitives/MxDHRepChange.v
src/PushButtonSynthesis/BYInversionReificationCache.v
src/PushButtonSynthesis/BarrettReduction.v
src/PushButtonSynthesis/BarrettReductionReificationCache.v
src/PushButtonSynthesis/BaseConversion.v
src/PushButtonSynthesis/BaseConversionReificationCache.v
src/PushButtonSynthesis/FancyMontgomeryReduction.v
src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
src/PushButtonSynthesis/InvertHighLow.v
src/PushButtonSynthesis/Primitives.v
src/PushButtonSynthesis/ReificationCache.v
src/PushButtonSynthesis/SaturatedSolinas.v
src/PushButtonSynthesis/SaturatedSolinasReificationCache.v
src/PushButtonSynthesis/SmallExamples.v
src/PushButtonSynthesis/UnsaturatedSolinas.v
src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
src/PushButtonSynthesis/WordByWordMontgomery.v
src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v
src/Rewriter/All.v
src/Rewriter/AllTacticsExtra.v
src/Rewriter/Rules.v
src/Rewriter/RulesProofs.v
src/Rewriter/TestRules.v
src/Rewriter/TestRulesProofs.v
src/Rewriter/Passes/AddAssocLeft.v
src/Rewriter/Passes/Arith.v
src/Rewriter/Passes/ArithWithCasts.v
src/Rewriter/Passes/FlattenThunkedRects.v
src/Rewriter/Passes/MulSplit.v
src/Rewriter/Passes/MultiRetSplit.v
src/Rewriter/Passes/NBE.v
src/Rewriter/Passes/NoSelect.v
src/Rewriter/Passes/RelaxBitwidthAdcSbb.v
src/Rewriter/Passes/StripLiteralCasts.v
src/Rewriter/Passes/Test.v
src/Rewriter/Passes/ToFancy.v
src/Rewriter/Passes/ToFancyWithCasts.v
src/Rewriter/Passes/UnfoldValueBarrier.v
src/Rewriter/PerfTesting/Core.v
src/Rewriter/PerfTesting/StandaloneOCamlMain.v
src/Spec/CompleteEdwardsCurve.v
src/Spec/Curve25519.v
src/Spec/ModularArithmetic.v
src/Spec/MontgomeryCurve.v
src/Spec/MxDH.v
src/Spec/WeierstrassCurve.v
src/Spec/Test/X25519.v
src/Stringification/C.v
src/Stringification/Go.v
src/Stringification/IR.v
src/Stringification/JSON.v
src/Stringification/Java.v
src/Stringification/Language.v
src/Stringification/Rust.v
src/Stringification/Zig.v
src/UnsaturatedSolinasHeuristics/Tests.v
src/Util/AdditionChainExponentiation.v
src/Util/Arg.v
src/Util/AutoRewrite.v
src/Util/Bool.v
src/Util/CPSNotations.v
src/Util/CPSUtil.v
src/Util/Comparison.v
src/Util/Compose.v
src/Util/Curry.v
src/Util/Decidable.v
src/Util/DefaultedTypes.v
src/Util/DynList.v
src/Util/Equality.v
src/Util/ErrorT.v
src/Util/Factorize.v
src/Util/FixCoqMistakes.v
src/Util/FsatzAutoLemmas.v
src/Util/FueledLUB.v
src/Util/GlobalSettings.v
src/Util/HList.v
src/Util/HProp.v
src/Util/IdfunWithAlt.v
src/Util/IffT.v
src/Util/Isomorphism.v
src/Util/LetIn.v
src/Util/LetInMonad.v
src/Util/Level.v
src/Util/ListUtil.v
src/Util/Listable.v
src/Util/Logic.v
src/Util/Loops.v
src/Util/MSetN.v
src/Util/NatUtil.v
src/Util/Notations.v
src/Util/NumTheoryUtil.v
src/Util/Option.v
src/Util/OptionList.v
src/Util/PER.v
src/Util/ParseTaps.v
src/Util/PartiallyReifiedProp.v
src/Util/Pointed.v
src/Util/PointedProp.v
src/Util/Pos.v
src/Util/PrimitiveHList.v
src/Util/PrimitiveProd.v
src/Util/PrimitiveSigma.v
src/Util/Prod.v
src/Util/QUtil.v
src/Util/Relations.v
src/Util/Sigma.v
src/Util/Sum.v
src/Util/Sumbool.v
src/Util/Tactics.v
src/Util/TagList.v
src/Util/Tower.v
src/Util/Tuple.v
src/Util/Unit.v
src/Util/Wf.v
src/Util/Wf1.v
src/Util/Wf2.v
src/Util/ZBounded.v
src/Util/ZRange.v
src/Util/ZUtil.v
src/Util/Bool/Equality.v
src/Util/Bool/IsTrue.v
src/Util/Bool/LeCompat.v
src/Util/Bool/Reflect.v
src/Util/Decidable/Bool2Prop.v
src/Util/Decidable/Decidable2Bool.v
src/Util/ErrorT/Show.v
src/Util/FMapPositive/Equality.v
src/Util/ListUtil/CombineExtend.v
src/Util/ListUtil/Concat.v
src/Util/ListUtil/Filter.v
src/Util/ListUtil/FoldBool.v
src/Util/ListUtil/FoldMap.v
src/Util/ListUtil/Forall.v
src/Util/ListUtil/ForallIn.v
src/Util/ListUtil/GroupAllBy.v
src/Util/ListUtil/IndexOf.v
src/Util/ListUtil/NthExt.v
src/Util/ListUtil/Partition.v
src/Util/ListUtil/Permutation.v
src/Util/ListUtil/PermutationCompat.v
src/Util/ListUtil/RemoveN.v
src/Util/ListUtil/SetoidList.v
src/Util/ListUtil/Split.v
src/Util/ListUtil/StdlibCompat.v
src/Util/Logic/Exists.v
src/Util/Logic/ExistsEqAnd.v
src/Util/Logic/Forall.v
src/Util/Logic/ImplAnd.v
src/Util/Logic/ProdForall.v
src/Util/MSetPositive/Equality.v
src/Util/MSetPositive/Facts.v
src/Util/MSetPositive/Show.v
src/Util/MSets/Iso.v
src/Util/MSets/Show.v
src/Util/MSets/Sum.v
src/Util/NUtil/Sorting.v
src/Util/NUtil/Testbit.v
src/Util/NUtil/WithoutReferenceToZ.v
src/Util/SideConditions/Autosolve.v
src/Util/SideConditions/CorePackages.v
src/Util/SideConditions/ModInvPackage.v
src/Util/SideConditions/ReductionPackages.v
src/Util/SideConditions/RingPackage.v
src/Util/Sigma/Associativity.v
src/Util/Sigma/Lift.v
src/Util/Sigma/MapProjections.v
src/Util/Sigma/Related.v
src/Util/Strings/Ascii.v
src/Util/Strings/Decimal.v
src/Util/Strings/NamingConventions.v
src/Util/Strings/ParseArithmetic.v
src/Util/Strings/ParseArithmeticToTaps.v
src/Util/Strings/Show.v
src/Util/Strings/Sorting.v
src/Util/Strings/String.v
src/Util/Strings/StringMap.v
src/Util/Strings/String_as_OT.v
src/Util/Strings/String_as_OT_old.v
src/Util/Strings/Parse/Common.v
src/Util/Structures/Orders.v
src/Util/Structures/Equalities/Iso.v
src/Util/Structures/Equalities/Sum.v
src/Util/Structures/Orders/Iso.v
src/Util/Structures/Orders/Sum.v
src/Util/Tactics/AllInstances.v
src/Util/Tactics/AllSuccesses.v
src/Util/Tactics/AppendUnderscores.v
src/Util/Tactics/BreakMatch.v
src/Util/Tactics/CPSId.v
src/Util/Tactics/CacheTerm.v
src/Util/Tactics/ChangeInAll.v
src/Util/Tactics/ClearAll.v
src/Util/Tactics/ClearDuplicates.v
src/Util/Tactics/ClearHead.v
src/Util/Tactics/ClearbodyAll.v
src/Util/Tactics/ConstrFail.v
src/Util/Tactics/Contains.v
src/Util/Tactics/ConvoyDestruct.v
src/Util/Tactics/CountBinders.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/EvarNormalize.v
src/Util/Tactics/FindHyp.v
src/Util/Tactics/Forward.v
src/Util/Tactics/GetGoal.v
src/Util/Tactics/HasBody.v
src/Util/Tactics/Head.v
src/Util/Tactics/HeadUnderBinders.v
src/Util/Tactics/MoveLetIn.v
src/Util/Tactics/NormalizeCommutativeIdentifier.v
src/Util/Tactics/Not.v
src/Util/Tactics/OnSubterms.v
src/Util/Tactics/PoseTermWithName.v
src/Util/Tactics/PrintContext.v
src/Util/Tactics/PrintGoal.v
src/Util/Tactics/Revert.v
src/Util/Tactics/RevertUntil.v
src/Util/Tactics/RewriteHyp.v
src/Util/Tactics/RunTacticAsConstr.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/SpecializeAllWays.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/TransparentAssert.v
src/Util/Tactics/UnfoldArg.v
src/Util/Tactics/UnifyAbstractReflexivity.v
src/Util/Tactics/UniquePose.v
src/Util/Tactics/VM.v
src/Util/Tactics/WarnIfGoalsRemain.v
src/Util/Telescope/Core.v
src/Util/Telescope/Equality.v
src/Util/Telescope/Instances.v
src/Util/ZRange/BasicLemmas.v
src/Util/ZRange/CornersMonotoneBounds.v
src/Util/ZRange/LandLorBounds.v
src/Util/ZRange/Operations.v
src/Util/ZRange/OperationsBounds.v
src/Util/ZRange/Show.v
src/Util/ZRange/SplitBounds.v
src/Util/ZRange/SplitRangeBounds.v
src/Util/ZUtil/AddGetCarry.v
src/Util/ZUtil/AddModulo.v
src/Util/ZUtil/ArithmeticShiftr.v
src/Util/ZUtil/Bitwise.v
src/Util/ZUtil/CC.v
src/Util/ZUtil/CPS.v
src/Util/ZUtil/Combine.v
src/Util/ZUtil/Definitions.v
src/Util/ZUtil/DistrIf.v
src/Util/ZUtil/Div.v
src/Util/ZUtil/Divide.v
src/Util/ZUtil/EquivModulo.v
src/Util/ZUtil/Ge.v
src/Util/ZUtil/Hints.v
src/Util/ZUtil/Land.v
src/Util/ZUtil/LandLorBounds.v
src/Util/ZUtil/LandLorShiftBounds.v
src/Util/ZUtil/Le.v
src/Util/ZUtil/Lnot.v
src/Util/ZUtil/LnotModulo.v
src/Util/ZUtil/Log2.v
src/Util/ZUtil/Lor.v
src/Util/ZUtil/Ltz.v
src/Util/ZUtil/Lxor.v
src/Util/ZUtil/ModExp.v
src/Util/ZUtil/ModInv.v
src/Util/ZUtil/Modulo.v
src/Util/ZUtil/Morphisms.v
src/Util/ZUtil/Mul.v
src/Util/ZUtil/MulSplit.v
src/Util/ZUtil/N2Z.v
src/Util/ZUtil/Nat2Z.v
src/Util/ZUtil/Notations.v
src/Util/ZUtil/Odd.v
src/Util/ZUtil/Ones.v
src/Util/ZUtil/OnesFrom.v
src/Util/ZUtil/Opp.v
src/Util/ZUtil/Peano.v
src/Util/ZUtil/Pow.v
src/Util/ZUtil/Pow2.v
src/Util/ZUtil/Pow2Mod.v
src/Util/ZUtil/Quot.v
src/Util/ZUtil/Rshi.v
src/Util/ZUtil/Sgn.v
src/Util/ZUtil/Shift.v
src/Util/ZUtil/SignBit.v
src/Util/ZUtil/Sorting.v
src/Util/ZUtil/Stabilization.v
src/Util/ZUtil/Tactics.v
src/Util/ZUtil/Testbit.v
src/Util/ZUtil/TruncatingShiftl.v
src/Util/ZUtil/TwosComplement.v
src/Util/ZUtil/Z2Nat.v
src/Util/ZUtil/ZSimplify.v
src/Util/ZUtil/Zselect.v
src/Util/ZUtil/Div/Bootstrap.v
src/Util/ZUtil/Hints/Core.v
src/Util/ZUtil/Hints/PullPush.v
src/Util/ZUtil/Hints/ZArith.v
src/Util/ZUtil/Hints/Ztestbit.v
src/Util/ZUtil/Modulo/Bootstrap.v
src/Util/ZUtil/Modulo/PullPush.v
src/Util/ZUtil/Tactics/CompareToSgn.v
src/Util/ZUtil/Tactics/DivModToQuotRem.v
src/Util/ZUtil/Tactics/DivideExistsMul.v
src/Util/ZUtil/Tactics/LinearSubstitute.v
src/Util/ZUtil/Tactics/LtbToLt.v
src/Util/ZUtil/Tactics/PeelLe.v
src/Util/ZUtil/Tactics/PrimeBound.v
src/Util/ZUtil/Tactics/PullPush.v
src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
src/Util/ZUtil/Tactics/RewriteModSmall.v
src/Util/ZUtil/Tactics/SimplifyFractionsLe.v
src/Util/ZUtil/Tactics/SolveRange.v
src/Util/ZUtil/Tactics/SolveTestbit.v
src/Util/ZUtil/Tactics/SplitMinMax.v
src/Util/ZUtil/Tactics/ZeroBounds.v
src/Util/ZUtil/Tactics/Ztestbit.v
src/Util/ZUtil/Tactics/PullPush/Modulo.v
src/Util/ZUtil/ZSimplify/Autogenerated.v
src/Util/ZUtil/ZSimplify/Core.v
src/Util/ZUtil/ZSimplify/Simple.v