Documentation

Complexity.Computability.Circuit.Boolean.BatchLookup

Batched table lookup with one sort #

A fixed table is hardwired into one source record per address. Query addresses are input wires; queries and padding are destination records. Sort once, broadcast matching source values, and reverse the saved sorting decisions on the values alone. Selecting the original request positions then returns the answers in input order, including repeated addresses. No request identifiers or restoration ranks are used. Empty keys, empty values, and zero requests are allowed.

The circuit uses CSLib's native Circuit representation. Input preparation shares exactly two constant gates, including when one or both are unused. The exact weighted cost and total gate count include these constants; the polynomial gate bound does not certify constructor runtime.

Main definitions #

Main results #

References #

Simplifies the nonuniform lookup construction in S. Schlesinger, Boolean circuit mass production formalization, using the sorting network of K. E. Batcher, Sorting Networks and Their Applications.

source
def Cslib.Circuits.Boolean.batchLookupCircuit.withPadding {k v requests padding d : ℕ} (table : BitString k → BitString v) (h : requests + (2 ^ k + padding) = BitonicSort.arity d) :
Circuit signature (requests * k) (requests * v)

Batched lookup using a specified power-of-two record count and padding.

Instances For
    source
    theorem Cslib.Circuits.Boolean.batchLookupCircuit.eval_withPadding {k v requests padding d : ℕ} (table : BitString k → BitString v) (h : requests + (2 ^ k + padding) = BitonicSort.arity d) (x : BitString (requests * k)) :
    directProductInput ((withPadding table h).eval interpretation x) = table ∘ directProductInput x

    Every request receives its table value, including repeated addresses.

    source
    theorem Cslib.Circuits.Boolean.batchLookupCircuit.cost_program_withPadding {k v requests padding d : ℕ} (table : BitString k → BitString v) (h : requests + (2 ^ k + padding) = BitonicSort.arity d) (cost : signature.Op → ℕ) :
    (withPadding table h).program.cost cost = (routeValuesCircuit Fin.castSucc (Fin.last k) d v).program.cost cost + cost (Op.const false) + cost (Op.const true)

    Input preparation adds exactly two shared constant gates to the routing cost.

    source
    theorem Cslib.Circuits.Boolean.batchLookupCircuit.size_withPadding {k v requests padding d : ℕ} (table : BitString k → BitString v) (h : requests + (2 ^ k + padding) = BitonicSort.arity d) :
    (withPadding table h).size = BitonicSort.sortTraceSize d * (12 * (k + v) + 14) + (1 + (BitonicSort.arity d - 1) * (6 * k + 1) + v * (1 + 4 * BitonicSort.arity d)) + 2

    Exact total gate count, including all constants and negations.

    source
    theorem Cslib.Circuits.Boolean.batchLookupCircuit.size_withPadding_le {k v requests padding d : ℕ} (table : BitString k → BitString v) (h : requests + (2 ^ k + padding) = BitonicSort.arity d) :
    (withPadding table h).size ≤ 24 * BitonicSort.arity d * (d + 1) ^ 2 * (k + v + 1)

    A factored gate bound, linear in record count and field width and quadratic in depth.

    source
    @[reducible, inline]
    abbrev Cslib.Circuits.Boolean.batchLookupCircuit.depth (requests k : ℕ) :
    ℕ

    The least sorting depth accommodating all requests and one source per address.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Circuits.Boolean.batchLookupCircuit.padding (requests k : ℕ) :
      ℕ

      The number of unused destinations filling the next power-of-two record count.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.batchLookupCircuit.add_padding_eq_arity (requests k : ℕ) :
        requests + (2 ^ k + padding requests k) = BitonicSort.arity (depth requests k)

        The canonical padding fills its sorting network exactly.

        source
        def Cslib.Circuits.Boolean.batchLookupCircuit {k v : ℕ} (table : BitString k → BitString v) (requests : ℕ) :
        Circuit signature (requests * k) (requests * v)

        Look up all input addresses in one hardwired table, preserving request order. Padding and sorting depth are inferred from the number of requests and the key width.

        Instances For
          source
          @[simp]
          theorem Cslib.Circuits.Boolean.eval_batchLookupCircuit {k v : ℕ} (table : BitString k → BitString v) (requests : ℕ) (x : BitString (requests * k)) :
          (batchLookupCircuit table requests).eval interpretation x = blockMap table requests x

          The complete circuit computes the table value at each input address.

          source
          theorem Cslib.Circuits.Boolean.size_batchLookupCircuit_le {k v : ℕ} (table : BitString k → BitString v) (requests : ℕ) :
          (batchLookupCircuit table requests).size ≤ 48 * (requests + 2 ^ k) * (Nat.clog 2 (requests + 2 ^ k) + 1) ^ 2 * (k + v + 1)

          Batched lookup uses at most the displayed bound in table size plus request count. This bounds circuit gates, not the running time of the circuit constructor.

          source
          theorem Cslib.Circuits.Boolean.complexity_blockMap_le_lookup {k v : ℕ} (table : BitString k → BitString v) (requests : ℕ) :
          complexity interpretation (blockMap table requests) ≤ 48 * (requests + 2 ^ k) * (Nat.clog 2 (requests + 2 ^ k) + 1) ^ 2 * (k + v + 1)

          Independent applications of any fixed table admit a shared lookup circuit.