Ferinko/elijah vlasov/johnson

.github/workflows/blueprint.yml

@@ -2,11 +2,10 @@ name: Compile blueprint
 
 on:
   push:
-    # branches:
-      # - main # Trigger on pushes to ANY branch now
+    branches: [main]
   workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
-  # pull_request:
-    # branches: [main]
+  pull_request:
+    branches: [main]
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
@@ -38,7 +37,7 @@ jobs:
 
       - name: check that all files are imported
         run: git diff --exit-code
-  
+
   build_project:
     runs-on: ubuntu-latest
     name: Build project
@@ -57,7 +56,6 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake build ArkLib
 
-
       - name: Build blueprint and copy to `home_page/blueprint`
         uses: xu-cheng/texlive-action@v2
         with:

.gitignore

@@ -19,3 +19,5 @@
 /blueprint/src/web.pdf
 
 .nvim.lua
+# Web files for local viewing
+/blueprint/web/

AUTHORS

@@ -5,4 +5,6 @@ Bolton Bailey
 Frantisek Silvasi
 Ilia Vlasov
 Julian Sutherland
-Chung Thai Nguyen
+Chung Thai Nguyen
+Poulami Das
+Mirco Richter

ArkLib.lean

@@ -5,15 +5,34 @@ import ArkLib.CommitmentScheme.MerkleTree
 import ArkLib.CommitmentScheme.SimpleRO
 import ArkLib.CommitmentScheme.Tensor
 import ArkLib.CommitmentScheme.Trivial
+import ArkLib.Data.Classes.DCast
+import ArkLib.Data.Classes.HasSize
+import ArkLib.Data.Classes.Initialize
+import ArkLib.Data.Classes.Serde
+import ArkLib.Data.Classes.Zeroize
 import ArkLib.Data.CodingTheory.Basic
-import ArkLib.Data.CodingTheory.JohnsonBound
+import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
+import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
+import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
+import ArkLib.Data.CodingTheory.BerlekampWelch.Existence
+import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
+import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
+import ArkLib.Data.CodingTheory.DivergenceOfSets
+import ArkLib.Data.CodingTheory.InterleavedCode
+import ArkLib.Data.CodingTheory.JohnsonBound.Basic
+import ArkLib.Data.CodingTheory.JohnsonBound.Choose2
+import ArkLib.Data.CodingTheory.JohnsonBound.Expectations
+import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas
+import ArkLib.Data.CodingTheory.ListDecodability
 import ArkLib.Data.CodingTheory.ProximityGap
 import ArkLib.Data.CodingTheory.ReedMuller
 import ArkLib.Data.CodingTheory.ReedSolomon
-import ArkLib.Data.CodingTheory
 import ArkLib.Data.EllipticCurve.BN254
-import ArkLib.Data.FieldTheory.BinaryTowerField.Basic
-import ArkLib.Data.FieldTheory.BinaryTowerField.Prelude
+import ArkLib.Data.FieldTheory.BinaryField.AdditiveNTT.NovelPolynomialBasis
+import ArkLib.Data.FieldTheory.BinaryField.AdditiveNTT.Prelude
+import ArkLib.Data.FieldTheory.BinaryField.Tower.Basic
+import ArkLib.Data.FieldTheory.BinaryField.Tower.Impl
+import ArkLib.Data.FieldTheory.BinaryField.Tower.Prelude
 import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_377
 import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_381
 import ArkLib.Data.FieldTheory.NonBinaryField.BN254
@@ -23,22 +42,32 @@ import ArkLib.Data.FieldTheory.NonBinaryField.Goldilocks
 import ArkLib.Data.FieldTheory.NonBinaryField.Mersenne
 import ArkLib.Data.FieldTheory.NonBinaryField.Secp256k1
 import ArkLib.Data.Fin.Basic
+import ArkLib.Data.Fin.Lift
+import ArkLib.Data.Fin.Pad
+import ArkLib.Data.Hash.DomainSep
+import ArkLib.Data.Hash.DuplexSponge
 import ArkLib.Data.Math.Basic
