Crate hifitime

Expand description

§Introduction to Hifitime

Hifitime is a powerful Rust and Python library designed for time management. It provides extensive functionalities with precise operations for time calculation in different time scales, making it suitable for engineering and scientific applications where general relativity and time dilation matter. Hifitime guarantees nanosecond precision for 65,536 centuries around the reference epoch of the initialization time scale, e.g. 01 January 1900 for TAI. Hifitime is also formally verified using the Kani model checker, read more about it this verification here.

Most users of Hifitime will only need to rely on the Epoch and Duration structures, and optionally the Weekday enum for week based computations. Scientific applications may make use of the TimeScale enum as well.

§Usage

First, install hifitime either with cargo add hifitime in your Rust project or pip install hifitime in Python.

If building from source, note that the Python package is only built if the python feature is enabled.

§Epoch (“datetime” equivalent)

Create an epoch in different time scales.

use hifitime::prelude::*;
use core::str::FromStr;
// Create an epoch in UTC
let epoch = Epoch::from_gregorian_utc(2000, 2, 29, 14, 57, 29, 37);
// Or from a string
let epoch_from_str = Epoch::from_str("2000-02-29T14:57:29.000000037 UTC").unwrap();
assert_eq!(epoch, epoch_from_str);
// Creating it from TAI will effectively show the number of leap seconds in between UTC an TAI at that epoch
let epoch_tai = Epoch::from_gregorian_tai(2000, 2, 29, 14, 57, 29, 37);
// The difference between two epochs is a Duration
let num_leap_s = epoch - epoch_tai;
assert_eq!(format!("{num_leap_s}"), "32 s");

// Trivially convert to another time scale
// Either by grabbing a subdivision of time in that time scale
assert_eq!(epoch.to_gpst_days(), 7359.623402777777); // Compare to the GPS time scale

// Or by fetching the exact duration
let mjd_offset = Duration::from_str("51603 days 14 h 58 min 33 s 184 ms 37 ns").unwrap();
assert_eq!(epoch.to_mjd_tt_duration(), mjd_offset); // Compare to the modified Julian days in the Terrestrial Time time scale.

In Python:

>>> from hifitime import *
>>> epoch = Epoch("2000-02-29T14:57:29.000000037 UTC")
>>> epoch
2000-02-29T14:57:29.000000037 UTC
>>> epoch_tai = Epoch.init_from_gregorian_tai(2000, 2, 29, 14, 57, 29, 37)
>>> epoch_tai
2000-02-29T14:57:29.000000037 TAI
>>> epoch.timedelta(epoch_tai)
32 s
>>> epoch.to_gpst_days()
7359.623402777777
>>> epoch.to_mjd_tt_duration()
51603 days 14 h 58 min 33 s 184 ms 37 ns
>>>

Hifitime provides several date time formats like RFC2822, ISO8601, or RFC3339.

use hifitime::efmt::consts::{ISO8601, RFC2822, RFC3339};
use hifitime::prelude::*;

let epoch = Epoch::from_gregorian_utc(2000, 2, 29, 14, 57, 29, 37);
// The default Display shows the UTC time scale
assert_eq!(format!("{epoch}"), "2000-02-29T14:57:29.000000037 UTC");
// Format it in RFC 2822
let fmt = Formatter::new(epoch, RFC2822);
assert_eq!(format!("{fmt}"), format!("Tue, 29 Feb 2000 14:57:29"));

// Or in ISO8601
let fmt = Formatter::new(epoch, ISO8601);
assert_eq!(
    format!("{fmt}"),
    format!("2000-02-29T14:57:29.000000037 UTC")
);

// Which is somewhat similar to RFC3339
let fmt = Formatter::new(epoch, RFC3339);
assert_eq!(
    format!("{fmt}"),
    format!("2000-02-29T14:57:29.000000037+00:00")
);

Need some custom format? Hifitime also supports the C89 token, cf. the documentation.

use core::str::FromStr;
use hifitime::prelude::*;

let epoch = Epoch::from_gregorian_utc_hms(2015, 2, 7, 11, 22, 33);

