Sparse memory with an explicit default

A sparse memory is Mathlib's association list with a constant value type. Its keys are unique; writing a cell replaces its old binding. Storing the default value still records a binding, so cardinality measures stored addresses rather than the support of the denoted function.

Main definitions

• SparseMemory: an association list of distinct addresses and values.
• SparseMemory.read: total memory semantics, with an explicit default value.
• SparseMemory.entries: the ordinary pair representation used for binary encoding.

Main results

• SparseMemory.read_insert: a write denotes functional update.
• SparseMemory.length_insert_le: a write adds at most one stored address.
• SparseMemory.length_insert_of_mem: overwriting an address does not grow the store.

References

The representation and lookup/update correctness reuse Mathlib's AList implementation.

@[reducible, inline]

abbrev Cslib.GenericRAM.SparseMemory (Address : Type u_1) (Value : Type u_2) : Type (max u_1 u_2)

Finite memory with distinct stored addresses. The default value is supplied to read.

def Cslib.GenericRAM.SparseMemory.entries {Address : Type u_1} {Value : Type u_2} (s : SparseMemory Address Value) : List (Address × Value)

The finite bindings, viewed as ordinary pairs for encoding.

def Cslib.GenericRAM.SparseMemory.read {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] (default : Value) (a : Address) (s : SparseMemory Address Value) : Value

Read a stored address, or return the supplied default.

theorem Cslib.GenericRAM.SparseMemory.entries_injective {Address : Type u_1} {Value : Type u_2} : Function.Injective entries

The ordinary entries determine the association list.

@[simp]

theorem Cslib.GenericRAM.SparseMemory.entries_empty {Address : Type u_1} {Value : Type u_2} : ∅.entries = []

@[simp]

theorem Cslib.GenericRAM.SparseMemory.read_empty {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] (default : Value) (a : Address) : read default a ∅ = default

Default-valued memory requires no stored cells.

@[simp]

theorem Cslib.GenericRAM.SparseMemory.length_entries {Address : Type u_1} {Value : Type u_2} (s : SparseMemory Address Value) : s.entries.length = s.entries.length

The pair representation has the same number of bindings.

theorem Cslib.GenericRAM.SparseMemory.read_insert {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] (default : Value) (a : Address) (v : Value) (s : SparseMemory Address Value) : (fun (b : Address) => read default b (AList.insert a v s)) = Function.update (fun (b : Address) => read default b s) a v

Writing denotes functional update, including when the value equals the default.

theorem Cslib.GenericRAM.SparseMemory.length_insert_le {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] (a : Address) (v : Value) (s : SparseMemory Address Value) : (entries (AList.insert a v s)).length ≤ s.entries.length + 1

A write adds at most one distinct stored address.

theorem Cslib.GenericRAM.SparseMemory.length_insert_of_mem {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] (a : Address) (v : Value) (s : SparseMemory Address Value) (ha : a ∈ s) : (entries (AList.insert a v s)).length = s.entries.length

Replacing an existing address preserves the number of stored addresses.

theorem Cslib.GenericRAM.SparseMemory.entries_insert {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] (a : Address) (v : Value) (s : SparseMemory Address Value) : entries (AList.insert a v s) = (a, v) :: List.filter (fun (e : Address × Value) => decide (a ≠ e.fst)) s.entries

A write is a filter followed by one cons, on the encoded pair representation.

theorem Cslib.GenericRAM.SparseMemory.read_eq_find {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] (default : Value) (a : Address) (s : SparseMemory Address Value) : read default a s = (Option.map Prod.snd (List.find? (fun (e : Address × Value) => decide (a = e.fst)) s.entries)).getD default

Lookup is a first-match scan of the encoded pair representation.

theorem Cslib.GenericRAM.SparseMemory.mem_entries_insert {Address : Type u_1} {Value : Type u_2} [DecidableEq Address] {a : Address} {v : Value} {s : SparseMemory Address Value} {e : Address × Value} : e ∈ entries (AList.insert a v s) ↔ e = (a, v) ∨ e ∈ s.entries ∧ a ≠ e.fst

Each binding after a write is either the new binding or a surviving old binding.