Source-owned time shim construction. The compiler/memory/synchronization operations are bound here; host clock and chrono timezone operations remain explicit environment effects because the current source HostRuntime does not provide those capabilities.

@[reducible, inline]

abbrev Miri.Input.EvalTimeConstruction.Host (Poll Instant System H D O Native Profiler : Type) : Type

Equations

• Miri.Input.EvalTimeConstruction.Host = Miri.Input.HostRuntime.Storage

@[reducible, inline]

abbrev Miri.Input.EvalTimeConstruction.World (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalTimeConstruction.User (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalTimeConstruction.State (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalTimeConstruction.Stored (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

structure Miri.Input.EvalTimeConstruction.HostEffects (S TZ Timestamp : Type) : Type

Genuine chrono host operations. utc and every conversion are required inputs; this constructor never substitutes a fixed timestamp or an identity timezone conversion. TZ lookup itself comes from the guest EnvVars state.

• utc : TZ
• utcTimestamp : Int64 → EStateM Interpreter.StepError S (Option Timestamp)
• parseTimezone : String → EStateM Interpreter.StepError S (Option TZ)
• withTimezone : Timestamp → TZ → EStateM Interpreter.StepError S Interpreter.TimeShims.BrokenDown

def Miri.Input.EvalTimeConstruction.guestTimezone {Os S : Type} [DecidableEq Os] (environment : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os S) (timezoneString : Os → Except Unit String) : EStateM Interpreter.StepError S (Option (Except Unit String))

Equations

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

def Miri.Input.EvalTimeConstruction.fromSource {Os R P H D O Aff B Poll Instant System Native Profiler C Error TZ Timestamp : Type} [DecidableEq Memory.MiriMemoryKind] [DecidableEq Os] (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (Stored Os R P H D O Aff B Poll Instant System Native Profiler)) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) C Interpreter.MachineHooks.FrameExtra) (choice : C) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState (Stored Os R P H D O Aff B Poll Instant System Native Profiler)) O) (syncEffects : Interpreter.TypedSyncMachine.Effects (EvalTypedSyncMachine.State Os R P H D O Aff B Poll Instant System Native Profiler)) (errors : Interpreter.IoError.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Error) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Option Interpreter.Clock.Duration)) (environment : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (State Os R P H D O Aff B Poll Instant System Native Profiler)) (timezoneString : Os → Except Unit String) (communicate : Bool) (host : HostEffects (State Os R P H D O Aff B Poll Instant System Native Profiler) TZ Timestamp) : Except Interpreter.StepError (Interpreter.TimeShims.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Instant System TZ Timestamp)

Bind source time policy to actual compiler facts, validity-aware guest memory, the single shared typed synchronization runtime, source function-byte allocation, errno, the canonical guest environment and live HostRuntime clock/deadline registries. Only chrono and OS-string conversion remain external.

Equations

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

def Miri.Input.EvalTimeConstruction.fromSourceWithEnvironment {Os R P H D O Aff B Poll Instant System Native Profiler C Error TZ Timestamp : Type} [DecidableEq Memory.MiriMemoryKind] [DecidableEq Os] (p : CompilerProviders.Prepared) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (EvalStartupAssembly.InnerControl Os R P H D O Aff B (Host Poll Instant System H D O Native Profiler)) C P) (environmentHost : EvalHostRuntimeConstruction.EnvironmentHostEffects (EvalStartupAssembly.InnerControl Os R P H D O Aff B (Host Poll Instant System H D O Native Profiler))) (osHost : EvalHostRuntimeConstruction.OsHostEffects Os) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState (Stored Os R P H D O Aff B Poll Instant System Native Profiler)) O) (syncEffects : Interpreter.TypedSyncMachine.Effects (EvalTypedSyncMachine.State Os R P H D O Aff B Poll Instant System Native Profiler)) (errors : Interpreter.IoError.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Error) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Option Interpreter.Clock.Duration)) (timezoneString : Os → Except Unit String) (communicate : Bool) (host : HostEffects (State Os R P H D O Aff B Poll Instant System Native Profiler) TZ Timestamp) : Except Interpreter.StepError (Interpreter.TimeShims.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Instant System TZ Timestamp)

Source entry point that constructs the guest TZ environment hook from the same EvalWorld root and memory bundle used by startup. The chrono/timezone database and OsString::into_string conversion remain genuine explicit host capabilities; clock, deadline registry, errno and typed synchronization are still derived by fromSource from the canonical runtime inputs.

Equations

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

def Miri.Input.EvalTimeConstruction.timeoutDeadline {S Instant System TZ Timestamp : Type} (time : Interpreter.TimeShims.Hooks S Instant System TZ Timestamp) (clock : Interpreter.Clock.TimeoutClock) (style : Interpreter.Clock.TimeoutStyle) (duration : Interpreter.Clock.Duration) : EStateM Interpreter.StepError S Concurrency.ThreadDeadline

Construct a futex deadline with the same actual host/virtual clock and deadline registry used by TimeShims. Keeping this helper here prevents a second deadline map or an elapsed-time placeholder in the futex constructor.

Equations

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