Copying arrays on the word RAM

The seven-register copy routine charges every address calculation, load, store, increment, and loop test. Source and destination may be disjoint in either order or equal. It is a fixed program: neither the length nor either address is baked into the code.

Main definitions

• Cslib.WordRAM.ArrayCopy.src, Cslib.WordRAM.ArrayCopy.dst, Cslib.WordRAM.ArrayCopy.len, Cslib.WordRAM.ArrayCopy.idx, Cslib.WordRAM.ArrayCopy.addr, Cslib.WordRAM.ArrayCopy.value, Cslib.WordRAM.ArrayCopy.one: the seven registers of the copy routine.
• Cslib.WordRAM.ArrayCopy.body, Cslib.WordRAM.ArrayCopy.program: single-word loop body and full copying program 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.
• Cslib.WordRAM.ArrayCopy.exec_of_separated_or_eq: the same native program also supports disjoint blocks in the reverse address order or identical source and 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 destination block.

@[simp]

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

Copying zero words leaves memory unchanged.

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

Reading within the copied destination block returns the corresponding source word.

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

Memory cells outside [dst, dst + k) are unchanged by copyPrefix.

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_of_separated_or_eq {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 ∨ x.regs dst + x.regs len ≤ x.regs src ∨ x.regs src = 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.

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

Forward copying between disjoint arrays, retaining the original calling convention.