// Parsing with a custom format
assert_eq!(
    Epoch::from_format_str("Sat, 07 Feb 2015 11:22:33", "%a, %d %b %Y %H:%M:%S").unwrap(),
    epoch
);

// And printing with a custom format
let fmt = Format::from_str("%a, %d %b %Y %H:%M:%S").unwrap();
assert_eq!(
    format!("{}", Formatter::new(epoch, fmt)),
    "Sat, 07 Feb 2015 11:22:33"
);

You can also grab the current system time in UTC, if the std feature is enabled (default), and find the next or previous day of the week.

use hifitime::prelude::*;

#[cfg(feature = "std")]
{
    let now = Epoch::now().unwrap();
    println!("{}", now.next(Weekday::Tuesday));
    println!("{}", now.previous(Weekday::Sunday));
}

Oftentimes, we’ll want to query something at a fixed step between two epochs. Hifitime makes this trivial with TimeSeries.

use hifitime::prelude::*;

let start = Epoch::from_gregorian_utc_at_midnight(2017, 1, 14);
let end = start + 12.hours();
let step = 2.hours();

let time_series = TimeSeries::inclusive(start, end, step);
let mut cnt = 0;
for epoch in time_series {
    #[cfg(feature = "std")]
    println!("{}", epoch);
    cnt += 1
}
// Check that there are indeed seven two-hour periods in a half a day,
// including start and end times.
assert_eq!(cnt, 7)

In Python:

>>> from hifitime import *
>>> start = Epoch.init_from_gregorian_utc_at_midnight(2017, 1, 14)
>>> end = start + Unit.Hour*12
>>> iterator = TimeSeries(start, end, step=Unit.Hour*2, inclusive=True)
>>> for epoch in iterator:
...     print(epoch)
...
2017-01-14T00:00:00 UTC
2017-01-14T02:00:00 UTC
2017-01-14T04:00:00 UTC
2017-01-14T06:00:00 UTC
2017-01-14T08:00:00 UTC
2017-01-14T10:00:00 UTC
2017-01-14T12:00:00 UTC
>>>

§Duration

use hifitime::prelude::*;
use core::str::FromStr;

// Create a duration using the `TimeUnits` helping trait.
let d = 5.minutes() + 7.minutes() + 35.nanoseconds();
assert_eq!(format!("{d}"), "12 min 35 ns");

// Or using the built-in enums
let d_enum = 12 * Unit::Minute + 35.0 * Unit::Nanosecond;

// But it can also be created from a string
let d_from_str = Duration::from_str("12 min 35 ns").unwrap();
assert_eq!(d, d_from_str);

Hifitime guarantees nanosecond precision, but most human applications don’t care too much about that. Durations can be rounded to provide a useful approximation for humans.

use hifitime::prelude::*;

// Create a duration using the `TimeUnits` helping trait.
let d = 5.minutes() + 7.minutes() + 35.nanoseconds();
// Round to the nearest minute
let rounded = d.round(1.minutes());
assert_eq!(format!("{rounded}"), "12 min");

// And this works on Epochs as well.
let previous_post = Epoch::from_gregorian_utc_hms(2015, 2, 7, 11, 22, 33);
let example_now = Epoch::from_gregorian_utc_hms(2015, 8, 17, 22, 55, 01);

// We'll round to the nearest fifteen days
let this_much_ago = example_now - previous_post;
assert_eq!(format!("{this_much_ago}"), "191 days 11 h 32 min 28 s");
let about_this_much_ago_floor = this_much_ago.floor(15.days());
assert_eq!(format!("{about_this_much_ago_floor}"), "180 days");
let about_this_much_ago_ceil = this_much_ago.ceil(15.days());
assert_eq!(format!("{about_this_much_ago_ceil}"), "195 days");

In Python:

>>> from hifitime import *
>>> d = Duration("12 min 32 ns")
>>> d.round(Unit.Minute*1)
12 min
>>> d
12 min 32 ns
>>>

§Comparison with `time` and `chrono`

