Polynomial-size Boolean circuits for binary-field arithmetic

The mass-production manuscript needs arithmetic in GF(2^width) at cost polynomial in width. Treating a field operation as an arbitrary finite function would cost exponential size and is not sufficient for the scheduler ledger.

Here GF(2^width) is represented in an arbitrary fixed vector-space basis over ZMod 2. Addition is coordinatewise XOR. Multiplication is expanded through the hardwired basis structure constants, so every output coordinate is a Boolean polynomial with width^2 quadratic terms. The resulting De Morgan circuit has cubic cost. This is nonuniform in the basis, exactly as allowed by the manuscript's circuit model, but its size proof is explicit and polynomial.

def Algebraic.MassProduction.boolToZModTwo : Bool →+* ZMod 2

The canonical ring map from Boolean-ring bits to ZMod 2.

Equations

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

theorem Algebraic.MassProduction.boolToZModTwo_injective : Function.Injective ⇑boolToZModTwo

noncomputable def Algebraic.MassProduction.boolEquivZModTwo : Bool ≃+* ZMod 2

Boolean-ring bits are ring-equivalent to the prime field ZMod 2.

Equations

• Algebraic.MassProduction.boolEquivZModTwo = RingEquiv.ofBijective Algebraic.MassProduction.boolToZModTwo Algebraic.MassProduction.boolEquivZModTwo._proof_3

@[reducible, inline]

abbrev Algebraic.MassProduction.BinaryExtension (width : ℕ) : Type

The binary extension field of vector-space dimension width.

Equations

• Algebraic.MassProduction.BinaryExtension width = GaloisField 2 width

noncomputable def Algebraic.MassProduction.binaryExtensionBasis (width : ℕ) (widthPositive : 0 < width) : Module.Basis (Fin width) (ZMod 2) (BinaryExtension width)

A fixed width-element basis of GF(2^width) over its prime field.

Equations

• Algebraic.MassProduction.binaryExtensionBasis width widthPositive = Module.finBasisOfFinrankEq (ZMod 2) (Algebraic.MassProduction.BinaryExtension width) ⋯

noncomputable def Algebraic.MassProduction.encodeBinaryExtension {width : ℕ} (widthPositive : 0 < width) (bits : Fin width → Bool) : BinaryExtension width

Encode width Boolean coordinates as one element of GF(2^width).

Equations

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

noncomputable def Algebraic.MassProduction.decodeBinaryExtension {width : ℕ} (widthPositive : 0 < width) (value : BinaryExtension width) : Fin width → Bool

Decode a field element into coordinates in the fixed basis.

Equations

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

@[simp]

theorem Algebraic.MassProduction.decodeBinaryExtension_encode {width : ℕ} (widthPositive : 0 < width) (bits : Fin width → Bool) : decodeBinaryExtension widthPositive (encodeBinaryExtension widthPositive bits) = bits

@[simp]

theorem Algebraic.MassProduction.encodeBinaryExtension_decode {width : ℕ} (widthPositive : 0 < width) (value : BinaryExtension width) : encodeBinaryExtension widthPositive (decodeBinaryExtension widthPositive value) = value

theorem Algebraic.MassProduction.encodeBinaryExtension_injective {width : ℕ} (widthPositive : 0 < width) : Function.Injective (encodeBinaryExtension widthPositive)

Encoding bit vectors in the fixed basis is injective.

@[simp]

theorem Algebraic.MassProduction.encodeBinaryExtension_zero {width : ℕ} (widthPositive : 0 < width) : encodeBinaryExtension widthPositive 0 = 0

@[simp]

theorem Algebraic.MassProduction.decodeBinaryExtension_zero_bits {width : ℕ} (widthPositive : 0 < width) : decodeBinaryExtension widthPositive 0 = 0

Zero has the all-zero coordinate vector in the chosen field basis.

theorem Algebraic.MassProduction.encodeBinaryExtension_ne_zero_iff {width : ℕ} (widthPositive : 0 < width) (bits : Fin width → Bool) : encodeBinaryExtension widthPositive bits ≠ 0 ↔ ∃ (bit : Fin width), bits bit = true

theorem Algebraic.MassProduction.binaryExtensionBasis_encode_coordinate {width : ℕ} (widthPositive : 0 < width) (bits : Fin width → Bool) (coordinate : Fin width) : (binaryExtensionBasis width widthPositive).equivFun (encodeBinaryExtension widthPositive bits) coordinate = boolEquivZModTwo (bits coordinate)

Coordinates of an encoded bit string are the corresponding prime-field bits.

