Circuit fragments for affine Boolean forms -- definitions

This module compiles affine Boolean forms over existing circuit wires. Each row uses one shared AND gate per coefficient/input pair followed by the linear-size parity fragment. The multi-row builder appends a linear threshold test deciding whether every affine output bit is zero.

def Complexity.PairwiseIndependentHash.AffineCircuit.linearValue {width : ℕ} (coefficients input : BitString width) (constant : Bool) : Bool

Semantic value of one affine Boolean form.

Equations

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

def Complexity.PairwiseIndependentHash.AffineCircuit.productGates (width : ℕ) : (Fin width → ℕ) → (Fin width → ℕ) → CircuitCode.RawCircuit

One product gate per coefficient/input coordinate.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.PairwiseIndependentHash.AffineCircuit.productGates 0 x_3 x_4 = []

def Complexity.PairwiseIndependentHash.AffineCircuit.productWire (available : ℕ) {width : ℕ} (coordinate : Fin width) : ℕ

Wire emitted for one coefficient/input product.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.productWire available coordinate = available + ↑coordinate

def Complexity.PairwiseIndependentHash.AffineCircuit.parityRefs (available constantRef : ℕ) {width : ℕ} : Fin (width + 1) → ℕ

Inputs to the parity stage: all product wires followed by the constant coefficient.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.parityRefs available constantRef i = Fin.lastCases constantRef (Complexity.PairwiseIndependentHash.AffineCircuit.productWire available) i

def Complexity.PairwiseIndependentHash.AffineCircuit.linearGateCount (width : ℕ) : ℕ

Exact gate count of one compiled affine Boolean form.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.linearGateCount width = width + (1 + 3 * (width + 1))

def Complexity.PairwiseIndependentHash.AffineCircuit.outputWire (available width : ℕ) : ℕ

Absolute wire carrying the compiled affine-form value.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.outputWire available width = Complexity.CircuitCode.Parity.outputWire (available + width) (width + 1)

def Complexity.PairwiseIndependentHash.AffineCircuit.compileLinearRaw (available : ℕ) {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) : CircuitCode.RawCircuit

Compile one affine Boolean form over existing coefficient, input, and constant wires.

Equations

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

def Complexity.PairwiseIndependentHash.AffineCircuit.rowAvailable (available width row : ℕ) : ℕ

Wire count available before compiling the selected affine row.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.rowAvailable available width row = available + row * Complexity.PairwiseIndependentHash.AffineCircuit.linearGateCount width

def Complexity.PairwiseIndependentHash.AffineCircuit.rowOutputWire (available width : ℕ) {rowCount : ℕ} (row : Fin rowCount) : ℕ

Absolute output wire of one row in a sequential affine matrix build.

Equations

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

def Complexity.PairwiseIndependentHash.AffineCircuit.compileRowsRaw (available width rowCount : ℕ) : (Fin rowCount → Fin (width + 1) → ℕ) → (Fin width → ℕ) → CircuitCode.RawCircuit

Compile every row of an affine Boolean matrix, retaining one output wire per row.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.PairwiseIndependentHash.AffineCircuit.compileRowsRaw available width 0 x_3 x✝ = []

def Complexity.PairwiseIndependentHash.AffineCircuit.zeroValue {width : ℕ} (output : BitString width) : Bool

Boolean value asserting that every coordinate of a fixed-width output is zero.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.zeroValue output = !decide (1 ≤ Fin.countP output)

def Complexity.PairwiseIndependentHash.AffineCircuit.rowsAvailable (available width rowCount : ℕ) : ℕ

Wire count available after all affine rows have been compiled.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.rowsAvailable available width rowCount = available + rowCount * Complexity.PairwiseIndependentHash.AffineCircuit.linearGateCount width

def Complexity.PairwiseIndependentHash.AffineCircuit.zeroGateCount (width rowCount : ℕ) : ℕ

Exact gate count of the full affine-zero fragment.

Equations

• Complexity.PairwiseIndependentHash.AffineCircuit.zeroGateCount width rowCount = rowCount * Complexity.PairwiseIndependentHash.AffineCircuit.linearGateCount width + (4 + 2 * rowCount)

def Complexity.PairwiseIndependentHash.AffineCircuit.zeroOutputWire (available width rowCount : ℕ) : ℕ

Absolute wire carrying the full affine-zero decision.

Equations

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

def Complexity.PairwiseIndependentHash.AffineCircuit.compileZeroRaw (available width rowCount : ℕ) (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) : CircuitCode.RawCircuit

Compile all affine rows and return true exactly when every row is zero.

Equations

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