Source-owned process entry construction. This module is kept separate from EvalStartupAssembly because the source Core imports the Unix foreign chain that itself depends on the legacy assembly module.
Evidence that every choice requested by the run loop is the same choice used to assemble its initial source package. This is an opt-in optimization: generic runners without this evidence continue to construct per-choice source packages.
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Equations
- Miri.Input.EvalSourceRunConstruction.State Os R P H D O Aff B Host = Miri.Input.EvalRuntimeConstruction.EntryState Os R P H D O Aff B Host
Instances For
@[reducible, inline]
abbrev
Miri.Input.EvalSourceRunConstruction.SourceHost
(Poll Instant System H D O Native Profiler : Type)
:
Equations
- Miri.Input.EvalSourceRunConstruction.SourceHost Poll Instant System H D O Native Profiler = Miri.Input.HostRuntime.Storage Poll Instant System H D O Native Profiler
Instances For
@[reducible, inline]
abbrev
Miri.Input.EvalSourceRunConstruction.SourceState
(Os R P H D O Aff B Poll Instant System Native Profiler : Type)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.initialStateFromSourceConfiguration
{Os R P H D O Aff B Poll Instant System Native Profiler : Type}
(configuration : InitialMachine.Configuration Aff B)
(memory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind)
(types : RuntimeArrayTypes.World)
(choices : Interpreter.ExecutionChoices.Tape)
(host : SourceHost Poll Instant System H D O Native Profiler)
:
Except Interpreter.StepError (SourceState Os R P H D O Aff B Poll Instant System Native Profiler)
Create the canonical initial EvalWorld for the source runner from the selected initialization configuration, imported memory, runtime type arrays, choice tape and actual host storage. The caller supplies the exact source configuration; this constructor applies it once, rather than requiring an arbitrary preassembled machine State.
Equations
- Miri.Input.EvalSourceRunConstruction.initialStateFromSourceConfiguration configuration memory types choices host = Miri.Input.InitialMachine.create configuration memory types choices host
Instances For
def
Miri.Input.EvalSourceRunConstruction.sourceArguments
{Os R P H D O Aff B Host C ClockHost : Type}
(compiler : CompilerProviders.Prepared)
(execution : EvalExecutable.Core Os R P H D O Aff B Host C ClockHost)
(facts : EvalStartupRuntimeConstruction.StartupFacts)
:
Except Interpreter.StepError
(ULift
(Interpreter.EntryArguments.Hooks Memory.MiriMemoryKind
(Interpreter.ThreadStacks.Storage (EvalExecutable.U Os R P H D O Aff B Host))
(Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (W Os R P H D O Aff B Host))) P C))
Compute argv hooks from the same fixed source execution config that will run Main and the MIR body. Compiler facts remain demand-local errors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.sourceClockToOuter
{Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type}
(clock :
Interpreter.Clock.HostHooks Instant System
(EvalUnixSourceConstruction.State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream
Error))
:
Interpreter.Clock.HostHooks Instant System
(EvalRuntimeConstruction.EntryState Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native
Profiler))
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.sourceDurationSinceToOuter
{Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type}
(operation :
System →
System →
Interpreter.Clock.M
(EvalUnixSourceConstruction.State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw
Listener TcpStream Error)
(Option Interpreter.Clock.Duration))
:
System →
System →
Interpreter.Clock.M
(EvalRuntimeConstruction.EntryState Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native
Profiler))
(Option Interpreter.Clock.Duration)
Equations
- Miri.Input.EvalSourceRunConstruction.sourceDurationSinceToOuter operation later earlier = Miri.Interpreter.ExecutionStateTransport.action (operation later earlier)
Instances For
def
Miri.Input.EvalSourceRunConstruction.sourceChoiceAccess
{Os R H D O Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type}
:
Interpreter.ExecutionChoices.Access
(Interpreter.ThreadStacks.State Memory.MiriMemoryKind
(EvalCallbackMachine.ThreadUser Os R EvalSyncPayload.Payload H D O Aff B Poll Instant System Native Profiler))
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.sourceMainFromExecution
[DecidableEq Memory.MiriMemoryKind]
{Os R P H D O Aff B Host C ClockHost : Type}
(prepared : EvalPreparation.Prepared)
(execution : EvalExecutable.Core Os R P H D O Aff B Host C ClockHost)
(limits : Interpreter.ExecutionMachine.Limits)
(choice : C)
(spans : Interpreter.AllocationDriver.SpanHooks)
(memory : EvalHostRuntimeConstruction.EnvironmentMemory (EvalStartupAssembly.InnerControl Os R P H D O Aff B Host) C P)
(initial : EvalRuntimeConstruction.EntryState Os R P H D O Aff B Host)
:
Except Interpreter.StepError
(Interpreter.MainMachine.Hooks (EvalExecutable.U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId)
(ABI.ArgAbi MIR.TyId) Aff P)
Construct Main/TLS from the exact source Core and compiler target facts. Extern-static lookup is closed over the same function registry and runtime root used by that Core; no complete Main hook record is accepted.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.assembleBootstrapHooks
{Os R P H D O Aff B Host C ClockHost : Type}
(arguments :
ULift
(Interpreter.EntryArguments.Hooks Memory.MiriMemoryKind
(Interpreter.ThreadStacks.Storage (EvalExecutable.U Os R P H D O Aff B Host))
(Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (W Os R P H D O Aff B Host))) P C))
(main :
Interpreter.MainMachine.Hooks (EvalExecutable.U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId)
(ABI.ArgAbi MIR.TyId) Aff P)
(environment :
Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os
(Interpreter.MainMachine.State (EvalExecutable.U Os R P H D O Aff B Host)))
(externStatics :
Interpreter.ExternStatic.InitHooks (Interpreter.MainMachine.State (EvalExecutable.U Os R P H D O Aff B Host)))
(compiler : CompilerProviders.Prepared)
(image : AllocationImage.Imported)
(vtableRuntime :
Interpreter.VTableMachine.Hooks Memory.MiriMemoryKind
(Interpreter.ThreadStacks.Storage (EvalExecutable.U Os R P H D O Aff B Host)) O)
(configuration : EvalBootstrap.Configuration Os)
:
EvalBootstrap.Configuration Os × EvalBootstrap.Hooks (EvalExecutable.U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId)
(ABI.ArgAbi MIR.TyId) Aff P
(Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (W Os R P H D O Aff B Host))) Os
Assemble the exact late-init hooks from already source-constructed argv and Main components plus canonical environment/static/vtable adapters. The argv capability is unlifted only at this typed boundary; no hooks dictionary is accepted as a whole.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.bootstrapFromSourceExecution
[DecidableEq Memory.MiriMemoryKind]
{Raw Listener TcpStream Error Os R P H D Aff B Poll Instant System Native Profiler C : Type}
(prepared : EvalPreparation.Prepared)
(execution :
EvalExecutable.Core Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler)
C Instant)
(limits : Interpreter.ExecutionMachine.Limits)
(choice : C)
(spans : Interpreter.AllocationDriver.SpanHooks)
(host : EvalHostRuntimeConstruction.OsHostEffects Os)
(hostEffects :
EvalHostRuntimeConstruction.EnvironmentHostEffects
(EvalStartupAssembly.InnerControl Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native
Profiler)))
(memory :
EvalHostRuntimeConstruction.EnvironmentMemory
(EvalStartupAssembly.InnerControl Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native
Profiler))
C P)
(configuration : EvalBootstrap.Configuration Os)
(initial :
EvalRuntimeConstruction.EntryState Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native
Profiler))
:
Except Interpreter.StepError
(ULift
(EvalBootstrap.Configuration Os × EvalBootstrap.Hooks
(EvalExecutable.U Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native
Profiler))
C (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId)
(ABI.ArgAbi MIR.TyId) Aff P
(Interpreter.ValidityMachine.Control
(Interpreter.ThreadStacks.Storage
(W Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B
(SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native
Profiler))))
Os))
Canonical Unix bootstrap. Dynamic symbols use the source Other dynamic
symbol constructor, and the scalar layouts come from the same compiler runtime
facts as the execution Core. No caller-provided encoding or target-sized
layout can diverge from the selected export.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Continue from the exact machine state produced by the source constructor. No host, descriptor or ownership store is rebuilt here.
def
Miri.Input.EvalSourceRunConstruction.runFromInitialProfiled
{Os R H D B Poll Instant System Native Profiler C : Type}
[DecidableEq Os]
[DecidableEq Memory.MiriMemoryKind]
{Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type}
(profile : Lean.Options)
(prepared : EvalPreparation.Prepared)
(image : AllocationImage.Imported)
(bytes : CompilerGlobalBytes.Prepared)
(options : EvalConfigurationCore.Options)
(sourceLeaves :
EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant
System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant
EvalSyncObjectAccess.Payload AddrIter)
(choice : C)
(initialConfiguration : InitialMachine.Configuration Interpreter.CpuAffinity.Mask B)
(bootstrapConfiguration : EvalBootstrap.Configuration Os)
(limits : Interpreter.ExecutionMachine.Limits)
(capacity iterationFuel : Nat)
(outerChoices : List C)
(initial :
EvalRunConstruction.State Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System
Native Profiler)
(stableChoice : Option (StableChoice choice) := none)
:
Except Interpreter.StepError
(EvalRunConstruction.RunResult
(EvalRunConstruction.State Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System
Native Profiler))
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.runFromInitial
{Os R H D B Poll Instant System Native Profiler C : Type}
[DecidableEq Os]
[DecidableEq Memory.MiriMemoryKind]
{Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type}
(prepared : EvalPreparation.Prepared)
(image : AllocationImage.Imported)
(bytes : CompilerGlobalBytes.Prepared)
(options : EvalConfigurationCore.Options)
(sourceLeaves :
EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant
System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant
EvalSyncObjectAccess.Payload AddrIter)
(choice : C)
(initialConfiguration : InitialMachine.Configuration Interpreter.CpuAffinity.Mask B)
(bootstrapConfiguration : EvalBootstrap.Configuration Os)
(limits : Interpreter.ExecutionMachine.Limits)
(capacity iterationFuel : Nat)
(outerChoices : List C)
(initial :
EvalRunConstruction.State Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System
Native Profiler)
(stableChoice : Option (StableChoice choice) := none)
:
Except Interpreter.StepError
(EvalRunConstruction.RunResult
(EvalRunConstruction.State Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System
Native Profiler))
Compatibility entry with the original positional API. Runtime profiling is
opt-in through runFromInitialProfiled; ordinary callers retain this exact
signature and delegate with profiler options disabled.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Explicit lower entry for callers that already own a HostRuntime payload. This keeps that contract available for existing embeddings while the normal production entry below performs the pinned machine construction itself.
def
Miri.Input.EvalSourceRunConstruction.runFromPreinitializedHost
{Os R H D B Poll Instant System Native Profiler C : Type}
[DecidableEq Os]
[DecidableEq Memory.MiriMemoryKind]
{Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type}
(prepared : EvalPreparation.Prepared)
(image : AllocationImage.Imported)
(bytes : CompilerGlobalBytes.Prepared)
(options : EvalConfigurationCore.Options)
(sourceLeaves :
EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant
System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant
EvalSyncObjectAccess.Payload AddrIter)
(choice : C)
(initialConfiguration : InitialMachine.Configuration Interpreter.CpuAffinity.Mask B)
(initialMemory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind)
(runtimeTypes : RuntimeArrayTypes.World)
(choiceTape : Interpreter.ExecutionChoices.Tape)
(host :
SourceHost Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler)
(bootstrapConfiguration : EvalBootstrap.Configuration Os)
(limits : Interpreter.ExecutionMachine.Limits)
(capacity iterationFuel : Nat)
(outerChoices : List C)
:
Except Interpreter.StepError
(EvalRunConstruction.RunResult
(EvalRunConstruction.State Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System
Native Profiler))
Equations
- One or more equations did not get rendered due to their size.
Instances For
Canonical normal process entry. Raw host lifecycle hooks and their exact external state are threaded through MachineConstruction.create. The returned guest state is the same state whose descriptor/ownership tables were created there; startup and execution continue without reinitializing either table. The result retains HostRuntime storage, including for resumable Pending states. It does not implicitly dispose host resources after a terminal guest outcome; embeddings may explicitly call HostRuntime.dispose once the retained state is no longer needed. Constructor rollback still uses MachineConstruction's protect path.
def
Miri.Input.EvalSourceRunConstruction.runFromSourceProfiled
{Os R H D B Poll Instant System Native Profiler C External : Type}
[DecidableEq Os]
[DecidableEq Memory.MiriMemoryKind]
{Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type}
(profile : Lean.Options)
(prepared : EvalPreparation.Prepared)
(image : AllocationImage.Imported)
(bytes : CompilerGlobalBytes.Prepared)
(options : EvalConfigurationCore.Options)
(sourceLeaves :
EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant
System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant
EvalSyncObjectAccess.Payload AddrIter)
(choice : C)
(initialConfiguration : InitialMachine.Configuration Interpreter.CpuAffinity.Mask B)
(initialMemory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind)
(runtimeTypes : RuntimeArrayTypes.World)
(choiceTape : Interpreter.ExecutionChoices.Tape)
(hostRuntime : HostRuntime.Hooks External Poll Instant System Native Profiler)
(bootstrapConfiguration : EvalBootstrap.Configuration Os)
(limits : Interpreter.ExecutionMachine.Limits)
(capacity iterationFuel : Nat)
(outerChoices : List C)
(useBuiltinChronoTz : Bool := true)
(stableChoice : Option (StableChoice choice) := none)
:
EStateM Interpreter.StepError External
(EvalRunConstruction.RunResult
(EvalRunConstruction.State Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System
Native Profiler))
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Input.EvalSourceRunConstruction.runFromSource
{Os R H D B Poll Instant System Native Profiler C External : Type}
[DecidableEq Os]
[DecidableEq Memory.MiriMemoryKind]
{Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type}
(prepared : EvalPreparation.Prepared)
(image : AllocationImage.Imported)
(bytes : CompilerGlobalBytes.Prepared)
(options : EvalConfigurationCore.Options)
(sourceLeaves :
EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant
System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant
EvalSyncObjectAccess.Payload AddrIter)
(choice : C)
(initialConfiguration : InitialMachine.Configuration Interpreter.CpuAffinity.Mask B)
(initialMemory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind)
(runtimeTypes : RuntimeArrayTypes.World)
(choiceTape : Interpreter.ExecutionChoices.Tape)
(hostRuntime : HostRuntime.Hooks External Poll Instant System Native Profiler)
(bootstrapConfiguration : EvalBootstrap.Configuration Os)
(limits : Interpreter.ExecutionMachine.Limits)
(capacity iterationFuel : Nat)
(outerChoices : List C)
(useBuiltinChronoTz : Bool := true)
(stableChoice : Option (StableChoice choice) := none)
:
EStateM Interpreter.StepError External
(EvalRunConstruction.RunResult
(EvalRunConstruction.State Os R EvalSyncPayload.Payload H D
(EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System
Native Profiler))
Compatibility entry with the original positional API. Profiling callers
use runFromSourceProfiled; ordinary callers delegate with profiling disabled.
Equations
- One or more equations did not get rendered due to their size.