Shared OR lookup over dynamic records

Sources supply keys and value fields; queries supply keys. One source array serves every query, including repeated queries. A query receives the bitwise OR of all matching source values; missing keys receive zero. The circuit sorts once and reverses saved swaps on the answer fields, so it needs neither request identifiers nor a second sort.

Inputs are ordinary variables or Boolean constants, using the existing substitute interface. All constants and negations are charged. Input preparation uses two shared constant gates even when unused. Sources, queries, keys, and values may all be empty. Padding records are destinations and cannot introduce a spurious source. These gate bounds do not certify constructor runtime.

Main definitions

• Cslib.Circuits.Boolean.batchOrCircuit: shared OR lookup with automatic padding.
• Cslib.Circuits.Boolean.batchOrCircuit.withPadding: the same construction with supplied padding.

Main results

• Cslib.Circuits.Boolean.eval_batchOrCircuit_iff: exact matching-source semantics.
• Cslib.Circuits.Boolean.batchOrCircuit.cost_program_withPadding: arbitrary weighted cost.
• Cslib.Circuits.Boolean.batchOrCircuit.size_withPadding: exact gate count.
• Cslib.Circuits.Boolean.size_batchOrCircuit_le: a factored bound for canonical padding.

References

Simplifies MassProduction/Nonuniform/BatchOrCircuit.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.batchOrCircuit.rows {input sources requests k v padding : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) : Fin (requests + (sources + padding)) → Fin (k + 1 + v) → Fin input ⊕ Bool

Symbolic request records, source records, and padding destinations.

def Cslib.Circuits.Boolean.batchOrCircuit.substitution {input sources requests k v padding d : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (h : requests + (sources + padding) = BitonicSort.arity d) : Fin (BitonicSort.arity d * (k + 1 + v)) → Fin input ⊕ Bool

Flatten symbolic records into variables and constants for the padded network.

def Cslib.Circuits.Boolean.batchOrCircuit.requestIndex {sources requests padding d : ℕ} (h : requests + (sources + padding) = BitonicSort.arity d) (request : Fin requests) : Fin (BitonicSort.arity d)

The original position of a request in the padded layout.

def Cslib.Circuits.Boolean.batchOrCircuit.outputs {sources requests v padding d : ℕ} (h : requests + (sources + padding) = BitonicSort.arity d) : Circuit signature (BitonicSort.arity d * v) (requests * v)

Select the values at the original request positions by free wiring.

def Cslib.Circuits.Boolean.batchOrCircuit.withPadding {input sources requests k v padding d : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (h : requests + (sources + padding) = BitonicSort.arity d) : Circuit signature input (requests * v)

Shared OR lookup with a supplied power-of-two record count.

theorem Cslib.Circuits.Boolean.batchOrCircuit.eval_withPadding_iff {input sources requests k v padding d : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (h : requests + (sources + padding) = BitonicSort.arity d) (x : BitString input) (request : Fin requests) (bit : Fin v) : (withPadding sourceKeys sourceValues queryKeys h).eval interpretation x (finProdFinEquiv (request, bit)) = true ↔ ∃ (source : Fin sources), substitute (sourceKeys source) x = substitute (queryKeys request) x ∧ substitute (sourceValues source) x bit = true

A query bit is true exactly when some matching source bit is true.

theorem Cslib.Circuits.Boolean.batchOrCircuit.cost_program_withPadding {input sources requests k v padding d : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (h : requests + (sources + padding) = BitonicSort.arity d) (cost : signature.Op → ℕ) : (withPadding sourceKeys sourceValues queryKeys 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 one shared gate for each Boolean constant.

theorem Cslib.Circuits.Boolean.batchOrCircuit.size_withPadding {input sources requests k v padding d : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (h : requests + (sources + padding) = BitonicSort.arity d) : (withPadding sourceKeys sourceValues queryKeys 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 gate count, including constants and negations, independent of the selectors.

theorem Cslib.Circuits.Boolean.batchOrCircuit.size_withPadding_le {input sources requests k v padding d : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (h : requests + (sources + padding) = BitonicSort.arity d) : (withPadding sourceKeys sourceValues queryKeys h).size ≤ 24 * BitonicSort.arity d * (d + 1) ^ 2 * (k + v + 1)

A bound linear in the record count and field width, and quadratic in sorting depth.

def Cslib.Circuits.Boolean.batchOrCircuit.depth (requests sources : ℕ) : ℕ

The least sorting depth accommodating the requests and sources; zero records use depth zero.

def Cslib.Circuits.Boolean.batchOrCircuit.padding (requests sources : ℕ) : ℕ

Unused destination slots filling the next power-of-two record count.

theorem Cslib.Circuits.Boolean.batchOrCircuit.add_padding_eq_arity (requests sources : ℕ) : requests + (sources + padding requests sources) = BitonicSort.arity (depth requests sources)

Padding fills the network exactly, also for an empty batch.

theorem Cslib.Circuits.Boolean.batchOrCircuit.arity_depth_le (requests sources : ℕ) : BitonicSort.arity (depth requests sources) ≤ 2 * (requests + sources + 1)

Canonical padding is linear in the total record count, including the empty batch.

def Cslib.Circuits.Boolean.batchOrCircuit {input sources requests k v : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) : Circuit signature input (requests * v)

Look up bitwise ORs of dynamic source values with automatic padding. Source and query keys may repeat, and absent keys return false.

theorem Cslib.Circuits.Boolean.eval_batchOrCircuit_iff {input sources requests k v : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (x : BitString input) (request : Fin requests) (bit : Fin v) : (batchOrCircuit sourceKeys sourceValues queryKeys).eval interpretation x (finProdFinEquiv (request, bit)) = true ↔ ∃ (source : Fin sources), substitute (sourceKeys source) x = substitute (queryKeys request) x ∧ substitute (sourceValues source) x bit = true

An output bit is true exactly when a matching source bit is true.

theorem Cslib.Circuits.Boolean.size_batchOrCircuit_le {input sources requests k v : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) : (batchOrCircuit sourceKeys sourceValues queryKeys).size ≤ 48 * (requests + sources + 1) * (Nat.clog 2 (requests + sources) + 1) ^ 2 * (k + v + 1)

Canonical shared OR lookup has linear record-count cost up to the displayed factors. This is a circuit gate bound, not a certificate of constructor runtime.