Documentation

Complexitylib.Models.RandomAccessMachine.Structured.Defs

Structured logarithmic-cost RAM programs — definitions #

This file defines a minimal first-order imperative language over RAM register stores. Atomic commands are the data-manipulating RAM instructions; sequencing, conditionals, and loops are structured syntax rather than program-counter arithmetic. The source semantics is independent of compilation and records the same operand-sensitive logarithmic cost and finite-support space measure as the target RAM.

Cmd.compileAt erases structured control flow into absolute jz/jmp targets. The compiler appends no hidden data operations: source and target executions therefore have equal register effects, logarithmic cost, and peak register space.

source
@[reducible, inline]
abbrev Complexity.RAM.Structured.Store :
Type

A source store maps register indices to natural-number contents.

Equations
Instances For
    source
    noncomputable def Complexity.RAM.Structured.Store.space (store : Store) :
    ℕ

    Logarithmic space occupied by a source store. This deliberately matches RAM.Cfg.space, but does not mention a target program counter.

    Equations
    Instances For
      source
      def Complexity.RAM.Structured.Input.bitValue (bit : Bool) :
      ℕ

      Natural-number representation of one input bit.

      Equations
      Instances For
        source
        def Complexity.RAM.Structured.Input.bitStore (lengthReg inputBase : ℕ) (bits : List Bool) :
        Store

        Store a bit string above a reserved register prefix, with its length in a distinguished register.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          inductive Complexity.RAM.Structured.Basic :
          Type

          Data-manipulating instructions of the structured source language. Control flow is represented by Cmd, so arbitrary jumps and halt are not source atoms.

          Instances For
            source
            @[implicit_reducible]
            instance Complexity.RAM.Structured.instReprBasic :
            Repr Basic
            Equations
            source
            def Complexity.RAM.Structured.instReprBasic.repr :
            Basic → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.RAM.Structured.instDecidableEqBasic.decEq (x✝ x✝¹ : Basic) :
              Decidable (x✝ = x✝¹)
              Equations
              Instances For
                source
                @[implicit_reducible]
                instance Complexity.RAM.Structured.instDecidableEqBasic :
                DecidableEq Basic
                Equations
                source
                def Complexity.RAM.Structured.instInhabitedBasic.default :
                Basic
                Equations
                Instances For
                  source
                  @[implicit_reducible]
                  instance Complexity.RAM.Structured.instInhabitedBasic :
                  Inhabited Basic
                  Equations
                  source
                  def Complexity.RAM.Structured.Basic.exec :
                  Basic → Store → Store

                  Execute one source-level basic instruction on a register store.

                  Equations
                  Instances For
                    source
                    def Complexity.RAM.Structured.Basic.instr :
                    Basic → Instr

                    Erase a source basic instruction to the corresponding RAM instruction.

                    Equations
                    Instances For
                      source
                      def Complexity.RAM.Structured.Basic.logCost :
                      Basic → Store → ℕ

                      Operand-sensitive source cost of one basic instruction.

                      Equations
                      Instances For
                        source
                        def Complexity.RAM.Structured.Basic.execList :
                        List Basic → Store → Store

                        Execute a straight-line list of basic instructions.

                        Equations
                        Instances For
                          source
                          inductive Complexity.RAM.Structured.Cmd :
                          Type

                          Minimal structured imperative syntax over RAM stores.

                          Instances For
                            source
                            def Complexity.RAM.Structured.instReprCmd.repr :
                            Cmd → ℕ → Std.Format
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[implicit_reducible]
                              instance Complexity.RAM.Structured.instReprCmd :
                              Repr Cmd
                              Equations
                              source
                              def Complexity.RAM.Structured.instDecidableEqCmd.decEq (x✝ x✝¹ : Cmd) :
                              Decidable (x✝ = x✝¹)
                              Equations
                              Instances For
                                source
                                @[implicit_reducible]
                                instance Complexity.RAM.Structured.instDecidableEqCmd :
                                DecidableEq Cmd
                                Equations
                                source
                                @[implicit_reducible]
                                instance Complexity.RAM.Structured.instInhabitedCmd :
                                Inhabited Cmd
                                Equations
                                source
                                def Complexity.RAM.Structured.instInhabitedCmd.default :
                                Cmd
                                Equations
                                Instances For
                                  source
                                  def Complexity.RAM.Structured.Cmd.codeSize :
                                  Cmd → ℕ

                                  Number of RAM instructions emitted for a structured command.

                                  Equations
                                  Instances For
                                    source
                                    def Complexity.RAM.Structured.Cmd.compileAt (start : ℕ) :
                                    Cmd → Program

                                    Compile a command whose first instruction will be placed at start. All generated branch destinations are absolute RAM program counters.

                                    Equations
                                    Instances For
                                      source
                                      def Complexity.RAM.Structured.Cmd.compile (cmd : Cmd) :
                                      Program

                                      Compile a closed source command and halt immediately after it finishes.

                                      Equations
                                      Instances For
                                        source
                                        def Complexity.RAM.Structured.Cmd.seqList :
                                        List Cmd → Cmd

                                        Right-associated sequential composition of a list of commands.

                                        Equations
                                        Instances For
                                          source
                                          def Complexity.RAM.Structured.Cmd.basics (ops : List Basic) :
                                          Cmd

                                          Embed a straight-line list of basic instructions as one structured command.

                                          Equations
                                          Instances For
                                            source
                                            inductive Complexity.RAM.Structured.Exec :
                                            Cmd → Store → Store → ℕ → ℕ → ℕ → Prop

                                            Independent big-step semantics for structured commands. Besides the final store, the relation records target instruction steps, exact logarithmic cost, and peak source-store space. Branch and loop-control costs are explicit.

                                            • skip (store : Store) : Exec Cmd.skip store store 0 0 store.space
                                            • basic (op : Basic) (store : Store) : Exec (Cmd.basic op) store (op.exec store) 1 (op.logCost store) (max store.space (op.exec store).space)
                                            • seq {first second : Cmd} {store middle final : Store} {firstSteps secondSteps firstCost secondCost firstSpace secondSpace : ℕ} (hfirst : Exec first store middle firstSteps firstCost firstSpace) (hsecond : Exec second middle final secondSteps secondCost secondSpace) : Exec (first.seq second) store final (firstSteps + secondSteps) (firstCost + secondCost) (max firstSpace secondSpace)
                                            • ifZero {test : ℕ} {onZero onNonzero : Cmd} {store final : Store} {steps cost space : ℕ} (htest : store test = 0) (hbranch : Exec onZero store final steps cost space) : Exec (Cmd.ifZero test onZero onNonzero) store final (steps + 1) (bitlen (store test) + 1 + cost) (max store.space space)
                                            • ifNonzero {test : ℕ} {onZero onNonzero : Cmd} {store final : Store} {steps cost space : ℕ} (htest : store test ≠ 0) (hbranch : Exec onNonzero store final steps cost space) : Exec (Cmd.ifZero test onZero onNonzero) store final (steps + 2) (bitlen (store test) + 1 + cost + 1) (max store.space space)
                                            • whileZero {test : ℕ} {body : Cmd} {store : Store} (htest : store test = 0) : Exec (Cmd.whileNonzero test body) store store 1 (bitlen (store test) + 1) store.space
                                            • whileNonzero {test : ℕ} {body : Cmd} {store middle final : Store} {bodySteps loopSteps bodyCost loopCost bodySpace loopSpace : ℕ} (htest : store test ≠ 0) (hbody : Exec body store middle bodySteps bodyCost bodySpace) (hloop : Exec (Cmd.whileNonzero test body) middle final loopSteps loopCost loopSpace) : Exec (Cmd.whileNonzero test body) store final (bodySteps + loopSteps + 2) (bitlen (store test) + 1 + bodyCost + 1 + loopCost) (max bodySpace loopSpace)
                                            Instances For