Repeated fixed-base conversion

Repeatedly divide a fixed-width binary input by a positive base. The circuit keeps the current fixed-width quotient and appends every remainder in least-significant-first order, with each remainder represented one-hot. This is the runtime base conversion needed by canonical prefix packing.

@[reducible]

noncomputable def Algebraic.MassProduction.BaseConversion.gateCount {base : ℕ} (inputWidth : ℕ) (basePositive : 0 < base) : ℕ → ℕ

Gate-count recurrence for repeated fixed-base division.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.BaseConversion.gateCount inputWidth basePositive 0 = 0

def Algebraic.MassProduction.BaseConversion.quotientInputIndex (inputWidth retainedBits : ℕ) : Fin inputWidth → Fin (inputWidth + retainedBits)

Read the current quotient prefix as the input to one more division.

Equations

• Algebraic.MassProduction.BaseConversion.quotientInputIndex inputWidth retainedBits = Fin.castAdd retainedBits

def Algebraic.MassProduction.BaseConversion.retainedInputIndex (inputWidth retainedBits : ℕ) : Fin retainedBits → Fin (inputWidth + retainedBits)

Retain an already emitted remainder bit after the quotient prefix.

Equations

• Algebraic.MassProduction.BaseConversion.retainedInputIndex inputWidth retainedBits = Fin.natAdd inputWidth

def Algebraic.MassProduction.BaseConversion.stepOutputIndex (inputWidth base digits : ℕ) : Fin (inputWidth + (digits + 1) * base) → Fin (inputWidth + base + digits * base)

Reorder the intermediate (new quotient, new remainder, old remainders) layout into (new quotient, old remainders, new remainder).

Equations

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

def Algebraic.MassProduction.BaseConversion.retainedOutputIndex (inputWidth base digits : ℕ) (bit : Fin (digits * base)) : Fin (inputWidth + (digits + 1) * base)

Output index of an already retained remainder bit.

Equations

• Algebraic.MassProduction.BaseConversion.retainedOutputIndex inputWidth base digits bit = ⟨inputWidth + ↑bit, ⋯⟩

def Algebraic.MassProduction.BaseConversion.newRemainderOutputIndex (inputWidth base digits : ℕ) (candidate : Fin base) : Fin (inputWidth + (digits + 1) * base)

Output index of a newly appended remainder bit.

Equations

• Algebraic.MassProduction.BaseConversion.newRemainderOutputIndex inputWidth base digits candidate = ⟨inputWidth + digits * base + ↑candidate, ⋯⟩

theorem Algebraic.MassProduction.BaseConversion.stepOutputIndex_quotient {inputWidth base digits : ℕ} (bit : Fin inputWidth) : stepOutputIndex inputWidth base digits (Fin.castAdd ((digits + 1) * base) bit) = ⟨↑bit, ⋯⟩

theorem Algebraic.MassProduction.BaseConversion.stepOutputIndex_retained {digits base inputWidth : ℕ} (bit : Fin (digits * base)) : stepOutputIndex inputWidth base digits (retainedOutputIndex inputWidth base digits bit) = ⟨inputWidth + base + ↑bit, ⋯⟩

theorem Algebraic.MassProduction.BaseConversion.stepOutputIndex_newRemainder {base inputWidth digits : ℕ} (candidate : Fin base) : stepOutputIndex inputWidth base digits (newRemainderOutputIndex inputWidth base digits candidate) = ⟨inputWidth + ↑candidate, ⋯⟩

noncomputable def Algebraic.MassProduction.BaseConversion.stepCircuit {base : ℕ} (inputWidth : ℕ) (basePositive : 0 < base) (digits : ℕ) : Circuit DeMorgan.signature (inputWidth + digits * base) (inputWidth + (digits + 1) * base)

One repeated-conversion step. The existing remainder log is retained at zero cost.

Equations

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

@[simp]

theorem Algebraic.MassProduction.BaseConversion.stepCircuit_size {base : ℕ} (inputWidth : ℕ) (basePositive : 0 < base) (digits : ℕ) : (stepCircuit inputWidth basePositive digits).size = FixedDivision.prefixGateCount inputWidth basePositive inputWidth

@[simp]

theorem Algebraic.MassProduction.BaseConversion.stepCircuit_eval_quotient {base inputWidth digits : ℕ} (basePositive : 0 < base) (input : Fin (inputWidth + digits * base) → Bool) (bit : Fin inputWidth) : (stepCircuit inputWidth basePositive digits).eval DeMorgan.interpretation input (Fin.castAdd ((digits + 1) * base) bit) = (FixedDivision.circuit inputWidth basePositive).eval DeMorgan.interpretation (fun (source : Fin inputWidth) => input (Fin.castAdd (digits * base) source)) (Fin.castAdd base bit)

@[simp]

