Fixed-width binary-reference lookup formulas #

This module exposes semantics, exact size, and support bounds for selecting a one-bit source with a fixed-width little-endian formula word.

@[simp]

BoolFormula.eval assignment (wordEqual word value) = decide (evaluatedWord word assignment = value)

A formula-word equality test agrees with extensional bit-string equality.

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.eval_select {width count : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) (assignment : ℕ → Bool) (hcount : count ≤ 2 ^ width) :

BoolFormula.eval assignment (select word values) = if hvalue : (evaluatedWord word assignment).unsignedValue < count then BoolFormula.eval assignment (values ⟨(evaluatedWord word assignment).unsignedValue, hvalue⟩) else false

Lookup returns the selected source exactly when the unsigned reference is in range, and false otherwise.

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.size_select {width count : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) (hword : ∀ (coordinate : Fin width), (word coordinate).size = 1) (hvalues : ∀ (index : Fin count), (values index).size = 1) :

(select word values).size = selectSize width count

Exact lookup-formula size for one-node word bits and sources.

theorem Complexity.CircuitCode.FixedWidth.LookupFormula.vars_select_lt {width count available : ℕ} (word : Fin width → BoolFormula) (values : Fin count → BoolFormula) (hword : ∀ (coordinate : Fin width), ∀ wire ∈ (word coordinate).vars, wire < available) (hvalues : ∀ (index : Fin count), ∀ wire ∈ (values index).vars, wire < available) (wire : ℕ) :

wire ∈ (select word values).vars → wire < available

Lookup support stays inside any prefix containing every word bit and source formula.

Documentation