Ferinko/elijah vlasov/johnson #27
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Ferinko/bw cleanups
existence proofs and imports; cleanup variables
* more on `SendWitness` * more on `SendWitness` * progress on `SendSingleWitness` and `CheckPred` * more on `CheckPred` * define equivalence for general composition * rename `CheckPred` => `CheckClaim` * new product instances for `OracleInterface`, refactor `SendWitness` * initial def of knowledge state function * add `ReduceClaim` * add `DoNothing` reduction * add TODOs for `OracleInterface` * add `ReduceClaim` * update import * minor changes
…d-zkEVM#57) * tentative new definition for rbr knowledge soundness * start revamping IOR defs in blueprint * start revamping the blueprint for IORs * some fixes * fixed mathbbm error in web version * ported over execution & composition semantics * add security defs & simple oracle reductions * ignore `web` folder in blueprint * more blueprint progress, removed `web` folder * remove `web.pdf` * added more \uses links * updated spartan description
Linear, Interleaved and Reed-Solomon codes + Berlekamp-welch.
…fied-zkEVM#58) * refactor `simulateQ'` and `distEq` for oracle comp * refactor transport lens to another file, defined "right" condition for KS * making progres on lens in oracle setting * start writing special cases of lenses * more lens defs * update imports * fix build, added TODOs for equiv * fix broken decl in blueprint * fix imports
…ports fix global import mathlib
…or `OracleInterface` (Verified-zkEVM#60) * introduce more Sum notation, add `MessagesUpTo` * refactor sum-check files * universe polymorphism for `OracleInterface` * add `OracleReduction` defs for lifting (oracle) context * update imports, more progress on single-round sum-check * finish setting up lenses for single round * defined full sum-check using sequential composition * fix broken build
* feat: concrete binary tower fields * rename file * simpler rw occs * fix import --------- Co-authored-by: Quang Dao <[email protected]>
* IOPP def version 1 * tools for stir * STIR tools + main thms - version1 * resolve merge conflict * tools for stir * STIR tools + main thms - version1 * adding whir repo * adding whir repo * resolve merge conflict * tools for stir * STIR tools + main thms - version1 * coding theory updates * added files from NM * removed Codingtheory folder from Whir * moved Coding theory files * FieldRSC, SmoothDom, MockListdecode * SmoothDom, SmoothRSC, linearMVextension * SmoothDom, SmoothRSC, linearMVextension * SmoothDom, SmoothRSC, linearMVextension * SmoothDom, SmoothRSC, linearMVextension * Smooth RSC * updated Combine with new RSC defs * removed files * updated Folding * updated Combine * updates to quotienting and folding * Update CODES * updated list-decodeability with general type* * ConstraintCodes 1 * PowerDomain and PowDomainFiber as Embeddings * PowerDomain and PowDomainFiber as Embeddings * PowerDomain and PowDomainFiber as Embeddings * PowerDomain and PowDomainFiber as Embeddings * ConstraintCodes * ConstraintCodes * ConstraintCodes * ConstraintCodes * ConstraintCodes * MultiConstraintCodes * Started WHIR folder * updates to STIR Lemmas * probability notation * updated stir lemmas * proximity gap WHIR version * new rate * new rate * new rate * updated lemmas and mainthms in stir * updated all lemmas in stir * edits on stir main thm * edits on stir main thm * stir updates * Proximity Generator + RSC Proximity Generatr * ConstraintRSC Test * main thm whir - work in progress * updated out of domain lemma, stir * updates to stir * stir updates * refine stir updates to match stir PR * refine stir updates to match stir PR * refine stir updates to match stir PR * minor: stir edit * minor: stir edit * minor: stir edit * commented unused def and added notes * ConstraintRSC some comments and renaming * formalization of mutual corr agreement * formalization of mutual corr agreement * update to conjecture 4.12, lemma 4.13 and folding * update basics from ArkLib * IC codes * testing notation * whir lemmas * prob notation * minor * added comments to lemmas * defs 4.16 - 4.18 about relative distance * defs 4.16 - 4.18 about relative distance * distance lemmas complete * stir PR preparation * out domain sampling lemmas in progress * out of domain sampling lemmas first version * updates to whir * updates to whir * update * whir lemmas * folding * block dist refine * whir main thm * whir main thm * refine coding theory defs * update mvlinearextension * audit in progress * comments in whir * added comments * auditing code * auditing code * whir up to date * whir up to date * whir up to date * whir up to date * whir up to date * updated comments * stir updates - generic \io, commented code, audit pass * minor import updates * minor import updates * resolved import conflicts, adjusted type, audited code * resolved import conflicts, adjusted type, audited code * resolved import conflicts, adjusted type, audited code * merged definitions of ReedSolomon codes and adjusted imports * added proximity gap thm in stir as well * minor * updates to the main thm * audited stir code * audited whir code * comments * minor * naming * minor * minor --------- Co-authored-by: PlanetMacro <[email protected]>
* small updates * delete comments in security/basic
Co-authored-by: Julian Sutherland <[email protected]> Co-authored-by: Quang Dao <[email protected]>
* cleanup BW condition * fix buggy aesop invocation * removed a private lemma --------- Co-authored-by: Katy Hristova <[email protected]>
* add general tree with arbitrary arities * refactor binary trees to another file * update imports
* refactor BCS & Fiat-Shamir files * update imports * update main theorem of STIR
* fix found during audit * added authors * cleanups * minor * minor * adjusted the index of folding parameter in main thm Co-authored-by: Miguel Quaresma<[email protected]>
* added blueprinting tex for stir * blueprint stir * whir blueprint * stir/whir tex * progress on blueprint * full version of blueprint * full version of blueprint * fix import decls * fix plastex related issued * fix plastex related issued
* re-org R1CS, define padding * starting to overhaul Spartan * refactor `Fin` and `Matrix` files, more progress on Spartan * added skeleton for Spartan * update imports
* refactor instances for ProtocolSpec * refactor protocol spec messages & challenges * define (slow) Fiat-Shamir transform * update import * add Fiat-Shamir to blueprint
* update lean_decls * define API for `DuplexSponge` * update import * add description for unimplemented instance
…M#75) * update linter options to match mathlib * init new files * update imports * update new docstring lint * flesh out serde and codec * initial translation of domain separators * update state for duplex sponge prover & verifier * update import * fix new linter errors * name change for FS state
* refactor Q to Q>=0, fix proofs * relHamming dist proofs * minor cleanup * more cleanups * another minor cleanup * fix dist -> minDist in singletonBound * final minor cleanups * minor fix --------- Co-authored-by: Frantisek Silvasi <[email protected]>
Collaborator
|
LGTM! |
* feat: blueprint for binary tower fields * feat: novel polynomial basis --------- Co-authored-by: Quang Dao <[email protected]>
…fied-zkEVM#78) * WIP commit * refactor up to `Security/Basic.lean` * more changes * refactor soundness files * changing composition * update lens special case definitions * more progress on sequential composition & other changes * refactor classes & defining more casts * finish casting up to reduction * fixing lens again (hopefully for final time) * error-free lens for now * more refactor of extractor lens * done with lens (for now) * done fixing component reductions * more error fixes * fix STIR and WHIR main theorem statement * fix workflow trigger * rest of the errors (hopefully) * final changes * another fix * fix blueprint decls
* initial bump * starting to fix errors * more fixes * more fixes * fixing linter errors
Ferinko
force-pushed
the
Ferinko/ElijahVlasov/johnson
branch
from
eff46ab to
7f62c24
Compare
Ferinko
force-pushed
the
Ferinko/ElijahVlasov/johnson
branch
2 times, most recently
from
1ec9dbd to
58d757d
Compare
Ferinko
force-pushed
the
Ferinko/ElijahVlasov/johnson
branch
from
58d757d to
c07c998
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.