-import ArkLib.Data.Math.DepCast
 import ArkLib.Data.Math.HList
+import ArkLib.Data.Matrix.Basic
+import ArkLib.Data.Matrix.Sparse
 import ArkLib.Data.MlPoly.Basic
 import ArkLib.Data.MlPoly.Equiv
 import ArkLib.Data.MvPolynomial.Degrees
 import ArkLib.Data.MvPolynomial.Interpolation
+import ArkLib.Data.MvPolynomial.LinearMvExtension
 import ArkLib.Data.MvPolynomial.Multilinear
 import ArkLib.Data.MvPolynomial.Notation
 import ArkLib.Data.MvPolynomial.Sumcheck
 import ArkLib.Data.Polynomial.EvenAndOdd
+import ArkLib.Data.Polynomial.Interface
 import ArkLib.Data.Probability.Instances
 import ArkLib.Data.Probability.Notation
+import ArkLib.Data.Tree.Binary
+import ArkLib.Data.Tree.General
 import ArkLib.Data.UniPoly.Basic
 import ArkLib.Data.UniPoly.BasicOld
 import ArkLib.Data.UniPoly.PolynomialReflection
+import ArkLib.OracleReduction.BCS.Basic
 import ArkLib.OracleReduction.Basic
 import ArkLib.OracleReduction.Cast
 import ArkLib.OracleReduction.Composition.Parallel.Basic
@@ -47,15 +76,24 @@ import ArkLib.OracleReduction.Composition.Sequential.General
 import ArkLib.OracleReduction.Composition.Sequential.ProtocolSpec
 import ArkLib.OracleReduction.Equiv
 import ArkLib.OracleReduction.Execution
-import ArkLib.OracleReduction.LiftContext.Basic
+import ArkLib.OracleReduction.FiatShamir.Basic
+import ArkLib.OracleReduction.FiatShamir.DuplexSponge.State
+import ArkLib.OracleReduction.LiftContext.Lens
+import ArkLib.OracleReduction.LiftContext.OracleReduction
+import ArkLib.OracleReduction.LiftContext.Reduction
 import ArkLib.OracleReduction.OracleInterface
 import ArkLib.OracleReduction.Prelude
+import ArkLib.OracleReduction.ProtocolSpec
 import ArkLib.OracleReduction.Security.Basic
-import ArkLib.OracleReduction.Transform.BCS
-import ArkLib.OracleReduction.Transform.FiatShamir
+import ArkLib.OracleReduction.Security.Implications
+import ArkLib.OracleReduction.Security.Rewinding
+import ArkLib.OracleReduction.Security.RoundByRound
+import ArkLib.OracleReduction.Security.StateRestoration
 import ArkLib.OracleReduction.VectorIOR
-import ArkLib.ProofSystem.Component.CheckPred
+import ArkLib.ProofSystem.Component.CheckClaim
+import ArkLib.ProofSystem.Component.DoNothing
 import ArkLib.ProofSystem.Component.RandomQuery
+import ArkLib.ProofSystem.Component.ReduceClaim
 import ArkLib.ProofSystem.Component.SendClaim
 import ArkLib.ProofSystem.Component.SendWitness
 import ArkLib.ProofSystem.ConstraintSystem.IndexedLookup
@@ -65,12 +103,32 @@ import ArkLib.ProofSystem.DSL
 import ArkLib.ProofSystem.Fri.RoundConsistency
 import ArkLib.ProofSystem.Plonk.Basic
 import ArkLib.ProofSystem.Spartan.Basic
