Uhlig decoder circuits

This module specifies the XOR decoder over one completed routing/resource state and implements it with shared linear-size Boolean folds. The final theorems identify the decoder's output with the semantic value selected by each request pair and give its exact gate cost.

Generic expression compatibility names

@[reducible, inline]

abbrev Algebraic.MassProduction.UhligCircuit.reindexExpression {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) (expression : DeMorgan.Expression sourceInputs) : DeMorgan.Expression targetInputs

Compatibility name for generic De Morgan expression input mapping.

Equations

• Algebraic.MassProduction.UhligCircuit.reindexExpression inputMap expression = Algebraic.DeMorgan.Expression.mapInputs inputMap expression

theorem Algebraic.MassProduction.UhligCircuit.reindexExpression_eval {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) (expression : DeMorgan.Expression sourceInputs) (input : Fin targetInputs → Bool) : DeMorgan.Expression.eval input (reindexExpression inputMap expression) = DeMorgan.Expression.eval (input ∘ inputMap) expression

theorem Algebraic.MassProduction.UhligCircuit.reindexExpression_gateCount {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) (expression : DeMorgan.Expression sourceInputs) : (reindexExpression inputMap expression).gateCount = expression.gateCount

theorem Algebraic.MassProduction.UhligCircuit.reindexExpression_standardCost {sourceInputs targetInputs : ℕ} (inputMap : Fin sourceInputs → Fin targetInputs) (expression : DeMorgan.Expression sourceInputs) : (reindexExpression inputMap expression).standardCost = expression.standardCost

@[reducible, inline]

abbrev Algebraic.MassProduction.UhligCircuit.xorExpression {inputs : ℕ} (left right : DeMorgan.Expression inputs) : DeMorgan.Expression inputs

Compatibility name for the generic De Morgan XOR expression.

Equations

• Algebraic.MassProduction.UhligCircuit.xorExpression left right = left.xor right

theorem Algebraic.MassProduction.UhligCircuit.xorExpression_eval {inputs : ℕ} (left right : DeMorgan.Expression inputs) (input : Fin inputs → Bool) : DeMorgan.Expression.eval input (xorExpression left right) = DeMorgan.Expression.eval input left + DeMorgan.Expression.eval input right

@[reducible, inline]

abbrev Algebraic.MassProduction.UhligCircuit.finXor {inputs : ℕ} (count : ℕ) (terms : Fin count → DeMorgan.Expression inputs) : DeMorgan.Expression inputs

Compatibility name for the generic finite XOR expression fold.

Equations

• Algebraic.MassProduction.UhligCircuit.finXor count terms = Algebraic.DeMorgan.Expression.finXor count terms

theorem Algebraic.MassProduction.UhligCircuit.finXor_eval {inputs : ℕ} (count : ℕ) (terms : Fin count → DeMorgan.Expression inputs) (input : Fin inputs → Bool) : DeMorgan.Expression.eval input (finXor count terms) = ∑ index : Fin count, DeMorgan.Expression.eval input (terms index)

@[reducible]

def Algebraic.MassProduction.UhligCircuit.layerInputCount (prefixWidth suffixWidth pairs : ℕ) : ℕ

Number of original input wires in one batched Uhlig layer.

Equations

• Algebraic.MassProduction.UhligCircuit.layerInputCount prefixWidth suffixWidth pairs = 2 * pairs * (prefixWidth + suffixWidth)

@[reducible]

def Algebraic.MassProduction.UhligCircuit.layerResourceOutputCount (prefixWidth pairs : ℕ) : ℕ

Number of resource-result wires in one batched Uhlig layer.

Equations

• Algebraic.MassProduction.UhligCircuit.layerResourceOutputCount prefixWidth pairs = (Algebraic.MassProduction.UhligCircuit.prefixLast prefixWidth + 2) * pairs

@[reducible]

def Algebraic.MassProduction.UhligCircuit.layerStateCount (prefixWidth suffixWidth pairs : ℕ) : ℕ

Original inputs followed by every (resource, pair) result.

Equations

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

