Documentation

CslibFrontier.Computability.WordRAM.ExactLog

Exact-basis Word-RAM binary logarithms and arithmetic helpers #

This file provides structured subprograms over Cslib.WordRAM.Basis.exact for floor and ceiling base-2 logarithms (log2Loop and clog2Loop), an equal-cost register-maximum gadget (maxCode), and an .exactBin execution helper (exec_exactBin).

Whereas Cslib.Algorithms.WordRAM.NatLog and Cslib.Algorithms.WordRAM.NatClog are Code .standard 4 programs with ExecWithin upper bounds, the subprograms here operate in the .exact basis using right-shift division by 2 (>>> 1) and carry exact closed-form Exec step counts (4 * Nat.log 2 rem + 2 and 5 * Nat.clog 2 rem + 2) together with explicit final-state formulas (log2LoopData and clog2LoopData) for embedding via Code.rename.

Main definitions #

Main results #

source
theorem Cslib.WordRAM.ExactLog.exec_exactBin {w r : ℕ} {f : BinOp} {dst i j : Fin r} {d : Data r} {v : ℕ} (hev : f.evalExact (d.regs i) (d.regs j) = some v) (hfit : Fits w v) :
Exec w (Code.op (Op.exactBin f dst i j)) d (d.set dst v) 1

Execute a single .exactBin operation when evalExact returns some v and Fits w v.

source
def Cslib.WordRAM.ExactLog.maxCode {n : ℕ} (dst a b : Fin n) :
Code Basis.exact n

3-instruction equal-cost branch setting register dst to max (x.regs a) (x.regs b).

Instances For
    source
    theorem Cslib.WordRAM.ExactLog.maxCode_exec {w n : ℕ} (dst a b : Fin n) (x : Data n) :
    Exec w (maxCode dst a b) x (x.set dst (max (x.regs a) (x.regs b))) 3

    maxCode dst a b executes deterministically in 3 instructions and sets dst to max (x.regs a) (x.regs b).

    source
    def Cslib.WordRAM.ExactLog.log2Body :
    Code Basis.exact 3

    One iteration of the floor-log₂ loop on Data 3 (reg 0 = rem, reg 1 = acc, reg 2 = 1): shifts rem right by 1 (rem / 2) and increments acc.

    Instances For
      source
      def Cslib.WordRAM.ExactLog.log2Loop :
      Code Basis.exact 3

      Floor-log₂ loop while 1 < rem do [ rem ← rem >>> 1; acc ← acc + 1 ].

      Instances For
        source
        def Cslib.WordRAM.ExactLog.log2LoopData (rem acc : ℕ) (x : Data 3) :
        Data 3

        Closed-form final state of log2Loop starting from rem in register 0 and acc in register 1.

        Instances For
          source
          theorem Cslib.WordRAM.ExactLog.log2Loop_exec {w : ℕ} (rem : ℕ) {acc : ℕ} {x : Data 3} (hrem : x.regs 0 = rem) (hacc : x.regs 1 = acc) (hone : x.regs 2 = 1) (hfit_rem : Fits w rem) (hfit_acc : Fits w (acc + Nat.log 2 rem)) :
          Exec w log2Loop x (log2LoopData rem acc x) (4 * Nat.log 2 rem + 2)

          log2Loop executes deterministically in 4 * Nat.log 2 rem + 2 instructions, accumulating acc + Nat.log 2 rem into register 1 and preserving all memory.

          source
          def Cslib.WordRAM.ExactLog.clog2Body :
          Code Basis.exact 3

          Body of clog2Loop on Data 3 (reg 0 = rem, reg 1 = acc, reg 2 = 1): updates rem ← (rem + 1) >>> 1 (= (rem + 1) / 2) and acc ← acc + 1.

          Instances For
            source
            def Cslib.WordRAM.ExactLog.clog2Loop :
            Code Basis.exact 3

            Ceiling-log₂ loop while 1 < rem do [ rem ← (rem + 1) >>> 1; acc ← acc + 1 ].

            Instances For
              source
              def Cslib.WordRAM.ExactLog.clog2LoopData (rem acc : ℕ) (x : Data 3) :
              Data 3

              Closed-form final state of clog2Loop.

              Instances For
                source
                theorem Cslib.WordRAM.ExactLog.clog2Loop_exec {w : ℕ} (rem : ℕ) {acc : ℕ} {x : Data 3} (hrem : x.regs 0 = rem) (hacc : x.regs 1 = acc) (hone : x.regs 2 = 1) (hfit_rem1 : Fits w (rem + 1)) (hfit_acc : Fits w (acc + Nat.clog 2 rem)) :
                Exec w clog2Loop x (clog2LoopData rem acc x) (5 * Nat.clog 2 rem + 2)

                clog2Loop executes deterministically in 5 * Nat.clog 2 rem + 2 instructions, accumulating acc + Nat.clog 2 rem into register 1 and preserving all memory.