Records for detecting checkpoint hits and repeats

The fixed-power circuit sorts one array of records. Stored records carry a checkpoint state and a payload, queries carry a state of the orbit prefix and its time, and padding fills the array. Records are sorted by a padding flag followed by their state, so that padding comes last. Both a checkpoint hit and a repeated state appear as two different records with equal keys, and sorting makes such a pair adjacent; a linear scan finds one (detect). The detected pair certifies one of the two situations exactly (detect_sorted_witness), even when complete records repeat. Sorting uses the native Batcher circuit bitonicSortCircuit.

Main definitions

• Cslib.Circuits.Boolean.Iteration.Record, Cslib.Circuits.Boolean.Iteration.Record.width, Cslib.Circuits.Boolean.Iteration.Record.key, Cslib.Circuits.Boolean.Iteration.Record.keyBits, Cslib.Circuits.Boolean.Iteration.Record.encode, Cslib.Circuits.Boolean.Iteration.Record.decode: a complete record, its sort key, and its bit encoding.
• Cslib.Circuits.Boolean.Iteration.Record.query, Cslib.Circuits.Boolean.Iteration.Record.stored, Cslib.Circuits.Boolean.Iteration.Record.pad, Cslib.Circuits.Boolean.Iteration.Record.collision, Cslib.Circuits.Boolean.Iteration.Record.initial, Cslib.Circuits.Boolean.Iteration.Record.Valid: query, checkpoint, and padding records, collision test, initial array, and validity predicate.
• Cslib.Circuits.Boolean.Iteration.Record.Witness: what a detected collision certifies.
• Cslib.Circuits.Boolean.Iteration.Record.pack, Cslib.Circuits.Boolean.Iteration.Record.sorted, Cslib.Circuits.Boolean.Iteration.Record.adjacentPair, Cslib.Circuits.Boolean.Iteration.Record.detect: array packing, sorting, and adjacent-collision scan.

Main results

• Cslib.Circuits.Boolean.Iteration.Record.detect_sorted_witness: if the orbit prefix reaches a checkpoint or repeats, the detected pair is a witness.

References

• Adapted from lean/Proofs/{Records,Detector}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

structure Cslib.Circuits.Boolean.Iteration.Record (n w : ℕ) : Type

A complete record carried through the sorting network.

• padding : Bool

  Padding records sort after all others and never collide.

• state : BitString n

  The state compared by the sort.

• checkpoint : Bool

  Whether this is a stored checkpoint rather than a query.

• index : BitVec w

  The time of a query in the orbit prefix.

• payload : BitString n

  The shifted state stored with a checkpoint.

theorem Cslib.Circuits.Boolean.Iteration.Record.ext {n w : ℕ} {x y : Record n w} (padding : x.padding = y.padding) (state : x.state = y.state) (checkpoint : x.checkpoint = y.checkpoint) (index : x.index = y.index) (payload : x.payload = y.payload) : x = y

theorem Cslib.Circuits.Boolean.Iteration.Record.ext_iff {n w : ℕ} {x y : Record n w} : x = y ↔ x.padding = y.padding ∧ x.state = y.state ∧ x.checkpoint = y.checkpoint ∧ x.index = y.index ∧ x.payload = y.payload

@[instance_reducible]

instance Cslib.Circuits.Boolean.Iteration.instDecidableEqRecord {n✝ w✝ : ℕ} : DecidableEq (Record n✝ w✝)

def Cslib.Circuits.Boolean.Iteration.instDecidableEqRecord.decEq {n✝ w✝ : ℕ} (x✝ x✝¹ : Record n✝ w✝) : Decidable (x✝ = x✝¹)

def Cslib.Circuits.Boolean.Iteration.Record.width (n w : ℕ) : ℕ

The number of bits of a record: its key, then its remaining fields.

def Cslib.Circuits.Boolean.Iteration.Record.key {n w : ℕ} (r : Record n w) : Lex (Fin (n + 1) → Bool)

The sort key: the padding flag, then the state.

def Cslib.Circuits.Boolean.Iteration.Record.keyBits {n w : ℕ} : Fin (n + 1) → Fin (width n w)

The key coordinates of an encoded record.

def Cslib.Circuits.Boolean.Iteration.Record.encode {n w : ℕ} (r : Record n w) : BitString (width n w)

The bits of a record: padding flag and state, then checkpoint flag, index and payload.

def Cslib.Circuits.Boolean.Iteration.Record.decode {n w : ℕ} (bits : BitString (width n w)) : Record n w

The record with the given bits; inverse to encode.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.Record.decode_encode {n w : ℕ} (r : Record n w) : decode r.encode = r

Decoding the bit encoding of a record recovers the record.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.Record.encode_decode {n w : ℕ} (bits : BitString (width n w)) : (decode bits).encode = bits

Encoding the decoded record of a bit string recovers the bit string.

theorem Cslib.Circuits.Boolean.Iteration.Record.encode_injective {n w : ℕ} : Function.Injective encode

Record bit encoding encode is injective.

