Finite semantic port of Miri's tree_borrows/unimap.rs. UniKeyMap keeps the source's reusable u32 index pool; UniValMap keeps optional values in an array indexed by the same value. Large collections are represented by Lean arrays, but all observable insertion/removal behavior is explicit.

structure Miri.TreeBorrows.UniIndex : Type

• idx : UInt32

def Miri.TreeBorrows.instDecidableEqUniIndex.decEq (x✝ x✝¹ : UniIndex) : Decidable (x✝ = x✝¹)

Equations

• Miri.TreeBorrows.instDecidableEqUniIndex.decEq { idx := a } { idx := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqUniIndex : DecidableEq UniIndex

Equations

• Miri.TreeBorrows.instDecidableEqUniIndex = Miri.TreeBorrows.instDecidableEqUniIndex.decEq

@[instance_reducible]

instance Miri.TreeBorrows.instReprUniIndex : Repr UniIndex

Equations

• Miri.TreeBorrows.instReprUniIndex = { reprPrec := Miri.TreeBorrows.instReprUniIndex.repr }

def Miri.TreeBorrows.instReprUniIndex.repr : UniIndex → Nat → Std.Format

Equations

• Miri.TreeBorrows.instReprUniIndex.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "idx" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.idx)).group) " }"

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedUniIndex : Inhabited UniIndex

Equations

• Miri.TreeBorrows.instInhabitedUniIndex = { default := Miri.TreeBorrows.instInhabitedUniIndex.default }

def Miri.TreeBorrows.UniIndex.toNat (index : UniIndex) : Nat

Equations

• index.toNat = index.idx.toNat

def Miri.TreeBorrows.UniIndex.ofNat? (value : Nat) : Option UniIndex

Equations

• Miri.TreeBorrows.UniIndex.ofNat? value = if value ≤ 4294967295 then some { idx := UInt32.ofNat value } else none

inductive Miri.TreeBorrows.UniKeyMapError : Type

• IndexSpaceExhausted (active : Nat) : UniKeyMapError

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqUniKeyMapError : DecidableEq UniKeyMapError

Equations

• Miri.TreeBorrows.instDecidableEqUniKeyMapError = Miri.TreeBorrows.instDecidableEqUniKeyMapError.decEq

def Miri.TreeBorrows.instDecidableEqUniKeyMapError.decEq (x✝ x✝¹ : UniKeyMapError) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.instReprUniKeyMapError.repr : UniKeyMapError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprUniKeyMapError : Repr UniKeyMapError

Equations

• Miri.TreeBorrows.instReprUniKeyMapError = { reprPrec := Miri.TreeBorrows.instReprUniKeyMapError.repr }

structure Miri.TreeBorrows.UniKeyMap (α : Type) : Type

Source UniKeyMap<K> from key to reusable index.

• mapping : Array (α × UniIndex)
• deassigned : Array UniIndex

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqUniKeyMap {α✝ : Type} [DecidableEq α✝] : DecidableEq (UniKeyMap α✝)

Equations

• Miri.TreeBorrows.instDecidableEqUniKeyMap = Miri.TreeBorrows.instDecidableEqUniKeyMap.decEq

def Miri.TreeBorrows.instDecidableEqUniKeyMap.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : UniKeyMap α✝) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.instReprUniKeyMap.repr {α✝ : Type} [Repr α✝] : UniKeyMap α✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprUniKeyMap {α✝ : Type} [Repr α✝] : Repr (UniKeyMap α✝)

Equations

• Miri.TreeBorrows.instReprUniKeyMap = { reprPrec := Miri.TreeBorrows.instReprUniKeyMap.repr }

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedUniKeyMap {a✝ : Type} : Inhabited (UniKeyMap a✝)

Equations

• Miri.TreeBorrows.instInhabitedUniKeyMap = { default := Miri.TreeBorrows.instInhabitedUniKeyMap.default }

inductive Miri.TreeBorrows.UniKeyMapInsertResult (α : Type) : Type

• Inserted {α : Type} (map : UniKeyMap α) (index : UniIndex) : UniKeyMapInsertResult α
• DuplicateKeyAfterReplacement {α : Type} (map : UniKeyMap α) (index : UniIndex) : UniKeyMapInsertResult α
• Error {α : Type} (map : UniKeyMap α) (error : UniKeyMapError) : UniKeyMapInsertResult α

@[instance_reducible]

instance Miri.TreeBorrows.instReprUniKeyMapInsertResult {α✝ : Type} [Repr α✝] : Repr (UniKeyMapInsertResult α✝)

Equations

• Miri.TreeBorrows.instReprUniKeyMapInsertResult = { reprPrec := Miri.TreeBorrows.instReprUniKeyMapInsertResult.repr }

def Miri.TreeBorrows.instReprUniKeyMapInsertResult.repr {α✝ : Type} [Repr α✝] : UniKeyMapInsertResult α✝ → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.UniKeyMap.get {α : Type} [BEq α] (map : UniKeyMap α) (key : α) : Option UniIndex

