Pure calendar/timezone portion of the chrono 0.4 / chrono-tz 0.10 UTC-to-local path used by Miri's localtime_r. Transition records are the generated IANA 2025b tables in ChronoTzData; this module never consults host zoneinfo or imports the Input layer.

@[reducible, inline]

abbrev Miri.Interpreter.ChronoTz.TZ : Type

Equations

• Miri.Interpreter.ChronoTz.TZ = String

@[reducible, inline]

abbrev Miri.Interpreter.ChronoTz.Timestamp : Type

Equations

• Miri.Interpreter.ChronoTz.Timestamp = Int64

def Miri.Interpreter.ChronoTz.validTimestamp (seconds : Int64) : Bool

DateTime::from_timestamp(secs, 0) converts to CE days and then uses NaiveDate::from_num_days_from_ce_opt; mirror its real MIN_YEAR/MAX_YEAR bounds rather than accepting every i32 day count.

Equations

• Miri.Interpreter.ChronoTz.validTimestamp seconds = (have days := seconds.toInt / 86400; have ceDay := days + 719163; pure (decide (-95746129 ≤ ceDay) && decide (ceDay ≤ 95745399))).run

def Miri.Interpreter.ChronoTz.timestamp (seconds : Int64) : Option Timestamp

Equations

• Miri.Interpreter.ChronoTz.timestamp seconds = if Miri.Interpreter.ChronoTz.validTimestamp seconds = true then some seconds else none

def Miri.Interpreter.ChronoTz.timezone (input : String) : Option TZ

Equations

• Miri.Interpreter.ChronoTz.timezone input = Miri.Interpreter.ChronoTz.timezoneName✝ input

def Miri.Interpreter.ChronoTz.convert (value : Timestamp) (zone : TZ) : Option TimeShims.BrokenDown

Equations

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