Repository navigation
Expand file tree
/
Copy pathCompStark.lean
More file actions
274 lines (259 loc) · 10.2 KB
/
Copy pathCompStark.lean
File metadata and controls
274 lines (259 loc) · 10.2 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
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