First hitting times from words of bounded width

For n-bit states, transient depths, phases and cycle lengths are below 2 ^ n, so they fit in n + 3 bits with room for one addition (depthWord, phaseWord, lengthWord). The closed forms for reachability and first hitting times (FunctionalGraph.reaches, FunctionalGraph.hittingTime) are then word computations from the depths, labels and phases of the two states: a comparison and a difference of depths for a transient target, a modular difference of phases for a periodic one (navigationFlag_eq_reaches, toNat_navigationTime). The output format is one reachability bit and n + 1 time bits (navigationBits); the time is specified only when the target is reachable, where it is below 2 ^ n (navigationBits_time).

These are word-level identities. The circuits that compute depths and labels are in Iteration.Depth and Iteration.LabelCircuit.

Main definitions

• Cslib.Circuits.Boolean.Iteration.navigationFlag, navigationTime: reachability and first hitting time as word computations.
• Cslib.Circuits.Boolean.Iteration.navigationBits: one flag bit and n + 1 time bits.

Main results

• Cslib.Circuits.Boolean.Iteration.navigationFlag_eq_reaches, Cslib.Circuits.Boolean.Iteration.toNat_navigationTime: agreement with the closed forms.
• Cslib.Circuits.Boolean.Iteration.navigationBits_flag, Cslib.Circuits.Boolean.Iteration.navigationBits_time: the output format.

References

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

noncomputable def Cslib.Circuits.Boolean.Iteration.depthWord {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : BitVec (n + 3)

The transient depth of x in n + 3 bits.

noncomputable def Cslib.Circuits.Boolean.Iteration.phaseWord {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : BitVec (n + 3)

The phase of x in n + 3 bits.

noncomputable def Cslib.Circuits.Boolean.Iteration.lengthWord {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : BitVec (n + 3)

The cycle length of x in n + 3 bits.

theorem Cslib.Circuits.Boolean.Iteration.transientDepth_lt_two_pow {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : FunctionalGraph.transientDepth f x < 2 ^ n

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.toNat_depthWord {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : (depthWord f x).toNat = FunctionalGraph.transientDepth f x

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.toNat_phaseWord {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : (phaseWord f x).toNat = FunctionalGraph.phase f x

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.toNat_lengthWord {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : (lengthWord f x).toNat = FunctionalGraph.cycleLength f x

noncomputable def Cslib.Circuits.Boolean.Iteration.navigationGap {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : BitVec (n + 3)

The difference of the transient depths of x and y.

noncomputable def Cslib.Circuits.Boolean.Iteration.navigationDistance {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : BitVec (n + 3)

The phase of y minus the phase of x at the end of its transient, modulo the cycle length of x.

noncomputable def Cslib.Circuits.Boolean.Iteration.navigationFlag {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : Bool

Reachability as a word computation: equal representatives for a periodic target, and a depth comparison and one state comparison for a transient target.

noncomputable def Cslib.Circuits.Boolean.Iteration.navigationTime {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : BitVec (n + 3)

The first hitting time as a word computation.

theorem Cslib.Circuits.Boolean.Iteration.toNat_navigationGap {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) (hle : FunctionalGraph.transientDepth f y ≤ FunctionalGraph.transientDepth f x) : (navigationGap f x y).toNat = FunctionalGraph.transientDepth f x - FunctionalGraph.transientDepth f y

theorem Cslib.Circuits.Boolean.Iteration.toNat_navigationDistance {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : (navigationDistance f x y).toNat = FunctionalGraph.cyclicDistance f x y

theorem Cslib.Circuits.Boolean.Iteration.depthWord_eq_zero_iff {n : ℕ} (f : BitString n → BitString n) (x : BitString n) : depthWord f x = 0 ↔ FunctionalGraph.transientDepth f x = 0

theorem Cslib.Circuits.Boolean.Iteration.navigationFlag_eq_reaches {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : navigationFlag f x y = FunctionalGraph.reaches f x y

theorem Cslib.Circuits.Boolean.Iteration.toNat_navigationTime {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) (h : FunctionalGraph.reaches f x y = true) : (navigationTime f x y).toNat = FunctionalGraph.hittingTime f x y

noncomputable def Cslib.Circuits.Boolean.Iteration.navigationBits {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : BitString (1 + (n + 1))

One reachability bit followed by n + 1 bits of the first hitting time.

theorem Cslib.Circuits.Boolean.Iteration.navigationBits_flag {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) : navigationBits f x y 0 = true ↔ ∃ (t : ℕ), f^[t] x = y

theorem Cslib.Circuits.Boolean.Iteration.navigationBits_time {n : ℕ} (f : BitString n → BitString n) (x y : BitString n) (h : ∃ (t : ℕ), f^[t] x = y) : have t := (word fun (i : Fin (n + 1)) => navigationBits f x y (Fin.natAdd 1 i)).toNat; f^[t] x = y ∧ (∀ j < t, f^[j] x ≠ y) ∧ t < 2 ^ n

The output format. When y is reachable from x, the time bits of navigationBits are the first hitting time, which is below 2 ^ n.