Circuits for the arithmetic of Reed–Muller decoding

The decoders Cslib.Code.lineListDecode and the self-correction by interpolation and majority trees query an oracle at computed points and combine the answers arithmetically. This module counts the arithmetic over the full binary basis of the field, where every operation on at most two field elements is one gate; the oracle queries are accounted for separately.

• The first nonzero entry of a vector of m available entries costs 4 * m + 2 gates (Cslib.Circuits.Synthesis.full_firstNonzero).
• The points x + t • v, for all t ∈ F, of the line through x and a fixed point z parametrized as in Cslib.Code.lineListDecode, together with the hint position, cost (q + 5) * m + 2 gates (Cslib.Circuits.Synthesis.full_linePoints).
• A combination with fixed weights of N available values costs 2 * N + 1 gates (Cslib.Circuits.Synthesis.full_weightedSum).
• A majority tree over 3 ^ L available values costs at most 2 * 3 ^ L - 2 gates (Cslib.Circuits.Synthesis.full_majTree): four gates for each majority of three, computed as c + [a = b] * (a - c).

Main results

• Cslib.Circuits.Synthesis.full_firstNonzero, Cslib.Circuits.Synthesis.full_linePoints, Cslib.Circuits.Synthesis.full_weightedSum, Cslib.Circuits.Synthesis.full_majTree.

References

• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]

theorem Cslib.Circuits.Synthesis.full_firstNonzero {F : Type u_1} [Field F] [DecidableEq F] {N : ℕ} {s : Set ((Fin N → F) → F)} {m : ℕ} (u : Fin m → (Fin N → F) → F) (hu : ∀ (i : Fin m), u i ∈ s) : Synthesis fullInterpretation s {fun (x : Fin N → F) => LinearAlgebra.firstNonzero fun (i : Fin m) => u i x} (4 * m + 2)

The first nonzero entry of a vector of m available functions costs 4 * m + 2 gates.

theorem Cslib.Circuits.Synthesis.full_linePoints {F : Type u_1} [Field F] [DecidableEq F] {N : ℕ} {s : Set ((Fin N → F) → F)} [Fintype F] {m : ℕ} (x : Fin m → (Fin N → F) → F) (hx : ∀ (i : Fin m), x i ∈ s) (z : Fin m → F) : Synthesis fullInterpretation s (Set.range fun (o : Option (F × Fin m)) (v : Fin N → F) => match o with | none => LinearAlgebra.firstNonzero (z - fun (i : Fin m) => x i v) | some (t, i) => ((fun (i : Fin m) => x i v) + t • (LinearAlgebra.firstNonzero (z - fun (i : Fin m) => x i v))⁻¹ • (z - fun (i : Fin m) => x i v)) i) ((Fintype.card F + 5) * m + 2)

The points of a line by a circuit. Given the coordinates of x as available functions and a fixed point z, the hint position firstNonzero (z - x) and the coordinates of all points x + t • (firstNonzero (z - x))⁻¹ • (z - x), t ∈ F, of the line through x and z cost (q + 5) * m + 2 gates of the full binary basis.

theorem Cslib.Circuits.Synthesis.full_weightedSum {F : Type u_1} [Field F] {N : ℕ} {s : Set ((Fin N → F) → F)} {ι : Type u_2} [Fintype ι] (c : ι → F) (f : ι → (Fin N → F) → F) (hf : ∀ (i : ι), f i ∈ s) : Synthesis fullInterpretation s {fun (x : Fin N → F) => ∑ i : ι, c i * f i x} (2 * Fintype.card ι + 1)

A combination with fixed weights of N' available functions costs 2 * N' + 1 gates.

theorem Cslib.Circuits.Synthesis.full_majTree {F : Type u_1} [Field F] [DecidableEq F] {N : ℕ} {s : Set ((Fin N → F) → F)} (L : ℕ) (f : Fin (3 ^ L) → (Fin N → F) → F) (hf : ∀ (k : Fin (3 ^ L)), f k ∈ s) : Synthesis fullInterpretation s {fun (x : Fin N → F) => Code.majTree L fun (k : Fin (3 ^ L)) => f k x} (2 * 3 ^ L - 2)

A majority tree by a circuit. A majority tree over 3 ^ L available functions costs at most 2 * 3 ^ L - 2 gates of the full binary basis.