Boolean circuits scheduled in layers

Each node reads only the preceding layer. Constants allow evaluation with no input wires; copies carry values across layers; NAND nodes may read a wire twice. The last layer supplies all outputs, and the empty program preserves all inputs. Wire indices have binary encodings.

The number of scheduled layers counts copies and empty layers too. It is not identified here with the depth of a De Morgan circuit. Layered.Compile converts ordinary shared circuits into exactly two layers per designated-output depth, with output selection as separate wiring.

Main definitions

• Cslib.Circuits.Boolean.Layered.Node, Cslib.Circuits.Boolean.Layered.Node.code, Cslib.Circuits.Boolean.Layered.Node.Valid, Cslib.Circuits.Boolean.Layered.Node.eval: constants, copies and NANDs, together with their tuple code, reference validity, and node evaluation.
• Cslib.Circuits.Boolean.Layered.evalLayer, Cslib.Circuits.Boolean.Layered.eval: evaluation of a single layer and of a list of layers.
• Cslib.Circuits.Boolean.Layered.outputWidth: the number of wires in the final row.
• Cslib.Circuits.Boolean.Layered.select: ordered output wiring, allowing repeated wires.
• Cslib.Circuits.Boolean.Layered.WellFormed: all references read the preceding layer.
• Cslib.Circuits.Boolean.Layered.encNode: two tag bits and binary wire indices.

References

The consecutive-layer presentation, including inserted copy gates, is used in C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2.

inductive Cslib.Circuits.Boolean.Layered.Node : Type

A node whose inputs are positions in the preceding layer.

• const (value : Bool) : Node
• copy (wire : ℕ) : Node
• nand (first second : ℕ) : Node

def Cslib.Circuits.Boolean.Layered.instDecidableEqNode.decEq (x✝ x✝¹ : Node) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Layered.instDecidableEqNode : DecidableEq Node

def Cslib.Circuits.Boolean.Layered.Node.code : Node → (Bool × Bool) × ℕ × ℕ

The two tag bits distinguish the four operations; unused wire positions are zero.

theorem Cslib.Circuits.Boolean.Layered.Node.code_injective : Function.Injective code

A node is uniquely determined by its tag-and-index tuple Node.code.

def Cslib.Circuits.Boolean.Layered.encNode : Node ↪ List Bool

Encode nodes with two operation bits and binary wire indices, including invalid indices.

def Cslib.Circuits.Boolean.Layered.Node.Valid (width : ℕ) : Node → Prop

A node is valid when each of its references exists in the preceding layer.

def Cslib.Circuits.Boolean.Layered.Node.eval (inputs : List Bool) : Node → Bool

Evaluate one node. Invalid references read false; correctness of a client interpreter may require Node.Valid rather than preserving this fallback.

def Cslib.Circuits.Boolean.Layered.evalLayer (inputs : List Bool) (layer : List Node) : List Bool

Evaluate a layer, preserving its order and repeated references.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_evalLayer (inputs : List Bool) (layer : List Node) : (evalLayer inputs layer).length = layer.length

Evaluating a layer produces one output bit per node in the layer.

def Cslib.Circuits.Boolean.Layered.eval (inputs : List Bool) : List (List Node) → List Bool

Execute the layers in order. No layers means identity, including on an empty input.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.eval_nil (inputs : List Bool) : eval inputs [] = inputs

Evaluating an empty schedule leaves the inputs unchanged.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.eval_cons (inputs : List Bool) (layer : List Node) (layers : List (List Node)) : eval inputs (layer :: layers) = eval (evalLayer inputs layer) layers

Evaluating layer :: layers evaluates layer on the inputs and then runs layers.

theorem Cslib.Circuits.Boolean.Layered.eval_append (inputs : List Bool) (first second : List (List Node)) : eval inputs (first ++ second) = eval (eval inputs first) second

Evaluating a concatenation of layer schedules runs the first schedule and then the second.

def Cslib.Circuits.Boolean.Layered.outputWidth (inputCount : ℕ) : List (List Node) → ℕ

The number of wires after the schedule, retaining the input width for an empty schedule.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.outputWidth_nil (inputCount : ℕ) : outputWidth inputCount [] = inputCount

The output width of an empty schedule is the input width.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.outputWidth_cons (inputCount : ℕ) (layer : List Node) (layers : List (List Node)) : outputWidth inputCount (layer :: layers) = outputWidth layer.length layers

The output width of layer :: layers is the output width of layers from layer.length.

theorem Cslib.Circuits.Boolean.Layered.outputWidth_append (inputCount : ℕ) (first second : List (List Node)) : outputWidth inputCount (first ++ second) = outputWidth (outputWidth inputCount first) second

The output width of a concatenated schedule is the output width of the second from the first.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_eval (inputs : List Bool) (layers : List (List Node)) : (eval inputs layers).length = outputWidth inputs.length layers

Evaluation has the width determined by the syntax, regardless of reference validity.

def Cslib.Circuits.Boolean.Layered.select (inputs : List Bool) (outputs : List ℕ) : List Bool

Select output wires in order, allowing repetitions. Selection adds no circuit layer.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_select (inputs : List Bool) (outputs : List ℕ) : (select inputs outputs).length = outputs.length

Output selection produces one bit per requested wire index.

theorem Cslib.Circuits.Boolean.Layered.eval_take_succ (inputs : List Bool) (layers : List (List Node)) {i : ℕ} (hi : i < layers.length) : eval inputs (List.take (i + 1) layers) = evalLayer (eval inputs (List.take i layers)) (layers.getD i [])

Extending a prefix executes precisely its next scheduled layer.

def Cslib.Circuits.Boolean.Layered.WellFormed (inputCount : ℕ) : List (List Node) → Prop

All references are in range in the immediately preceding layer.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.wellFormed_nil (inputCount : ℕ) : WellFormed inputCount []

The empty layer schedule is well-formed for any input width.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.wellFormed_cons (inputCount : ℕ) (layer : List Node) (layers : List (List Node)) : WellFormed inputCount (layer :: layers) ↔ (∀ node ∈ layer, Node.Valid inputCount node) ∧ WellFormed layer.length layers

layer :: layers is well-formed iff every node in layer is valid for inputCount and layers is well-formed for layer.length.

theorem Cslib.Circuits.Boolean.Layered.wellFormed_append (inputCount : ℕ) (first second : List (List Node)) : WellFormed inputCount (first ++ second) ↔ WellFormed inputCount first ∧ WellFormed (outputWidth inputCount first) second

A concatenated schedule is well-formed iff the first is well-formed and the second is well-formed for the output width of the first.

theorem Cslib.Circuits.Boolean.Layered.WellFormed.valid_getD {inputs : List Bool} {layers : List (List Node)} (h : WellFormed inputs.length layers) {i : ℕ} (hi : i < layers.length) (node : Node) : node ∈ layers.getD i [] → Node.Valid (eval inputs (List.take i layers)).length node

Each scheduled layer reads valid wires of the evaluated prefix.