Bit encodings of points and lines

Field elements are read through an additive bijection bits : K ≃+ BitString b, so adding a fixed point is a coordinatewise exclusive or. A point of K ^ ℓ is ℓ consecutive blocks of b bits, and a batch of t points is t consecutive point blocks. A batch of lines u + c • v is listed point by point in a fixed order of s scalars.

Main definitions

• Cslib.BitString.pointBits: the bits of one point.
• Cslib.BitString.pointEquiv: the equivalence between points and their bits.
• Cslib.BitString.targetBits: the bits of a batch of points.
• Cslib.BitString.lineBits: the listed points of a batch of lines.

Main results

• Cslib.BitString.pointBits_add: point encodings preserve addition.
• Cslib.BitString.pointBits_injective: distinct points have distinct encodings.

References

• Adapted from the vector encodings in MassProduction/BinaryEncoding.lean of S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.BitString.pointBits {K : Type u_1} {ℓ b : ℕ} [Add K] (bits : K ≃+ BitString b) (u : Fin ℓ → K) : BitString (ℓ * b)

The bits of a point: block i holds the bits of coordinate i.

theorem Cslib.BitString.pointBits_add {K : Type u_1} {ℓ b : ℕ} [Add K] (bits : K ≃+ BitString b) (u v : Fin ℓ → K) : pointBits bits (u + v) = pointBits bits u + pointBits bits v

Point bits add coordinatewise.

theorem Cslib.BitString.pointBits_injective {K : Type u_1} {ℓ b : ℕ} [Add K] (bits : K ≃+ BitString b) : Function.Injective (pointBits bits)

Distinct points have distinct bits.

def Cslib.BitString.pointEquiv {K : Type u_1} {ℓ b : ℕ} [Add K] (bits : K ≃+ BitString b) : (Fin ℓ → K) ≃ BitString (ℓ * b)

Points of K ^ ℓ are their bits.

@[simp]

theorem Cslib.BitString.pointEquiv_apply {K : Type u_1} {ℓ b : ℕ} [Add K] (bits : K ≃+ BitString b) (u : Fin ℓ → K) : (pointEquiv bits) u = pointBits bits u

pointEquiv bits sends a point to its bits pointBits bits.

def Cslib.BitString.targetBits {K : Type u_1} {ℓ b t : ℕ} [Add K] (bits : K ≃+ BitString b) (targets : Fin t → Fin ℓ → K) : BitString (t * (ℓ * b))

The bits of a batch of points: block i holds the bits of point i.

def Cslib.BitString.lineBits {K : Type u_1} {ℓ b s t : ℕ} [Semiring K] (bits : K ≃+ BitString b) (scalar : Fin s → K) (targets directions : Fin t → Fin ℓ → K) : BitString (t * (s * (ℓ * b)))

The listed points of a batch of lines: block i lists, for each scalar index j, the bits of targets i + scalar j • directions i.