Raw parity-circuit fragments -- definitions

This module builds an appendable fan-in-two circuit for the XOR of selected existing wires. One false initializer and three gates per selected wire give a linear construction that retains sharing, unlike expansion into a Boolean formula tree.

def Complexity.CircuitCode.Parity.foldXor (count : ℕ) : (Fin count → Bool) → Bool

XOR of a fixed-width Boolean vector, defined from its first coordinate toward its last coordinate.

Equations

• Complexity.CircuitCode.Parity.foldXor 0 x_2 = false
• Complexity.CircuitCode.Parity.foldXor count.succ bits = (bits 0 ^^ Complexity.CircuitCode.Parity.foldXor count fun (i : Fin count) => bits i.succ)

def Complexity.CircuitCode.Parity.accumulatorWire (available step : ℕ) : ℕ

Accumulator wire before processing the selected wire at step.

Equations

• Complexity.CircuitCode.Parity.accumulatorWire available step = available + 3 * step

def Complexity.CircuitCode.Parity.orWire (available step : ℕ) : ℕ

First wire emitted while folding one selected bit into the accumulator.

Equations

• Complexity.CircuitCode.Parity.orWire available step = available + 1 + 3 * step

def Complexity.CircuitCode.Parity.andWire (available step : ℕ) : ℕ

Second wire emitted while folding one selected bit into the accumulator.

Equations

• Complexity.CircuitCode.Parity.andWire available step = Complexity.CircuitCode.Parity.orWire available step + 1

def Complexity.CircuitCode.Parity.xorGates (available step input : ℕ) : RawCircuit

The three gates computing accumulator XOR input with shared intermediates.

Equations

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

def Complexity.CircuitCode.Parity.steps (available step count : ℕ) : (Fin count → ℕ) → RawCircuit

Process successive selected wires, starting at the supplied fold step.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.Parity.steps available step 0 x_2 = []

def Complexity.CircuitCode.Parity.outputWire (available inputCount : ℕ) : ℕ

Absolute wire carrying the final parity value.

Equations

• Complexity.CircuitCode.Parity.outputWire available inputCount = Complexity.CircuitCode.Parity.accumulatorWire available inputCount

def Complexity.CircuitCode.Parity.compileRaw (available : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) : RawCircuit

Compile the XOR of selected existing wires as an appendable raw fragment.

The fragment first creates a false accumulator and then uses three shared gates per selected wire.

Equations

• Complexity.CircuitCode.Parity.compileRaw available refs = [Complexity.CircuitCode.RawGate.constant 0 false] ++ Complexity.CircuitCode.Parity.steps available 0 inputCount refs