The same source address algorithm on the actual machine-only hook state. Global allocation conversion cannot invent a MIR frame merely to adjust a pointer. Source choices, address-map updates and reuse clock acquisition retain exact ordering; the low-level GlobalAddressState algorithm remains shared.

@[reducible, inline]

abbrev Miri.Interpreter.MachineAddress.State (K U : Type) : Type

Equations

• Miri.Interpreter.MachineAddress.State K U = Miri.Interpreter.MachineHooks.MachineState K (Miri.Interpreter.PointerMachine.User U)

@[reducible, inline]

abbrev Miri.Interpreter.MachineAddress.M (K U A : Type) : Type

Equations

• Miri.Interpreter.MachineAddress.M K U A = EStateM Miri.Interpreter.StepError (Miri.Interpreter.MachineAddress.State K U) A

structure Miri.Interpreter.MachineAddress.Hooks (K U : Type) : Type

• arithmetic : Memory.PointerArithmetic
• externalAddress : Memory.AllocId → Memory.AllocAddresses.AllocationAddressInfo → M K U UInt64
• classifyAddressError : Memory.AllocAddresses.AddressStateError → StepError

def Miri.Interpreter.MachineAddress.assign {K U : Type} (h : Hooks K U) (id : Memory.AllocId) (kind : Option Memory.AllocAddresses.AddressMemoryKind) (choice : Memory.AllocAddresses.AddressRandomChoices) : M K U UInt64

Equations

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

def Miri.Interpreter.MachineAddress.addrFromAllocId {K U : Type} (access : ExecutionChoices.Access (State K U)) (h : Hooks K U) (id : Memory.AllocId) (kind : Option Memory.AllocAddresses.AddressMemoryKind) : M K U UInt64

Equations

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

theorem Miri.Interpreter.MachineAddress.stack_miss_request {K U : Type} (access : ExecutionChoices.Access (State K U)) (h : Hooks K U) (state : State K U) (id : Memory.AllocId) (info : Memory.AllocationInfo) (generation : Memory.AllocAddresses.AddressGenerationState) (missing : Array.find? (fun (row : Memory.AllocAddresses.BaseAddressEntry) => row.allocId == id) state.user.addresses.baseAddr = none) (metadata : state.memory.getAllocInfo id = Except.ok info) (data : info.kind = Memory.AllocationKind.liveData) (live : state.memory.isAllocLive id = true) (managed : state.user.addresses.addressMode = Memory.AllocAddresses.AddressSpaceMode.managed) (currentGeneration : state.user.addresses.generation = some generation) : addrFromAllocId access h id (some Memory.AllocAddresses.AddressMemoryKind.stack) state = (ExecutionChoices.index access ExecutionChoices.IndexSite.addressSlack 16 >>= fun (selected : Nat) => if valid : selected < 16 then assign h id (some Memory.AllocAddresses.AddressMemoryKind.stack) { reuse := false, crossThread := false, poolIndex := 0, slack := ⟨selected, valid⟩ } else throw (StepError.invalidProgram "checked address slack exceeded support")) state

The stack-miss source branch requests exactly one Fin16 slack sample before the deterministic assignment. No source address success is assumed.

theorem Miri.Interpreter.MachineAddress.stack_miss_supplied {K U : Type} (access : ExecutionChoices.Access (State K U)) (h : Hooks K U) (state : State K U) (id : Memory.AllocId) (info : Memory.AllocationInfo) (generation : Memory.AllocAddresses.AddressGenerationState) (tape : ExecutionChoices.Tape) (value : Nat) (missing : Array.find? (fun (row : Memory.AllocAddresses.BaseAddressEntry) => row.allocId == id) state.user.addresses.baseAddr = none) (metadata : state.memory.getAllocInfo id = Except.ok info) (data : info.kind = Memory.AllocationKind.liveData) (live : state.memory.isAllocLive id = true) (managed : state.user.addresses.addressMode = Memory.AllocAddresses.AddressSpaceMode.managed) (currentGeneration : state.user.addresses.generation = some generation) (currentTape : access.get state = tape) (strict : tape.policy = ExecutionChoices.Policy.strict) (head : tape.inputs[tape.cursor]? = some (ExecutionChoices.Input.index ExecutionChoices.IndexSite.addressSlack value)) (supported : value < 16) : addrFromAllocId access h id (some Memory.AllocAddresses.AddressMemoryKind.stack) state = assign h id (some Memory.AllocAddresses.AddressMemoryKind.stack) { reuse := false, crossThread := false, poolIndex := 0, slack := ⟨value, supported⟩ } (access.put state { inputs := tape.inputs, cursor := tape.cursor + 1, policy := tape.policy, generatedChoices := tape.generatedChoices, diagnosticRngState := tape.diagnosticRngState, events := tape.events.push { request := ExecutionChoices.Request.index ExecutionChoices.IndexSite.addressSlack 16, input := ExecutionChoices.Input.index ExecutionChoices.IndexSite.addressSlack value } })

A legal supplied stack-slack sample is consumed exactly once before actual source assignment; assignment's non-choice outcome remains explicit.

def Miri.Interpreter.MachineAddress.resultState {S A : Type} : EStateM.Result StepError S A → S

Source action outcomes retain their effects on both error and success.

Equations

• Miri.Interpreter.MachineAddress.resultState (EStateM.Result.ok a state) = state
• Miri.Interpreter.MachineAddress.resultState (EStateM.Result.error a state) = state

theorem Miri.Interpreter.MachineAddress.assign_managed_payload {K U : Type} (h : Hooks K U) (state : State K U) (id : Memory.AllocId) (kind : Option Memory.AllocAddresses.AddressMemoryKind) (choices : Memory.AllocAddresses.AddressRandomChoices) (managed : state.user.addresses.addressMode = Memory.AllocAddresses.AddressSpaceMode.managed) (noRace : state.dataRace = none) : (resultState (assign h id kind choices state)).user.payload = state.user.payload