Merge remote-tracking branch 'origin/Ferinko/ElijahVlasov/johnson' into ElijahVlasov/johnson

Author: ElijahVlasov

.gitignore

@@ -16,4 +16,6 @@
 
 # LaTeX PDF files for blueprint
 # *print.pdf
-/blueprint/src/web.pdf
+/blueprint/src/web.pdf
+
+.nvim.lua

.vscode/settings.json

@@ -0,0 +1,16 @@
+{
+    "editor.insertSpaces": true,
+    "editor.tabSize": 2,
+    "editor.rulers" : [100],
+    "editor.acceptSuggestionOnEnter": "smart",
+    "files.encoding": "utf8",
+    "files.eol": "\n",
+    "files.insertFinalNewline": true,
+    "files.trimFinalNewlines": true,
+    "files.trimTrailingWhitespace": true,
+    "git.ignoreLimitWarning": true,
+    "files.readonlyInclude": {
+      "**/.elan/**": true,
+      "**/.lake/**": true
+    }
+  }

ArkLib.lean

@@ -10,10 +10,10 @@ import ArkLib.Data.CodingTheory.JohnsonBound
 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.FFT
 import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_377
 import ArkLib.Data.FieldTheory.NonBinaryField.BLS12_381
 import ArkLib.Data.FieldTheory.NonBinaryField.BN254
@@ -23,9 +23,9 @@ 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.Math.Fin
+import ArkLib.Data.Math.Basic
+import ArkLib.Data.Math.DepCast
 import ArkLib.Data.Math.HList
-import ArkLib.Data.Math.Operations
 import ArkLib.Data.MlPoly.Basic
 import ArkLib.Data.MlPoly.Equiv
 import ArkLib.Data.MvPolynomial.Degrees
@@ -40,15 +40,24 @@ import ArkLib.Data.UniPoly.Basic
 import ArkLib.Data.UniPoly.BasicOld
 import ArkLib.Data.UniPoly.PolynomialReflection
 import ArkLib.OracleReduction.Basic
-import ArkLib.OracleReduction.Composition.Sequential
-import ArkLib.OracleReduction.Composition.Virtual
+import ArkLib.OracleReduction.Cast
+import ArkLib.OracleReduction.Composition.Parallel.Basic
+import ArkLib.OracleReduction.Composition.Sequential.Append
+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.OracleInterface
 import ArkLib.OracleReduction.Prelude
 import ArkLib.OracleReduction.Security.Basic
+import ArkLib.OracleReduction.Transform.BCS
+import ArkLib.OracleReduction.Transform.FiatShamir
 import ArkLib.OracleReduction.VectorIOR
-import ArkLib.ProofSystem.Components
+import ArkLib.ProofSystem.Component.CheckPred
+import ArkLib.ProofSystem.Component.RandomQuery
+import ArkLib.ProofSystem.Component.SendClaim
+import ArkLib.ProofSystem.Component.SendWitness
 import ArkLib.ProofSystem.ConstraintSystem.IndexedLookup
 import ArkLib.ProofSystem.ConstraintSystem.Plonk
 import ArkLib.ProofSystem.ConstraintSystem.R1CS
@@ -57,11 +66,11 @@ 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.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.Oracle
-import ArkLib.Transform.BCS
-import ArkLib.Transform.FiatShamir

ArkLib/CommitmentScheme/Fold.lean

@@ -14,6 +14,9 @@ import ArkLib.Data.CodingTheory.ProximityGap
 /-!
   # Folding-based Polynomial Commitment Schemes
 
+  NOTE: this file should be deprecated now in favor of newer developments on FRI/STIR/WHIR in
+  `ProofSystem`
+
   We define the folding IOP underlying polynomial commitment schemes such as FRI, Circle-FRI,
   BaseFold, FRI-Binius, and so on.
 
@@ -75,13 +78,13 @@ instance : IsSingleRound (pSpec R n) where
 /-- Recognize that the (only) message from the prover to the verifier has type `Vector R (2 ^ n)`,
   and hence can be turned into an oracle for evaluating the polynomial -/
 instance instOracleInterfaceMessagePSpec : OracleInterface ((pSpec R n).Message default) := by
-  simp only [pSpec, default, Matrix.cons_val_zero, Message, getType]
+  simp [pSpec, default, Message, getType]
   exact instOracleInterfaceVector
 
 /-- Recognize that the challenge from the verifier to the prover has type `R`, and hence can be
   sampled uniformly at random -/
 instance instSampleableChallengePSpec : Sampleable ((pSpec R n).Challenge default) := by
-  simp only [pSpec, default, Matrix.cons_val_one, Matrix.head_cons, Challenge, getType]
+  simp [Challenge, pSpec, default]
   infer_instance
 
 structure PrvState (k : Fin n) where

ArkLib/CommitmentScheme/MerkleTree.lean

@@ -5,7 +5,7 @@ Authors: Quang Dao
 -/
 
 import VCVio
