Keyed unsigned minimum -- definitions

A keyed selector compares two little-endian keys and returns the winning key together with its payload. Inputs are packed record-first: left key, left payload, right key, then right payload.

def Complexity.BitString.keyedMinimumInput {keyWidth payloadWidth : ℕ} (leftKey : BitString keyWidth) (leftPayload : BitString payloadWidth) (rightKey : BitString keyWidth) (rightPayload : BitString payloadWidth) : BitString (keyWidth + payloadWidth + (keyWidth + payloadWidth))

Canonical record-first input order for keyed minimum selection.

Equations

• leftKey.keyedMinimumInput leftPayload rightKey rightPayload = Fin.append (Fin.append leftKey leftPayload) (Fin.append rightKey rightPayload)

def Complexity.BitString.unsignedKeyedMin {keyWidth payloadWidth : ℕ} (leftKey : BitString keyWidth) (leftPayload : BitString payloadWidth) (rightKey : BitString keyWidth) (rightPayload : BitString payloadWidth) : BitString (keyWidth + payloadWidth)

Select the record with smaller unsigned key, choosing the left record on ties.

Equations

• leftKey.unsignedKeyedMin leftPayload rightKey rightPayload = if leftKey.unsignedValue ≤ rightKey.unsignedValue then Fin.append leftKey leftPayload else Fin.append rightKey rightPayload

def Complexity.Circuit.keyedMinimumComparisonInput (keyWidth payloadWidth : ℕ) : Fin (keyWidth + keyWidth) → Fin (keyWidth + payloadWidth + (keyWidth + payloadWidth))

Embed the two key blocks from record-first input into comparator order.

Equations

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

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

Key comparison followed by an unchanged copy of both complete records.

Equations

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

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

Fan-in-two circuit selecting the record with minimum unsigned key.

Equations

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