Native Boolean circuits for sparse orbit charts

Constants are supplied by the caller and charged once there. Both chart directions use linear arithmetic per interval and a shared-flag selector. No exponent-dependent circuit is duplicated across the interval table.

Main definitions

• The encode and decode maps are defined in the imported chart modules.

Main results

• CounterIntervalChart.synthesis_encode, CounterIntervalChart.synthesis_decode: linear gate counts in the number of intervals and word width.

References

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

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.synthesis_encode {n R a : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (s : Set (BitString a → Bool)) (x : BitString a → BitVec n) (hx : wordWires x ⊆ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) : Synthesis interpretation s (wires fun (z : BitString a) => chart.encode (x z)) (R * (220 * (n + 3)))

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.synthesis_decode {n R a : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (s : Set (BitString a → Bool)) (rep : BitString a → BitVec n) (p : BitString a → BitVec (chartWidth n)) (hr : wordWires rep ⊆ s) (hp : wordWires p ⊆ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) : Synthesis interpretation s (wires fun (z : BitString a) => chart.decode (rep z) (p z)) (R * (150 * (n + 3)))