Decoding sparse interval coordinates, including intervals crossing phase zero

Main definitions

• 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)

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.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.phaseDistance_toNat {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (p : BitVec (chartWidth n)) (hp : p.toNat < FunctionalGraph.cycleLength f (chart.first j)) : (chart.phaseDistance j p).toNat = (p.toNat + FunctionalGraph.cycleLength f (chart.first j) - FunctionalGraph.phase f (chart.first j) % FunctionalGraph.cycleLength f (chart.first j)) % FunctionalGraph.cycleLength f (chart.first j)

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.phaseDistance_of_contains {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (j : Fin R) (y : BitVec n) (hy : chart.contains j y = true) : (chart.phaseDistance j (BitVec.ofNat (chartWidth n) (FunctionalGraph.phase f y))).toNat = y.toNat - chart.start j

The decoded distance is exactly the numerical offset within a containing interval.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.phaseDistance_hit {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (j : Fin R) (y : BitVec n) (hc : FunctionalGraph.canonicalCycle f (chart.first j) = FunctionalGraph.canonicalCycle f y) : f^[(chart.phaseDistance j (BitVec.ofNat (chartWidth n) (FunctionalGraph.phase f y))).toNat] (chart.first j) = y

On a matching cycle, the decoded distance really reaches the requested state.

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.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.decodedRow_eq {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (j : Fin R) (p : BitVec (chartWidth n)) : chart.decodedRow j p = BitVec.ofNat n (chart.start j + (chart.phaseDistance j p).toNat)

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.

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.decodeFlag_of_contains {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (j : Fin R) (y : BitVec n) (hy : chart.contains j y = true) : chart.decodeFlag j (FunctionalGraph.canonicalCycle f y) (BitVec.ofNat (chartWidth n) (FunctionalGraph.phase f y)) = true

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.decodedRow_spec {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (j : Fin R) (y : BitVec n) (hy : chart.decodeFlag j (FunctionalGraph.canonicalCycle f y) (BitVec.ofNat (chartWidth n) (FunctionalGraph.phase f y)) = true) : chart.decodedRow j (BitVec.ofNat (chartWidth n) (FunctionalGraph.phase f y)) = y

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