Packing a Boolean function into line-parity codes

Split the inputs of f : BooleanFunction (p + w) into a prefix a of p bits and a suffix z of w bits. An injection place assigns every prefix a code copy c, an information point u and a bit position r. For each copy and suffix, the information symbol at u is the field element whose bit r is f (Fin.append a z) for the prefix a placed at (c, u, r), and false at unplaced bits (packedBit). The line-parity code extends these symbols to a codeword (codeword), and every bit of every codeword value is a Boolean function of the suffix alone (resource).

Summing the resources of a request along any punctured line through its information point recovers the requested value (sum_resource): the codeword value at the point is the sum along the line, bits is additive, and the code is systematic on its information set. A request is therefore answered from s = Fintype.card K - 1 resource values (succ_eq_card), where Fintype.card K = 2 ^ b (card_eq_two_pow).

Main definitions

• Cslib.Circuits.Boolean.MassProduction.Pipeline.packedBit: the packed information bits.
• Cslib.Circuits.Boolean.MassProduction.Pipeline.codeword: the codeword of a copy and suffix.
• Cslib.Circuits.Boolean.MassProduction.Pipeline.resource: a codeword bit as a function of the suffix.

Main results

• Cslib.Circuits.Boolean.MassProduction.Pipeline.sum_resource: recovery along a line.
• Cslib.Circuits.Boolean.MassProduction.Pipeline.succ_eq_two_pow: s + 1 = 2 ^ b when the nonzero scalars are numbered by Fin s and the field elements are bit strings of length b.

References

• Adapted from MassProduction/HighRate/BooleanRecovery.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.packedBit {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b p w copies : ℕ} (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (f : BooleanFunction (p + w)) (z : BitString w) (c : Fin copies) (u : Fin ℓ → K) (r : Fin b) : Bool

Bit r of the information symbol at u in copy c for the suffix z: the value of f at the prefix placed at (c, u, r), and false if no prefix is placed there.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.codeword {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b p w copies : ℕ} (bits : K ≃+ BitString b) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (f : BooleanFunction (p + w)) (z : BitString w) (c : Fin copies) : (Fin ℓ → K) → K

The codeword of copy c for the suffix z, extending the packed information symbols.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.resource {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b p w copies : ℕ} (bits : K ≃+ BitString b) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (f : BooleanFunction (p + w)) (c : Fin copies) (y : Fin ℓ → K) (r : Fin b) : BooleanFunction w

The resource of copy c, point y and bit r: bit r of the codeword value at y, as a function of the suffix.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.packedBit_place {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b p w copies : ℕ} {C : LineCode K ℓ} {place : BitString p ↪ Fin copies × ↥C.info × Fin b} {f : BooleanFunction (p + w)} (a : BitString p) (z : BitString w) : packedBit C place f z (place a).1 (↑(place a).2.1) (place a).2.2 = f (Fin.append a z)

The packed bit at a placed prefix is the value of f there.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.sum_scalar {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {s : ℕ} {M : Type u_2} [AddCommMonoid M] (scalar : Fin s ≃ { c : K // c ≠ 0 }) (g : K → M) : ∑ j : Fin s, g ↑(scalar j) = ∑ c ∈ Finset.univ.erase 0, g c

Numbering the nonzero scalars by scalar sums over the punctured line.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.sum_resource {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b s p w copies : ℕ} {C : LineCode K ℓ} {place : BitString p ↪ Fin copies × ↥C.info × Fin b} {f : BooleanFunction (p + w)} (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (a : BitString p) (z : BitString w) {v : Fin ℓ → K} (hv : v ≠ 0) : ∑ j : Fin s, resource bits C place f (place a).1 (↑(place a).2.1 + ↑(scalar j) • v) (place a).2.2 z = f (Fin.append a z)

Recovery along a line. The resources of the request (a, z), at the points u + scalar j • v of a punctured line through its information point u, sum to f (Fin.append a z).

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.card_eq_two_pow {b : ℕ} {K : Type u_2} [Add K] [Fintype K] (bits : K ≃+ BitString b) : Fintype.card K = 2 ^ b

A type whose elements are the bit strings of length b has 2 ^ b elements.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.succ_eq_card {s : ℕ} {K : Type u_2} [Zero K] [Fintype K] (scalar : Fin s ≃ { c : K // c ≠ 0 }) : s + 1 = Fintype.card K

Numbering the nonzero elements by Fin s leaves s + 1 elements.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.succ_eq_two_pow {b s : ℕ} {K : Type u_2} [Add K] [Zero K] (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) : s + 1 = 2 ^ b

The sizes agree: s + 1 = 2 ^ b.