Documentation

Complexity.Algorithms.WordRAM.NatSqrt

A charged native integer square root #

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.NatSqrt.arg :
Fin 6

Input integer, preserved.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.NatSqrt.root :
    Fin 6

    Current root and output.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.NatSqrt.next :
      Fin 6

      Successor of the current root.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.NatSqrt.square :
        Fin 6

        Square of the successor.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.NatSqrt.one :
          Fin 6

          Constant one.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.NatSqrt.bound :
            Fin 6

            Input plus one.

            Instances For
              source
              def Cslib.Algorithms.WordRAM.NatSqrt.body :
              WordRAM.Code WordRAM.Basis.standard 6

              Advance the root and compute the next square.

              Instances For
                source
                def Cslib.Algorithms.WordRAM.NatSqrt.program :
                WordRAM.Code WordRAM.Basis.standard 6

                A fixed program for the integer square root, with all square computations charged.

                Instances For
                  source
                  theorem Cslib.Algorithms.WordRAM.NatSqrt.exec {w : ℕ} (x : WordRAM.Data 6) (hfit : WordRAM.Fits w (4 * x.regs arg + 4)) :
                  ∃ (y : WordRAM.Data 6), WordRAM.ExecWithin w program x y (5 * (x.regs arg).sqrt + 7) ∧ y.regs root = (x.regs arg).sqrt ∧ y.regs arg = x.regs arg ∧ y.mem = x.mem ∧ y.regs one = 1

                  Compute Nat.sqrt n in at most 5 sqrt(n) + 7 instructions, preserving input and memory. The linear bound 4n + 4 covers the final unsuccessful square as well as all counters.

                  source
                  theorem Cslib.Algorithms.WordRAM.NatSqrt.exec_rename {r w : ℕ} (f : Fin 6 → Fin r) (hf : Function.Injective f) (x : WordRAM.Data r) (hfit : WordRAM.Fits w (4 * x.regs (f arg) + 4)) :
                  ∃ (y : WordRAM.Data r), WordRAM.ExecWithin w (WordRAM.Code.rename f program) x y (5 * (x.regs (f arg)).sqrt + 7) ∧ y.regs (f root) = (x.regs (f arg)).sqrt ∧ y.regs (f arg) = x.regs (f arg) ∧ y.mem = x.mem ∧ y.regs (f one) = 1

                  Run successive squares on any injectively chosen registers.