-import ArkLib.ProofSystem.Sumcheck.Basic
-import ArkLib.ProofSystem.Sumcheck.SingleRound
+import ArkLib.ProofSystem.Stir
+import ArkLib.ProofSystem.Stir.Combine
+import ArkLib.ProofSystem.Stir.Folding
+import ArkLib.ProofSystem.Stir.MainThm
+import ArkLib.ProofSystem.Stir.OutOfDomSmpl
+import ArkLib.ProofSystem.Stir.ProximityBound
+import ArkLib.ProofSystem.Stir.ProximityGap
+import ArkLib.ProofSystem.Stir.Quotienting
+import ArkLib.ProofSystem.Sumcheck.Impl.Basic
+import ArkLib.ProofSystem.Sumcheck.Spec.General
+import ArkLib.ProofSystem.Sumcheck.Spec.SingleRound
+import ArkLib.ProofSystem.Whir
+import ArkLib.ProofSystem.Whir.BlockRelDistance
+import ArkLib.ProofSystem.Whir.Folding
+import ArkLib.ProofSystem.Whir.GenMutualCorrAgreement
+import ArkLib.ProofSystem.Whir.MainThm
+import ArkLib.ProofSystem.Whir.OutofDomainSmpl
+import ArkLib.ProofSystem.Whir.ProximityGap
+import ArkLib.ProofSystem.Whir.ProximityGen
 import ArkLib.ToMathlib.BigOperators.Fin
 import ArkLib.ToMathlib.Finset.Basic
 import ArkLib.ToMathlib.Finsupp.Fin
 import ArkLib.ToMathlib.MvPolynomial.Equiv
 import ArkLib.ToMathlib.NumberTheory.PrattCertificate
 import ArkLib.ToMathlib.UInt.Equiv
+import ArkLib.ToVCVio.DistEq
+import ArkLib.ToVCVio.Lemmas
 import ArkLib.ToVCVio.Oracle
+import ArkLib.ToVCVio.SimOracle

ArkLib/CommitmentScheme/Basic.lean

@@ -29,39 +29,41 @@ namespace Commitment
 
 open OracleSpec OracleComp SubSpec
 
-variable {n : ℕ} {ι : Type}
+variable {ι : Type} (oSpec : OracleSpec ι) (Data Randomness Commitment : Type)
 
-structure Commit (oSpec : OracleSpec ι) (Data Randomness Commitment : Type) where
+structure Commit where
   commit : Data → Randomness → OracleComp oSpec Commitment
 
-structure Opening (pSpec : ProtocolSpec n) (oSpec : OracleSpec ι) (Data : Type)
-    [O : OracleInterface Data] (Randomness Commitment : Type) where
-  opening : Proof pSpec oSpec (Commitment × O.Query × O.Response) (Data × Randomness)
+variable [O : OracleInterface Data] {n : ℕ} (pSpec : ProtocolSpec n)
+
+structure Opening where
+  opening : Proof oSpec (Commitment × O.Query × O.Response) (Data × Randomness) pSpec
 
 -- abbrev Statement (Data Commitment : Type) [O : OracleInterface Data] :=
 --  Commitment × O.Query × O.Response
 
 -- abbrev Witness (Data Randomness : Type) := Data × Randomness
 
-structure Scheme (pSpec : ProtocolSpec n) (oSpec : OracleSpec ι) (Data : Type) [O : OracleInterface Data]
-    (Randomness Commitment : Type) extends
-      Commit oSpec Data Randomness Commitment,
-      Opening pSpec oSpec Data Randomness Commitment
+structure Scheme extends
+    Commit oSpec Data Randomness Commitment,
+    Opening oSpec Data Randomness Commitment pSpec
 
 section Security
 
 noncomputable section
 
 open scoped NNReal
 
-variable {pSpec : ProtocolSpec n} [∀ i, VCVCompatible (pSpec.Challenge i)] [DecidableEq ι]
-  {oSpec : OracleSpec ι} {Data : Type} [O : OracleInterface Data] {Randomness : Type} [Fintype Randomness]
-  {Commitment : Type} [oSpec.FiniteRange]
+variable [∀ i, VCVCompatible (pSpec.Challenge i)] [DecidableEq ι]
+  {oSpec : OracleSpec ι} {Data : Type} [O : OracleInterface Data] {Randomness : Type}
+  [Fintype Randomness]
+  {Commitment : Type} [oSpec.FiniteRange] {n : ℕ} {pSpec : ProtocolSpec n}
+  [∀ i, VCVCompatible (pSpec.Challenge i)]
 
 /-- A commitment scheme satisfies **correctness** with error `correctnessError` if for all
   `data : Data`, `randomness : Randomness`, and `query : O.Query`, the probability of accepting upon
   executing the commitment and opening procedures honestly is at least `1 - correctnessError`. -/
