def Hex.GFq.packedGF2FpPoly (lower : UInt64) (n : Nat) : FpPoly 2

Interpret a packed single-word binary modulus as the corresponding generic FpPoly 2 polynomial. lower supplies the coefficients of degrees < n; the leading degree-n coefficient is inserted explicitly.

Equations

• Hex.GFq.packedGF2FpPoly lower n = Hex.FpPoly.ofCoeffs ((List.map (fun (i : Nat) => if lower >>> i.toUInt64 &&& 1 = 0 then 0 else 1) (List.range n)).toArray.push 1)

class Hex.GFq.PackedGF2Entry (n : Nat) : Type

A committed Conway-table entry at p = 2 that is also available as a single-word packed GF2n modulus. The lower field stores the lower coefficients of the monic degree-n modulus; the leading x^n coefficient is implicit in GF2Poly.ofUInt64Monic lower n.

• entry : Conway.SupportedEntry 2 n
• lower : UInt64
• conway_eq_packed : Conway.conwayPoly 2 n entry = packedGF2FpPoly (lower n) n
• degree_pos : 0 < n
• degree_lt_word : n < 64
• packed_irreducible : (GF2Poly.ofUInt64Monic (lower n) n).Irreducible

theorem Hex.GFq.packedGF2Entry_2_1_irreducible : (GF2Poly.ofUInt64Monic 1 1).Irreducible

The packed modulus corresponding to the committed Conway entry C(2, 1) = X + 1.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_1 : PackedGF2Entry 1

The current committed table supports a packed GF2n view of C(2, 1).

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GFq.packedGF2Entry_2_2_irreducible : (GF2Poly.ofUInt64Monic 3 2).Irreducible

The packed Conway modulus for C(2, 2) (0x3) is irreducible, checked from its certificate.

theorem Hex.GFq.packedGF2Entry_2_3_irreducible : (GF2Poly.ofUInt64Monic 3 3).Irreducible

The packed Conway modulus for C(2, 3) (0x3) is irreducible, checked from its certificate.

theorem Hex.GFq.packedGF2Entry_2_5_irreducible : (GF2Poly.ofUInt64Monic 5 5).Irreducible

The packed Conway modulus for C(2, 5) (0x5) is irreducible, checked from its certificate.

theorem Hex.GFq.packedGF2Entry_2_6_irreducible : (GF2Poly.ofUInt64Monic 27 6).Irreducible

The packed Conway modulus for C(2, 6) (0x1B) is irreducible, checked from its certificate.

theorem Hex.GFq.packedGF2Entry_2_7_irreducible : (GF2Poly.ofUInt64Monic 3 7).Irreducible

The packed Conway modulus for C(2, 7) (0x3) is irreducible, checked from its certificate.

theorem Hex.GFq.packedGF2Entry_2_8_irreducible : (GF2Poly.ofUInt64Monic 29 8).Irreducible

The packed Conway modulus for C(2, 8) (0x1D) is irreducible, checked from its certificate.

This is not the AES modulus. AES uses x^8 + x^4 + x^3 + x + 1 (0x1B), a different irreducible of the same degree, so GF2q 8 and the AES field are different presentations of the same 256-element field.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_2 : PackedGF2Entry 2

The committed table supports a packed GF2n view of C(2, 2).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_3 : PackedGF2Entry 3

The committed table supports a packed GF2n view of C(2, 3).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_4 : PackedGF2Entry 4

The committed table supports a packed GF2n view of C(2, 4).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_5 : PackedGF2Entry 5

The committed table supports a packed GF2n view of C(2, 5).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_6 : PackedGF2Entry 6

The committed table supports a packed GF2n view of C(2, 6).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_7 : PackedGF2Entry 7

The committed table supports a packed GF2n view of C(2, 7).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GFq.packedGF2Entry_2_8 : PackedGF2Entry 8

