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

An identity layer of width width has width nodes.

@[simp]

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

Evaluating an identity layer of matching width returns the input row unchanged.

@[simp]

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

Evaluating any number of replicated identity layers returns the input row unchanged.

@[simp]

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

Replicated identity layers of width width have output width 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

Padding to target produces max layers.length target layers.

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

When layers.length ≤ target, padding to target produces exactly target layers.

@[simp]

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

When target ≤ layers.length, padTo leaves the schedule unchanged.

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

Padding preserves the output width of a layered schedule.

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

Padding a well-formed layered schedule preserves WellFormed.