Equations

• map.get key = Option.map Prod.snd (Array.find? (fun (entry : α × Miri.TreeBorrows.UniIndex) => entry.fst == key) map.mapping)

def Miri.TreeBorrows.UniKeyMap.containsKey {α : Type} [BEq α] (map : UniKeyMap α) (key : α) : Bool

Equations

• map.containsKey key = (map.get key).isSome

def Miri.TreeBorrows.UniKeyMap.insert {α : Type} [BEq α] (map : UniKeyMap α) (key : α) : UniKeyMapInsertResult α

Source insertion pops a reusable index first, otherwise converts the current active map length to u32. A duplicate key preserves Rust HashMap's replacement mutation before returning the source panic as an explicit result.

Equations

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

def Miri.TreeBorrows.UniKeyMap.getOrInsert {α : Type} [BEq α] (map : UniKeyMap α) (key : α) : UniKeyMapInsertResult α

Equations

• map.getOrInsert key = match map.get key with | some index => Miri.TreeBorrows.UniKeyMapInsertResult.Inserted map index | none => map.insert key

def Miri.TreeBorrows.UniKeyMap.remove {α : Type} [BEq α] (map : UniKeyMap α) (key : α) : UniKeyMap α

Equations

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

def Miri.TreeBorrows.UniKeyMap.size {α : Type} (map : UniKeyMap α) : Nat

Equations

• map.size = map.mapping.size

structure Miri.TreeBorrows.UniValMap (α : Type) : Type

Source UniValMap<V> as a vector of optional values.

• data : Array (Option α)

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqUniValMap {α✝ : Type} [DecidableEq α✝] : DecidableEq (UniValMap α✝)

Equations

• Miri.TreeBorrows.instDecidableEqUniValMap = Miri.TreeBorrows.instDecidableEqUniValMap.decEq

def Miri.TreeBorrows.instDecidableEqUniValMap.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : UniValMap α✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.TreeBorrows.instDecidableEqUniValMap.decEq { data := a } { data := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.TreeBorrows.instReprUniValMap.repr {α✝ : Type} [Repr α✝] : UniValMap α✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprUniValMap {α✝ : Type} [Repr α✝] : Repr (UniValMap α✝)

Equations

• Miri.TreeBorrows.instReprUniValMap = { reprPrec := Miri.TreeBorrows.instReprUniValMap.repr }

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedUniValMap {a✝ : Type} : Inhabited (UniValMap a✝)

Equations

• Miri.TreeBorrows.instInhabitedUniValMap = { default := Miri.TreeBorrows.instInhabitedUniValMap.default }

def Miri.TreeBorrows.UniValMap.extendTo {α : Type u_1} (data : Array (Option α)) (length : Nat) : Array (Option α)

Equations

• Miri.TreeBorrows.UniValMap.extendTo data length = data ++ Array.replicate (length - data.size) none

def Miri.TreeBorrows.UniValMap.containsIdx {α : Type} (map : UniValMap α) (index : UniIndex) : Bool

Equations

• map.containsIdx index = match map.data[index.toNat]? with | some value => value.isSome | none => false

def Miri.TreeBorrows.UniValMap.insert {α : Type} (map : UniValMap α) (index : UniIndex) (value : α) : UniValMap α

Source insert permanently overwrites any old value at the index.

Equations

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

def Miri.TreeBorrows.UniValMap.get {α : Type} (map : UniValMap α) (index : UniIndex) : Option α

Equations

• map.get index = match map.data[index.toNat]? with | some value => value | none => none

def Miri.TreeBorrows.UniValMap.remove {α : Type} (map : UniValMap α) (index : UniIndex) : UniValMap α

Equations

• map.remove index = if h : index.toNat < map.data.size then { data := map.data.set index.toNat none h } else map

def Miri.TreeBorrows.UniValMap.trimTrailingNone {α : Type} (map : UniValMap α) : UniValMap α

Canonical representation for source UniValMap::equivalent equality. Rust treats trailing None slots as absent when comparing maps; trimming them before Lean's structural range-map comparison preserves that behavior.

Equations

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

def Miri.TreeBorrows.UniValMap.isEmpty {α : Type} (map : UniValMap α) : Bool

Equations

• map.isEmpty = map.data.all Option.isNone

def Miri.TreeBorrows.UniValMap.entries {α : Type} (map : UniValMap α) : Array (UniIndex × α)

Equations

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

def Miri.TreeBorrows.UniValMap.orInsert {α : Type} (map : UniValMap α) (index : UniIndex) (default : α) : UniValMap α × α

Equations

• map.orInsert index default = match map.get index with | some value => (map, value) | none => (map.insert index default, default)

def Miri.TreeBorrows.UniValMap.size {α : Type} (map : UniValMap α) : Nat

Equations

• map.size = map.data.size