A checked port of Miri's DedupRangeMap<T> range partition.

structure Miri.DataStructures.ByteRange : Type

A half-open byte interval, matching ops::Range<u64>.

• start : UInt64
• stop : UInt64

def Miri.DataStructures.instDecidableEqByteRange.decEq (x✝ x✝¹ : ByteRange) : Decidable (x✝ = x✝¹)

Equations

• Miri.DataStructures.instDecidableEqByteRange.decEq { start := a, stop := a_1 } { start := b, stop := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqByteRange : DecidableEq ByteRange

Equations

• Miri.DataStructures.instDecidableEqByteRange = Miri.DataStructures.instDecidableEqByteRange.decEq

@[instance_reducible]

instance Miri.DataStructures.instReprByteRange : Repr ByteRange

Equations

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

def Miri.DataStructures.instReprByteRange.repr : ByteRange → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instInhabitedByteRange : Inhabited ByteRange

Equations

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

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

One range and its associated value.

• range : ByteRange
• data : α

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqRangeMapSegment {α✝ : Type} [DecidableEq α✝] : DecidableEq (RangeMapSegment α✝)

Equations

• Miri.DataStructures.instDecidableEqRangeMapSegment = Miri.DataStructures.instDecidableEqRangeMapSegment.decEq

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

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instReprRangeMapSegment {α✝ : Type} [Repr α✝] : Repr (RangeMapSegment α✝)

Equations

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

inductive Miri.DataStructures.DedupRangeMapError : Type

Explicit equivalents of the source's checked-size failures and panics.

• sizeError (error : ABI.SizeError) : DedupRangeMapError
• offsetNotCovered (offset mapSize : UInt64) : DedupRangeMapError
• iterationPastMap (endOffset mapSize : UInt64) : DedupRangeMapError
• indexOutOfBounds (index length : Nat) : DedupRangeMapError
• splitOutsideSegment (index : Nat) (offset start stop : UInt64) : DedupRangeMapError
• mergeRequiresAdjacent (previousEnd nextStart : UInt64) : DedupRangeMapError

def Miri.DataStructures.instDecidableEqDedupRangeMapError.decEq (x✝ x✝¹ : DedupRangeMapError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqDedupRangeMapError : DecidableEq DedupRangeMapError

Equations

• Miri.DataStructures.instDecidableEqDedupRangeMapError = Miri.DataStructures.instDecidableEqDedupRangeMapError.decEq

@[instance_reducible]

instance Miri.DataStructures.instReprDedupRangeMapError : Repr DedupRangeMapError

Equations

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

def Miri.DataStructures.instReprDedupRangeMapError.repr : DedupRangeMapError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instToStringDedupRangeMapError : ToString DedupRangeMapError

Equations

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

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

The source's ordered vector of half-open intervals.

• entries : Array (RangeMapSegment α)

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

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instDecidableEqDedupRangeMap {α✝ : Type} [DecidableEq α✝] : DecidableEq (DedupRangeMap α✝)

Equations

• Miri.DataStructures.instDecidableEqDedupRangeMap = Miri.DataStructures.instDecidableEqDedupRangeMap.decEq

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

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instReprDedupRangeMap {α✝ : Type} [Repr α✝] : Repr (DedupRangeMap α✝)

Equations

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

@[instance_reducible]

instance Miri.DataStructures.instInhabitedDedupRangeMap {a✝ : Type} : Inhabited (DedupRangeMap a✝)

Equations

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

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

Mutations carry state even on failure, preserving operations performed before the corresponding Rust panic.

• state : α
• outcome : Except DedupRangeMapError Unit

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

Result of preparing a source iter_mut call. The map already contains the source's start/end splits and opportunistic merges; positions identify exactly the entries borrowed by the returned Rust iterator.

• state : DedupRangeMap α
• positions : Array Nat
• segments : Array (RangeMapSegment α)
• outcome : Except DedupRangeMapError Unit

def Miri.DataStructures.DedupRangeMap.new {α : Type} (size : ABI.Size) (initial : α) : DedupRangeMap α

Equations

• Miri.DataStructures.DedupRangeMap.new size initial = if (size.bytes == 0) = true then { } else { entries := #[{ range := { start := 0, stop := size.bytes }, data := initial }] }

def Miri.DataStructures.DedupRangeMap.size {α : Type} (map : DedupRangeMap α) : ABI.Size

The source reports the last interval's end, or zero for an empty map.

Equations

• map.size = match map.entries.back? with | none => Miri.ABI.Size.ZERO | some segment => Miri.ABI.Size.ofBytes segment.range.stop

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

Equations

• map.isEmpty = map.entries.isEmpty

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

Equations

• map.length = map.entries.size

def Miri.DataStructures.DedupRangeMap.iter {α : Type} (map : DedupRangeMap α) (offset len : ABI.Size) : Except DedupRangeMapError (Array (RangeMapSegment α))

Read-only iteration returns complete stored segments intersecting the requested interval; edge segments are not split or clipped.

Equations

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

def Miri.DataStructures.DedupRangeMap.iterAll {α : Type} (map : DedupRangeMap α) : Array (RangeMapSegment α)

Equations

• map.iterAll = map.entries

def Miri.DataStructures.DedupRangeMap.index {α : Type} (map : DedupRangeMap α) (position : Nat) : Except DedupRangeMapError (RangeMapSegment α)

Read a stored segment by vector position.

Equations

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

def Miri.DataStructures.DedupRangeMap.setAtPos {α : Type} (map : DedupRangeMap α) (position : Nat) (data : α) : DedupMutationResult (DedupRangeMap α)

Replace a stored segment's value, corresponding to mutation through a returned mutable iterator reference.

Equations

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

def Miri.DataStructures.DedupRangeMap.iterMutWithClone {α : Type} (map : DedupRangeMap α) (offset len : ABI.Size) [DecidableEq α] (cloneData : α → α) : IterMutResult α

Perform source iter_mut's eager start split, bounded duplicate merge scan, and end split. The returned position list represents the mutable slice; callers can update those entries using setAtPos.

Equations

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

def Miri.DataStructures.DedupRangeMap.iterMut {α : Type} (map : DedupRangeMap α) (offset len : ABI.Size) [DecidableEq α] : IterMutResult α

Prepare a mutable range using value-preserving copies on splits. This is the usual instance for value-like Lean state and is exact when the Rust Clone implementation returns the same value. Use iterMutWithClone when a modeled clone operation produces a different value.

Equations

• map.iterMut offset len = map.iterMutWithClone offset len id

def Miri.DataStructures.DedupRangeMap.modifyRangeWithClone {α : Type} (map : DedupRangeMap α) (offset len : ABI.Size) [DecidableEq α] (cloneData : α → α) (modify : ByteRange → α → α) : IterMutResult α

Apply one pure update to every segment selected by iter_mut. Splitting and merging happen first, before the callback updates values, as in Rust.

Equations

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

def Miri.DataStructures.DedupRangeMap.modifyRange {α : Type} (map : DedupRangeMap α) (offset len : ABI.Size) [DecidableEq α] (modify : ByteRange → α → α) : IterMutResult α

Apply a pure update after source iter_mut splitting and merging. The default split copy preserves the immutable Lean value.

Equations

• map.modifyRange offset len modify = map.modifyRangeWithClone offset len id modify

def Miri.DataStructures.DedupRangeMap.modifyAll {α : Type} (map : DedupRangeMap α) (modify : ByteRange → α → α) : DedupRangeMap α

Apply an update to every element without splitting or merging, matching iter_mut_all.

Equations

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

def Miri.DataStructures.DedupRangeMap.mergeAdjacentThorough {α : Type} (map : DedupRangeMap α) [DecidableEq α] : DedupMutationResult (DedupRangeMap α)

Coalesce every adjacent equal run, with the same adjacency assertion as the source. On a failed assertion the vector contains only the already-built prefix.

Equations

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

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

Sorted, gapless, nonempty intervals beginning at zero.

Equations

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

theorem Miri.DataStructures.DedupRangeMap.new_wellFormed {α : Type} (size : ABI.Size) (initial : α) : (new size initial).WellFormed

def Miri.DataStructures.DedupRangeMap.tacticName_full_range_scan : Lean.ParserDescr

Equations

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

theorem Miri.DataStructures.DedupRangeMap.iterMut_new_full {A : Type} [DecidableEq A] (size : ABI.Size) (value : A) (positive : size.bytes ≠ 0) : (new size value).iterMut ABI.Size.ZERO size = { state := new size value, positions := #[0], segments := #[{ range := { start := 0, stop := size.bytes }, data := value }], outcome := Except.ok () }