Circuit synthesis for reachability and first hitting times

This module synthesizes the navigation word (reaches f x y, hittingTime f x y) on pair inputs z : BitString (n + n) in two ways:

• synthesis_navigation_given_flag: when a circuit transientReach already decides reachability on transient targets (0 < transientDepth f y), we combine two depth circuits, two cycle-label circuits, a streaming modular difference (synthesis_subMod), and word arithmetic to output navigationBits f (inputLeft z) (inputRight z) without evaluating a variable-time iterate;
• synthesis_navigation: when no external transient-reachability circuit is supplied, we evaluate f^[transientDepth f x - transientDepth f y] x by binary powering (synthesis_binary_powering) to decide transient reachability directly.

Main results

• Cslib.Circuits.Boolean.Iteration.synthesis_navigation_given_flag: synthesizes navigationBits using an external transient-reachability circuit.
• Cslib.Circuits.Boolean.Iteration.synthesis_navigation: synthesizes navigationBits using binary powering for the transient check.

References

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

theorem Cslib.Circuits.Boolean.Iteration.synthesis_navigation_given_flag {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)) (label : Circuit signature n (labelWidth n)) (hl : ∀ (x : Fin n → Bool), label.eval interpretation x = canonicalLabel f x) (transientReach : Circuit signature (n + n) 1) (htr : ∀ (z : BitString (n + n)), 0 < FunctionalGraph.transientDepth f (inputRight z) → (transientReach.eval interpretation z 0 = true ↔ ∃ (t : ℕ), f^[t] (inputLeft z) = inputRight z)) : Synthesis interpretation (inputs (n + n)) (Set.range fun (i : Fin (1 + (n + 1))) (z : Fin (n + n) → Bool) => navigationBits f (inputLeft z) (inputRight z) i) (2 + 2 * depth.size + 2 * label.size + transientReach.size + 50 * (n + 4) ^ 2 + (49 * n + 138))

Combine depth, cycle-label, and a supplied transient-reachability flag into the exact reachability bit and first hitting time.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_navigation {n : ℕ} (f : BitString n → BitString n) (K : ℕ) (hpowers : ∀ j < n + 1, ∃ (pow : Circuit signature n n), pow.Computes interpretation f^[2 ^ j] ∧ pow.size ≤ K) (depth : Circuit signature n (n + 2)) (hd : ∀ (x : Fin n → Bool), word (depth.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth f x)) (label : Circuit signature n (labelWidth n)) (hl : ∀ (x : Fin n → Bool), label.eval interpretation x = canonicalLabel f x) : Synthesis interpretation (inputs (n + n)) (Set.range fun (i : Fin (1 + (n + 1))) (z : Fin (n + n) → Bool) => navigationBits f (inputLeft z) (inputRight z) i) (4 + 4 * depth.size + 2 * label.size + (n + 1) * (K + 4 * n) + 50 * (n + 4) ^ 2 + (73 * n + 198))

Combine depth, cycle-label, and binary-powering circuits into the navigation word.