Building, measuring, and bounding CSLib programs

This file extends CSLib's straight-line programs (Cslib.Circuits.Program):

• Program.ofLines builds the program whose gate j computes a given line reading the inputs and the j gates before it; Program.lines_ofLines reads those lines back, widened by Program.wireCastLE.
• Program.depths_eq_lines_depth states CSLib's depth equation line by line, and Program.wireDepths_le bounds every wire's depth by any certificate that bounds each line's depth at its own wire.
• Program.totalFanIn and Circuit.totalFanIn count the wires read by all gates. They are the weighted cost Program.cost from Complexitylib.Algebraic.Cost in which each operation costs its arity, so that API (for instance Program.cost_eq_sum_lines) applies to them.

This file lives in Complexitylib/Cslib/ because it extends CSLib types in their home namespace Cslib.Circuits; its contents are candidates for upstreaming to CSLib.

Main definitions

• Cslib.Circuits.Program.ofLines — a program from its lines
• Cslib.Circuits.Program.wireCastLE — a wire of a shorter program, widened
• Cslib.Circuits.Program.totalFanIn, Cslib.Circuits.Circuit.totalFanIn — the total fan-in

Main results

• Cslib.Circuits.Program.lines_ofLines — the lines of Program.ofLines
• Cslib.Circuits.Program.depths_eq_lines_depth — CSLib's depth equation, line by line
• Cslib.Circuits.Program.wireDepths_le — bounding CSLib depth by a line-wise certificate

theorem Cslib.Circuits.Wire.elim_eq_addCases_index {N g : ℕ} {α : Sort u_1} (x : Fin N → α) (v : Fin g → α) (w : Wire N g) : elim x v w = Fin.addCases x v w.index

A valuation of wires is the valuation of their indices that lists the inputs and then the gates.

theorem Cslib.Circuits.Program.wireDepths_gate_castSucc {σ : Signature} {N g : ℕ} (p : Program σ N g) (line : Line σ N g) (w : Wire N g) : (p.gate line).wireDepths w.castSucc = p.wireDepths w

Widening a wire into a longer program keeps its CSLib depth.

theorem Cslib.Circuits.Program.depths_eq_lines_depth {σ : Signature} {N g : ℕ} (p : Program σ N g) (j : Fin g) : p.depths j = (p.lines j).depth p.wireDepths

Line j of a program has the CSLib depth of gate j.

def Cslib.Circuits.Program.ofLines {σ : Signature} {N : ℕ} (g : ℕ) : ((j : Fin g) → Line σ N ↑j) → Program σ N g

The program whose line j is F j, a line reading only the inputs and the j gates before it.

Equations

• Cslib.Circuits.Program.ofLines 0 x_2 = Cslib.Circuits.Program.empty
• Cslib.Circuits.Program.ofLines g.succ F = (Cslib.Circuits.Program.ofLines g fun (j : Fin g) => F j.castSucc).gate (F (Fin.last g))

def Cslib.Circuits.Program.wireCastLE {N j g : ℕ} (h : j ≤ g) : Wire N j → Wire N g

Regard a wire of a program with j gates as a wire of a program with g ≥ j gates, extending the first.

Equations

• Cslib.Circuits.Program.wireCastLE h = Cslib.Circuits.Wire.elim Cslib.Circuits.Wire.input fun (k : Fin j) => Cslib.Circuits.Wire.gate (Fin.castLE h k)

@[simp]

theorem Cslib.Circuits.Program.index_wireCastLE {N j g : ℕ} (h : j ≤ g) (w : Wire N j) : (wireCastLE h w).index = Fin.castLE ⋯ w.index

Widening a wire keeps its index.

theorem Cslib.Circuits.Program.lines_ofLines {σ : Signature} {N : ℕ} (g : ℕ) (F : (j : Fin g) → Line σ N ↑j) (j : Fin g) : (ofLines g F).lines j = (F j).mapWires (wireCastLE ⋯)

The lines of Program.ofLines are the given lines, widened.

theorem Cslib.Circuits.Line.depth_mono {σ : Signature} {N g : ℕ} (l : Line σ N g) {d e : Wire N g → ℕ} (h : ∀ (a : Fin (σ.Arity l.op)), d (l.wires a) ≤ e (l.wires a)) : l.depth d ≤ l.depth e

A line's depth is monotone in the depths of the wires it reads.

theorem Cslib.Circuits.Program.wireDepths_le {σ : Signature} {N g : ℕ} (p : Program σ N g) (b : Wire N g → ℕ) (hb : ∀ (j : Fin g), (p.lines j).depth b ≤ b (Wire.gate j)) (w : Wire N g) : p.wireDepths w ≤ b w

Bounding CSLib depth by a line-wise certificate. If b bounds every line's depth at the line's own wire, it bounds every wire's depth.

def Cslib.Circuits.Program.totalFanIn {σ : Signature} {N g : ℕ} (p : Program σ N g) : ℕ

The total fan-in of a program: the number of wires read by all its gates, counted with multiplicity. It is the program's cost when every operation costs its arity.

Equations

• p.totalFanIn = Cslib.Circuits.Program.cost σ.Arity p

theorem Cslib.Circuits.Program.totalFanIn_eq_cost {σ : Signature} {N g : ℕ} (p : Program σ N g) : p.totalFanIn = cost σ.Arity p

The total fan-in is the cost charging each operation its arity.

@[simp]

theorem Cslib.Circuits.Program.totalFanIn_empty {σ : Signature} {N : ℕ} : empty.totalFanIn = 0

The empty program reads no wires.

@[simp]

theorem Cslib.Circuits.Program.totalFanIn_gate {σ : Signature} {N g : ℕ} (p : Program σ N g) (line : Line σ N g) : (p.gate line).totalFanIn = p.totalFanIn + σ.Arity line.op

A new gate adds its arity to the total fan-in.

theorem Cslib.Circuits.Program.totalFanIn_eq_sum_lines {σ : Signature} {N g : ℕ} (p : Program σ N g) : p.totalFanIn = ∑ j : Fin g, σ.Arity (p.lines j).op

The total fan-in is the sum of the arities of the program's lines.

def Cslib.Circuits.Circuit.totalFanIn {σ : Signature} {N m : ℕ} (c : Circuit σ N m) : ℕ

The total fan-in of a circuit: the number of wires read by all its gates, counted with multiplicity. Designated outputs read nothing.

Equations

• c.totalFanIn = c.program.totalFanIn

theorem Cslib.Circuits.Circuit.totalFanIn_eq_cost {σ : Signature} {N m : ℕ} (c : Circuit σ N m) : c.totalFanIn = c.cost σ.Arity

The total fan-in of a circuit is the cost charging each operation its arity.

@[simp]

theorem Cslib.Circuits.Circuit.totalFanIn_mk {σ : Signature} {N m g : ℕ} (p : Program σ N g) (outputs : Fin m → Wire N g) : { size := g, program := p, outputs := outputs }.totalFanIn = p.totalFanIn

A circuit's total fan-in is its program's.

@[simp]

theorem Cslib.Circuits.Circuit.totalFanIn_wiring {σ : Signature} {N m : ℕ} (select : Fin m → Fin N) : (wiring σ select).totalFanIn = 0

A wiring has no gates, so it reads no wires.