stdlib.time

Time Library

Generated from v0.65.7. 8 source files, 144 documented symbols.

calendar.xi

fn calendar_month_name(month: Int) -> Str

The full English month name (1 = January). Params: month - the month number. Returns: "January".."December"; an out-of-range month yields "Unknown". Complexity: O(1).

• Postcondition: ((month == 1) => (result == "January")) && ((month == 2) => (result == "February")) && ((month == 3) => (result == "March")) && ((month == 4) => (result == "April")) && ((month == 5) => (result == "May")) && ((month == 6) => (result == "June")) && ((month == 7) => (result == "July")) && ((month == 8) => (result == "August")) && ((month == 9) => (result == "September")) && ((month == 10) => (result == "October")) && ((month == 11) => (result == "November")) && ((month == 12) => (result == "December")) && ((month < 1 || month > 12) => (result == "Unknown"))

fn calendar_month_name_short(month: Int) -> Str

The three-letter month abbreviation. Params: month - the month number. Returns: "Jan".."Dec"; an out-of-range month yields "Unk". Complexity: O(1).

• Postcondition: ((month == 1) => (result == "Jan")) && ((month == 2) => (result == "Feb")) && ((month == 3) => (result == "Mar")) && ((month == 4) => (result == "Apr")) && ((month == 5) => (result == "May")) && ((month == 6) => (result == "Jun")) && ((month == 7) => (result == "Jul")) && ((month == 8) => (result == "Aug")) && ((month == 9) => (result == "Sep")) && ((month == 10) => (result == "Oct")) && ((month == 11) => (result == "Nov")) && ((month == 12) => (result == "Dec")) && ((month < 1 || month > 12) => (result == "Unk"))

fn calendar_weekday_name(weekday: Int) -> Str

The full English weekday name (0 = Sunday). Params: weekday - 0 for Sunday through 6 for Saturday. Returns: "Sunday".."Saturday"; out of range yields "Unknown". Complexity: O(1).

• Postcondition: ((weekday == 0) => (result == "Sunday")) && ((weekday == 1) => (result == "Monday")) && ((weekday == 2) => (result == "Tuesday")) && ((weekday == 3) => (result == "Wednesday")) && ((weekday == 4) => (result == "Thursday")) && ((weekday == 5) => (result == "Friday")) && ((weekday == 6) => (result == "Saturday")) && ((weekday < 0 || weekday > 6) => (result == "Unknown"))

fn calendar_weekday_name_short(weekday: Int) -> Str

The three-letter weekday abbreviation. Params: weekday - 0 for Sunday through 6 for Saturday. Returns: "Sun".."Sat"; out of range yields "Unk". Complexity: O(1).

• Postcondition: ((weekday == 0) => (result == "Sun")) && ((weekday == 1) => (result == "Mon")) && ((weekday == 2) => (result == "Tue")) && ((weekday == 3) => (result == "Wed")) && ((weekday == 4) => (result == "Thu")) && ((weekday == 5) => (result == "Fri")) && ((weekday == 6) => (result == "Sat")) && ((weekday < 0 || weekday > 6) => (result == "Unk"))

fn calendar_days_in_month(year: Int, month: Int) -> Int

The number of days in that month. Params: year, month - the calendar fields. Returns: 28-31 days. Complexity: O(1).

• Postcondition: ((month == 2) => (result == 28 || result == 29)) && ((month == 4 || month == 6 || month == 9 || month == 11) => (result == 30)) && ((month == 1 || month == 3 || month == 5 || month == 7 || month == 8 || month == 10 || month == 12) => (result == 31)) && ((month < 1 || month > 12) => (result == 31))

fn calendar_first_weekday(year: Int, month: Int) -> Int

The weekday of the first day of the month. Params: year, month - the calendar fields. Returns: 0 for Sunday through 6 for Saturday. Complexity: O(1).

• Postcondition: (0 <= result && result < 7) && ((year == 1970 && month == 1) => (result == 4))

fn calendar_weeks_in_year(year: Int) -> Int

The number of ISO weeks in that year. Params: year - the year. Returns: 52, or 53 when the ISO year has 53 weeks. Complexity: O(1).

• Postcondition: result == 52 || result == 53

fn calendar_easter(year: Int) -> Date

The date of Easter Sunday in that year. Params: year - the year. Returns: the Easter Sunday date (Meeus/Jones/Butcher computus). Complexity: O(1).

• Postcondition: (year >= 1583) => (result.year == year && ((result.month == 3 && 22 <= result.day && result.day <= 31) || (result.month == 4 && 1 <= result.day && result.day <= 25)))

fn calendar_julian_day(year: Int, month: Int, day: Int) -> Int

The Julian Day Number of the date. Params: year, month, day - the calendar fields. Returns: the astronomical Julian Day Number. Complexity: O(1).

• Postcondition: result == days_from_civil_cl(year, month, day) + 2440588

fn calendar_from_julian_day(jd: Int) -> Date

The calendar date for a Julian Day Number. Params: jd - the Julian Day Number. Returns: the corresponding Date. Complexity: O(1).

