Synthesizing the transient compressed-forest reachability flag

Given a circuit c computing f : BitString n → BitString n, a depth circuit depth, and tables : ForestCircuitTables f L, this module synthesizes the 1-bit circuit deciding reachability ∃ t, f^[t] (inputLeft z) = inputRight z whenever the target inputRight z is transient (0 < transientDepth f (inputRight z)).

Main definitions

• Cslib.Circuits.Boolean.Iteration.transientForestCost: gate budget of the transient compressed-forest reachability subcircuit.

Main results

• Cslib.Circuits.Boolean.Iteration.synthesis_transient_forest_reachability: synthesizes a 1-bit circuit deciding reachability to transient targets within transientForestCost.

References

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

def Cslib.Circuits.Boolean.Iteration.transientForestCost (n s d M E L : ℕ) : ℕ

Gate budget for the transient compressed-forest reachability query.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_transient_forest_reachability {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (depth : Circuit signature n (n + 2)) (hd : ∀ (x : Fin n → Bool), word (depth.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth (c.eval interpretation) x)) (tables : ForestCircuitTables (c.eval interpretation) L) : ∃ (out : Circuit signature (n + n) 1), (∀ (z : BitString (n + n)), 0 < FunctionalGraph.transientDepth (c.eval interpretation) (inputRight z) → (out.eval interpretation z 0 = true ↔ ∃ (t : ℕ), (c.eval interpretation)^[t] (inputLeft z) = inputRight z)) ∧ out.size ≤ transientForestCost n c.size depth.size tables.markCount tables.edgeTable.count L

Synthesize the transient reachability flag from a depth circuit and forest tables.