theorem Algebraic.MassProduction.boolEquivZModTwo_decode_coordinate {width : ℕ} (widthPositive : 0 < width) (value : BinaryExtension width) (coordinate : Fin width) : boolEquivZModTwo (decodeBinaryExtension widthPositive value coordinate) = (binaryExtensionBasis width widthPositive).equivFun value coordinate

Mapping a decoded coordinate back to the prime field returns the basis coordinate of the field element.

theorem Algebraic.MassProduction.card_binaryExtension {width : ℕ} (widthPositive : 0 < width) : Nat.card (BinaryExtension width) = 2 ^ width

The chosen representation has exactly 2^width field elements.

theorem Algebraic.MassProduction.encodeBinaryExtension_add {width : ℕ} (widthPositive : 0 < width) (left right : Fin width → Bool) : encodeBinaryExtension widthPositive (left + right) = encodeBinaryExtension widthPositive left + encodeBinaryExtension widthPositive right

Encoding turns coordinatewise XOR into field addition.

noncomputable def Algebraic.MassProduction.multiplicationStructureBit {width : ℕ} (widthPositive : 0 < width) (left right output : Fin width) : Bool

One hardwired multiplication structure constant of the fixed field basis, represented as a Boolean bit.

Equations

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

theorem Algebraic.MassProduction.binaryExtension_mul_coordinate {width : ℕ} (widthPositive : 0 < width) (left right : BinaryExtension width) (output : Fin width) : (binaryExtensionBasis width widthPositive).equivFun (left * right) output = ∑ leftCoordinate : Fin width, ∑ rightCoordinate : Fin width, (binaryExtensionBasis width widthPositive).equivFun left leftCoordinate * (binaryExtensionBasis width widthPositive).equivFun right rightCoordinate * (binaryExtensionBasis width widthPositive).equivFun ((binaryExtensionBasis width widthPositive) leftCoordinate * (binaryExtensionBasis width widthPositive) rightCoordinate) output

Multiplication coordinates are bilinear polynomials in the input coordinates, with the chosen basis multiplication table as coefficients.

def Algebraic.MassProduction.binaryExtensionPairIndex {width : ℕ} (side : Fin 2) (coordinate : Fin width) : Fin (2 * width)

Row-major index of one bit in a pair of field elements.

Equations

• Algebraic.MassProduction.binaryExtensionPairIndex side coordinate = finProdFinEquiv (side, coordinate)

def Algebraic.MassProduction.binaryExtensionPairInput {width : ℕ} (input : Fin (2 * width) → Bool) (side : Fin 2) : Fin width → Bool

Select one of the two encoded field elements supplied to a binary field operation.

Equations

• Algebraic.MassProduction.binaryExtensionPairInput input side coordinate = input (Algebraic.MassProduction.binaryExtensionPairIndex side coordinate)

noncomputable def Algebraic.MassProduction.multiplicationCoordinateTerm {width : ℕ} (widthPositive : 0 < width) (output left right : Fin width) : Arithmetic.Expression Bool (2 * width)

One structure-constant term contributing to a field multiplication coordinate.

Equations

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

noncomputable def Algebraic.MassProduction.multiplicationCoordinateExpression {width : ℕ} (widthPositive : 0 < width) (output : Fin width) : Arithmetic.Expression Bool (2 * width)

Boolean polynomial for one output coordinate of field multiplication.

Equations

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

@[simp]

theorem Algebraic.MassProduction.multiplicationCoordinateTerm_weightedCost {width : ℕ} (widthPositive : 0 < width) (output left right : Fin width) : Arithmetic.Expression.weightedCost 4 1 (multiplicationCoordinateTerm widthPositive output left right) = 2

Each multiplication-table term has two Boolean AND nodes.

theorem Algebraic.MassProduction.multiplicationCoordinateExpression_weightedCost {width : ℕ} (widthPositive : 0 < width) (output : Fin width) : Arithmetic.Expression.weightedCost 4 1 (multiplicationCoordinateExpression widthPositive output) = 6 * (width * width)

One multiplication coordinate compiles to exactly 6 * width^2 standard De Morgan gates: two ANDs and four XOR-implementation gates per structure-table entry.