• Postcondition: (jd >= 2440588 - 719468) => (calendar_julian_day(result.year, result.month, result.day) == jd)

fn calendar_month_grid(year: Int, month: Int) -> Vec[Int]

The weekday slots of the month, 0 for empty cells. Params: year, month - the calendar fields. Returns: a 42-slot grid starting on the first day's weekday. Complexity: O(1).

• Postcondition: (result.len() == 42) && ((year == 1970 && month == 1) => (result[0] == 0 && result[4] == 1))

fn calendar_is_weekend(d: &Date) -> Bool

True if d falls on a Saturday or Sunday. Params: d - the date. Returns: whether the weekday is 0 (Sunday) or 6 (Saturday). Complexity: O(1).

• Postcondition: result == (time.date_day_of_week(d.year, d.month, d.day) == 0 || time.date_day_of_week(d.year, d.month, d.day) == 6)

fn calendar_add_months_overflow_safe(d: &Date, n: Int) -> Date

d advanced by n months, clamping the day. Params: d - the base date; n - the month offset. Returns: the shifted date with the day clamped to the target month. Complexity: O(1).

• Postcondition: (1 <= result.month && result.month <= 12) && (result.day <= 31) && (result.day <= d.day) && ((1 <= d.day) => (1 <= result.day)) && ((n == 0 && 1 <= d.month && d.month <= 12 && 1 <= d.day && d.day <= 28) => (result.year == d.year && result.month == d.month && result.day == d.day))

---

---

---

chrono.xi

fn chrono_now() -> DateTime

The current local date and time. Returns: the current date/time (the runtime clock is UTC; local is a documented alias in this build). Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: 0 <= result.hour && result.hour < 24
• Postcondition: 0 <= result.minute && result.minute < 60
• Postcondition: 0 <= result.second && result.second < 60
• Postcondition: 0 <= result.weekday && result.weekday < 7

fn chrono_from_timestamp(ts: Int) -> DateTime

The DateTime at Unix timestamp ts. Params: ts - seconds since the Unix epoch. Returns: the UTC date/time at that instant. Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: 0 <= result.hour && result.hour < 24
• Postcondition: 0 <= result.minute && result.minute < 60
• Postcondition: 0 <= result.second && result.second < 60
• Postcondition: 0 <= result.weekday && result.weekday < 7

fn chrono_to_timestamp(dt: &DateTime) -> Int

The Unix timestamp of dt. Params: dt - the date/time. Returns: seconds since the Unix epoch. Complexity: O(1).

• Postcondition: (0 <= dt.second && dt.second < 60) => ((result - dt.second) % 60 == 0)

fn chrono_add_seconds(dt: &DateTime, n: Int) -> DateTime

dt advanced by n seconds. Params: dt - the date/time; n - the second offset. Returns: the shifted date/time. Complexity: O(1).

• Postcondition: chrono_to_timestamp(&result) == chrono_to_timestamp(dt) + n

fn chrono_add_days(dt: &DateTime, n: Int) -> DateTime

dt advanced by n days. Params: dt - the date/time; n - the day offset. Returns: the shifted date/time. Complexity: O(1).

• Postcondition: chrono_to_timestamp(&result) == chrono_to_timestamp(dt) + n * 86400

fn chrono_add_months(dt: &DateTime, n: Int) -> DateTime

dt advanced by n months, clamping the day. Params: dt - the date/time; n - the month offset. Returns: the shifted date/time with the day clamped to the target month. Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: result.hour == dt.hour && result.minute == dt.minute && result.second == dt.second

fn chrono_add_years(dt: &DateTime, n: Int) -> DateTime

dt advanced by n years, clamping Feb 29. Params: dt - the date/time; n - the year offset. Returns: the shifted date/time with the day clamped for non-leap years. Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: result.hour == dt.hour && result.minute == dt.minute && result.second == dt.second

fn chrono_diff(a: &DateTime, b: &DateTime) -> Duration

The elapsed time between a and b. Params: a - the later date/time; b - the earlier date/time. Returns: a - b as a Duration. Complexity: O(1).

• Postcondition: result.nanos == 0
• Postcondition: result.secs == chrono_to_timestamp(a) - chrono_to_timestamp(b)

fn chrono_weekday(dt: &DateTime) -> Int

The day of the week of dt. Params: dt - the date/time. Returns: 0 for Sunday through 6 for Saturday. Complexity: O(1).

• Precondition: 0 <= dt.weekday && dt.weekday < 7

fn chrono_compare(a: &DateTime, b: &DateTime) -> Int

Compare two date/times. Params: a - the left operand; b - the right operand. Returns: negative, zero, or positive for a before, equal, after b. Complexity: O(1).

• Postcondition: (0 - 1) <= result && result <= 1

fn chrono_timezone_offset(dt: &DateTime) -> Int

The UTC offset of dt in seconds. Params: dt - the date/time. Returns: 0 (the runtime clock is UTC). Complexity: O(1).

• Postcondition: result == 0

fn chrono_utc_now() -> DateTime