def Algebraic.MassProduction.UhligCircuit.originalInputFromState {prefixWidth suffixWidth pairs : ℕ} (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : Fin (layerInputCount prefixWidth suffixWidth pairs) → Bool

Read the original-input prefix of a layer state.

Equations

• Algebraic.MassProduction.UhligCircuit.originalInputFromState state input = state (Fin.castAdd (Algebraic.MassProduction.UhligCircuit.layerResourceOutputCount prefixWidth pairs) input)

def Algebraic.MassProduction.UhligCircuit.resourceStateIndex {prefixWidth pairs suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) (pair : Fin pairs) : Fin (layerStateCount prefixWidth suffixWidth pairs)

State wire carrying one resource result.

Equations

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

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

Embed one local pair input into the original-input prefix of a layer state.

Equations

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

def Algebraic.MassProduction.UhligCircuit.stateSourceIndicatorExpression {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (source : Fin (prefixLast prefixWidth + 1)) : DeMorgan.Expression (layerStateCount prefixWidth suffixWidth pairs)

Prefix equality test for one request inside a layer state.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.stateSourceIndicatorExpression_eval_eq_true_iff {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (source : Fin (prefixLast prefixWidth + 1)) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : DeMorgan.Expression.eval state (stateSourceIndicatorExpression pair side source) = true ↔ requestSource (originalInputFromState state) pair side = source

def Algebraic.MassProduction.UhligCircuit.resourceValueExpression {prefixWidth pairs suffixWidth : ℕ} (resource : Fin (prefixLast prefixWidth + 2)) (pair : Fin pairs) : DeMorgan.Expression (layerStateCount prefixWidth suffixWidth pairs)

Resource-result input expression for the decoder.

Equations

• Algebraic.MassProduction.UhligCircuit.resourceValueExpression resource pair = Algebraic.DeMorgan.Expression.input (Algebraic.MassProduction.UhligCircuit.resourceStateIndex resource pair)

def Algebraic.MassProduction.UhligCircuit.fixedResourceTermExpression {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) (resource : Fin (prefixLast prefixWidth + 2)) : DeMorgan.Expression (layerStateCount prefixWidth suffixWidth pairs)

One fixed decoder term: either the selected resource-result wire or the free false constant.

Equations

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

def Algebraic.MassProduction.UhligCircuit.fixedDecodedExpression {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : DeMorgan.Expression (layerStateCount prefixWidth suffixWidth pairs)

XOR decoder for fixed prefix values.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.fixedDecodedExpression_eval {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : DeMorgan.Expression.eval state (fixedDecodedExpression pair side first second) = have resources := Fin.cases (uhligRecoveryPair first second).1 (fun (x : Fin 1) => (uhligRecoveryPair first second).2) side; ∑ resource ∈ resources, state (resourceStateIndex resource pair)

def Algebraic.MassProduction.UhligCircuit.decodedExpression {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) : DeMorgan.Expression (layerStateCount prefixWidth suffixWidth pairs)

Runtime decoder selected by the two actual request prefixes.

Equations

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

def Algebraic.MassProduction.UhligCircuit.decodedStateValue {prefixWidth suffixWidth pairs : ℕ} (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) (pair : Fin pairs) (side : Fin 2) : Bool

Semantic decoder on a completed layer state.

Equations

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

theorem Algebraic.MassProduction.UhligCircuit.decodedExpression_eval {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : DeMorgan.Expression.eval state (decodedExpression pair side) = decodedStateValue state pair side

Decoder circuit

def Algebraic.MassProduction.UhligCircuit.decoderPairSide {pairs : ℕ} (output : Fin (2 * pairs)) : Fin pairs × Fin 2

Recover the pair and side represented by a row-major direct-product output.

Equations

• Algebraic.MassProduction.UhligCircuit.decoderPairSide output = finProdFinEquiv.symm (Fin.cast ⋯ output)

def Algebraic.MassProduction.UhligCircuit.decoderOutputExpression {pairs prefixWidth suffixWidth : ℕ} (output : Fin (2 * pairs)) : DeMorgan.Expression (layerStateCount prefixWidth suffixWidth pairs)

Decoder expression attached to one row-major output.

Equations

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

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.decoderGateCount (prefixWidth suffixWidth pairs : ℕ) (output : Fin (2 * pairs)) : ℕ

Gate count of one compiled decoder output.

Equations

• Algebraic.MassProduction.UhligCircuit.decoderGateCount prefixWidth suffixWidth pairs output = (Algebraic.MassProduction.UhligCircuit.decoderOutputExpression output).gateCount

noncomputable def Algebraic.MassProduction.UhligCircuit.decoderCircuit (prefixWidth suffixWidth pairs : ℕ) : Circuit DeMorgan.signature (layerStateCount prefixWidth suffixWidth pairs) (2 * pairs)

All requested outputs decoded in ordinary row-major order.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.decoderCircuit_size (prefixWidth suffixWidth pairs : ℕ) : (decoderCircuit prefixWidth suffixWidth pairs).size = ∑ output : Fin (2 * pairs), decoderGateCount prefixWidth suffixWidth pairs output

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.decoderCircuit_eval {prefixWidth suffixWidth pairs : ℕ} (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) (output : Fin (2 * pairs)) : (decoderCircuit prefixWidth suffixWidth pairs).eval DeMorgan.interpretation state output = have pairSide := decoderPairSide output; decodedStateValue state pairSide.1 pairSide.2

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.decoderCircuit_cost (prefixWidth suffixWidth pairs : ℕ) : (decoderCircuit prefixWidth suffixWidth pairs).cost DeMorgan.standardCost = ∑ output : Fin (2 * pairs), (decoderOutputExpression output).standardCost

Shared linear-size Boolean folds

def Algebraic.MassProduction.UhligCircuit.xorInputExpression (count : ℕ) : Arithmetic.Expression Bool count

Arithmetic XOR of all input wires. Compiling the arithmetic addition gate preserves sharing, so this avoids the duplication inherent in a De Morgan formula for XOR.

Equations

• Algebraic.MassProduction.UhligCircuit.xorInputExpression count = Algebraic.DeMorgan.ArithmeticExpression.finSum count fun (input : Fin count) => Algebraic.Arithmetic.Expression.input input

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.xorInputGateCount (count : ℕ) : ℕ

Program-gate count of the shared XOR fold.

Equations

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

noncomputable def Algebraic.MassProduction.UhligCircuit.xorInputCircuit (count : ℕ) : Circuit DeMorgan.signature count 1

De Morgan circuit obtained by compiling the shared arithmetic XOR fold.

Equations

• Algebraic.MassProduction.UhligCircuit.xorInputCircuit count = Algebraic.DeMorgan.ArithmeticExpression.circuit (Algebraic.MassProduction.UhligCircuit.xorInputExpression count)

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.xorInputCircuit_size (count : ℕ) : (xorInputCircuit count).size = xorInputGateCount count

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.xorInputCircuit_eval (count : ℕ) (input : Fin count → Bool) : (xorInputCircuit count).eval DeMorgan.interpretation input 0 = Finset.univ.sum input

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.xorInputCircuit_cost (count : ℕ) : (xorInputCircuit count).cost DeMorgan.standardCost = count * 4

def Algebraic.MassProduction.UhligCircuit.orInputExpression (count : ℕ) : DeMorgan.Expression count

OR of all input wires.

Equations

• Algebraic.MassProduction.UhligCircuit.orInputExpression count = Algebraic.DeMorgan.Expression.finOr count fun (input : Fin count) => Algebraic.DeMorgan.Expression.input input

@[reducible]

def Algebraic.MassProduction.UhligCircuit.orInputGateCount (count : ℕ) : ℕ

Program-gate count of the shared OR fold.

Equations

• Algebraic.MassProduction.UhligCircuit.orInputGateCount count = (Algebraic.MassProduction.UhligCircuit.orInputExpression count).gateCount

def Algebraic.MassProduction.UhligCircuit.orInputCircuit (count : ℕ) : Circuit DeMorgan.signature count 1

De Morgan circuit implementing the shared OR fold.

Equations

• Algebraic.MassProduction.UhligCircuit.orInputCircuit count = (Algebraic.MassProduction.UhligCircuit.orInputExpression count).circuit

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.orInputCircuit_size (count : ℕ) : (orInputCircuit count).size = orInputGateCount count

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.orInputCircuit_eval (count : ℕ) (input : Fin count → Bool) : (orInputCircuit count).eval DeMorgan.interpretation input 0 = DeMorgan.Expression.finOrValue count input

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.orInputCircuit_cost (count : ℕ) : (orInputCircuit count).cost DeMorgan.standardCost = count

noncomputable def Algebraic.MassProduction.UhligCircuit.fixedResourceVectorCircuit {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : Circuit DeMorgan.signature (layerStateCount prefixWidth suffixWidth pairs) (prefixLast prefixWidth + 2)

Produce all fixed-prefix resource terms before their shared XOR fold.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.fixedResourceVectorCircuit_size {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : (fixedResourceVectorCircuit pair side first second).size = ∑ resource : Fin (prefixLast prefixWidth + 2), (fixedResourceTermExpression pair side first second resource).gateCount

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.fixedResourceVectorCircuit_eval {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) (resource : Fin (prefixLast prefixWidth + 2)) : (fixedResourceVectorCircuit pair side first second).eval DeMorgan.interpretation state resource = DeMorgan.Expression.eval state (fixedResourceTermExpression pair side first second resource)

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.fixedResourceVectorCircuit_cost {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : (fixedResourceVectorCircuit pair side first second).cost DeMorgan.standardCost = 0

noncomputable def Algebraic.MassProduction.UhligCircuit.sharedFixedDecodedCircuit {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : Circuit DeMorgan.signature (layerStateCount prefixWidth suffixWidth pairs) 1

Fixed-prefix decoder with a circuit-level shared XOR fold.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedFixedDecodedCircuit_size {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : (sharedFixedDecodedCircuit pair side first second).size = ∑ resource : Fin (prefixLast prefixWidth + 2), (fixedResourceTermExpression pair side first second resource).gateCount + xorInputGateCount (prefixLast prefixWidth + 2)

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedFixedDecodedCircuit_eval {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : (sharedFixedDecodedCircuit pair side first second).eval DeMorgan.interpretation state 0 = have resources := Fin.cases (uhligRecoveryPair first second).1 (fun (x : Fin 1) => (uhligRecoveryPair first second).2) side; ∑ resource ∈ resources, state (resourceStateIndex resource pair)

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedFixedDecodedCircuit_cost {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : (sharedFixedDecodedCircuit pair side first second).cost DeMorgan.standardCost = 4 * (prefixLast prefixWidth + 2)

def Algebraic.MassProduction.UhligCircuit.candidatePostprocessExpression : DeMorgan.Expression 3

Three-input postprocessor for one candidate prefix pair. The second source indicator is outermost so the row decoder has one-hot form.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.candidatePostprocessExpression_eval (input : Fin 3 → Bool) : DeMorgan.Expression.eval input candidatePostprocessExpression = (input 1 && (input 0 && input 2))

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.candidateDecodedGateCount (prefixWidth suffixWidth pairs : ℕ) (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : ℕ

Program-gate count of one fully specified decoder candidate.

Equations

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

noncomputable def Algebraic.MassProduction.UhligCircuit.candidateDecodedCircuit {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : Circuit DeMorgan.signature (layerStateCount prefixWidth suffixWidth pairs) 1

Circuit for one hardwired pair of possible request prefixes.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.candidateDecodedCircuit_size {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) : (candidateDecodedCircuit pair side first second).size = candidateDecodedGateCount prefixWidth suffixWidth pairs pair side first second

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.candidateDecodedCircuit_eval {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first second : Fin (prefixLast prefixWidth + 1)) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : (candidateDecodedCircuit pair side first second).eval DeMorgan.interpretation state 0 = (DeMorgan.Expression.eval state (stateSourceIndicatorExpression pair 1 second) && (DeMorgan.Expression.eval state (stateSourceIndicatorExpression pair 0 first) && (sharedFixedDecodedCircuit pair side first second).eval DeMorgan.interpretation state 0))

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.candidateRowGateCount (prefixWidth suffixWidth pairs : ℕ) (pair : Fin pairs) (side : Fin 2) (first : Fin (prefixLast prefixWidth + 1)) : ℕ

Program-gate count of one row of decoder candidates.

Equations

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

noncomputable def Algebraic.MassProduction.UhligCircuit.candidateRowCircuit {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first : Fin (prefixLast prefixWidth + 1)) : Circuit DeMorgan.signature (layerStateCount prefixWidth suffixWidth pairs) 1

OR all candidates for the second request prefix while retaining one fixed candidate for the first prefix.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.candidateRowCircuit_size {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first : Fin (prefixLast prefixWidth + 1)) : (candidateRowCircuit pair side first).size = candidateRowGateCount prefixWidth suffixWidth pairs pair side first

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.candidateRowCircuit_eval {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (first : Fin (prefixLast prefixWidth + 1)) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : (candidateRowCircuit pair side first).eval DeMorgan.interpretation state 0 = (DeMorgan.Expression.eval state (stateSourceIndicatorExpression pair 0 first) && (sharedFixedDecodedCircuit pair side first (requestSource (originalInputFromState state) pair 1)).eval DeMorgan.interpretation state 0)

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.sharedDecodedGateCount (prefixWidth suffixWidth pairs : ℕ) (pair : Fin pairs) (side : Fin 2) : ℕ

Program-gate count of one complete shared output decoder.

Equations

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

noncomputable def Algebraic.MassProduction.UhligCircuit.sharedDecodedCircuit {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) : Circuit DeMorgan.signature (layerStateCount prefixWidth suffixWidth pairs) 1

Shared decoder for one requested output.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedDecodedCircuit_size {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) : (sharedDecodedCircuit pair side).size = sharedDecodedGateCount prefixWidth suffixWidth pairs pair side

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedDecodedCircuit_eval {pairs prefixWidth suffixWidth : ℕ} (pair : Fin pairs) (side : Fin 2) (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) : (sharedDecodedCircuit pair side).eval DeMorgan.interpretation state 0 = decodedStateValue state pair side

@[reducible]

noncomputable def Algebraic.MassProduction.UhligCircuit.sharedDecoderOutputGateCount (prefixWidth suffixWidth pairs : ℕ) (output : Fin (2 * pairs)) : ℕ

Gate count of the shared decoder attached to one row-major output.

Equations

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

noncomputable def Algebraic.MassProduction.UhligCircuit.sharedDecoderCircuit (prefixWidth suffixWidth pairs : ℕ) : Circuit DeMorgan.signature (layerStateCount prefixWidth suffixWidth pairs) (2 * pairs)

Shared decoders for all row-major outputs.

Equations

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

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedDecoderCircuit_size (prefixWidth suffixWidth pairs : ℕ) : (sharedDecoderCircuit prefixWidth suffixWidth pairs).size = ∑ output : Fin (2 * pairs), sharedDecoderOutputGateCount prefixWidth suffixWidth pairs output

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedDecoderCircuit_eval {prefixWidth suffixWidth pairs : ℕ} (state : Fin (layerStateCount prefixWidth suffixWidth pairs) → Bool) (output : Fin (2 * pairs)) : (sharedDecoderCircuit prefixWidth suffixWidth pairs).eval DeMorgan.interpretation state output = have pairSide := decoderPairSide output; decodedStateValue state pairSide.1 pairSide.2

@[simp]

theorem Algebraic.MassProduction.UhligCircuit.sharedDecoderCircuit_cost (prefixWidth suffixWidth pairs : ℕ) : (sharedDecoderCircuit prefixWidth suffixWidth pairs).cost DeMorgan.standardCost = ∑ output : Fin (2 * pairs), have pairSide := decoderPairSide output; (sharedDecodedCircuit pairSide.1 pairSide.2).cost DeMorgan.standardCost