Register frames for renamed native programs

Main results

• Code.preserves_rename_of_forall: a renamed routine preserves a register when the routine preserves every register renamed to it.
• Code.preserves_rename: injective renaming retains a register preservation guarantee.
• Code.preserves_rename_of_forall_ne: registers outside an embedded register bank are preserved without unfolding the subroutine's instruction graph.
• Code.preserves_rename_of_offset: a contiguous bank preserves registers outside its interval.
• Data.extend_regs_of_eq, Data.extend_regs_of_notMem, Data.extend_regs_of_forall_ne, Data.extend_castLE_regs_of_le: read registers inside or outside an extended bank.
• Data.extend_mem: an extended state has the actual callee memory.

The range-based register equation and memory projection come from Samuel Schlesinger and Renfei Zhou's subroutine infrastructure.

theorem Cslib.WordRAM.Code.preserves_rename_of_forall {B : Basis} {r s : ℕ} {f : Fin r → Fin s} {i : Fin s} {c : Code B r} (h : ∀ (j : Fin r), f j = i → Preserves j c) : Preserves i (rename f c)

A renamed routine preserves register i when the routine preserves every register that the renaming sends to i.

theorem Cslib.WordRAM.Code.preserves_rename {B : Basis} {r s : ℕ} {f : Fin r → Fin s} (hf : Function.Injective f) {i : Fin r} {c : Code B r} (h : Preserves i c) : Preserves (f i) (rename f c)

An injectively embedded routine preserves the corresponding embedded register.

theorem Cslib.WordRAM.Data.extend_regs_of_eq {r s : ℕ} {f : Fin r → Fin s} (hf : Function.Injective f) (y : Data r) (x : Data s) (i : Fin r) (j : Fin s) (h : f i = j) : (extend f y x).regs j = y.regs i

Read a register in the callee's injective bank.

theorem Cslib.WordRAM.Data.extend_regs_of_notMem {r r' : ℕ} {f : Fin r → Fin r'} (y : Data r) (x : Data r') {j : Fin r'} (hj : j ∉ Set.range f) : (extend f y x).regs j = x.regs j

Registers outside Set.range f retain their caller values under Data.extend.

theorem Cslib.WordRAM.Data.extend_regs_of_forall_ne {r s : ℕ} {f : Fin r → Fin s} (y : Data r) (x : Data s) (i : Fin s) (hi : ∀ (j : Fin r), f j ≠ i) : (extend f y x).regs i = x.regs i

Read a caller register outside the callee's bank.

theorem Cslib.WordRAM.Data.extend_castLE_regs_of_le {r s : ℕ} {hrs : r ≤ s} (y : Data r) (x : Data s) (i : Fin s) (hi : r ≤ ↑i) : (extend (Fin.castLE hrs) y x).regs i = x.regs i

Read a caller register above a Fin.castLE low-register bank.

@[simp]

theorem Cslib.WordRAM.Data.extend_mem {r r' : ℕ} (f : Fin r → Fin r') (y : Data r) (x : Data r') : (extend f y x).mem = y.mem

Extending registers retains the actual returned memory, including callee writes.

theorem Cslib.WordRAM.Code.preserves_rename_of_forall_ne {B : Basis} {r r' : ℕ} (c : Code B r) (f : Fin r → Fin r') (i : Fin r') (hi : ∀ (j : Fin r), f j ≠ i) : Preserves i (rename f c)

A renamed subroutine cannot write a register outside the image of its register embedding. This generalizes the former private framing rule of the fusion-node register banks.

theorem Cslib.WordRAM.Code.preserves_rename_of_offset {B : Basis} {r s offset : ℕ} (c : Code B r) (f : Fin r → Fin s) (hf : ∀ (j : Fin r), ↑(f j) = offset + ↑j) (i : Fin s) (hi : ↑i < offset ∨ offset + r ≤ ↑i) : Preserves i (rename f c)

A subroutine placed at a fixed register offset preserves every register outside its bank. The value equation also covers enumerated embeddings once their offset is checked.