The current UTC date and time. Returns: the current date/time in UTC. Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: 0 <= result.hour && result.hour < 24
• Postcondition: 0 <= result.minute && result.minute < 60
• Postcondition: 0 <= result.second && result.second < 60
• Postcondition: 0 <= result.weekday && result.weekday < 7

---

---

---

date.xi

fn date_new(year: Int, month: Int, day: Int) -> Date

Build a Date from its fields. Params: year, month, day - the calendar fields. Returns: a Date. Values are not validated. Complexity: O(1).

• Postcondition: result.year == year && result.month == month && result.day == day

fn date_now() -> Date

Today's date from the system clock. Returns: the current date (UTC). Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12 && 1 <= result.day && result.day <= 31

fn date_from_timestamp(ts: Int) -> Date

The date at Unix timestamp ts (UTC). Params: ts - seconds since the Unix epoch. Returns: the calendar date at that instant. Complexity: O(1).

• Postcondition: (ts == 0) => (result.year == 1970 && result.month == 1 && result.day == 1)

fn date_to_timestamp(d: &Date) -> Int

The Unix timestamp at midnight UTC of d. Params: d - the date. Returns: seconds since the epoch at 00:00:00 UTC. Complexity: O(1).

• Postcondition: (d.year == 1970 && d.month == 1 && d.day == 1) => (result == 0)

fn date_weekday(d: &Date) -> Int

The day of the week of d (0 = Sunday). Params: d - the date. Returns: 0 for Sunday through 6 for Saturday. Complexity: O(1).

• Postcondition: (d.year == 1970 && d.month == 1 && d.day == 1) => (result == 4)

fn date_day_of_year(d: &Date) -> Int

The ordinal day of the year (1-366). Params: d - the date. Returns: 1 for January 1st. Complexity: O(month).

• Postcondition: (d.month == 1) => (result == d.day)

fn date_day_of_month(d: &Date) -> Int

The day-of-month field of d. Params: d - the date. Returns: the day field. Complexity: O(1).

• Postcondition: result == d.day

fn date_days_in_month(year: Int, month: Int) -> Int

The number of days in that month. Params: year, month - the calendar fields. Returns: 28-31 days. Complexity: O(1).

• Postcondition: ((month == 2) => (result == 28 || result == 29)) && ((month == 4 || month == 6 || month == 9 || month == 11) => (result == 30)) && ((month == 1 || month == 3 || month == 5 || month == 7 || month == 8 || month == 10 || month == 12) => (result == 31))

fn date_is_leap(year: Int) -> Bool

True if year is a leap year. Params: year - the year. Returns: whether February has 29 days in that year. Complexity: O(1).

• Postcondition: ((year % 400 == 0) => (result == true)) && ((year % 4 != 0) => (result == false)) && ((year % 100 == 0 && year % 400 != 0) => (result == false))

fn date_add_days(d: &Date, n: Int) -> Date

d offset by n days. Params: d - the base date; n - the day offset (may be negative). Returns: the shifted date. Complexity: O(1).

• Postcondition: (n == 0) => (result.year == d.year && result.month == d.month && result.day == d.day)

fn date_sub_days(d: &Date, n: Int) -> Date

d offset by -n days. Params: d - the base date; n - the day offset to subtract. Returns: the shifted date. Complexity: O(1).

• Postcondition: (n == 0) => (result.year == d.year && result.month == d.month && result.day == d.day)

fn date_diff_days(a: &Date, b: &Date) -> Int

The number of days between a and b (a - b). Params: a - the minuend; b - the subtrahend. Returns: a - b in days. Complexity: O(1).

• Postcondition: (a.year == b.year && a.month == b.month && a.day == b.day) => (result == 0)

fn date_compare(a: &Date, b: &Date) -> Int

Compare two dates. Params: a - the left operand; b - the right operand. Returns: negative, zero, or positive for a before, equal, after b. Complexity: O(1).

• Postcondition: ((a.year == b.year && a.month == b.month && a.day == b.day) => (result == 0)) && ((a.year < b.year) => (result == 0 - 1)) && ((a.year > b.year) => (result == 1))

---

---

---

duration.xi

fn duration_secs(n: Int) -> Duration

A duration of n whole seconds. Params: n - the number of seconds. Returns: a Duration of exactly n seconds. Complexity: O(1).

• Postcondition: result.secs == n && result.nanos == 0

fn duration_millis(n: Int) -> Duration

A duration of n milliseconds. Params: n - the number of milliseconds. Returns: a Duration of exactly n milliseconds. Complexity: O(1).

• Postcondition: ((n >= 0 && n % 1000 == 0) => (result.secs == n / 1000 && result.nanos == 0))

fn duration_micros(n: Int) -> Duration

A duration of n microseconds. Params: n - the number of microseconds. Returns: a Duration of exactly n microseconds. Complexity: O(1).

• Postcondition: ((n >= 0 && n % 1000000 == 0) => (result.secs == n / 1000000 && result.nanos == 0))

fn duration_nanos(n: Int) -> Duration

A duration of n nanoseconds. Params: n - the number of nanoseconds. Returns: a Duration of exactly n nanoseconds. Complexity: O(1).

