Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Conversion.Defs

Conversion between raw circuits and fixed-width descriptions -- definitions #

This module encodes each bounded topologically ordered raw circuit into the fixed gate-slot representation. Active slots contain fixed-width little-endian references and all inactive slots are zero. The inverse direction is the Description.toRawCircuit operation from the core fixed-width layer.

source
def Complexity.CircuitCode.FixedWidth.GateSlot.referenceBits (width value : ℕ) :
BitString width

A natural number truncated to one fixed-width little-endian reference word.

Equations
Instances For
    source
    def Complexity.CircuitCode.FixedWidth.GateSlot.ofRawGate (width : ℕ) (gate : RawGate) :
    GateSlot width

    Encode one raw gate into a fixed-width slot. References outside the word range are truncated; bounded well-formed circuits never take that path.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.CircuitCode.FixedWidth.Description.ofRawCircuit {inputWidth gateBound : ℕ} (circuit : RawCircuit) (hbound : List.length circuit ≤ gateBound) :
      Description inputWidth gateBound

      Canonical fixed-slot description of a raw circuit within gateBound. Slots after the circuit's final gate are all zero.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.CircuitCode.FixedWidth.ValidDescription (inputWidth gateBound : ℕ) :
        Type

        Valid fixed-width descriptions at one arity and gate bound.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable instance Complexity.CircuitCode.FixedWidth.instFintypeValidDescription (inputWidth gateBound : ℕ) :
          Fintype (ValidDescription inputWidth gateBound)
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[instance_reducible]
          instance Complexity.CircuitCode.FixedWidth.instDecidableEqValidDescription (inputWidth gateBound : ℕ) :
          DecidableEq (ValidDescription inputWidth gateBound)
          Equations
          source
          def Complexity.CircuitCode.FixedWidth.BoundedRawCircuit (inputWidth gateBound : ℕ) :
          Type

          Nonempty topologically ordered raw circuits within one gate bound.

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