First off, both time and chrono are fantastic libraries in their own right. There’s a reason why they have millions and millions of downloads. Secondly, hifitime was started in October 2017, so quite a while before the revival of time (~ 2019).

One of the key differences is that both chrono and time separate the concepts of “time” and “date.” Hifitime asserts that this is physically invalid: both a time and a date are an offset from a reference in a given time scale. That’s why, Hifitime does not separate the components that make up a date, but instead, only stores a fixed duration with respect to TAI. Moreover, Hifitime is formally verified with a model checker, which is much more thorough than property testing.

More importantly, neither time nor chrono are suitable for astronomy, astrodynamics, or any physics that must account for time dilation due to relativistic speeds or lack of the Earth as a gravity source (which sets the “tick” of a second).

Hifitime also natively supports the UT1 time scale (the only “true” time) if built with the ut1 feature.

§Features

Initialize a high precision Epoch from the system time in UTC
Leap seconds (as announced by the IETF on a yearly basis)
UTC representation with ISO8601 and RFC3339 formatting and blazing fast parsing (45 nanoseconds)
Trivial support of time arithmetic: addition (e.g. 2.hours() + 3.seconds()), subtraction (e.g. 2.hours() - 3.seconds()), round/floor/ceil operations (e.g. 2.hours().round(3.seconds()))
Supports ranges of Epochs and TimeSeries (linspace of Epochs and Durations)
Trivial conversion between many time scales
High fidelity Ephemeris Time / Dynamic Barycentric Time (TDB) computations from ESA’s Navipedia
Julian dates and Modified Julian dates
Embedded device friendly: no-std and const fn where possible

This library is validated against NASA/NAIF SPICE for the Ephemeris Time to Universal Coordinated Time computations: there are exactly zero nanoseconds of difference between SPICE and hifitime for the computation of ET and UTC after 01 January 1972. Refer to the leap second section for details. Other examples are validated with external references, as detailed on a test-by-test basis.

§Supported time scales

Temps Atomique International (TAI)
Universal Coordinated Time (UTC)
Terrestrial Time (TT)
Ephemeris Time (ET) without the small perturbations as per NASA/NAIF SPICE leap seconds kernel
Dynamic Barycentric Time (TDB), a higher fidelity ephemeris time
Global Positioning System (GPST)
Galileo System Time (GST)
BeiDou Time (BDT)
UNIX

Hifitime offers means to convert between time scales coarsely and precisely. The Polynomial structure allows description of the state of a Timescale with respect to a reference, as typically needed by precise applications or Timescale monitoring & maintenance.

§Non-features

Time-agnostic / date-only epochs. Hifitime only supports the combination of date and time, but the Epoch::{at_midnight, at_noon} is provided as helper functions.

§Design

No software is perfect, so please report any issue or bug on Github.

§Duration

Under the hood, a Duration is represented as a 16 bit signed integer of centuries (i16) and a 64 bit unsigned integer (u64) of the nanoseconds past that century. The overflowing and underflowing of nanoseconds is handled by changing the number of centuries such that the nanoseconds number never represents more than one century (just over four centuries can be stored in 64 bits).

Advantages:

Exact precision of a duration: using a floating point value would cause large durations (e.g. Julian Dates) to have less precision than smaller durations. Durations in hifitime have exactly one nanosecond of precision for 65,536 centuries.
Skipping floating point operations allows this library to be used in embedded devices without a floating point unit.
Duration arithmetics are exact, e.g. one third of an hour is exactly twenty minutes and not “0.33333 hours.”

Disadvantages:

Most astrodynamics applications require the computation of a duration in floating point values such as when querying an ephemeris. This design leads to an overhead of about 5.2 nanoseconds according to the benchmarks (Duration to f64 seconds benchmark). You may run the benchmarks with cargo bench.

§Epoch

The Epoch stores a duration with respect to the reference of a time scale, and that time scale itself. For monotonic time on th Earth, Standard of Fundamental Astronomy (SOFA) recommends of opting for a glitch-free time scale like TAI (i.e. without discontinuities like leap seconds or non-uniform seconds like TDB).

