Unsigned binary minimum -- definitions

The construction emits the comparator bit beside an unchanged copy of both input words, then feeds that tuple to the fixed-width multiplexer.

def Complexity.BitString.unsignedMin {width : ℕ} (left right : BitString width) : BitString width

Select the word of smaller unsigned value, choosing the left word on ties.

Equations

• left.unsignedMin right = if left.unsignedValue ≤ right.unsignedValue then left else right

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

Comparator output followed by an unchanged copy of its two input words.

Equations

• Complexity.Circuit.unsignedLEWithPayload width = (Complexity.Circuit.unsignedLE width).parallel (Complexity.Circuit.projectInputs fun (input : Fin (width + width)) => input)

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

Fan-in-two circuit selecting the unsigned minimum of two consecutive words.

Equations

• Complexity.Circuit.unsignedMin width = (Complexity.Circuit.multiplexer width).compose (Complexity.Circuit.unsignedLEWithPayload width)