Binary polynomial arithmetic on bitvectors

TheoremDegree bound for a polynomial built from a coefficient list#✓fully proved

A polynomial built from a low-coefficient-first list has degree strictly less than the list length, including for an empty list and over a trivial semiring.

theorem degree_ofCoeffList_lt {R : Type*} [Semiring R] (l : List R) :
    (ofCoeffList l).degree < (l.length : WithBot Nat)

Used by 4

Used byFixed-width binary words as residues modulo a monic polynomial · Remainder coefficients of an encoded binary word are its bits · The binary modulus is monic · Degree of the binary modulus

TheoremReconstructing a polynomial from a fixed-width coefficient list#✓fully proved

Reconstruct a polynomial from any fixed-width list containing all its possibly nonzero coefficients.

theorem ofCoeffList_ofFn_coeff {R : Type*} [Semiring R] (p : Polynomial R) (s : Nat)
    (h : p.degree < (s : WithBot Nat)) :
    ofCoeffList (List.ofFn fun i : Fin s => p.coeff i.val) = p

DefinitionBitvector of the low coefficients of a binary polynomial#✓fully proved

Extract the lowest s binary coefficients of a polynomial as a fixed-width bitvector. Coefficients at indices at least s are deliberately truncated.

noncomputable def toBitVec (s : Nat) (p : Polynomial (ZMod 2)) : BitVec s :=
  (BitVec.ofBoolListLE (List.ofFn fun i : Fin s => decide (p.coeff i.val = 1))).cast
    List.length_ofFn

Used by 5

Used byFixed-width binary words as residues modulo a monic polynomial · Inverse map of the binary word residue equivalence · Bitvector encoding recovers the original word · Polynomial encoding recovers a low-degree polynomial · Exhaustive search returns an irreducible binary modulus

DefinitionBinary polynomial of a bitvector#✓fully proved

The polynomial over ZMod 2 whose coefficient of X ^ i is the i-th least-significant bit of w.

noncomputable def toPolynomial {s : Nat} (w : BitVec s) : Polynomial (ZMod 2) :=
  Polynomial.ofCoeffList (w.toBoolListLE.map fun b => if b then 1 else 0)

Uses 1 · Used by 20

Statement usesLittle-endian bits of a bitvector

Used byFixed-width binary words as residues modulo a monic polynomial · Forward map of the binary word residue equivalence · Remainder coefficients of an encoded binary word are its bits · Modular multiplication matches the polynomial quotient · Modular multiplication by \(X\) matches the quotient root · Modular powering matches the polynomial quotient · Bitwise xor corresponds to residue addition · Reduction of the root power in a binary residue ring · Coefficients of the binary polynomial of a bitvector · Evaluation of modular Horner multiplication · Evaluation of modular multiplication by \(X\) · Evaluation of modular powering · Monic binary modulus of a fixed-width word · The binary modulus is monic · Degree of the binary modulus · Bitvector encoding recovers the original word · Polynomial encoding recovers a low-degree polynomial · Bitwise xor corresponds to polynomial addition over \(\mathbb{F}_2\) · Exhaustive search returns an irreducible binary modulus · Inverse test succeeds exactly for irreducible moduli

TheoremCoefficients of the binary polynomial of a bitvector#✓fully proved

Every coefficient of the polynomial encoding is the corresponding least-significant bit; indices outside the fixed width have coefficient zero.

theorem coeff_toPolynomial {s : Nat} (w : BitVec s) (i : Nat) :
    w.toPolynomial.coeff i = if w.getLsbD i then 1 else 0

Uses 2 · Used by 10

Statement usesBinary polynomial of a bitvector

Proof usesLittle-endian bits of a bitvector

Used byRemainder coefficients of an encoded binary word are its bits · Reduction of the root power in a binary residue ring · Evaluation of modular Horner multiplication · Evaluation of modular multiplication by \(X\) · Evaluation of modular powering · Bitvector encoding recovers the original word · Polynomial encoding recovers a low-degree polynomial · Bitwise xor corresponds to polynomial addition over \(\mathbb{F}_2\) · Exhaustive search returns an irreducible binary modulus · Inverse test succeeds exactly for irreducible moduli

TheoremBitvector encoding recovers the original word#✓fully proved

Extracting the coefficients of an encoded word recovers the original fixed-width word.