noncomputable def Algebraic.MassProduction.binaryExtensionMulBits {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : Fin width → Bool

Multiplication on encoded binary-field values, exposed as a Boolean vector function.

Equations

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

theorem Algebraic.MassProduction.multiplicationCoordinateExpression_eval {width : ℕ} (widthPositive : 0 < width) (output : Fin width) (input : Fin (2 * width) → Bool) : Arithmetic.Expression.eval id input (multiplicationCoordinateExpression widthPositive output) = binaryExtensionMulBits widthPositive input output

The structure-constant expression computes the corresponding decoded coordinate of field multiplication.

@[reducible]

noncomputable def Algebraic.MassProduction.multiplicationCoordinateGateCount {width : ℕ} (widthPositive : 0 < width) (output : Fin width) : ℕ

Gate count produced by compiling one multiplication coordinate.

Equations

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

noncomputable def Algebraic.MassProduction.binaryExtensionMulCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature (2 * width) width

Explicit De Morgan circuit for multiplication in GF(2^width).

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionMulCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionMulCircuit widthPositive).size = ∑ output : Fin width, multiplicationCoordinateGateCount widthPositive output

@[simp]

theorem Algebraic.MassProduction.binaryExtensionMulCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : (binaryExtensionMulCircuit widthPositive).eval DeMorgan.interpretation input = binaryExtensionMulBits widthPositive input

The explicit multiplication circuit has exactly the encoded field multiplication semantics.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionMulCircuit_cost {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionMulCircuit widthPositive).cost DeMorgan.standardCost = width * (6 * (width * width))

Exact standard cost of the structure-constant multiplication circuit.

theorem Algebraic.MassProduction.binaryExtensionMulCircuit_cost_le_cube {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionMulCircuit widthPositive).cost DeMorgan.standardCost ≤ 6 * width ^ 3

Cubic field-multiplication cost in a conventional power notation.

def Algebraic.MassProduction.additionCoordinateExpression {width : ℕ} (output : Fin width) : Arithmetic.Expression Bool (2 * width)

One coordinatewise XOR expression for binary-field addition.

Equations

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

def Algebraic.MassProduction.binaryExtensionAddBits {width : ℕ} (input : Fin (2 * width) → Bool) : Fin width → Bool

Boolean representation of binary-field addition.

Equations

• Algebraic.MassProduction.binaryExtensionAddBits input = Algebraic.MassProduction.binaryExtensionPairInput input 0 + Algebraic.MassProduction.binaryExtensionPairInput input 1

theorem Algebraic.MassProduction.encode_binaryExtensionAddBits {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : encodeBinaryExtension widthPositive (binaryExtensionAddBits input) = encodeBinaryExtension widthPositive (binaryExtensionPairInput input 0) + encodeBinaryExtension widthPositive (binaryExtensionPairInput input 1)

The coordinatewise XOR representation agrees with addition in the chosen extension field.

@[simp]

theorem Algebraic.MassProduction.additionCoordinateExpression_eval {width : ℕ} (output : Fin width) (input : Fin (2 * width) → Bool) : Arithmetic.Expression.eval id input (additionCoordinateExpression output) = binaryExtensionAddBits input output

@[reducible]

def Algebraic.MassProduction.additionCoordinateGateCount {width : ℕ} (output : Fin width) : ℕ

Gate count produced by compiling one addition coordinate.

Equations

• Algebraic.MassProduction.additionCoordinateGateCount output = Algebraic.DeMorgan.arithmeticTranslation.compiledGateCount (Algebraic.MassProduction.additionCoordinateExpression output).circuit

def Algebraic.MassProduction.binaryExtensionAddCircuit (width : ℕ) : Circuit DeMorgan.signature (2 * width) width

Explicit coordinatewise De Morgan circuit for binary-field addition.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionAddCircuit_size (width : ℕ) : (binaryExtensionAddCircuit width).size = ∑ output : Fin width, additionCoordinateGateCount output

@[simp]

theorem Algebraic.MassProduction.binaryExtensionAddCircuit_eval {width : ℕ} (input : Fin (2 * width) → Bool) : (binaryExtensionAddCircuit width).eval DeMorgan.interpretation input = binaryExtensionAddBits input

@[simp]

theorem Algebraic.MassProduction.binaryExtensionAddCircuit_cost {width : ℕ} : (binaryExtensionAddCircuit width).cost DeMorgan.standardCost = 4 * width

Field addition costs exactly four standard gates per coordinate with the chosen four-gate XOR implementation.

def Algebraic.MassProduction.binaryExtensionSideCircuit (width : ℕ) (side : Fin 2) : Circuit DeMorgan.signature (2 * width) width

Free projection of one field element from a row-major pair.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSideCircuit_size (width : ℕ) (side : Fin 2) : (binaryExtensionSideCircuit width side).size = 0

binaryExtensionSideCircuit is pure wiring: it has no gates.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSideCircuit_eval {width : ℕ} (side : Fin 2) (input : Fin (2 * width) → Bool) : (binaryExtensionSideCircuit width side).eval DeMorgan.interpretation input = binaryExtensionPairInput input side

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSideCircuit_cost {width : ℕ} (side : Fin 2) : (binaryExtensionSideCircuit width side).cost DeMorgan.standardCost = 0

noncomputable def Algebraic.MassProduction.binaryExtensionSquareBits {width : ℕ} (widthPositive : 0 < width) (input : Fin width → Bool) : Fin width → Bool

Boolean representation of squaring one encoded field element.

Equations

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

noncomputable def Algebraic.MassProduction.binaryExtensionSquareCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature width width

Squaring circuit obtained by feeding one input vector to both sides of the multiplication circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSquareCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionSquareCircuit widthPositive).size = ∑ output : Fin width, multiplicationCoordinateGateCount widthPositive output

