Fixed-divisor Boolean division

This module implements one transition of binary long division by a fixed positive natural number. The remainder is represented one-hot. For a target remainder s, the only possible pre-transition naturals are s and divisor + s; consequently every next-state bit is the OR of exactly two branches. This gives a transition circuit linear in the divisor and avoids introducing any finite-enumeration instances.

def Algebraic.MassProduction.FixedDivision.boolNat : Bool → ℕ

Natural value of one Boolean digit.

Equations

• Algebraic.MassProduction.FixedDivision.boolNat false = 0
• Algebraic.MassProduction.FixedDivision.boolNat true = 1

def Algebraic.MassProduction.FixedDivision.boolFin : Bool → Fin 2

A Boolean digit regarded as an element of Fin 2.

Equations

• Algebraic.MassProduction.FixedDivision.boolFin false = 0
• Algebraic.MassProduction.FixedDivision.boolFin true = 1

@[simp]

theorem Algebraic.MassProduction.FixedDivision.boolFin_val (bit : Bool) : ↑(boolFin bit) = boolNat bit

def Algebraic.MassProduction.FixedDivision.bitVectorIndex {width : ℕ} (bits : Fin width → Bool) : Fin (2 ^ width)

The natural represented by a fixed-width little-endian bit vector.

Equations

• Algebraic.MassProduction.FixedDivision.bitVectorIndex bits = finFunctionFinEquiv fun (bit : Fin width) => Algebraic.MassProduction.FixedDivision.boolFin (bits bit)

theorem Algebraic.MassProduction.FixedDivision.bitVectorIndex_val {width : ℕ} (bits : Fin width → Bool) : ↑(bitVectorIndex bits) = ∑ bit : Fin width, boolNat (bits bit) * 2 ^ ↑bit

theorem Algebraic.MassProduction.FixedDivision.bitVectorIndex_cons {width : ℕ} (bit : Bool) (bits : Fin width → Bool) : ↑(bitVectorIndex (Fin.cons bit bits)) = boolNat bit + 2 * ↑(bitVectorIndex bits)

Prepending a little-endian bit performs one binary bit step.

def Algebraic.MassProduction.FixedDivision.transitionRaw {divisor : ℕ} (state : Fin divisor) (bit : Bool) : ℕ

One binary long-division transition before reducing modulo the divisor.

Equations

• Algebraic.MassProduction.FixedDivision.transitionRaw state bit = 2 * ↑state + Algebraic.MassProduction.FixedDivision.boolNat bit

theorem Algebraic.MassProduction.FixedDivision.transitionRaw_lt_two_mul {divisor : ℕ} (state : Fin divisor) (bit : Bool) : transitionRaw state bit < 2 * divisor

def Algebraic.MassProduction.FixedDivision.transitionState {divisor : ℕ} (_divisorPositive : 0 < divisor) (state : Fin divisor) (bit : Bool) : Fin divisor

Next remainder, using the fact that one transition is below twice the positive divisor and therefore needs at most one subtraction.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FixedDivision.transitionState_val {divisor : ℕ} (divisorPositive : 0 < divisor) (state : Fin divisor) (bit : Bool) : ↑(transitionState divisorPositive state bit) = if transitionRaw state bit < divisor then transitionRaw state bit else transitionRaw state bit - divisor

def Algebraic.MassProduction.FixedDivision.transitionQuotientBit {divisor : ℕ} (state : Fin divisor) (bit : Bool) : Bool

The quotient digit emitted by one transition.

Equations

• Algebraic.MassProduction.FixedDivision.transitionQuotientBit state bit = decide (divisor ≤ Algebraic.MassProduction.FixedDivision.transitionRaw state bit)

theorem Algebraic.MassProduction.FixedDivision.transition_decompose {divisor : ℕ} (divisorPositive : 0 < divisor) (state : Fin divisor) (bit : Bool) : transitionRaw state bit = boolNat (transitionQuotientBit state bit) * divisor + ↑(transitionState divisorPositive state bit)

One transition decomposes its raw value into the emitted binary quotient digit and the next remainder.

def Algebraic.MassProduction.FixedDivision.rawState {divisor : ℕ} (_divisorPositive : 0 < divisor) (raw : Fin (2 * divisor)) : Fin divisor

