Calling fixed code in a register bank

ExecWithin.call combines charged argument preparation, a proved routine in an injectively renamed register bank, and a charged continuation. The continuation receives the routine's entire postcondition and the unchanged registers outside its bank. The postcondition may describe both results and memory frames: register renaming leaves memory unchanged, so no separate memory transport proof is needed.

Unlike bounded-footprint data-structure contracts, this rule does not require every word in the caller state to fit or specify a finite footprint. It retains exactly the hypotheses of the supplied execution proof, including routines that tolerate arbitrary unused memory.

Main results

• Data.comap_set, Data.comap_set_of_forall_ne: transport register updates through a bank view.
• Exec.rename_post, ExecWithin.rename_post: retain postconditions and the caller register frame.
• ExecWithin.call: inline a fixed-code routine with additive instruction accounting.

These composition lemmas use the existing register-renaming semantics. Data.comap_set was extracted from the priority-queue calling convention by Renfei Zhou.

theorem Cslib.WordRAM.Data.comap_set {r s : ℕ} {f : Fin r → Fin s} (hf : Function.Injective f) (x : Data s) (i : Fin r) (v : ℕ) : comap f (x.set (f i) v) = (comap f x).set i v

Updating an embedded register updates the corresponding register in the bank view.

theorem Cslib.WordRAM.Data.comap_set_of_forall_ne {r s : ℕ} {f : Fin r → Fin s} (x : Data s) (i : Fin s) (v : ℕ) (hi : ∀ (j : Fin r), f j ≠ i) : comap f (x.set i v) = comap f x

A register update outside a bank leaves its entire view unchanged.

theorem Cslib.WordRAM.Exec.rename_post {B : Basis} {r s w t : ℕ} {f : Fin r → Fin s} (hf : Function.Injective f) {c : Code B r} {x : Data s} {Q : Data r → Prop} (h : ∃ (y : Data r), Exec w c (Data.comap f x) y t ∧ Q y) : ∃ (y : Data s), Exec w (Code.rename f c) x y t ∧ Q (Data.comap f y) ∧ ∀ (i : Fin s), (∀ (j : Fin r), f j ≠ i) → y.regs i = x.regs i

Run a routine in a larger register file, retaining its entire postcondition and the frame outside its bank. Renaming preserves the exact instruction count.

theorem Cslib.WordRAM.ExecWithin.rename_post {B : Basis} {r s w t : ℕ} {f : Fin r → Fin s} (hf : Function.Injective f) {c : Code B r} {x : Data s} {Q : Data r → Prop} (h : ∃ (y : Data r), ExecWithin w c (Data.comap f x) y t ∧ Q y) : ∃ (y : Data s), ExecWithin w (Code.rename f c) x y t ∧ Q (Data.comap f y) ∧ ∀ (i : Fin s), (∀ (j : Fin r), f j ≠ i) → y.regs i = x.regs i

Bounded-time version of Exec.rename_post.

theorem Cslib.WordRAM.ExecWithin.call {B : Basis} {r r' w tPrep tCall tCont : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) {prep cont : Code B r'} {callee : Code B r} {x a : Data r'} {Q : Data r → Prop} {R : Data r' → Prop} (hprep : ExecWithin w prep x a tPrep) (hcallee : ∃ (b : Data r), ExecWithin w callee (Data.comap f a) b tCall ∧ Q b) (hcont : ∀ (b : Data r'), Q (Data.comap f b) → (∀ (i : Fin r'), (∀ (j : Fin r), f j ≠ i) → b.regs i = a.regs i) → ∃ (y : Data r'), ExecWithin w cont b y tCont ∧ R y) : ∃ (y : Data r'), ExecWithin w (prep.seq ((Code.rename f callee).seq cont)) x y (tPrep + tCall + tCont) ∧ R y

Call a routine in an injective register bank and pass its postcondition and register frame to the continuation. Preparation, routine execution, and continuation are all charged; renaming itself emits no instruction. Any memory assertion in Q refers to the actual returned memory.