Native programs in a caller-owned memory window

MemoryWindow.compile translates standard native code to use a runtime memory base. Three additional registers hold the base, the source word modulus and an address temporary. A load executes an addition, a load and a remainder; a store executes an addition and a store. Other instructions and all branch decisions retain the source register values.

MemoryWindow.view clips memory words to the source width. Consequently arbitrary dirty memory in the caller's window is allowed: no bulk initialization or copying of that window is implicit in the translation. The view is only a relation between ordinary native data, not a new machine or execution semantics. Source executions must still be established using WordRAM.Exec.

This compiler is original native program work. It does not supply an algorithm, an execution certificate or a bound for any source program.

def Cslib.WordRAM.MemoryWindow.Reg.base {r : ℕ} : Fin (r + 3)

Runtime address of source memory cell zero.

def Cslib.WordRAM.MemoryWindow.Reg.modulus {r : ℕ} : Fin (r + 3)

Runtime value 2^w for the source word width w.

def Cslib.WordRAM.MemoryWindow.Reg.address {r : ℕ} : Fin (r + 3)

Temporary absolute address used by translated loads and stores.

def Cslib.WordRAM.MemoryWindow.compileOp {r : ℕ} : Op Basis.standard r → Code Basis.standard (r + 3)

One source instruction with actual address additions and load normalization.

def Cslib.WordRAM.MemoryWindow.compile {r : ℕ} : Code Basis.standard r → Code Basis.standard (r + 3)

Rebase all memory accesses, retaining ordinary native branching and loop control.

def Cslib.WordRAM.MemoryWindow.view {r : ℕ} (w b : ℕ) (x : Data (r + 3)) : Data r

Source data represented by a target register bank and clipped, shifted memory.

structure Cslib.WordRAM.MemoryWindow.Matches {r : ℕ} (w b : ℕ) (x : Data r) (y : Data (r + 3)) : Prop

Ordinary value equalities relating source and target native data.

• view_eq : view w b y = x

  The source register bank and clipped memory agree.

• base_eq : y.regs Reg.base = b

  The base register has the chosen runtime address.

• modulus_eq : y.regs Reg.modulus = 2 ^ w

  The modulus register has the source word modulus.

theorem Cslib.WordRAM.MemoryWindow.size_compileOp {r : ℕ} (o : Op Basis.standard r) : (compileOp o).size ≤ 3

The compiler expands a flat instruction into at most three instructions.

theorem Cslib.WordRAM.MemoryWindow.size_compile {r : ℕ} (c : Code Basis.standard r) : (compile c).size ≤ 3 * c.size

Branches and loop overhead also satisfy the factor-three code-size bound.

theorem Cslib.WordRAM.MemoryWindow.readsWidth_compileOp {r : ℕ} (o : Op Basis.standard r) : (compileOp o).ReadsWidth ↔ o.ReadsWidth

Memory rebasing introduces no reads of the physical word width.

theorem Cslib.WordRAM.MemoryWindow.readsWidth_compile {r : ℕ} (c : Code Basis.standard r) : (compile c).ReadsWidth ↔ c.ReadsWidth

The compiled code reads the word width exactly when the source does.

theorem Cslib.WordRAM.MemoryWindow.Matches.regs {r w b : ℕ} {x : Data r} {y : Data (r + 3)} (h : Matches w b x y) (i : Fin r) : y.regs (Fin.castAdd 3 i) = x.regs i

Matching source registers have their exact target-bank values.

theorem Cslib.WordRAM.MemoryWindow.Matches.mem {r w b : ℕ} {x : Data r} {y : Data (r + 3)} (h : Matches w b x y) (a : ℕ) : y.mem (b + a) % 2 ^ w = x.mem a

Matching source memory has the clipped target word at its shifted address.

