Fixed-width binary-reference lookup formulas -- definitions

A lookup formula interprets a little-endian formula word as an index into a finite family of one-bit source formulas. It disjoins one equality-guarded source per index. Out-of-range words select no source and therefore evaluate to false.

This construction is deliberately formula-level: clients may name primary input wires and already-emitted gate wires uniformly before compiling the result as the next appendable raw-circuit fragment.

def Complexity.CircuitCode.FixedWidth.LookupFormula.evaluatedWord {width : ℕ} (word : Fin width → BoolFormula) (assignment : ℕ → Bool) : BitString width

Evaluate a vector of bit formulas as one fixed-width word.

Equations

• Complexity.CircuitCode.FixedWidth.LookupFormula.evaluatedWord word assignment coordinate = Complexity.BoolFormula.eval assignment (word coordinate)

def Complexity.CircuitCode.FixedWidth.LookupFormula.wordEqual {width : ℕ} (word : Fin width → BoolFormula) (value : BitString width) : BoolFormula

Equality test between a formula word and one constant bit string.

Equations

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

def Complexity.CircuitCode.FixedWidth.LookupFormula.candidate {width count : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) (index : Fin count) : BoolFormula

Equality-guarded source formula for one candidate index.

Equations

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

def Complexity.CircuitCode.FixedWidth.LookupFormula.select {width count : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) : BoolFormula

Select the source named by a fixed-width binary formula word. Words whose unsigned value is outside count select no source and return false.

Equations

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

def Complexity.CircuitCode.FixedWidth.LookupFormula.selectSize (width count : ℕ) : ℕ

Exact tree size of select when every input bit and source is a one-node formula.

Equations

• Complexity.CircuitCode.FixedWidth.LookupFormula.selectSize width count = 1 + count * (30 * width + 6)