Documentation

Complexitylib.Models.RandomAccessMachine.Structured.UnaryDecode.Defs

Structured RAM terminated-unary cursor decoder — definitions #

This reusable parser consumes the first terminated-unary field of an input bit array. It is the first nested-control component of the RAM circuit evaluator: the loop can exit either successfully at a zero terminator or unsuccessfully at the end of the available array.

source
def Complexity.RAM.Structured.UnaryDecode.verdictReg :
ℕ

Success verdict: one exactly when a zero terminator was consumed.

Equations
Instances For
    source
    def Complexity.RAM.Structured.UnaryDecode.valueReg :
    ℕ

    Decoded unary value.

    Equations
    Instances For
      source
      def Complexity.RAM.Structured.UnaryDecode.pointerReg :
      ℕ

      Address of the next unconsumed input bit.

      Equations
      Instances For
        source
        def Complexity.RAM.Structured.UnaryDecode.remainingReg :
        ℕ

        Number of unconsumed input bits.

        Equations
        Instances For
          source
          def Complexity.RAM.Structured.UnaryDecode.oneReg :
          ℕ

          Constant-one register.

          Equations
          Instances For
            source
            def Complexity.RAM.Structured.UnaryDecode.bitReg :
            ℕ

            Current input bit.

            Equations
            Instances For
              source
              def Complexity.RAM.Structured.UnaryDecode.activeReg :
              ℕ

              Loop activity flag.

              Equations
              Instances For
                source
                def Complexity.RAM.Structured.UnaryDecode.inputBase :
                ℕ

                First register occupied by input bits.

                Equations
                Instances For
                  source
                  def Complexity.RAM.Structured.UnaryDecode.inputStore (bits : List Bool) :
                  Store

                  Reserved-register input store for one unary field and its suffix.

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

                    Initialize the parser cursor, accumulator, constant, and activity flag.

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

                      Parser initialization.

                      Equations
                      Instances For
                        source
                        def Complexity.RAM.Structured.UnaryDecode.stopTruncated :
                        Cmd

                        Record an unterminated field after exhausting the available input.

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

                          Record a successfully consumed zero terminator.

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

                            Consume one available bit and either stop or increment the unary value.

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

                              One parser iteration, including the exhausted-input case.

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

                                Iterate until the parser records success or truncation.

                                Equations
                                Instances For
                                  source
                                  structure Complexity.RAM.Structured.UnaryDecode.CursorReady (inputLength : ℕ) (remaining : List Bool) (offset value : ℕ) (store : Store) :
                                  Prop

                                  Semantic calling convention for invoking mainLoop at an existing cursor.

                                  The already-consumed prefix is represented by offset; value is the current field's unary accumulator, and remaining is the still-readable suffix. Registers at or above inputBase are data rather than parser scratch, so the loop's routine theorem can frame them unchanged.

                                  • total_eq : offset + remaining.length = inputLength

                                    Consumed and remaining bits account for the original input.

                                  • value_le_offset : value ≤ offset

                                    The current field accumulator cannot exceed the absolute cursor offset.

                                  • verdict_eq : store verdictReg = 0

                                    No successful terminator has been recorded yet.

                                  • value_eq : store valueReg = value

                                    The accumulator contains the current field's consumed one-bits.

                                  • pointer_eq : store pointerReg = inputBase + offset

                                    The cursor points to the first remaining bit.

                                  • remaining_eq : store remainingReg = remaining.length

                                    The remaining-length register agrees with the semantic suffix.

                                  • one_eq : store oneReg = 1

                                    The parser's constant-one register is initialized.

                                  • active_eq : store activeReg = 1

                                    The loop is active.

                                  • input_eq (delta : ℕ) : store (inputBase + offset + delta) = match remaining[delta]? with | some bit => Input.bitValue bit | none => 0

                                    Physical input registers encode the remaining semantic suffix.

                                  Instances For
                                    source
                                    def Complexity.RAM.Structured.UnaryDecode.loopStepCount (remaining : List Bool) :
                                    ℕ

                                    Exact transition count for invoking mainLoop at a semantic suffix.

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

                                      Complete terminated-unary decoder.

                                      Equations
                                      Instances For
                                        source
                                        def Complexity.RAM.Structured.UnaryDecode.compiled :
                                        Program

                                        Concrete compiled RAM decoder.

                                        Equations
                                        Instances For
                                          source
                                          def Complexity.RAM.Structured.UnaryDecode.stepCount (bits : List Bool) :
                                          ℕ

                                          Exact compiled transition count through the first terminator or exhaustion.

                                          Equations
                                          Instances For
                                            source
                                            def Complexity.RAM.Structured.UnaryDecode.timeBound (inputLength : ℕ) :
                                            ℕ

                                            Explicit logarithmic-time budget.

                                            Equations
                                            Instances For
                                              source
                                              def Complexity.RAM.Structured.UnaryDecode.spaceBound (inputLength : ℕ) :
                                              ℕ

                                              Explicit peak-space budget.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                def Complexity.RAM.Structured.UnaryDecode.quasilinearBound (inputLength : ℕ) :
                                                ℕ

                                                Shifted quasilinear comparison function.

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