chore: bump Lean stack to v4.31.0

AGENTS.md

@@ -8,6 +8,7 @@ Start with [`README.md`](README.md) for project overview.
 ## Fast Start
 
 1. For a convenient routine check, start with `./scripts/validate.sh`.
+   Before committing or pushing, run it in full; it enforces the `ArkLib/Data` zero-warning gate.
 2. On a cold clone, run `lake exe cache get` first.
 3. If you add, rename, or delete files under `ArkLib/`, `git add` new paths before validation.
 4. If you also want Lean style linting, run `./scripts/validate.sh --lint`.

ArkLib/Commitments/Functional/KZG/Binding.lean

@@ -630,8 +630,14 @@ lemma binding_cond_le_t_sdh_cond {n : ℕ} {AuxState : Type} [SampleableType G
       ((Option.map (fun result : RunResult => result.2) result₂).getD false)
       (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ) rfl hresp hg₁ hpair
       hverify₁ hverify₂
-  simpa only [bindingGameExt, kzg, OptionT.mk, pSpec', impl, sample, body, run₁, run₂,
-      pack, gameComp, P, Q] using hmono
+  change
+    Pr[P | OptionT.mk (do
+      let τ ← sample
+      (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))]
+    ≤ Pr[Q | OptionT.mk (do
+      let τ ← sample
+      (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))]
+  exact hmono
 
 omit [DecidableEq G₁] [Module (ZMod p) (Additive G₁)]
   [Module (ZMod p) (Additive G₂)] in
@@ -662,16 +668,16 @@ lemma t_sdh_game_eq {n : ℕ} {AuxState : Type} [SampleableType G₁]
       (bindingReduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) AuxState
         adversary) := by
   let scheme := kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)
