Pinned alloc/isolated_alloc.rs:1–309. Actual anonymous RW mmap, munmap, zeroing and sysconf are external host effects. Layout normalization, first-fit compressed bitmaps, page/huge ownership and removal order are source operations. These are host addresses, never fabricated MIR allocation addresses.

structure Miri.Interpreter.NativeIsolatedAlloc.Layout : Type

• size : Nat
• align : Nat

@[instance_reducible]

instance Miri.Interpreter.NativeIsolatedAlloc.instReprLayout : Repr Layout

Equations

• Miri.Interpreter.NativeIsolatedAlloc.instReprLayout = { reprPrec := Miri.Interpreter.NativeIsolatedAlloc.instReprLayout.repr }

def Miri.Interpreter.NativeIsolatedAlloc.instReprLayout.repr : Layout → Nat → Std.Format

Equations

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

structure Miri.Interpreter.NativeIsolatedAlloc.Page : Type

• address : Nat
• occupied : Array Bool

def Miri.Interpreter.NativeIsolatedAlloc.instReprPage.repr : Page → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.NativeIsolatedAlloc.instReprPage : Repr Page

Equations

• Miri.Interpreter.NativeIsolatedAlloc.instReprPage = { reprPrec := Miri.Interpreter.NativeIsolatedAlloc.instReprPage.repr }

structure Miri.Interpreter.NativeIsolatedAlloc.Segment : Type

• address : Nat
• size : Nat

def Miri.Interpreter.NativeIsolatedAlloc.instReprSegment.repr : Segment → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.NativeIsolatedAlloc.instReprSegment : Repr Segment

Equations

• Miri.Interpreter.NativeIsolatedAlloc.instReprSegment = { reprPrec := Miri.Interpreter.NativeIsolatedAlloc.instReprSegment.repr }

structure Miri.Interpreter.NativeIsolatedAlloc.Storage : Type

• pageSize : Nat
• pages : Array Page
• huge : Array Segment

@[instance_reducible]

instance Miri.Interpreter.NativeIsolatedAlloc.instReprStorage : Repr Storage

Equations

• Miri.Interpreter.NativeIsolatedAlloc.instReprStorage = { reprPrec := Miri.Interpreter.NativeIsolatedAlloc.instReprStorage.repr }

def Miri.Interpreter.NativeIsolatedAlloc.instReprStorage.repr : Storage → Nat → Std.Format

Equations

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

structure Miri.Interpreter.NativeIsolatedAlloc.Access (S : Type) : Type

• get : S → Storage
• put : S → Storage → S

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

• hostBits : Nat
• sysconfPageSize : EStateM StepError S Nat
• mmapAnonymousReadWrite : Nat → EStateM StepError S Nat

  Host MAP_PRIVATE|MAP_ANONYMOUS with PROT_READ|PROT_WRITE, null hint, fd=-1 and offset=0. Actual OS zeroed pages, no substituted return address.

• munmap : Nat → Nat → EStateM StepError S Int32
• zero : Nat → Nat → EStateM StepError S Unit

def Miri.Interpreter.NativeIsolatedAlloc.create {S : Type} (h : Host S) : EStateM StepError S Storage

Source construction queries the real host page size once.

Equations

• Miri.Interpreter.NativeIsolatedAlloc.create h = do let size ← h.sysconfPageSize let size ← Miri.Interpreter.NativeIsolatedAlloc.word✝ h size pure { pageSize := size }

def Miri.Interpreter.NativeIsolatedAlloc.allocate {S : Type} (a : Access S) (h : Host S) (requested : Layout) (zeroed : Bool) : EStateM StepError S Nat

Compression normalization precedes huge dispatch. Existing pages are tried in source vector order. Bitmap insertion occurs before host zeroing, so errors retain the same allocation prefix. Huge mmap is always zeroed by its OS contract.

Equations

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

def Miri.Interpreter.NativeIsolatedAlloc.deallocate {S : Type} (a : Access S) (h : Host S) (pointer : Nat) (requested : Layout) : EStateM StepError S Unit

Source removes the owning page/segment before munmap, retaining that removal on host failure. Huge wrong-layout assertion also follows removal.

Equations

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

def Miri.Interpreter.NativeIsolatedAlloc.pages (storage : Storage) : Array Segment

Small-page ranges precede huge ranges, as source Iterator::chain.

Equations

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