Documentation

Complexitylib.Circuits.BinaryComparison

Little-endian binary comparison #

This module exposes unsigned semantics for fixed-width little-endian words, a linear-size Boolean formula comparing two consecutive input words, and its verified compilation to a typed fan-in-two circuit.

source
theorem Complexity.BitString.unsignedLE_eq_decide {width : ℕ} (left right : BitString width) :
left.unsignedLE right = decide (left.unsignedValue ≤ right.unsignedValue)

Recursive most-significant-bit comparison agrees with unsigned natural comparison.

source
@[simp]
theorem Complexity.BoolFormula.eval_ofBool (value : Bool) (assignment : ℕ → Bool) :
eval assignment (ofBool value) = value

Constant formula leaves evaluate to their embedded Boolean values.

source
theorem Complexity.BoolFormula.eval_unsignedLEOf {width : ℕ} (left right : Fin width → BoolFormula) (assignment : ℕ → Bool) :
eval assignment (unsignedLEOf left right) = BitString.unsignedLE (fun (i : Fin width) => eval assignment (left i)) fun (i : Fin width) => eval assignment (right i)

Comparing vectors of formulas compares their evaluated unsigned words.

source
theorem Complexity.BoolFormula.size_unsignedLEOf {width : ℕ} (left right : Fin width → BoolFormula) (hleft : ∀ (i : Fin width), (left i).size = 1) (hright : ∀ (i : Fin width), (right i).size = 1) :
(unsignedLEOf left right).size = 15 * width + 1

The generalized comparator retains the exact linear size when every operand bit is represented by one formula node.

source
@[simp]
theorem Complexity.BoolFormula.eval_unsignedLELeftConstant {width : ℕ} (left : BitString width) (rightBase : ℕ) (assignment : ℕ → Bool) :
eval assignment (unsignedLELeftConstant left rightBase) = decide (left.unsignedValue ≤ BitString.unsignedValue fun (i : Fin width) => assignment (rightBase + ↑i))

Constant-left comparison has the expected unsigned semantics.

source
@[simp]
theorem Complexity.BoolFormula.eval_unsignedLERightConstant {width : ℕ} (leftBase : ℕ) (right : BitString width) (assignment : ℕ → Bool) :
eval assignment (unsignedLERightConstant leftBase right) = decide ((BitString.unsignedValue fun (i : Fin width) => assignment (leftBase + ↑i)) ≤ right.unsignedValue)

Constant-right comparison has the expected unsigned semantics.

source
@[simp]
theorem Complexity.BoolFormula.size_unsignedLELeftConstant {width : ℕ} (left : BitString width) (rightBase : ℕ) :
(unsignedLELeftConstant left rightBase).size = 15 * width + 1

A constant-left comparator has exactly fifteen nodes per bit, plus its base constant.

source
@[simp]
theorem Complexity.BoolFormula.size_unsignedLERightConstant {width : ℕ} (leftBase : ℕ) (right : BitString width) :
(unsignedLERightConstant leftBase right).size = 15 * width + 1

A constant-right comparator has exactly fifteen nodes per bit, plus its base constant.

source
theorem Complexity.BoolFormula.vars_unsignedLELeftConstant_lt {width : ℕ} (left : BitString width) (rightBase available : ℕ) (hright : rightBase + width ≤ available) (j : ℕ) :
j ∈ (unsignedLELeftConstant left rightBase).vars → j < available

Every variable in a constant-left comparator lies in its right operand block.

source
theorem Complexity.BoolFormula.vars_unsignedLERightConstant_lt {width : ℕ} (leftBase : ℕ) (right : BitString width) (available : ℕ) (hleft : leftBase + width ≤ available) (j : ℕ) :
j ∈ (unsignedLERightConstant leftBase right).vars → j < available

Every variable in a constant-right comparator lies in its left operand block.

source
@[simp]
theorem Complexity.BoolFormula.size_unsignedLE (width : ℕ) :
(unsignedLE width).size = 15 * width + 1

The unsigned-comparison formula has exactly fifteen nodes per input bit, plus its base constant.

source
@[simp]
theorem Complexity.BoolFormula.eval_unsignedLE (width : ℕ) (left right : BitString width) :
eval (BitString.toTotal (Fin.append left right)) (unsignedLE width) = decide (left.unsignedValue ≤ right.unsignedValue)

The formula compares two consecutive fixed-width little-endian input words as unsigned naturals.

source
@[simp]
theorem Complexity.CircuitCode.length_unsignedLERawCircuit (width : ℕ) :
List.length (unsignedLERawCircuit width) = 15 * width + 1

Exact raw gate count for the unsigned-comparison construction.

source
theorem Complexity.CircuitCode.unsignedLERawCircuit_wellFormed (width : ℕ) [NeZero width] :
RawCircuit.WellFormed (width + width) (unsignedLERawCircuit width)

The raw unsigned-comparison construction is a valid single-output circuit for every positive word width.

source
noncomputable def Complexity.Circuit.unsignedLE (width : ℕ) [NeZero width] :
Circuit Basis.andOr2 (width + width) 1 (List.length (CircuitCode.unsignedLERawCircuit width) - 1)

Typed fan-in-two circuit comparing two consecutive width-bit unsigned little-endian words.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.Circuit.size_unsignedLE (width : ℕ) [NeZero width] :
    (unsignedLE width).size = 15 * width + 1

    Exact size of the typed unsigned-comparison circuit.

    source
    @[simp]
    theorem Complexity.Circuit.eval_unsignedLE (width : ℕ) [NeZero width] (left right : BitString width) :
    (unsignedLE width).eval (Fin.append left right) 0 = decide (left.unsignedValue ≤ right.unsignedValue)

    The typed circuit returns the unsigned comparison of its two input words.