Documentation

Complexitylib.Models.RandomAccessMachine.Structured.GateStep.Defs

Structured RAM serialized-gate step — definitions #

This program composes the terminated-unary cursor routine with the decoded-gate kernel. Its input is one canonical gate encoding followed immediately by the current Boolean wire memo. The fixed three-bit header is consumed directly, the two references are decoded by two calls to the same loop, and the resulting gate is evaluated and appended without specializing the program to the input.

source
def Complexity.RAM.Structured.GateStep.headerOpReg :
ℕ

The operation header bit is retained in the consumed input prefix.

Equations
Instances For
    source
    def Complexity.RAM.Structured.GateStep.headerNegated0Reg :
    ℕ

    The first negation header bit is retained in the consumed input prefix.

    Equations
    Instances For
      source
      def Complexity.RAM.Structured.GateStep.headerNegated1Reg :
      ℕ

      The second negation header bit is retained in the consumed input prefix.

      Equations
      Instances For
        source
        def Complexity.RAM.Structured.GateStep.savedInput0Reg :
        ℕ

        The first decoded reference is retained in the consumed input prefix.

        Equations
        Instances For
          source
          def Complexity.RAM.Structured.GateStep.inputBits (gate : CircuitCode.RawGate) (wires : List Bool) :
          List Bool

          Canonical gate code followed by its current wire memo.

          Equations
          Instances For
            source
            def Complexity.RAM.Structured.GateStep.memoBase (gate : CircuitCode.RawGate) :
            ℕ

            First physical register occupied by the wire memo.

            Equations
            Instances For
              source
              def Complexity.RAM.Structured.GateStep.inputStore (gate : CircuitCode.RawGate) (wires : List Bool) :
              Store

              Machine input for one serialized gate and the current wire memo.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.RAM.Structured.GateStep.headerOps :
                List Basic

                Consume and retain the fixed operation and negation header bits.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Complexity.RAM.Structured.GateStep.saveRestartOps :
                  List Basic

                  Save the first reference and restart the cursor accumulator for the second.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Complexity.RAM.Structured.GateStep.marshalOps :
                    List Basic

                    Marshal the parsed cursor state into the decoded-gate evaluator ABI.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Complexity.RAM.Structured.GateStep.program :
                      Cmd

                      Parse and evaluate one serialized gate, appending its result to the memo.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Complexity.RAM.Structured.GateStep.compiled :
                        Program

                        Concrete compiled serialized-gate step.

                        Equations
                        Instances For
                          source
                          def Complexity.RAM.Structured.GateStep.stepCount (gate : CircuitCode.RawGate) :
                          ℕ

                          Exact transition count for a canonical serialized gate.

                          Equations
                          Instances For
                            source
                            def Complexity.RAM.Structured.GateStep.storeBound (gate : CircuitCode.RawGate) (wires : List Bool) :
                            ℕ

                            Uniform envelope including the newly appended wire.

                            Equations
                            Instances For
                              source
                              def Complexity.RAM.Structured.GateStep.timeBound (gate : CircuitCode.RawGate) (wires : List Bool) :
                              ℕ

                              Explicit logarithmic-cost budget for one serialized-gate step.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def Complexity.RAM.Structured.GateStep.spaceBound (gate : CircuitCode.RawGate) (wires : List Bool) :
                                ℕ

                                Explicit peak-space budget including the appended memo cell.

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