Fixed-width binary circuit-description codec -- definitions

This module flattens bounded gate-slot descriptions into one Boolean cube. Gate slots have a total fixed-width codec. Description decoding is partial only because the count word can represent values above gateBound.

def Complexity.CircuitCode.FixedWidth.GateSlot.encode {width : ℕ} (slot : GateSlot width) : BitString (3 + (width + width))

Flatten one gate slot into its three control bits followed by its two little-endian reference words.

Equations

• slot.encode = Fin.append ![slot.op, slot.negated0, slot.negated1] (Fin.append slot.input0 slot.input1)

def Complexity.CircuitCode.FixedWidth.GateSlot.decode {width : ℕ} (bits : BitString (3 + (width + width))) : GateSlot width

Split one fixed-width gate-slot word into its structural fields.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.encode {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : BitString (codeWidth inputWidth gateBound)

Flatten a bounded description into its count word followed by all gate slots in row-major order.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.countBits {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) : BitString (gateCountWidth gateBound)

Extract the leading fixed-width gate-count word.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.slotBits {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) (slot : Fin gateBound) : BitString (gateSlotWidth inputWidth gateBound)

Extract one fixed-width gate slot from a flattened description.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.countValue {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) : ℕ

Natural value represented by the leading little-endian count word.

Equations

• Complexity.CircuitCode.FixedWidth.Description.countValue code = Nat.fromBitsLE (Complexity.CircuitCode.FixedWidth.Description.countBits code).toList

def Complexity.CircuitCode.FixedWidth.Description.decode? {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) : Option (Description inputWidth gateBound)

Decode one flattened description, rejecting exactly the out-of-range gate-count words.

Equations

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