The committed table supports a packed GF2n view of C(2, 8).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Hex.GFq (p n : Nat) [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : Type

Canonical finite field with p^n elements for a committed Conway-table entry, using the generic quotient-field representation.

Equations

• Hex.GFq p n h = Hex.GFqField.FiniteField (Hex.Conway.conwayPoly p n h) ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Hex.GFq.modulus {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : FpPoly p

The Conway modulus selected for a committed GFq p n entry.

Equations

• Hex.GFq.modulus h = Hex.Conway.conwayPoly p n h

@[simp]

theorem Hex.GFq.modulus_eq_conway {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : modulus h = Conway.conwayPoly p n h

GFq.modulus is the Conway polynomial selected by the committed entry.

@[simp]

theorem Hex.GFq.modulus_nonconstant {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : 0 < (modulus h).degree

The selected Conway modulus has positive degree.

theorem Hex.GFq.modulus_irreducible {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : (modulus h).Irreducible

The selected Conway modulus is irreducible.

theorem Hex.GFq.modulus_prime {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : Nat.Prime p

The selected Conway modulus lives over a prime base field.

def Hex.GFq.ofPoly {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) (g : FpPoly p) : GFq p n h

Reduce a polynomial into the canonical field selected by a committed Conway entry.

The entry already carries h.prime, so this needs no separate prime-modulus instance from the caller.

Equations

• Hex.GFq.ofPoly h g = Hex.GFqField.ofPoly (Hex.GFq.modulus h) ⋯ ⋯ ⋯ g

@[simp]

theorem Hex.GFq.ofPoly_eq_field_ofPoly {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) (g : FpPoly p) : ofPoly h g = GFqField.ofPoly (modulus h) ⋯ ⋯ ⋯ g

GFq.ofPoly delegates to the generic quotient-field constructor with the selected Conway modulus.

def Hex.GFq.repr {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) : FpPoly p

Project a canonical field element to its reduced polynomial representative.

Equations

• x.repr = Hex.GFqField.repr x

@[simp]

theorem Hex.GFq.repr_eq_field_repr {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) : x.repr = GFqField.repr x

GFq.repr is the generic quotient-field representative projection.

theorem Hex.GFq.ext {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} {x y : GFq p n h} (hxy : x.repr = y.repr) : x = y

Two canonical GFq elements are equal when their reduced polynomial representatives agree.

theorem Hex.GFq.ext_iff {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} {x y : GFq p n h} : x = y ↔ x.repr = y.repr

@[simp]

theorem Hex.GFq.repr_ofPoly {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) (g : FpPoly p) : (ofPoly h g).repr = GFqRing.reduceMod (modulus h) g

The canonical representative of an injected FpPoly is that polynomial reduced modulo the selected Conway polynomial. Lets a caller normalise a repr (ofPoly h g) round-trip to a plain reduceMod.

@[simp]

theorem Hex.GFq.repr_zero {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (h : Conway.SupportedEntry p n) : repr 0 = GFqRing.reduceMod (modulus h) 0

The canonical representative of 0 in GFq is reduction of 0 modulo the selected Conway polynomial.

@[simp]

theorem Hex.GFq.repr_one {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (h : Conway.SupportedEntry p n) : repr 1 = GFqRing.reduceMod (modulus h) 1

The canonical representative of 1 in GFq is reduction of 1 modulo the selected Conway polynomial.

@[simp]

theorem Hex.GFq.repr_add {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x y : GFq p n h) : (x + y).repr = GFqRing.reduceMod (modulus h) (x.repr + y.repr)

The canonical representative of a sum in GFq reduces from the sum of representatives modulo the selected Conway polynomial.

@[simp]

theorem Hex.GFq.repr_mul {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x y : GFq p n h) : (x * y).repr = GFqRing.reduceMod (modulus h) (x.repr * y.repr)

The canonical representative of a product in GFq reduces from the product of representatives modulo the selected Conway polynomial.

@[simp]

theorem Hex.GFq.repr_neg {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) : (-x).repr = GFqRing.reduceMod (modulus h) (-x.repr)

The representative of a negation reduces from the negated representative.

@[simp]

theorem Hex.GFq.repr_sub {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x y : GFq p n h) : (x - y).repr = GFqRing.reduceMod (modulus h) (x.repr - y.repr)

The representative of a subtraction reduces from the difference of representatives.

@[simp]

theorem Hex.GFq.repr_natCast {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (h : Conway.SupportedEntry p n) (k : Nat) : (↑k).repr = GFqRing.reduceMod (modulus h) (FpPoly.C ↑k)

The canonical representative of a natural literal in GFq is the reduction modulo the selected Conway polynomial of the constant polynomial carrying the literal as a ZMod64 coefficient.

@[simp]

theorem Hex.GFq.repr_div {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x y : GFq p n h) : (x / y).repr = GFqRing.repr (x.toQuotient * (GFqField.inv y).toQuotient)

The canonical representative of a quotient in GFq lifts the quotient-ring product of the dividend's representative with the inverse of the divisor.

@[simp]

theorem Hex.GFq.repr_pow {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) (k : Nat) : (x ^ k).repr = GFqRing.repr (x.toQuotient ^ k)

The canonical representative of a natural power in GFq lifts the quotient-ring power of the underlying quotient representative.

@[simp]

theorem Hex.GFq.repr_zpow_ofNat {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) (k : Nat) : repr (x ^ Int.ofNat k) = GFqRing.repr (x.toQuotient ^ k)

The canonical representative of a nonnegative integer power in GFq lifts the quotient-ring power of the underlying quotient representative.

@[simp]

theorem Hex.GFq.repr_zpow_negSucc {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) (k : Nat) : repr (x ^ Int.negSucc k) = GFqRing.repr (GFqField.inv (GFqField.pow x (k + 1))).toQuotient

The canonical representative of a negative integer power in GFq lifts the inverse of the corresponding quotient-ring positive power.

@[simp]

theorem Hex.GFq.repr_intCast {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (h : Conway.SupportedEntry p n) (i : Int) : (↑i).repr = GFqRing.repr ↑i

The canonical representative of an integer literal in GFq lifts the quotient-ring integer-cast representative.

@[simp]

theorem Hex.GFq.repr_nsmul {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (k : Nat) (x : GFq p n h) : (k • x).repr = GFqRing.repr (k • x.toQuotient)

The representative of a natural scalar action lifts the quotient-ring action.

@[simp]

theorem Hex.GFq.repr_zsmul {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (k : Int) (x : GFq p n h) : (k • x).repr = GFqRing.repr (k • x.toQuotient)

The representative of an integer scalar action lifts the quotient-ring action.

@[simp]

theorem Hex.GFq.repr_inv_zero {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (h : Conway.SupportedEntry p n) : 0⁻¹.repr = GFqRing.reduceMod (modulus h) 0

The zero inverse in GFq follows the field wrapper's junk-value convention and has zero representative.

@[simp]

theorem Hex.GFq.inv_zero {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (h : Conway.SupportedEntry p n) : 0⁻¹ = 0

The zero inverse in GFq follows the field wrapper's junk-value convention.

theorem Hex.GFq.div_eq_mul_inv {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x y : GFq p n h) : x / y = x * y⁻¹

Division in GFq is multiplication by inverse.

theorem Hex.GFq.mul_inv_cancel {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {h : Conway.SupportedEntry p n} {x : GFq p n h} (hx : x ≠ 0) : x * x⁻¹ = 1

A nonzero GFq element cancels against its inverse on the right.

theorem Hex.GFq.inv_mul_cancel {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {h : Conway.SupportedEntry p n} {x : GFq p n h} (hx : x ≠ 0) : x⁻¹ * x = 1

A nonzero GFq element cancels against its inverse on the left.

theorem Hex.GFq.ofPoly_eq_ofPoly_iff_reduceMod_eq {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) (f g : FpPoly p) : ofPoly h f = ofPoly h g ↔ GFqRing.reduceMod (modulus h) f = GFqRing.reduceMod (modulus h) g

Two GFq.ofPoly constructors produce the same field element exactly when their inputs have the same reduced representative modulo the selected Conway polynomial.

@[simp]

theorem Hex.GFq.ofPoly_reduceMod {p n : Nat} [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) (f : FpPoly p) : ofPoly h (GFqRing.reduceMod (modulus h) f) = ofPoly h f

Injecting an FpPoly into GFq is invariant under pre-reduction modulo the selected Conway polynomial: a caller may drop a reduceMod already sitting under ofPoly.

def Hex.GFq.frob {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) : GFq p n h

The Frobenius endomorphism on the canonical Conway-backed field, computed as the p-th power on the underlying quotient representation.

Equations

• x.frob = Hex.GFqField.frob x

theorem Hex.GFq.frob_eq_pow {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) : x.frob = x ^ p

GFq.frob is the p-th power map.

@[simp]

theorem Hex.GFq.repr_frob {p n : Nat} [ZMod64.Bounds p] {h : Conway.SupportedEntry p n} (x : GFq p n h) : x.frob.repr = GFqRing.repr (x.toQuotient ^ p)

The representative of GFq.frob is the quotient-ring p-th power representative.

@[reducible, inline]

abbrev Hex.GFqC (p n : Nat) [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] : Type

Ergonomic generic finite field for a committed Conway-table entry.

Use GFqC p n when the committed entry should be inferred from the current Conway table. Use explicit GFq p n h when a proof needs to name the witness.

Equations

• Hex.GFqC p n = Hex.GFq p n Hex.GFq.CommittedEntry.entry

@[reducible, inline]

abbrev Hex.GFqC.entry {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] : Conway.SupportedEntry p n

The committed Conway-table entry selected for GFqC p n.

Equations

• Hex.GFqC.entry = Hex.GFq.CommittedEntry.entry

@[reducible, inline]

abbrev Hex.GFqC.modulus {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] : FpPoly p

The Conway modulus selected for the committed GFqC p n field.

Equations

• Hex.GFqC.modulus = Hex.GFq.modulus Hex.GFqC.entry

theorem Hex.GFqC.modulus_eq_gfq {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] : modulus = GFq.modulus entry

Hex.GFqC.modulus delegates to the explicit-entry Hex.GFq.modulus.

def Hex.GFqC.ofPoly {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (g : FpPoly p) : GFqC p n

Reduce a polynomial into the committed GFqC p n field.

Equations

• Hex.GFqC.ofPoly g = Hex.GFq.ofPoly Hex.GFqC.entry g

theorem Hex.GFqC.ofPoly_eq_gfq {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (g : FpPoly p) : ofPoly g = GFq.ofPoly entry g

GFqC.ofPoly delegates to the explicit-entry GFq.ofPoly.

def Hex.GFqC.repr {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x : GFqC p n) : FpPoly p

Project a committed GFqC element to its reduced polynomial representative.

Equations

• x.repr = Hex.GFq.repr x

theorem Hex.GFqC.repr_eq_gfq {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x : GFqC p n) : x.repr = GFq.repr x

GFqC.repr delegates to the explicit-entry GFq.repr.

@[simp]

theorem Hex.GFqC.repr_ofPoly {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (g : FpPoly p) : (ofPoly g).repr = GFqRing.reduceMod modulus g

The representative of an injected polynomial is reduction modulo the selected committed Conway polynomial.

@[simp]

theorem Hex.GFqC.repr_add {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x y : GFqC p n) : (x + y).repr = GFqRing.reduceMod modulus (x.repr + y.repr)

The canonical representative of a sum in GFqC reduces from the sum of representatives modulo the selected committed Conway polynomial.

@[simp]

theorem Hex.GFqC.repr_mul {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x y : GFqC p n) : (x * y).repr = GFqRing.reduceMod modulus (x.repr * y.repr)

The canonical representative of a product in GFqC reduces from the product of representatives modulo the selected committed Conway polynomial.

def Hex.GFqC.frob {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x : GFqC p n) : GFqC p n

The Frobenius endomorphism on the committed GFqC p n field.

Equations

• x.frob = Hex.GFq.frob x

theorem Hex.GFqC.frob_eq_gfq {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x : GFqC p n) : x.frob = GFq.frob x

GFqC.frob delegates to the explicit-entry GFq.frob.

theorem Hex.GFqC.frob_eq_pow {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x : GFqC p n) : x.frob = x ^ p

GFqC.frob is the p-th power map.

@[simp]

theorem Hex.GFqC.repr_frob {p n : Nat} [ZMod64.Bounds p] [h : GFq.CommittedEntry p n] (x : GFqC p n) : x.frob.repr = GFqRing.repr (x.toQuotient ^ p)

The representative of GFqC.frob is the quotient-ring p-th power representative.

@[reducible, inline]

abbrev Hex.GF2q (n : Nat) [h : GFq.PackedGF2Entry n] : Type

Optimized canonical binary field for committed Conway entries that have a single-word packed modulus.

Equations

• Hex.GF2q n = Hex.GF2n n (Hex.GFq.PackedGF2Entry.lower n) ⋯ ⋯ ⋯

def Hex.GF2q.supportedEntry {n : Nat} [h : GFq.PackedGF2Entry n] : Conway.SupportedEntry 2 n

The supported Conway-table entry backing this optimized binary field.

Equations

• Hex.GF2q.supportedEntry = Hex.GFq.PackedGF2Entry.entry

@[simp]

theorem Hex.GF2q.supportedEntry_eq {n : Nat} [h : GFq.PackedGF2Entry n] : supportedEntry = GFq.PackedGF2Entry.entry

GF2q.supportedEntry is the committed packed Conway entry.

def Hex.GF2q.lower {n : Nat} [h : GFq.PackedGF2Entry n] : UInt64

The lower-word packed modulus selected for a committed optimized GF2q entry.

Equations

• Hex.GF2q.lower = Hex.GFq.PackedGF2Entry.lower n

@[simp]

theorem Hex.GF2q.lower_eq {n : Nat} [h : GFq.PackedGF2Entry n] : lower = GFq.PackedGF2Entry.lower n

GF2q.lower is the lower-word modulus stored in the packed entry.

def Hex.GF2q.modulus {n : Nat} [h : GFq.PackedGF2Entry n] : GF2Poly

The packed modulus polynomial selected for a committed optimized GF2q entry.

Equations

• Hex.GF2q.modulus = Hex.GF2Poly.ofUInt64Monic (Hex.GFq.PackedGF2Entry.lower n) n

@[simp]

theorem Hex.GF2q.modulus_eq_ofUInt64Monic {n : Nat} [h : GFq.PackedGF2Entry n] : modulus = GF2Poly.ofUInt64Monic (GFq.PackedGF2Entry.lower n) n

GF2q.modulus is the packed monic polynomial selected by the entry.

theorem Hex.GF2q.conway_eq_packed {n : Nat} [h : GFq.PackedGF2Entry n] : Conway.conwayPoly 2 n GFq.PackedGF2Entry.entry = GFq.packedGF2FpPoly (GFq.PackedGF2Entry.lower n) n

The packed modulus, viewed through the generic FpPoly 2 representation, is the committed Conway polynomial for this entry.

theorem Hex.GF2q.gfq_modulus_eq_packedFpPoly {n : Nat} [h : GFq.PackedGF2Entry n] : GFq.modulus GFq.PackedGF2Entry.entry = GFq.packedGF2FpPoly lower n

The generic GFq modulus for a packed binary entry agrees with the packed modulus viewed as an FpPoly 2.

@[simp]

theorem Hex.GF2q.degree_pos {n : Nat} [h : GFq.PackedGF2Entry n] : 0 < n

The selected packed modulus has positive extension degree.

@[simp]

theorem Hex.GF2q.degree_lt_word {n : Nat} [h : GFq.PackedGF2Entry n] : n < 64

The selected packed modulus fits in the single-word GF2n representation.

theorem Hex.GF2q.modulus_irreducible {n : Nat} [h : GFq.PackedGF2Entry n] : modulus.Irreducible

The selected packed modulus is irreducible.

def Hex.GF2q.ofWord {n : Nat} [h : GFq.PackedGF2Entry n] (w : UInt64) : GF2q n

Reduce a machine word into the optimized binary field selected by a committed packed Conway entry.

Equations

• Hex.GF2q.ofWord w = Hex.GF2n.reduce w

@[simp]

theorem Hex.GF2q.ofWord_eq_reduce {n : Nat} [h : GFq.PackedGF2Entry n] (w : UInt64) : ofWord w = GF2n.reduce w

GF2q.ofWord delegates to the packed GF2n reducer for the selected Conway modulus.

def Hex.GF2q.repr {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : UInt64

Project an optimized binary field element to its packed machine-word representative.

Equations

• x.repr = x.val

@[simp]

theorem Hex.GF2q.repr_eq_val {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : x.repr = x.val

GF2q.repr is the packed-word value stored by GF2n.

def Hex.GF2q.wordFpPoly {n : Nat} (w : UInt64) : FpPoly 2

Interpret the low n bits of a packed binary word as an FpPoly 2 polynomial.

Equations

• Hex.GF2q.wordFpPoly w = Hex.FpPoly.ofCoeffs (List.map (fun (i : Nat) => if w >>> i.toUInt64 &&& 1 = 0 then 0 else 1) (List.range n)).toArray

def Hex.GF2q.reprFpPoly {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : FpPoly 2

Interpret the packed representative of an optimized binary-field element as a generic FpPoly 2 polynomial.

Equations

• x.reprFpPoly = Hex.GF2q.wordFpPoly x.repr

def Hex.GF2q.toGFq {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : GFq 2 n supportedEntry

Map an optimized packed canonical binary-field element into the generic canonical GFq 2 n model for the same committed Conway entry.

Equations

• x.toGFq = Hex.GFq.ofPoly Hex.GF2q.supportedEntry x.reprFpPoly

@[simp]

theorem Hex.GF2q.reprFpPoly_eq_wordFpPoly {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : x.reprFpPoly = wordFpPoly x.repr

GF2q.reprFpPoly is the low-bit FpPoly 2 view of the packed representative.

@[simp]

theorem Hex.GF2q.toGFq_eq_ofPoly {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : x.toGFq = GFq.ofPoly supportedEntry x.reprFpPoly

GF2q.toGFq injects the packed representative through GFq.ofPoly.

@[simp]

theorem Hex.GF2q.toGFq_ofWord {n : Nat} [h : GFq.PackedGF2Entry n] (w : UInt64) : (ofWord w).toGFq = GFq.ofPoly supportedEntry (wordFpPoly (ofWord w).repr)

Bridging a packed word into GFq 2 n injects the reduced packed representative as an FpPoly 2.

@[simp]

theorem Hex.GF2q.toGFq_repr {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : x.toGFq.repr = GFqRing.reduceMod (GFq.modulus supportedEntry) x.reprFpPoly

The generic representative of GF2q.toGFq is the selected Conway-modulus reduction of the packed representative viewed as an FpPoly 2.

theorem Hex.GF2q.ext {n : Nat} [h : GFq.PackedGF2Entry n] {x y : GF2q n} (hxy : x.repr = y.repr) : x = y

Two optimized GF2q elements are equal when their packed representatives agree.

theorem Hex.GF2q.ext_iff {n : Nat} [h : GFq.PackedGF2Entry n] {x y : GF2q n} : x = y ↔ x.repr = y.repr

@[simp]

theorem Hex.GF2q.repr_ofWord {n : Nat} [h : GFq.PackedGF2Entry n] (w : UInt64) : (ofWord w).repr = (GF2n.reduce w).val

The packed representative of a word injected into GF2q is that word reduced into the field by GF2n.reduce, relating the raw UInt64 word to the canonical packed GF2q representation.

@[simp]

theorem Hex.GF2q.repr_zero {n : Nat} [h : GFq.PackedGF2Entry n] : repr 0 = 0

The packed representative of 0 in GF2q is the zero word.

@[simp]

theorem Hex.GF2q.repr_one {n : Nat} [h : GFq.PackedGF2Entry n] : repr 1 = 1

The packed representative of 1 in GF2q is the one word.

@[simp]

theorem Hex.GF2q.repr_natCast {n : Nat} [h : GFq.PackedGF2Entry n] (k : Nat) : (↑k).repr = (GF2n.natCast k).val

The packed representative of a natural-number literal is stored by the packed backend's characteristic-two natural cast.

@[simp]

theorem Hex.GF2q.repr_intCast {n : Nat} [h : GFq.PackedGF2Entry n] (k : Int) : (↑k).repr = (GF2n.intCast k).val

The packed representative of an integer literal is stored by the packed backend's characteristic-two integer cast.

@[simp]

theorem Hex.GF2q.repr_neg {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : (-x).repr = x.repr

In characteristic two, negation preserves the packed representative.

@[simp]

theorem Hex.GF2q.repr_sub {n : Nat} [h : GFq.PackedGF2Entry n] (x y : GF2q n) : (x - y).repr = (GF2n.reduce (x.repr ^^^ y.repr)).val

The packed representative of a subtraction is the reduced XOR of representatives.

@[simp]

theorem Hex.GF2q.repr_nsmul {n : Nat} [h : GFq.PackedGF2Entry n] (k : Nat) (x : GF2q n) : (k • x).repr = if k % 2 = 0 then 0 else x.repr

Natural scalar multiplication in optimized binary fields depends only on the scalar parity.

@[simp]

theorem Hex.GF2q.repr_zsmul {n : Nat} [h : GFq.PackedGF2Entry n] (k : Int) (x : GF2q n) : (k • x).repr = if k.natAbs % 2 = 0 then 0 else x.repr

Integer scalar multiplication in optimized binary fields depends only on the absolute-value parity.

@[simp]

theorem Hex.GF2q.repr_add {n : Nat} [h : GFq.PackedGF2Entry n] (x y : GF2q n) : (x + y).repr = (GF2n.reduce (x.repr ^^^ y.repr)).val

The packed representative of a sum is the reduced XOR of representatives.

@[simp]

theorem Hex.GF2q.repr_mul {n : Nat} [h : GFq.PackedGF2Entry n] (x y : GF2q n) : (x * y).repr = (have product := clmul x.repr y.repr; GF2n.reduceWide product.fst product.snd).val

The packed representative of a product is the reduced carry-less product of representatives.

@[simp]

theorem Hex.GF2q.repr_inv {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) : x⁻¹.repr = (GF2n.inv x).val

The packed representative of an inverse is the representative stored by the packed GF2n inversion path.

@[simp]

theorem Hex.GF2q.repr_div {n : Nat} [h : GFq.PackedGF2Entry n] (x y : GF2q n) : (x / y).repr = (GF2n.div x y).val

The packed representative of a quotient is the representative stored by the packed GF2n division path.

@[simp]

theorem Hex.GF2q.repr_pow {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) (k : Nat) : (x ^ k).repr = (GF2n.pow x k).val

The packed representative of a natural power is stored by the packed GF2n square-and-multiply power.

@[simp]

theorem Hex.GF2q.repr_zpow_ofNat {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) (k : Nat) : repr (x ^ Int.ofNat k) = (GF2n.zpow x (Int.ofNat k)).val

The packed representative of a nonnegative integer power is stored by the packed GF2n integer-power operation.

@[simp]

theorem Hex.GF2q.repr_zpow_negSucc {n : Nat} [h : GFq.PackedGF2Entry n] (x : GF2q n) (k : Nat) : repr (x ^ Int.negSucc k) = (GF2n.zpow x (Int.negSucc k)).val

The packed representative of a negative integer power is stored by the packed GF2n integer-power operation.