Merge branch 'main' into tr/ring-switching-subprotocol

Author: tobias-rothmann

.github/workflows/ci.yml

@@ -85,7 +85,7 @@ jobs:
             ${{ runner.os }}-lean-docs-${{ hashFiles('lake-manifest.json') }}
             ${{ runner.os }}-lean-docs-
 
-      - uses: actions/setup-python@v6
+      - uses: actions/setup-python@v7
         with:
           python-version: "3.12"
 

.github/workflows/docs-integrity.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v7
-      - uses: actions/setup-python@v6
+      - uses: actions/setup-python@v7
         with:
           python-version: "3.12"
       - name: Check docs integrity

.github/workflows/kb-generated.yml

@@ -30,7 +30,7 @@ jobs:
           fetch-depth: 0
           token: ${{ secrets.GITHUB_TOKEN }}
 
-      - uses: actions/setup-python@v6
+      - uses: actions/setup-python@v7
         with:
           python-version: "3.12"
 

ArkLib.lean

@@ -83,6 +83,7 @@ import ArkLib.Data.CodingTheory.PolishchukSpielman.Resultant
 import ArkLib.Data.CodingTheory.Prelims
 import ArkLib.Data.CodingTheory.ProximityGap.AHIV22
 import ArkLib.Data.CodingTheory.ProximityGap.AHIV22Support
+import ArkLib.Data.CodingTheory.ProximityGap.AffineGenerator
 import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.BWMatrix
 import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.GoodCoeffs
 import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AffineLines.JointAgreement
@@ -228,6 +229,7 @@ import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.ScalarRoun
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.SeqCompose
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.SingleRound
 import ArkLib.OracleReduction.Security.Implications
+import ArkLib.OracleReduction.Security.RbrGame
 import ArkLib.OracleReduction.Security.Rewinding
 import ArkLib.OracleReduction.Security.RoundByRound
 import ArkLib.OracleReduction.Security.SpecialSoundness
@@ -308,6 +310,6 @@ import ArkLib.ToVCVio.EvalDist.Defs.Support
 import ArkLib.ToVCVio.EvalDist.Instances.OptionT
 import ArkLib.ToVCVio.OracleComp.Coercions.SubSpec
 import ArkLib.ToVCVio.OracleComp.EvalDist
+import ArkLib.ToVCVio.OracleComp.QueryTracking.LoggingOracle
 import ArkLib.ToVCVio.OracleComp.SimSemantics.SimulateQ
-import ArkLib.ToVCVio.ToMathlib.Control.StateT
 import ArkLib.ToVCVio.ToMathlib.Data.Vector.Basic

ArkLib/Commitments/Functional/KZG/Binding.lean