@[simp] theorem toBitVec_toPolynomial {s : Nat} (w : BitVec s) :
    w.toPolynomial.toBitVec s = w

Uses 3 · Used by 1

Statement usesBinary polynomial of a bitvector · Bitvector of the low coefficients of a binary polynomial

Proof usesCoefficients of the binary polynomial of a bitvector

Used byFixed-width binary words as residues modulo a monic polynomial

TheoremPolynomial encoding recovers a low-degree polynomial#✓fully proved

A polynomial whose degree is below the selected width is recovered after coefficient extraction and fixed-width encoding.

@[simp] theorem toPolynomial_toBitVec (s : Nat) (p : Polynomial (ZMod 2))
    (h : p.degree < (s : WithBot Nat)) : (p.toBitVec s).toPolynomial = p

Uses 3 · Used by 1

Statement usesBinary polynomial of a bitvector · Bitvector of the low coefficients of a binary polynomial

Proof usesCoefficients of the binary polynomial of a bitvector

Used byFixed-width binary words as residues modulo a monic polynomial

TheoremBitwise xor corresponds to polynomial addition over \(\mathbb{F}_2\)#✓fully proved

Polynomial encoding turns bitwise xor into addition over ZMod 2; this is not the carried integer addition on bitvectors.

theorem toPolynomial_xor {s : Nat} (x y : BitVec s) :
    (x ^^^ y).toPolynomial = x.toPolynomial + y.toPolynomial

Uses 2 · Used by 3

Statement usesBinary polynomial of a bitvector

Proof usesCoefficients of the binary polynomial of a bitvector

Used byBitwise xor corresponds to residue addition · Evaluation of modular Horner multiplication · Evaluation of modular multiplication by \(X\)

DefinitionMonic binary modulus of a fixed-width word#✓fully proved

The monic polynomial obtained by adjoining the width term X ^ s to the encoded lower coefficients.

noncomputable def monicModulus {s : Nat} (g : BitVec s) : Polynomial (ZMod 2) :=
  Polynomial.X ^ s + g.toPolynomial

Uses 1 · Used by 14

Statement usesBinary polynomial of a bitvector

Used byFixed-width binary words as residues modulo a monic polynomial · Forward map of the binary word residue equivalence · Remainder coefficients of an encoded binary word are its bits · Modular multiplication matches the polynomial quotient · Modular multiplication by \(X\) matches the quotient root · Modular powering matches the polynomial quotient · Inverse map of the binary word residue equivalence · Bitwise xor corresponds to residue addition · Reduction of the root power in a binary residue ring · The binary modulus is monic · Degree of the binary modulus · Minimality of the binary modulus found by exhaustive search · Exhaustive search returns an irreducible binary modulus · Inverse test succeeds exactly for irreducible moduli

TheoremThe binary modulus is monic#✓fully proved

The binary modulus associated to a fixed-width word is monic, including at width zero.

theorem monicModulus_monic {s : Nat} (g : BitVec s) : g.monicModulus.Monic

Uses 4 · Used by 3

Statement usesMonic binary modulus of a fixed-width word

Proof usesLittle-endian bits of a bitvector · Binary polynomial of a bitvector · Degree bound for a polynomial built from a coefficient list

Used byFixed-width binary words as residues modulo a monic polynomial · Remainder coefficients of an encoded binary word are its bits · Inverse map of the binary word residue equivalence

TheoremDegree of the binary modulus#✓fully proved

The natural degree of the binary modulus is exactly the width of its lower coefficients.

theorem monicModulus_natDegree {s : Nat} (g : BitVec s) : g.monicModulus.natDegree = s

Uses 4 · Used by 2

Statement usesMonic binary modulus of a fixed-width word

Proof usesLittle-endian bits of a bitvector · Binary polynomial of a bitvector · Degree bound for a polynomial built from a coefficient list

Used byFixed-width binary words as residues modulo a monic polynomial · Remainder coefficients of an encoded binary word are its bits

DefinitionFixed-width binary words as residues modulo a monic polynomial#✓fully proved

Fixed-width binary words are in bijection with residues modulo their associated monic polynomial. This is an ordinary equivalence because builtin bitvector addition has carries.

BitVec.adjoinRootEquiv · 29 lines

