A shared batched OR circuit

Source keys, source flags, and query keys are supplied by input wires or constants. One source array serves every query, including repeated queries. The output is in query order and missing keys return false.

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

Query identifiers fit in the sorting depth.

noncomputable def Algebraic.MassProduction.Nonuniform.BatchOr.layoutWiring {sources keyWidth inputs valueWidth requests padding depth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceValues : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (queryKeys : Fin requests → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + requests + padding = Sorting.networkRecords depth) : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth)) → DeMorgan.Wiring inputs

Prepare dynamic source records and queries with fixed ordering metadata.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BatchOr.layoutWiring_eval {sources keyWidth inputs valueWidth requests padding depth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceValues : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (queryKeys : Fin requests → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + requests + padding = Sorting.networkRecords depth) (input : Fin inputs → Bool) : (fun (bit : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth (depth + 1) valueWidth))) => DeMorgan.Wiring.eval input (layoutWiring sourceKeys sourceValues queryKeys recordCount bit)) = Routing.routingInputBits (fun (source : Fin sources) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source bit)) (fun (source : Fin sources) => Fin.append (fun (x : Fin (depth + 1)) => false) fun (bit : Fin valueWidth) => DeMorgan.Wiring.eval input (sourceValues source bit)) (fun (request : Fin requests) (bit : Fin keyWidth) => DeMorgan.Wiring.eval input (queryKeys request bit)) (fun (request : Fin requests) => Fin.append (CanonicalMetadataRouting.destinationOrderMetadata ⋯ request) fun (x : Fin valueWidth) => false) (fun (x : Fin padding) (x_1 : Fin keyWidth) => false) (fun (x : Fin padding) => Fin.append (paddingRoutingKey fun (x : Fin depth) => false) fun (x : Fin valueWidth) => false) recordCount

The prepared bits are exactly the concrete routing layout.

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

Fixed output wires extract all query values in their original order.

Equations

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

noncomputable def Algebraic.MassProduction.Nonuniform.BatchOr.circuit {sources keyWidth inputs valueWidth requests padding depth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceValues : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (queryKeys : Fin requests → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + requests + padding = Sorting.networkRecords depth) : Circuit DeMorgan.signature inputs (requests * valueWidth)

Two sorts and a shared propagation scan compute the complete batched OR.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.BatchOr.circuit_size {sources keyWidth inputs valueWidth requests padding depth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceValues : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (queryKeys : Fin requests → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + requests + padding = Sorting.networkRecords depth) : (circuit sourceKeys sourceValues queryKeys recordCount).size = ∑ output : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth (depth + 1 + valueWidth))), (layoutWiring sourceKeys sourceValues queryKeys recordCount output).expression.gateCount + (Broadcast.routingCircuit depth keyWidth (depth + 1) valueWidth).size

The exact gate count of circuit.

theorem Algebraic.MassProduction.Nonuniform.BatchOr.circuit_eval_iff {sources keyWidth inputs valueWidth requests padding depth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceValues : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (queryKeys : Fin requests → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + requests + padding = Sorting.networkRecords depth) (input : Fin inputs → Bool) (request : Fin requests) (bit : Fin valueWidth) : (circuit sourceKeys sourceValues queryKeys recordCount).eval DeMorgan.interpretation input (finProdFinEquiv (request, bit)) = true ↔ ∃ (source : Fin sources), ((fun (keyBit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source keyBit)) = fun (keyBit : Fin keyWidth) => DeMorgan.Wiring.eval input (queryKeys request keyBit)) ∧ DeMorgan.Wiring.eval input (sourceValues source bit) = true

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

theorem Algebraic.MassProduction.Nonuniform.BatchOr.circuit_cost_le {sources keyWidth inputs valueWidth requests padding depth : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceValues : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (queryKeys : Fin requests → Fin keyWidth → DeMorgan.Wiring inputs) (recordCount : sources + requests + padding = Sorting.networkRecords depth) : (circuit sourceKeys sourceValues queryKeys recordCount).cost DeMorgan.standardCost ≤ 128 * Sorting.networkRecords depth * (depth + keyWidth + valueWidth + 2) ^ 5

A linear record-count bound with a fixed width/depth polynomial.

theorem Algebraic.MassProduction.Nonuniform.BatchOr.existsCircuit {sources keyWidth inputs valueWidth requests : ℕ} (sourceKeys : Fin sources → Fin keyWidth → DeMorgan.Wiring inputs) (sourceValues : Fin sources → Fin valueWidth → DeMorgan.Wiring inputs) (queryKeys : Fin requests → Fin keyWidth → DeMorgan.Wiring inputs) : ∃ (routed : Circuit DeMorgan.signature inputs (requests * valueWidth)), (∀ (input : Fin inputs → Bool) (request : Fin requests) (bit : Fin valueWidth), routed.eval DeMorgan.interpretation input (finProdFinEquiv (request, bit)) = true ↔ ∃ (source : Fin sources), ((fun (keyBit : Fin keyWidth) => DeMorgan.Wiring.eval input (sourceKeys source keyBit)) = fun (keyBit : Fin keyWidth) => DeMorgan.Wiring.eval input (queryKeys request keyBit)) ∧ DeMorgan.Wiring.eval input (sourceValues source bit) = true) ∧ routed.cost DeMorgan.standardCost ≤ 256 * (sources + requests + 1) * (FiniteParameters.binaryDepth (sources + requests + 1) + keyWidth + valueWidth + 2) ^ 5

Canonical padding gives a circuit of size linear in sources plus queries. The extra one in the bound covers the empty batch as well.