Repository navigation
Expand file tree
/
Copy pathCompStark.lean
More file actions
200 lines (199 loc) · 7.74 KB
/
Copy pathCompStark.lean
File metadata and controls
200 lines (199 loc) · 7.74 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
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.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.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.Lde
public import CompStark.Stark.Fast.QuotientSpec
public import CompStark.Stark.Fast.OpeningsSpec
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