Circuit fragments for affine Boolean forms -- proof internals

theorem Complexity.PairwiseIndependentHash.AffineCircuit.linearValue_eq_sum_add_internal {width : ℕ} (coefficients input : BitString width) (constant : Bool) : linearValue coefficients input constant = ∑ coordinate : Fin width, coefficients coordinate * input coordinate + constant

theorem Complexity.PairwiseIndependentHash.AffineCircuit.zeroValue_eq_decide_internal {width : ℕ} (output : BitString width) : zeroValue output = decide (output = fun (x : Fin width) => false)

theorem Complexity.PairwiseIndependentHash.AffineCircuit.length_productGates_internal (width : ℕ) (coefficientRefs inputRefs : Fin width → ℕ) : List.length (productGates width coefficientRefs inputRefs) = width

theorem Complexity.PairwiseIndependentHash.AffineCircuit.length_compileLinearRaw_internal (available : ℕ) {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) : List.length (compileLinearRaw available coefficientRefs inputRefs constantRef) = linearGateCount width

theorem Complexity.PairwiseIndependentHash.AffineCircuit.outputWire_eq_internal (available : ℕ) {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) : outputWire available width = available + List.length (compileLinearRaw available coefficientRefs inputRefs constantRef) - 1

theorem Complexity.PairwiseIndependentHash.AffineCircuit.evalAux?_compileLinearRaw_internal (available : ℕ) [NeZero available] {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) (coefficients input : BitString width) (constant : Bool) (wires : Array Bool) (hsize : wires.size = available) (hcoefficientRefs : ∀ (i : Fin width), coefficientRefs i < available) (hinputRefs : ∀ (i : Fin width), inputRefs i < available) (hconstantRef : constantRef < available) (hcoefficients : ∀ (i : Fin width), wires[coefficientRefs i]? = some (coefficients i)) (hinputs : ∀ (i : Fin width), wires[inputRefs i]? = some (input i)) (hconstant : wires[constantRef]? = some constant) : ∃ (result : Array Bool), (compileLinearRaw available coefficientRefs inputRefs constantRef).evalAux? wires = some result ∧ result.size = wires.size + linearGateCount width ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[outputWire available width]? = some (linearValue coefficients input constant)

theorem Complexity.PairwiseIndependentHash.AffineCircuit.length_compileRowsRaw_internal (available width rowCount : ℕ) (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) : List.length (compileRowsRaw available width rowCount coefficientRefs inputRefs) = rowCount * linearGateCount width

theorem Complexity.PairwiseIndependentHash.AffineCircuit.evalAux?_compileRowsRaw_internal (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (coefficients : Fin rowCount → BitString (width + 1)) (input : BitString width) (wires : Array Bool) (hsize : wires.size = available) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) (hcoefficients : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), wires[coefficientRefs row coordinate]? = some (coefficients row coordinate)) (hinputs : ∀ (coordinate : Fin width), wires[inputRefs coordinate]? = some (input coordinate)) : ∃ (result : Array Bool), (compileRowsRaw available width rowCount coefficientRefs inputRefs).evalAux? wires = some result ∧ result.size = available + rowCount * linearGateCount width ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ ∀ (row : Fin rowCount), result[rowOutputWire available width row]? = some (linearValue (fun (coordinate : Fin width) => coefficients row coordinate.castSucc) input (coefficients row (Fin.last width)))

theorem Complexity.PairwiseIndependentHash.AffineCircuit.length_compileZeroRaw_internal (available width rowCount : ℕ) (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) : List.length (compileZeroRaw available width rowCount coefficientRefs inputRefs) = zeroGateCount width rowCount

theorem Complexity.PairwiseIndependentHash.AffineCircuit.zeroOutputWire_eq_internal (available width rowCount : ℕ) (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) : zeroOutputWire available width rowCount = available + List.length (compileZeroRaw available width rowCount coefficientRefs inputRefs) - 1

