Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.Instruction.DenseSimDefs

Dense-overlay instruction simulation -- controller definitions #

These definitions connect the dense instruction kernels to the existing fixed-program selector and representation-independent buffered cleanup pass.

source
def Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) :
Instr → TM (n + 1)

Execute one selected instruction against the dense public-input overlay.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.RAM.RegisterStore.Machine.denseDispatchProgramTM {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) :
    TM (n + 1)

    Dense finite branch tree selected by a decrementing PC copy.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.RAM.RegisterStore.Machine.denseProgramInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) :
      TM (n + 1)

      Copy the dense snapshot PC into selector scratch and dispatch once.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.RAM.RegisterStore.Machine.denseInstructionStore (input : List Bool) (instruction : Instr) (pcValue : ℕ) (overlay : Store) :
        Store

        Mutable overlay after one dense instruction.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.RAM.RegisterStore.Machine.denseInstructionPC (input : List Bool) (instruction : Instr) (pcValue : ℕ) (overlay : Store) :
          ℕ

          Program counter after one dense instruction.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.RAM.RegisterStore.Machine.denseInstructionCleanupValue (input : List Bool) (instruction : Instr) (overlay : Store) :
            Fin 5 → ℕ

            Exact values left on the five physical cleanup roles by a dense kernel.

            Equations
            Instances For
              source
              def Complexity.RAM.RegisterStore.Machine.denseInstructionRemainingValue (instruction : Instr) (overlay : Store) :
              ℕ

              Old overlay counter state before generic buffered cleanup.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Complexity.RAM.RegisterStore.Machine.DenseInstructionExecutionResult {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (instruction : Instr) (pcValue : ℕ) (overlay : Store) (work : Fin (n + 1) → Tape) :
                Prop

                Common dense semantic endpoint before representation cleanup.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Complexity.RAM.RegisterStore.Machine.DenseInstructionCleanupReady {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (instruction : Instr) (pcValue : ℕ) (overlay : Store) (sourceHeadBound : ℕ) (work : Fin (n + 1) → Tape) :
                  Prop

                  Dense endpoint plus the marker and source-cursor bounds needed by cleanup.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Complexity.RAM.RegisterStore.Machine.denseExecuteInstructionTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (instruction : Instr) (pcValue : ℕ) (overlay : Store) :
                    ℕ

                    Runtime of one statically selected dense instruction before cleanup.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Complexity.RAM.RegisterStore.Machine.denseDispatchProgramTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue : ℕ) :
                      Program → ℕ → ℕ

                      Dense branch-tree runtime for a represented selector.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Complexity.RAM.RegisterStore.Machine.denseProgramInstructionTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (pcValue : ℕ) (overlay : Store) :
                        ℕ

                        Complete dense selection and selected-instruction runtime.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Complexity.RAM.RegisterStore.Machine.denseProgramStepTM {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) :
                          TM (n + 1)

                          Select, execute, and clean one dense RAM instruction.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Complexity.RAM.RegisterStore.Machine.denseProgramStepSourceHeadBound {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (pcValue : ℕ) (overlay : Store) :
                            ℕ

                            Source-head bound after dense selection and execution.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def Complexity.RAM.RegisterStore.Machine.denseProgramStepTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (pcValue : ℕ) (overlay : Store) :
                              ℕ

                              Exact compositional time for one selected and cleaned dense RAM step.

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