§Leap second support

Leap seconds allow TAI (the absolute time reference) and UTC (the civil time reference) to not drift too much. In short, UTC allows humans to see the sun at zenith at noon, whereas TAI does not worry about that. Leap seconds are introduced to allow for UTC to catch up with the absolute time reference of TAI. Specifically, UTC clocks are “stopped” for one second to make up for the accumulated difference between TAI and UTC. These leap seconds are announced several months in advance by IERS, cf. in the IETF leap second reference.

The “placement” of these leap seconds in the formatting of a UTC date is left up to the software: there is no common way to handle this. Some software prevents a second tick, i.e. at 23:59:59 the UTC clock will tick for two seconds (instead of one) before hoping to 00:00:00. Some software, like hifitime, allow UTC dates to be formatted as 23:59:60 on strictly the days when a leap second is inserted. For example, the date 2016-12-31 23:59:60 UTC is a valid date in hifitime because a leap second was inserted on 01 Jan 2017.

As of version 4.1.2, you may call LatestLeapSeconds::default().is_up_to_date() in Rust and LatestLeapSeconds().is_up_to_date() in Python to check that Hifitime is up to date with the latest leap seconds. In Rust, you’ll need to enable the lts (long term support) crate feature.

§Important

Prior to the first leap second, NAIF SPICE claims that there were nine seconds of difference between TAI and UTC: this is different from the Standard of Fundamental Astronomy (SOFA). SOFA’s iauDat function will return non-integer leap seconds from 1960 to 1972. It will return an error for dates prior to 1960. Hifitime only accounts for leap seconds announced by IERS in its computations: there is a ten (10) second jump between TAI and UTC on 01 January 1972. This allows the computation of UNIX time to be a specific offset of TAI in hifitime. However, the prehistoric (pre-1972) leap seconds as returned by SOFA are available in the leap_seconds() method of an epoch if the iers_only parameter is set to false.

§Ephemeris Time vs Dynamic Barycentric Time (TDB)

In theory, as of January 2000, ET and TDB should now be identical. However, the NASA NAIF leap seconds files (e.g. naif00012.tls) use a simplified algorithm to compute the TDB:

Equation [4], which ignores small-period fluctuations, is accurate to about 0.000030 seconds.

In order to provide full interoperability with NAIF, hifitime uses the NAIF algorithm for “ephemeris time” and the ESA algorithm for “dynamical barycentric time.” Hence, if exact NAIF behavior is needed, use all of the functions marked as et instead of the tdb functions, such as epoch.to_et_seconds() instead of epoch.to_tdb_seconds().

§Formal Verification with Kani

Hifitime uses the Kani model checker for formal verification. The verification harnesses serve two purposes:

