aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
blob: 2ca7a4b8925fd1b3b9a762a93bdf866293f865f4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
-R src Crypto
-R bbv/theories bbv
bbv/theories/BinNotation.v
bbv/theories/BinNotationZ.v
bbv/theories/DepEq.v
bbv/theories/DepEqNat.v
bbv/theories/HexNotation.v
bbv/theories/HexNotationWord.v
bbv/theories/HexNotationZ.v
bbv/theories/NLib.v
bbv/theories/N_Z_nat_conversions.v
bbv/theories/NatLib.v
bbv/theories/Nomega.v
bbv/theories/ReservedNotations.v
bbv/theories/Word.v
bbv/theories/WordScope.v
bbv/theories/ZHints.v
bbv/theories/ZLib.v
src/AbstractInterpretation.v
src/AbstractInterpretationProofs.v
src/AbstractInterpretationWf.v
src/AbstractInterpretationZRangeProofs.v
src/BoundsPipeline.v
src/CLI.v
src/COperationSpecifications.v
src/CStringification.v
src/CompilersTestCases.v
src/Demo.v
src/GENERATEDIdentifiersWithoutTypes.v
src/GENERATEDIdentifiersWithoutTypesProofs.v
src/Language.v
src/LanguageInversion.v
src/LanguageWf.v
src/MiscCompilerPasses.v
src/MiscCompilerPassesProofs.v
src/PreLanguage.v
src/Rewriter.v
src/RewriterInterpProofs1.v
src/RewriterProofs.v
src/RewriterProofsTactics.v
src/RewriterRules.v
src/RewriterRulesProofs.v
src/RewriterWf1.v
src/RewriterWf2.v
src/SlowPrimeSynthesisExamples.v
src/StandaloneHaskellMain.v
src/StandaloneOCamlMain.v
src/TAPSort.v
src/UnderLets.v
src/UnderLetsProofs.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/Ring.v
src/Algebra/ScalarMult.v
src/Algebra/SubsetoidRing.v
src/Arithmetic/BarrettReduction.v
src/Arithmetic/BaseConversion.v
src/Arithmetic/Core.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/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/ExtractionHaskell/saturated_solinas.v
src/ExtractionHaskell/unsaturated_solinas.v
src/ExtractionHaskell/word_by_word_montgomery.v
src/ExtractionOCaml/saturated_solinas.v
src/ExtractionOCaml/unsaturated_solinas.v
src/ExtractionOCaml/word_by_word_montgomery.v
src/Fancy/Barrett256.v
src/Fancy/Compiler.v
src/Fancy/Montgomery256.v
src/Fancy/Prod.v
src/Fancy/Spec.v
src/Primitives/EdDSARepChange.v
src/Primitives/MxDHRepChange.v
src/PushButtonSynthesis/BarrettReduction.v
src/PushButtonSynthesis/BarrettReductionReificationCache.v
src/PushButtonSynthesis/FancyMontgomeryReduction.v
src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
src/PushButtonSynthesis/InvertHighLow.v
src/PushButtonSynthesis/LegacySynthesisTactics.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/Arith.v
src/Rewriter/ArithWithCasts.v
src/Rewriter/NBE.v
src/Rewriter/StripLiteralCasts.v
src/Rewriter/ToFancy.v
src/Rewriter/ToFancyWithCasts.v
src/Spec/CompleteEdwardsCurve.v
src/Spec/Ed25519.v
src/Spec/EdDSA.v
src/Spec/ModularArithmetic.v
src/Spec/MontgomeryCurve.v
src/Spec/MxDH.v
src/Spec/WeierstrassCurve.v
src/Spec/Test/X25519.v
src/Util/AdditionChainExponentiation.v
src/Util/Arg.v
src/Util/AutoRewrite.v
src/Util/Bool.v
src/Util/BoundedWord.v
src/Util/CPSNotations.v
src/Util/CPSUtil.v
src/Util/ChangeInAll.v
src/Util/Comparison.v
src/Util/Curry.v
src/Util/Decidable.v
src/Util/DefaultedTypes.v
src/Util/Equality.v
src/Util/ErrorT.v
src/Util/Factorize.v
src/Util/FixCoqMistakes.v
src/Util/FixedWordSizes.v
src/Util/FixedWordSizesEquality.v
src/Util/FsatzAutoLemmas.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/ListUtil.v
src/Util/Logic.v
src/Util/Loops.v
src/Util/NUtil.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/WordUtil.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/Reflect.v
src/Util/Decidable/Bool2Prop.v
src/Util/Decidable/Decidable2Bool.v
src/Util/FMapPositive/Equality.v
src/Util/ListUtil/FoldBool.v
src/Util/ListUtil/Forall.v
src/Util/ListUtil/ForallIn.v
src/Util/ListUtil/SetoidList.v
src/Util/Logic/ExistsEqAnd.v
src/Util/Logic/ImplAnd.v
src/Util/Logic/ProdForall.v
src/Util/MSetPositive/Equality.v
src/Util/MSetPositive/Facts.v
src/Util/NUtil/WithoutReferenceToZ.v
src/Util/SideConditions/AdmitPackage.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/BinaryString.v
src/Util/Strings/Decimal.v
src/Util/Strings/Equality.v
src/Util/Strings/HexString.v
src/Util/Strings/OctalString.v
src/Util/Strings/ParseArithmetic.v
src/Util/Strings/Show.v
src/Util/Strings/String.v
src/Util/Strings/StringMap.v
src/Util/Strings/String_as_OT.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/ClearbodyAll.v
src/Util/Tactics/ConstrFail.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/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/Revert.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/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/ZUtil/AddGetCarry.v
src/Util/ZUtil/AddModulo.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/Log2.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/Notations.v
src/Util/ZUtil/Odd.v
src/Util/ZUtil/Ones.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/Sorting.v
src/Util/ZUtil/Stabilization.v
src/Util/ZUtil/Tactics.v
src/Util/ZUtil/Testbit.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/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