Counting wire uses in CSLib circuits

A wire use is one argument slot of a gate or one designated output. Repeated arguments of the same gate and repeated outputs are separate uses. In particular, counting distinct consumer gates would give the wrong fan-out.

Circuit.inputUses counts uses of original inputs. Circuit.excessFanout counts uses beyond the first for each gate wire, and Circuit.sharedGates selects gates with at least two uses. Outputs count as uses, so these notions also handle a gate that supplies both another gate and a designated output. On a trimmed single-output circuit this selects the usual shared internal gates.

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.WireUse {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Type

A gate argument slot or a designated output, counting repeated occurrences separately.

Equations

• c.WireUse = ((j : Fin c.size) × Fin (σ.Arity (c.program.lines j).op) ⊕ Fin m)

def Cslib.Circuits.Circuit.useWire {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.WireUse → Wire n c.size

The wire read by an argument slot or a designated output.

Equations

• c.useWire (Sum.inl ⟨j, a⟩) = (c.program.lines j).wires a
• c.useWire (Sum.inr o) = c.outputs o

def Cslib.Circuits.Circuit.wireUses {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (w : Wire n c.size) : ℕ

The number of uses of a wire, including designated outputs.

Equations

• c.wireUses w = {u : c.WireUse | c.useWire u = w}.card

def Cslib.Circuits.Circuit.inputUses {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ℕ

Total occurrences of original input wires among gate arguments and outputs.

Equations

• c.inputUses = ∑ i : Fin n, c.wireUses (Cslib.Circuits.Wire.input i)

def Cslib.Circuits.Circuit.excessFanout {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ℕ

Gate-wire uses beyond the first; unused gates contribute zero.

Equations

• c.excessFanout = ∑ j : Fin c.size, (c.wireUses (Cslib.Circuits.Wire.gate j) - 1)

def Cslib.Circuits.Circuit.sharedGates {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Finset (Fin c.size)

Gates whose output is used at least twice. Primary inputs are excluded.

Equations

• c.sharedGates = {j : Fin c.size | 2 ≤ c.wireUses (Cslib.Circuits.Wire.gate j)}

def Cslib.Circuits.Circuit.NoUnusedGates {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Prop

Every gate wire supplies at least one gate argument or designated output.

Equations

• c.NoUnusedGates = ∀ (j : Fin c.size), 0 < c.wireUses (Cslib.Circuits.Wire.gate j)