Self-delimiting input-pair circuits -- definitions

This module materializes the library's list-level pairing codec from Boolean constants and selected primary inputs. The resulting circuit can feed a fixed serialized query directly into another circuit.

def Complexity.Circuit.pairSourceWidth (leftWidth rightWidth : ℕ) : ℕ

Width of pair left right when the two payload widths are fixed.

Equations

• Complexity.Circuit.pairSourceWidth leftWidth rightWidth = 2 * leftWidth + 2 + rightWidth

instance Complexity.Circuit.instNeZeroNatPairSourceWidth (leftWidth rightWidth : ℕ) : NeZero (pairSourceWidth leftWidth rightWidth)

def Complexity.Circuit.pairSourceList {inputWidth leftWidth rightWidth : ℕ} (left : Fin leftWidth → InputSource inputWidth) (right : Fin rightWidth → InputSource inputWidth) : List (InputSource inputWidth)

Source list for the self-delimiting pair: duplicate the left sources, write the 01 separator, then copy the right sources verbatim.

Equations

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

def Complexity.Circuit.pairSources {inputWidth leftWidth rightWidth : ℕ} (left : Fin leftWidth → InputSource inputWidth) (right : Fin rightWidth → InputSource inputWidth) : Fin (pairSourceWidth leftWidth rightWidth) → InputSource inputWidth

Fixed-width tuple of input sources spelling one self-delimiting pair.

Equations

• Complexity.Circuit.pairSources left right coordinate = (Complexity.Circuit.pairSourceList left right)[↑coordinate]

def Complexity.Circuit.pairInputSources {inputWidth leftWidth rightWidth : ℕ} [NeZero inputWidth] (left : Fin leftWidth → InputSource inputWidth) (right : Fin rightWidth → InputSource inputWidth) : Circuit Basis.andOr2 inputWidth (pairSourceWidth leftWidth rightWidth) 0

Zero-internal-gate circuit materializing one self-delimiting pair.

Equations

• Complexity.Circuit.pairInputSources left right = Complexity.Circuit.inputSources (Complexity.Circuit.pairSources left right)