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: constants, copies and NANDs.
• Cslib.Circuits.Boolean.Layered.eval: evaluation 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

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

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

@[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

theorem Cslib.Circuits.Boolean.Layered.eval_append (inputs : List Bool) (first second : List (List Node)) : eval inputs (first ++ second) = eval (eval inputs first) 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

@[simp]

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

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

@[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

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 []

@[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

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

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.