Padding layered Boolean circuits with copies

An identity layer copies every wire in order. Appending such layers extends a schedule to a chosen layer count without changing its value or output width. Schedules already longer than the target are unchanged. The construction also covers zero-width rows and empty schedules.

Main definitions

• Cslib.Circuits.Boolean.Layered.identityLayer: one copy node per input wire.
• Cslib.Circuits.Boolean.Layered.padTo: append copies up to a target layer count.

Main results

• Cslib.Circuits.Boolean.Layered.eval_padTo: padding preserves evaluation on actual inputs.
• Cslib.Circuits.Boolean.Layered.outputWidth_padTo: padding preserves the final width.
• Cslib.Circuits.Boolean.Layered.WellFormed.padTo: padding preserves valid references.
• Cslib.Circuits.Boolean.Layered.length_padTo: the resulting length is the larger of the original length and the target.

References

Copy gates between consecutive layers are used in Gentry, Section 2.

def Cslib.Circuits.Boolean.Layered.identityLayer (width : ℕ) : List Node

Copy every wire in order, including the empty row when width = 0.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_identityLayer (width : ℕ) : (identityLayer width).length = width

theorem Cslib.Circuits.Boolean.Layered.valid_identityLayer (width : ℕ) (node : Node) : node ∈ identityLayer width → Node.Valid width node

@[simp]

theorem Cslib.Circuits.Boolean.Layered.evalLayer_identityLayer (inputs : List Bool) : evalLayer inputs (identityLayer inputs.length) = inputs

@[simp]

theorem Cslib.Circuits.Boolean.Layered.eval_replicate_identityLayer (inputs : List Bool) (count : ℕ) : eval inputs (List.replicate count (identityLayer inputs.length)) = inputs

@[simp]

theorem Cslib.Circuits.Boolean.Layered.outputWidth_replicate_identityLayer (width count : ℕ) : outputWidth width (List.replicate count (identityLayer width)) = width

theorem Cslib.Circuits.Boolean.Layered.wellFormed_replicate_identityLayer (width count : ℕ) : WellFormed width (List.replicate count (identityLayer width))

def Cslib.Circuits.Boolean.Layered.padTo (inputCount target : ℕ) (layers : List (List Node)) : List (List Node)

Extend a schedule to target layers by copying its final row. Longer schedules are retained.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_padTo (inputCount target : ℕ) (layers : List (List Node)) : (padTo inputCount target layers).length = max layers.length target

theorem Cslib.Circuits.Boolean.Layered.length_padTo_of_le (inputCount target : ℕ) (layers : List (List Node)) (h : layers.length ≤ target) : (padTo inputCount target layers).length = target

@[simp]

theorem Cslib.Circuits.Boolean.Layered.padTo_eq_self (inputCount target : ℕ) (layers : List (List Node)) (h : target ≤ layers.length) : padTo inputCount target layers = layers

@[simp]

theorem Cslib.Circuits.Boolean.Layered.eval_padTo (inputs : List Bool) (target : ℕ) (layers : List (List Node)) : eval inputs (padTo inputs.length target layers) = eval inputs layers

The input count must describe the actual input row; reference validity is unnecessary.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.outputWidth_padTo (inputCount target : ℕ) (layers : List (List Node)) : outputWidth inputCount (padTo inputCount target layers) = outputWidth inputCount layers

theorem Cslib.Circuits.Boolean.Layered.WellFormed.padTo {inputCount : ℕ} {layers : List (List Node)} (h : WellFormed inputCount layers) (target : ℕ) : WellFormed inputCount (Layered.padTo inputCount target layers)