• Postcondition: ((n >= 0 && n % 1000000000 == 0) => (result.secs == n / 1000000000 && result.nanos == 0))

fn duration_from_secs_f64(f: Float64) -> Duration

A duration from a fractional seconds value. Params: f - the fractional seconds value. Returns: a Duration equal to f seconds. Complexity: O(1).

• Postcondition: (f == 0) => (result.secs == 0 && result.nanos == 0)

fn duration_add(a: Duration, b: Duration) -> Duration

The sum of two durations. Params: a - the left operand; b - the right operand. Returns: a + b. Complexity: O(1).

• Postcondition: 0 <= result.nanos && result.nanos < 1000000000

fn duration_sub(a: Duration, b: Duration) -> Duration

The difference of two durations. Params: a - the left operand; b - the right operand. Returns: a - b. Complexity: O(1).

• Postcondition: 0 <= result.nanos && result.nanos < 1000000000

fn duration_mul(a: Duration, n: Int) -> Duration

a scaled by the integer n. Params: a - the duration; n - the scale factor. Returns: a * n. Complexity: O(1).

• Precondition: n >= 0
• Postcondition: 0 <= result.nanos && result.nanos < 1000000000

fn duration_div(a: Duration, n: Int) -> Duration

a divided by the integer n. Params: a - the duration; n - the divisor. Returns: a / n, or a zero duration if n is zero. Complexity: O(1).

• Postcondition: (n == 0) => (result.secs == 0 && result.nanos == 0)

fn duration_as_secs(d: Duration) -> Int

The whole seconds of d. Params: d - the duration. Returns: the seconds component. Complexity: O(1).

• Postcondition: result == d.secs

fn duration_as_millis(d: Duration) -> Int

d in whole milliseconds. Params: d - the duration. Returns: the duration truncated to milliseconds. Complexity: O(1).

• Postcondition: result == d.secs * 1000 + d.nanos / 1000000

fn duration_as_micros(d: Duration) -> Int

d in whole microseconds. Params: d - the duration. Returns: the duration truncated to microseconds. Complexity: O(1).

• Postcondition: result == d.secs * 1000000 + d.nanos / 1000

fn duration_as_nanos(d: Duration) -> Int

d in whole nanoseconds. Params: d - the duration. Returns: the duration truncated to nanoseconds. Complexity: O(1).

• Postcondition: result == d.secs * 1000000000 + d.nanos

fn duration_compare(a: Duration, b: Duration) -> Int

Compare two durations. Params: a - the left operand; b - the right operand. Returns: negative, zero, or positive for a before, equal, after b. Complexity: O(1).

• Postcondition: ((a.secs == b.secs && a.nanos == b.nanos) => (result == 0)) && ((a.secs < b.secs) => (result == 0 - 1)) && ((a.secs > b.secs) => (result == 1))

fn duration_is_zero(d: Duration) -> Bool

True if d is exactly zero. Params: d - the duration. Returns: whether both components are zero. Complexity: O(1).

• Postcondition: result == (d.secs == 0 && d.nanos == 0)

---

---

---

instant.xi

fn instant_now() -> Instant

The current monotonic instant. Returns: an Instant from the system monotonic clock. Complexity: O(1).

• Postcondition: result.t >= 0

fn instant_elapsed(i: Instant) -> Duration

The time elapsed since i. Params: i - the earlier instant. Returns: now - i. Complexity: O(1).

• Postcondition: 0 <= result.nanos && result.nanos < 1000000000

fn instant_duration_since(a: Instant, b: Instant) -> Duration

The time between a and b. Params: a - the later instant; b - the earlier instant. Returns: a - b. Complexity: O(1).

• Postcondition: result == Duration.from_millis(a.t - b.t)

fn instant_add(i: Instant, d: Duration) -> Instant

i advanced by d. Params: i - the instant; d - the duration to add. Returns: i + d. Complexity: O(1).

• Postcondition: result.t == i.t + d.as_millis()

fn instant_sub(i: Instant, d: Duration) -> Instant

i moved back by d. Params: i - the instant; d - the duration to subtract. Returns: i - d. Complexity: O(1).

• Postcondition: result.t == i.t - d.as_millis()

fn instant_compare(a: Instant, b: Instant) -> Int

Compare two instants. Params: a - the left operand; b - the right operand. Returns: negative, zero, or positive for a before, equal, after b. Complexity: O(1).

• Postcondition: ((a.t == b.t) => (result == 0)) && ((a.t < b.t) => (result == 0 - 1)) && ((a.t > b.t) => (result == 1))

fn instant_to_millis(i: Instant) -> Int

i as milliseconds since an arbitrary origin. Params: i - the instant. Returns: the underlying millisecond reading. Complexity: O(1).

• Postcondition: result == i.t

fn instant_from_millis(ms: Int) -> Instant

An instant from a millisecond reading. Params: ms - a millisecond reading from the same arbitrary origin. Returns: the corresponding Instant. Complexity: O(1).

• Postcondition: result.t == ms

---

---

---

iso8601.xi

