Word-addressed memory as a state-transition specification

Memory.spec w is a memory oracle: the interface through which a data-structure implementation reaches storage. Its state is the contents of every cell together with an allocation frontier. Every address below the frontier is allocated, and allocation hands out the block that starts at the frontier. The operations read a cell, write a cell, and allocate a block, either zeroed (alloc, charged per cell) or with its old contents (allocDirty, charged one unit).

Admissibility carries the preconditions a word RAM needs. Accessed addresses must be allocated, written values must fit a w-bit word, and the frontier after an allocation must fit. Under these preconditions the frontier and every cell keep fitting a word (WellFormed.step), so an allocated address fits too (WellFormed.fits_of_lt_frontier).

An implementation over this interface is an ordinary Memory.Prog program. Its correctness and its operation charges are proved against step and charge, without registers or instruction counts. charge is the memory-level currency; executing such a program on the word RAM is a separate step that exchanges it into instructions. Allocation never reuses addresses, as in Cslib.WordRAM.alloc, so blocks allocated at different times are disjoint (Cslib.WordRAM.Block.disjoint_of_le). A program reuses memory by keeping a block it allocated.

Main definitions

• Memory.State, Memory.Op, Memory.step, Memory.valid: cells and frontier, operations with their answers, the transition function and the admissibility preconditions.
• Memory.spec: the deterministic specification at word size w.
• Memory.charge: one unit per read, write and dirty allocation; k + 1 for a zeroed block of k cells.
• Memory.Prog, Memory.read, Memory.write, Memory.alloc, Memory.allocDirty: programs over the oracle and its four one-call programs.
• Memory.WellFormed: the frontier and all cell contents fit a w-bit word.
• Memory.State.init: the word RAM's input convention as a memory state.

Main results

• Memory.WellFormed.step, Memory.WellFormed.run: admissible operations preserve well-formedness.
• Memory.WellFormed.fits_of_lt_frontier: allocated addresses fit a word.
• Memory.one_le_charge: every operation costs at least one unit.
• Memory.frontier_le_step, Memory.frontier_le_run: the frontier never decreases.
• Memory.mem_step_of_lt_frontier: an operation changes an allocated cell only by writing it.
• Memory.wellFormed_init: the input convention is well formed.

structure Cslib.DataStructure.Memory.State : Type

Memory: the contents of every cell, and the frontier below which cells are allocated.

• mem : ℕ → ℕ

  The contents of the cell at each address.

• frontier : ℕ

  Every address below the frontier is allocated; the next block starts here.

theorem Cslib.DataStructure.Memory.State.ext {x y : State} (mem : x.mem = y.mem) (frontier : x.frontier = y.frontier) : x = y

theorem Cslib.DataStructure.Memory.State.ext_iff {x y : State} : x = y ↔ x.mem = y.mem ∧ x.frontier = y.frontier

inductive Cslib.DataStructure.Memory.Op : Type

Operations on memory. Addresses are words computed by the caller.

• read (addr : ℕ) : Op

  Read the cell at an address.

• write (addr value : ℕ) : Op

  Write a value to the cell at an address.

• alloc (count : ℕ) : Op

  Allocate count zeroed cells at the frontier and return their base address.

• allocDirty (count : ℕ) : Op

  Allocate count cells at the frontier without clearing them and return their base address.

@[instance_reducible]

instance Cslib.DataStructure.Memory.instDecidableEqOp : DecidableEq Op

def Cslib.DataStructure.Memory.instDecidableEqOp.decEq (x✝ x✝¹ : Op) : Decidable (x✝ = x✝¹)

@[reducible, inline]

abbrev Cslib.DataStructure.Memory.Op.Result : Op → Type

The answer type of each operation: a read and an allocation return a word.

def Cslib.DataStructure.Memory.step (s : State) (o : Op) : State × o.Result

The transition of each operation. An allocation returns the old frontier.

def Cslib.DataStructure.Memory.valid (w : ℕ) (s : State) : Op → Prop

Admissibility at word size w: accessed addresses are allocated, written values fit a word, and an allocation leaves a fitting frontier.

@[instance_reducible]

instance Cslib.DataStructure.Memory.instDecidableValid (w : ℕ) (s : State) (o : Op) : Decidable (valid w s o)

@[reducible, inline]

abbrev Cslib.DataStructure.Memory.spec (w : ℕ) : StateTransitionSpec

Word-addressed memory at word size w.

def Cslib.DataStructure.Memory.charge : State → Op → ℕ

The memory-level currency: one unit per read, write and dirty allocation, and k + 1 units for a zeroed block of k cells.

@[reducible, inline]

abbrev Cslib.DataStructure.Memory.Prog (α : Type) : Type

Programs over the memory oracle. They are the clients of Memory.spec w at every word size.

@[reducible, inline]

abbrev Cslib.DataStructure.Memory.read (a : ℕ) : Prog ℕ

Read the cell at address a.

@[reducible, inline]

abbrev Cslib.DataStructure.Memory.write (a v : ℕ) : Prog Unit

Write v to the cell at address a.

@[reducible, inline]

abbrev Cslib.DataStructure.Memory.alloc (k : ℕ) : Prog ℕ

Allocate k zeroed cells and return their base address.

@[reducible, inline]

abbrev Cslib.DataStructure.Memory.allocDirty (k : ℕ) : Prog ℕ