Every raw value below twice the divisor has a predecessor-state half.

Equations

• Algebraic.MassProduction.FixedDivision.rawState _divisorPositive raw = ⟨↑raw / 2, ⋯⟩

def Algebraic.MassProduction.FixedDivision.rawBit {divisor : ℕ} (raw : Fin (2 * divisor)) : Bool

Low binary digit of a raw transition value.

Equations

• Algebraic.MassProduction.FixedDivision.rawBit raw = (↑raw).bodd

theorem Algebraic.MassProduction.FixedDivision.raw_reconstruct {divisor : ℕ} (divisorPositive : 0 < divisor) (raw : Fin (2 * divisor)) : transitionRaw (rawState divisorPositive raw) (rawBit raw) = ↑raw

def Algebraic.MassProduction.FixedDivision.lowerRaw {divisor : ℕ} (divisorPositive : 0 < divisor) (target : Fin divisor) : Fin (2 * divisor)

The lower raw representative of a target next remainder.

Equations

• Algebraic.MassProduction.FixedDivision.lowerRaw divisorPositive target = ⟨↑target, ⋯⟩

def Algebraic.MassProduction.FixedDivision.upperRaw {divisor : ℕ} (_divisorPositive : 0 < divisor) (target : Fin divisor) : Fin (2 * divisor)

The upper raw representative of a target next remainder.

Equations

• Algebraic.MassProduction.FixedDivision.upperRaw _divisorPositive target = ⟨divisor + ↑target, ⋯⟩

def Algebraic.MassProduction.FixedDivision.stateInputIndex {divisor : ℕ} (state : Fin divisor) : Fin (divisor + 1)

State wires occupy the prefix of a (state..., bit) transition input.

Equations

• Algebraic.MassProduction.FixedDivision.stateInputIndex state = Fin.castAdd 1 state

def Algebraic.MassProduction.FixedDivision.bitInputIndex (divisor : ℕ) : Fin (divisor + 1)

The runtime bit is the final transition input.

Equations

• Algebraic.MassProduction.FixedDivision.bitInputIndex divisor = Fin.last divisor

def Algebraic.MassProduction.FixedDivision.bitLiteralExpression {divisor : ℕ} (wanted : Bool) : DeMorgan.Expression (divisor + 1)

An input literal which is true exactly when the runtime bit has the hardwired requested value.

Equations

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

def Algebraic.MassProduction.FixedDivision.branchExpression {divisor : ℕ} (divisorPositive : 0 < divisor) (raw : Fin (2 * divisor)) : DeMorgan.Expression (divisor + 1)

One predecessor branch for a raw transition value.

Equations

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

def Algebraic.MassProduction.FixedDivision.nextStateExpression {divisor : ℕ} (divisorPositive : 0 < divisor) (target : Fin divisor) : DeMorgan.Expression (divisor + 1)

One next-state bit is the OR of its lower and upper predecessors.

Equations

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

def Algebraic.MassProduction.FixedDivision.quotientExpression {divisor : ℕ} (divisorPositive : 0 < divisor) : DeMorgan.Expression (divisor + 1)

The emitted quotient bit is the OR of all upper-predecessor branches.

Equations

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

def Algebraic.MassProduction.FixedDivision.oneHotTransitionInput {divisor : ℕ} (current : Fin divisor) (bit : Bool) : Fin (divisor + 1) → Bool

Canonical transition input with a one-hot current remainder.

Equations

• Algebraic.MassProduction.FixedDivision.oneHotTransitionInput current bit = Fin.append (fun (state : Fin divisor) => decide (state = current)) fun (x : Fin 1) => bit

@[simp]

theorem Algebraic.MassProduction.FixedDivision.oneHotTransitionInput_state {divisor : ℕ} (current state : Fin divisor) (bit : Bool) : oneHotTransitionInput current bit (stateInputIndex state) = decide (state = current)

@[simp]

theorem Algebraic.MassProduction.FixedDivision.oneHotTransitionInput_bit {divisor : ℕ} (current : Fin divisor) (bit : Bool) : oneHotTransitionInput current bit (bitInputIndex divisor) = bit

