Repository navigation
Expand file tree
/
Copy pathCompStark.lean
More file actions
575 lines (560 loc) · 24.8 KB
/
Copy pathCompStark.lean
File metadata and controls
575 lines (560 loc) · 24.8 KB
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
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
module
public import CompStark.BaseField
public import CompStark.Mont32.BaseField
public import CompStark.Mont32.Challenge
public import CompStark.KoalaBear.Field
public import CompStark.BabyBear.Field
public import CompStark.BabyBear.Challenge
public import CompStark.BabyBear.Poseidon2
public import CompStark.Poseidon2.Basic
public import CompStark.Poseidon2.KoalaBear
public import CompStark.Poseidon2.BabyBear
public import CompStark.Poseidon2.Map
public import CompStark.Poseidon2.Arithmetic
public import CompStark.Poseidon2.ArithmeticLemmas
public import CompStark.Poseidon2.Unrolled
public import CompStark.Poseidon2.Packed
public import CompStark.Poseidon2.PackedBabyBear
public import CompStark.Poseidon2.PackedInstances
public import CompStark.Poseidon2.PackedKernels
public import CompStark.Poseidon2.PackedKoalaBear
public import CompStark.Poseidon2.PackedLanes
public import CompStark.Poseidon2.PackedCorrectness
public import CompStark.Poseidon2.PackedCorrectness24
public import CompStark.Hash.Sponge
public import CompStark.Merkle.Tree
public import CompStark.Merkle.Packed
public import CompStark.Merkle.PackedColumns
public import CompStark.Merkle.PackedCorrectness
public import CompStark.Merkle.RootCorrectness
public import CompStark.Poseidon2.Impl
public import CompStark.Poseidon2.PackedField
public import CompStark.KoalaBear.Poseidon2
public import CompStark.Plonky3.Hash
public import CompStark.Challenger
public import CompStark.Primitives
public import CompStark.Stark.Proof
public import CompStark.Merkle.Mmcs
public import CompStark.Merkle.Mixed
public import CompStark.Merkle.MixedMulti
public import CompStark.Stark.Challenge
public import CompStark.DomainSeparator
public import CompStark.KoalaBear.Challenge
public import CompStark.Stark.Field
public import CompStark.Fri.Verifier
public import CompStark.Stark.Air
public import CompStark.Stark.Fingerprint
public import CompStark.Lookup.LogUp
public import CompStark.Lookup.Poly
public import CompStark.Lookup.Lookup
public import CompStark.Lookup.Quotient
public import CompStark.Stark.Verifier
public import CompStark.Plonky3.Primitives
public import CompStark.Mont32.Json
public import CompStark.Stark.Config
public import CompStark.Stark.Points
public import CompStark.Stark.Constraints
public import CompStark.Stark.Recompose
public import CompStark.Fri.Prover
public import CompStark.Fri.Assumptions
public import CompStark.Fri.FoldWords
public import CompStark.Fri.FoldWordsCorrectness
public import CompStark.Fri.Shapes
public import CompStark.Fri.Refines
public import CompStark.Stark.Prover
public import CompStark.Plonky3.Prover
public import CompStark.Batch.Proof
public import CompStark.Batch.Verifier
public import CompStark.Batch.Prover
public import CompStark.Plonky3.Batch
public import CompStark.Complete.LogUp
public import CompStark.Complete.LogUpQuotient
public import CompStark.Batch.Refines
public import CompStark.Stark.Refines
public import CompStark.Stark.Prog
public import CompStark.Stark.ProgWords
public import CompStark.Stark.ProgGroup
public import CompStark.Stark.ProgGen
public import CompStark.Stark.ProgCorrect
public import CompStark.Stark.ProgAlloc
public import CompStark.Stark.ProgCompile
public import CompStark.Stark.Fast
public import CompStark.Stark.Fast.Transcript
public import CompStark.Stark.Fast.Rel
public import CompStark.Stark.Fast.Lde
public import CompStark.Stark.Fast.QuotientSpec
public import CompStark.Stark.Fast.OpeningsSpec
public import CompStark.Stark.Fast.Chunks
public import CompStark.Stark.Fast.Commit
public import CompStark.Stark.Fast.ProgWords
public import CompStark.Stark.Fast.ProgGroup
public import CompStark.Stark.Fast.Vectors
public import CompStark.Stark.Fast.Openings
public import CompStark.Stark.Fast.Quotient
public import CompStark.Stark.Fast.LookupQuotient
public import CompStark.Stark.Fast.Permutation
public import CompStark.Stark.Fast.Refines
public import CompStark.Stark.Fast.Verify
public import CompStark.KoalaBear.Fast
public import CompStark.KoalaBear.Group
public import CompStark.BabyBear.Fast
public import CompStark.Stark.Quotient
public import CompStark.Complete.Defs
public import CompStark.Poseidon2.ArkLib
public import CompStark.Merkle.VCVio
public import CompStark.Merkle.ExtractMixed
public import CompStark.Complete.Merkle
public import CompStark.Complete.Deep
public import CompStark.Complete.Fold
public import CompStark.Complete.FriRound
public import CompStark.Complete.Fri
public import CompStark.Complete.Lde
public import CompStark.Complete.Quotient
public import CompStark.Complete.Stark
public import CompStark.Complete.Pcs
public import CompStark.Complete.Batch
public import CompStark.Stark.Satisfied
public import CompStark.Stark.Setup
public import CompStark.KoalaBear.Completeness
public import CompStark.Sound.Domain
public import CompStark.Iop.StarkSetup
public import CompStark.Iop.StarkError
public import CompStark.Iop.Fri
public import CompStark.Iop.Execution
public import CompStark.Iop.Stark
public import CompStark.Iop.Gate
public import CompStark.Iop.Batch
public import CompStark.Sound.Steps
public import CompStark.Sound.Fri
public import CompStark.Sound.Algebra
public import CompStark.Sound.Batching
public import CompStark.Sound.Decoding
public import CompStark.Sound.Assembly
public import CompStark.Iop.BatchSetup
public import CompStark.Iop.BatchError
public import CompStark.Sound.BatchAssembly
public import CompStark.Iop.BatchSoundness
public import CompStark.Iop.StarkSoundness
public import CompStark.Sound.Johnson
public import CompStark.Calculator.Numbers
public import CompStark.Calculator.Bounds
public import CompStark.Calculator.Sound
public import CompStark.Calculator.Security
public import CompStark.Sound.LogUp
public import CompStark.Sound.Telescope
public import CompStark.Sound.BatchLogUp
public import CompStark.Sound.Inclusion
public import CompStark.Sound.Counts
public import CompStark.Sound.Range
public import CompStark.Iop.LookupInclusion
public import CompStark.Calculator.McaBound
public import CompStark.Batch.Setup
public import CompStark.Fs.BatchRandomOracle
public import CompStark.Sound.BatchRbr
public import CompStark.Iop.BatchKnowledge
public import CompStark.Iop.BatchCompleteness
public import CompStark.Iop.StarkCompleteness
public import CompStark.Sound.Sampling
public import CompStark.Sound.Rbr
public import CompStark.Iop.StarkKnowledge
public import CompStark.Iop.StarkStateRestoration
public import CompStark.Iop.BatchStateRestoration
public import CompStark.Fs.RandomOracle
public import CompStark.Fs.StarkSimulate
public import CompStark.Fs.StarkCalls
public import CompStark.Fs.StarkTranscript
public import CompStark.Fs.StarkAccept
public import CompStark.Fs.FriFold
public import CompStark.Fs.FriBinding
public import CompStark.Fs.StarkCheck
public import CompStark.Fs.StarkDeep
public import CompStark.Fs.StarkChallenges
public import CompStark.Fs.Observations
public import CompStark.Fs.Samples
public import CompStark.Fs.HashChain
public import CompStark.Fs.MerkleLog
public import CompStark.Fs.StarkSetup
public import CompStark.Fs.DomainSeparator
public import CompStark.Fs.StarkLengths
public import CompStark.Fs.MixedAccept
public import CompStark.Fs.BatchAccept
public import CompStark.Fs.MixedBinding
public import CompStark.Fs.BatchDeep
public import CompStark.Fs.BatchCheck
public import CompStark.Fs.BatchExtract
public import CompStark.Fs.BatchSimulate
public import CompStark.Fs.BatchCalls
public import CompStark.Fs.BatchTranscript
public import CompStark.Fs.BatchLengths
public import CompStark.Fs.BatchSetup
public import CompStark.Fs.Draws
public import CompStark.Fs.Stark
public import CompStark.Fs.StarkWords
public import CompStark.Fs.StarkTerminal
public import CompStark.Fs.StarkParse
public import CompStark.Fs.StarkStable
public import CompStark.Fs.BatchWords
public import CompStark.Fs.Batch
public import CompStark.Fs.StarkFiatShamir
public import CompStark.Fs.StarkBcs
public import CompStark.Calculator.FiatShamir
public import CompStark.Fs.BatchFiatShamir
public import CompStark.Fs.BatchParse
public import CompStark.Fs.BatchTerminal
public import CompStark.Fs.BatchStable
public import CompStark.Fs.BatchBcs
public import CompStark.Keccak.Scalar
public import CompStark.Keccak.WordLoop
public import CompStark.Keccak.Sponge
public import CompStark.Keccak.Hash
public import CompStark.Keccak.Refines
public import CompStark.Keccak.Merkle
public import CompStark.Keccak.MerkleGenerate
public import CompStark.Keccak.MerkleRows
public import CompStark.Keccak.Duplex
public import CompStark.Keccak.Prepared
public import CompStark.Sumcheck.ByteMap
public import CompStark.Sumcheck.Fold
public import CompStark.Sumcheck.Preparation
public import CompStark.Sumcheck.Buffer
public import CompStark.Sumcheck.PackedFold
public import CompStark.Sumcheck.IndexFold
public import CompStark.Pcs.RingSwitch
public import CompStark.Pcs.Tensor
public import CompStark.Pcs.HonestRound
public import CompStark.Pcs.HonestWhir
public import CompStark.Pcs.Encoding
public import CompStark.Pcs.CoordinateMap
public import CompStark.Pcs.Induction
public import CompStark.Pcs.Accumulated
public import CompStark.Pcs.NativeRound
public import CompStark.Pcs.Basis
public import CompStark.Pcs.NativeBasis
public import CompStark.Sumcheck.WordProductProofs
public import CompStark.Pcs.BasisWindow
public import CompStark.Pcs.BasisColumn
public import CompStark.Pcs.BasisColumnPrepared
public import CompStark.Pcs.InductionDot
public import CompStark.Pcs.PackedInductionDot
public import CompStark.Pcs.SparseInduction
public import CompStark.Pcs.CompactInduction
public import CompStark.Pcs.TwiddleRow
public import CompStark.Pcs.TiledInduction
public import CompStark.Pcs.SparseStrip
public import CompStark.Pcs.DirectSums
public import CompStark.Pcs.ChallengeFold
public import CompStark.Pcs.FusedRound
public import CompStark.Pcs.BitFold
public import CompStark.Pcs.Projected
public import CompStark.Pcs.TensorProjection
public import CompStark.Pcs.TensorProjectionActive
public import CompStark.Pcs.ByteFoldRows
public import CompStark.Pcs.MixedDot
public import CompStark.Pcs.TensorProjectionPacked
public import CompStark.Pcs.WindowBitFold
public import CompStark.Pcs.WindowScatter
public import CompStark.Pcs.FusedPairs
public import CompStark.Pcs.FusedTensor
public import CompStark.Pcs.TensorRing
public import CompStark.Pcs.WindowFold
public import CompStark.BinaryFields.Basic
public import CompStark.BinaryFields.Generator
public import CompStark.BinaryFields.Native
public import CompStark.BinaryFields.WordProduct
public import CompStark.Compiled.CostScale
public import CompStark.Compiled.PathKeys
public import CompStark.Compiled.WitnessRandomOracle
public import CompStark.Compose.ListLift
public import CompStark.Compose.Reduction
public import CompStark.Compose.Transport
public import CompStark.Compose.WitnessListLift
public import CompStark.Compose.WitnessOrder
public import CompStark.Keccak.Commit.Bytes
public import CompStark.Keccak.Commit.Collision
public import CompStark.Keccak.Commit.CollisionOracle
public import CompStark.Keccak.Commit.Consistent
public import CompStark.Keccak.Commit.FullWidth
public import CompStark.Keccak.Commit.HashMemo
public import CompStark.Keccak.Commit.Masked
public import CompStark.Keccak.Commit.Merkle
public import CompStark.Keccak.Commit.Native
public import CompStark.Keccak.Commit.RandomOracleTrace
public import CompStark.Keccak.Commit.RootMemo
public import CompStark.Keccak.Commit.ScalarMerkle
public import CompStark.Keccak.Commit.WordBuffer
public import CompStark.Keccak.Commit.WordRead
public import CompStark.Keccak.Construction
public import CompStark.Keccak.Embedding
public import CompStark.Keccak.EmbeddingData
public import CompStark.Keccak.Factors
public import CompStark.Keccak.Gkr
public import CompStark.Keccak.Gkr.BetaBoundary
public import CompStark.Keccak.Gkr.Claims
public import CompStark.Keccak.Gkr.Executable
public import CompStark.Keccak.Gkr.ExecutableClaims
public import CompStark.Keccak.Gkr.ExecutionBounds
public import CompStark.Keccak.Gkr.InitialBoundary
public import CompStark.Keccak.Gkr.InitialSampling
public import CompStark.Keccak.Gkr.Knowledge
public import CompStark.Keccak.Gkr.KnowledgeBoundaries
public import CompStark.Keccak.Gkr.KnowledgeBounds
public import CompStark.Keccak.Gkr.KnowledgeEncoding
public import CompStark.Keccak.Gkr.KnowledgeLocal
public import CompStark.Keccak.Gkr.KnowledgePhases
public import CompStark.Keccak.Gkr.KnowledgePrefix
public import CompStark.Keccak.Gkr.KnowledgeRounds
public import CompStark.Keccak.Gkr.KnowledgeSchedule
public import CompStark.Keccak.Gkr.KnowledgeSumcheck
public import CompStark.Keccak.Gkr.LayerExecution
public import CompStark.Keccak.Gkr.LayerSequence
public import CompStark.Keccak.Gkr.LocalBounds
public import CompStark.Keccak.Gkr.OpeningAlgebra
public import CompStark.Keccak.Gkr.OpeningBoundaries
public import CompStark.Keccak.Gkr.OpeningExecution
public import CompStark.Keccak.Gkr.PhaseBoundaries
public import CompStark.Keccak.Gkr.PhaseBounds
public import CompStark.Keccak.Gkr.PhasePolynomials
public import CompStark.Keccak.Gkr.Protocol
public import CompStark.Keccak.Gkr.ProtocolExecution
public import CompStark.Keccak.Gkr.ProtocolSoundness
public import CompStark.Keccak.GkrProver.BinaryEvaluation
public import CompStark.Keccak.GkrProver.BinaryTensor
public import CompStark.Keccak.GkrProver.BinaryValues
public import CompStark.Keccak.GkrProver.BucketLoops
public import CompStark.Keccak.GkrProver.BucketProofs
public import CompStark.Keccak.GkrProver.Cofactor
public import CompStark.Keccak.GkrProver.CofactorBlocks
public import CompStark.Keccak.GkrProver.CofactorTransport
public import CompStark.Keccak.GkrProver.Completeness
public import CompStark.Keccak.GkrProver.ConstantBlocks
public import CompStark.Keccak.GkrProver.EarlyPackTrace
public import CompStark.Keccak.GkrProver.EarlyRounds
public import CompStark.Keccak.GkrProver.FieldTransport
public import CompStark.Keccak.GkrProver.FoldedPackMaps
public import CompStark.Keccak.GkrProver.Honest
public import CompStark.Keccak.GkrProver.InputBitSemantics
public import CompStark.Keccak.GkrProver.InputColumns
public import CompStark.Keccak.GkrProver.InputOpeningHonest
public import CompStark.Keccak.GkrProver.InputOpeningSemantics
public import CompStark.Keccak.GkrProver.InputTables
public import CompStark.Keccak.GkrProver.InputTableValues
public import CompStark.Keccak.GkrProver.Kernels
public import CompStark.Keccak.GkrProver.LatePack
public import CompStark.Keccak.GkrProver.LayerTrace
public import CompStark.Keccak.GkrProver.Native
public import CompStark.Keccak.GkrProver.NativeBatching
public import CompStark.Keccak.GkrProver.NativeCompleteness
public import CompStark.Keccak.GkrProver.NativeEarlyRounds
public import CompStark.Keccak.GkrProver.NativeInitialClaim
public import CompStark.Keccak.GkrProver.NativeLayerHonest
public import CompStark.Keccak.GkrProver.NativeLayerSemantics
public import CompStark.Keccak.GkrProver.NativeLoops
public import CompStark.Keccak.GkrProver.NativeOpening
public import CompStark.Keccak.GkrProver.NativePackSemantics
public import CompStark.Keccak.GkrProver.NativeReductionTrace
public import CompStark.Keccak.GkrProver.NativeSetup
public import CompStark.Keccak.GkrProver.NativeTensor
public import CompStark.Keccak.GkrProver.NativeTensorContraction
public import CompStark.Keccak.GkrProver.NativeWitnessCompleteness
public import CompStark.Keccak.GkrProver.OpeningSemantics
public import CompStark.Keccak.GkrProver.OpeningTrace
public import CompStark.Keccak.GkrProver.PackBoundary
public import CompStark.Keccak.GkrProver.Packed
public import CompStark.Keccak.GkrProver.PackedAccumulation
public import CompStark.Keccak.GkrProver.PackedBlocks
public import CompStark.Keccak.GkrProver.PackedProofs
public import CompStark.Keccak.GkrProver.PackedTableContraction
public import CompStark.Keccak.GkrProver.PackedTableValues
public import CompStark.Keccak.GkrProver.PackedWords
public import CompStark.Keccak.GkrProver.PackHonest
public import CompStark.Keccak.GkrProver.PackSemantics
public import CompStark.Keccak.GkrProver.PackTerminal
public import CompStark.Keccak.GkrProver.PackTrace
public import CompStark.Keccak.GkrProver.PayloadProofs
public import CompStark.Keccak.GkrProver.PositionHonest
public import CompStark.Keccak.GkrProver.PositionSemantics
public import CompStark.Keccak.GkrProver.PositionTerminal
public import CompStark.Keccak.GkrProver.PositionTrace
public import CompStark.Keccak.GkrProver.ProductAccumulation
public import CompStark.Keccak.GkrProver.ProductEvaluation
public import CompStark.Keccak.GkrProver.ProductProofs
public import CompStark.Keccak.GkrProver.ProductSemantics
public import CompStark.Keccak.GkrProver.ProductVertices
public import CompStark.Keccak.GkrProver.QuadraticHonest
public import CompStark.Keccak.GkrProver.QuadraticRounds
public import CompStark.Keccak.GkrProver.QuadraticTerminal
public import CompStark.Keccak.GkrProver.QuadraticTrace
public import CompStark.Keccak.GkrProver.QuadraticValues
public import CompStark.Keccak.GkrProver.Refinement
public import CompStark.Keccak.GkrProver.RetainedProducts
public import CompStark.Keccak.GkrProver.Rmfe
public import CompStark.Keccak.GkrProver.RmfeProofs
public import CompStark.Keccak.GkrProver.SharedTable
public import CompStark.Keccak.GkrProver.SubsetTables
public import CompStark.Keccak.GkrProver.SumcheckBlocks
public import CompStark.Keccak.GkrProver.TensorAccumulation
public import CompStark.Keccak.GkrProver.TensorBlocks
public import CompStark.Keccak.GkrProver.TensorContraction
public import CompStark.Keccak.GkrProver.TensorEndpoints
public import CompStark.Keccak.GkrProver.TensorHonest
public import CompStark.Keccak.GkrProver.TensorInterpolation
public import CompStark.Keccak.GkrProver.TensorLift
public import CompStark.Keccak.GkrProver.TensorProofs
public import CompStark.Keccak.GkrProver.TensorRmfe
public import CompStark.Keccak.GkrProver.TensorRows
public import CompStark.Keccak.GkrProver.TensorSuffix
public import CompStark.Keccak.GkrProver.TensorValues
public import CompStark.Keccak.GkrProver.TransposeSemantics
public import CompStark.Keccak.GkrProver.WeightMapEval
public import CompStark.Keccak.GkrProver.WeightMapProofs
public import CompStark.Keccak.GkrProver.WitnessTrace
public import CompStark.Keccak.GkrProver.WordOpeningSemantics
public import CompStark.Keccak.GkrProver.WriterLog
public import CompStark.Keccak.GkrProver.WriterSchedule
public import CompStark.Keccak.Gkr.ResidualAlgebra
public import CompStark.Keccak.Gkr.RoundProjection
public import CompStark.Keccak.Gkr.Soundness
public import CompStark.Keccak.Gkr.StateImages
public import CompStark.Keccak.Gkr.SumcheckExecution
public import CompStark.Keccak.Gkr.Tensor
public import CompStark.Keccak.Gkr.Transport
public import CompStark.Keccak.Gkr.WireEncoding
public import CompStark.Keccak.Gkr.WireExecution
public import CompStark.Keccak.Lanes
public import CompStark.Keccak.Native
public import CompStark.Keccak.Transcript.Correspondence
public import CompStark.Keccak.Transcript.Duplex
public import CompStark.Keccak.Transcript.Native
public import CompStark.Multilinear.Algebra.AmbientStacking
public import CompStark.Multilinear.Algebra.ExecutableCoefficients
public import CompStark.Multilinear.Algebra.Fingerprint
public import CompStark.Multilinear.Algebra.GrandProduct
public import CompStark.Multilinear.Algebra.Multilinear
public import CompStark.Multilinear.Algebra.PaddedProduct
public import CompStark.Multilinear.Algebra.RootFamily
public import CompStark.Multilinear.Algebra.Stacking
public import CompStark.Multilinear.Retained
public import CompStark.Multilinear.Threshold
public import CompStark.Pcs.AdditiveEncoding
public import CompStark.Pcs.BinaryDomain
public import CompStark.Pcs.Bits
public import CompStark.Pcs.Conversion
public import CompStark.Pcs.Decoder
public import CompStark.Pcs.Evaluated
public import CompStark.Pcs.ExactDecoder
public import CompStark.Pcs.Extraction
public import CompStark.Pcs.ExtractorCache
public import CompStark.Pcs.FastEncoding
public import CompStark.Pcs.PackedCodeword
public import CompStark.Pcs.PackedEncoding
public import CompStark.Pcs.ParallelClaims
public import CompStark.Pcs.Parameters
public import CompStark.Pcs.Prover.Encoding
public import CompStark.Pcs.Radius
public import CompStark.Pcs.RingSwitch.BadEvents
public import CompStark.Pcs.RingSwitch.Fields
public import CompStark.Pcs.RingSwitch.Frobenius
public import CompStark.Pcs.RingSwitch.Protocol
public import CompStark.Pcs.RingSwitch.Prover
public import CompStark.Pcs.RingSwitch.TargetWord
public import CompStark.Pcs.Schedule
public import CompStark.Pcs.Verifier
public import CompStark.Pcs.Weights
public import CompStark.Pcs.WordEncoding
public import CompStark.Pcs.WordSum
public import CompStark.Multilinear.Algebra.MaskedMle
public import CompStark.Multilinear.Algebra.Mle
public import CompStark.Multilinear.Algebra.SumcheckBound
public import CompStark.Multilinear.Basic
public import CompStark.Pcs.Errors
public import CompStark.Pcs.LevelBounds
public import CompStark.Pcs.Levels
public import CompStark.Pcs.Multiplicity
public import CompStark.Pcs.ProductionLevels
public import CompStark.Pcs.Honest
public import CompStark.Multilinear.GrandProduct
public import CompStark.Multilinear.GrandProductHonest
public import CompStark.Multilinear.Coefficients
public import CompStark.Multilinear.GrandProductDecision
public import CompStark.Multilinear.GrandProductBadEvents
public import CompStark.Multilinear.WordGrandProduct
public import CompStark.Compiled.ChallengeSnapshot
public import CompStark.Compiled.FreshOracleLog
public import CompStark.Compiled.FreshSnapshot
public import CompStark.Compiled.MerkleTrace
public import CompStark.Compiled.MerkleOracle
public import CompStark.Keccak.Commit.Codec
public import CompStark.Keccak.Commit.MerkleCodec
public import CompStark.Tables.Basic
public import CompStark.Tables.Examples
public import CompStark.Tables.Fingerprint
public import CompStark.Tables.Bus
public import CompStark.Tables.Riders
public import CompStark.Tables.Leaves
public import CompStark.Tables.BusSound
public import CompStark.Tables.Decomposition
public import CompStark.Tables.Forms
public import CompStark.Tables.BusOutput
public import CompStark.Tables.BusDecomposition
public import CompStark.Tables.BusProtocol
public import CompStark.Tables.TablePoly
public import CompStark.Tables.TableSumcheck
public import CompStark.Tables.Argument
public import CompStark.Tables.Stack
public import CompStark.Tables.Composed.External
public import CompStark.Tables.Composed.Pool
public import CompStark.Tables.Composed.Outer
public import CompStark.Tables.Composed.Budget
public import CompStark.Tables.Composed.Certificate
public import CompStark.Tables.Composed.HonestBus
public import CompStark.Tables.Composed.HonestTable
public import CompStark.Tables.Composed.Honest
public import CompStark.Tables.Composed.Verifier
public import CompStark.Tables.Composed.Keccak.Transport
public import CompStark.Tables.Composed.Keccak.Encoding
public import CompStark.Tables.Composed.Keccak.Table
public import CompStark.Tables.Composed.Keccak.Rider
public import CompStark.Tables.Composed.Keccak.Start
public import CompStark.Tables.Composed.Keccak.Ring
public import CompStark.Tables.Composed.Keccak.Checks
public import CompStark.Tables.Composed.Keccak.Protocol
public import CompStark.Tables.Composed.Keccak.External
public import CompStark.Tables.Composed.Keccak.Honest
public import CompStark.Compiled.Projection
public import CompStark.Compiled.Presentation
public import CompStark.Compiled.Whir
public import CompStark.Compiled.Protocol
public import CompStark.Compiled.Transfer
public import CompStark.Tables.Compiled.Presentation
public import CompStark.Tables.Compiled.Protocol
public import CompStark.Tables.Compiled.Transfer
public import CompStark.Tables.Compiled.Acceptance
public import CompStark.Compiled.Transcript
public import CompStark.Compiled.Count
public import CompStark.Compiled.Check
public import CompStark.Tables.Compiled.Transcript
public import CompStark.Tables.Compiled.Count
public import CompStark.Compiled.WhirTerminal
public import CompStark.Tables.Compiled.Soundness
public import CompStark.Tables.Compiled.External
public import CompStark.Tables.Compiled.Verifier
public import CompStark.Pcs.HonestRoundFast
public import CompStark.Pcs.EvaluatedLadder
public import CompStark.Compiled.Prover
public import CompStark.Compiled.GrandProductProver
public import CompStark.Compiled.WhirProver
public import CompStark.Tables.Compiled.Prover
public import CompStark.Tables.Compiled.KeccakProver
public import CompStark.Compiled.ProverChecks
public import CompStark.Compiled.ProverRun
public import CompStark.Compiled.GrandProductRun
public import CompStark.Tables.Compiled.HonestRun
public import CompStark.Compiled.WhirRun
public import CompStark.Compiled.LeafRows
public import CompStark.Tables.Compiled.Completeness
public import CompStark.Tables.Compiled.KeccakFollows
public import CompStark.Tables.Composed.Extractor
public import CompStark.Tables.Compiled.Extractor
public import CompStark.Tables.Compiled.Listed
public import CompStark.Tables.Compiled.ListedOracle
public import CompStark.Tables.Compiled.ListedGame