Batched lookup in the concrete routing layout #
Only source keys must be injective. Repeated queries and padding records with active keys are allowed: their preserved metadata distinguishes them when the output order is restored.
theorem
Algebraic.MassProduction.Nonuniform.Broadcast.routingCircuit_layoutValue
{destinationCount orderWidth sourceCount keyWidth valueWidth paddingCount depth : ℕ}
(destinationFits : destinationCount ≤ 2 ^ orderWidth)
(sourceKeys : Fin sourceCount → Fin keyWidth → Bool)
(sourceMetadata : Fin sourceCount → Fin (orderWidth + 1) → Bool)
(sourceValues : Fin sourceCount → Fin valueWidth → Bool)
(destinationKeys : Fin destinationCount → Fin keyWidth → Bool)
(destinationValues : Fin destinationCount → Fin valueWidth → Bool)
(paddingKeys : Fin paddingCount → Fin keyWidth → Bool)
(paddingTails : Fin paddingCount → Fin orderWidth → Bool)
(paddingValues : Fin paddingCount → Fin valueWidth → Bool)
(sourceKeysInjective : Function.Injective sourceKeys)
(sourceFor : Fin destinationCount → Fin sourceCount)
(matchingKey : ∀ (destination : Fin destinationCount), sourceKeys (sourceFor destination) = destinationKeys destination)
(recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth)
(target : Fin destinationCount)
:
have input :=
Routing.routingInputBits sourceKeys
(fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys
(fun (destination : Fin destinationCount) =>
Fin.append (CanonicalMetadataRouting.destinationOrderMetadata destinationFits destination)
(destinationValues destination))
paddingKeys
(fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding))
recordCount;
RoutingMetadata.recordValue
((routingCircuit depth keyWidth (orderWidth + 1) valueWidth).eval DeMorgan.interpretation input)
(Fin.castLE ⋯ target) = sourceValues (sourceFor target)
The existing packed layout supports repeated lookup requests through the shared broadcast circuit, without any uniqueness premise on query keys.