diff --git a/ArkLib.lean b/ArkLib.lean index 0de3d6b0b6..840b28df84 100644 --- a/ArkLib.lean +++ b/ArkLib.lean @@ -39,6 +39,7 @@ import ArkLib.Data.Classes.HasSize import ArkLib.Data.Classes.Initialize import ArkLib.Data.Classes.Serde import ArkLib.Data.Classes.Slice +import ArkLib.Data.CodingTheory.Basic.BlockRelDistance import ArkLib.Data.CodingTheory.Basic.DecodingRadius import ArkLib.Data.CodingTheory.Basic.Distance import ArkLib.Data.CodingTheory.Basic.LinearCode diff --git a/ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean b/ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean new file mode 100644 index 0000000000..7f28c42202 --- /dev/null +++ b/ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean @@ -0,0 +1,298 @@ +/- +Copyright (c) 2025-2026 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Poulami Das (Least Authority), Alexander Hicks, Ilia Vlasov +-/ + +import Mathlib.Data.Finset.Union + +import ArkLib.Data.CodingTheory.Basic.RelativeDistance +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.ListDecodability +import ArkLib.Data.Domain.CosetFftDomain.Block +import ArkLib.Data.Domain.CosetFftDomain.Subdomain + +/-! +# Block Relative Distance for smooth Reed-Solomon Codes + +## Implementation notes + +Block relative distance is defined for smooth rather than constrained Reed Solomon codes, +as is done in the reference paper, as they are more general. + +## References + +* [Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., *WHIR: Reed–Solomon Proximity Testing + with Super-Fast Verification*][ACFY24] + +-/ + +namespace BlockRelDistance + +open Domain ListDecodable NNReal ReedSolomon CosetFftDomainClass + +variable {F : Type} [Field F] [DecidableEq F] + {n k : ℕ} + {φ : SmoothCosetFftDomain n F} + {f g : Fin (2 ^ n) → F} + +/-- Let C be a smooth ReedSolomon code `C = RS[F, ι^(2ⁱ), φ', m]` and `f,g : ι^(2ⁱ) → F`, then + the (i,k)-wise block relative distance is defined as + Δᵣ(i, k, f, S', φ', g) = |{z ∈ ι ^ 2^k : ∃ y ∈ Block(i,k,S',φ',z) f(y) ≠ g(y)}| / |ι^(2^k)|. -/ +def disagreementSet + (k : ℕ) (φ : SmoothCosetFftDomain n F) (f g : Fin (2 ^ n) → F) : Finset F := + { z ∈ (φ.subdomain k).toFinset | ∃ i ∈ blockIdx φ k z, f i ≠ g i } + +@[simp] +lemma disagreementSet_sub_subdomain : + disagreementSet k φ f g ⊆ (φ.subdomain k).toFinset := by simp [disagreementSet] + +@[simp] +lemma disagreementSet_intersect_subdomain_eq : + disagreementSet k φ f g ∩ (φ.subdomain k).toFinset = + disagreementSet k φ f g := by simp [disagreementSet] + +@[simp] +lemma card_disagreementSet_le : + (disagreementSet k φ f g).card ≤ 2 ^ (n - k) := by + rw [show 2 ^ (n - k) = Finset.card (φ.subdomain k).toFinset by simp] + exact Finset.card_le_card (by simp) + +lemma disagreementSet_k_0 : + disagreementSet 0 φ f g = { z ∈ φ.toFinset | ∃ i, φ i = z ∧ f i ≠ g i } := by + ext z + by_cases hmem : z ∈ φ + · have ⟨i, hi⟩ := hmem + have hblock := blockIdx_k_0_of_eq hi + constructor + · aesop + (add simp [disagreementSet]) + (add safe (by rw [mem_subdomain_0_iff_mem])) + · simp only [Finset.mem_filter, mem_toFinset_iff_mem, hmem, + true_and, disagreementSet, forall_exists_index] + intro j hj + have : i = j := by + have := CosetFftDomainClass.injective φ (a₁ := i) + aesop + aesop + (add safe (by rw [mem_subdomain_0_iff_mem])) + · aesop + (add simp [disagreementSet, blockIdx_k_0_of_ne_mem]) + +lemma disagreementSet_k_0_eq_image : + disagreementSet 0 φ f g = Finset.image φ { i | f i ≠ g i } := by + aesop (add simp [disagreementSet_k_0]) + +@[simp] +lemma card_disagreementSet_k_0 : + (disagreementSet 0 φ f g).card = Finset.card { i | f i ≠ g i } := by + rw [disagreementSet_k_0_eq_image, Finset.card_image_of_injective _ (by simp)] + +/-- Given the disagreementSet from above, we obtain the block distance as |disagreementSet|. + Definition 4.17 from [ACFY24]. +-/ +def blockDistance + (k : ℕ) (φ : SmoothCosetFftDomain n F) (f g : Fin (2 ^ n) → F) : ℕ := + Finset.card <| disagreementSet k φ f g + +/-- Given the disagreementSet from above, we obtain the block relative distance as + |disagreementSet|/ |ι ^ (2^k)|. + Definition 4.17 from [ACFY24]. +-/ +def blockRelDistance + (k : ℕ) (φ : SmoothCosetFftDomain n F) (f g : Fin (2 ^ n) → F) : ℚ≥0 := + (blockDistance k φ f g : ℚ≥0) / (φ.subdomain k).toFinset.card + +/-- Notation `Δ𞁒(k, φ', f, g)` is the k-wise block distance. -/ +scoped notation "Δ𞁒("k", "φ'", "f", "g")" => blockDistance k φ' f g + +/-- Notation `δ𞁒(k, φ', f, g)` is the k-wise block relative distance. -/ +scoped notation "δ𞁒("k", "φ'", "f", "g")" => blockRelDistance k φ' f g + +/-- blockDistance from a set of words. -/ +noncomputable def blockDistanceFromCode + (k : ℕ) (φ : SmoothCosetFftDomain n F) (f : Fin (2 ^ n) → F) + (C : Set (Fin (2 ^ n) → F)) : ℕ∞ := + sInf {d | ∃ v ∈ C, blockDistance k φ f v ≤ d} + +/-- blockRelDistance from a set of words. -/ +noncomputable def blockRelDistanceFromCode + (k : ℕ) (φ : SmoothCosetFftDomain n F) (f : Fin (2 ^ n) → F) + (C : Set (Fin (2 ^ n) → F)) : ENNReal := + sInf {d | ∃ v ∈ C, blockRelDistance k φ f v ≤ d} + +scoped notation "Δ𞁒("k", "φ'", "f", "C")" => blockDistanceFromCode k φ' f C +scoped notation "δ𞁒("k", "φ'", "f", "C")" => blockRelDistanceFromCode k φ' f C + +/-- The block distance simplifies to the standard Hamming distance when `k=0`. -/ +@[simp] +lemma blockDistance_eq_hammingDist_k_0 : + Δ𞁒(0, φ, f, g) = Δ₀(f, g) := by simp [blockDistance, hammingDist] + +/-- The block relative distance simplifies to the standard relative Hamming distance when `k=0`. -/ +lemma blockRelDistance_eq_relHammingDist_k_0 : + δ𞁒(0, φ, f, g) = δᵣ(f, g) := by simp [blockRelDistance, Code.relHammingDist] + +/-- Definition 4.18 + For a smooth ReedSolomon code C = RS[F, ι^(2ⁱ), φ', m], proximity parameter δ ∈ [0,1] + function f : ι^(2ⁱ) → F, we define the following as the list of codewords of C δ-close to f, + i.e., u ∈ C such that Δᵣ(k, φ', f, u) ≤ δ. -/ +noncomputable def blockRelDistanceBall + (k : ℕ) (φ : SmoothCosetFftDomain n F) + (f : Fin (2 ^ n) → F) + (δ : ℝ≥0) (C : Set (Fin (2 ^ n) → F)) : Set (Fin (2 ^ n) → F) := + { u ∈ C | δ𞁒(k, φ, f, u) ≤ δ } + +/-- `Λ𞁒(C, k, φ', f, δ)` denotes the list of codewords of C δ-close to f, + wrt to the block relative distance. -/ +scoped notation "Λ𞁒("C", "k", "φ'", "f", "δ")" => + blockRelDistanceBall k φ' f δ C + +private def complDisagreementSet + (k : ℕ) (φ : SmoothCosetFftDomain n F) (f g : Fin (2 ^ n) → F) : Finset F := + (φ.subdomain k).toFinset \ disagreementSet k φ f g + +@[simp] +private lemma card_complDisagreementSet_le : + (complDisagreementSet k φ f g).card ≤ 2 ^ (n - k) := by + simp [complDisagreementSet, Finset.card_sdiff] + +@[simp] +private lemma complDisagreementSet_sub_subdomain : + complDisagreementSet k φ f g ⊆ (φ.subdomain k).toFinset := by simp [complDisagreementSet] + +private lemma blockRelDistance_eq_one_sub' : + δ𞁒(k, φ, f, g) = + 1 - ((complDisagreementSet k φ f g).card : ℚ) / (φ.subdomain k).toFinset.card := by + aesop + (add simp [complDisagreementSet, Finset.card_sdiff, blockRelDistance, blockDistance]) + (add unsafe (by ring_nf)) + +private lemma blockRelDistance_eq_one_sub : + δ𞁒(k, φ, f, g) = + 1 - ((complDisagreementSet k φ f g).card : ℚ≥0) / (φ.subdomain k).toFinset.card := by + rw [←NNRat.coe_inj, blockRelDistance_eq_one_sub', + NNRat.coe_sub (by aesop (add safe [(by field_simp), (by norm_cast)]))] + rfl + +private def agreementBlockUnion + (k : ℕ) (φ : SmoothCosetFftDomain n F) + (f g : Fin (2 ^ n) → F) : Finset (Fin (2 ^ n)) := + Finset.biUnion (complDisagreementSet k φ f g) (blockIdx φ k) + +@[simp] +private lemma card_agreementBlockUnion_le : + (agreementBlockUnion k φ f g).card ≤ 2 ^ n := by + conv_rhs => + rw [show 2 ^ n = (Finset.univ (α := Fin (2 ^ n))).card by simp] + exact Finset.card_le_card (by simp) + +private lemma card_agreementBlockUnion + (hkn : k ≤ n) : + (agreementBlockUnion k φ f g).card = + 2 ^ k * (complDisagreementSet k φ f g).card := by + unfold agreementBlockUnion + rw [Finset.card_biUnion (by + aesop + (add simp [Set.PairwiseDisjoint, Set.Pairwise]) + (add safe disjoint_blockIdx) + )] + rw [Finset.sum_equiv + (Equiv.refl _) + (g := fun _ ↦ 2 ^ k) + (t := complDisagreementSet k φ f g) + (by simp) + (fun i hi ↦ by + have := complDisagreementSet_sub_subdomain hi + aesop (add simp [card_block_of_mem_subdomain']) + )] + aesop (add unsafe (by rw [mul_comm])) + +private lemma agreement_sub_agreementBlockUnion : + agreementBlockUnion k φ f g ⊆ ({ i | f i = g i } : Finset _) := fun x hx ↦ by + aesop (add simp [agreementBlockUnion, complDisagreementSet, disagreementSet]) + +private lemma card_disagreement_le : + Finset.card { i | f i ≠ g i } ≤ 2 ^ n - (agreementBlockUnion k φ f g).card := by + conv_rhs => + lhs + rw [show 2 ^ n = (Fintype.card (α := Fin (2 ^ n))) by simp] + rw [←Finset.card_compl] + exact Finset.card_le_card <| fun x hx ↦ by + simp only [Finset.mem_compl] + intro contra + have := agreement_sub_agreementBlockUnion contra + simp_all + +private lemma relHammingDist_le_sub_agreementBlockUnion' : + δᵣ(f, g) ≤ 1 - ((agreementBlockUnion k φ f g).card : ℚ) / (2 ^ n) := by + unfold Code.relHammingDist + simp only [hammingDist, ne_eq, Fintype.card_fin, Nat.cast_pow, Nat.cast_ofNat, NNRat.cast_div, + NNRat.cast_natCast, NNRat.cast_pow, NNRat.cast_ofNat] + apply le_trans (b := ((2 ^ n - (agreementBlockUnion k φ f g).card) / (2 ^ n) : ℚ)) + · field_simp + conv_rhs => + rw [show (_ - _) = Nat.cast (2 ^ n - (agreementBlockUnion k φ f g).card +) by rw [Nat.cast_sub (by simp)]; simp] + rw [Nat.cast_le] + exact card_disagreement_le + · field_simp + aesop + +private lemma relHammingDist_le_sub_agreementBlockUnion : + δᵣ(f, g) ≤ 1 - ((agreementBlockUnion k φ f g).card : ℚ≥0) / (2 ^ n) := by + have := relHammingDist_le_sub_agreementBlockUnion' (f := f) (g := g) (φ := φ) + (k := k) + rw [←NNRat.cast_le (K := ℚ)] + exact le_trans this <| le_of_eq <| by + rw [NNRat.coe_sub (by aesop (add safe [(by field_simp), (by norm_cast)]))] + rfl + +/-- Claim 4.19 from [ACFY24], Part 1 + For a smooth Reed-Solomon code, the standard relative Hamming distance `δᵣ(f,g)` + is a lower bound for the k-wise block relative distance `δᵣ(k, φ, f, g)`. +-/ +lemma relHammingDist_le_blockRelDistance (hkn : k ≤ n) : + δᵣ(f, g) ≤ δ𞁒(k, φ, f, g) := by + apply le_trans + · exact relHammingDist_le_sub_agreementBlockUnion + (f := f) (g := g) (φ := φ) (k := k) + · rw [card_agreementBlockUnion hkn] + rw [Nat.cast_mul] + simp only [Nat.cast_pow, Nat.cast_ofNat] + have : (Nat.cast (2 : ℕ) ^ n : ℚ≥0) = (Nat.cast <| 2 ^ k * 2 ^ (n - k)) := by + rw [←Nat.pow_add, Nat.add_sub_of_le hkn] + simp + rw [show (2 : ℚ≥0) ^ n = (((2 : ℕ) ^ n) : ℚ≥0) by rfl, this, Nat.cast_mul] + simp only [Nat.cast_pow, Nat.cast_ofNat, tsub_le_iff_right, ge_iff_le] + conv_rhs => + rhs + field_simp + rw [blockRelDistance_eq_one_sub] + simp only [card_toFinset, Fintype.card_fin, Nat.cast_pow, Nat.cast_ofNat] + rw [←NNRat.coe_le_coe] + simp only [NNRat.cast_one, NNRat.cast_add, NNRat.cast_div, NNRat.cast_natCast, NNRat.cast_pow, + NNRat.cast_ofNat] + rw [NNRat.coe_sub (by aesop (add safe [(by field_simp), (by norm_cast)]))] + simp + +/-- Claim 4.19 from [ACFY24], Part 2 + As a consequence of `relHammingDist_le_blockRelDistance`, the list of codewords + within a certain block relative distance `δ` is a subset of the list of codewords + within the same relative Hamming distance `δ`. +-/ +lemma listBlock_subset_listHamming + (hkn : k ≤ n) (δ : ℝ≥0) (C : Set (Fin (2 ^ n) → F)) : + Λ𞁒(C, k, φ, f, δ) ⊆ closeCodewordsRel C f δ := by + intro u hu + simp only [blockRelDistanceBall, Set.mem_sep_iff] at hu + refine ⟨hu.1, ?_⟩ + have h1 := relHammingDist_le_blockRelDistance + (φ := φ) (k := k) (f := f) (g := u) hkn + simp only [relHammingBall, Set.mem_setOf_eq, ge_iff_le] + apply le_trans (b := NNRat.cast δ𞁒(k, φ, f, u)) + · rewrite [NNRat.cast_le] + convert h1 + · aesop + +end BlockRelDistance diff --git a/ArkLib/Data/Domain/CosetFftDomain/Block.lean b/ArkLib/Data/Domain/CosetFftDomain/Block.lean index 57be3c5fd9..12e2143399 100644 --- a/ArkLib/Data/Domain/CosetFftDomain/Block.lean +++ b/ArkLib/Data/Domain/CosetFftDomain/Block.lean @@ -42,7 +42,7 @@ variable {ω : D} {k : ℕ} {x y : F} open Finset Polynomial -/-- The `k`th roots of `x` from the domain `ω`. +/-- The `2^k`th roots of `x` from the domain `ω`. This is the definition 4.16 from [ACFY24]. Note, we do not require `x` to be from a subdomain. -/ @@ -54,23 +54,18 @@ def block (ω : D) (k : ℕ) (x : F) : Finset F := lemma mem_block : y ∈ block ω k x ↔ y ∈ ω ∧ y ^ 2 ^ k = x := by simp [block] -/-- There are no roots of `0` in any domain. -/ -@[simp] -lemma block_x_0 : - block ω k 0 = ∅ := by aesop - @[simp] -lemma block_k_1 : +lemma block_k_0 : block ω 0 x = if x ∈ ω then {x} else ∅ := by aesop /-- An alternative definition of `block` in terms of `Polynomial.nthRootsFinset`. -/ lemma block_eq_nthRootsFinset : - block ω k x = nthRootsFinset (2 ^ k) x ∩ toFinset ω := by aesop (add unsafe cases Nat) + block ω k x = nthRootsFinset (2 ^ k) x ∩ toFinset ω := by aesop /-- The cardinality of a block does not exceed its degree. -/ @[simp] -lemma card_block_le : +lemma block_card_le : (block ω k x).card ≤ 2 ^ k := by rw [block_eq_nthRootsFinset] exact le_trans (card_le_card inter_subset_left) <| by @@ -79,6 +74,10 @@ lemma card_block_le : (@Multiset.toFinset_card_le F (Classical.decEq F) _) (card_nthRoots _ _) +/-- Blocks corresponding to different points are disjoint. -/ +theorem disjoint_block {x y : F} (hxy : x ≠ y) : + Disjoint (block ω k x) (block ω k y) := by aesop (add simp [disjoint_iff]) + /-- The set of indices of a block of `ω` at `x` of the degree `k`. -/ def blockIdx (ω : D) (k : ℕ) (x : F) : Finset ι := {i | ω i ^ 2 ^ k = x} @@ -101,17 +100,14 @@ lemma mem_blockIdx_iff_mem_block {i : ι} : lemma blockIdx_x_0 : blockIdx ω k 0 = ∅ := by aesop (add simp [mem_blockIdx_iff_mem_block]) -lemma blockIdx_k_1_of_eq {i : ι} (hi : ω i = x) : +lemma blockIdx_k_0_of_eq {i : ι} (hi : ω i = x) : blockIdx ω 0 x = {i} := by ext j have := CosetFftDomainClass.injective ω (a₁ := i) (a₂ := j) - aesop - (add simp [mem_blockIdx_iff_mem_block]) + aesop (add simp [mem_blockIdx_iff_mem_block]) -lemma blockIdx_k_1_of_ne_mem (hx : x ∉ ω) : - blockIdx ω 0 x = ∅ := by - aesop - (add simp [mem_blockIdx_iff_mem_block]) +lemma blockIdx_k_0_of_ne_mem (hx : x ∉ ω) : + blockIdx ω 0 x = ∅ := by aesop (add simp [mem_blockIdx_iff_mem_block]) /-- `blockIdx` is the preimage of `block`. -/ lemma blockIdx_eq_preimage_block : @@ -129,6 +125,11 @@ lemma card_blockIdx : (add simp [blockIdx_eq_preimage_block, card_preimage]) (add unsafe congrArg) +/-- The sets of indices of blocks corresponding to different points are disjoint. -/ +theorem disjoint_blockIdx {x y : F} (hxy : x ≠ y) : + Disjoint (blockIdx ω k x) (blockIdx ω k y) := by + aesop (add simp [disjoint_iff_ne, mem_blockIdx_iff_mem_block]) + end CosetFftDomainClass end Domain diff --git a/ArkLib/ProofSystem/Whir/BlockRelDistance.lean b/ArkLib/ProofSystem/Whir/BlockRelDistance.lean index 089656a3aa..787e2cb544 100644 --- a/ArkLib/ProofSystem/Whir/BlockRelDistance.lean +++ b/ArkLib/ProofSystem/Whir/BlockRelDistance.lean @@ -34,6 +34,8 @@ The definitions from Section 4.3.1 correspond to i = 0. namespace BlockRelDistance +namespace Obsolete + open ListDecodable NNReal ReedSolomon variable {F : Type*} [Field F] @@ -204,5 +206,6 @@ lemma listBlock_subset_listHamming ‹DecidableEq F› from Subsingleton.elim _ _] exact_mod_cast h3 +end Obsolete end BlockRelDistance diff --git a/ArkLib/ProofSystem/Whir/Folding.lean b/ArkLib/ProofSystem/Whir/Folding.lean index 42af4e6c7c..24b7704f5e 100644 --- a/ArkLib/ProofSystem/Whir/Folding.lean +++ b/ArkLib/ProofSystem/Whir/Folding.lean @@ -40,7 +40,7 @@ Todo: should we aim to add tags? namespace Fold -open BlockRelDistance Vector Finset +open BlockRelDistance Obsolete Vector Finset variable {F : Type} [Field F] {ι : Type} [Pow ι ℕ] diff --git a/ArkLib/ProofSystem/Whir/RBRSoundness.lean b/ArkLib/ProofSystem/Whir/RBRSoundness.lean index ab56871233..f1abb8f03c 100644 --- a/ArkLib/ProofSystem/Whir/RBRSoundness.lean +++ b/ArkLib/ProofSystem/Whir/RBRSoundness.lean @@ -40,7 +40,7 @@ Todo: should we aim to add tags? -/ namespace WhirIOP -open BigOperators BlockRelDistance MutualCorrAgreement Generator Finset +open BigOperators BlockRelDistance Obsolete MutualCorrAgreement Generator Finset ListDecodable NNReal ReedSolomon variable {F : Type} [Field F] [Fintype F] [DecidableEq F]