List-valued block assertions

These are specializations of Block.Realizes, not an additional memory model.

Main definitions

• Block.HoldsList: a contiguous block realizes a list.

Main results

• Block.HoldsList.append_one: a store immediately after a list appends one element.
• Block.HoldsList.frame: writes outside the block preserve its list.
• Block.holdsList_append_iff: concatenation is equivalent to two adjacent represented blocks.

@[reducible, inline]

abbrev Cslib.WordRAM.Block.HoldsList (base : ℕ) (xs : List ℕ) (mem : ℕ → ℕ) : Prop

The block starting at base realizes exactly the entries of xs.

theorem Cslib.WordRAM.Block.HoldsList.get {base : ℕ} {xs : List ℕ} {mem : ℕ → ℕ} (h : HoldsList base xs mem) (i : ℕ) (hi : i < xs.length) : mem (base + i) = xs[i]

Read an entry of a represented list.

theorem Cslib.WordRAM.Block.holdsList_nil (base : ℕ) (mem : ℕ → ℕ) : HoldsList base [] mem

An empty list imposes no memory constraints.

theorem Cslib.WordRAM.Block.HoldsList.take {base : ℕ} {xs : List ℕ} {mem : ℕ → ℕ} (h : HoldsList base xs mem) (k : ℕ) : HoldsList base (List.take k xs) mem

The prefix of a represented list is represented in the same memory.

theorem Cslib.WordRAM.Block.HoldsList.append_one {base : ℕ} {xs : List ℕ} {mem : ℕ → ℕ} (h : HoldsList base xs mem) (v : ℕ) : HoldsList base (xs ++ [v]) (Function.update mem (base + xs.length) v)

A store immediately following a represented list appends an element.

theorem Cslib.WordRAM.Block.HoldsList.frame {base : ℕ} {xs : List ℕ} {mem mem' : ℕ → ℕ} (h : HoldsList base xs mem) (heq : ∀ (a : ℕ), base ≤ a → a < base + xs.length → mem' a = mem a) : HoldsList base xs mem'

Writes outside the represented block preserve the list.

theorem Cslib.WordRAM.Block.HoldsList.append {base : ℕ} {xs ys : List ℕ} {mem : ℕ → ℕ} (h : HoldsList base xs mem) (h' : HoldsList (base + xs.length) ys mem) : HoldsList base (xs ++ ys) mem

Append two adjacent represented blocks.

theorem Cslib.WordRAM.Block.holdsList_append_iff {base : ℕ} {xs ys : List ℕ} {mem : ℕ → ℕ} : HoldsList base (xs ++ ys) mem ↔ HoldsList base xs mem ∧ HoldsList (base + xs.length) ys mem

A represented concatenation consists of two adjacent represented blocks.