-import ArkLib.Data.Math.Operations
+import ArkLib.Data.Math.Basic
 import ArkLib.CommitmentScheme.Basic
 import Mathlib.Data.Vector.Snoc
 
@@ -181,72 +181,112 @@ def verifyProof {n : ℕ} (i : Fin (2 ^ n)) (leaf : α) (root : α) (proof : Lis
   let putative_root ← getPutativeRoot α i leaf proof
   guard (putative_root = root)
 
--- Belongs in VCVio, not sure if its already there somewhwere
-def implement_with_function (hash : α × α -> α) : QueryImpl (spec α) (StateT Unit (OracleComp (emptySpec))) where
-  impl q := match q with
-    | ⟨_, ⟨left, right⟩⟩ =>
-        do
-          let out := hash (left, right)
-          return out
 
+theorem buildLayer_neverFails (α : Type) [inst : DecidableEq α] [inst_1 : SelectableType α]
+    (preexisting_cache : (spec α).QueryCache) (n : ℕ)
+    (leaves : List.Vector α (2 ^ (n + 1))) :
+    ((simulateQ randomOracle (buildLayer α n leaves)).run preexisting_cache).neverFails := by
+  simp_rw [buildLayer]
+  simp [neverFails_query_bind]
+  -- I now require a "neverFails_mmap_iff" lemma, but I don't see one in VCVio.
+  -- Feels like evidence for avoiding Vector-based merkle trees in favor of inductive-based ones.
+  sorry
+
+/--
+Building a Merkle tree never results in failure
+(no matter what queries have already been made to the oracle before it runs).
+-/
+theorem buildMerkleTree_neverFails (α : Type) [DecidableEq α] [SelectableType α] {n : ℕ}
+    (leaves : List.Vector α (2 ^ n)) (preexisting_cache : (spec α).QueryCache) :
+    ((simulateQ randomOracle (buildMerkleTree α n leaves)).run preexisting_cache).neverFails := by
+  -- It feels like there should be some kind of tactic that inspects the structure of the
+  -- `buildMerkleTree` definition to see that it never even mentions failure,
+  -- and therefore can't fail.
+  induction n generalizing preexisting_cache with
+  | zero =>
+    simp [buildMerkleTree, getRoot, generateProof, verifyProof, getPutativeRoot]
+  | succ n ih =>
+    simp [buildMerkleTree, neverFails_bind_iff]
+    constructor
+    · exact buildLayer_neverFails α preexisting_cache n leaves
+    · intro next_leaves next_cache h_mem_support
+      apply ih
 
 /-- Completeness theorem for Merkle trees: for any full binary tree with `2 ^ n` leaves, and for any
-  index `i`, the verifier accepts the opening proof at index `i` generated by the prover. -/
-theorem completeness {n : ℕ} (leaves : List.Vector α (2 ^ n)) (i : Fin (2 ^ n)) (hash : α × α -> α) :
-    ((do
+  index `i`, the verifier accepts the opening proof at index `i` generated by the prover.
+-/
+theorem completeness [SelectableType α] {n : ℕ}
+    (leaves : List.Vector α (2 ^ n)) (i : Fin (2 ^ n)) (hash : α × α -> α)
+    (preexisting_cache : (spec α).QueryCache) :
+    (((do
       let cache ← buildMerkleTree α n leaves
       let proof := generateProof α i cache
       let verif ← verifyProof α i leaves[i] (getRoot α cache) proof).simulateQ
-      (implement_with_function α hash)
-      ()).neverFails := by
-  induction n with
-  | zero =>
-    simp [buildMerkleTree, getRoot, generateProof, verifyProof, getPutativeRoot]
-    have : i = 0 := by aesop
-    subst i
-    simp [Fin.instGetElemFinVal]
-    -- TODO: the below is not necessary once `neverFails` lemmas are (re-)added
-    unfold neverFails neverFailsWhen allWhen OracleComp.construct FreeMonad.construct
-    simp [pure, StateT.pure, OptionT.pure, OptionT.mk]
-  | succ n ih =>
-    -- simp_all [Fin.getElem_fin, Vector.getElem_eq_get, Fin.eta, getRoot, Fin.val_zero,
-    --   Nat.pow_zero, Fin.zero_eta, Vector.get_zero, bind_pure_comp, id_map', probFailure_eq_zero_iff,
-    --   neverFails_bind_iff, buildMerkleTree, generateProof, LawfulMonad.bind_assoc, bind_map_left,
-    --   Cache.upper_cons, Cache.leaves_cons]
-    -- refine ⟨?_, ?_⟩
-    -- ·
-      simp [buildLayer, simulateQ, simulateQ, implement_with_function]
-      sorry
-
-    -- · intro newLeaves h_newLeaves
-    --   let i' : Fin (2 ^ n) := i.val / 2
-    --   specialize ih newLeaves i'
-    --   rcases ih with ⟨ih', ih⟩
-    --   sorry
-      -- refine ⟨?_, ?_⟩
-      -- · exact ih'
-      -- · intro cache h_cache
-      --   specialize ih cache h_cache
-      --   unfold verifyProof
-      --   simp only [guard_eq, neverFails_bind_iff]
-      --   unfold verifyProof at ih
-      --   simp only [guard_eq, neverFails_bind_iff] at ih
-      --   rcases ih with ⟨ih_getroot, ih_cmp⟩
-      --   refine ⟨?_, ?_⟩
-      --   · -- I think this just needs a simple lemma about `getPutativeRoot`
-      --     sorry
-      --   · intro root h_root
-      --     specialize ih_cmp root
-      --     have : root ∈ (getPutativeRoot α i'
-      --                     (newLeaves.get i') (generateProof α i' cache)).support := by
-
-      --       sorry
-      --     specialize ih_cmp this
-      --     simp [apply_ite] at ih_cmp
-      --     rw [ih_cmp]
-      --     simp [apply_ite]
-      --     simp [Cache.cons]
-      --     sorry
+      (randomOracle)).run preexisting_cache).neverFails := by
+  simp [neverFails_bind_iff]
+  constructor
+  · -- buildMerkleTree never fails
+    exact buildMerkleTree_neverFails α leaves preexisting_cache
+  · -- verifyProof never fails on the output of generateProof after buildMerkleTree
+    intros merkle_tree_cache query_cache h_mem_support
+    -- Need a theorem to characterize
+    -- `((simulateQ randomOracle (buildMerkleTree α n leaves)).run preexisting_cache).support`
+    -- i.e.
+    --  - All merkle_tree_cache parent-child relationships are in the query_cache
+    --  - Everything in the preexisting_cache is in the query_cache
+    --  - Nothing else is in the query_cache
+    sorry
+
+
+
+
+
+
+--   induction n with
+--   | zero =>
+--     simp [buildMerkleTree, getRoot, generateProof, verifyProof, getPutativeRoot]
+--     have : i = 0 := by aesop
+--     subst i
+--     simp [Fin.instGetElemFinVal]
+--   | succ n ih =>
+--     -- simp_all [Fin.getElem_fin, Vector.getElem_eq_get, Fin.eta, getRoot, Fin.val_zero,
+--     --   Nat.pow_zero, Fin.zero_eta, Vector.get_zero, bind_pure_comp, id_map', probFailure_eq_zero_iff,
+--     --   neverFails_bind_iff, buildMerkleTree, generateProof, LawfulMonad.bind_assoc, bind_map_left,
+--     --   Cache.upper_cons, Cache.leaves_cons]
+--     -- refine ⟨?_, ?_⟩
+--     -- ·
+--     simp [buildLayer, simulateQ, simulateQ, implement_with_function]
+--     sorry
+
+--     -- · intro newLeaves h_newLeaves
+--     --   let i' : Fin (2 ^ n) := i.val / 2
+--     --   specialize ih newLeaves i'
+--     --   rcases ih with ⟨ih', ih⟩
+--     --   sorry
+--       -- refine ⟨?_, ?_⟩
+--       -- · exact ih'
+--       -- · intro cache h_cache
+--       --   specialize ih cache h_cache
+--       --   unfold verifyProof
+--       --   simp only [guard_eq, neverFails_bind_iff]
+--       --   unfold verifyProof at ih
+--       --   simp only [guard_eq, neverFails_bind_iff] at ih
+--       --   rcases ih with ⟨ih_getroot, ih_cmp⟩
+--       --   refine ⟨?_, ?_⟩
+--       --   · -- I think this just needs a simple lemma about `getPutativeRoot`
+--       --     sorry
+--       --   · intro root h_root
+--       --     specialize ih_cmp root
+--       --     have : root ∈ (getPutativeRoot α i'
+--       --                     (newLeaves.get i') (generateProof α i' cache)).support := by
+
+--       --       sorry
+--       --     specialize ih_cmp this
+--       --     simp [apply_ite] at ih_cmp
+--       --     rw [ih_cmp]
+--       --     simp [apply_ite]
+--       --     simp [Cache.cons]
+--       --     sorry
 
 
 -- theorem soundness (i : Fin (2 ^ n)) (leaf : α) (proof : Vector α n) :

ArkLib/Data/CodingTheory.lean

@@ -0,0 +1,11 @@
+import ArkLib.Data.CodingTheory.Basic
+import ArkLib.Data.CodingTheory.BerlekampWelch
+import ArkLib.Data.CodingTheory.BivariatePoly
+import ArkLib.Data.CodingTheory.DivergenceOfSets
+import ArkLib.Data.CodingTheory.InterleavedCode
+import ArkLib.Data.CodingTheory.ListDecodability
+import ArkLib.Data.CodingTheory.Prelims
+import ArkLib.Data.CodingTheory.ProximityGap
+import ArkLib.Data.CodingTheory.PolishchukSpielman
+import ArkLib.Data.CodingTheory.ReedMuller
+import ArkLib.Data.CodingTheory.ReedSolomon