noncomputable def adjoinRootEquiv {s : Nat} (g : BitVec s) :
    BitVec s ≃ AdjoinRoot g.monicModulus where
  toFun w := AdjoinRoot.mk g.monicModulus w.toPolynomial
  invFun z := (AdjoinRoot.modByMonicHom g.monicModulus_monic z).toBitVec s
  left_inv w := by
    change (AdjoinRoot.modByMonicHom g.monicModulus_monic
      (AdjoinRoot.mk g.monicModulus w.toPolynomial)).toBitVec s = w
    rw [AdjoinRoot.modByMonicHom_mk,
      (Polynomial.modByMonic_eq_self_iff g.monicModulus_monic).mpr,
      BitVec.toBitVec_toPolynomial]
    rw [Polynomial.degree_eq_natDegree g.monicModulus_monic.ne_zero,
      g.monicModulus_natDegree]
    exact degree_toPolynomial_lt w
  right_inv z := by
    obtain ⟨p, rfl⟩ := AdjoinRoot.mk_surjective z
    change AdjoinRoot.mk g.monicModulus
      ((AdjoinRoot.modByMonicHom g.monicModulus_monic
        (AdjoinRoot.mk g.monicModulus p)).toBitVec s).toPolynomial =
        AdjoinRoot.mk g.monicModulus p
    rw [AdjoinRoot.modByMonicHom_mk,
      Polynomial.toPolynomial_toBitVec s _ (by
        calc
          _ < g.monicModulus.degree :=
            Polynomial.degree_modByMonic_lt _ g.monicModulus_monic
          _ = (s : WithBot Nat) := by
            rw [Polynomial.degree_eq_natDegree g.monicModulus_monic.ne_zero,
              g.monicModulus_natDegree])]
    simpa using AdjoinRoot.mk_leftInverse g.monicModulus_monic
      (AdjoinRoot.mk g.monicModulus p)

Uses 9 · Used by 9

Statement usesMonic binary modulus of a fixed-width word · The binary modulus is monic · Degree of the binary modulus · Bitvector encoding recovers the original word · Little-endian bits of a bitvector · Binary polynomial of a bitvector · Degree bound for a polynomial built from a coefficient list · Bitvector of the low coefficients of a binary polynomial · Polynomial encoding recovers a low-degree polynomial

Used byForward map of the binary word residue equivalence · Remainder coefficients of an encoded binary word are its bits · Modular multiplication matches the polynomial quotient · Modular multiplication by \(X\) matches the quotient root · Modular powering matches the polynomial quotient · Inverse map of the binary word residue equivalence · Bitwise xor corresponds to residue addition · Reduction of the root power in a binary residue ring · Inverse test succeeds exactly for irreducible moduli

TheoremForward map of the binary word residue equivalence#✓fully proved

The forward equivalence is the canonical quotient constructor applied to the polynomial encoding.

@[simp] theorem adjoinRootEquiv_apply {s : Nat} (g w : BitVec s) :
    g.adjoinRootEquiv w = AdjoinRoot.mk g.monicModulus w.toPolynomial

Uses 3 · Used by 7

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word · Binary polynomial of a bitvector

Used byRemainder coefficients of an encoded binary word are its bits · Modular multiplication matches the polynomial quotient · Modular multiplication by \(X\) matches the quotient root · Modular powering matches the polynomial quotient · Bitwise xor corresponds to residue addition · Reduction of the root power in a binary residue ring · Inverse test succeeds exactly for irreducible moduli

TheoremInverse map of the binary word residue equivalence#✓fully proved

The inverse equivalence extracts the canonical remainder's lowest s binary coefficients.

@[simp] theorem adjoinRootEquiv_symm_apply {s : Nat} (g : BitVec s)
    (z : AdjoinRoot g.monicModulus) :
    g.adjoinRootEquiv.symm z =
      (AdjoinRoot.modByMonicHom g.monicModulus_monic z).toBitVec s

Uses 4

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word · The binary modulus is monic · Bitvector of the low coefficients of a binary polynomial

TheoremRemainder coefficients of an encoded binary word are its bits#✓fully proved

The canonical remainder coordinates of an encoded word are exactly its low-first bits.

theorem adjoinRootEquiv_coeff {s : Nat} (g w : BitVec s) (i : Fin s) :
    (AdjoinRoot.modByMonicHom g.monicModulus_monic
      (g.adjoinRootEquiv w)).coeff i.val = if w.getLsbD i.val then 1 else 0

