Repository navigation
Expand file tree
/
Copy pathCompStark.lean
More file actions
208 lines (207 loc) · 7.95 KB
/
Copy pathCompStark.lean
File metadata and controls
208 lines (207 loc) · 7.95 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
module
public import CompStark.Basic
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.Packed24
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.Multi
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.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.Norm
public import CompStark.Stark.Fast.Lde
public import CompStark.Stark.Fast.QuotientSpec
public import CompStark.Stark.Fast.OpeningsSpec
public import CompStark.Stark.Fast.BatchInv
public import CompStark.Stark.Fast.Commit
public import CompStark.Stark.Fast.WordsLemmas
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.Words
public import CompStark.Stark.Quotient
public import CompStark.Stark.ExtWords
public import CompStark.Complete.Defs
public import CompStark.Poseidon2.ArkLib
public import CompStark.Merkle.VCVio
public import CompStark.Merkle.Extract
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.Completeness
public import CompStark.BatchCompleteness
public import CompStark.KoalaBear.Completeness
public import CompStark.Sound.Defs
public import CompStark.Iop
public import CompStark.SoundnessError
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.BatchIop
public import CompStark.BatchSoundnessError
public import CompStark.Sound.BatchAssembly
public import CompStark.BatchSoundness
public import CompStark.Sound.Single
public import CompStark.Soundness
public import CompStark.Sound.Johnson
public import CompStark.Sound.CurveBW
public import CompStark.Sound.PowersMca
public import CompStark.Sound.Numbers
public import CompStark.Sound.NumbersNi
public import CompStark.Sound.BatchNumbersNi
public import CompStark.SecurityCalculator
public import CompStark.Sound.Calculator
public import CompStark.Security
public import CompStark.Sound.CurveCA
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.LookupInclusion
public import CompStark.Sound.LossyMca
public import CompStark.Fs.FreshQuery
public import CompStark.Fs.DigestClash
public import CompStark.NonInteractiveError
public import CompStark.Sound.FriRun
public import CompStark.BatchNonInteractiveError
public import CompStark.Batch.Setup
public import CompStark.BatchRandomOracle
public import CompStark.BatchNonInteractive
public import CompStark.Sound.BatchRbr
public import CompStark.Sound.Sampling
public import CompStark.Sound.ConsistentQueries
public import CompStark.Sound.Rbr
public import CompStark.RandomOracle
public import CompStark.Ni.Natural
public import CompStark.Ni.Answers
public import CompStark.Ni.QueryBound
public import CompStark.Ni.Parse
public import CompStark.Ni.BcsRun
public import CompStark.Ni.BcsFold
public import CompStark.Ni.BcsFri
public import CompStark.Ni.BcsCheck
public import CompStark.Ni.BcsDeep
public import CompStark.Ni.Bcs
public import CompStark.Ni.BcsChallenges
public import CompStark.Ni.Rounds
public import CompStark.Ni.FirstQueries
public import CompStark.Ni.RoundBounds
public import CompStark.Ni.Binding
public import CompStark.Ni.Setup
public import CompStark.Ni.Accepted
public import CompStark.Ni.Extracted
public import CompStark.Ni.BadQuery
public import CompStark.Ni.Assembly
public import CompStark.Ni.BatchRun
public import CompStark.Ni.BatchAccept
public import CompStark.Ni.BatchFri
public import CompStark.Ni.BatchBind
public import CompStark.Ni.BatchDeep
public import CompStark.Ni.BatchCheck
public import CompStark.Ni.BatchBcs
public import CompStark.Ni.BatchNatural
public import CompStark.Ni.BatchQueryBound
public import CompStark.Ni.BatchParse
public import CompStark.Ni.BatchChallenges
public import CompStark.Ni.BatchRounds
public import CompStark.Ni.BatchRoundBounds
public import CompStark.Ni.BatchExtracted
public import CompStark.Ni.BatchAccepted
public import CompStark.Ni.BatchSetup
public import CompStark.Ni.BatchBadQuery
public import CompStark.Ni.BatchAssembly
public import CompStark.NonInteractive