Bit-vector records and fixed dictionaries for compressed-forest navigation

This module encodes the subtree interval labels (low x, high x) and the edge-anchor records (a, low a, high a, depthWord f a) of a compressed checkpoint forest as fixed-width bit strings, wraps synthesis_lookupOr into synthesis_fixed_dictionary returning hit flags and value records, and packages the nonconstructive forest tables (ForestCircuitTables) needed by the reachability circuit.

Main definitions

• Cslib.Circuits.Boolean.Iteration.forestLabelWord: packs (low x, high x) as two (n + 1)-bit words.
• Cslib.Circuits.Boolean.Iteration.forestAnchorWord: packs (x, forestLabelWord low high x, depthWord f x).
• Cslib.Circuits.Boolean.Iteration.dictionaryCost: gate count of a shared fixed-dictionary lookup.
• Cslib.Circuits.Boolean.Iteration.ForestCircuitTables: combined mark and compressed-edge tables for a functional graph on BitString n.

Main results

• Cslib.Circuits.Boolean.Iteration.forest_label_interval: interval containment on unpacked (n + 1)-bit words matches low y ≤ low x ∧ low x ≤ high y.
• Cslib.Circuits.Boolean.Iteration.synthesis_fixed_dictionary: synthesizes hit flags and value records for Q queries into an M-entry dictionary.
• Cslib.Circuits.Boolean.Iteration.exists_forest_circuit_tables: existence of ForestCircuitTables f L for 0 < L.

References

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

