Block Relative Distance for smooth Reed-Solomon Codes #
This file formalizes the notion of mutual correlated agreement for proximity generators, introduced in Section 4 [ACFY24].
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. The definition of `block' is also stated in a more general form than the reference paper.
We define distances for smooth ReedSolomon codes with respect to power and fiber domains, as per Section 4.3.1, [ACFY24]. We have generalized the definitions for a generic i to present (i,k)-wise distance measures. This modification is necessary to support following lemmas from Section 4.3.2. The definitions from Section 4.3.1 correspond to i = 0.
References #
- [Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., WHIR: Reed–Solomon Proximity Testing with Super-Fast Verification][ACFY24]
The 2^k-th power images over an embedding φ : ι ↪ F and a finite set
of elements S : Finset ι.
In particular, it returns the set of field elements y ∈ F for which there exists x ∈ S
such that y = (φ x)^(2ᵏ). It models the image of the map x ↦ (φ x)^(2ᵏ) restricted to S.
Semantically: indexPowT S φ k = { (φ x)^(2ᵏ) | x ∈ S } ⊆ F.
Instances For
For i ≤ k, the generic 2^(k-i)-th power fiber over y ∈ indexPowT S φ k.
For φ' : ι^(2ⁱ) → F, this defines the preimage of y under the map
x^(2ⁱ) ↦ x^(2ᵏ) restricted to x^(2ⁱ) ∈ S'.
It returns the subset S' of elements of type ι^(2ⁱ)
such that (x^(2ⁱ))^(2^(k-i)) = x^(2^k) = y.
Example i = 0 : powFiberT 0 k S' φ' y = { x ∈ S' | (x)^(2^k) = y }.
Example i = 1 : powFiberT 1 k S' φ' y = { x^2 ∈ S' | (x^2)^(2^(k-1)) = y }.
Instances For
Definition 4.16
For ι be a smooth evaluation domain, k be a folding parameter, z ∈ (ι^(2ᵏ)),
Block is the set of elements { y ∈ S', y ^ 2^(k-i) = z }, for S' : Finset ι^(2ⁱ).
Instances For
The class DecidableBlockDisagreement provides a decidability instance for testing
pointwise inequality of two functions f, g : ι^(2ⁱ) → F on elements of block i k S' φ' z,
for all z ∈ LpowT S' φ' k.
This class abstracts the decidability condition required to determine whether two
functions disagree on any point in the preimage of z under the map x^(2ⁱ) ↦ x^(2ᵏ) over the
evaluation domain φ' : ι^(2ⁱ) ↪ F. This is useful in defining sets of such z.
Instances
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)|.
Below, we define a disagreementSet(i,k,f,S',φ') as a map (g → Finset (indexPow S φ k)) using the class DecidableBlockDisagreement, to filter a finite subset of the Finset (indexPow S φ k), as per {z ∈ ι ^ 2^k : ∃ y ∈ Block(i,k,S',φ',z) f(y) ≠ g(y)} for a given g.
Instances For
Definition 4.17 Given the disagreementSet from above, we obtain the block relative distance as |disagreementSet|/ |ι ^ (2^k)|
Instances For
notation Δᵣ(i, k, f, S', φ', g) is the (i,k)-wise block relative distance.
Instances For
The block relative distance simplifies to the standard relative Hamming distance when k=0.
For the set S ⊆ F^ι, we define the minimum block relative distance wrt set S.
Instances For
notation Δₛ(i, k, f, S', φ', Set) denotes the minimum block relative distance wrt Set.
Instances For
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 Δᵣ(i, k, f, S', φ', u) ≤ δ.
Instances For
Λᵣ(i, k, f, S', C, hcode, δ) denotes the list of codewords of C δ-close to f,
wrt to the block relative distance.
Instances For
Claim 4.19, Part 1
For a smooth Reed-Solomon code, the standard relative Hamming distance δᵣ(f,g)
is a lower bound for the (i, k)-wise block relative distance Δᵣ(i, k, f, S', φ', g).
Claim 4.19, 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 δ.