theorem Algebraic.MassProduction.FixedDivision.bitLiteralExpression_eval_oneHot {divisor : ℕ} (_divisorPositive : 0 < divisor) (current : Fin divisor) (bit wanted : Bool) : DeMorgan.Expression.eval (oneHotTransitionInput current bit) (bitLiteralExpression wanted) = decide (bit = wanted)

theorem Algebraic.MassProduction.FixedDivision.rawState_rawBit_eq_iff {divisor : ℕ} (divisorPositive : 0 < divisor) (raw : Fin (2 * divisor)) (current : Fin divisor) (bit : Bool) : rawState divisorPositive raw = current ∧ rawBit raw = bit ↔ ↑raw = transitionRaw current bit

theorem Algebraic.MassProduction.FixedDivision.branchExpression_eval_oneHot_eq_true_iff {divisor : ℕ} (divisorPositive : 0 < divisor) (raw : Fin (2 * divisor)) (current : Fin divisor) (bit : Bool) : DeMorgan.Expression.eval (oneHotTransitionInput current bit) (branchExpression divisorPositive raw) = true ↔ ↑raw = transitionRaw current bit

theorem Algebraic.MassProduction.FixedDivision.nextStateExpression_eval_oneHot {divisor : ℕ} (divisorPositive : 0 < divisor) (current target : Fin divisor) (bit : Bool) : DeMorgan.Expression.eval (oneHotTransitionInput current bit) (nextStateExpression divisorPositive target) = decide (target = transitionState divisorPositive current bit)

theorem Algebraic.MassProduction.FixedDivision.quotientExpression_eval_oneHot {divisor : ℕ} (divisorPositive : 0 < divisor) (current : Fin divisor) (bit : Bool) : DeMorgan.Expression.eval (oneHotTransitionInput current bit) (quotientExpression divisorPositive) = transitionQuotientBit current bit

def Algebraic.MassProduction.FixedDivision.transitionOutputExpression {divisor : ℕ} (divisorPositive : 0 < divisor) (output : Fin (divisor + 1)) : DeMorgan.Expression (divisor + 1)

One expression for each next-state wire, followed by the quotient bit.

Equations

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

@[reducible]

def Algebraic.MassProduction.FixedDivision.transitionGateCount {divisor : ℕ} (divisorPositive : 0 < divisor) : ℕ

Emitted gate count of the complete transition circuit.

Equations

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

def Algebraic.MassProduction.FixedDivision.transitionCircuit {divisor : ℕ} (divisorPositive : 0 < divisor) : Circuit DeMorgan.signature (divisor + 1) (divisor + 1)

One verified long-division transition.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FixedDivision.transitionCircuit_size {divisor : ℕ} (divisorPositive : 0 < divisor) : (transitionCircuit divisorPositive).size = transitionGateCount divisorPositive

@[simp]

theorem Algebraic.MassProduction.FixedDivision.transitionCircuit_eval_state {divisor : ℕ} (divisorPositive : 0 < divisor) (current target : Fin divisor) (bit : Bool) : (transitionCircuit divisorPositive).eval DeMorgan.interpretation (oneHotTransitionInput current bit) target.castSucc = decide (target = transitionState divisorPositive current bit)

@[simp]

theorem Algebraic.MassProduction.FixedDivision.transitionCircuit_eval_quotient {divisor : ℕ} (divisorPositive : 0 < divisor) (current : Fin divisor) (bit : Bool) : (transitionCircuit divisorPositive).eval DeMorgan.interpretation (oneHotTransitionInput current bit) (Fin.last divisor) = transitionQuotientBit current bit

Unrolling transitions over a fixed-width input