def Cslib.Circuits.Boolean.Iteration.forestLabelWord {n : ℕ} (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : BitString (n + 1 + (n + 1))

Two (n + 1)-bit words holding the lower and upper subtree ranks of a state.

def Cslib.Circuits.Boolean.Iteration.forestLowWord {n : ℕ} (r : BitString (n + 1 + (n + 1))) : BitVec (n + 1)

Unpack the lower subtree rank word from a forest label record.

def Cslib.Circuits.Boolean.Iteration.forestHighWord {n : ℕ} (r : BitString (n + 1 + (n + 1))) : BitVec (n + 1)

Unpack the upper subtree rank word from a forest label record.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.forestLowWord_bits {n : ℕ} (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestLowWord (forestLabelWord low high x) = BitVec.ofNat (n + 1) ↑(low x)

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.forestHighWord_bits {n : ℕ} (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestHighWord (forestLabelWord low high x) = BitVec.ofNat (n + 1) ↑(high x)

theorem Cslib.Circuits.Boolean.Iteration.forestLowWord_toNat {n : ℕ} (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : (forestLowWord (forestLabelWord low high x)).toNat = ↑(low x)

theorem Cslib.Circuits.Boolean.Iteration.forestHighWord_toNat {n : ℕ} (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : (forestHighWord (forestLabelWord low high x)).toNat = ↑(high x)

theorem Cslib.Circuits.Boolean.Iteration.forest_label_interval {n : ℕ} (low high : BitString n → Fin (Nat.card (BitString n))) (a h : BitString n) : (!(forestLowWord (forestLabelWord low high h)).ult (forestLowWord (forestLabelWord low high a)) && !(forestHighWord (forestLabelWord low high a)).ult (forestLowWord (forestLabelWord low high h))) = true ↔ low a ≤ low h ∧ low h ≤ high a

Word-level interval containment on unpacked (n + 1)-bit words matches rank containment.

noncomputable def Cslib.Circuits.Boolean.Iteration.forestAnchorWord {n : ℕ} (f : BitString n → BitString n) (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : BitString (n + (n + 1 + (n + 1)) + (n + 3))

An anchor record packs a marked state, its two interval words, and its (n + 3)-bit depth.

def Cslib.Circuits.Boolean.Iteration.forestAnchorState {n : ℕ} (r : BitString (n + (n + 1 + (n + 1)) + (n + 3))) : BitString n

Unpack the marked state from an anchor record.

def Cslib.Circuits.Boolean.Iteration.forestAnchorLabels {n : ℕ} (r : BitString (n + (n + 1 + (n + 1)) + (n + 3))) : BitString (n + 1 + (n + 1))

Unpack the interval label pair from an anchor record.

def Cslib.Circuits.Boolean.Iteration.forestAnchorDepth {n : ℕ} (r : BitString (n + (n + 1 + (n + 1)) + (n + 3))) : BitVec (n + 3)

Unpack the (n + 3)-bit transient depth word from an anchor record.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.forestAnchorState_bits {n : ℕ} (f : BitString n → BitString n) (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestAnchorState (forestAnchorWord f low high x) = x

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.forestAnchorLabels_bits {n : ℕ} (f : BitString n → BitString n) (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestAnchorLabels (forestAnchorWord f low high x) = forestLabelWord low high x

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.forestAnchorDepth_bits {n : ℕ} (f : BitString n → BitString n) (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestAnchorDepth (forestAnchorWord f low high x) = depthWord f x

def Cslib.Circuits.Boolean.Iteration.dictionaryCost (n v M Q : ℕ) : ℕ

Gate bound for a shared fixed-dictionary lookup with M keys and Q queries of v-bit records.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_fixed_dictionary {n a v M Q : ℕ} (s : Set (BooleanFunction a)) (keys : Fin M → BitString n) (hkeys : Function.Injective keys) (values : Fin M → BitString v) (queries : BitString a → Fin Q → BitString n) (hq : ∀ (j : Fin Q), (wires fun (z : BitString a) => queries z j) ⊆ s) : ∃ (flags : BitString a → Fin Q → Bool) (records : BitString a → Fin Q → BitString v), (∀ (z : BitString a) (j : Fin Q), (flags z j = true ↔ ∃ (i : Fin M), keys i = queries z j) ∧ ∀ (i : Fin M), keys i = queries z j → records z j = values i) ∧ Synthesis interpretation s ((Set.range fun (j : Fin Q) (z : Fin a → Bool) => flags z j) ∪ ⋃ (j : Fin Q), wires fun (z : BitString a) => records z j) (dictionaryCost n v M Q)

Shared lookup for a fixed injective dictionary, returning hit flags and v-bit records.

structure Cslib.Circuits.Boolean.Iteration.ForestCircuitTables {n : ℕ} (f : BitString n → BitString n) (L : ℕ) : Type

Combined checkpoint-mark and compressed-edge tables for a functional graph on BitString n.

• H : Finset (BitString n)

  Underlying checkpoint set.

• cover (x : BitString n) : FunctionalGraph.Repeats f x L ∨ ∃ t < 2 * L, f^[t] x ∈ self.H

  Every L-step prefix either repeats or hits H within 2 * L steps.

• low : BitString n → Fin (Nat.card (BitString n))

  Lower subtree rank label.

• high : BitString n → Fin (Nat.card (BitString n))

  Upper subtree rank label.

• interval (x y : BitString n) : self.low y ≤ self.low x ∧ self.low x ≤ self.high y ↔ ∃ t ≤ FunctionalGraph.transientDepth f x, f^[t] x = y

  Subtree interval containment characterizes ancestry before cycle entry.

• markCount : ℕ

  Number of refined forest marks.

• marks : Fin self.markCount → BitString n

  Enumeration of the refined forest marks.

• marks_injective : Function.Injective self.marks

  Refined marks are pairwise distinct.

• marks_mem (x : BitString n) : x ∈ FunctionalGraph.forestMarks f self.H ↔ ∃ (i : Fin self.markCount), self.marks i = x

  marks enumerates forestMarks f H exactly.

• markCount_le : self.markCount ≤ 2 * (2 ^ n / L)

  At most 2 * (2 ^ n / L) refined marks exist.

• edgeTable : FunctionalGraph.ForestEdgeTable f self.H L

  Compressed-edge table for non-root marks.

• edgeCount_le : self.edgeTable.count ≤ 2 * (2 ^ n / L)

  At most 2 * (2 ^ n / L) compressed edges exist.

theorem Cslib.Circuits.Boolean.Iteration.exists_forest_circuit_tables {n : ℕ} (f : BitString n → BitString n) (L : ℕ) (hL : 0 < L) : Nonempty (ForestCircuitTables f L)

Existence of ForestCircuitTables f L for any 0 < L.