The exact gate count of binaryExtensionSquareCircuit.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSquareCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin width → Bool) : (binaryExtensionSquareCircuit widthPositive).eval DeMorgan.interpretation input = binaryExtensionSquareBits widthPositive input

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSquareCircuit_cost {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionSquareCircuit widthPositive).cost DeMorgan.standardCost = width * (6 * (width * width))

def Algebraic.MassProduction.binaryExtensionPairBits {width : ℕ} (left right : Fin width → Bool) : Fin (2 * width) → Bool

Pack two equally wide bit vectors into the row-major two-block layout.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionPairBits_apply {width : ℕ} (left right : Fin width → Bool) (side : Fin 2) (coordinate : Fin width) : binaryExtensionPairBits left right (binaryExtensionPairIndex side coordinate) = Fin.cases (left coordinate) (fun (x : Fin 1) => right coordinate) side

@[simp]

theorem Algebraic.MassProduction.binaryExtensionPairInput_pairBits_zero {width : ℕ} (left right : Fin width → Bool) : binaryExtensionPairInput (binaryExtensionPairBits left right) 0 = left

@[simp]

theorem Algebraic.MassProduction.binaryExtensionPairInput_pairBits_one {width : ℕ} (left right : Fin width → Bool) : binaryExtensionPairInput (binaryExtensionPairBits left right) 1 = right

theorem Algebraic.MassProduction.Circuit.eval_parallelPair_eq_binaryExtensionPairBits {n width : ℕ} (left right : Circuit DeMorgan.signature n width) (input : Fin n → Bool) : (left.parallelPair right).eval DeMorgan.interpretation input = binaryExtensionPairBits (left.eval DeMorgan.interpretation input) (right.eval DeMorgan.interpretation input)

A parallelPair circuit has exactly the corresponding packed-pair semantics.

noncomputable def Algebraic.MassProduction.binaryExtensionSquareRightCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature (2 * width) width

Squaring the second state component while retaining the two-component input namespace.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSquareRightCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionSquareRightCircuit widthPositive).size = (binaryExtensionSquareCircuit widthPositive).size

binaryExtensionSquareRightCircuit has exactly the gates of binaryExtensionSquareCircuit; the surrounding wiring adds none.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionSquareRightCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : (binaryExtensionSquareRightCircuit widthPositive).eval DeMorgan.interpretation input = binaryExtensionSquareBits widthPositive (binaryExtensionPairInput input 1)

@[simp]

theorem Algebraic.MassProduction.encode_binaryExtensionSquareBits {width : ℕ} (widthPositive : 0 < width) (input : Fin width → Bool) : encodeBinaryExtension widthPositive (binaryExtensionSquareBits widthPositive input) = encodeBinaryExtension widthPositive input * encodeBinaryExtension widthPositive input

Encoding the squaring output gives the square of the encoded input.

@[simp]

theorem Algebraic.MassProduction.encode_binaryExtensionMulBits {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : encodeBinaryExtension widthPositive (binaryExtensionMulBits widthPositive input) = encodeBinaryExtension widthPositive (binaryExtensionPairInput input 0) * encodeBinaryExtension widthPositive (binaryExtensionPairInput input 1)

Encoding the multiplication output gives the product of the two encoded input blocks.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionMulBits_pair_decode {width : ℕ} (widthPositive : 0 < width) (left right : BinaryExtension width) : binaryExtensionMulBits widthPositive (binaryExtensionPairBits (decodeBinaryExtension widthPositive left) (decodeBinaryExtension widthPositive right)) = decodeBinaryExtension widthPositive (left * right)

noncomputable def Algebraic.MassProduction.binaryExtensionInverseUpdateInputsCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature (2 * width) (2 * width)

Inputs for one inverse-state update: the square of the second component, followed by the unchanged first component.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseUpdateInputsCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInverseUpdateInputsCircuit widthPositive).size = (binaryExtensionSquareRightCircuit widthPositive).size + (binaryExtensionSideCircuit width 0).size

