Documentation

Complexitylib.Circuits.Encoding.Threshold.Defs

Raw threshold-circuit fragments #

This file defines an appendable raw circuit that tests whether at least a specified number of existing Boolean wires are true. The construction is the standard unary dynamic program. Its state after reading i inputs records, for each r, whether at least r of those inputs were true.

Two gates update each state cell:

next (r + 1) = previous (r + 1) OR (input AND previous r).

The fragment starts with reusable false and true wires, emits the table in row-major order, and ends with a copy of the requested final state. Thus it has exactly 3 + 2 * k * threshold gates for k referenced inputs.

source
def Complexity.CircuitCode.Threshold.falseWire (available : ℕ) :
ℕ

The constant-false wire at the start of a threshold fragment.

Equations
Instances For
    source
    def Complexity.CircuitCode.Threshold.trueWire (available : ℕ) :
    ℕ

    The constant-true wire at the start of a threshold fragment.

    Equations
    Instances For
      source
      def Complexity.CircuitCode.Threshold.andWire (available threshold inputRow thresholdColumn : ℕ) :
      ℕ

      The conjunction wire for table cell (inputRow, thresholdColumn).

      Equations
      Instances For
        source
        def Complexity.CircuitCode.Threshold.cellWire (available threshold inputRow thresholdColumn : ℕ) :
        ℕ

        The completed dynamic-programming state wire for a table cell.

        Equations
        Instances For
          source
          def Complexity.CircuitCode.Threshold.stateWire (available threshold : ℕ) :
          ℕ → ℕ → ℕ

          Wire representing whether the first inputCount inputs contain at least required true values.

          The zero threshold is always true. Before any input has been processed, every positive threshold is false. All other states are table-cell outputs.

          Equations
          Instances For
            source
            def Complexity.CircuitCode.Threshold.cellGates (available threshold inputRow thresholdColumn input : ℕ) :
            RawCircuit

            The two raw gates that update one unary threshold-table cell.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.CircuitCode.Threshold.rowPrefix (available threshold inputRow input : ℕ) :
              ℕ → RawCircuit

              Emit the first columnCount cells of one table row.

              Equations
              Instances For
                source
                def Complexity.CircuitCode.Threshold.rows (available threshold inputRow inputCount : ℕ) :
                (Fin inputCount → ℕ) → RawCircuit

                Emit successive table rows, starting at inputRow.

                Equations
                Instances For
                  source
                  def Complexity.CircuitCode.Threshold.outputWire (available inputCount threshold : ℕ) :
                  ℕ

                  Absolute wire carrying the threshold fragment's final output.

                  Equations
                  Instances For
                    source
                    def Complexity.CircuitCode.Threshold.compileRaw (available threshold : ℕ) {inputCount : ℕ} (refs : Fin inputCount → ℕ) :
                    RawCircuit

                    Compile an at-least-threshold test over existing absolute wire references.

                    The result is appendable without renumbering. Its output is true exactly when at least threshold of the referenced wires are true.

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