theorem Complexity.PairwiseIndependentHash.AffineCircuit.evalAux?_compileZeroRaw_internal (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (coefficients : Fin rowCount → BitString (width + 1)) (input : BitString width) (wires : Array Bool) (hsize : wires.size = available) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) (hcoefficients : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), wires[coefficientRefs row coordinate]? = some (coefficients row coordinate)) (hinputs : ∀ (coordinate : Fin width), wires[inputRefs coordinate]? = some (input coordinate)) : ∃ (result : Array Bool), (compileZeroRaw available width rowCount coefficientRefs inputRefs).evalAux? wires = some result ∧ result.size = wires.size + zeroGateCount width rowCount ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[zeroOutputWire available width rowCount]? = some (zeroValue fun (row : Fin rowCount) => linearValue (fun (coordinate : Fin width) => coefficients row coordinate.castSucc) input (coefficients row (Fin.last width)))

theorem Complexity.PairwiseIndependentHash.AffineCircuit.topologicallyWellFormed_compileLinearRaw_internal (available : ℕ) [NeZero available] {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) (hcoefficientRefs : ∀ (i : Fin width), coefficientRefs i < available) (hinputRefs : ∀ (i : Fin width), inputRefs i < available) (hconstantRef : constantRef < available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (compileLinearRaw available coefficientRefs inputRefs constantRef)

theorem Complexity.PairwiseIndependentHash.AffineCircuit.compileLinearRaw_wellFormed_internal (available : ℕ) [NeZero available] {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) (hcoefficientRefs : ∀ (i : Fin width), coefficientRefs i < available) (hinputRefs : ∀ (i : Fin width), inputRefs i < available) (hconstantRef : constantRef < available) : CircuitCode.RawCircuit.WellFormed available (compileLinearRaw available coefficientRefs inputRefs constantRef)

theorem Complexity.PairwiseIndependentHash.AffineCircuit.topologicallyWellFormed_compileZeroRaw_internal (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (compileZeroRaw available width rowCount coefficientRefs inputRefs)

theorem Complexity.PairwiseIndependentHash.AffineCircuit.compileZeroRaw_wellFormed_internal (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) : CircuitCode.RawCircuit.WellFormed available (compileZeroRaw available width rowCount coefficientRefs inputRefs)

theorem Complexity.PairwiseIndependentHash.AffineCircuit.eval?_compileZeroRaw_internal (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) (input : BitString available) : (compileZeroRaw available width rowCount coefficientRefs inputRefs).eval? input.toList = some (zeroValue fun (row : Fin rowCount) => linearValue (fun (coordinate : Fin width) => input ⟨coefficientRefs row coordinate.castSucc, ⋯⟩) (fun (coordinate : Fin width) => input ⟨inputRefs coordinate, ⋯⟩) (input ⟨coefficientRefs row (Fin.last width), ⋯⟩))

theorem Complexity.PairwiseIndependentHash.AffineCircuit.linearValue_affineRow_internal {domainWidth rangeWidth : ℕ} (seed : BitString (affineSeedWidth domainWidth rangeWidth)) (input : BitString domainWidth) (row : Fin rangeWidth) : linearValue (fun (coordinate : Fin domainWidth) => affineRows seed row coordinate.castSucc) input (affineRows seed row (Fin.last domainWidth)) = affineEval seed input row

theorem Complexity.PairwiseIndependentHash.AffineCircuit.zeroValue_affineEval_internal {domainWidth rangeWidth : ℕ} (seed : BitString (affineSeedWidth domainWidth rangeWidth)) (input : BitString domainWidth) : (zeroValue fun (row : Fin rangeWidth) => linearValue (fun (coordinate : Fin domainWidth) => affineRows seed row coordinate.castSucc) input (affineRows seed row (Fin.last domainWidth))) = decide (affineEval seed input = fun (x : Fin rangeWidth) => false)