fn date_iso8601(d: &Date) -> Str

Format d as YYYY-MM-DD. Params: d - the date. Returns: the zero-padded ISO date string. Complexity: O(1).

• Postcondition: ((d.year >= 0 && d.year < 10000 && d.month >= 0 && d.month < 100 && d.day >= 0 && d.day < 100) => (result.len() == 10))

fn datetime_iso8601(dt: &DateTime) -> Str

Format dt with date and time components. Params: dt - the date/time. Returns: "YYYY-MM-DDTHH:MM:SS". Complexity: O(1).

• Postcondition: ((dt.year >= 0 && dt.year < 10000 && dt.month >= 0 && dt.month < 100 && dt.day >= 0 && dt.day < 100 && dt.hour >= 0 && dt.hour < 100 && dt.minute >= 0 && dt.minute < 100 && dt.second >= 0 && dt.second < 100) => (result.len() == 19))

fn iso8601_parse(s: Str) -> Option[DateTime]

Parse an ISO-8601 string into a DateTime. Params: s - a "YYYY-MM-DD" or "YYYY-MM-DDTHH:MM:SS" string, optionally suffixed with 'Z' or a numeric offset. Returns: Some(DateTime) on success, None on malformed or out-of-range input. Offsets are accepted and treated as UTC. Complexity: O(1).

• Postcondition: ((s.len() < 10) => (result.is_none == true)) && ((result.is_some == true) => (s.len() >= 10))

fn rfc3339_format(dt: &DateTime) -> Str

Format dt as a full RFC-3339 timestamp. Params: dt - the date/time. Returns: "YYYY-MM-DDTHH:MM:SSZ" (UTC). Complexity: O(1).

• Postcondition: ((dt.year >= 0 && dt.year < 10000 && dt.month >= 0 && dt.month < 100 && dt.day >= 0 && dt.day < 100 && dt.hour >= 0 && dt.hour < 100 && dt.minute >= 0 && dt.minute < 100 && dt.second >= 0 && dt.second < 100) => (result.len() == 20))

fn rfc3339_parse(s: Str) -> Option[DateTime]

Parse an RFC-3339 timestamp. Params: s - a "YYYY-MM-DDTHH:MM:SS" string with a 'Z' or numeric offset. Returns: Some(DateTime) on success, None on malformed input. Complexity: O(1).

• Postcondition: ((s.len() < 10) => (result.is_none == true)) && ((result.is_some == true) => (s.len() >= 10))

fn iso8601_date_parse(s: Str) -> Option[Date]

Parse a YYYY-MM-DD string into a Date. Params: s - the date string. Returns: Some(Date) on success, None on malformed or out-of-range input. Complexity: O(1).

• Postcondition: result is Some(_) => (1 <= result.value.month && result.value.month <= 12)
• Postcondition: result is Some(_) => (1 <= result.value.day && result.value.day <= 31)

fn iso8601_week_date(d: &Date) -> (Int, Int, Int)

(year, week, weekday) in ISO week numbering. Params: d - the date. Returns: the ISO week year, ISO week number (1-53), and ISO weekday (1 = Monday .. 7 = Sunday). Complexity: O(1).

• Precondition: 1 <= d.month && d.month <= 12
• Precondition: 1 <= d.day && d.day <= 31
• Postcondition: result._1 >= 1 && result._1 <= 53
• Postcondition: result._2 >= 1 && result._2 <= 7

fn iso8601_ordinal_date(d: &Date) -> (Int, Int)

(year, day_of_year) in ordinal form. Params: d - the date. Returns: the year and the day of the year (1-366). Complexity: O(month).

• Precondition: 1 <= d.month && d.month <= 12
• Precondition: 1 <= d.day && d.day <= 31
• Postcondition: result._1 >= 1 && result._1 <= 366

fn timestamp_iso8601(ts: Int) -> Str

Format the Unix timestamp ts as an ISO-8601 string. Params: ts - seconds since the Unix epoch. Returns: "YYYY-MM-DDTHH:MM:SS" in UTC. Complexity: O(1).

• Postcondition: (ts == 0) => (result == "1970-01-01T00:00:00")

---

---

---

time.xi

type Duration

=== Duration -- a span of time ===

Field	Type
secs	Int
nanos	Int

Derives: Eq, Clone, Ord

fn new(secs: Int, nanos: Int) -> Duration

Duration from whole seconds plus a nanosecond remainder (normalized).

• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn from_secs(s: Int) -> Duration

Duration of s whole seconds.

• Postcondition: result.secs == s && result.nanos == 0

fn from_secs_f64(secs: Float64) -> Duration

Duration from fractional seconds (truncated toward zero).

• Postcondition: (secs >= 0) => (0 <= result.nanos && result.nanos < NANOS_PER_SEC)

fn from_millis(ms: Int) -> Duration

Duration of ms milliseconds.

• Postcondition: result.as_nanos() == ms * NANOS_PER_MILLI
• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn from_micros(us: Int) -> Duration

Duration of us microseconds.

