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 : ℕ} (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.

def Cslib.BitString.pointEquiv {K : Type u_1} {ℓ b : ℕ} (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 : ℕ} (bits : K ≃ BitString b) (u : Fin ℓ → K) : (pointEquiv bits) u = pointBits (⇑bits) u

pointEquiv bits sends a point to its bits pointBits bits.

@[simp]

theorem Cslib.BitString.pointEquiv_symm_apply {K : Type u_1} {ℓ b : ℕ} (bits : K ≃ BitString b) (y : BitString (ℓ * b)) (i : Fin ℓ) : (pointEquiv bits).symm y i = bits.symm (block y i)

(pointEquiv bits).symm decodes coordinate i from block i (Cslib.BitString.block).

@[simp]

theorem Cslib.BitString.pointEquiv_symm_pointBits {K : Type u_1} {ℓ b : ℕ} (bits : K ≃ BitString b) (u : Fin ℓ → K) : (pointEquiv bits).symm (pointBits (⇑bits) u) = u

Decoding the bits of a point gives the point back.

@[simp]

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

Decoding the bits of a point (under an additive equivalence) gives the point back.

@[simp]

theorem Cslib.BitString.pointBits_pointEquiv_symm {K : Type u_1} {ℓ b : ℕ} (bits : K ≃ BitString b) (y : BitString (ℓ * b)) : pointBits (⇑bits) ((pointEquiv bits).symm y) = y

Encoding the point with given bits gives the bits back.

theorem Cslib.BitString.pointBits_injective {K : Type u_1} {ℓ b : ℕ} {E : Type u_2} [EquivLike E K (BitString b)] (bits : E) : Function.Injective (pointBits ⇑bits)

Distinct points have distinct 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.