Ordered metadata arrays with an exact key-to-row index.

The index stores only row positions, never values. Payloads therefore occur once in the ordered rows. A certificate ties each index to those exact rows; constructors and mutations rebuild both together. Iteration retains source array order and duplicate-key lookup semantics.

structure Miri.Memory.KeyedArray (K V : Type) (keyFn : V → K) [BEq K] [Hashable K] : Type

• keys : Array K
• rows : Array V
• indexState : Nat × Std.HashMap K (Array Nat)
• exact : indexState self = canonicalIndex (keys self)
• aligned : (keys self).size = (rows self).size
• keysMatchRows : keys self = Array.map keyFn (rows self)

def Miri.Memory.KeyedArray.empty {K V : Type} [BEq K] [Hashable K] (keyFn : V → K) : KeyedArray K V keyFn

Equations

• Miri.Memory.KeyedArray.empty keyFn = { keys := #[], rows := #[], indexState := (0, ∅), exact := ⋯, aligned := ⋯, keysMatchRows := ⋯ }

def Miri.Memory.KeyedArray.ofArray {K V : Type} [BEq K] [Hashable K] (keyFn : V → K) (rows : Array V) : KeyedArray K V keyFn

Equations

• One or more equations did not get rendered due to their size.

def Miri.Memory.KeyedArray.keyOf {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (_table : KeyedArray K V keyFn) : V → K

Equations

• _table.keyOf = keyFn

def Miri.Memory.KeyedArray.toArray {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) : Array V

Equations

• table.toArray = Miri.Memory.KeyedArray.rows✝ table

def Miri.Memory.KeyedArray.toPairs {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) : Array (K × V)

Equations

• table.toPairs = (Miri.Memory.KeyedArray.keys✝ table).zip (Miri.Memory.KeyedArray.rows✝ table)

def Miri.Memory.KeyedArray.find? {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (key : K) : Option V

Equations

• table.find? key = do let indices ← (Miri.Memory.KeyedArray.indexState✝ table).snd.get? key let rowIndex ← indices[0]? (Miri.Memory.KeyedArray.rows✝ table)[rowIndex]?

def Miri.Memory.KeyedArray.any? {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (key : K) (p : V → Bool) : Bool

Test every same-key row, preserving the historical Array.any behavior for deliberately constructed duplicate metadata keys.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Memory.KeyedArray.valuesFor {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (key : K) : Array V

Equations

• One or more equations did not get rendered due to their size.

def Miri.Memory.KeyedArray.contains {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (key : K) : Bool

Equations

• table.contains key = (Miri.Memory.KeyedArray.indexState✝ table).snd.contains key

def Miri.Memory.KeyedArray.isEmpty {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) : Bool

Equations

• table.isEmpty = (Miri.Memory.KeyedArray.rows✝ table).isEmpty

def Miri.Memory.KeyedArray.size {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) : Nat

Equations

• table.size = (Miri.Memory.KeyedArray.rows✝ table).size

def Miri.Memory.KeyedArray.push {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (value : V) : KeyedArray K V keyFn

Append while preserving first-row lookup and source iteration order.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Memory.KeyedArray.filter {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (keep : K → V → Bool) : KeyedArray K V keyFn

Filter and reindex a cold metadata table.

Equations

• table.filter keep = Miri.Memory.KeyedArray.ofArray keyFn (Array.filter (fun (row : V) => keep (keyFn row) row) (Miri.Memory.KeyedArray.rows✝ table))

def Miri.Memory.KeyedArray.mapValues {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (f : V → V) : KeyedArray K V keyFn

Map rows in source order and rebuild the index, allowing key changes.

Equations

• table.mapValues f = Miri.Memory.KeyedArray.ofArray keyFn (Array.map f (Miri.Memory.KeyedArray.rows✝ table))

def Miri.Memory.KeyedArray.mapValuesChecked {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} [DecidableEq K] (table : KeyedArray K V keyFn) (f : V → V) : KeyedArray K V keyFn

Map row payloads, reusing the certified index when the mapped rows retain the exact key sequence. A map that changes keys falls back to a full reindex, so this preserves the unrestricted semantics of mapValues.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Memory.KeyedArray.modifyAt {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (i : Nat) (f : V → V) (preserves : ∀ (row : V), keyFn (f row) = keyFn row) : KeyedArray K V keyFn

Apply a key-preserving row update while retaining the certified key sequence and index. The proof obligation is local to the update function.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Memory.KeyedArray.mapValuesForKey {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (key : K) (f : V → V) (preserves : ∀ (row : V), keyFn (f row) = keyFn row) : KeyedArray K V keyFn

Update every row at a key's certified positions, retaining the existing index.

Equations

• One or more equations did not get rendered due to their size.

theorem Miri.Memory.KeyedArray.contains_rows {K V : Type} [BEq K] [Hashable K] {keyFn : V → K} [LawfulBEq K] [LawfulHashable K] (table : KeyedArray K V keyFn) (key : K) : table.contains key = (Array.map keyFn table.toArray).contains key

The certified hash index contains precisely the keys of current rows.

theorem Miri.Memory.KeyedArray.find_of_contains {K V : Type} [BEq K] [Hashable K] [LawfulBEq K] [LawfulHashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (key : K) (present : table.contains key = true) : ∃ (row : V), table.find? key = some row

A certified present key always selects a real row, including duplicate keys.

theorem Miri.Memory.KeyedArray.contains_false_of_find_none {K V : Type} [BEq K] [Hashable K] [LawfulBEq K] [LawfulHashable K] {keyFn : V → K} (table : KeyedArray K V keyFn) (key : K) (missing : table.find? key = none) : table.contains key = false

Missing lookup excludes index membership, without an additional coherence law.