Identity of a frame's locals backing buffer (stack.rs locals_addr). This is interpreter metadata, not a Rust allocation or pointer provenance.

structure Miri.Interpreter.LocalsIdentity : Type

• token : Nat

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqLocalsIdentity : DecidableEq LocalsIdentity

Equations

• Miri.Interpreter.instDecidableEqLocalsIdentity = Miri.Interpreter.instDecidableEqLocalsIdentity.decEq

def Miri.Interpreter.instDecidableEqLocalsIdentity.decEq (x✝ x✝¹ : LocalsIdentity) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqLocalsIdentity.decEq { token := a } { token := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprLocalsIdentity : Repr LocalsIdentity

Equations

• Miri.Interpreter.instReprLocalsIdentity = { reprPrec := Miri.Interpreter.instReprLocalsIdentity.repr }

def Miri.Interpreter.instReprLocalsIdentity.repr : LocalsIdentity → Nat → Std.Format

Equations

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

def Miri.Interpreter.LocalsIdentity.ofAllocationToken (token : Nat) : LocalsIdentity

The embedding supplies the actual abstract host-buffer token. Equal tokens represent equal buffer identity; a host allocator may explicitly reuse tokens.

Equations

• Miri.Interpreter.LocalsIdentity.ofAllocationToken token = { token := token }

structure Miri.Interpreter.LocalsIdentitySupply : Type

Optional lifetime-unique ghost labeling discipline. Callers supply a next unused token explicitly; no frame receives an invented default identity. This labels lifetimes rather than modeling possible host-address reuse.

• nextUnused : Nat

def Miri.Interpreter.instReprLocalsIdentitySupply.repr : LocalsIdentitySupply → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprLocalsIdentitySupply : Repr LocalsIdentitySupply

Equations

• Miri.Interpreter.instReprLocalsIdentitySupply = { reprPrec := Miri.Interpreter.instReprLocalsIdentitySupply.repr }

def Miri.Interpreter.LocalsIdentitySupply.allocate (supply : LocalsIdentitySupply) : LocalsIdentitySupply × LocalsIdentity

Equations

• supply.allocate = ({ nextUnused := supply.nextUnused + 1 }, Miri.Interpreter.LocalsIdentity.ofAllocationToken supply.nextUnused)