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.depthWord, Cslib.Circuits.Boolean.Iteration.phaseWord, Cslib.Circuits.Boolean.Iteration.lengthWord: (n + 3)-bit words for transient depth, phase, and cycle length.
• Cslib.Circuits.Boolean.Iteration.navigationGap, Cslib.Circuits.Boolean.Iteration.navigationDistance: depth difference and cyclic phase difference as (n + 3)-bit words.
• Cslib.Circuits.Boolean.Iteration.navigationFlag, Cslib.Circuits.Boolean.Iteration.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

The transient depth of any n-bit state is strictly less than 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

depthWord f x has natural value 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

phaseWord f x has natural value 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

lengthWord f x has natural value 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

When transientDepth f y ≤ transientDepth f x, navigationGap f x y has natural value transientDepth f x - transientDepth f 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

depthWord f x is zero if and only if 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

The word-level reachability flag navigationFlag f x y agrees with 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

When y is reachable from x, navigationTime f x y has natural value 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

Bit 0 of navigationBits f x y is true iff y is reachable from x under f.

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.