Primitive raw-circuit fragment gates

This definitions layer provides the small proof-free gates shared by raw circuit fragment builders. A duplicated-input gate copies or negates an existing wire, while a wire paired with its negation supplies either Boolean constant.

def Complexity.CircuitCode.RawGate.copy (input : ℕ) (negated : Bool := false) : RawGate

Copy an existing wire, optionally negating it for free on both input edges.

Equations

• Complexity.CircuitCode.RawGate.copy input negated = { op := Complexity.AndOrOp.and, input₀ := input, input₁ := input, negated₀ := negated, negated₁ := negated }

def Complexity.CircuitCode.RawGate.constant (input : ℕ) : Bool → RawGate

Produce a Boolean constant from an existing wire and its negation.

Equations

• Complexity.CircuitCode.RawGate.constant input false = { op := Complexity.AndOrOp.and, input₀ := input, input₁ := input, negated₀ := false, negated₁ := true }
• Complexity.CircuitCode.RawGate.constant input true = { op := Complexity.AndOrOp.or, input₀ := input, input₁ := input, negated₀ := false, negated₁ := true }

def Complexity.CircuitCode.RawCircuit.appendOutputMatch (inputWidth : ℕ) (circuit : RawCircuit) (expected : Bool) : RawCircuit

Append one final gate whose output is true exactly when the original circuit output equals expected. The reference is the original last-gate wire, so semantic use requires the original circuit to be nonempty.

Equations

• Complexity.CircuitCode.RawCircuit.appendOutputMatch inputWidth circuit expected = circuit ++ [Complexity.CircuitCode.RawGate.copy (inputWidth + List.length circuit - 1) !expected]

def Complexity.CircuitCode.RawCircuit.appendOutputMatchBit (inputWidth : ℕ) (circuit : RawCircuit) (expected : Bool) : RawCircuit

Append two final gates whose output is true exactly when the original circuit output equals expected. Unlike appendOutputMatch, the first new gate contains expected without negating it, which is useful when serializing a circuit whose expected bit is supplied by a live input wire.

Equations

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