The exact gate count of binaryExtensionInverseUpdateInputsCircuit.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseUpdateInputsCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : (binaryExtensionInverseUpdateInputsCircuit widthPositive).eval DeMorgan.interpretation input = binaryExtensionPairBits (binaryExtensionSquareBits widthPositive (binaryExtensionPairInput input 1)) (binaryExtensionPairInput input 0)

noncomputable def Algebraic.MassProduction.binaryExtensionInverseUpdateBits {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : Fin width → Bool

The new second component in one inverse-exponentiation round.

Equations

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

@[simp]

theorem Algebraic.MassProduction.encode_binaryExtensionInverseUpdateBits {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : encodeBinaryExtension widthPositive (binaryExtensionInverseUpdateBits widthPositive input) = encodeBinaryExtension widthPositive (binaryExtensionPairInput input 1) * encodeBinaryExtension widthPositive (binaryExtensionPairInput input 1) * encodeBinaryExtension widthPositive (binaryExtensionPairInput input 0)

Field-level semantics of one inverse-state update.

noncomputable def Algebraic.MassProduction.binaryExtensionInverseStepBits {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : Fin (2 * width) → Bool

One state transition (x, y) -> (x, y^2 * x).

Equations

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

noncomputable def Algebraic.MassProduction.binaryExtensionInverseStepCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature (2 * width) (2 * width)

De Morgan circuit for one shared inverse-exponentiation state round.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseStepCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInverseStepCircuit widthPositive).size = (binaryExtensionSideCircuit width 0).size + ((binaryExtensionInverseUpdateInputsCircuit widthPositive).size + ∑ output : Fin width, multiplicationCoordinateGateCount widthPositive output)

The exact gate count of binaryExtensionInverseStepCircuit.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseStepCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin (2 * width) → Bool) : (binaryExtensionInverseStepCircuit widthPositive).eval DeMorgan.interpretation input = binaryExtensionInverseStepBits widthPositive input

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseStepCircuit_cost {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInverseStepCircuit widthPositive).cost DeMorgan.standardCost = 2 * (width * (6 * (width * width)))

One inverse-exponentiation round costs exactly two field multiplications.

theorem Algebraic.MassProduction.binaryExtensionInverseIteration_encode {width : ℕ} (widthPositive : 0 < width) (input : Fin width → Bool) (steps : ℕ) : have state := Circuit.iterateFunction (binaryExtensionInverseStepBits widthPositive) steps (binaryExtensionPairBits input input); encodeBinaryExtension widthPositive (binaryExtensionPairInput state 0) = encodeBinaryExtension widthPositive input ∧ encodeBinaryExtension widthPositive (binaryExtensionPairInput state 1) = encodeBinaryExtension widthPositive input ^ (2 ^ (steps + 1) - 1)

Starting from (x, x), after steps rounds the state is (x, x^(2^(steps+1)-1)) at the field level.

def Algebraic.MassProduction.binaryExtensionInverseInitialCircuit (width : ℕ) : Circuit DeMorgan.signature width (2 * width)

Duplicate one encoded field input into the initial inverse state.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseInitialCircuit_size (width : ℕ) : (binaryExtensionInverseInitialCircuit width).size = 0

binaryExtensionInverseInitialCircuit is pure wiring: it has no gates.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseInitialCircuit_eval {width : ℕ} (input : Fin width → Bool) : (binaryExtensionInverseInitialCircuit width).eval DeMorgan.interpretation input = binaryExtensionPairBits input input

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseInitialCircuit_cost {width : ℕ} : (binaryExtensionInverseInitialCircuit width).cost DeMorgan.standardCost = 0

noncomputable def Algebraic.MassProduction.binaryExtensionInverseStateCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature width (2 * width)

State circuit after the fixed width - 2 inverse-exponentiation rounds.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseStateCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInverseStateCircuit widthPositive).size = (binaryExtensionInverseInitialCircuit width).size + (width - 2) * (binaryExtensionInverseStepCircuit widthPositive).size

