Appending one word to a realized memory block

Main results

• Block.Realizes.snoc: the actual one-cell memory update realizes Fin.snoc of the prior finite array. This is a memory identity; a caller must separately charge its store instruction.

This narrow topic module keeps the Fin.snoc dependency and append-specific proof out of Allocation. Clients of core allocation then avoid an interface change and rebuild when the append API changes; consumers import this module alongside Block.Realizes.update as needed.

theorem Cslib.WordRAM.Block.Realizes.snoc {base n : ℕ} {mem : ℕ → ℕ} {v : Fin n → ℕ} (h : { base := base, length := n }.Realizes mem v) (a : ℕ) : { base := base, length := n + 1 }.Realizes (Function.update mem (base + n) a) (Fin.snoc v a)

Appending a value at the first cell after an array realizes the extended finite function.