• Postcondition: result.as_nanos() == us * NANOS_PER_MICRO
• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn from_nanos(ns: Int) -> Duration

Duration of ns nanoseconds.

• Postcondition: result.as_nanos() == ns
• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn as_secs(self: Self) -> Int

Whole seconds of the duration.

• Postcondition: result == self.secs

fn as_millis(self: Self) -> Int

Whole milliseconds of the duration.

• Precondition: 0 <= self.nanos && self.nanos < NANOS_PER_SEC

fn as_micros(self: Self) -> Int

Whole microseconds of the duration.

• Precondition: 0 <= self.nanos && self.nanos < NANOS_PER_SEC

fn as_nanos(self: Self) -> Int

Total nanoseconds of the duration.

• Precondition: 0 <= self.nanos && self.nanos < NANOS_PER_SEC

fn as_secs_f64(self: Self) -> Float64

Duration as fractional seconds.

• Precondition: 0 <= self.nanos && self.nanos < NANOS_PER_SEC

fn subsec_nanos(self: Self) -> Int

Nanosecond remainder within the current second.

• Precondition: 0 <= self.nanos && self.nanos < NANOS_PER_SEC
• Postcondition: 0 <= result && result < NANOS_PER_SEC

fn add(self: Self, other: Duration) -> Duration

Sum of two durations.

• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn sub(self: Self, other: Duration) -> Duration

Difference of two durations.

• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn mul(self: Self, factor: Int) -> Duration

Duration multiplied by an integer factor.

• Precondition: factor >= 0
• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn div(self: Self, divisor: Int) -> Duration

Duration divided by an integer divisor.

• Precondition: divisor != 0

fn checked_add(self: Self, other: Duration) -> Option[Duration]

Checked sum; None on overflow.

• Postcondition: result is Some(_) => (0 <= result.value.nanos && result.value.nanos < NANOS_PER_SEC)

fn checked_sub(self: Self, other: Duration) -> Option[Duration]

Checked difference; None when it would be negative.

• Postcondition: result is None => self.as_nanos() < other.as_nanos()
• Postcondition: result is Some(_) => self.as_nanos() >= other.as_nanos()
• Postcondition: result is Some(_) => (0 <= result.value.nanos && result.value.nanos < NANOS_PER_SEC)

fn monotonic_ms() -> Int

Monotonic clock reading in milliseconds since an unspecified epoch. Never decreases and is unaffected by wall-clock adjustments, so it is the supported source for elapsed-time measurement. Backed by the runtime's xiom_async_now_ms (QueryPerformanceCounter on Windows, CLOCK_MONOTONIC on POSIX, clock() fallback); the same source as xiom.async.async_now_ms and xiom.async.timer.Stopwatch. Complexity: O(1). Thread-safe.

• Precondition: true
• Postcondition: result >= 0

type Instant

=== Instant -- a point in time (monotonic clock) ===

Field	Type
t	Int

fn now() -> Instant

The current monotonic instant (millisecond resolution), backed by the runtime monotonic clock (xiom_async_now_ms); immune to wall-clock adjustments. t is milliseconds from the monotonic origin.

• Postcondition: result.t >= 0
• Precondition: true

fn elapsed(self: Self) -> Duration

Time elapsed since this instant (monotonic clock, millisecond resolution).

• Precondition: true
• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC

fn duration_since(self: Self, earlier: Instant) -> Duration

Time from earlier to this instant (millisecond resolution).

• Postcondition: 0 <= result.nanos && result.nanos < NANOS_PER_SEC
• Postcondition: result.as_nanos() == (self.t - earlier.t) * NANOS_PER_MILLI

fn add(self: Self, d: Duration) -> Instant

Instant shifted forward by d (millisecond precision).

• Postcondition: d.as_millis() >= 0 => result.t >= self.t

fn sub(self: Self, d: Duration) -> Instant

Instant shifted backward by d (millisecond precision).

• Postcondition: d.as_millis() >= 0 => result.t <= self.t

type SystemTime

=== SystemTime -- wall clock time ===

Field	Type
secs	Int
nanos	Int

fn now() -> SystemTime

Wall-clock reading (may move backwards when the clock is adjusted).

• Precondition: true
• Postcondition: result.nanos == 0

fn unix_epoch() -> SystemTime

The Unix epoch (1970-01-01T00:00:00Z).

• Postcondition: result.secs == 0 && result.nanos == 0

fn duration_since(self: Self, earlier: SystemTime) -> Result[Duration, Str]

Time from earlier to this reading; Err when it precedes it.

• Postcondition: result.is_ok == (self.secs > earlier.secs || (self.secs == earlier.secs && self.nanos >= earlier.nanos))
• Postcondition: result.is_ok => (0 <= result.value.nanos && result.value.nanos < NANOS_PER_SEC)

fn secs_since_epoch(self: Self) -> Int

Whole seconds since the Unix epoch.

• Postcondition: result == self.secs

type DateTime

=== DateTime -- calendar date and time ===

Field	Type
year	Int
month	Int
day	Int
hour	Int
minute	Int
second	Int
weekday	Int

fn now() -> DateTime

Current UTC date and time.

