def Miri.Interpreter.LinuxForeignMachine.bindMemory {U C Host Payload Place B I : Type} (allocation : UnixMemoryMachine.Hooks U C Host Payload) (choice : C) (choices : UnixMemoryMachine.Choices) (base : LinuxMemory.Hooks (UnixMemoryMachine.State U) Place B I) : UnixMemoryMachine.M U (LinuxMemory.Hooks (UnixMemoryMachine.State U) Place B I)

Actual mmap allocation/deallocation plus Linux mremap's distinct Zero initialization of growth bytes. Address and reuse choices are explicit.

Equations

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

def Miri.Interpreter.LinuxForeignMachine.bindReallocateVia {User Payload C Host Extra Place B I : Type} (lens : FunctionPointers.AddressLens User Payload) (allocation : UnixMemoryMachine.Hooks Payload C Host Extra) (choices : UnixMemoryMachine.Choices) (base : LinuxMemory.Hooks (MachineHooks.State Memory.MiriMemoryKind User) Place B I) : LinuxMemory.Hooks (MachineHooks.State Memory.MiriMemoryKind User) Place B I

Equations

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

def Miri.Interpreter.LinuxForeignMachine.threadAddressLens {U : Type} : FunctionPointers.AddressLens (ThreadStacks.Storage (PointerMachine.User U)) U

Canonical ThreadStacks stores the address engine as its actual user; these kernel-checked laws justify lifting allocation without shadow state.

Equations

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

def Miri.Interpreter.LinuxForeignMachine.bindTls {U C O X FnABI ArgABI Aff P Place H D Other E HM Os B I : Type} (main : MainMachine.Hooks U C O X FnABI ArgABI Aff P) (statics : U → ExternStatic.State) (base : LinuxForeign.Hooks (MainMachine.State U) Place H D Other E HM Os B I) : LinuxForeign.Hooks (MainMachine.State U) Place H D Other E HM Os B I

GNU thread atexit shares the actual static symbol map, compiler instance registry and destructor arena. DSO comparison remains address-only as source.

Equations

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