theorem Algebraic.MassProduction.BaseConversion.stepCircuit_eval_retained {base inputWidth digits : ℕ} (basePositive : 0 < base) (input : Fin (inputWidth + digits * base) → Bool) (bit : Fin (digits * base)) : (stepCircuit inputWidth basePositive digits).eval DeMorgan.interpretation input (retainedOutputIndex inputWidth base digits bit) = input (Fin.natAdd inputWidth bit)

@[simp]

theorem Algebraic.MassProduction.BaseConversion.stepCircuit_eval_newRemainder {base inputWidth digits : ℕ} (basePositive : 0 < base) (input : Fin (inputWidth + digits * base) → Bool) (candidate : Fin base) : (stepCircuit inputWidth basePositive digits).eval DeMorgan.interpretation input (newRemainderOutputIndex inputWidth base digits candidate) = (FixedDivision.circuit inputWidth basePositive).eval DeMorgan.interpretation (fun (source : Fin inputWidth) => input (Fin.castAdd (digits * base) source)) (Fin.natAdd inputWidth candidate)

noncomputable def Algebraic.MassProduction.BaseConversion.circuit {base : ℕ} (inputWidth : ℕ) (basePositive : 0 < base) (digits : ℕ) : Circuit DeMorgan.signature inputWidth (inputWidth + digits * base)

Repeated fixed-base conversion circuit.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.BaseConversion.circuit inputWidth basePositive 0 = Cslib.Circuits.Circuit.castCounts ⋯ ⋯ (Cslib.Circuits.Circuit.id Algebraic.DeMorgan.signature inputWidth)

@[simp]

theorem Algebraic.MassProduction.BaseConversion.circuit_size {base : ℕ} (inputWidth : ℕ) (basePositive : 0 < base) (digits : ℕ) : (circuit inputWidth basePositive digits).size = gateCount inputWidth basePositive digits

Repeated conversion emits exactly gateCount gates.

def Algebraic.MassProduction.BaseConversion.quotientValue {inputWidth : ℕ} (input : Fin inputWidth → Bool) (base digits : ℕ) : ℕ

Natural quotient represented by the current quotient block.

Equations

• Algebraic.MassProduction.BaseConversion.quotientValue input base digits = ↑(Algebraic.MassProduction.FixedDivision.bitVectorIndex input) / base ^ digits

def Algebraic.MassProduction.BaseConversion.digitValue {base inputWidth : ℕ} (basePositive : 0 < base) (input : Fin inputWidth → Bool) (digit : ℕ) : Fin base

The digitth least-significant base digit, as a bounded index.

Equations

• Algebraic.MassProduction.BaseConversion.digitValue basePositive input digit = ⟨↑(Algebraic.MassProduction.FixedDivision.bitVectorIndex input) / base ^ digit % base, ⋯⟩

theorem Algebraic.MassProduction.BaseConversion.circuit_quotient_value {base inputWidth : ℕ} (basePositive : 0 < base) (input : Fin inputWidth → Bool) (digits : ℕ) : ↑(FixedDivision.bitVectorIndex fun (bit : Fin inputWidth) => (circuit inputWidth basePositive digits).eval DeMorgan.interpretation input (Fin.castAdd (digits * base) bit)) = quotientValue input base digits

The current quotient block has value input / base^digits.

theorem Algebraic.MassProduction.BaseConversion.circuit_digit_oneHot {base inputWidth : ℕ} (basePositive : 0 < base) (input : Fin inputWidth → Bool) (digits : ℕ) (digit : Fin digits) (candidate : Fin base) : (circuit inputWidth basePositive digits).eval DeMorgan.interpretation input (Fin.natAdd inputWidth (finProdFinEquiv (digit, candidate))) = decide (candidate = digitValue basePositive input ↑digit)

Every emitted remainder block is one-hot at the corresponding base digit.

@[simp]

theorem Algebraic.MassProduction.BaseConversion.stepCircuit_cost {base inputWidth : ℕ} (basePositive : 0 < base) (digits : ℕ) : (stepCircuit inputWidth basePositive digits).cost DeMorgan.standardCost = (FixedDivision.circuit inputWidth basePositive).cost DeMorgan.standardCost

theorem Algebraic.MassProduction.BaseConversion.circuit_cost {base inputWidth : ℕ} (basePositive : 0 < base) (digits : ℕ) : (circuit inputWidth basePositive digits).cost DeMorgan.standardCost = digits * (FixedDivision.circuit inputWidth basePositive).cost DeMorgan.standardCost

Repeated conversion charges exactly one divider per emitted digit.

theorem Algebraic.MassProduction.BaseConversion.circuit_cost_le {base inputWidth : ℕ} (basePositive : 0 < base) (digits : ℕ) : (circuit inputWidth basePositive digits).cost DeMorgan.standardCost ≤ digits * (inputWidth * (8 * base))

Coarse explicit cost bound for digits base digits.