Shared concrete raw-memory operations: rustc memory.rs:1423–1480 and Miri helpers.rs:755–835. Reads include initialization checks and appropriate provenance stripping; all access/touched effects commit before errors.

@[reducible, inline]

abbrev Miri.Interpreter.RawMemoryMachine.M (K User A : Type) : Type

Equations

• Miri.Interpreter.RawMemoryMachine.M = Miri.Interpreter.MachineHooks.M

def Miri.Interpreter.RawMemoryMachine.reference {K User : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (write : Bool) (pointer : Memory.Pointer (Option Memory.Provenance)) (size : ABI.Size) : M K User (Option (Memory.AllocationAccessRef Memory.Provenance TreeBorrows.BorrowTree))

Equations

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

def Miri.Interpreter.RawMemoryMachine.readBytes {K User : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : UInt64) : M K User ByteArray

Equations

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

def Miri.Interpreter.RawMemoryMachine.readUnsigned {K User : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (pointer : Memory.Pointer (Option Memory.Provenance)) (size : ABI.Size) : M K User ABI.U128

Equations

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

def Miri.Interpreter.RawMemoryMachine.readByte {K User : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (pointer : Memory.Pointer (Option Memory.Provenance)) : M K User UInt8

Equations

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

def Miri.Interpreter.RawMemoryMachine.writeBytes {K User : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (pointer : Memory.Pointer (Option Memory.Provenance)) (bytes : ByteArray) : M K User Unit

Allocation.writeBytes clears overwritten provenance and initializes every byte. A failing overwrite retains its partially mutated allocation.

Equations

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

def Miri.Interpreter.RawMemoryMachine.writeRepeatedByte {K User : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (pointer : Memory.Pointer (Option Memory.Provenance)) (byte : UInt8) (count : UInt64) : M K User Unit

Equations

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

def Miri.Interpreter.RawMemoryMachine.writeCString {K User : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (bytes : ByteArray) (pointer : Memory.Pointer (Option Memory.Provenance)) (capacity : UInt64) : M K User (Bool × UInt64)

Miri helpers.rs:783–801. Insufficient caller capacity returns the needed length without touching the pointer. Successful writes include the terminator.

Equations

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

def Miri.Interpreter.RawMemoryMachine.offset (arithmetic : Memory.PointerArithmetic) (pointer : Memory.Pointer (Option Memory.Provenance)) (amount : UInt64) : Except StepError (Memory.Pointer (Option Memory.Provenance))

String scanning uses wrapping offsets, without an inbounds check before its next byte read. The byte read owns the actual access bounds check.

Equations

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

def Miri.Interpreter.RawMemoryMachine.checkPointer {K User : Type} (config : PlaceMachine.AccessConfig K User) (pointer : Memory.Pointer (Option Memory.Provenance)) : M K User Unit

Explicit ptr_get_alloc_id(...,0), unlike a zero-size dereference this must resolve pointer identity and reject integer/dangling address resolution.

Equations

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