Copying disjoint arrays on the word RAM

The seven-register copy routine charges every address calculation, load, store, increment, and loop test. Its source precedes its destination, as in a bump-allocated growing array. It is a fixed program: neither the length nor either address is baked into the code.

Main definitions

• Cslib.WordRAM.ArrayCopy.program: copying between addresses supplied in registers.
• Cslib.WordRAM.ArrayCopy.copyPrefix: mathematical specification of the writes.

Main results

• Cslib.WordRAM.ArrayCopy.exec: copying n words within 7 * n + 4 instructions, preserving the source and all cells outside the destination.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms.

def Cslib.WordRAM.ArrayCopy.copyPrefix (mem : ℕ → ℕ) (src dst k : ℕ) : ℕ → ℕ

The memory after copying a prefix into a disjoint destination block.

@[simp]

theorem Cslib.WordRAM.ArrayCopy.copyPrefix_zero (mem : ℕ → ℕ) (src dst : ℕ) : copyPrefix mem src dst 0 = mem

theorem Cslib.WordRAM.ArrayCopy.copyPrefix_read {mem : ℕ → ℕ} {src dst k j : ℕ} (hj : j < k) : copyPrefix mem src dst k (dst + j) = mem (src + j)

theorem Cslib.WordRAM.ArrayCopy.copyPrefix_outside {mem : ℕ → ℕ} {src dst k a : ℕ} (ha : ¬(dst ≤ a ∧ a < dst + k)) : copyPrefix mem src dst k a = mem a

theorem Cslib.WordRAM.ArrayCopy.copyPrefix_succ (mem : ℕ → ℕ) (src dst k : ℕ) : copyPrefix mem src dst (k + 1) = Function.update (copyPrefix mem src dst k) (dst + k) (mem (src + k))

@[reducible, inline]

abbrev Cslib.WordRAM.ArrayCopy.src : Fin 7

Source base, destination base, length, index, temporary address, value, and one.

@[reducible, inline]

abbrev Cslib.WordRAM.ArrayCopy.dst : Fin 7

Destination base.

@[reducible, inline]

abbrev Cslib.WordRAM.ArrayCopy.len : Fin 7

Number of words.

@[reducible, inline]

abbrev Cslib.WordRAM.ArrayCopy.idx : Fin 7

Loop index.

@[reducible, inline]

abbrev Cslib.WordRAM.ArrayCopy.addr : Fin 7

Temporary address.

@[reducible, inline]

abbrev Cslib.WordRAM.ArrayCopy.value : Fin 7

Temporary value.

@[reducible, inline]

abbrev Cslib.WordRAM.ArrayCopy.one : Fin 7

Constant one.

def Cslib.WordRAM.ArrayCopy.body : Code Basis.standard 7

Five data instructions per copied word.

def Cslib.WordRAM.ArrayCopy.program : Code Basis.standard 7

A fixed copying program with all three parameters in registers.

theorem Cslib.WordRAM.ArrayCopy.exec {w : ℕ} (x : Data 7) (h1 : Fits w 1) (hs : Fits w (x.regs src + x.regs len)) (hd : Fits w (x.regs dst + x.regs len)) (hdisj : x.regs src + x.regs len ≤ x.regs dst) : ∃ (y : Data 7), ExecWithin w program x y (7 * x.regs len + 4) ∧ y.mem = copyPrefix x.mem (x.regs src) (x.regs dst) (x.regs len) ∧ y.regs src = x.regs src ∧ y.regs dst = x.regs dst ∧ y.regs len = x.regs len

Low-level structured copying charges register setup and all loop instructions, excluding the final halt. The one-past-end addresses must fit a word. Boundedness of the input memory and registers is a separate premise when using ExecWithin.bounded to obtain bounded-word execution.