Constant and primary-input source circuits -- definitions

An input source is either a Boolean constant or one selected primary input. A source tuple materializes any positive collection of such values using only counted output gates and no internal gates.

inductive Complexity.Circuit.InputSource (inputWidth : ℕ) : Type

One output source: a Boolean constant or a selected primary input.

• constant {inputWidth : ℕ} (value : Bool) : InputSource inputWidth
• input {inputWidth : ℕ} (coordinate : Fin inputWidth) : InputSource inputWidth

def Complexity.Circuit.InputSource.eval {inputWidth : ℕ} (source : InputSource inputWidth) (input : BitString inputWidth) : Bool

Semantic value of one source under a primary-input assignment.

Equations

• (Complexity.Circuit.InputSource.constant value).eval input = value
• (Complexity.Circuit.InputSource.input coordinate).eval input = input coordinate

def Complexity.Circuit.inputSourceOutputGate {inputWidth : ℕ} [NeZero inputWidth] (source : InputSource inputWidth) : Gate Basis.andOr2 (inputWidth + 0)

Output gate materializing one source.

Equations

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

def Complexity.Circuit.inputSources {inputWidth outputWidth : ℕ} [NeZero inputWidth] [NeZero outputWidth] (sources : Fin outputWidth → InputSource inputWidth) : Circuit Basis.andOr2 inputWidth outputWidth 0

Materialize a tuple of constants and selected primary inputs.

Equations

• Complexity.Circuit.inputSources sources = { gates := Fin.elim0, outputs := fun (output : Fin outputWidth) => Complexity.Circuit.inputSourceOutputGate (sources output), acyclic := ⋯ }