Documentation

Complexity.Computability.WordRAM.ArrayNormalize

Charged in-place normalization of an array #

ArrayNormalize.program replaces each word of a supplied interval by its remainder modulo a supplied positive modulus. It executes actual loads, remainders and stores; the untouched memory need not already be normalized. This small topic module avoids adding an application specific transformation to the allocation API.

source
@[reducible, inline]
abbrev Cslib.WordRAM.ArrayNormalize.base :
Fin 7

First address to normalize.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.WordRAM.ArrayNormalize.length :
    Fin 7

    Number of words.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.WordRAM.ArrayNormalize.modulus :
      Fin 7

      Positive normalization modulus.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.WordRAM.ArrayNormalize.index :
        Fin 7

        Current index.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.WordRAM.ArrayNormalize.address :
          Fin 7

          Temporary absolute address.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.WordRAM.ArrayNormalize.value :
            Fin 7

            Loaded and normalized word.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.WordRAM.ArrayNormalize.one :
              Fin 7

              Constant one.

              Instances For
                source
                def Cslib.WordRAM.ArrayNormalize.body :
                Code Basis.standard 7

                Normalize one cell with five actual native instructions.

                Instances For
                  source
                  def Cslib.WordRAM.ArrayNormalize.program :
                  Code Basis.standard 7

                  Fixed code for in-place normalization of an interval supplied in registers.

                  Instances For
                    source
                    def Cslib.WordRAM.ArrayNormalize.normalizePrefix (mem : ℕ → ℕ) (b M k : ℕ) :
                    ℕ → ℕ

                    Mathematical memory after normalizing a prefix; this is not a machine operation.

                    Instances For
                      source
                      theorem Cslib.WordRAM.ArrayNormalize.normalizePrefix_read (mem : ℕ → ℕ) (b M n j : ℕ) (hj : j < n) :
                      normalizePrefix mem b M n (b + j) = mem (b + j) % M

                      Every cell in the normalized interval contains its original remainder.

                      source
                      theorem Cslib.WordRAM.ArrayNormalize.normalizePrefix_outside (mem : ℕ → ℕ) (b M n a : ℕ) (ha : ¬(b ≤ a ∧ a < b + n)) :
                      normalizePrefix mem b M n a = mem a

                      Normalizing an interval leaves all outside memory unchanged.

                      source
                      theorem Cslib.WordRAM.ArrayNormalize.exec {W b M n : ℕ} (x : Data 7) (hb : x.regs base = b) (hn : x.regs length = n) (hm : x.regs modulus = M) (hM : 0 < M) (hfit : Fits W (b + n + M + 2)) :
                      ∃ (y : Data 7), ExecWithin W program x y (7 * n + 4) ∧ y.mem = normalizePrefix x.mem b M n ∧ y.regs base = b ∧ y.regs length = n ∧ y.regs modulus = M

                      In-place normalization costs at most 7n+4 native instructions, including every indexed load/store and loop decision. The input arguments and all outside memory are preserved.