A concrete nonuniform batched table lookup circuit

The table has one hardwired source record per address. Query addresses are input wires, and their ordering identifiers are hardwired. The verified two-sort router returns every table value in query order, including repeated addresses. Its charged size is linear in table size plus query count up to the displayed polynomial in bit widths and sorting depth.

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.requestsFit {keyWidth requests padding depth : ℕ} (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) : requests ≤ 2 ^ depth

Query identifiers fit in the sorting depth.

noncomputable def Algebraic.MassProduction.Nonuniform.BatchLookup.layout {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) (input : Fin (requests * keyWidth) → Bool) : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth (depth + 1 + valueWidth))) → Bool

The exact packed input of the batched lookup circuit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.Nonuniform.BatchLookup.layoutWiring {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth)) → DeMorgan.Wiring (requests * keyWidth)

The table and identifiers are constants; query addresses are input wires.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.layoutWiring_eval {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) (input : Fin (requests * keyWidth) → Bool) : (fun (bit : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth))) => DeMorgan.Wiring.eval input (layoutWiring table recordCount bit)) = layout table recordCount input

The wiring layer implements the packed layout exactly.

def Algebraic.MassProduction.Nonuniform.BatchLookup.outputIndex {keyWidth requests padding depth valueWidth : ℕ} (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) (output : Fin (requests * valueWidth)) : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth))

Select each result from its literal destination record.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.Nonuniform.BatchLookup.circuit {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) : Circuit DeMorgan.signature (requests * keyWidth) (requests * valueWidth)

Batched lookup using one hardwired table and two explicit sorting passes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.circuit_size {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) : (circuit table recordCount).size = ∑ output : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth (depth + 1 + valueWidth))), (layoutWiring table recordCount output).expression.gateCount + (Broadcast.routingCircuit depth keyWidth (depth + 1) valueWidth).size

The exact gate count of circuit.

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.circuit_eval {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) (input : Fin (requests * keyWidth) → Bool) (request : Fin requests) (bit : Fin valueWidth) : (circuit table recordCount).eval DeMorgan.interpretation input (finProdFinEquiv (request, bit)) = table (fun (addressBit : Fin keyWidth) => input (finProdFinEquiv (request, addressBit))) bit

Every query receives its table value, with arbitrary address repetition.

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.circuit_cost {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) : (circuit table recordCount).cost DeMorgan.standardCost = (Broadcast.routingCircuit depth keyWidth (depth + 1) valueWidth).cost DeMorgan.standardCost

Input preparation and output selection add no charged gates.

theorem Algebraic.MassProduction.Nonuniform.BatchLookup.circuit_cost_le {keyWidth valueWidth requests padding depth : ℕ} (table : (Fin keyWidth → Bool) → Fin valueWidth → Bool) (recordCount : 2 ^ keyWidth + requests + padding = Sorting.networkRecords depth) : (circuit table recordCount).cost DeMorgan.standardCost ≤ depth * depth * Sorting.networkRecords depth * (2 * RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth * (2 * ((keyWidth + 1) * (6 * (keyWidth + 1) + 4)) + 4)) + Sorting.networkRecords depth * (valueWidth * (6 * keyWidth + 4)) + (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth) + depth * depth * Sorting.networkRecords depth * (2 * RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth * (2 * ((depth + 2) * (6 * (depth + 2) + 4)) + 4)))

Explicit size bound for the complete batched table lookup circuit.