Keyed unsigned minimum #

This module exposes a linear-size selector that compares two unsigned keys and returns the winning key with its associated payload.

@[simp]

(unsignedLEWithKeyedPayload keyWidth payloadWidth).size = 17 * keyWidth + 2 * payloadWidth + 1

Comparator-with-records has exact size linear in key and payload widths.

@[simp]

theorem Complexity.Circuit.eval_unsignedLEWithKeyedPayload (keyWidth payloadWidth : ℕ) [NeZero keyWidth] (leftKey : BitString keyWidth) (leftPayload : BitString payloadWidth) (rightKey : BitString keyWidth) (rightPayload : BitString payloadWidth) :

(unsignedLEWithKeyedPayload keyWidth payloadWidth).eval (leftKey.keyedMinimumInput leftPayload rightKey rightPayload) = BitString.multiplexerInput (decide (leftKey.unsignedValue ≤ rightKey.unsignedValue)) (Fin.append leftKey leftPayload) (Fin.append rightKey rightPayload)

Comparator-with-records emits its decision before the two complete records.

@[simp]

theorem Complexity.Circuit.size_unsignedKeyedMin (keyWidth payloadWidth : ℕ) [NeZero keyWidth] :

(unsignedKeyedMin keyWidth payloadWidth).size = 20 * keyWidth + 5 * payloadWidth + 1

The keyed selector has exact size linear in key and payload widths.

@[simp]

theorem Complexity.Circuit.eval_unsignedKeyedMin (keyWidth payloadWidth : ℕ) [NeZero keyWidth] (leftKey : BitString keyWidth) (leftPayload : BitString payloadWidth) (rightKey : BitString keyWidth) (rightPayload : BitString payloadWidth) :

(unsignedKeyedMin keyWidth payloadWidth).eval (leftKey.keyedMinimumInput leftPayload rightKey rightPayload) = leftKey.unsignedKeyedMin leftPayload rightKey rightPayload

The selector returns the record with smaller key, choosing left on ties.

Documentation