Relocating raw circuit fragments -- definitions

A raw fragment whose incoming wires begin at zero can be mounted after an arbitrary prefix by adding the prefix width to every wire reference. Gate order, negation flags, and operations are unchanged.

def Complexity.CircuitCode.RawGate.shift (offset : ℕ) (gate : RawGate) : RawGate

Add a fixed offset to both input references of a raw gate.

Equations

• Complexity.CircuitCode.RawGate.shift offset gate = { op := gate.op, input₀ := offset + gate.input₀, input₁ := offset + gate.input₁, negated₀ := gate.negated₀, negated₁ := gate.negated₁ }

def Complexity.CircuitCode.RawCircuit.shift (offset : ℕ) (circuit : RawCircuit) : RawCircuit

Relocate every reference in a raw circuit by the same wire offset.

Equations

• Complexity.CircuitCode.RawCircuit.shift offset circuit = List.map (Complexity.CircuitCode.RawGate.shift offset) circuit