Allocate k cells without clearing them and return their base address.

@[simp]

theorem Cslib.DataStructure.Memory.step_read (s : State) (a : ℕ) : step s (Op.read a) = (s, s.mem a)

@[simp]

theorem Cslib.DataStructure.Memory.step_write (s : State) (a v : ℕ) : step s (Op.write a v) = ({ mem := Function.update s.mem a v, frontier := s.frontier }, ())

@[simp]

theorem Cslib.DataStructure.Memory.step_alloc (s : State) (k : ℕ) : step s (Op.alloc k) = ({ mem := WordRAM.clear s.mem s.frontier k, frontier := s.frontier + k }, s.frontier)

@[simp]

theorem Cslib.DataStructure.Memory.step_allocDirty (s : State) (k : ℕ) : step s (Op.allocDirty k) = ({ mem := s.mem, frontier := s.frontier + k }, s.frontier)

@[simp]

theorem Cslib.DataStructure.Memory.valid_read (w : ℕ) (s : State) (a : ℕ) : valid w s (Op.read a) ↔ a < s.frontier

@[simp]

theorem Cslib.DataStructure.Memory.valid_write (w : ℕ) (s : State) (a v : ℕ) : valid w s (Op.write a v) ↔ a < s.frontier ∧ WordRAM.Fits w v

@[simp]

theorem Cslib.DataStructure.Memory.valid_alloc (w : ℕ) (s : State) (k : ℕ) : valid w s (Op.alloc k) ↔ WordRAM.Fits w (s.frontier + k)

@[simp]

theorem Cslib.DataStructure.Memory.valid_allocDirty (w : ℕ) (s : State) (k : ℕ) : valid w s (Op.allocDirty k) ↔ WordRAM.Fits w (s.frontier + k)

@[simp]

theorem Cslib.DataStructure.Memory.charge_read (s : State) (a : ℕ) : charge s (Op.read a) = 1

@[simp]

theorem Cslib.DataStructure.Memory.charge_write (s : State) (a v : ℕ) : charge s (Op.write a v) = 1

@[simp]

theorem Cslib.DataStructure.Memory.charge_alloc (s : State) (k : ℕ) : charge s (Op.alloc k) = k + 1

@[simp]

theorem Cslib.DataStructure.Memory.charge_allocDirty (s : State) (k : ℕ) : charge s (Op.allocDirty k) = 1

theorem Cslib.DataStructure.Memory.one_le_charge (s : State) (o : Op) : 1 ≤ charge s o

Every memory operation costs at least one unit, so the number of operations, hence the glue run after them, is paid for by their charges.

@[instance_reducible]

instance Cslib.DataStructure.Memory.decidableValidHistory (w : ℕ) (s : State) (os : List Op) : Decidable ((spec w).ValidHistory s os)

Admissibility of a concrete history is decidable.

Frontier and frame

theorem Cslib.DataStructure.Memory.frontier_le_step (s : State) (o : Op) : s.frontier ≤ (step s o).1.frontier

No operation lowers the frontier.

theorem Cslib.DataStructure.Memory.frontier_le_run {w : ℕ} (s : State) (os : List Op) : s.frontier ≤ ((spec w).run s os).1.frontier

No sequence of operations lowers the frontier.

theorem Cslib.DataStructure.Memory.mem_step_of_lt_frontier (s : State) (o : Op) {a : ℕ} (ha : a < s.frontier) (hw : ∀ (v : ℕ), o ≠ Op.write a v) : (step s o).1.mem a = s.mem a

An operation changes an allocated cell only by writing to it. Allocation clears cells at or above the frontier only.

Word fit

structure Cslib.DataStructure.Memory.WellFormed (w : ℕ) (s : State) : Prop

The frontier and every cell fit a w-bit word. Admissible operations preserve this.

• frontier_fits : WordRAM.Fits w s.frontier

  The frontier fits a word, hence so does every allocated address.

• mem_fits (a : ℕ) : WordRAM.Fits w (s.mem a)

  Every cell holds a word.

theorem Cslib.DataStructure.Memory.WellFormed.fits_of_lt_frontier {w : ℕ} {s : State} (h : WellFormed w s) {a : ℕ} (ha : a < s.frontier) : WordRAM.Fits w a

Allocated addresses fit a word.

theorem Cslib.DataStructure.Memory.WellFormed.step {w : ℕ} {s : State} (h : WellFormed w s) {o : Op} (hv : valid w s o) : WellFormed w (Memory.step s o).1

Admissible operations preserve well-formedness.

theorem Cslib.DataStructure.Memory.WellFormed.run {w : ℕ} {s : State} (h : WellFormed w s) {os : List Op} (hv : (spec w).ValidHistory s os) : WellFormed w ((spec w).run s os).1

Admissible histories preserve well-formedness.

The input convention

def Cslib.DataStructure.Memory.State.init (input : List ℕ) : State

The word RAM's input convention (Cslib.WordRAM.Data.init) as a memory state: the input length at address 0, the input words at addresses 1, …, n, and everything up to the input allocated.

theorem Cslib.DataStructure.Memory.wellFormed_init {w : ℕ} {input : List ℕ} (hin : WordRAM.InputFits w input) (hf : WordRAM.Fits w (input.length + 1)) : WellFormed w (State.init input)

The input convention is well formed when the input and its frontier fit a word.