Panic-freedom proofs (#[kani::proof]): Most harnesses verify that functions do not panic for any possible input. These use kani::any() to generate fully symbolic inputs and call the function under test. They prove the absence of arithmetic overflow, division by zero, out-of-bounds access, and other runtime failures across the entire input space.

Functional correctness contracts (#[kani::ensures] + #[kani::proof_for_contract]): Selected functions have formal specifications attached directly to the function signature. These contracts express postconditions that the function must satisfy, for example, that total_nanoseconds() returns centuries * NPC + nanoseconds, or that Duration::min returns a value no greater than either input. The proof_for_contract harnesses verify these contracts for all inputs, enabling compositional verification: callers can rely on the contract without re-verifying the implementation.

Loop contracts (#[kani::loop_invariant]): The Duration::Mul<f64> precision-finding loop is annotated with a loop invariant that bounds the iteration variable, enabling Kani to verify termination inductively rather than by unrolling.

§Important Update on Versioning Strategy

We want to inform our users of an important change in Hifitime’s versioning approach. Starting with version 3.9.0, minor version updates may include changes that could potentially break backward compatibility. While we strive to maintain stability and minimize disruptions, this change allows us to incorporate significant improvements and adapt more swiftly to evolving user needs. We recommend users to carefully review the release notes for each update, even minor ones, to understand any potential impacts on their existing implementations. Our commitment to providing a robust and dynamic time management library remains steadfast, and we believe this change in versioning will better serve the evolving demands of our community.

§Development

Thanks for considering to help out on Hifitime!

For Rust development, cargo is all you need, along with build tools for the minimum supported Rust version.

§Python development

First, please install maturin and set up a Python virtual environment from which to develop. Also make sure that the package version in Cargo.toml is greater than any published version. For example, if the latest version published on PyPi is 4.0.0-a.0 (for alpha-0), make sure that you change the Cargo.toml file such that you’re at least in version alpha-1, or the pip install will download from PyPi instead of installing from the local folder. To run the Python tests, you must install pytest in your virtual environment.

The exact steps should be:

Jump into the virtual environment: source .venv/bin/activate (e.g.)
Make sure pytest is installed: pip install pytest
Build hifitime specifying the output folder of the Python egg: maturin build -F python --out dist
Install the egg: pip install dist/hifitime-4.0.0.alpha1-cp311-cp311-linux_x86_64.whl
Run the tests using the environmental pytest: .venv/bin/pytest

§Type hinting

Hifitime uses the approach from dora to enable type hinting in IDEs. This approach requires running maturin twice: once to generate to the bindings and a second time for it to incorporate the pyi file.

maturin develop -F python;
python generate_stubs.py hifitime hifitime.pyi;
maturin develop

Re-exports§

pub use errors::DurationError;
pub use errors::HifitimeError;
pub use errors::ParsingError;
pub use crate::Freq;
pub use crate::Frequencies;
pub use crate::TimeUnits;
pub use crate::Unit;

Modules§

efmt
errors
initializers
leap_seconds
ops
parse
prelude
pythonpython
ut1ut1

Structs§

Duration: Defines generally usable durations for nanosecond precision valid for 32,768 centuries in either direction, and only on 80 bits / 10 octets.
Epoch: Defines a nanosecond-precision Epoch.
Polynomial: Interpolation Polynomial used for example in TimeScale maintenance, precise monitoring or conversions.
TimeSeries: An iterator of a sequence of evenly spaced Epochs.

Enums§

Freq: An Enum to convert frequencies to their approximate duration, rounded to the closest nanosecond.
MonthName: Defines Month names, can be initialized either from its variant or its integer (1 for January).
TimeScale: Enum of the different time systems available
Unit: An Enum to perform time unit conversions.
Weekday

Constants§

BDT_REF_EPOCH: BDT(BeiDou): 2005 Dec 31st Midnight BDT (BeiDou) reference epoch is 2005 December 31st UTC at midnight. This time scale is synchronized with UTC. |UTC - TAI| = XX Leap Seconds on that day.
DAYS_GPS_TAI_OFFSET
DAYS_PER_CENTURY: DAYS_PER_CENTURY corresponds to the number of days per century in the Julian calendar.
DAYS_PER_CENTURY_I64
DAYS_PER_CENTURY_U64
DAYS_PER_WEEK
DAYS_PER_WEEK_I64
DAYS_PER_YEAR: DAYS_PER_YEAR corresponds to the number of days per year in the Julian calendar.
DAYS_PER_YEAR_NLD: DAYS_PER_YEAR_NLD corresponds to the number of days per year without leap days.
ELB
ET_EPOCH_S: The Ephemeris Time epoch, in seconds
GPST_REF_EPOCH
GST_REF_EPOCH: GST (Galileo) reference epoch is 13 seconds before 1999 August 21 UTC at midnight. |UTC - TAI| = XX Leap Seconds on that day.
J1900_REF_EPOCH: The J1900 reference epoch (1900-01-01 at noon) TAI.
J2000_REF_EPOCH: The J2000 reference epoch (2000-01-01 at midnight) TAI. |UTC - TAI| = XX Leap Seconds on that day.
JD_J1900: Julian date for the J1900 epoch, as per NAIF SPICE.
JD_J2000: Julian date for the J2000 epoch, as per NAIF SPICE.
JD_J1900_NOON: Sum of J19000 and MJD_OFFSET, J1900 at noon.
LB: L_B = 1 - d(TDB)/d(TCB)
LG: L_G = 1 - d(TT)/d(TCG)
MJD_J1900: Julian days between 01 Jan 1900 at midnight and the Modified Julian Day at 17 November 1858.
MJD_J2000: Julian days between 01 Jan 2000 at noon and the Modified Julian Day at 17 November 1858.
MJD_OFFSET: Modified Julian Date in seconds as defined here. MJD epoch is Modified Julian Day at 17 November 1858 at midnight.
NAIF_EB: NAIF leap second kernel data for EB used to calculate the eccentric anomaly of the heliocentric orbit of the Earth-Moon barycenter.
NAIF_K: NAIF leap second kernel data used to calculate the difference between ET and TAI.
NAIF_M0: NAIF leap second kernel data for M_0 used to calculate the mean anomaly of the heliocentric orbit of the Earth-Moon barycenter.
NAIF_M1: NAIF leap second kernel data for M_1 used to calculate the mean anomaly of the heliocentric orbit of the Earth-Moon barycenter.
NANOSECONDS_PER_CENTURY
NANOSECONDS_PER_DAY
NANOSECONDS_PER_HOUR
NANOSECONDS_PER_MICROSECOND
NANOSECONDS_PER_MILLISECOND
NANOSECONDS_PER_MINUTE
NANOSECONDS_PER_SECOND
QZSST_REF_EPOCH: QZSS and GPS share the same reference epoch.
SECONDS_BDT_TAI_OFFSET
SECONDS_BDT_TAI_OFFSET_I64
SECONDS_GPS_TAI_OFFSET
SECONDS_GPS_TAI_OFFSET_I64
SECONDS_GST_TAI_OFFSET
SECONDS_GST_TAI_OFFSET_I64
SECONDS_PER_CENTURY: SECONDS_PER_CENTURY defines the number of seconds per century.
SECONDS_PER_DAY: SECONDS_PER_DAY defines the number of seconds per day.
SECONDS_PER_DAY_I64
SECONDS_PER_HOUR: SECONDS_PER_HOUR defines the number of seconds per hour.
SECONDS_PER_MINUTE: SECONDS_PER_MINUTE defines the number of seconds per minute.
SECONDS_PER_SIDEREAL_YEAR: SECONDS_PER_SIDEREAL_YEAR corresponds to the number of seconds per sidereal year from NIST.
SECONDS_PER_TROPICAL_YEAR: SECONDS_PER_TROPICAL_YEAR corresponds to the number of seconds per tropical year from NAIF SPICE.
SECONDS_PER_YEAR: SECONDS_PER_YEAR corresponds to the number of seconds per julian year from NAIF SPICE.
SECONDS_PER_YEAR_I64
TDB0_S: TDB0 is the TDB offset at TAI 1977-01-01 00:00:00 (s)
UNIX_REF_EPOCH: The UNIX reference epoch of 1970-01-01 in TAI duration, accounting only for IERS leap seconds.

Traits§

Frequencies: A trait to automatically convert some primitives to an approximate frequency as a duration.
TimeUnits: A trait to automatically convert some primitives to a duration

Functions§

is_gregorian_valid: Returns true if the provided Gregorian date is valid. Leap second days may have 60 seconds.

Crate hifitime

Crate hifitime Copy item path

§Introduction to Hifitime

§Usage

§Epoch (“datetime” equivalent)

§Duration

§Comparison with time and chrono

§Features

§Supported time scales

§Non-features

§Design

§Duration

§Epoch

§Leap second support

§Important

§Ephemeris Time vs Dynamic Barycentric Time (TDB)

§Formal Verification with Kani

§Important Update on Versioning Strategy

§Development

§Python development

§Type hinting

Re-exports§

Modules§

Structs§

Enums§

Constants§

Traits§

Functions§

Crate hifitime

§Comparison with `time` and `chrono`