Fixed-width binary circuit-description codec -- proof internals

theorem Complexity.CircuitCode.FixedWidth.GateSlot.decode_encode_internal {width : ℕ} (slot : GateSlot width) : decode slot.encode = slot

theorem Complexity.CircuitCode.FixedWidth.GateSlot.encode_decode_internal {width : ℕ} (bits : BitString (3 + (width + width))) : (decode bits).encode = bits

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

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

Internal exact equivalence between gate slots and their fixed-width binary words.

Equations

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

theorem Complexity.CircuitCode.FixedWidth.Description.countBits_encode_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : countBits description.encode = GateSlot.referenceBits (gateCountWidth gateBound) description.gateCountNat

theorem Complexity.CircuitCode.FixedWidth.Description.slotBits_encode_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (slot : Fin gateBound) : slotBits description.encode slot = (description.slots slot).encode

theorem Complexity.CircuitCode.FixedWidth.Description.countValue_encode_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : countValue description.encode = description.gateCountNat

theorem Complexity.CircuitCode.FixedWidth.Description.decode?_encode_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : decode? description.encode = some description

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

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

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