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: a complete record and its bit encoding.
• Cslib.Circuits.Boolean.Iteration.Record.initial: checkpoints, then the orbit prefix, then padding.
• Cslib.Circuits.Boolean.Iteration.Record.Witness: what a detected collision certifies.
• Cslib.Circuits.Boolean.Iteration.Record.sorted, Record.detect: sort and 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

@[simp]

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

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

theorem Cslib.Circuits.Boolean.Iteration.Record.key_decode {n w : ℕ} (bits : BitString (width n w)) : (decode bits).key = toLex (bits ∘ keyBits)

The sort key of a decoded record is read from its key coordinates.

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

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

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.

theorem Cslib.Circuits.Boolean.Iteration.Record.initial_stored {n w M R : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (hR : M + (K + 1) ≤ R) (j : Fin M) : initial f T K checkpoints x ⟨↑j, ⋯⟩ = stored (checkpoints j) (f^[T - K] (checkpoints j))

theorem Cslib.Circuits.Boolean.Iteration.Record.initial_query {n w M R : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (hR : M + (K + 1) ≤ R) (j : Fin (K + 1)) : initial f T K checkpoints x ⟨M + ↑j, ⋯⟩ = query (f^[↑j] x) ↑j

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.

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

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.

theorem Cslib.Circuits.Boolean.Iteration.Record.collision_witness {n w M : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (a b : Record n w) (ha : Valid f T K checkpoints x a) (hb : Valid f T K checkpoints x b) (hc : a.collision b = true) : Witness f T K checkpoints x a b

A collision between valid records is a witness, without requiring unique records.

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

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.

theorem Cslib.Circuits.Boolean.Iteration.Record.sorted_perm {n w : ℕ} (d : ℕ) (records : Fin (BitonicSort.arity d) → Record n w) : (List.ofFn (sorted d records)).Perm (List.ofFn records)

theorem Cslib.Circuits.Boolean.Iteration.Record.monotone_key_sorted {n w : ℕ} (d : ℕ) (records : Fin (BitonicSort.arity d) → Record n w) : Monotone (key ∘ sorted d records)

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.initial_collision {n w M R : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (hR : M + (K + 1) ≤ R) (hK : K < 2 ^ w) (hcover : (∃ d ≤ K, ∃ (h : Fin M), f^[d] x = checkpoints h) ∨ ∃ (i : ℕ) (j : ℕ), i < j ∧ j ≤ K ∧ f^[i] x = f^[j] x) : ∃ (a : Fin R) (b : Fin R), initial f T K checkpoints x a ≠ initial f T K checkpoints x b ∧ (initial f T K checkpoints x a).key = (initial f T K checkpoints x b).key ∧ (initial f T K checkpoints x a).padding = false

A checkpoint hit or a repeat of the prefix gives two different initial records with equal keys, the first of which is not padding.

theorem Cslib.Circuits.Boolean.Iteration.Record.sorted_has_collision {n w : ℕ} (d : ℕ) (records : Fin (BitonicSort.arity d) → Record n w) (hex : ∃ (a : Fin (BitonicSort.arity d)) (b : Fin (BitonicSort.arity d)), records a ≠ records b ∧ (records a).key = (records b).key ∧ (records a).padding = false) : ∃ (j : Fin (BitonicSort.arity d - 1)), (adjacentPair (sorted d records) j).1.collision (adjacentPair (sorted d records) j).2 = true

Sorting turns such a pair into a flagged adjacent pair.

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.