Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.WordEncode.Defs

Self-delimiting word emission — definitions #

The encoded-store update path needs to re-emit decoded entries. A generic work-tape pass either emits one unary width mark per source bit or copies the payload bits themselves. wordEncodeTM composes those passes around a rewind.

source
inductive Complexity.RAM.RegisterStore.Machine.WorkEmitMode :
Type

Which half of a self-delimiting word a work-tape pass emits.

Instances For
    source
    @[implicit_reducible]
    instance Complexity.RAM.RegisterStore.Machine.instDecidableEqWorkEmitMode :
    DecidableEq WorkEmitMode
    Equations
    source
    @[implicit_reducible]
    instance Complexity.RAM.RegisterStore.Machine.instFintypeWorkEmitMode :
    Fintype WorkEmitMode

    WorkEmitMode is a finite controller parameter.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    inductive Complexity.RAM.RegisterStore.Machine.WorkEmitPhase :
    Type

    Finite phases of one work-tape emission pass.

    Instances For
      source
      @[implicit_reducible]
      instance Complexity.RAM.RegisterStore.Machine.instDecidableEqWorkEmitPhase :
      DecidableEq WorkEmitPhase
      Equations
      source
      @[implicit_reducible]
      instance Complexity.RAM.RegisterStore.Machine.instFintypeWorkEmitPhase :
      Fintype WorkEmitPhase

      WorkEmitPhase has exactly two states.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.RAM.RegisterStore.Machine.workEmitBits :
      WorkEmitMode → List Bool → List Bool

      Bits emitted by one complete pass. Width mode emits unary length followed by its zero separator; payload mode copies the source bits verbatim.

      Equations
      Instances For
        source
        def Complexity.RAM.RegisterStore.Machine.workEmitTM {n : ℕ} (idx : Fin n) (mode : WorkEmitMode) :
        TM n

        Scan one canonical Boolean work tape and append either its unary-width header or its payload to the output.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.RAM.RegisterStore.Machine.workEmitTime (bits : List Bool) :
          ℕ

          Exact time of one work-tape emission pass.

          Equations
          Instances For
            source
            def Complexity.RAM.RegisterStore.Machine.wordEncodeTM {n : ℕ} (idx : Fin n) :
            TM n

            Emit one complete self-delimiting word from a canonical binary work tape.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.RAM.RegisterStore.Machine.wordEncodeTime (value : ℕ) :
              ℕ

              Conservative exact-composition bound for one emitted natural.

              Equations
              Instances For
                source
                def Complexity.RAM.RegisterStore.Machine.rewindWordEncodeTM {n : ℕ} (idx : Fin n) :
                TM n

                Rewind an arbitrary positive cursor over canonical binary contents, then emit the complete self-delimiting word.

                Equations
                Instances For
                  source
                  def Complexity.RAM.RegisterStore.Machine.rewindWordEncodeTime (value headBound : ℕ) :
                  ℕ

                  Composition bound for rewind followed by complete word emission.

                  Equations
                  Instances For