theorem Cslib.Circuits.Boolean.Iteration.Record.key_eq_iff {n w : ℕ} (a b : Record n w) : a.key = b.key ↔ a.padding = b.padding ∧ a.state = b.state

Two records have equal sort keys iff they have the same padding flag and state.

def Cslib.Circuits.Boolean.Iteration.Record.query {n w : ℕ} (state : BitString n) (index : ℕ) : Record n w

A query for the state at time index of the orbit prefix.

def Cslib.Circuits.Boolean.Iteration.Record.stored {n w : ℕ} (state payload : BitString n) : Record n w

A stored checkpoint with its payload.

def Cslib.Circuits.Boolean.Iteration.Record.pad {n w : ℕ} : Record n w

A padding record.

def Cslib.Circuits.Boolean.Iteration.Record.collision {n w : ℕ} (a b : Record n w) : Bool

Two records collide when neither is padding, their states agree, and they differ.

theorem Cslib.Circuits.Boolean.Iteration.Record.collision_iff {n w : ℕ} (a b : Record n w) : a.collision b = true ↔ a.padding = false ∧ b.padding = false ∧ a.state = b.state ∧ a ≠ b

collision a b holds iff neither record is padding, their states are equal, and the records are distinct.

def Cslib.Circuits.Boolean.Iteration.Record.initial {n w M R : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (j : Fin R) : Record n w

The initial array: stored checkpoints, then the orbit prefix up to time K, then padding. Checkpoint h stores the state T - K steps later.

def Cslib.Circuits.Boolean.Iteration.Record.Valid {n w M : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (r : Record n w) : Prop

A record that is padding, a stored checkpoint, or a query of the orbit prefix.

inductive Cslib.Circuits.Boolean.Iteration.Record.Witness {n w M : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) : Record n w → Record n w → Prop

What a collision certifies: the prefix reaches a checkpoint, or it repeats.

• hitLeft {n w M : ℕ} {f : BitString n → BitString n} {T K : ℕ} {checkpoints : Fin M → BitString n} {x : BitString n} (h : Fin M) (d : ℕ) (hd : d ≤ K) (heq : f^[d] x = checkpoints h) : Witness f T K checkpoints x (stored (checkpoints h) (f^[T - K] (checkpoints h))) (query (f^[d] x) d)

  A stored checkpoint followed by the prefix state at time d that equals it.

• hitRight {n w M : ℕ} {f : BitString n → BitString n} {T K : ℕ} {checkpoints : Fin M → BitString n} {x : BitString n} (h : Fin M) (d : ℕ) (hd : d ≤ K) (heq : f^[d] x = checkpoints h) : Witness f T K checkpoints x (query (f^[d] x) d) (stored (checkpoints h) (f^[T - K] (checkpoints h)))

  The prefix state at time d followed by the checkpoint it equals.

• repeated {n w M : ℕ} {f : BitString n → BitString n} {T K : ℕ} {checkpoints : Fin M → BitString n} {x : BitString n} (i j : ℕ) (hi : i ≤ K) (hj : j ≤ K) (hne : i ≠ j) (heq : f^[i] x = f^[j] x) : Witness f T K checkpoints x (query (f^[i] x) i) (query (f^[j] x) j)

  Two different times of the prefix with equal states.

Sorting and detection

def Cslib.Circuits.Boolean.Iteration.Record.pack {n w R : ℕ} (records : Fin R → Record n w) : BitString (R * width n w)

Records stored in consecutive blocks of bits.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.Record.directProductInput_pack {n w R : ℕ} (records : Fin R → Record n w) (j : Fin R) : directProductInput (pack records) j = (records j).encode

Extracting the j-th block of pack records gives encode (records j).

def Cslib.Circuits.Boolean.Iteration.Record.sorted {n w : ℕ} (d : ℕ) (records : Fin (BitonicSort.arity d) → Record n w) : Fin (BitonicSort.arity d) → Record n w

Sort records by padding flag and state with the native Batcher circuit.

def Cslib.Circuits.Boolean.Iteration.Record.adjacentPair {n w R : ℕ} (records : Fin R → Record n w) (j : Fin (R - 1)) : Record n w × Record n w

Two adjacent records of an array.

def Cslib.Circuits.Boolean.Iteration.Record.detect {n w R : ℕ} (records : Fin R → Record n w) : Record n w × Record n w

The last colliding adjacent pair, or two padding records if there is none.

theorem Cslib.Circuits.Boolean.Iteration.Record.detect_sorted_witness {n w M : ℕ} (f : BitString n → BitString n) (T K d : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (hR : M + (K + 1) ≤ BitonicSort.arity d) (hK : K < 2 ^ w) (hcover : (∃ t ≤ K, ∃ (h : Fin M), f^[t] x = checkpoints h) ∨ ∃ (i : ℕ) (j : ℕ), i < j ∧ j ≤ K ∧ f^[i] x = f^[j] x) : have pair := detect (sorted d (initial f T K checkpoints x)); Witness f T K checkpoints x pair.1 pair.2

If the prefix up to time K reaches a checkpoint or repeats, the detected pair of the sorted initial array is a witness.