A checked Lean port of Miri's allocation-object range map.

@[reducible, inline]

abbrev Miri.DataStructures.Position : Type

Equations

• Miri.DataStructures.Position = Nat

structure Miri.DataStructures.PositionRange : Type

The half-open vector interval returned by an imperfect access classification.

• start : Position
• stop : Position

def Miri.DataStructures.instDecidableEqPositionRange.decEq (x✝ x✝¹ : PositionRange) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqPositionRange : DecidableEq PositionRange

Equations

• Miri.DataStructures.instDecidableEqPositionRange = Miri.DataStructures.instDecidableEqPositionRange.decEq

@[instance_reducible]

instance Miri.DataStructures.instReprPositionRange : Repr PositionRange

Equations

• Miri.DataStructures.instReprPositionRange = { reprPrec := Miri.DataStructures.instReprPositionRange.repr }

def Miri.DataStructures.instReprPositionRange.repr : PositionRange → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instInhabitedPositionRange : Inhabited PositionRange

Equations

• Miri.DataStructures.instInhabitedPositionRange = { default := Miri.DataStructures.instInhabitedPositionRange.default }

inductive Miri.DataStructures.AccessType : Type

The three classifications returned by RangeObjectMap::access_type.

• perfectlyOverlapping (position : Position) : AccessType
• empty (position : Position) : AccessType
• imperfectlyOverlapping (positions : PositionRange) : AccessType

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqAccessType : DecidableEq AccessType

Equations

• Miri.DataStructures.instDecidableEqAccessType = Miri.DataStructures.instDecidableEqAccessType.decEq

