Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Conversion

Conversion between raw circuits and fixed-width descriptions #

Canonical zero padding makes valid fixed-width descriptions exactly equivalent to nonempty topologically ordered raw circuits within the gate bound. The two round trips preserve every gate, reference, and control bit.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.GateSlot.toList_referenceBits (width value : ℕ) :
(referenceBits width value).toList = width.toBitsLE value

A fixed-width reference word serializes to the expected little-endian bits.

source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.toRawGate_ofRawGate {width : ℕ} {gate : RawGate} (hinput0 : gate.input₀ < 2 ^ width) (hinput1 : gate.input₁ < 2 ^ width) :
(ofRawGate width gate).toRawGate = gate

Encoding and decoding a raw gate is exact when both references fit.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.GateSlot.ofRawGate_toRawGate {width : ℕ} (slot : GateSlot width) :
ofRawGate width slot.toRawGate = slot

Every fixed slot is recovered after conversion through raw-gate syntax.

source
theorem Complexity.CircuitCode.FixedWidth.Description.toRawCircuit_ofRawCircuit {inputWidth gateBound : ℕ} {circuit : RawCircuit} (htopological : RawCircuit.TopologicallyWellFormed inputWidth circuit) (hbound : List.length circuit ≤ gateBound) :
(ofRawCircuit circuit hbound).toRawCircuit = circuit

Encoding a bounded topologically ordered raw circuit and converting it back preserves the exact gate list.

source
theorem Complexity.CircuitCode.FixedWidth.Description.ofRawCircuit_wellFormed {inputWidth gateBound : ℕ} {circuit : RawCircuit} (hcircuit : RawCircuit.WellFormed inputWidth circuit) (hbound : List.length circuit ≤ gateBound) :
(ofRawCircuit circuit hbound).WellFormed

A bounded valid raw circuit produces a valid fixed-width description.

source
theorem Complexity.CircuitCode.FixedWidth.Description.ofRawCircuit_toRawCircuit {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hcanonical : description.CanonicallyPadded) :
ofRawCircuit description.toRawCircuit ⋯ = description

Canonical padding makes conversion from a description through raw syntax an exact round trip.

source
def Complexity.CircuitCode.FixedWidth.wellFormedEquiv (inputWidth gateBound : ℕ) :
ValidDescription inputWidth gateBound ≃ BoundedRawCircuit inputWidth gateBound

Valid fixed-width descriptions are exactly bounded valid raw circuits.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.CircuitCode.FixedWidth.wellFormedEquiv_apply_val {inputWidth gateBound : ℕ} (description : ValidDescription inputWidth gateBound) :
    ↑((wellFormedEquiv inputWidth gateBound) description) = (↑description).toRawCircuit

    The forward equivalence map is the raw-circuit view of a valid fixed-width description.

    source
    @[simp]
    theorem Complexity.CircuitCode.FixedWidth.wellFormedEquiv_symm_val {inputWidth gateBound : ℕ} (circuit : BoundedRawCircuit inputWidth gateBound) :
    ↑((wellFormedEquiv inputWidth gateBound).symm circuit) = Description.ofRawCircuit ↑circuit ⋯

    The inverse equivalence map is canonical fixed-width conversion of a bounded raw circuit.

    source
    @[instance_reducible]
    noncomputable instance Complexity.CircuitCode.FixedWidth.instFintypeBoundedRawCircuit (inputWidth gateBound : ℕ) :
    Fintype (BoundedRawCircuit inputWidth gateBound)
    Equations
    • One or more equations did not get rendered due to their size.