The input-layer adapter for the pure Chrono/Chrono-TZ source port. Keeping this out of the Interpreter umbrella avoids an Interpreter → Input cycle.

def Miri.Input.EvalChronoTimeSource.effects (S : Type) : EvalTimeConstruction.HostEffects S Interpreter.ChronoTz.TZ Interpreter.ChronoTz.Timestamp

Equations

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

def Miri.Input.EvalChronoTimeSource.sourceTimeSource {Os SourceState : Type} (os : EvalHostRuntimeConstruction.OsHostEffects Os) : EvalSourceHostEffects.TimeSource Os SourceState

Construct the source's optional time provider from actual host OsString encoding operations. The environment lookup remains a guest-state operation inside EvalTimeConstruction; this host input only performs Unix into_string.

Equations

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

def Miri.Input.EvalChronoTimeSource.install {Os R EnvControl SourceState H D O Aff B Raw Listener TcpStream Error ErrorHost Meta Path Poll AddrIter Instant System Native Profiler RunState : Type} (host : EvalSourceHostEffects.Seed Os R EnvControl SourceState H D O Aff B Raw Listener TcpStream Error ErrorHost Meta Path Poll AddrIter Instant System Native Profiler RunState) : EvalSourceHostEffects.Seed Os R EnvControl SourceState H D O Aff B Raw Listener TcpStream Error ErrorHost Meta Path Poll AddrIter Instant System Native Profiler RunState

Install the built-in provider only as an explicit source-factory choice. The host seed's optional time field remains absent when callers do not use this constructor, preserving Core's demand-local no-provider fallback.

Equations

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

def Miri.Input.EvalChronoTimeSource.installSourceInput {Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type} (input : EvalCallDispatchConstruction.SourceInput Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter) : EvalCallDispatchConstruction.SourceInput Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter

Explicit production-source constructor adapter: preserve all supplied raw host leaves and install the built-in Unix chrono provider in the host seed. Callers that need the demand-local missing-provider behavior can pass the unmodified SourceInput instead.

Equations

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