Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Codec

Fixed-width binary circuit-description codec #

Gate slots are in exact correspondence with their fixed-width Boolean words. Bounded descriptions also have an exact codec, except that decoding rejects the count words whose values exceed the advertised gate bound.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.GateSlot.decode_encode {width : ℕ} (slot : GateSlot width) :
decode slot.encode = slot

Decoding the fixed-width code of a gate slot recovers the slot.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.GateSlot.encode_decode {width : ℕ} (bits : BitString (3 + (width + width))) :
(decode bits).encode = bits

Encoding any decoded fixed-width gate-slot word recovers the word.

source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.encode_injective {width : ℕ} :
Function.Injective encode

Fixed-width gate-slot encoding is injective.

source
def Complexity.CircuitCode.FixedWidth.GateSlot.codecEquiv (width : ℕ) :
GateSlot width ≃ BitString (3 + (width + width))

Gate slots are in exact correspondence with fixed-width Boolean words.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.CircuitCode.FixedWidth.Description.countBits_encode {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) :
    countBits description.encode = GateSlot.referenceBits (gateCountWidth gateBound) description.gateCountNat

    Encoding places the gate count in the leading count word.

    source
    @[simp]
    theorem Complexity.CircuitCode.FixedWidth.Description.slotBits_encode {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (slot : Fin gateBound) :
    slotBits description.encode slot = (description.slots slot).encode

    Encoding places each gate slot in its corresponding fixed-width block.

    source
    @[simp]
    theorem Complexity.CircuitCode.FixedWidth.Description.countValue_encode {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) :
    countValue description.encode = description.gateCountNat

    Reading the leading count word of an encoding recovers the gate count.

    source
    @[simp]
    theorem Complexity.CircuitCode.FixedWidth.Description.decode?_encode {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) :
    decode? description.encode = some description

    Encoding and then decoding a bounded description is exact.

    source
    theorem Complexity.CircuitCode.FixedWidth.Description.encode_eq_of_decode?_eq_some {inputWidth gateBound : ℕ} {code : BitString (codeWidth inputWidth gateBound)} {description : Description inputWidth gateBound} (hdecode : decode? code = some description) :
    description.encode = code

    A successfully decoded description re-encodes to the original word.

    source
    theorem Complexity.CircuitCode.FixedWidth.Description.decode?_eq_some_iff {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) (description : Description inputWidth gateBound) :
    decode? code = some description ↔ code = description.encode

    Decoding succeeds with a description exactly on that description's fixed-width code.

    source
    theorem Complexity.CircuitCode.FixedWidth.Description.encode_injective {inputWidth gateBound : ℕ} :
    Function.Injective encode

    Fixed-width bounded-description encoding is injective.