Skip to content

Batched FRI soundness #273

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Julek wants to merge 225 commits into
base: main
Choose a base branch
from
Draft

Batched FRI soundness #273

Show file tree
Hide file tree
Changes from 222 commits
Commits
Show all changes
225 commits
Select commit Hold shift + click to select a range
cc2629a
small improvement to statement of h_le_1 assumption of Polishchuk_Spi…
Julek Jun 16, 2025
1ea945c
Update ArkLib/Data/CodingTheory/BivariatePoly.lean
quangvdao Jun 16, 2025
4c24ea3
WIP
Julek Jun 24, 2025
6473dd3
degreeX_mul done
Julek Jun 24, 2025
3b0e419
Weighted degree
ElijahVlasov Jun 23, 2025
ede0236
Root multiplicity
ElijahVlasov Jun 25, 2025
5412d78
WIP
ElijahVlasov Jun 26, 2025
07436ca
Decoder spec
ElijahVlasov Jun 26, 2025
36619fd
WIP
ElijahVlasov Jun 27, 2025
0dd8767
fix typeclass inference
Ferinko Jun 27, 2025
28fb534
Guruswami-Sudan blueprint.
ElijahVlasov Jun 27, 2025
043f26d
After rebase
ElijahVlasov Jul 4, 2025
7462c26
Add proximity gap paper guruswami-sudan
ElijahVlasov Jul 8, 2025
35ad389
Add non-zero condition into GS
ElijahVlasov Jul 9, 2025
e8ab9f3
Lemma 5.4
ElijahVlasov Jul 11, 2025
036b9b4
split filest
katyhr Jun 4, 2025
f03501a
PS lemma second draft
katyhr Jun 4, 2025
90dc65b
some changes
katyhr Jun 5, 2025
06709ab
edited dependency
katyhr Jun 5, 2025
ca7c5e5
new degreeX def
katyhr Jun 6, 2025
456fa03
building the lemmas database
katyhr Jun 6, 2025
b9d59ae
division condition fixed, moved defs, some cleanup
katyhr Jun 12, 2025
7898607
major cleanup and reorg, still some sorries left
katyhr Jun 12, 2025
910c3de
Removed some unneeded assumptions, fixed definitions with missing arg…
Julek Jun 13, 2025
daefa87
simplified proof of quotient_nezero
Julek Jun 13, 2025
34048f5
Filled in sorrys in monomial_xy definition
Julek Jun 13, 2025
ae025f8
Added monomial_xy_def, a simple equality that acts as an effective de…
Julek Jun 13, 2025
1c10793
Rebased FRI implementation
ElijahVlasov Jun 12, 2025
c845d15
Fixes to the FRI implementation
Julek Jun 16, 2025
2fc64ee
Rebased FRI implementation
ElijahVlasov Jun 12, 2025
a8e28de
Fixed imports
Julek Jul 1, 2025
dd8e7ff
quick type fix
Julek Jul 15, 2025
b9770e0
WIP
ElijahVlasov Jul 16, 2025
fa77c8a
WIp
ElijahVlasov Jul 21, 2025
0bbadc1
Lemma 5.7
ElijahVlasov Jul 24, 2025
e7294ca
Draft implementation of a single round of the FRI protocol using the …
Julek Jul 27, 2025
5770d71
Fixed negation issue and a bit of refactoring
Julek Jul 27, 2025
7cea0ea
some more cleanup
Julek Jul 28, 2025
a031880
WIP
ElijahVlasov Jul 28, 2025
cc2336e
WIP
ElijahVlasov Jul 28, 2025
a74f238
Lemma 5.6
ElijahVlasov Jul 28, 2025
7548a12
Theorem 6.1
ElijahVlasov Jul 29, 2025
7173684
Bivariate.lean
Ferinko Jul 29, 2025
1ee9c10
Theorem 6.2
ElijahVlasov Jul 29, 2025
5f8e2bb
EvenAndOdd.lean - remove _def, use .eq_def
Ferinko Jul 29, 2025
fc09744
Impl.lean - simplify query
Ferinko Jul 29, 2025
4e451f0
Domain.lean - ascencion
Ferinko Jul 29, 2025
453c822
Domain.lean
Ferinko Jul 29, 2025
4265658
refactor Q to Q>=0, fix proofs
Ferinko Jun 19, 2025
e9023d5
relHamming dist proofs
katyhr Jun 19, 2025
e46aec3
minor cleanup
Ferinko Jun 19, 2025
9d26457
more cleanups
katyhr Jun 19, 2025
0405d2e
final minor cleanups
katyhr Jun 19, 2025
3b95d6e
ProximityGaps draft1
katyhr Jun 25, 2025
5ab89e9
some stuff
katyhr Jun 26, 2025
15bc72d
proximity wip
katyhr Jul 11, 2025
def6bdb
line 257
katyhr Jul 11, 2025
2da9f41
WIP - thing3 + nonempty explicitly given
Ferinko Jul 11, 2025
addf08c
fix decidable equality
Ferinko Jul 11, 2025
14f1bdb
def generalProximityGap
katyhr Jul 17, 2025
4aa5a4d
fix generalProximityGap
Ferinko Jul 17, 2025
0237fe9
or something like this
Ferinko Jul 17, 2025
8f3ba9d
latest WIP
katyhr Jul 18, 2025
eabf704
proximityGaps results
katyhr Jul 28, 2025
cb96f05
cleanup proximity, reedsolomon, divergence and prelims
Ferinko Jul 30, 2025
003a841
fix the variable name
Ferinko Jul 30, 2025
5d53683
Merge pull request #30 from NethermindEth/Ferinko/Katy/ProximityWIP
katyhr Jul 31, 2025
f7c936f
WIP
ElijahVlasov Aug 4, 2025
486c569
Merge remote-tracking branch 'origin/Katy/ProximityWIP' into ElijahVl…
ElijahVlasov Aug 4, 2025
61111e8
Lemma 6.3
ElijahVlasov Aug 5, 2025
9e46cf7
WIP
ElijahVlasov Aug 11, 2025
79a74b5
Theorem 7.1
ElijahVlasov Aug 11, 2025
8fedbab
Fixed
ElijahVlasov Aug 12, 2025
5f77194
7.2
ElijahVlasov Aug 12, 2025
2a4078f
7.3
ElijahVlasov Aug 12, 2025
f706239
7.4
ElijahVlasov Aug 12, 2025
7924247
7.5
ElijahVlasov Aug 13, 2025
4255693
7.6!!!🥃🥃🥃🥃🥃🥃🥃
ElijahVlasov Aug 13, 2025
9d795d9
Merge pull request #29 from NethermindEth/Huh
Ferinko Aug 18, 2025
7b6ba03
Merge branch 'Katy/PSLemmaRebased' into Katy/BivariateRebase
katyhr Aug 18, 2025
c47f7f6
Merge branch 'Julek/ElijahVlasov/fri-implementation-rebase' into Katy…
katyhr Aug 18, 2025
d30a264
Merge branch 'ElijahVlasov/theorem_6_1' into Katy/BivariateRebase
katyhr Aug 18, 2025
7ec001a
Bivariate merged
katyhr Aug 18, 2025
f137320
more weighted degrees, remove redundant variables
katyhr Aug 20, 2025
994c08e
weighted degree and monomial degree lemmas and proofs
katyhr Aug 26, 2025
d4e65ee
AppendixA_1 first draft
katyhr Aug 29, 2025
03db23c
dependency for rational functions added
katyhr Aug 29, 2025
dec92da
fixed a typo
katyhr Aug 29, 2025
840a99a
first draft of some stuff
katyhr Aug 29, 2025
69135af
WIP - Hmonic
Ferinko Sep 4, 2025
525294c
Sketch of L function field and its ring of integers
Julek Sep 15, 2025
e77fddd
Preliminary lemmas and defs for polynomials
katyhr Sep 16, 2025
f39b937
added Polynomial prelims
katyhr Sep 16, 2025
ea42d72
initial cleanup after new defs
katyhr Sep 16, 2025
923ff6e
`UniPoly` equivalence relation and quotient operations (#106)
dhsorens Aug 26, 2025
1ba6dcc
feat: Inductive Merkle Trees with completeness theorem (#44)
BoltonBailey Aug 26, 2025
c818fb6
Blueprint for Guruswami-Sudan (#81)
ElijahVlasov Aug 27, 2025
0229e76
[DRAFT] Fix: WHIR/STIR (#85)
alexanderlhicks Aug 27, 2025
ffd2081
Add comprehensive dependency analysis toolkit (#133)
quangvdao Aug 27, 2025
38f4981
feat: rename `oracle` => `answer` in OracleInterface (#134)
quangvdao Aug 27, 2025
9dfbc7b
feat: reorganize workflows (#135)
quangvdao Aug 27, 2025
28e6934
feat: change lakefile.lean to lakefile.toml (#136)
quangvdao Aug 28, 2025
834d5cd
chore: Renaming of oracle interface instances (#139)
quangvdao Aug 29, 2025
743b20b
lemma decoded_polynomial_lt_deg [ArkLib/Data/CodingTheory/ReedSolomon…
winger Aug 30, 2025
550210a
theorem singleton_bound_linear [ArkLib/Data/CodingTheory/Basic.lean] …
winger Aug 30, 2025
8a16c4b
theorem dist'_eq_dist [ArkLib/Data/CodingTheory/Basic.lean] #107
winger Aug 30, 2025
2cf6fd2
Add missing lemma
winger Aug 31, 2025
2863ff6
instance {s} : LawfulFunctor (fun α => FullData α s) [ArkLib/ToMathli…
winger Aug 30, 2025
09648ce
Revert theorem def to original
winger Aug 31, 2025
ccf1cd1
feat: Define BN254 curve (#138)
quangvdao Sep 9, 2025
ac9fc1d
define KoalaBear field, change name of `fieldSize`
quangvdao Sep 12, 2025
1ee36fe
feat: define Koala Bear field & Poseidon2 spec (#204)
quangvdao Sep 12, 2025
391bbe2
feat: add PR summary workflow
alexanderlhicks Sep 14, 2025
c8b039c
accidently pointed to old model
alexanderlhicks Sep 14, 2025
3aac2c6
fix: correct diff command in pr-summary workflow
alexanderlhicks Sep 14, 2025
f6973b2
fix: use single quotes in pr-summary workflow
alexanderlhicks Sep 14, 2025
9c6d89c
fix: use diff_url in pr-summary workflow
alexanderlhicks Sep 14, 2025
f0614ca
feat: adopt mathlib4 diff strategy for pr-summary
alexanderlhicks Sep 14, 2025
bdc8bed
fix: pass diff as env var in pr-summary workflow
alexanderlhicks Sep 14, 2025
108bc92
revert: use pull_request trigger
alexanderlhicks Sep 14, 2025
79f7b92
rebase
katyhr Sep 16, 2025
128cab2
Lambda_T
katyhr Sep 18, 2025
8dd6f89
weight function from Appendix A.2
Julek Sep 18, 2025
349e207
Simplification of weight definition
Julek Sep 18, 2025
f9ed102
wip
katyhr Sep 19, 2025
63a1db5
replace tilda with tilde + formalised homomorphism from ring of regul…
Julek Sep 19, 2025
b0edcb8
draft of everything but claim A_2
katyhr Sep 22, 2025
fb423cc
Defined Hensel lemma coefficients
Julek Sep 26, 2025
d56b6f9
latest wip
katyhr Sep 30, 2025
295d05b
Appendix A done?
Julek Sep 30, 2025
4efd576
minor edit to account for a new namespace
katyhr Oct 1, 2025
dcd9d90
namespace change
katyhr Oct 1, 2025
d097dae
added docstrings
katyhr Oct 1, 2025
64595c6
cleanup + docstrings
katyhr Oct 1, 2025
d5aa527
minor edit
katyhr Oct 1, 2025
7c88a9a
corrected build error
katyhr Oct 1, 2025
56cdbdc
corrections from rebase
katyhr Oct 1, 2025
9037a3d
ProximityGap file after rebase
ElijahVlasov Oct 1, 2025
296499b
WIP
ElijahVlasov Oct 1, 2025
7e29afc
WIP
ElijahVlasov Oct 1, 2025
e4ddcf7
Claim 5.8 composed
ElijahVlasov Oct 1, 2025
857b08d
5.9 ???
ElijahVlasov Oct 1, 2025
5cc7ce9
5.9 !!!
ElijahVlasov Oct 1, 2025
9fefb28
Lemma 5.10
ElijahVlasov Oct 1, 2025
c22e539
claim 5.11
ElijahVlasov Oct 1, 2025
7eabebf
cleanup and fix
Julek Oct 1, 2025
206b704
Cleanup of Bivariate
Julek Oct 1, 2025
624d489
discr_y
ElijahVlasov Oct 2, 2025
dab9518
First attempt at taming implicits
ElijahVlasov Oct 2, 2025
661b5f7
cleanup, reorder plus docstrings and updated intro
katyhr Oct 3, 2025
4717fae
updated intro and moved some defs/statements from bivariate
katyhr Oct 3, 2025
7f1d6ed
Some comments
ElijahVlasov Oct 9, 2025
46ce77b
Commentary
ElijahVlasov Oct 10, 2025
41d13ea
Merge remote-tracking branch 'public/main' into ElijahVlasov/section5
ElijahVlasov Oct 10, 2025
a7360b9
Post-merge fixes
ElijahVlasov Oct 10, 2025
4ac8cd1
Post merge fixes
ElijahVlasov Oct 13, 2025
ace83dd
Remove stale stuff
ElijahVlasov Oct 13, 2025
3fa7fe5
make sure Finite -> Fintype is noncomputable, remove sorries, clean u…
Ferinko Oct 13, 2025
8b592ff
cleanup proximitygap.lean
Ferinko Oct 14, 2025
1e60977
add [Finite F] to eq_5_12 and lemma_5_6; cleanup review artefacts,
Ferinko Oct 14, 2025
3c9c480
WIP - fixmeup; degreeX_mul
Ferinko Oct 14, 2025
125a8aa
WIP - fixup later; towards a sane proof
Ferinko Oct 15, 2025
b2b5d51
some changes
quangvdao Oct 21, 2025
6504834
bug fix
quangvdao Oct 21, 2025
d72488a
Merge branch 'main' into ElijahVlasov/section5
quangvdao Oct 21, 2025
80856ed
Merge branch 'ElijahVlasov/section5' of https://github.com/Nethermind…
quangvdao Oct 21, 2025
88db08a
Polynomial.Bivariate
ElijahVlasov Oct 27, 2025
9ba0b15
Merge remote-tracking branch 'origin/ElijahVlasov/section5' into Elij…
ElijahVlasov Oct 27, 2025
85f9aa1
Separable
ElijahVlasov Oct 27, 2025
9b54a14
opaque -> def
ElijahVlasov Oct 27, 2025
0bbb873
Fix typo
ElijahVlasov Oct 27, 2025
c619f77
CommRing -> Field
ElijahVlasov Oct 27, 2025
d6786e9
Section 6 of Proximity Gaps
ElijahVlasov Aug 25, 2025
07336b1
Section 7
ElijahVlasov Aug 25, 2025
818f05c
WIP review section 6
Julek Oct 29, 2025
e6d3fd9
WIP 6.3 - almost done
Ferinko Oct 29, 2025
f993a35
WIP - 6.3 (done?)
Ferinko Oct 29, 2025
2b7b751
WIP - review 7.1
Ferinko Oct 30, 2025
2996cfc
WIP - review 7.2
Ferinko Oct 30, 2025
966724e
WIP - theorem 7.3
Ferinko Oct 30, 2025
46daf7c
WIP - 7.4 is in progress
Ferinko Oct 30, 2025
1fa2e8b
WIP - 7.4 finished
Ferinko Oct 31, 2025
9cc8867
- ensure all Rs \ge 0
Ferinko Oct 31, 2025
149b144
WIP - 7.6
Ferinko Oct 31, 2025
3c1bbf4
review section 7
Julek Oct 31, 2025
929d508
Fixed typeclass issue
Julek Nov 1, 2025
204f87b
WIP
ElijahVlasov Nov 5, 2025
8a63dd6
Renaming
ElijahVlasov Nov 5, 2025
b82874b
WIP
ElijahVlasov Nov 6, 2025
48a94ab
Merge remote-tracking branch 'public/main' into ElijahVlasov/section7_r
ElijahVlasov Nov 6, 2025
1df5178
Section 6 docstrings
ElijahVlasov Nov 7, 2025
fafccbd
Docstrings for section 7.
ElijahVlasov Nov 7, 2025
d6dfe42
Fix to mu_set + better docstrings for 6.3, 7.5 and 7.6
Julek Nov 15, 2025
9a5fd25
Added Fintype proof for coeffs_of_close_proximity_curve
Julek Nov 15, 2025
a006d5d
WIP
ElijahVlasov Oct 13, 2025
62b9739
Claim 8.1
ElijahVlasov Oct 14, 2025
11f54ff
WIP
ElijahVlasov Oct 15, 2025
08c9fb8
WIP
ElijahVlasov Oct 16, 2025
8de5a8b
WIP
ElijahVlasov Oct 17, 2025
e71ae9b
WIP
Julek Oct 17, 2025
1aa1f63
WIP
Julek Nov 4, 2025
eb53efd
WIP
Julek Nov 6, 2025
c5bd31b
8.2 done?
Julek Nov 6, 2025
e8274ef
Initial 8.1 cleanup
Julek Nov 6, 2025
d943d60
fix of 8.1 to use CosetDomain instead of Domain
Julek Nov 6, 2025
726f922
A bit more cleanup of 8.2
Julek Nov 6, 2025
08ec251
8.1 WIP
Julek Nov 15, 2025
9828dbf
sum_add_one made trivial
Ferinko Nov 17, 2025
e745507
sum_add_one
Ferinko Nov 17, 2025
38f3714
first pass on 8.x
Ferinko Nov 17, 2025
d47c820
cleanup Soundness, SingleRound and Basic
Ferinko Nov 18, 2025
39e68ac
pow_inj now uses pow_inj_mod
Ferinko Nov 19, 2025
74bfbad
D_def is now simple
Ferinko Nov 19, 2025
51ec87a
cleanup the instance issues, document what's happening
Ferinko Nov 20, 2025
1fc8d7f
the first version of reconcile
Ferinko Nov 21, 2025
b86f532
fix aesop_reconcile, now does not need arguments
Ferinko Nov 21, 2025
fd73b06
Closing 8.1 WIP
Julek Nov 24, 2025
52c618d
fix aesop_reconcile; generalise over the group
Ferinko Nov 24, 2025
eff7de0
Completed body of proof in body of f_succ'
Julek Nov 24, 2025
ffccee0
Merge branch 'Ferinko/ElijahVlasov/fri-soundness' of github.com:Nethe…
Julek Nov 24, 2025
785bb38
WIP
Julek Dec 4, 2025
53c4ff5
Completed 8.3 + simplification of cosets and FinType proof for domains
Julek Dec 9, 2025
2d29cdc
Completed proof of fin_equiv_coset
Julek Dec 9, 2025
c53e400
WIP
Julek Dec 9, 2025
265b6cb
Fixes and cleanup
Julek Dec 9, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions ArkLib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ import ArkLib.OracleReduction.Security.RoundByRound
import ArkLib.OracleReduction.Security.SpecialSoundness
import ArkLib.OracleReduction.Security.StateRestoration
import ArkLib.OracleReduction.VectorIOR
import ArkLib.ProofSystem.BatchedFri.Soundness
import ArkLib.ProofSystem.BatchedFri.Spec.General
import ArkLib.ProofSystem.BatchedFri.Spec.SingleRound
import ArkLib.ProofSystem.Binius.BinaryBasefold.Basic
Expand Down Expand Up @@ -191,6 +192,7 @@ import ArkLib.ToMathlib.Data.IndexedBinaryTree.Equiv
import ArkLib.ToMathlib.Data.IndexedBinaryTree.Lemmas
import ArkLib.ToMathlib.Finset.Basic
import ArkLib.ToMathlib.Finsupp.Fin
import ArkLib.ToMathlib.List.Basic
import ArkLib.ToMathlib.MvPolynomial.Equiv
import ArkLib.ToMathlib.NumberTheory.PrattCertificate
import ArkLib.ToMathlib.UInt.Equiv
Expand Down
Loading