Uses 9

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word · The binary modulus is monic

Proof usesForward map of the binary word residue equivalence · Coefficients of the binary polynomial of a bitvector · Degree of the binary modulus · Little-endian bits of a bitvector · Binary polynomial of a bitvector · Degree bound for a polynomial built from a coefficient list

TheoremBitwise xor corresponds to residue addition#✓fully proved

Bitwise xor corresponds to quotient addition; builtin bitvector addition does not.

theorem adjoinRootEquiv_xor {s : Nat} (g x y : BitVec s) :
    g.adjoinRootEquiv (x ^^^ y) = g.adjoinRootEquiv x + g.adjoinRootEquiv y

Uses 5 · Used by 1

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word

Proof usesForward map of the binary word residue equivalence · Binary polynomial of a bitvector · Bitwise xor corresponds to polynomial addition over \(\mathbb{F}_2\)

Used byReduction of the root power in a binary residue ring

TheoremReduction of the root power in a binary residue ring#✓fully proved

The defining quotient equation reduces root ^ s to the encoded lower coefficients.

theorem adjoinRoot_root_pow {s : Nat} (g : BitVec s) :
    AdjoinRoot.root g.monicModulus ^ s = g.adjoinRootEquiv g

Uses 6 · Used by 3

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word

Proof usesForward map of the binary word residue equivalence · Bitwise xor corresponds to residue addition · Coefficients of the binary polynomial of a bitvector · Binary polynomial of a bitvector

Used byModular multiplication matches the polynomial quotient · Modular multiplication by \(X\) matches the quotient root · Modular powering matches the polynomial quotient

DefinitionMultiplication by \(X\) of a binary polynomial residue#✓fully proved

Multiply a binary residue by X, reducing by X ^ s + g when its top bit is set.

def mulXMod {s : Nat} (g w : BitVec s) : BitVec s :=
  if w.getMsbD 0 then w.shiftLeft 1 ^^^ g else w.shiftLeft 1

Used by 4

Used byModular multiplication by \(X\) matches the quotient root · Evaluation of modular Horner multiplication · Evaluation of modular multiplication by \(X\) · Modular multiplication of binary polynomial residues

DefinitionModular multiplication of binary polynomial residues#✓fully proved

Multiply binary residues by low-first Horner evaluation of the second operand's bits.

