Register frames for renamed native programs

Main results

• Code.preserves_rename_of_forall_ne: registers outside an embedded register bank are preserved without unfolding the subroutine's instruction graph.

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.