-  simp only [Groups.tSdhExperiment]
+  simp only [Groups.tSdhExperiment, Groups.tSdhGame]
   congr 1
   let pSpec' : ProtocolSpec 1 := ⟨!v[.P_to_V], !v[G₁]⟩
   let impl : QueryImpl _ (StateT unifSpec.QueryCache ProbComp) :=
     QueryImpl.addLift
       (randomOracle : QueryImpl unifSpec (StateT unifSpec.QueryCache ProbComp))
       (challengeQueryImpl (pSpec := pSpec'))
-  simpa only [bindingGameExt, bindingReduction, kzg, OptionT.mk, pSpec', impl, scheme,
-      OptionT.run_map] using
-    OptionT.map_mk_bind_eq_of_body
+  dsimp only [bindingGameExt, bindingReduction, kzg, OptionT.mk, pSpec', impl, scheme,
+    OptionT.run_map]
+  convert OptionT.map_mk_bind_eq_of_body
       (sample := (Groups.sampleNonzeroZMod (p := p) : ProbComp (ZMod p)))
       (body₁ := fun τ => (simulateQ impl (do
         let srs := Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ
@@ -715,9 +721,9 @@ lemma t_sdh_game_eq {n : ℕ} {AuxState : Type} [SampleableType G₁]
       (hBody := by
         intro τ
         dsimp only
-        refine StateT.map_run'_eq_of_map_eq _ _ _ _ (∅ : unifSpec.QueryCache) ?_
+        refine StateT.map_run'_eq_of_map_eq (∅ : unifSpec.QueryCache) ?_
         simp only [simulateQ_bind, simulateQ_pure, map_eq_bind_pure_comp, bind_assoc]
-        congr 1)
+        congr 1) using 1 <;> rfl
 
 omit [DecidableEq G₁] in
 /-- The t-SDH experiment is bounded by the t-SDH error. -/
@@ -746,7 +752,8 @@ theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
   letI game := Commitment.bindingGame (init := pure ∅) (impl := randomOracle)
     (AuxState := AuxState) (scheme := scheme) (adversary := adversary)
   letI game_ext := bindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary scheme
-  convert (
+  change Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game] ≤ tSdhError
+  exact
     calc Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game]
     _ = Pr[bindingCondExt (p := p) (n := n) | game_ext] :=
       binding_game_ext_eq_binding_game (pairing := pairing) adversary
@@ -760,7 +767,7 @@ theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
       (bindingReduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) AuxState adversary) :=
       t_sdh_game_eq (g₁ := g₁) (g₂ := g₂) (pairing := pairing) adversary
     _ ≤ tSdhError := t_sdh_error_bound (g₁ := g₁) (g₂ := g₂) (pairing := pairing)
-      tSdhError htSdh adversary)
+      tSdhError htSdh adversary
 
 end Binding
 

ArkLib/Commitments/Functional/KZG/Correctness.lean

@@ -172,8 +172,10 @@ theorem correctness (hpG1 : Nat.card G₁ = p) {g₁ : G₁} {g₂ : G₂}
   obtain ⟨⟨ck, vk⟩, hkeygen, hx⟩ := hx
   rw [mem_support_bind_iff] at hx
   obtain ⟨⟨cm, decomm⟩, hcommit, hx⟩ := hx
-  replace hkeygen := OracleComp.mem_support_of_mem_support_liftComp _ _ hkeygen
-  replace hcommit := OracleComp.mem_support_of_mem_support_liftComp _ _ hcommit
+  replace hkeygen := OracleComp.mem_support_of_mem_support_liftComp
+    (superSpec := _) (oa := _) (x := (ck, vk)) hkeygen
+  replace hcommit := OracleComp.mem_support_of_mem_support_liftComp
+    (superSpec := _) (oa := _) (x := (cm, decomm)) hcommit
   rw [mem_support_bind_iff] at hkeygen
   obtain ⟨τ, _hτ, hkeygen⟩ := hkeygen
   rw [mem_support_pure_iff] at hkeygen
@@ -191,8 +193,9 @@ theorem correctness (hpG1 : Nat.card G₁ = p) {g₁ : G₁} {g₂ : G₂}
       (commit (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).1 data)
       (generateOpening (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).1 data query)
       query (OracleInterface.answer data query) := by
-    simpa [OracleInterface.answer] using
-      (KZG.correctness (pairing := pairing) (g₁ := g₁) (g₂ := g₂) hpG1 n τ data query)
+    change verifyOpening pairing _ _ _ query ((CPolynomial.ofFn data).eval query) = true
+    simpa only [CPolynomial.ofFn] using
+      KZG.correctness (pairing := pairing) (g₁ := g₁) (g₂ := g₂) hpG1 n τ data query
   simp only [Option.elimM] at hx
   rw [mem_support_bind_iff] at hx
   obtain ⟨openingOpt, hopeningOpt, hx⟩ := hx

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

@@ -296,7 +296,7 @@ lemma function_binding_game_ext_support_srs {n L : ℕ} {AuxState : Type} [Sampl
             (τ', Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ', cm', queryOf',
               (fun i => responseOf' i), accepts, proofs))
           (Option.map (fun resultOf i => (resultOf i).2) resultPairs)) := by
-    simpa [mem_support_pure_iff] using hx
+    exact (mem_support_pure_iff _ _).mp hx
   cases hres : resultPairs with
   | none => simp [hres] at hx'
   | some resultOf =>
@@ -343,10 +343,10 @@ lemma function_binding_game_ext_support_verify_all {n L : ℕ} {AuxState : Type}
         ((Option.map (fun resultOf i => (resultOf i).1) opts_v).bind fun accepts =>
           Option.map
             (fun proofs =>
-              (τ_v, Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v, cm_v, queryOf_v,
-                (fun i => responseOf_v i), accepts, proofs))
+              (τ_v, Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v, claim_v.1,
+                claim_v.2.fst, (fun i => claim_v.2.2.1 i), accepts, proofs))
             (Option.map (fun resultOf i => (resultOf i).2) opts_v)) := by
-      simpa [mem_support_pure_iff] using hx
+      exact (mem_support_pure_iff _ _).mp hx
     cases hres : opts_v with
     | none => simp [hres] at hx'
     | some resultOf =>
@@ -611,7 +611,7 @@ lemma arsdh_game_eq {n L : ℕ} {AuxState : Type} [SampleableType G₁]
       (hBody := by
         intro τ
         dsimp only
-        refine StateT.map_run'_eq_of_map_eq _ _ _ _ (∅ : unifSpec.QueryCache) ?_
+        refine StateT.map_run'_eq_of_map_eq (∅ : unifSpec.QueryCache) ?_
         simp only [simulateQ_bind, simulateQ_pure, map_eq_bind_pure_comp, bind_assoc]
         congr 1
         funext claimResult
@@ -648,7 +648,9 @@ theorem function_binding {g₁ : G₁} {g₂ : G₂}
   letI game := Commitment.functionBindingGame (init := pure ∅) (impl := randomOracle) (hn := rfl)
     (AuxState := AuxState) (scheme := scheme) (adversary := adversary)
   letI game_ext := functionBindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary scheme
-  convert (
+  change Pr[Commitment.functionBindingCondition (Data := Fin (n + 1) → ZMod p) | game]
+    ≤ arsdhError
+  exact
     calc Pr[Commitment.functionBindingCondition (Data := Fin (n + 1) → ZMod p) | game]
     _ = Pr[functionBindingCondExt n L | game_ext] :=
       function_binding_game_ext_eq_function_binding_game (pairing := pairing) adversary
@@ -660,7 +662,7 @@ theorem function_binding {g₁ : G₁} {g₂ : G₂}
       (reduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) L hn AuxState adversary) :=
       arsdh_game_eq (g₁ := g₁) (g₂ := g₂) (pairing := pairing) hn adversary
     _ ≤ arsdhError := arsdh_error_bound (g₁ := g₁) (g₂ := g₂) (pairing := pairing) hn
-      arsdhError hArsdh adversary)
+      arsdhError hArsdh adversary
 
 
 end FunctionBinding

ArkLib/Data/Classes/FunEquiv.lean

@@ -40,7 +40,7 @@ instance : DFunEquiv (∀ a : α, β a) α β where
 /-- The forward direction of the equivalence is a `DFunLike`. -/
 instance : DFunLike F α β where
   coe := DFunEquiv.equiv.toFun
-  coe_injective' := DFunEquiv.equiv.injective
+  coe_injective := DFunEquiv.equiv.injective
 
 /-- Coercion from the dependent function type `∀ a : α, β a` to another type `F` that has a
 `DFunEquiv` instance.

ArkLib/Data/CodingTheory/Basic/Distance.lean

@@ -686,7 +686,7 @@ theorem dist'_eq_dist : ‖C‖₀'.toNat = ‖C‖₀ := by
             (by simpa [hvals] using hVals_nonempty))
       -- `vals.min ≤ dStar` since `dStar ∈ vals`.
       have h_le : vals.min ≤ (dStar : ℕ∞) := by
-        simpa using (Finset.min_le hmem_min')
+        exact Finset.min_le hmem_min'
       -- `dStar ≤ a` for all `a ∈ vals`, hence `dStar ≤ vals.min`.
       have h_ge : (dStar : ℕ∞) ≤ vals.min := by
         -- Use the universal lower-bound property of `min'`.
@@ -789,7 +789,7 @@ lemma possibleDistsToCode_nonempty_iff
   -- Goal: (∃ d, ∃ c ∈ C, c ≠ w ∧ δf w c = d) ↔ (∃ c, c ∈ C \ {w})
 
   -- 2. Unfold set difference on RHS
-  simp only [Set.mem_diff, Set.mem_singleton_iff]
+  simp only [Set.mem_sdiff, Set.mem_singleton_iff]
   -- Goal: (∃ d, ∃ c ∈ C, c ≠ w ∧ δf w c = d) ↔ (∃ c, c ∈ C ∧ c ≠ w)
 
   -- 3. Prove the iff

ArkLib/Data/CodingTheory/Basic/LinearCode.lean

@@ -257,14 +257,14 @@ scoped macro_rules
 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 [Fintype ι] (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c
+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`.
 Definition 3.7 [BCGM25]. -/
-def projectedCode [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
+def projectedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) :=
   {w | ∃ c ∈ C, w = c|[T]}
 
 notation:60 C "|[" T "]" => projectedCode C T
@@ -281,7 +281,9 @@ lemma projectedCode_linearCombination [Field F] (LC : LinearCode ι F) (T : Fins
     exact ⟨Submodule.sum_mem _ fun j _ => Submodule.smul_mem _ _ (hw j |>.1),
       fun t ht => by simp [show ∀ j, U j t = w j t from
         fun j => congr_fun (hw j |>.2) ⟨t, ht⟩]⟩
-  exact ⟨w, hw.1, funext fun t => by simpa using Eq.symm (hw.2 t t.2)⟩
+  exact ⟨w, hw.1, funext fun t => by
+    change (∑ j, c j * U j t.1) = w t.1
+    exact Eq.symm (hw.2 t t.2)⟩
 
 /-- A linear code is maximum distance separable (MDS) if its parameters meet the singleton bound. -/
 def IsMDS {ι : Type} [Fintype ι] [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
@@ -384,14 +386,8 @@ lemma rank_genMatrix_eq_dim [Field F] (LC : LinearCode ι F) :
 /-- The dimension of the linear code given by a generator matrix is the rank of the matrix. -/
 lemma dim_fromRowGenMat {k n : ℕ} [Field F] {G : Matrix (Fin k) (Fin n) F} :
     dim (fromRowGenMat G) = G.rank := by
-  unfold fromRowGenMat;
-  convert congr_arg (fun s : Submodule F _ => Module.finrank F s) _;
-  rotate_left;
-  · exact Submodule.span F (Set.range (fun i => G i));
-  · ext; simp [Matrix.vecMulLinear];
-    simp +decide [funext_iff, Matrix.vecMul, Submodule.mem_span_range_iff_exists_fun];
-    rfl;
-  · convert Matrix.rank_eq_finrank_span_row G using 1
+  unfold dim fromRowGenMat
+  rw [range_vecMulLinear, Matrix.rank_eq_finrank_span_row]
 
 /-- Given a linear code of length `ι` and dimension `dim` over a field `F`, we define its `ι × dim`
 generator matrix as a matrix whose columns are an `F`-basis of the code. -/
@@ -511,8 +507,8 @@ theorem singletonBound [CommRing F] [StrongRankCondition F]
       have hxS : ∀ i ∈ S, (x : ι → F) i = 0 := by
         intro i hi
         have := congrArg (fun (f : (S → F)) => f ⟨i, hi⟩) (by simpa using hx)
-        -- simp at this
-        simpa using this
+        change (x : ι → F) i = 0 at this
+        exact this
       -- bound the weight of x by |Sᶜ|
       let A : Finset ι := Finset.univ.filter (fun i => (x : ι → F) i ≠ 0)
       have hA_subset_compl : A ⊆ Sᶜ := by

ArkLib/Data/CodingTheory/Basic/MDSCode.lean

@@ -106,8 +106,7 @@ lemma IsMDS_of_matrix_IsMDS [Field F] [DecidableEq F] {G : Matrix (Fin k) (Fin n
       refine le_trans (h_dist_ge (u - v) ?_ ?_) ?_
       · exact Submodule.sub_mem _ hu hv
       · exact sub_ne_zero_of_ne huv
-      · convert hd using 1
-        exact congr_arg Finset.card (Finset.filter_congr fun x _ => by simp [sub_eq_zero])
+      · simpa only [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero] using hd
   have h_dist_le : Code.dist (fromRowGenMat G).carrier ≤ n - k + 1 := by
     contrapose! h_singleton_bound
     rw [tsub_add_eq_add_tsub ]

ArkLib/Data/CodingTheory/Basic/RelativeDistance.lean

@@ -287,7 +287,6 @@ lemma relCloseToCode_iff_relCloseToCodeword_of_minDist [Nonempty ι] [DecidableE
       use v; constructor
       · simp only [Subtype.coe_prop]
       · rw [relDistFromPickRelClosestCodeword_of_Nonempty_Code] at h_dist_le_e
-        simp only at h_dist_le_e
         rw [←ENNReal.coe_le_coe]
         exact h_dist_le_e
   · -- Direction 2: (←)
@@ -363,14 +362,11 @@ theorem relDistFromCode_le_iff_distFromCode_toENNReal_le {C : Set (ι → F)} (u
     δᵣ(u, C) ≤ δ ↔ (Δ₀(u, C) : ENNReal) ≤ δ * (Fintype.card ι : ℝ≥0) := by
   rw [relDistFromCode_le_iff_distFromCode_le]
   constructor <;> intro h
-  · simp_all only [ENNReal.coe_natCast]
-    convert ENNReal.ofReal_le_ofReal
-      (Nat.floor_le (show 0 ≤ δ * (Fintype.card ι : ℝ≥0) by positivity)) |>
-        le_trans (ENNReal.ofReal_le_ofReal <| ?_) using 1
-    any_goals exact Nat.cast (distFromCode u C |> ENat.toNat)
-    · cases h : distFromCode u C <;> aesop
-    · simp [ENNReal.ofReal_mul]
-    · cases h' : distFromCode u C <;> aesop
+  · refine (ENat.toENNReal_le.mpr h).trans ?_
+    change ((⌊δ * (Fintype.card ι : ℝ≥0)⌋₊ : ℝ≥0) : ENNReal) ≤
+      (δ * (Fintype.card ι : ℝ≥0) : ℝ≥0)
+    exact ENNReal.coe_le_coe.mpr
+      (Nat.floor_le (show 0 ≤ δ * (Fintype.card ι : ℝ≥0) by positivity))
   · contrapose! h
     cases h' : distFromCode u C
     · simp_all only [ENat.coe_lt_top, ENNReal.coe_natCast, ENat.toENNReal_top]