Pinned alloc/alloc_bytes.rs:41–165, isolated-allocator branch. The host pointer is retained with its original (possibly empty) slice layout; allocation and destruction use the one-byte-adjusted layout. Host copy/read are genuine memory effects, never manufactured byte observations. Global allocator mode remains outside this isolated-native construction.

structure Miri.Interpreter.NativeAllocBytes.Buffer : Type

• pointer : Nat
• layout : NativeIsolatedAlloc.Layout

def Miri.Interpreter.NativeAllocBytes.instReprBuffer.repr : Buffer → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.NativeAllocBytes.instReprBuffer : Repr Buffer

Equations

• Miri.Interpreter.NativeAllocBytes.instReprBuffer = { reprPrec := Miri.Interpreter.NativeAllocBytes.instReprBuffer.repr }

structure Miri.Interpreter.NativeAllocBytes.Host (S : Type) : Type

• allocator : NativeIsolatedAlloc.Host S
• copyFrom : Nat → Array UInt8 → EStateM StepError S Unit
• read : Nat → Nat → EStateM StepError S (Array UInt8)

def Miri.Interpreter.NativeAllocBytes.allocate {S : Type} (access : NativeIsolatedAlloc.Access S) (host : Host S) (layout : NativeIsolatedAlloc.Layout) (zeroed : Bool) : EStateM StepError S Buffer

alloc_with: the actual isolated allocator's address, including distinct nonempty backing for zero-length slices. Layout validation runs in allocate.

Equations

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

def Miri.Interpreter.NativeAllocBytes.fromBytes {S : Type} (access : NativeIsolatedAlloc.Access S) (host : Host S) (bytes : Array UInt8) (align : Nat) : EStateM StepError S Buffer

Equations

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

def Miri.Interpreter.NativeAllocBytes.zeroed {S : Type} (access : NativeIsolatedAlloc.Access S) (host : Host S) (size align : Nat) : EStateM StepError S Buffer

Equations

• Miri.Interpreter.NativeAllocBytes.zeroed access host size align = Miri.Interpreter.NativeAllocBytes.allocate access host { size := size, align := align } true

def Miri.Interpreter.NativeAllocBytes.snapshot {S : Type} (host : Host S) (buffer : Buffer) : EStateM StepError S (Array UInt8)

Source Deref exposes exactly the original size, even for empty slices.

Equations

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

def Miri.Interpreter.NativeAllocBytes.clone {S : Type} (access : NativeIsolatedAlloc.Access S) (host : Host S) (buffer : Buffer) : EStateM StepError S Buffer

Equations

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

def Miri.Interpreter.NativeAllocBytes.release {S : Type} (access : NativeIsolatedAlloc.Access S) (host : Host S) (buffer : Buffer) : EStateM StepError S Unit

Equations

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

structure Miri.Interpreter.NativeAllocBytes.GlobalHost (S : Type) : Type

Actual standard allocator effects. Null is allocation exhaustion, unlike isolated mmap failure (which is a source assertion failure).

• hostBits : Nat
• allocate : NativeIsolatedAlloc.Layout → Bool → EStateM StepError S Nat
• deallocate : Nat → NativeIsolatedAlloc.Layout → EStateM StepError S Unit
• copyFrom : Nat → Array UInt8 → EStateM StepError S Unit
• read : Nat → Nat → EStateM StepError S (Array UInt8)

def Miri.Interpreter.NativeAllocBytes.globalAllocate {S : Type} (host : GlobalHost S) (layout : NativeIsolatedAlloc.Layout) (zeroed : Bool) : EStateM StepError S (Option Buffer)

Source alloc_with returns None for conversion/layout errors or null.

Equations

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

def Miri.Interpreter.NativeAllocBytes.globalFromBytes {S : Type} (host : GlobalHost S) (bytes : Array UInt8) (align : Nat) : EStateM StepError S Buffer

Equations

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

def Miri.Interpreter.NativeAllocBytes.globalSnapshot {S : Type} (host : GlobalHost S) (buffer : Buffer) : EStateM StepError S (Array UInt8)

Equations

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

def Miri.Interpreter.NativeAllocBytes.globalClone {S : Type} (host : GlobalHost S) (buffer : Buffer) : EStateM StepError S Buffer

Equations

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

def Miri.Interpreter.NativeAllocBytes.globalRelease {S : Type} (host : GlobalHost S) (buffer : Buffer) : EStateM StepError S Unit

Equations

• Miri.Interpreter.NativeAllocBytes.globalRelease host buffer = host.deallocate buffer.pointer (Miri.Interpreter.NativeAllocBytes.actualLayout✝ buffer.layout)