blob: 4e3d52282b3ed3323a8aeb68b869d482fb785249 (
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
|
-R src Crypto
-R Bedrock Bedrock
Bedrock/Nomega.v
Bedrock/Word.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/Arithmetic/Core.v
src/Arithmetic/Karatsuba.v
src/Arithmetic/ModularArithmeticPre.v
src/Arithmetic/ModularArithmeticTheorems.v
src/Arithmetic/PrimeFieldTheorems.v
src/Arithmetic/Saturated.v
src/Arithmetic/BarrettReduction/Generalized.v
src/Arithmetic/BarrettReduction/HAC.v
src/Arithmetic/BarrettReduction/Wikipedia.v
src/Arithmetic/MontgomeryReduction/Definition.v
src/Arithmetic/MontgomeryReduction/Proofs.v
src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
src/Compilers/CommonSubexpressionElimination.v
src/Compilers/CommonSubexpressionEliminationDenote.v
src/Compilers/CommonSubexpressionEliminationInterp.v
src/Compilers/CommonSubexpressionEliminationProperties.v
src/Compilers/CommonSubexpressionEliminationWf.v
src/Compilers/Conversion.v
src/Compilers/CountLets.v
src/Compilers/Equality.v
src/Compilers/Eta.v
src/Compilers/EtaInterp.v
src/Compilers/EtaWf.v
src/Compilers/ExprInversion.v
src/Compilers/FilterLive.v
src/Compilers/FoldTypes.v
src/Compilers/Inline.v
src/Compilers/InlineInterp.v
src/Compilers/InlineWf.v
src/Compilers/InputSyntax.v
src/Compilers/InterpByIso.v
src/Compilers/InterpByIsoProofs.v
src/Compilers/InterpProofs.v
src/Compilers/InterpWf.v
src/Compilers/InterpWfRel.v
src/Compilers/Linearize.v
src/Compilers/LinearizeInterp.v
src/Compilers/LinearizeWf.v
src/Compilers/Map.v
src/Compilers/MapCastByDeBruijn.v
src/Compilers/MapCastByDeBruijnInterp.v
src/Compilers/MapCastByDeBruijnWf.v
src/Compilers/MultiSizeTest.v
src/Compilers/Reify.v
src/Compilers/Relations.v
src/Compilers/RenameBinders.v
src/Compilers/Rewriter.v
src/Compilers/RewriterInterp.v
src/Compilers/RewriterWf.v
src/Compilers/SmartMap.v
src/Compilers/Syntax.v
src/Compilers/TestCase.v
src/Compilers/Tuple.v
src/Compilers/TypeInversion.v
src/Compilers/TypeUtil.v
src/Compilers/Wf.v
src/Compilers/WfInversion.v
src/Compilers/WfProofs.v
src/Compilers/WfReflective.v
src/Compilers/WfReflectiveGen.v
src/Compilers/Named/AListContext.v
src/Compilers/Named/Compile.v
src/Compilers/Named/CompileInterp.v
src/Compilers/Named/CompileProperties.v
src/Compilers/Named/CompileWf.v
src/Compilers/Named/Context.v
src/Compilers/Named/ContextDefinitions.v
src/Compilers/Named/ContextOn.v
src/Compilers/Named/ContextProperties.v
src/Compilers/Named/DeadCodeElimination.v
src/Compilers/Named/EstablishLiveness.v
src/Compilers/Named/FMapContext.v
src/Compilers/Named/IdContext.v
src/Compilers/Named/InterpretToPHOAS.v
src/Compilers/Named/InterpretToPHOASInterp.v
src/Compilers/Named/InterpretToPHOASWf.v
src/Compilers/Named/MapCast.v
src/Compilers/Named/MapCastInterp.v
src/Compilers/Named/MapCastWf.v
src/Compilers/Named/NameUtil.v
src/Compilers/Named/NameUtilProperties.v
src/Compilers/Named/PositiveContext.v
src/Compilers/Named/RegisterAssign.v
src/Compilers/Named/RegisterAssignInterp.v
src/Compilers/Named/SmartMap.v
src/Compilers/Named/Syntax.v
src/Compilers/Named/WeakListContext.v
src/Compilers/Named/Wf.v
src/Compilers/Named/WfInterp.v
src/Compilers/Named/ContextProperties/NameUtil.v
src/Compilers/Named/ContextProperties/SmartMap.v
src/Compilers/Named/ContextProperties/Tactics.v
src/Compilers/Named/PositiveContext/Defaults.v
src/Compilers/Named/PositiveContext/DefaultsProperties.v
src/Compilers/Z/ArithmeticSimplifier.v
src/Compilers/Z/ArithmeticSimplifierInterp.v
src/Compilers/Z/ArithmeticSimplifierUtil.v
src/Compilers/Z/ArithmeticSimplifierWf.v
src/Compilers/Z/BinaryNotationConstants.v
src/Compilers/Z/CNotations.v
src/Compilers/Z/CommonSubexpressionElimination.v
src/Compilers/Z/CommonSubexpressionEliminationInterp.v
src/Compilers/Z/CommonSubexpressionEliminationWf.v
src/Compilers/Z/FoldTypes.v
src/Compilers/Z/HexNotationConstants.v
src/Compilers/Z/Inline.v
src/Compilers/Z/InlineInterp.v
src/Compilers/Z/InlineWf.v
src/Compilers/Z/JavaNotations.v
src/Compilers/Z/MapCastByDeBruijn.v
src/Compilers/Z/MapCastByDeBruijnInterp.v
src/Compilers/Z/MapCastByDeBruijnWf.v
src/Compilers/Z/OpInversion.v
src/Compilers/Z/Reify.v
src/Compilers/Z/Syntax.v
src/Compilers/Z/Bounds/Interpretation.v
src/Compilers/Z/Bounds/MapCastByDeBruijn.v
src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v
src/Compilers/Z/Bounds/Pipeline.v
src/Compilers/Z/Bounds/Relax.v
src/Compilers/Z/Bounds/RoundUpLemmas.v
src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
src/Compilers/Z/Bounds/Pipeline/Definition.v
src/Compilers/Z/Bounds/Pipeline/Glue.v
src/Compilers/Z/Bounds/Pipeline/OutputType.v
src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
src/Compilers/Z/Syntax/Equality.v
src/Compilers/Z/Syntax/Util.v
src/Curves/Edwards/AffineProofs.v
src/Curves/Edwards/Pre.v
src/Curves/Edwards/XYZT.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/Projective.v
src/LegacyArithmetic/ArchitectureToZLike.v
src/LegacyArithmetic/ArchitectureToZLikeProofs.v
src/LegacyArithmetic/BarretReduction.v
src/LegacyArithmetic/BaseSystem.v
src/LegacyArithmetic/BaseSystemProofs.v
src/LegacyArithmetic/Interface.v
src/LegacyArithmetic/InterfaceProofs.v
src/LegacyArithmetic/MontgomeryReduction.v
src/LegacyArithmetic/Pow2Base.v
src/LegacyArithmetic/Pow2BaseProofs.v
src/LegacyArithmetic/VerdiTactics.v
src/LegacyArithmetic/ZBounded.v
src/LegacyArithmetic/ZBoundedZ.v
src/LegacyArithmetic/Double/Core.v
src/LegacyArithmetic/Double/Proofs/BitwiseOr.v
src/LegacyArithmetic/Double/Proofs/Decode.v
src/LegacyArithmetic/Double/Proofs/LoadImmediate.v
src/LegacyArithmetic/Double/Proofs/Multiply.v
src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
src/LegacyArithmetic/Double/Proofs/SelectConditional.v
src/LegacyArithmetic/Double/Proofs/ShiftLeft.v
src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
src/LegacyArithmetic/Double/Proofs/ShiftRight.v
src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v
src/Primitives/EdDSARepChange.v
src/Primitives/MxDHRepChange.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/Specific/ArithmeticSynthesisTest.v
src/Specific/ArithmeticSynthesisTest130.v
src/Specific/IntegrationTestDisplayCommon.v
src/Specific/IntegrationTestLadderstep.v
src/Specific/IntegrationTestLadderstep130.v
src/Specific/IntegrationTestLadderstep130Display.v
src/Specific/IntegrationTestLadderstepDisplay.v
src/Specific/IntegrationTestMul.v
src/Specific/IntegrationTestMulDisplay.v
src/Specific/IntegrationTestSquare.v
src/Specific/IntegrationTestSquareDisplay.v
src/Specific/IntegrationTestSub.v
src/Specific/IntegrationTestSubDisplay.v
src/Specific/IntegrationTestTemporaryMiscCommon.v
src/Specific/FancyMachine256/Barrett.v
src/Specific/FancyMachine256/Core.v
src/Specific/FancyMachine256/Montgomery.v
src/Util/AdditionChainExponentiation.v
src/Util/AutoRewrite.v
src/Util/Bool.v
src/Util/BoundedWord.v
src/Util/CPSUtil.v
src/Util/ChangeInAll.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/ForLoop.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/ForLoop/Instances.v
src/Util/ForLoop/InvariantFramework.v
src/Util/ForLoop/Tests.v
src/Util/ForLoop/Unrolling.v
src/Util/Logic/ImplAnd.v
src/Util/Sigma/Associativity.v
src/Util/Sigma/Lift.v
src/Util/Sigma/MapProjections.v
src/Util/Tactics/BreakMatch.v
src/Util/Tactics/ChangeInAll.v
src/Util/Tactics/ClearAll.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/MoveLetIn.v
src/Util/Tactics/Not.v
src/Util/Tactics/OnSubterms.v
src/Util/Tactics/PrintContext.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/TransparentAssert.v
src/Util/Tactics/UnifyAbstractReflexivity.v
src/Util/Tactics/UniquePose.v
src/Util/Tactics/VM.v
src/Util/ZUtil/AddGetCarry.v
src/Util/ZUtil/Definitions.v
src/Util/ZUtil/Div.v
src/Util/ZUtil/EquivModulo.v
src/Util/ZUtil/Hints.v
src/Util/ZUtil/Land.v
src/Util/ZUtil/Modulo.v
src/Util/ZUtil/Morphisms.v
src/Util/ZUtil/Notations.v
src/Util/ZUtil/Pow2Mod.v
src/Util/ZUtil/Quot.v
src/Util/ZUtil/Sgn.v
src/Util/ZUtil/Stabilization.v
src/Util/ZUtil/Tactics.v
src/Util/ZUtil/Testbit.v
src/Util/ZUtil/ZSimplify.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/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/ZeroBounds.v
src/Util/ZUtil/Tactics/Ztestbit.v
src/Util/ZUtil/Tactics/PullPush/Modulo.v
src/Util/ZUtil/Zselect.v
src/Util/ZUtil/ZSimplify/Autogenerated.v
src/Util/ZUtil/ZSimplify/Core.v
src/Util/ZUtil/ZSimplify/Simple.v
|
