Fixed-width encoded-gate evaluation formulas -- definitions

This module defines the formula-level step used to evaluate one gate slot in a fixed-width circuit description. Its two binary references select primary inputs or already-computed gate values, its negation bits conditionally flip those values, and its operation bit selects AND or OR.

The source formulas are abstract. A later sequential construction instantiates them with primary-input wires and output wires of earlier gate-step fragments.

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.codeOfAssignment (inputWidth gateBound : ℕ) (assignment : ℕ → Bool) : BitString (codeWidth inputWidth gateBound)

Restrict an unbounded assignment to the encoded-description prefix.

Equations

• Complexity.CircuitCode.FixedWidth.Description.GateFormula.codeOfAssignment inputWidth gateBound assignment coordinate = assignment ↑coordinate

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.decodedSlot (inputWidth gateBound : ℕ) (slot : Fin gateBound) (assignment : ℕ → Bool) : GateSlot (referenceWidth inputWidth gateBound)

Decode one gate slot from the description prefix of an assignment.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.operationBit (inputWidth gateBound : ℕ) (slot : Fin gateBound) : BoolFormula

Formula for the operation bit of one encoded gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.negated0Bit (inputWidth gateBound : ℕ) (slot : Fin gateBound) : BoolFormula

Formula for the first negation bit of one encoded gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.negated1Bit (inputWidth gateBound : ℕ) (slot : Fin gateBound) : BoolFormula

Formula for the second negation bit of one encoded gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.negateIf (flag value : BoolFormula) : BoolFormula

Conditionally negate a formula value according to a Boolean flag formula.

Equations

• Complexity.CircuitCode.FixedWidth.Description.GateFormula.negateIf flag value = (flag.disj value).conj (flag.conj value).neg

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.applyOperation (operation left right : BoolFormula) : BoolFormula

Apply the encoded operation convention: true selects AND and false OR.

Equations

• Complexity.CircuitCode.FixedWidth.Description.GateFormula.applyOperation operation left right = (left.conj right).disj (operation.neg.conj (left.disj right))

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.selected0 (inputWidth gateBound : ℕ) (slot : Fin gateBound) (sources : Fin (inputWidth + ↑slot) → BoolFormula) : BoolFormula

Select the first referenced source value for one gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.selected1 (inputWidth gateBound : ℕ) (slot : Fin gateBound) (sources : Fin (inputWidth + ↑slot) → BoolFormula) : BoolFormula

Select the second referenced source value for one gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.gate (inputWidth gateBound : ℕ) (slot : Fin gateBound) (sources : Fin (inputWidth + ↑slot) → BoolFormula) : BoolFormula

Evaluate one encoded gate from an abstract family of available sources.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.GateFormula.gateSize (inputWidth gateBound : ℕ) (slot : Fin gateBound) : ℕ

Exact tree size of one encoded-gate formula when every source is a one-node variable formula.

Equations

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