def Miri.DataStructures.instDecidableEqAccessType.decEq (x✝ x✝¹ : AccessType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.DataStructures.instDecidableEqAccessType.decEq (Miri.DataStructures.AccessType.perfectlyOverlapping position) (Miri.DataStructures.AccessType.empty position_1) = isFalse ⋯
• Miri.DataStructures.instDecidableEqAccessType.decEq (Miri.DataStructures.AccessType.perfectlyOverlapping position) (Miri.DataStructures.AccessType.imperfectlyOverlapping positions) = isFalse ⋯
• Miri.DataStructures.instDecidableEqAccessType.decEq (Miri.DataStructures.AccessType.empty position) (Miri.DataStructures.AccessType.perfectlyOverlapping position_1) = isFalse ⋯
• Miri.DataStructures.instDecidableEqAccessType.decEq (Miri.DataStructures.AccessType.empty a) (Miri.DataStructures.AccessType.empty b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.DataStructures.instDecidableEqAccessType.decEq (Miri.DataStructures.AccessType.empty position) (Miri.DataStructures.AccessType.imperfectlyOverlapping positions) = isFalse ⋯
• Miri.DataStructures.instDecidableEqAccessType.decEq (Miri.DataStructures.AccessType.imperfectlyOverlapping positions) (Miri.DataStructures.AccessType.perfectlyOverlapping position) = isFalse ⋯
• Miri.DataStructures.instDecidableEqAccessType.decEq (Miri.DataStructures.AccessType.imperfectlyOverlapping positions) (Miri.DataStructures.AccessType.empty position) = isFalse ⋯

@[instance_reducible]

instance Miri.DataStructures.instReprAccessType : Repr AccessType

Equations

• Miri.DataStructures.instReprAccessType = { reprPrec := Miri.DataStructures.instReprAccessType.repr }

def Miri.DataStructures.instReprAccessType.repr : AccessType → Nat → Std.Format

Equations

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

inductive Miri.DataStructures.OffsetSearch : Type

A binary-search result: either the containing object or its insertion slot.

• found (position : Position) : OffsetSearch
• insertionPoint (position : Position) : OffsetSearch

def Miri.DataStructures.instDecidableEqOffsetSearch.decEq (x✝ x✝¹ : OffsetSearch) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.DataStructures.instDecidableEqOffsetSearch.decEq (Miri.DataStructures.OffsetSearch.found a) (Miri.DataStructures.OffsetSearch.found b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.DataStructures.instDecidableEqOffsetSearch.decEq (Miri.DataStructures.OffsetSearch.found position) (Miri.DataStructures.OffsetSearch.insertionPoint position_1) = isFalse ⋯
• Miri.DataStructures.instDecidableEqOffsetSearch.decEq (Miri.DataStructures.OffsetSearch.insertionPoint position) (Miri.DataStructures.OffsetSearch.found position_1) = isFalse ⋯

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqOffsetSearch : DecidableEq OffsetSearch

Equations

• Miri.DataStructures.instDecidableEqOffsetSearch = Miri.DataStructures.instDecidableEqOffsetSearch.decEq

def Miri.DataStructures.instReprOffsetSearch.repr : OffsetSearch → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instReprOffsetSearch : Repr OffsetSearch

Equations

• Miri.DataStructures.instReprOffsetSearch = { reprPrec := Miri.DataStructures.instReprOffsetSearch.repr }

inductive Miri.DataStructures.RangeObjectMapError : Type

Explicit forms of the panics and invalid vector operations in the Rust API.

• memory (error : Memory.MemoryError) : RangeObjectMapError
• positionOutOfBounds (position length : Nat) : RangeObjectMapError
• positionRangeReversed (start stop : Nat) : RangeObjectMapError
• positionRangeOutOfBounds (start stop length : Nat) : RangeObjectMapError
• previousObjectOverlaps (position : Position) (previousEnd newStart : ABI.Size) : RangeObjectMapError
• nextObjectOverlaps (position : Position) (newEnd nextStart : ABI.Size) : RangeObjectMapError
• internalIndexOutOfBounds (position length : Nat) : RangeObjectMapError

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqRangeObjectMapError : DecidableEq RangeObjectMapError

Equations

• Miri.DataStructures.instDecidableEqRangeObjectMapError = Miri.DataStructures.instDecidableEqRangeObjectMapError.decEq

def Miri.DataStructures.instDecidableEqRangeObjectMapError.decEq (x✝ x✝¹ : RangeObjectMapError) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.DataStructures.instReprRangeObjectMapError.repr : RangeObjectMapError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instReprRangeObjectMapError : Repr RangeObjectMapError

Equations

• Miri.DataStructures.instReprRangeObjectMapError = { reprPrec := Miri.DataStructures.instReprRangeObjectMapError.repr }

@[instance_reducible]

instance Miri.DataStructures.instToStringRangeObjectMapError : ToString RangeObjectMapError

Equations

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

structure Miri.DataStructures.RangeObject (α : Type) : Type

One entry in the source Vec<Elem<T>>.

• range : Memory.AllocRange
• data : α

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqRangeObject {α✝ : Type} [DecidableEq α✝] : DecidableEq (RangeObject α✝)

Equations

• Miri.DataStructures.instDecidableEqRangeObject = Miri.DataStructures.instDecidableEqRangeObject.decEq

def Miri.DataStructures.instDecidableEqRangeObject.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : RangeObject α✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.DataStructures.instDecidableEqRangeObject.decEq { range := a, data := a_1 } { range := b, data := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Miri.DataStructures.instReprRangeObject.repr {α✝ : Type} [Repr α✝] : RangeObject α✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instReprRangeObject {α✝ : Type} [Repr α✝] : Repr (RangeObject α✝)

Equations

• Miri.DataStructures.instReprRangeObject = { reprPrec := Miri.DataStructures.instReprRangeObject.repr }

structure Miri.DataStructures.RangeObjectMap (α : Type) : Type

The map keeps the source's sorted vector representation.

• objects : Array (RangeObject α)

def Miri.DataStructures.instDecidableEqRangeObjectMap.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : RangeObjectMap α✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.DataStructures.instDecidableEqRangeObjectMap.decEq { objects := a } { objects := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqRangeObjectMap {α✝ : Type} [DecidableEq α✝] : DecidableEq (RangeObjectMap α✝)

Equations

• Miri.DataStructures.instDecidableEqRangeObjectMap = Miri.DataStructures.instDecidableEqRangeObjectMap.decEq

@[instance_reducible]

instance Miri.DataStructures.instReprRangeObjectMap {α✝ : Type} [Repr α✝] : Repr (RangeObjectMap α✝)

Equations

• Miri.DataStructures.instReprRangeObjectMap = { reprPrec := Miri.DataStructures.instReprRangeObjectMap.repr }

def Miri.DataStructures.instReprRangeObjectMap.repr {α✝ : Type} [Repr α✝] : RangeObjectMap α✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instInhabitedRangeObjectMap {a✝ : Type} : Inhabited (RangeObjectMap a✝)

Equations

• Miri.DataStructures.instInhabitedRangeObjectMap = { default := Miri.DataStructures.instInhabitedRangeObjectMap.default }

structure Miri.DataStructures.MutationResult (α : Type) : Type

Mutating Rust methods may panic after changing the vector. Keep that state alongside an explicit error so Lean callers can observe the exact partial effect.

• state : α
• outcome : Except RangeObjectMapError Unit

def Miri.DataStructures.RangeObjectMap.new {α : Type} : RangeObjectMap α

Equations

• Miri.DataStructures.RangeObjectMap.new = { }

@[inline]

def Miri.DataStructures.RangeObjectMap.length {α : Type} (map : RangeObjectMap α) : Nat

Equations

• map.length = map.objects.size

@[inline]

def Miri.DataStructures.RangeObjectMap.isEmpty {α : Type} (map : RangeObjectMap α) : Bool

Equations

• map.isEmpty = map.objects.isEmpty

@[inline]

def Miri.DataStructures.RangeObjectMap.ranges {α : Type} (map : RangeObjectMap α) : Array Memory.AllocRange

Equations

• map.ranges = Array.map Miri.DataStructures.RangeObject.range map.objects

def Miri.DataStructures.RangeObjectMap.index {α : Type} (map : RangeObjectMap α) (position : Position) : Except RangeObjectMapError α

Checked read corresponding to Rust indexing.

Equations

• map.index position = if h : position < map.objects.size then pure map.objects[position].data else throw (Miri.DataStructures.RangeObjectMapError.positionOutOfBounds position map.objects.size)

def Miri.DataStructures.RangeObjectMap.setAtPos {α : Type} (map : RangeObjectMap α) (position : Position) (data : α) : MutationResult (RangeObjectMap α)

Checked replacement corresponding to Rust IndexMut. Invalid indices leave the map unchanged.

Equations

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

def Miri.DataStructures.RangeObjectMap.modifyAtPos {α : Type} (map : RangeObjectMap α) (position : Position) (modify : α → α) : MutationResult (RangeObjectMap α)

Checked in-place data update corresponding to a borrow through IndexMut.

Equations

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

def Miri.DataStructures.RangeObjectMap.iter {α : Type} (map : RangeObjectMap α) : Array α

Source iter() order, materialized as an array for the pure Lean API.

Equations

• map.iter = Array.map Miri.DataStructures.RangeObject.data map.objects

def Miri.DataStructures.RangeObjectMap.findOffset {α : Type} (map : RangeObjectMap α) (offset : ABI.Size) : Except RangeObjectMapError OffsetSearch

Finds the object containing an offset, or the vector insertion position.

Equations

• map.findOffset offset = Miri.DataStructures.RangeObjectMap.findOffsetAux✝ map.objects offset 0 map.objects.size

def Miri.DataStructures.RangeObjectMap.accessType {α : Type} (map : RangeObjectMap α) (range : Memory.AllocRange) : Except RangeObjectMapError AccessType

Classify a byte access exactly as Miri does. In particular the end byte is computed as range.end() - 1; empty accesses can therefore produce the same underflow error as the source instead of receiving special treatment.

Equations

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

def Miri.DataStructures.RangeObjectMap.insertAtPos {α : Type} (map : RangeObjectMap α) (position : Position) (range : Memory.AllocRange) (data : α) : MutationResult (RangeObjectMap α)

Insert before checking adjacency, as in Rust. The returned state therefore contains the inserted element when a subsequent size check or assertion fails.

Equations

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

def Miri.DataStructures.RangeObjectMap.removePosRange {α : Type} (map : RangeObjectMap α) (start stop : Position) : MutationResult (RangeObjectMap α)

Remove a vector interval, corresponding to Vec::drain(start..stop).

Equations

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

def Miri.DataStructures.RangeObjectMap.removeFromPos {α : Type} (map : RangeObjectMap α) (position : Position) : MutationResult (RangeObjectMap α)

Remove one position, corresponding to Vec::remove.

Equations

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

def Miri.DataStructures.RangeObjectMap.WellFormed {α : Type} (map : RangeObjectMap α) : Prop

Sorted, non-overlapping ranges, stated using checked exclusive endpoints.

Equations

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

theorem Miri.DataStructures.RangeObjectMap.new_wellFormed {α : Type} : new.WellFormed

theorem Miri.DataStructures.RangeObjectMap.setAtPos_preserves_ranges {α : Type} (map : RangeObjectMap α) (position : Position) (data : α) (inBounds : position < map.objects.size) : (map.setAtPos position data).state.ranges = map.ranges