• Precondition: true
• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: 0 <= result.hour && result.hour < 24
• Postcondition: 0 <= result.minute && result.minute < 60
• Postcondition: 0 <= result.second && result.second < 60
• Postcondition: 0 <= result.weekday && result.weekday < 7

fn year(self: Self) -> Int

Year component (UTC).

• Postcondition: result == self.year

fn month(self: Self) -> Int

Month component 1..12 (UTC).

• Postcondition: 1 <= result && result <= 12

fn day(self: Self) -> Int

Day-of-month component 1..31 (UTC).

• Postcondition: 1 <= result && result <= 31

fn hour(self: Self) -> Int

Hour component 0..23 (UTC).

• Postcondition: 0 <= result && result < 24

fn minute(self: Self) -> Int

Minute component 0..59 (UTC).

• Postcondition: 0 <= result && result < 60

fn second(self: Self) -> Int

Second component 0..59 (UTC).

• Postcondition: 0 <= result && result < 60

fn weekday(self: Self) -> Int

Numeric day of week.

• Postcondition: 0 <= result && result < 7

fn utc_now() -> DateTime

Current UTC DateTime (alias of DateTime.now).

• Precondition: true
• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: 0 <= result.hour && result.hour < 24
• Postcondition: 0 <= result.minute && result.minute < 60
• Postcondition: 0 <= result.second && result.second < 60
• Postcondition: 0 <= result.weekday && result.weekday < 7

fn datetime_from_epoch(epoch: Int) -> DateTime

DateTime from a Unix epoch (seconds since 1970-01-01T00:00:00Z) in UTC. Public wrapper over the calendar decomposition; local-time conversion in xiom.time.tz builds on it.

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: 0 <= result.hour && result.hour < 24
• Postcondition: 0 <= result.minute && result.minute < 60
• Postcondition: 0 <= result.second && result.second < 60
• Postcondition: 0 <= result.weekday && result.weekday < 7

fn local_now() -> DateTime

