Uhlig routing circuits

This module lifts Uhlig's two-request recovery invariant to Boolean functions on independent row-major inputs. It defines the finite semantic layer, explicitly routes each request suffix to its selected resources, and composes those routers with an externally supplied bank of shorter-function circuits.

def Algebraic.MassProduction.UhligCircuit.prefixLast (prefixWidth : ℕ) : ℕ

The final source index among the 2 ^ prefixWidth prefix assignments.

Equations

• Algebraic.MassProduction.UhligCircuit.prefixLast prefixWidth = 2 ^ prefixWidth - 1

theorem Algebraic.MassProduction.UhligCircuit.prefixCount_eq (prefixWidth : ℕ) : prefixLast prefixWidth + 1 = 2 ^ prefixWidth

def Algebraic.MassProduction.UhligCircuit.restriction {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (source : Fin (prefixLast prefixWidth + 1)) : ScalarFunction Bool suffixWidth

Restrict the first prefixWidth variables of a Boolean function to one canonical source value.

Equations

• Algebraic.MassProduction.UhligCircuit.restriction function source suffix = function (Algebraic.MassProduction.InputSplit.joinedInput (Fin.cast ⋯ source) suffix)

def Algebraic.MassProduction.UhligCircuit.resourceFunction {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (resource : Fin (prefixLast prefixWidth + 2)) : ScalarFunction Bool suffixWidth

Uhlig's resource functions, now viewed as functions of the unspecialized suffix variables.

Equations

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

def Algebraic.MassProduction.UhligCircuit.pairRequest {pairs : ℕ} (pair : Fin pairs) (side : Fin 2) : Fin (2 * pairs)

Pair-major enumeration of the 2 * pairs requests.

Equations

• Algebraic.MassProduction.UhligCircuit.pairRequest pair side = Fin.cast ⋯ (finProdFinEquiv (pair, side))

def Algebraic.MassProduction.UhligCircuit.requestBlock {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : Fin (prefixWidth + suffixWidth) → Bool

The full input block belonging to one side of one request pair.

Equations

• Algebraic.MassProduction.UhligCircuit.requestBlock input pair side = Algebraic.MassProduction.directProductInput input (Algebraic.MassProduction.UhligCircuit.pairRequest pair side)

def Algebraic.MassProduction.UhligCircuit.requestPrefix {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : Fin prefixWidth → Bool

The prefix bits of one request.

Equations

• Algebraic.MassProduction.UhligCircuit.requestPrefix input pair side bit = Algebraic.MassProduction.UhligCircuit.requestBlock input pair side (Fin.castAdd suffixWidth bit)

def Algebraic.MassProduction.UhligCircuit.requestSuffix {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : Fin suffixWidth → Bool

The suffix bits of one request.

Equations

• Algebraic.MassProduction.UhligCircuit.requestSuffix input pair side bit = Algebraic.MassProduction.UhligCircuit.requestBlock input pair side (Fin.natAdd prefixWidth bit)

def Algebraic.MassProduction.UhligCircuit.requestSource {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : Fin (prefixLast prefixWidth + 1)

Canonical numeric source selected by the request prefix.

Equations

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

def Algebraic.MassProduction.UhligCircuit.recoveryPair {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) : Finset (Fin (prefixLast prefixWidth + 2)) × Finset (Fin (prefixLast prefixWidth + 2))

The two disjoint resource sets assigned to one request pair.

Equations

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

def Algebraic.MassProduction.UhligCircuit.routedSuffix {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (resource : Fin (prefixLast prefixWidth + 2)) : Fin suffixWidth → Bool

Runtime suffix sent to one resource. Disjointness makes the first two branches mutually exclusive; an unused resource receives an arbitrary zero suffix.

Equations

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

def Algebraic.MassProduction.UhligCircuit.resourceValue {prefixWidth suffixWidth pairs : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (resource : Fin (prefixLast prefixWidth + 2)) : Bool

Value produced by one resource for one request pair.

Equations

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

def Algebraic.MassProduction.UhligCircuit.decodedValue {prefixWidth suffixWidth pairs : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : Bool

Decode one requested output by XORing its assigned resource values.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.joined_request_eq_requestBlock {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : InputSplit.joinedInput (Fin.cast ⋯ (requestSource input pair side)) (requestSuffix input pair side) = requestBlock input pair side

The runtime prefix and suffix really reassemble the selected input block.

theorem Algebraic.MassProduction.UhligCircuit.restriction_requestSource_requestSuffix {prefixWidth suffixWidth pairs : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : restriction function (requestSource input pair side) (requestSuffix input pair side) = function (requestBlock input pair side)

theorem Algebraic.MassProduction.UhligCircuit.routedSuffix_eq_left {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (resource : Fin (prefixLast prefixWidth + 2)) (member : resource ∈ (recoveryPair input pair).1) : routedSuffix input pair resource = requestSuffix input pair 0

theorem Algebraic.MassProduction.UhligCircuit.routedSuffix_eq_right {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (resource : Fin (prefixLast prefixWidth + 2)) (member : resource ∈ (recoveryPair input pair).2) : routedSuffix input pair resource = requestSuffix input pair 1

theorem Algebraic.MassProduction.UhligCircuit.decodedValue_eq {prefixWidth suffixWidth pairs : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : decodedValue function input pair side = function (requestBlock input pair side)

Exact correctness for one side of one pair.

theorem Algebraic.MassProduction.UhligCircuit.decodedValue_eq_directProduct {prefixWidth suffixWidth pairs : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) : (fun (output : Fin (2 * pairs)) => have pairSide := finProdFinEquiv.symm (Fin.cast ⋯ output); decodedValue function input pairSide.1 pairSide.2) = directProduct function (2 * pairs) input

Exact row-major finite Uhlig layer: decoding all pairs is the ordinary direct product of the original function.

Explicit routing expressions

def Algebraic.MassProduction.UhligCircuit.localInputIndex {prefixWidth suffixWidth : ℕ} (side : Fin 2) (coordinate : Fin (prefixWidth + suffixWidth)) : Fin (2 * (prefixWidth + suffixWidth))

Input coordinate in one two-request block.

Equations

• Algebraic.MassProduction.UhligCircuit.localInputIndex side coordinate = finProdFinEquiv (side, coordinate)

def Algebraic.MassProduction.UhligCircuit.localPrefix {prefixWidth suffixWidth : ℕ} (input : Fin (2 * (prefixWidth + suffixWidth)) → Bool) (side : Fin 2) : Fin prefixWidth → Bool

Prefix bits in one two-request block.

Equations

• Algebraic.MassProduction.UhligCircuit.localPrefix input side bit = input (Algebraic.MassProduction.UhligCircuit.localInputIndex side (Fin.castAdd suffixWidth bit))

def Algebraic.MassProduction.UhligCircuit.localSuffix {prefixWidth suffixWidth : ℕ} (input : Fin (2 * (prefixWidth + suffixWidth)) → Bool) (side : Fin 2) : Fin suffixWidth → Bool

Suffix bits in one two-request block.

Equations

• Algebraic.MassProduction.UhligCircuit.localSuffix input side bit = input (Algebraic.MassProduction.UhligCircuit.localInputIndex side (Fin.natAdd prefixWidth bit))

def Algebraic.MassProduction.UhligCircuit.localSource {prefixWidth suffixWidth : ℕ} (input : Fin (2 * (prefixWidth + suffixWidth)) → Bool) (side : Fin 2) : Fin (prefixLast prefixWidth + 1)

Numeric source represented by a local request prefix.

Equations

• Algebraic.MassProduction.UhligCircuit.localSource input side = Fin.cast ⋯ (Algebraic.MassProduction.RuntimePacking.source (Algebraic.MassProduction.UhligCircuit.localPrefix input side))

def Algebraic.MassProduction.UhligCircuit.sourceIndicatorExpression {prefixWidth suffixWidth : ℕ} (side : Fin 2) (source : Fin (prefixLast prefixWidth + 1)) : DeMorgan.Expression (2 * (prefixWidth + suffixWidth))

Indicator that one local request prefix equals a fixed source.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.sourceIndicatorExpression_eval_eq_true_iff {prefixWidth suffixWidth : ℕ} (side : Fin 2) (source : Fin (prefixLast prefixWidth + 1)) (input : Fin (2 * (prefixWidth + suffixWidth)) → Bool) : DeMorgan.Expression.eval input (sourceIndicatorExpression side source) = true ↔ localSource input side = source

def Algebraic.MassProduction.UhligCircuit.fixedRoutedSuffixExpression {prefixWidth suffixWidth : ℕ} (first second : Fin (prefixLast prefixWidth + 1)) (resource : Fin (prefixLast prefixWidth + 2)) (bit : Fin suffixWidth) : DeMorgan.Expression (2 * (prefixWidth + suffixWidth))

The fixed suffix input chosen for a resource after the two prefixes have been hardwired.

Equations

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

def Algebraic.MassProduction.UhligCircuit.routedSuffixExpression {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) (bit : Fin suffixWidth) : DeMorgan.Expression (2 * (prefixWidth + suffixWidth))

Runtime routing for one suffix bit, written as a one-hot selection over the two request prefixes.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.fixedRoutedSuffixExpression_eval {prefixWidth suffixWidth : ℕ} (first second : Fin (prefixLast prefixWidth + 1)) (resource : Fin (prefixLast prefixWidth + 2)) (bit : Fin suffixWidth) (input : Fin (2 * (prefixWidth + suffixWidth)) → Bool) : DeMorgan.Expression.eval input (fixedRoutedSuffixExpression first second resource bit) = if resource ∈ (uhligRecoveryPair first second).1 then localSuffix input 0 bit else if resource ∈ (uhligRecoveryPair first second).2 then localSuffix input 1 bit else false

theorem Algebraic.MassProduction.UhligCircuit.routedSuffixExpression_eval {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) (bit : Fin suffixWidth) (input : Fin (2 * (prefixWidth + suffixWidth)) → Bool) : DeMorgan.Expression.eval input (routedSuffixExpression resource bit) = if resource ∈ (uhligRecoveryPair (localSource input 0) (localSource input 1)).1 then localSuffix input 0 bit else if resource ∈ (uhligRecoveryPair (localSource input 0) (localSource input 1)).2 then localSuffix input 1 bit else false

noncomputable def Algebraic.MassProduction.UhligCircuit.resourceRouterCircuit {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) : Circuit DeMorgan.signature (2 * (prefixWidth + suffixWidth)) suffixWidth

Explicit circuit routing one pair's suffix to one Uhlig resource.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.resourceRouterCircuit_eval {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) (input : Fin (2 * (prefixWidth + suffixWidth)) → Bool) (bit : Fin suffixWidth) : (resourceRouterCircuit resource).eval DeMorgan.interpretation input bit = if resource ∈ (uhligRecoveryPair (localSource input 0) (localSource input 1)).1 then localSuffix input 0 bit else if resource ∈ (uhligRecoveryPair (localSource input 0) (localSource input 1)).2 then localSuffix input 1 bit else false

Batched routing and supplied resource circuits

def Algebraic.MassProduction.UhligCircuit.pairInputMap {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (input : Fin (2 * (prefixWidth + suffixWidth))) : Fin (2 * pairs * (prefixWidth + suffixWidth))

Embed one local two-request input into the corresponding global pair.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.pairInputMap_localInputIndex {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (coordinate : Fin (prefixWidth + suffixWidth)) : pairInputMap pair (localInputIndex side coordinate) = finProdFinEquiv (pairRequest pair side, coordinate)

theorem Algebraic.MassProduction.UhligCircuit.localPrefix_pairInputMap {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : localPrefix (input ∘ pairInputMap pair) side = requestPrefix input pair side

theorem Algebraic.MassProduction.UhligCircuit.localSuffix_pairInputMap {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : localSuffix (input ∘ pairInputMap pair) side = requestSuffix input pair side

theorem Algebraic.MassProduction.UhligCircuit.localSource_pairInputMap {pairs prefixWidth suffixWidth : ℕ} (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (side : Fin 2) : localSource (input ∘ pairInputMap pair) side = requestSource input pair side

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.resourceRouterGateCount (prefixWidth suffixWidth : ℕ) (resource : Fin (prefixLast prefixWidth + 2)) : ℕ

Charged/gate count of one resource router.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.resourceRouterCircuit_size {prefixWidth suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) : (resourceRouterCircuit resource).size = resourceRouterGateCount prefixWidth suffixWidth resource

noncomputable def Algebraic.MassProduction.UhligCircuit.resourceRouterArrayCircuit {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resource : Fin (prefixLast prefixWidth + 2)) : Circuit DeMorgan.signature (2 * pairs * (prefixWidth + suffixWidth)) (pairs * suffixWidth)

Route all request pairs to one shared resource circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.resourceRouterArrayCircuit_size {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resource : Fin (prefixLast prefixWidth + 2)) : (resourceRouterArrayCircuit pairs resource).size = ∑ _pair : Fin pairs, resourceRouterGateCount prefixWidth suffixWidth resource

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.resourceRouterArrayCircuit_eval {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resource : Fin (prefixLast prefixWidth + 2)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) (bit : Fin suffixWidth) : (resourceRouterArrayCircuit pairs resource).eval DeMorgan.interpretation input (finProdFinEquiv (pair, bit)) = routedSuffix input pair resource bit

noncomputable def Algebraic.MassProduction.UhligCircuit.routedResourceCircuit {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resource : Fin (prefixLast prefixWidth + 2)) (resourceCircuit : Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : Circuit DeMorgan.signature (2 * pairs * (prefixWidth + suffixWidth)) pairs

Compose one supplied pairs-copy resource circuit after its explicit Uhlig router.

Equations

• Algebraic.MassProduction.UhligCircuit.routedResourceCircuit pairs resource resourceCircuit = resourceCircuit.comp (Algebraic.MassProduction.UhligCircuit.resourceRouterArrayCircuit pairs resource)

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.routedResourceCircuit_size {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resource : Fin (prefixLast prefixWidth + 2)) (resourceCircuit : Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (routedResourceCircuit pairs resource resourceCircuit).size = ∑ _pair : Fin pairs, resourceRouterGateCount prefixWidth suffixWidth resource + resourceCircuit.size

theorem Algebraic.MassProduction.UhligCircuit.routedResourceCircuit_eval {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (pairs : ℕ) (resource : Fin (prefixLast prefixWidth + 2)) (resourceCircuit : Circuit DeMorgan.signature (pairs * suffixWidth) pairs) (computes : resourceCircuit.ComputesWith DeMorgan.interpretation (directProduct (resourceFunction function resource) pairs)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (pair : Fin pairs) : (routedResourceCircuit pairs resource resourceCircuit).eval DeMorgan.interpretation input pair = resourceValue function input pair resource

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.routedResourceGateCount (prefixWidth suffixWidth pairs : ℕ) (resourceGateCounts : Fin (prefixLast prefixWidth + 2) → ℕ) (resource : Fin (prefixLast prefixWidth + 2)) : ℕ

Gate count of one routed supplied resource circuit.

Equations

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

noncomputable def Algebraic.MassProduction.UhligCircuit.resourceBankCircuit {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : Circuit DeMorgan.signature (2 * pairs * (prefixWidth + suffixWidth)) ((prefixLast prefixWidth + 2) * pairs)

All Uhlig resources evaluated in parallel, in (resource, pair) order.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.resourceBankCircuit_size {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (resourceBankCircuit pairs resourceCircuits).size = ∑ resource : Fin (prefixLast prefixWidth + 2), routedResourceGateCount prefixWidth suffixWidth pairs (fun (resource : Fin (prefixLast prefixWidth + 2)) => (resourceCircuits resource).size) resource

theorem Algebraic.MassProduction.UhligCircuit.resourceBankCircuit_eval {prefixWidth suffixWidth : ℕ} (function : ScalarFunction Bool (prefixWidth + suffixWidth)) (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) (computes : ∀ (resource : Fin (prefixLast prefixWidth + 2)), (resourceCircuits resource).ComputesWith DeMorgan.interpretation (directProduct (resourceFunction function resource) pairs)) (input : Fin (2 * pairs * (prefixWidth + suffixWidth)) → Bool) (resource : Fin (prefixLast prefixWidth + 2)) (pair : Fin pairs) : (resourceBankCircuit pairs resourceCircuits).eval DeMorgan.interpretation input (finProdFinEquiv (resource, pair)) = resourceValue function input pair resource

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.resourceBankCircuit_cost {prefixWidth suffixWidth : ℕ} (pairs : ℕ) (resourceCircuits : Fin (prefixLast prefixWidth + 2) → Circuit DeMorgan.signature (pairs * suffixWidth) pairs) : (resourceBankCircuit pairs resourceCircuits).cost DeMorgan.standardCost = ∑ resource : Fin (prefixLast prefixWidth + 2), (∑ _pair : Fin pairs, (resourceRouterCircuit resource).cost DeMorgan.standardCost + (resourceCircuits resource).cost DeMorgan.standardCost)