Documentation

Complexitylib.Circuits.BinaryComparison.Defs

Little-endian binary comparison -- definitions #

This module defines unsigned interpretation and comparison for fixed-width little-endian bit strings, together with a linear-size Boolean formula for the comparison. The two input words occupy consecutive variable blocks.

source
def Complexity.BitString.unsignedValue {width : ℕ} (bits : BitString width) :
ℕ

Interpret a fixed-width bit string as an unsigned little-endian natural.

Equations
Instances For
    source
    def Complexity.BitString.unsignedLE {width : ℕ} :
    BitString width → BitString width → Bool

    Compare two equally wide little-endian words from their most significant bits downward.

    Equations
    • One or more equations did not get rendered due to their size.
    • x_3.unsignedLE x_4 = true
    Instances For
      source
      def Complexity.BoolFormula.ofBool :
      Bool → BoolFormula

      Embed one Boolean value as a constant formula leaf.

      Equations
      Instances For
        source
        def Complexity.BoolFormula.unsignedLEOf {width : ℕ} :
        (Fin width → BoolFormula) → (Fin width → BoolFormula) → BoolFormula

        Compare two fixed-width vectors of Boolean formulas as little-endian unsigned words. This general form supports variables, constants, and later compiled wire layouts without changing the comparator tree.

        Equations
        Instances For
          source
          def Complexity.BoolFormula.unsignedLELeftConstant {width : ℕ} (left : BitString width) (rightBase : ℕ) :
          BoolFormula

          Compare a constant left word with a variable block beginning at rightBase.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.BoolFormula.unsignedLERightConstant {width : ℕ} (leftBase : ℕ) (right : BitString width) :
            BoolFormula

            Compare a variable block beginning at leftBase with a constant right word.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.BoolFormula.unsignedLEAux (width leftBase rightBase : ℕ) :
              BoolFormula

              Formula for unsigned comparison of two width-bit words beginning at the given variable bases.

              Equations
              Instances For
                source
                def Complexity.BoolFormula.unsignedLE (width : ℕ) :
                BoolFormula

                Formula comparing the first width input variables with the next width variables as unsigned little-endian words.

                Equations
                Instances For
                  source
                  def Complexity.CircuitCode.unsignedLERawCircuit (width : ℕ) :
                  RawCircuit

                  Raw fan-in-two circuit comparing two consecutive width-bit unsigned little-endian words.

                  Equations
                  Instances For