local_now is the UTC alias for backward compatibility; real local wall-clock conversion lives in xiom.time.tz (tzdata phase 1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31
• Postcondition: 0 <= result.hour && result.hour < 24
• Postcondition: 0 <= result.minute && result.minute < 60
• Postcondition: 0 <= result.second && result.second < 60
• Postcondition: 0 <= result.weekday && result.weekday < 7

fn sleep(dur: Duration)

=== Sleep / Wait === Sleep for the given duration (blocking; millisecond resolution -- a sub-millisecond duration returns immediately, and the nanos field is truncated to whole milliseconds).

• Precondition: true

fn sleep_ms(ms: Int)

Sleep for ms milliseconds (blocking; millisecond resolution). A non-positive value returns immediately.

• Precondition: true

fn sleep_until(instant: Instant)

Sleep until the given monotonic instant (millisecond resolution -- instant.t is a monotonic millisecond reading, so this compares the same clock the instant was taken from).

• Precondition: true

type Date

Date -- calendar date (year, month, day) with day-number arithmetic on the proleptic Gregorian calendar.

Field	Type
year	Int
month	Int
day	Int

fn date_new(year: Int, month: Int, day: Int) -> Date

date_new creates a Date from year, month, day. The caller supplies a calendar month (1-12) and day (1-31); the fields are stored unchanged, with no further validation. Complexity: O(1).

• Precondition: 1 <= month && month <= 12
• Precondition: 1 <= day && day <= 31
• Postcondition: result.year == year
• Postcondition: result.month == month
• Postcondition: result.day == day

fn date_now() -> Date

date_now returns the current date computed from the Unix timestamp. Complexity: O(1). Uses time(0) for the system clock.

• Precondition: true
• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31

fn date_year(d: &Date) -> Int

date_year returns the year field of a Date. Complexity: O(1).

• Postcondition: result == d.year

fn date_month(d: &Date) -> Int

date_month returns the month field of a Date (1-12). Complexity: O(1).

• Precondition: 1 <= d.month && d.month <= 12
• Postcondition: 1 <= result && result <= 12

fn date_day(d: &Date) -> Int

date_day returns the day-of-month field of a Date (1-31). Complexity: O(1).

• Precondition: 1 <= d.day && d.day <= 31
• Postcondition: 1 <= result && result <= 31

fn date_is_leap_year(year: Int) -> Bool

date_is_leap_year returns true if the given year is a leap year in the proleptic Gregorian calendar. Complexity: O(1).

• Postcondition: result == (year % 400 == 0 || (year % 4 == 0 && year % 100 != 0))

fn date_days_in_month(year: Int, month: Int) -> Int

date_days_in_month returns the number of days in the given month of the given year (1..31). Valid for proleptic Gregorian. Complexity: O(1).

• Postcondition: 28 <= result && result <= 31

fn date_day_of_week(year: Int, month: Int, day: Int) -> Int

date_day_of_week returns the day of the week for the given date using Zeller's congruence (Gregorian). 0 = Sunday, ..., 6 = Saturday. Complexity: O(1).

• Postcondition: 0 <= result && result <= 6

fn date_day_of_year(year: Int, month: Int, day: Int) -> Int

date_day_of_year returns the ordinal day of the year (1-366) for the given date. Complexity: O(1).

• Postcondition: (1 <= day && day <= 31 && 1 <= month && month <= 12) => (1 <= result && result <= 366)

fn date_iso8601(d: &Date) -> Str

date_iso8601 formats a Date as a zero-padded "YYYY-MM-DD" string. Complexity: O(1). No dynamic allocation overhead beyond str_concat.

• Postcondition: (0 <= d.year && d.year <= 9999) => result.len() == 10

fn date_from_iso8601(s: Str) -> Option[Date]

date_from_iso8601 parses a "YYYY-MM-DD" string into a Date. Returns None if the format is malformed or values out of range. Complexity: O(1).

• Postcondition: result is Some(_) => (1 <= result.value.month && result.value.month <= 12)
• Postcondition: result is Some(_) => (1 <= result.value.day && result.value.day <= 31)

fn date_add_days(d: &Date, days: Int) -> Date

date_add_days returns a new Date offset by the given number of days. Handles negative days correctly. Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31

fn date_diff_days(a: &Date, b: &Date) -> Int

date_diff_days returns the number of days between a and b (a - b). Complexity: O(1).

• Postcondition: (a.year == b.year && a.month == b.month && a.day == b.day) => result == 0

fn date_compare(a: &Date, b: &Date) -> Int

date_compare compares two dates. Returns -1 if a < b, 0 if equal, 1 if a > b. Complexity: O(1).

• Postcondition: (0 - 1) <= result && result <= 1

fn unix_timestamp() -> Int

unix_timestamp returns the current Unix timestamp (seconds since epoch). Delegates to the C time(2) call. Complexity: O(1).

• Precondition: true

fn timestamp_to_date(ts: Int) -> Date

timestamp_to_date converts a Unix timestamp (seconds) to a Date. Uses the existing civil_from_days calendar decomposition. Complexity: O(1).

• Postcondition: 1 <= result.month && result.month <= 12
• Postcondition: 1 <= result.day && result.day <= 31

fn date_to_timestamp(d: &Date) -> Int

date_to_timestamp converts a Date to a Unix timestamp (0:00:00 UTC). Complexity: O(1).

• Postcondition: result % SECS_PER_DAY == 0

fn iso8601_now() -> Str

iso8601_now returns the current date as an ISO-8601 "YYYY-MM-DD" string. Complexity: O(1).

• Postcondition: result.len() >= 10

fn format_timestamp(ts: Int) -> Str

format_timestamp formats a Unix timestamp as a human-readable date-time string "YYYY-MM-DD HH:MM:SS" (UTC). Complexity: O(1).

• Postcondition: result.len() >= 19

fn strftime(spec: Str, d: &Date) -> Str

Format a Date per the supported conversion set (see the module comment).

• Postcondition: spec.len() == 0 => result.len() == 0

type DateParse

Parse a date per the supported conversion set (see the module comment). Returns None when the input does not match the spec, the month/day are out of range, or the spec uses an unsupported conversion. Result struct instead of Option[Date]: Option-of-struct payloads collide with Option[Int] in combined programs (COMPILER_BUGS.md BUG 12 family).

Field	Type
is_ok	Bool
date	Date

fn strptime(s: Str, spec: Str) -> DateParse

Parse a date/time string with a strftime-style spec; unparsed fields are left at their defaults with the error set.

• Postcondition: result.is_ok => (1 <= result.date.month && result.date.month <= 12)
• Postcondition: result.is_ok => (1 <= result.date.day && result.date.day <= 31)
• Postcondition: !result.is_ok => (result.date.month == 1 && result.date.day == 1)

---

---

tz.xi

fn tz_offset_secs_at(epoch: Int) -> Result[Int, Str]

Local offset from UTC in seconds at an explicit Unix epoch (DST-aware). Positive means local time is ahead of UTC.

• Postcondition: result.is_ok => ((0 - 43200) <= result.value && result.value <= 50400)
• Postcondition: result.is_err => result.error.len() > 0

fn tz_local_offset_secs() -> Result[Int, Str]

Current local offset from UTC in seconds (DST-aware for the host zone).

• Postcondition: result.is_ok => ((0 - 43200) <= result.value && result.value <= 50400)
• Postcondition: result.is_err => result.error.len() > 0

fn tz_is_dst() -> Result[Bool, Str]

True when the host zone is currently observing daylight saving time.

• Postcondition: result.is_err => result.error.len() > 0

fn tz_local_epoch_secs() -> Result[Int, Str]

Current local Unix epoch (UTC seconds + local offset).

• Postcondition: result.is_err => result.error.len() > 0

fn tz_local_now() -> Result[DateTime, Str]

Current local wall-clock DateTime for the host zone.

• Postcondition: result.is_ok => (1 <= result.value.month && result.value.month <= 12)
• Postcondition: result.is_ok => (1 <= result.value.day && result.value.day <= 31)
• Postcondition: result.is_err => result.error.len() > 0

---

---

---