@@ -352,7 +352,7 @@ lemma binding_game_ext_eq_binding_game {n : ℕ} {AuxState : Type} [SampleableTy
           = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
               <$> (simulateQ randomOracle (Groups.sampleNonzeroZMod (p := p))).run' ∅ := by
-            rw [← StateT.run'_map_comm, ← simulateQ_map]
+            rw [← StateT.run'_map', ← simulateQ_map]
             rfl
       _ = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
@@ -417,8 +417,8 @@ lemma binding_game_ext_eq_binding_game {n : ℕ} {AuxState : Type} [SampleableTy
         (f := id) (post := fun _ => proj)
         (hBody := by
           intro τ
-          rw [← StateT.run'_map_comm (Option.map id),
-            ← StateT.run'_map_comm (Option.map proj)]
+          rw [← StateT.run'_map' (f := Option.map id),
+            ← StateT.run'_map' (f := Option.map proj)]
           apply congrArg (fun mx : StateT unifSpec.QueryCache ProbComp
             (Option (BindingOutput (p := p) n)) => mx.run' ∅)
           dsimp only [bodyBase, bodyExt]

ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean

@@ -241,7 +241,7 @@ lemma function_binding_game_ext_eq_function_binding_game {n L : ℕ} {AuxState :
           = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
               <$> (simulateQ randomOracle (Groups.sampleNonzeroZMod (p := p))).run' ∅ := by
-            rw [← StateT.run'_map_comm, ← simulateQ_map]
+            rw [← StateT.run'_map', ← simulateQ_map]
             rfl
       _ = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
@@ -251,7 +251,7 @@ lemma function_binding_game_ext_eq_function_binding_game {n L : ℕ} {AuxState :
   simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp]
   congr 1
   funext τ
-  rw [← map_eq_bind_pure_comp, ← StateT.run'_map_comm, ← simulateQ_map]
+  rw [← map_eq_bind_pure_comp, ← StateT.run'_map', ← simulateQ_map]
   simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp]
   congr 1
   funext x

ArkLib/Data/CodingTheory/Basic/LinearCode.lean

@@ -255,22 +255,29 @@ scoped macro_rules
 
 /-- Let `c` be a word of length `ι`. For every finite `ι`-subset `T` , we define the projection of a
 word `c` to `T` as the word obtained by restricting the indexing set of `c` to `T`.
-We denote this by `c|[T]`.
 Definition 3.7 [BCGM25]. -/
 def projectedWord (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
 
-notation:60 c "|[" T "]" => projectedWord c T
-
 /-- Let `C` be a code of length `ι`. For every finite `ι`-subset `T`, we define the projected code
-`C|[T]` as the set of projected codewords `c|[T]`, for `c ∈ C`.
+as the set of projected codewords.
 Definition 3.7 [BCGM25]. -/
 def projectedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
-  {w | ∃ c ∈ C, w = c|[T]}
+  {w | ∃ c ∈ C, w = projectedWord c T}
+
+open Submodule
+
+/-- The projected code of a linear code, as a submodule of `T → F`.
+Definition 3.7 [BCGM25]. -/
+def projectedCodeSubmod [Field F] (LC : LinearCode ι F) (T : Finset ι) :
+    Submodule F (T → F) := LC.map (LinearMap.funLeft F F (Subtype.val : T → ι))
 
-notation:60 C "|[" T "]" => projectedCode C T
+/-- Membership in `projectedCodeSubmod` is membership in `projectedCode` of the underlying set. -/
+lemma mem_projectedCodeSubmod_iff [Field F] (LC : LinearCode ι F) (T : Finset ι)
+    (w : T → F) : w ∈ projectedCodeSubmod LC T ↔ w ∈ projectedCode LC.carrier T :=
+  Submodule.mem_map.trans <| exists_congr fun _ => and_congr_right fun _ => eq_comm
 
-/-- Let `T` be a finite subset of `ι`. If every word in a collection lies in the projected code
-`C|[T]`, then so do all `F`-linear combinations of these. -/
+/-- Let `T` be a finite subset of `ι`. If every word in a collection lies in the projected code,
+then so do all `F`-linear combinations of these. -/
 lemma projectedCode_linearCombination [Field F] (LC : LinearCode ι F) (T : Finset ι) {α : Type}
     [Fintype α] (U : α → (ι → F)) (c : α → F)
     (hU : ∀ j, projectedWord (U j) T ∈ projectedCode LC.carrier T) :

ArkLib/Data/CodingTheory/Prelims.lean

@@ -10,6 +10,7 @@ import Mathlib.LinearAlgebra.AffineSpace.Pointwise
 import Mathlib.LinearAlgebra.AffineSpace.Combination
 import Mathlib.RingTheory.Henselian
 
+
 /-! # Coding-Theory Preliminaries -/
 
 section TensorCombination
@@ -34,6 +35,7 @@ def multilinearCombine {ϑ : ℕ} {ι : Type*}
     (u : (Fin (2 ^ ϑ)) → ι → A) (r : Fin ϑ → F) : (ι → A) :=
   fun colIdx => ∑ rowIdx : Fin (2^ϑ), ((multilinearWeight r rowIdx) : F) • ((u rowIdx colIdx) : A)
 notation:20 r " |⨂| " u => multilinearCombine (u := u) (r := r)
+
 end TensorCombination
 noncomputable section
 
@@ -297,6 +299,29 @@ instance instNonemptyAffineSubspace_mk' {V : Type*} [AddCommGroup V] [Module F V
     (p : V) (direction : Submodule F V) : Nonempty (AffineSubspace.mk' p direction) :=
   nonempty_subtype.mpr ⟨p, AffineSubspace.self_mem_mk' p direction⟩
 
+/-- The affine-space combination of codewords `U` at seed `x`:
+`U 0 + ∑ i, x i • U (i+1)`, i.e. `vecMul (1, x) U`. -/
+abbrev affineComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) : ι → F :=
+  Matrix.vecMul (Fin.cons 1 x) U
+
+/-- The linear combination `∑ i, l i • U (i+1)` of the "direction" codewords. -/
+abbrev linComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (l : Fin s → F) : ι → F :=
+  fun k => ∑ i, l i * U i.succ k
+
+omit [Fintype ι] [DecidableEq F] [Fintype F] in
+/-- The affine combination along the line `x ↦ v + t • lam` in seed space. -/
+lemma affineComb_line {s : ℕ} (U : Fin (s + 1) → (ι → F)) (v lam : Fin s → F) (t : F) :
+    affineComb U (v + t • lam) = affineComb U v + t • (linComb U lam) := by
+  have hsplit : (Fin.cons 1 (v + t • lam) : Fin (s + 1) → F) =
+      Fin.cons 1 v + t • (Fin.cons (0 : F) lam : Fin (s + 1) → F) := by
+    ext i
+    refine Fin.cases ?_ ?_ i <;> simp
+  have hlin : Matrix.vecMul (Fin.cons (0 : F) lam : Fin (s + 1) → F) U = linComb U lam := by
+    ext k
+    simp [Matrix.vecMul, dotProduct, Fin.sum_univ_succ, linComb]
+  change Matrix.vecMul (Fin.cons 1 (v + t • lam) : Fin (s + 1) → F) U = _
+  rw [hsplit, Matrix.add_vecMul, Matrix.smul_vecMul, hlin]
+
 end
 end Affine