-def correctness (scheme : Scheme pSpec oSpec Data Randomness Commitment)
+def correctness (scheme : Scheme oSpec Data Randomness Commitment pSpec)
     (correctnessError : ℝ≥0) : Prop :=
   ∀ data : Data,
   ∀ randomness : Randomness,
@@ -72,14 +74,15 @@ def correctness (scheme : Scheme pSpec oSpec Data Randomness Commitment)
         return result] ≥ 1 - correctnessError
 
 /-- A commitment scheme satisfies **perfect correctness** if it satisfies correctness with no error.
-  -/
-def perfectCorrectness (scheme : Scheme pSpec oSpec Data Randomness Commitment) : Prop :=
+-/
+def perfectCorrectness (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop :=
   correctness scheme 0
 
 /-- An adversary in the (evaluation) binding game returns a commitment `cm`, a query `q`, two
   purported responses `r₁, r₂` to the query, and an auxiliary private state (to be passed to the
   malicious prover in the opening procedure). -/
-def BindingAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState : Type) [O : OracleInterface Data] :=
+def BindingAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState : Type)
+    [O : OracleInterface Data] :=
   OracleComp oSpec (Commitment × O.Query × O.Response × O.Response × AuxState)
 
 /-- A commitment scheme satisfies **(evaluation) binding** with error `bindingError` if for all
@@ -94,11 +97,11 @@ def BindingAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState : Type) [
 
   Informally, evaluation binding says that it's computationally infeasible to open a commitment to
   two different responses for the same query. -/
-def binding (scheme : Scheme pSpec oSpec Data Randomness Commitment)
+def binding (scheme : Scheme oSpec Data Randomness Commitment pSpec)
     (bindingError : ℝ≥0): Prop :=
   ∀ AuxState : Type,
   ∀ adversary : BindingAdversary oSpec Data Commitment AuxState,
-  ∀ prover : Prover pSpec oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit,
+  ∀ prover : Prover oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit pSpec,
     False
     -- [ fun ⟨x, x', b₁, b₂⟩ => x ≠ x' ∧ b₁ ∧ b₂ | do
     --     let result ← liftM adversary
@@ -133,12 +136,12 @@ def ExtractabilityAdversary (oSpec : OracleSpec ι) (Data Commitment AuxState :
   Informally, extractability says that if an adversary can convince the verifier to accept an
   opening, then the extractor must be able to recover some underlying data that is consistent with
   the evaluation query. -/
-def extractability (scheme : Scheme pSpec oSpec Data Randomness Commitment)
+def extractability (scheme : Scheme oSpec Data Randomness Commitment pSpec)
     (extractabilityError : ℝ≥0) : Prop :=
   ∃ extractor : StraightlineExtractor oSpec Data Commitment,
   ∀ AuxState : Type,
   ∀ adversary : ExtractabilityAdversary oSpec Data Commitment AuxState,
-  ∀ prover : Prover pSpec oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit,
+  ∀ prover : Prover oSpec (Commitment × O.Query × O.Response) AuxState Bool Unit pSpec,
     False
     -- [ fun ⟨b, d, q, r⟩ => b ∧ O.oracle d q = r | do
     --     let result ← liftM (simulate loggingOracle ∅ adversary)
@@ -156,7 +159,7 @@ def extractability (scheme : Scheme pSpec oSpec Data Randomness Commitment)
 /-- A commitment scheme satisfies **hiding** with error `hidingError` if ....
 
 Note: have to put it as `hiding'` because `hiding` is already used somewhere else. -/
-def hiding' (scheme : Scheme pSpec oSpec Data Randomness Commitment) : Prop := sorry
+def hiding' (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop := sorry
 
 #check seededOracle