Decoding sparse interval coordinates, including intervals crossing phase zero

Main definitions

• CounterIntervalChart.negativePhase, CounterIntervalChart.phaseDistance, CounterIntervalChart.decodedRow, CounterIntervalChart.decodeFlag: per-interval phase offset, decoded candidate word, and interval match test.
• CounterIntervalChart.decode: recover a state from its representative and phase.

Main results

• CounterIntervalChart.decode_spec: decoding canonical coordinates recovers the state.

References

• Adapted from lean/Proofs/CounterChartDecode.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.negativePhase {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : BitVec (chartWidth n)

Additive inverse of the initial phase modulo the cycle length.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.negativePhase_toNat {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) : (chart.negativePhase j).toNat = (FunctionalGraph.cycleLength f (chart.first j) - FunctionalGraph.phase f (chart.first j)) % FunctionalGraph.cycleLength f (chart.first j)

The natural-number value of chart.negativePhase j is the additive inverse of the initial phase of interval j modulo its cycle length.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.phaseDistance {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (p : BitVec (chartWidth n)) : BitVec (chartWidth n)

Distance from the interval start, modulo its cycle length.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.decodedRow {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (p : BitVec (chartWidth n)) : BitVec n

Recover the word by adding the phase distance to the interval start.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.decodeFlag {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (rep : BitVec n) (p : BitVec (chartWidth n)) : Bool

Test the representative and whether the phase distance lies in the interval.

noncomputable def Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.decode {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (rep : BitVec n) (p : BitVec (chartWidth n)) : BitString n

Select a matching interval and return its decoded word.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.decode_spec {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (y : BitVec n) : chart.decode (FunctionalGraph.canonicalCycle f y) (BitVec.ofNat (chartWidth n) (FunctionalGraph.phase f y)) = fun (i : Fin n) => y.getLsbD ↑i

Decoding the canonical cycle representative and phase of y recovers the bits of y.