Depth and cycle-label feature extraction for pair inputs

Given a pair input z : BitString (n + n) split into inputLeft z and inputRight z, this module packages the synthesis of the (n + 3)-bit transient depth words (depthWord) and the cycle-label components (canonicalCycle, lengthWord, phaseWord) from precomputed depth and cycle-label circuits.

Main definitions

• Cslib.Circuits.Boolean.Iteration.inputLeft: first n-bit state of a (n + n)-bit input.
• Cslib.Circuits.Boolean.Iteration.inputRight: second n-bit state of a (n + n)-bit input.

Main results

• Cslib.Circuits.Boolean.Iteration.synthesis_depthWord: extracts depthWord f (x z) from a depth circuit.
• Cslib.Circuits.Boolean.Iteration.synthesis_label_parts: extracts the canonical cycle representative, cycle length word, and phase word from a cycle-label circuit.

References

• Adapted from lean/Proofs/NavigationFeatures.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.Circuits.Boolean.Iteration.inputLeft {n : ℕ} (z : BitString (n + n)) : BitString n

The first n-bit state in a pair input.

def Cslib.Circuits.Boolean.Iteration.inputRight {n : ℕ} (z : BitString (n + n)) : BitString n

The second n-bit state in a pair input.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_depthWord {n : ℕ} (f : BitString n → BitString n) (depth : Circuit signature n (n + 2)) (hd : ∀ (x : Fin n → Bool), word (depth.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth f x)) (s : Set (BooleanFunction (n + n))) (x : BitString (n + n) → BitString n) (hx : wires x ⊆ s) (hz : (fun (x : BitString (n + n)) => false) ∈ s) : Synthesis interpretation s (wordWires fun (z : BitString (n + n)) => depthWord f (x z)) depth.size

Evaluate a depth circuit on an available state and widen its output to n + 3 bits.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_label_parts {n : ℕ} (f : BitString n → BitString n) (label : Circuit signature n (labelWidth n)) (hl : ∀ (x : Fin n → Bool), label.eval interpretation x = canonicalLabel f x) (s : Set (BooleanFunction (n + n))) (x : BitString (n + n) → BitString n) (hx : wires x ⊆ s) : Synthesis interpretation s (((wires fun (z : BitString (n + n)) => FunctionalGraph.canonicalCycle f (x z)) ∪ wordWires fun (z : BitString (n + n)) => lengthWord f (x z)) ∪ wordWires fun (z : BitString (n + n)) => phaseWord f (x z)) label.size

Evaluate a cycle-label circuit on an available state and unpack its three fields.