Typed circuits as CSLib straight-line programs

CSLib's circuits (Cslib.Circuits.Circuit) are straight-line programs over a signature, and Basis.signature (in Complexitylib.Circuits.Basis.Defs) makes each Complexitylib basis such a signature: an operation symbol of B.signature is a whole gate kind of B, so Gate.kind turns each gate into one.

Circuit.toStraightLine translates a typed circuit Circuit B N M G into a CSLib circuit over B.signature. The program lists the G internal gates and then the M output gates, and the CSLib outputs are the last M gates, so the translation has exactly G + M gates, the typed circuit's size.

Main definitions

• Complexity.Gate.kind — the gate kind of a gate, an operation symbol of B.signature
• Complexity.Circuit.toStraightLine — a typed circuit as a CSLib circuit

def Complexity.Gate.kind {B : Basis} {W : ℕ} (gate : Gate B W) : B.GateKind

The gate kind of a gate: its operation, fan-in, and negation flags.

Equations

• gate.kind = { op := gate.op, fanIn := gate.fanIn, arityOk := ⋯, negated := gate.negated }

def Complexity.StraightLine.wireOfIndex {N j : ℕ} (w : ℕ) (hw : w < N + j) : Cslib.Circuits.Wire N j

The CSLib wire with index w in the layout of typed circuits, where the first N wires are the inputs and wire N + j is gate j.

Equations

• Complexity.StraightLine.wireOfIndex w hw = if h : w < N then Cslib.Circuits.Wire.input ⟨w, h⟩ else Cslib.Circuits.Wire.gate ⟨w - N, ⋯⟩

def Complexity.Circuit.straightLineAt {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (j : Fin (G + M)) : Cslib.Circuits.Line B.signature N ↑j

Line j of the straight-line form of a typed circuit: internal gate j for j < G, and output gate j - G otherwise.

Equations

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

def Complexity.Circuit.toStraightLine {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : Cslib.Circuits.Circuit B.signature N M

The typed circuit c as a CSLib circuit over B.signature: its internal gates followed by its output gates, with the output gates as outputs.

Equations

• c.toStraightLine = { size := G + M, program := Cslib.Circuits.Program.ofLines (G + M) c.straightLineAt, outputs := fun (o : Fin M) => Cslib.Circuits.Wire.gate (Fin.natAdd G o) }