Documentation

Complexitylib.Cslib.Circuit.Wire

Wire indices and the topological order of programs #

Wire.index numbers the wires of a program by listing the inputs first and then the gates in program order. A gate reads only wires whose index is below its own (Program.lines_wires_lt), which is the topological order of a straight-line program made numeric. The computation rules Wire.lastCases_last and Wire.lastCases_castSucc complete CSLib's Wire.lastCases.

These declarations come from the complexitylib-integration branch of the author's CSLib fork (commit 2a4389b), where they lived in Cslib.Computability.Circuit.Wire and Cslib.Computability.Circuit.Program; upstream CSLib did not adopt 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.

source
def Cslib.Circuits.Wire.index {inputCount gateCount : ℕ} :
Wire inputCount gateCount → Fin (inputCount + gateCount)

The position of a wire when the inputs are listed first, followed by the gates in program order. A gate reads only wires whose index is below its own.

Equations
Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Wire.index_input {inputCount gateCount : ℕ} (i : Fin inputCount) :
    (input i).index = Fin.castAdd gateCount i
    source
    @[simp]
    theorem Cslib.Circuits.Wire.index_gate {inputCount gateCount : ℕ} (j : Fin gateCount) :
    (gate j).index = Fin.natAdd inputCount j
    source
    @[simp]
    theorem Cslib.Circuits.Wire.lastCases_last {inputCount gateCount : ℕ} {motive : Wire inputCount (gateCount + 1) → Sort u_1} (last : motive (gate (Fin.last gateCount))) (castSucc : (wire : Wire inputCount gateCount) → motive wire.castSucc) :
    lastCases last castSucc (gate (Fin.last gateCount)) = last
    source
    @[simp]
    theorem Cslib.Circuits.Wire.lastCases_castSucc {inputCount gateCount : ℕ} {motive : Wire inputCount (gateCount + 1) → Sort u_1} (last : motive (gate (Fin.last gateCount))) (castSucc : (wire : Wire inputCount gateCount) → motive wire.castSucc) (wire : Wire inputCount gateCount) :
    lastCases last castSucc wire.castSucc = castSucc wire
    source
    @[simp]
    theorem Cslib.Circuits.Wire.val_index_castSucc {inputCount gateCount : ℕ} (wire : Wire inputCount gateCount) :
    ↑wire.castSucc.index = ↑wire.index
    source
    theorem Cslib.Circuits.Program.lines_wires_lt {σ : Signature} {n g : ℕ} (p : Program σ n g) (gate : Fin g) (argument : Fin (σ.Arity (p.lines gate).op)) :
    ↑((p.lines gate).wires argument).index < n + ↑gate

    Every argument of a widened line is an input or an earlier gate.