theorem Cslib.WordRAM.MemoryWindow.exec_compileOp {r w W b : ℕ} {o : Op Basis.standard r} {x x' : Data r} {y : Data (r + 3)} (ho : ¬o.ReadsWidth) (he : Op.eval w o x = some x') (hx : Data.Bounded w x) (hxy : Matches w b x y) (hw : w ≤ W) (hfit : Fits W (b + 2 ^ w)) : ∃ (y' : Data (r + 3)), ExecWithin W (compileOp o) y y' 3 ∧ Matches w b x' y' ∧ ∀ (a : ℕ), a < b ∨ b + 2 ^ w ≤ a → y'.mem a = y.mem a

A translated source instruction has actual native execution within three instructions. All source addresses fit the bounded source word, so the only writes are inside the runtime window. Dirty words are normalized by the translated load itself.

theorem Cslib.WordRAM.MemoryWindow.view_bounded {r : ℕ} (w b : ℕ) (y : Data (r + 3)) (hregs : ∀ (i : Fin r), Fits w (y.regs (Fin.castAdd 3 i))) : Data.Bounded w (view w b y)

Clipped memory is source-word bounded whenever the represented register bank is bounded. No condition is imposed on the unnormalized physical memory words.

theorem Cslib.WordRAM.MemoryWindow.exec {r w W b : ℕ} {c : Code Basis.standard r} {x x' : Data r} {n : ℕ} (he : Exec w c x x' n) (hc : ¬c.ReadsWidth) (hx : Data.Bounded w x) {y : Data (r + 3)} (hxy : Matches w b x y) (hw : w ≤ W) (hfit : Fits W (b + 2 ^ w)) : ∃ (y' : Data (r + 3)), ExecWithin W (compile c) y y' (3 * n) ∧ Matches w b x' y' ∧ ∀ (a : ℕ), a < b ∨ b + 2 ^ w ≤ a → y'.mem a = y.mem a

Every actual bounded deterministic source execution gives an actual target execution with at most three times its charged instructions. The base and modulus survive, source registers and clipped memory agree, and the entire caller memory outside the reserved window survives. This is a compiler correctness rule over the existing native Exec, not an assumed execution contract for an algorithm.

theorem Cslib.WordRAM.MemoryWindow.execWithin {r w W b T : ℕ} {c : Code Basis.standard r} {x x' : Data r} (he : ExecWithin w c x x' T) (hc : ¬c.ReadsWidth) (hx : Data.Bounded w x) {y : Data (r + 3)} (hxy : Matches w b x y) (hw : w ≤ W) (hfit : Fits W (b + 2 ^ w)) : ∃ (y' : Data (r + 3)), ExecWithin W (compile c) y y' (3 * T) ∧ Matches w b x' y' ∧ ∀ (a : ℕ), a < b ∨ b + 2 ^ w ≤ a → y'.mem a = y.mem a

The bounded-time form of memory-window compiler correctness.

def Cslib.WordRAM.MemoryWindow.normalizeBankList {r : ℕ} : List (Fin r) → Code Basis.standard (r + 3)

Normalize a static list of source registers, retaining the runtime base and modulus.

def Cslib.WordRAM.MemoryWindow.normalizeRegisters (r : ℕ) : Code Basis.standard (r + 3)

A fixed instruction sequence normalizing each source register once. The final self-copy also makes the zero-register case an ordinary nonempty native program.

theorem Cslib.WordRAM.MemoryWindow.exec_normalizeRegisters {r w W b : ℕ} (x : Data (r + 3)) (hb : x.regs Reg.base = b) (hm : x.regs Reg.modulus = 2 ^ w) (hw : w ≤ W) : ∃ (y : Data (r + 3)), ExecWithin W (normalizeRegisters r) x y (r + 1) ∧ y.mem = x.mem ∧ Matches w b (view w b y) y ∧ Data.Bounded w (view w b y) ∧ ∀ (j : Fin r), y.regs (Fin.castAdd 3 j) = x.regs (Fin.castAdd 3 j) % 2 ^ w

Actual register normalization supplies a bounded source view without clearing any memory. The base, modulus and every caller memory cell are preserved.