The exact gate count of binaryExtensionInverseStateCircuit.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseStateCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin width → Bool) : (binaryExtensionInverseStateCircuit widthPositive).eval DeMorgan.interpretation input = Circuit.iterateFunction (binaryExtensionInverseStepBits widthPositive) (width - 2) (binaryExtensionPairBits input input)

noncomputable def Algebraic.MassProduction.binaryExtensionInversePreSquareCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature width width

Select the accumulated exponent before the final squaring.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInversePreSquareCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInversePreSquareCircuit widthPositive).size = (binaryExtensionInverseStateCircuit widthPositive).size + (binaryExtensionSideCircuit width 1).size

The exact gate count of binaryExtensionInversePreSquareCircuit.

noncomputable def Algebraic.MassProduction.binaryExtensionInverseCircuit {width : ℕ} (widthPositive : 0 < width) : Circuit DeMorgan.signature width width

Explicit inverse circuit using the addition chain x -> x^3 -> x^7 -> ... -> x^(2^(width-1)-1), followed by one square.

Equations

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

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseCircuit_size {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInverseCircuit widthPositive).size = (binaryExtensionInversePreSquareCircuit widthPositive).size + (binaryExtensionSquareCircuit widthPositive).size

The exact gate count of binaryExtensionInverseCircuit.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInversePreSquareCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin width → Bool) : (binaryExtensionInversePreSquareCircuit widthPositive).eval DeMorgan.interpretation input = binaryExtensionPairInput (Circuit.iterateFunction (binaryExtensionInverseStepBits widthPositive) (width - 2) (binaryExtensionPairBits input input)) 1

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseCircuit_eval {width : ℕ} (widthPositive : 0 < width) (input : Fin width → Bool) : (binaryExtensionInverseCircuit widthPositive).eval DeMorgan.interpretation input = binaryExtensionSquareBits widthPositive (binaryExtensionPairInput (Circuit.iterateFunction (binaryExtensionInverseStepBits widthPositive) (width - 2) (binaryExtensionPairBits input input)) 1)

theorem Algebraic.MassProduction.encode_binaryExtensionInverseCircuit_eval {width : ℕ} (widthAtLeastTwo : 2 ≤ width) (input : Fin width → Bool) : encodeBinaryExtension ⋯ ((binaryExtensionInverseCircuit ⋯).eval DeMorgan.interpretation input) = encodeBinaryExtension ⋯ input ^ (2 ^ width - 2)

The field element encoded by the inverse circuit is x^(2^width-2).

theorem Algebraic.MassProduction.binaryExtension_pow_card_sub_two_eq_inv {width : ℕ} (widthPositive : 0 < width) (value : BinaryExtension width) (valueNonzero : value ≠ 0) : value ^ (2 ^ width - 2) = value⁻¹

In a binary extension field, the penultimate positive power is the multiplicative inverse of every nonzero element.

theorem Algebraic.MassProduction.binaryExtensionInverseCircuit_correct {width : ℕ} (widthAtLeastTwo : 2 ≤ width) (input : Fin width → Bool) (inputNonzero : encodeBinaryExtension ⋯ input ≠ 0) : (binaryExtensionInverseCircuit ⋯).eval DeMorgan.interpretation input = decodeBinaryExtension ⋯ (encodeBinaryExtension ⋯ input)⁻¹

On nonzero inputs, the explicit circuit computes multiplicative inversion in GF(2^width).

theorem Algebraic.MassProduction.binaryExtensionInverseCircuit_correct_of_positive {width : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (input : Fin width → Bool) (inputNonzero : encodeBinaryExtension widthPositive input ≠ 0) : (binaryExtensionInverseCircuit widthPositive).eval DeMorgan.interpretation input = decodeBinaryExtension widthPositive (encodeBinaryExtension widthPositive input)⁻¹

Proof-parameter-stable form of inverse-circuit correctness.

@[simp]

theorem Algebraic.MassProduction.binaryExtensionInverseCircuit_cost {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInverseCircuit widthPositive).cost DeMorgan.standardCost = (width - 2) * (2 * (width * (6 * (width * width)))) + width * (6 * (width * width))

Exact cost of the inverse addition chain: two multiplications per round, followed by one final squaring.

theorem Algebraic.MassProduction.binaryExtensionInverseCircuit_cost_le_fourth {width : ℕ} (widthPositive : 0 < width) : (binaryExtensionInverseCircuit widthPositive).cost DeMorgan.standardCost ≤ 12 * width ^ 4

The explicit inversion circuit has quartic Boolean gate cost.