Polynomial-time operations on layered Boolean circuits

Node tags and binary wire indices are read from their actual encoding. Lookups use the binary index calculus, which bounds an index before converting it to unary. Invalid references retain the specified fallback without running for time proportional to the numerical index.

Main results

• Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeCode: read a node's code.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeConst, computableInPolyTime_nodeCopy, computableInPolyTime_nodeNand: construct nodes.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeEval: evaluate one node.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_evalLayer: evaluate one layer.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_select: select ordered outputs.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_outputWidth: compute the final row width in unary, retaining the input width for an empty schedule.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeCode : Turing.MultiTapeTM.ComputableInPolyTime Node.code encNode (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

Read the two tag bits and two binary wire indices without changing the encoding.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeConst : Turing.MultiTapeTM.ComputableInPolyTime Node.const Turing.MultiTapeTM.encBool encNode

Construct a constant node.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeCopy : Turing.MultiTapeTM.ComputableInPolyTime Node.copy Turing.MultiTapeTM.encNat encNode

Construct a copy node, preserving the binary wire index.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeNand : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => Node.nand p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) encNode

Construct a NAND node, preserving both binary wire indices.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_nodeEval {α : Type} {input : α ↪ List Bool} {node : α → Node} {inputs : α → List Bool} (hnode : Turing.MultiTapeTM.ComputableInPolyTime node input encNode) (hinputs : Turing.MultiTapeTM.ComputableInPolyTime inputs input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Node.eval (inputs a) (node a)) input Turing.MultiTapeTM.encBool

Node evaluation is polynomial in the encoded input, including invalid binary wire indices.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_evalLayer {α : Type} {input : α ↪ List Bool} {layer : α → List Node} {inputs : α → List Bool} (hlayer : Turing.MultiTapeTM.ComputableInPolyTime layer input (Turing.MultiTapeTM.encList encNode)) (hinputs : Turing.MultiTapeTM.ComputableInPolyTime inputs input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evalLayer (inputs a) (layer a)) input Turing.MultiTapeTM.encBits

Evaluate a computed layer, preserving the raw bit-string output encoding.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_select {α : Type} {input : α ↪ List Bool} {inputs : α → List Bool} {outputs : α → List ℕ} (hinputs : Turing.MultiTapeTM.ComputableInPolyTime inputs input Turing.MultiTapeTM.encBits) (houtputs : Turing.MultiTapeTM.ComputableInPolyTime outputs input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => select (inputs a) (outputs a)) input Turing.MultiTapeTM.encBits

Free output selection is polynomial even for malformed binary indices.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_outputWidth {α : Type} {input : α ↪ List Bool} {inputCount : α → ℕ} {layers : α → List (List Node)} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hlayers : Turing.MultiTapeTM.ComputableInPolyTime layers input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList encNode))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => outputWidth (inputCount a) (layers a)) input Turing.MultiTapeTM.encUnary

Read the last layer's length, or retain the computed input width for an empty schedule.