def mulMod {s t : Nat} (g x : BitVec s) (y : BitVec t) : BitVec s :=
  y.toBoolListLE.foldr
    (fun b c => if b then x ^^^ g.mulXMod c else g.mulXMod c) (0#s)

Uses 2 · Used by 6

Statement usesMultiplication by \(X\) of a binary polynomial residue · Little-endian bits of a bitvector

Used byModular multiplication matches the polynomial quotient · Evaluation of modular Horner multiplication · Evaluation of modular powering · Modular powering of binary polynomial residues · Exhaustive inverse test for a binary polynomial modulus · Inverse test succeeds exactly for irreducible moduli

DefinitionModular powering of binary polynomial residues#✓fully proved

Raise a binary residue to a natural power by tail-recursive repeated multiplication.

def powMod {s t : Nat} (g : BitVec s) (u : BitVec t) (e : Nat) : BitVec s :=
  Nat.foldTR e (fun _ _ c => g.mulMod c u) (1#s)

Uses 1 · Used by 2

Statement usesModular multiplication of binary polynomial residues

Used byModular powering matches the polynomial quotient · Evaluation of modular powering

TheoremEvaluation of modular multiplication by \(X\)#✓fully proved

Multiplication by X has its expected evaluation in every commutative ring receiving ZMod 2.

theorem eval₂_mulXMod {s : Nat} {R : Type*} [CommRing R]
    (φ : ZMod 2 →+* R) (r : R) (g w : BitVec s)
    (hr : r ^ s = g.toPolynomial.eval₂ φ r) :
    (g.mulXMod w).toPolynomial.eval₂ φ r =
      r * w.toPolynomial.eval₂ φ r

Uses 4 · Used by 2

Statement usesMultiplication by \(X\) of a binary polynomial residue · Binary polynomial of a bitvector

Proof usesCoefficients of the binary polynomial of a bitvector · Bitwise xor corresponds to polynomial addition over \(\mathbb{F}_2\)

Used byModular multiplication by \(X\) matches the quotient root · Evaluation of modular Horner multiplication

TheoremEvaluation of modular Horner multiplication#✓fully proved

Horner multiplication has its expected evaluation in every commutative ring receiving ZMod 2; the second operand may have any width.

theorem eval₂_mulMod {s t : Nat} {R : Type*} [CommRing R]
    (φ : ZMod 2 →+* R) (r : R) (g x : BitVec s) (y : BitVec t)
    (hr : r ^ s = g.toPolynomial.eval₂ φ r) :
    (g.mulMod x y).toPolynomial.eval₂ φ r =
      x.toPolynomial.eval₂ φ r * y.toPolynomial.eval₂ φ r

Uses 7 · Used by 2

Statement usesModular multiplication of binary polynomial residues · Binary polynomial of a bitvector

Proof usesCoefficients of the binary polynomial of a bitvector · Evaluation of modular multiplication by \(X\) · Multiplication by \(X\) of a binary polynomial residue · Little-endian bits of a bitvector · Bitwise xor corresponds to polynomial addition over \(\mathbb{F}_2\)

Used byModular multiplication matches the polynomial quotient · Evaluation of modular powering

TheoremEvaluation of modular powering#✓fully proved

Repeated multiplication has its expected power evaluation for positive result width.

theorem eval₂_powMod {s t : Nat} {R : Type*} [CommRing R]
    (φ : ZMod 2 →+* R) (r : R) (g : BitVec s) (u : BitVec t) (e : Nat)
    (hs : 0 < s) (hr : r ^ s = g.toPolynomial.eval₂ φ r) :
    (g.powMod u e).toPolynomial.eval₂ φ r =
      (u.toPolynomial.eval₂ φ r) ^ e

Uses 5 · Used by 1

Statement usesModular powering of binary polynomial residues · Binary polynomial of a bitvector

Proof usesCoefficients of the binary polynomial of a bitvector · Evaluation of modular Horner multiplication · Modular multiplication of binary polynomial residues

Used byModular powering matches the polynomial quotient

TheoremModular multiplication by \(X\) matches the quotient root#✓fully proved

Modular multiplication by X agrees with multiplication by the quotient root.

theorem adjoinRootEquiv_mulXMod {s : Nat} (g w : BitVec s) :
    g.adjoinRootEquiv (g.mulXMod w) =
      AdjoinRoot.root g.monicModulus * g.adjoinRootEquiv w

Uses 7

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word · Multiplication by \(X\) of a binary polynomial residue

Proof usesForward map of the binary word residue equivalence · Reduction of the root power in a binary residue ring · Evaluation of modular multiplication by \(X\) · Binary polynomial of a bitvector

TheoremModular multiplication matches the polynomial quotient#✓fully proved

Modular Horner multiplication agrees with multiplication in the polynomial quotient.

theorem adjoinRootEquiv_mulMod {s t : Nat} (g x : BitVec s) (y : BitVec t) :
    g.adjoinRootEquiv (g.mulMod x y) =
      g.adjoinRootEquiv x * AdjoinRoot.mk g.monicModulus y.toPolynomial

Uses 7 · Used by 1

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word · Modular multiplication of binary polynomial residues · Binary polynomial of a bitvector

Proof usesForward map of the binary word residue equivalence · Reduction of the root power in a binary residue ring · Evaluation of modular Horner multiplication

Used byInverse test succeeds exactly for irreducible moduli

TheoremModular powering matches the polynomial quotient#✓fully proved

Modular powering agrees with powering in the polynomial quotient, including width zero.

theorem adjoinRootEquiv_powMod {s t : Nat} (g : BitVec s) (u : BitVec t) (e : Nat) :
    g.adjoinRootEquiv (g.powMod u e) =
      (AdjoinRoot.mk g.monicModulus u.toPolynomial) ^ e

Uses 7

Statement usesFixed-width binary words as residues modulo a monic polynomial · Monic binary modulus of a fixed-width word · Modular powering of binary polynomial residues · Binary polynomial of a bitvector

Proof usesForward map of the binary word residue equivalence · Reduction of the root power in a binary residue ring · Evaluation of modular powering

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.