def Algebraic.MassProduction.FixedDivision.initialStateExpression {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (state : Fin divisor) : DeMorgan.Expression inputWidth

Initial one-hot remainder state, before any input bit is read.

Equations

• Algebraic.MassProduction.FixedDivision.initialStateExpression divisorPositive state = Algebraic.DeMorgan.Expression.constant (decide (state = ⟨0, divisorPositive⟩))

@[reducible]

def Algebraic.MassProduction.FixedDivision.initialStateGateCount {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) : ℕ

Emitted gate count of the free-cost initial constant vector.

Equations

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

def Algebraic.MassProduction.FixedDivision.initialStateCircuit {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) : Circuit DeMorgan.signature inputWidth divisor

Initial one-hot state as a circuit on the eventual input namespace.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FixedDivision.initialStateCircuit_size {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) : (initialStateCircuit inputWidth divisorPositive).size = initialStateGateCount inputWidth divisorPositive

@[simp]

theorem Algebraic.MassProduction.FixedDivision.initialStateCircuit_eval {inputWidth divisor : ℕ} (input : Fin inputWidth → Bool) (divisorPositive : 0 < divisor) (state : Fin divisor) : (initialStateCircuit inputWidth divisorPositive).eval DeMorgan.interpretation input state = decide (state = ⟨0, divisorPositive⟩)

@[reducible]

def Algebraic.MassProduction.FixedDivision.prefixGateCount {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) : ℕ → ℕ

Gate count after a fixed number of unrolled transition rounds.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.FixedDivision.prefixGateCount inputWidth divisorPositive 0 = Algebraic.MassProduction.FixedDivision.initialStateGateCount inputWidth divisorPositive

def Algebraic.MassProduction.FixedDivision.roundInputIndex (inputWidth rounds : ℕ) (roundFits : rounds + 1 ≤ inputWidth) : Fin inputWidth

Input bit processed at the next big-endian round.

Equations

• Algebraic.MassProduction.FixedDivision.roundInputIndex inputWidth rounds roundFits = ⟨rounds, ⋯⟩.rev

def Algebraic.MassProduction.FixedDivision.roundInputCircuit (inputWidth rounds : ℕ) (roundFits : rounds + 1 ≤ inputWidth) : Circuit DeMorgan.signature inputWidth 1

The zero-gate circuit selecting the next original input bit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FixedDivision.roundInputCircuit_size (inputWidth rounds : ℕ) (roundFits : rounds + 1 ≤ inputWidth) : (roundInputCircuit inputWidth rounds roundFits).size = 0

roundInputCircuit is pure wiring: it has no gates.

@[simp]

theorem Algebraic.MassProduction.FixedDivision.roundInputCircuit_eval {inputWidth rounds : ℕ} (input : Fin inputWidth → Bool) (roundFits : rounds + 1 ≤ inputWidth) : (roundInputCircuit inputWidth rounds roundFits).eval DeMorgan.interpretation input 0 = input (roundInputIndex inputWidth rounds roundFits)

def Algebraic.MassProduction.FixedDivision.transitionRoundInputIndex (divisor rounds : ℕ) : Fin (divisor + 1) → Fin (divisor + rounds + 1)

Reorder (state..., prior quotient..., current bit) into the transition circuit's (state..., current bit) input.

Equations

• Algebraic.MassProduction.FixedDivision.transitionRoundInputIndex divisor rounds i = Fin.lastCases (Fin.last (divisor + rounds)) (fun (state : Fin divisor) => ⟨↑state, ⋯⟩) i

@[simp]

theorem Algebraic.MassProduction.FixedDivision.transitionRoundInputIndex_state {divisor rounds : ℕ} (state : Fin divisor) : transitionRoundInputIndex divisor rounds state.castSucc = ⟨↑state, ⋯⟩

@[simp]

theorem Algebraic.MassProduction.FixedDivision.transitionRoundInputIndex_bit {divisor rounds : ℕ} : transitionRoundInputIndex divisor rounds (Fin.last divisor) = Fin.last (divisor + rounds)

theorem Algebraic.MassProduction.FixedDivision.transitionRoundInput_oneHot {divisor rounds : ℕ} (current : Fin divisor) (priorQuotient : Fin rounds → Bool) (bit : Bool) : (Fin.append (Fin.append (fun (state : Fin divisor) => decide (state = current)) priorQuotient) fun (x : Fin 1) => bit) ∘ transitionRoundInputIndex divisor rounds = oneHotTransitionInput current bit

def Algebraic.MassProduction.FixedDivision.retainedQuotientInputIndex (divisor rounds : ℕ) (bit : Fin rounds) : Fin (divisor + rounds + 1)

Select a retained little-endian quotient bit from the middle block.

Equations

• Algebraic.MassProduction.FixedDivision.retainedQuotientInputIndex divisor rounds bit = ⟨divisor + ↑bit, ⋯⟩

def Algebraic.MassProduction.FixedDivision.divisionStepCircuit {divisor : ℕ} (divisorPositive : 0 < divisor) (rounds : ℕ) : Circuit DeMorgan.signature (divisor + rounds + 1) (divisor + (rounds + 1))

Update the remainder and prepend the new least-significant quotient bit, while retaining all earlier quotient bits for free.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FixedDivision.divisionStepCircuit_size {divisor : ℕ} (divisorPositive : 0 < divisor) (rounds : ℕ) : (divisionStepCircuit divisorPositive rounds).size = transitionGateCount divisorPositive

theorem Algebraic.MassProduction.FixedDivision.divisionStepCircuit_eval_state {divisor rounds : ℕ} (divisorPositive : 0 < divisor) (current target : Fin divisor) (priorQuotient : Fin rounds → Bool) (bit : Bool) : (divisionStepCircuit divisorPositive rounds).eval DeMorgan.interpretation (Fin.append (Fin.append (fun (state : Fin divisor) => decide (state = current)) priorQuotient) fun (x : Fin 1) => bit) (Fin.castAdd (rounds + 1) target) = decide (target = transitionState divisorPositive current bit)

theorem Algebraic.MassProduction.FixedDivision.divisionStepCircuit_eval_newQuotient {divisor rounds : ℕ} (divisorPositive : 0 < divisor) (current : Fin divisor) (priorQuotient : Fin rounds → Bool) (bit : Bool) : (divisionStepCircuit divisorPositive rounds).eval DeMorgan.interpretation (Fin.append (Fin.append (fun (state : Fin divisor) => decide (state = current)) priorQuotient) fun (x : Fin 1) => bit) (Fin.natAdd divisor 0) = transitionQuotientBit current bit

theorem Algebraic.MassProduction.FixedDivision.divisionStepCircuit_eval_priorQuotient {divisor rounds : ℕ} (divisorPositive : 0 < divisor) (current : Fin divisor) (priorQuotient : Fin rounds → Bool) (bit : Bool) (priorBit : Fin rounds) : (divisionStepCircuit divisorPositive rounds).eval DeMorgan.interpretation (Fin.append (Fin.append (fun (state : Fin divisor) => decide (state = current)) priorQuotient) fun (x : Fin 1) => bit) (Fin.natAdd divisor priorBit.succ) = priorQuotient priorBit

def Algebraic.MassProduction.FixedDivision.streamState {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) (rounds : ℕ) : rounds ≤ inputWidth → Fin divisor

Remainder after a prefix of the big-endian input stream.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.FixedDivision.streamState divisorPositive input 0 x_2 = ⟨0, divisorPositive⟩

def Algebraic.MassProduction.FixedDivision.streamQuotientBits {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) (rounds : ℕ) (fits : rounds ≤ inputWidth) : Fin rounds → Bool

Little-endian quotient bits accumulated after a stream prefix.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.FixedDivision.streamQuotientBits divisorPositive input 0 x_3 bit = bit.elim0

noncomputable def Algebraic.MassProduction.FixedDivision.divisionPrefixCircuit {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) (rounds : ℕ) (fits : rounds ≤ inputWidth) : Circuit DeMorgan.signature inputWidth (divisor + rounds)

Gate count recurrence is the initial constant vector plus one transition per processed bit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FixedDivision.divisionPrefixCircuit_size {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) (rounds : ℕ) (fits : rounds ≤ inputWidth) : (divisionPrefixCircuit inputWidth divisorPositive rounds fits).size = prefixGateCount inputWidth divisorPositive rounds

The unrolled circuit emits exactly prefixGateCount gates.

theorem Algebraic.MassProduction.FixedDivision.divisionPrefixCircuit_eval {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) (rounds : ℕ) (fits : rounds ≤ inputWidth) : (divisionPrefixCircuit inputWidth divisorPositive rounds fits).eval DeMorgan.interpretation input = Fin.append (fun (state : Fin divisor) => decide (state = streamState divisorPositive input rounds fits)) (streamQuotientBits divisorPositive input rounds fits)

The unrolled circuit exposes the exact one-hot remainder and accumulated little-endian quotient after every processed prefix.

Arithmetic meaning of the stream state

def Algebraic.MassProduction.FixedDivision.streamInputBits {inputWidth : ℕ} (input : Fin inputWidth → Bool) (rounds : ℕ) (fits : rounds ≤ inputWidth) : Fin rounds → Bool

The sequence of original bits read in the first rounds big-endian rounds.

Equations

• Algebraic.MassProduction.FixedDivision.streamInputBits input rounds fits round = input (Algebraic.MassProduction.FixedDivision.roundInputIndex inputWidth ↑round ⋯)

theorem Algebraic.MassProduction.FixedDivision.streamInputBits_succ {inputWidth rounds : ℕ} (input : Fin inputWidth → Bool) (fits : rounds + 1 ≤ inputWidth) : streamInputBits input (rounds + 1) fits = Fin.snoc (streamInputBits input rounds ⋯) (input (roundInputIndex inputWidth rounds fits))

theorem Algebraic.MassProduction.FixedDivision.streamInputBits_full {inputWidth : ℕ} (input : Fin inputWidth → Bool) : streamInputBits input inputWidth ⋯ = input ∘ Fin.rev

def Algebraic.MassProduction.FixedDivision.streamValue {inputWidth : ℕ} (input : Fin inputWidth → Bool) (rounds : ℕ) (fits : rounds ≤ inputWidth) : ℕ

Natural value of the big-endian prefix processed so far.

Equations

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

theorem Algebraic.MassProduction.FixedDivision.streamValue_succ {inputWidth rounds : ℕ} (input : Fin inputWidth → Bool) (fits : rounds + 1 ≤ inputWidth) : streamValue input (rounds + 1) fits = boolNat (input (roundInputIndex inputWidth rounds fits)) + 2 * streamValue input rounds ⋯

theorem Algebraic.MassProduction.FixedDivision.streamValue_full {inputWidth : ℕ} (input : Fin inputWidth → Bool) : streamValue input inputWidth ⋯ = ↑(bitVectorIndex input)

theorem Algebraic.MassProduction.FixedDivision.stream_decomposition {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) (rounds : ℕ) (fits : rounds ≤ inputWidth) : streamValue input rounds fits = ↑(bitVectorIndex (streamQuotientBits divisorPositive input rounds fits)) * divisor + ↑(streamState divisorPositive input rounds fits)

At every round, the processed prefix is quotient times divisor plus the one-hot remainder state.

theorem Algebraic.MassProduction.FixedDivision.streamQuotientBits_value {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) : ↑(bitVectorIndex (streamQuotientBits divisorPositive input inputWidth ⋯)) = ↑(bitVectorIndex input) / divisor

The completed quotient stream represents ordinary natural division.

theorem Algebraic.MassProduction.FixedDivision.streamState_value {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) : ↑(streamState divisorPositive input inputWidth ⋯) = ↑(bitVectorIndex input) % divisor

The completed one-hot state is ordinary natural remainder.

Public fixed-division circuit

def Algebraic.MassProduction.FixedDivision.divisionOutputIndex (inputWidth divisor : ℕ) : Fin (inputWidth + divisor) → Fin (divisor + inputWidth)

Reorder (remainder one-hot..., quotient bits...) into the public (quotient bits..., remainder one-hot...) layout.

Equations

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

noncomputable def Algebraic.MassProduction.FixedDivision.circuit {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) : Circuit DeMorgan.signature inputWidth (inputWidth + divisor)

Fixed-divisor long division. Quotient bits have the same width as the input (with leading zeros), followed by a one-hot remainder vector.

Equations

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

@[simp]

theorem Algebraic.MassProduction.FixedDivision.circuit_size {divisor : ℕ} (inputWidth : ℕ) (divisorPositive : 0 < divisor) : (circuit inputWidth divisorPositive).size = prefixGateCount inputWidth divisorPositive inputWidth

The public divider emits exactly prefixGateCount gates.

@[simp]

theorem Algebraic.MassProduction.FixedDivision.circuit_eval_quotient {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) (bit : Fin inputWidth) : (circuit inputWidth divisorPositive).eval DeMorgan.interpretation input (Fin.castAdd divisor bit) = streamQuotientBits divisorPositive input inputWidth ⋯ bit

@[simp]

theorem Algebraic.MassProduction.FixedDivision.circuit_eval_remainder {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) (remainder : Fin divisor) : (circuit inputWidth divisorPositive).eval DeMorgan.interpretation input (Fin.natAdd inputWidth remainder) = decide (remainder = streamState divisorPositive input inputWidth ⋯)

theorem Algebraic.MassProduction.FixedDivision.circuit_quotient_value {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) : ↑(bitVectorIndex fun (bit : Fin inputWidth) => (circuit inputWidth divisorPositive).eval DeMorgan.interpretation input (Fin.castAdd divisor bit)) = ↑(bitVectorIndex input) / divisor

Reading the quotient block back as a natural gives exact division.

def Algebraic.MassProduction.FixedDivision.remainder {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) : Fin divisor

Canonical bounded remainder represented by the one-hot output block.

Equations

• Algebraic.MassProduction.FixedDivision.remainder divisorPositive input = ⟨↑(Algebraic.MassProduction.FixedDivision.bitVectorIndex input) % divisor, ⋯⟩

theorem Algebraic.MassProduction.FixedDivision.streamState_eq_remainder {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) : streamState divisorPositive input inputWidth ⋯ = remainder divisorPositive input

theorem Algebraic.MassProduction.FixedDivision.circuit_remainder_oneHot {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (input : Fin inputWidth → Bool) (candidate : Fin divisor) : (circuit inputWidth divisorPositive).eval DeMorgan.interpretation input (Fin.natAdd inputWidth candidate) = decide (candidate = remainder divisorPositive input)

The remainder output is exactly one-hot at input mod divisor.

Explicit cost bound

theorem Algebraic.MassProduction.FixedDivision.bitLiteralExpression_standardCost_le {divisor : ℕ} (wanted : Bool) : (bitLiteralExpression wanted).standardCost ≤ 1

theorem Algebraic.MassProduction.FixedDivision.branchExpression_standardCost_le {divisor : ℕ} (divisorPositive : 0 < divisor) (raw : Fin (2 * divisor)) : (branchExpression divisorPositive raw).standardCost ≤ 2

theorem Algebraic.MassProduction.FixedDivision.nextStateExpression_standardCost_le {divisor : ℕ} (divisorPositive : 0 < divisor) (target : Fin divisor) : (nextStateExpression divisorPositive target).standardCost ≤ 5

theorem Algebraic.MassProduction.FixedDivision.quotientExpression_standardCost_le {divisor : ℕ} (divisorPositive : 0 < divisor) : (quotientExpression divisorPositive).standardCost ≤ 3 * divisor

theorem Algebraic.MassProduction.FixedDivision.transitionCircuit_cost_le {divisor : ℕ} (divisorPositive : 0 < divisor) : (transitionCircuit divisorPositive).cost DeMorgan.standardCost ≤ 8 * divisor

One long-division transition costs at most eight gates per divisor state.

@[simp]

theorem Algebraic.MassProduction.FixedDivision.initialStateCircuit_cost {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) : (initialStateCircuit inputWidth divisorPositive).cost DeMorgan.standardCost = 0

@[simp]

theorem Algebraic.MassProduction.FixedDivision.divisionStepCircuit_cost {divisor : ℕ} (divisorPositive : 0 < divisor) (rounds : ℕ) : (divisionStepCircuit divisorPositive rounds).cost DeMorgan.standardCost = (transitionCircuit divisorPositive).cost DeMorgan.standardCost

theorem Algebraic.MassProduction.FixedDivision.divisionPrefixCircuit_cost {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) (rounds : ℕ) (fits : rounds ≤ inputWidth) : (divisionPrefixCircuit inputWidth divisorPositive rounds fits).cost DeMorgan.standardCost = rounds * (transitionCircuit divisorPositive).cost DeMorgan.standardCost

Unrolling charges exactly one transition cost per input bit.

theorem Algebraic.MassProduction.FixedDivision.circuit_cost_le {divisor inputWidth : ℕ} (divisorPositive : 0 < divisor) : (circuit inputWidth divisorPositive).cost DeMorgan.standardCost ≤ inputWidth * (8 * divisor)

The public divider has cost at most 8 * inputWidth * divisor.