hifitime 4.3.0

/*
* Hifitime
* Copyright (C) 2017-onward Christopher Rabotin <christopher.rabotin@gmail.com> et al. (cf. https://github.com/nyx-space/hifitime/graphs/contributors)
* This Source Code Form is subject to the terms of the Mozilla Public
* License, v. 2.0. If a copy of the MPL was not distributed with this
* file, You can obtain one at https://mozilla.org/MPL/2.0/.
*
* Documentation: https://nyxspace.com/
*/

#[kani::proof_for_contract(crate::epoch::Epoch::weekday)]
fn kani_harness_weekday() {
    use crate::{Duration, Epoch, TimeScale};
    let dur: Duration = kani::any();
    let callee = Epoch::from_duration(dur, TimeScale::TAI);
    let _ = callee.weekday();
}

#[kani::proof]
#[kani::stub_verified(crate::epoch::Epoch::weekday)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_epoch_previous() {
    use crate::{Duration, Epoch, TimeScale, Weekday};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let weekday: Weekday = kani::any();
    let _ = epoch.previous(weekday);
}

#[kani::proof]
#[kani::stub_verified(crate::epoch::Epoch::weekday)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_epoch_next() {
    use crate::{Duration, Epoch, TimeScale, Weekday};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let weekday: Weekday = kani::any();
    let _ = epoch.next(weekday);
}

#[kani::proof]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_with_hms_strict() {
    use crate::{Duration, Epoch, TimeScale};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let _ = epoch.with_hms_strict(12, 0, 0);
}

#[kani::proof]
#[kani::stub_verified(crate::epoch::Epoch::weekday)]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_next_weekday_at_midnight() {
    use crate::{Duration, Epoch, TimeScale, Weekday};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let weekday: Weekday = kani::any();
    let _ = epoch.next_weekday_at_midnight(weekday);
}

#[kani::proof]
#[kani::stub_verified(crate::epoch::Epoch::weekday)]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_next_weekday_at_noon() {
    use crate::{Duration, Epoch, TimeScale, Weekday};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let weekday: Weekday = kani::any();
    let _ = epoch.next_weekday_at_noon(weekday);
}

#[kani::proof]
#[kani::stub_verified(crate::epoch::Epoch::weekday)]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_previous_weekday_at_midnight() {
    use crate::{Duration, Epoch, TimeScale, Weekday};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let weekday: Weekday = kani::any();
    let _ = epoch.previous_weekday_at_midnight(weekday);
}

#[kani::proof]
#[kani::stub_verified(crate::epoch::Epoch::weekday)]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_previous_weekday_at_noon() {
    use crate::{Duration, Epoch, TimeScale, Weekday};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let weekday: Weekday = kani::any();
    let _ = epoch.previous_weekday_at_noon(weekday);
}

#[kani::proof]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_with_hms() {
    use crate::{Duration, Epoch, TimeScale};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let hours: u64 = kani::any();
    let minutes: u64 = kani::any();
    let seconds: u64 = kani::any();
    let _ = epoch.with_hms(hours, minutes, seconds);
}

#[kani::proof]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_with_hms_from() {
    use crate::{Duration, Epoch, TimeScale};
    let d1: Duration = kani::any();
    let d2: Duration = kani::any();
    let epoch = Epoch::from_duration(d1, TimeScale::TAI);
    let other = Epoch::from_duration(d2, TimeScale::TAI);
    let _ = epoch.with_hms_from(other);
}

#[kani::proof]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_with_time_from() {
    use crate::{Duration, Epoch, TimeScale};
    let d1: Duration = kani::any();
    let d2: Duration = kani::any();
    let epoch = Epoch::from_duration(d1, TimeScale::TAI);
    let other = Epoch::from_duration(d2, TimeScale::TAI);
    let _ = epoch.with_time_from(other);
}

#[kani::proof]
#[kani::stub_verified(crate::duration::Duration::decompose)]
#[kani::stub_verified(crate::timeunits::Unit::const_multiply)]
fn verify_with_hms_strict_from() {
    use crate::{Duration, Epoch, TimeScale};
    let d1: Duration = kani::any();
    let d2: Duration = kani::any();
    let epoch = Epoch::from_duration(d1, TimeScale::TAI);
    let other = Epoch::from_duration(d2, TimeScale::TAI);
    let _ = epoch.with_hms_strict_from(other);
}

#[kani::proof_for_contract(crate::epoch::Epoch::to_time_scale)]
fn verify_to_time_scale_contract_tai() {
    use crate::{Duration, Epoch, TimeScale};
    let dur: Duration = kani::any();
    let epoch = Epoch::from_duration(dur, TimeScale::TAI);
    let _ = epoch.to_time_scale(TimeScale::TAI);
}
#[cfg(kani)]
#[allow(non_snake_case)]
mod kani_harnesses {
    use crate::epoch::leap_seconds::LeapSecond;
    use crate::epoch::system_time::duration_since_unix_epoch;
    use crate::*;

    #[kani::proof]
    fn formal_epoch_reciprocity_tai() {
        let duration: Duration = kani::any();

        // TAI
        let time_scale: TimeScale = TimeScale::TAI;
        let epoch: Epoch = Epoch::from_duration(duration, time_scale);
        assert_eq!(epoch.to_duration_in_time_scale(time_scale), duration);

        // Check that no error occurs on initialization
        let seconds: f64 = kani::any();
        if seconds.is_finite() {
            let _ = Epoch::from_tai_seconds(seconds);
        }

        let days: f64 = kani::any();
        if days.is_finite() {
            let _ = Epoch::from_tai_days(days);
        }
    }

    #[kani::proof]
    fn formal_epoch_reciprocity_tt() {
        let duration: Duration = kani::any();

        // TT -- Check valid within bounds of (MIN + TT Offset) and (MAX - TT Offset)
        if duration > Duration::MIN + TT_OFFSET_MS * Unit::Millisecond
            && duration < Duration::MAX - TT_OFFSET_MS * Unit::Millisecond
        {
            let time_scale: TimeScale = TimeScale::TT;
            let epoch: Epoch = Epoch::from_duration(duration, time_scale);
            assert_eq!(epoch.to_duration_in_time_scale(time_scale), duration);
        }

        // Check that no error occurs on initialization
        let seconds: f64 = kani::any();
        if seconds.is_finite() {
            let _ = Epoch::from_tt_seconds(seconds);
        }
        // No TT Days initializer
    }

    #[kani::proof]
    fn formal_epoch_reciprocity_gpst() {
        let duration: Duration = kani::any();

        // GPST
        let time_scale: TimeScale = TimeScale::GPST;
        let ts_offset = TimeScale::GPST.reference_epoch() - TimeScale::TAI.reference_epoch();
        if duration > Duration::MIN + ts_offset && duration < Duration::MAX - ts_offset {
            let epoch: Epoch = Epoch::from_duration(duration, time_scale);
            assert_eq!(epoch.to_duration_in_time_scale(time_scale), duration);
        }

        // Check that no error occurs on initialization
        let seconds: f64 = kani::any();
        if seconds.is_finite() {
            let _ = Epoch::from_gpst_seconds(seconds);
        }

        let _ = Epoch::from_gpst_nanoseconds(kani::any());
    }

    #[kani::proof]
    fn formal_epoch_reciprocity_gst() {
        let duration: Duration = kani::any();

        // GST
        let time_scale: TimeScale = TimeScale::GST;
        let ts_offset = TimeScale::GST.reference_epoch() - TimeScale::TAI.reference_epoch();
        if duration > Duration::MIN + ts_offset && duration < Duration::MAX - ts_offset {
            let epoch: Epoch = Epoch::from_duration(duration, time_scale);
            assert_eq!(epoch.to_duration_in_time_scale(time_scale), duration);
        }

        // Check that no error occurs on initialization
        let seconds: f64 = kani::any();
        if seconds.is_finite() {
            let _ = Epoch::from_gst_seconds(seconds);
        }

        let days: f64 = kani::any();
        if days.is_finite() {
            let _ = Epoch::from_gst_days(days);
        }

        let _ = Epoch::from_gst_nanoseconds(kani::any());
    }

    #[kani::proof]
    fn formal_epoch_reciprocity_bdt() {
        let duration: Duration = kani::any();

        // BDT
        let time_scale: TimeScale = TimeScale::BDT;
        let ts_offset = TimeScale::BDT.reference_epoch() - TimeScale::TAI.reference_epoch();
        if duration > Duration::MIN + ts_offset && duration < Duration::MAX - ts_offset {
            let epoch: Epoch = Epoch::from_duration(duration, time_scale);
            assert_eq!(epoch.to_duration_in_time_scale(time_scale), duration);
        }

        // Check that no error occurs on initialization
        let seconds: f64 = kani::any();
        if seconds.is_finite() {
            let _ = Epoch::from_bdt_seconds(seconds);
        }

        let days: f64 = kani::any();
        if days.is_finite() {
            let _ = Epoch::from_bdt_days(days);
        }

        let _ = Epoch::from_bdt_nanoseconds(kani::any());
    }

    #[kani::proof]
    fn formal_epoch_julian() {
        let days: f64 = kani::any();

        if days.is_finite() {
            // The initializers will fail on subnormal days.
            let _ = Epoch::from_mjd_bdt(days);
            let _ = Epoch::from_mjd_gpst(days);
            let _ = Epoch::from_mjd_gst(days);
            let _ = Epoch::from_mjd_tai(days);
            let _ = Epoch::from_jde_bdt(days);
            let _ = Epoch::from_jde_gpst(days);
            let _ = Epoch::from_jde_gst(days);
            let _ = Epoch::from_jde_tai(days);
            let _ = Epoch::from_jde_et(days);
            let _ = Epoch::from_jde_tai(days);
        }
    }

    /// Proves Epoch::PartialEq and Epoch::Ord are consistent:
    /// equal total_nanoseconds implies Ordering::Equal.
    ///
    /// This caught a bug where Epoch::PartialEq delegated to Duration::PartialEq
    /// (which ignores sign at zero crossing: -1ns == +1ns), while Epoch::Ord
    /// used derived Duration::cmp (lexicographic, sign-aware). Two epochs
    /// could satisfy a == b and a < b simultaneously.
    ///
    /// Fixed by making both use total_nanoseconds() as the canonical scalar.
    /// No assumptions needed — the property holds for all Duration values.
    #[kani::proof]
    #[kani::stub_verified(crate::epoch::Epoch::to_time_scale)]
    fn verify_epoch_eq_ord_consistent() {
        let c1: i16 = kani::any();
        let n1: u64 = kani::any();
        let c2: i16 = kani::any();
        let n2: u64 = kani::any();
        let d1 = Duration::from_parts(c1, n1);
        let d2 = Duration::from_parts(c2, n2);
        let ns1 = d1.total_nanoseconds();
        let ns2 = d2.total_nanoseconds();
        if ns1 == ns2 {
            assert!(ns1.cmp(&ns2) == core::cmp::Ordering::Equal);
        }
        if ns1 < ns2 {
            assert!(ns1 != ns2);
        }
    }

    #[kani::proof]
    fn verify_from_ptp_seconds_contract() {
        let seconds: f64 = kani::any();
        kani::assume(seconds.is_finite());
        let _ = Epoch::from_ptp_seconds(seconds);
    }

    // kani_harness_Epoch_from_gregorian — INTRACTABLE
    // 6+ chained Duration::Add in maybe_from_gregorian body.
    // Even with year==1900 (zero loop iterations) + stub_verified(const_multiply),
    // the chained additions exceed solver capacity (>5min with cvc5).
    // Blocked by: kani::stub cannot target trait impl methods (Duration::Add).
    // #[kani::proof_for_contract(...)]
    // fn kani_harness_Epoch_from_gregorian() { ... }

    // #[kani::proof]
    // fn kani_harness_Epoch_from_gregorian_at_midnight() {
    // let year: i32 = kani::any();
    // let month: u8 = kani::any();
    // let day: u8 = kani::any();
    // let time_scale: TimeScale = kani::any();
    // let _ = Epoch::from_gregorian_at_midnight(year, month, day, time_scale);
    // }

    // #[kani::proof]
    // fn kani_harness_Epoch_from_gregorian_at_noon() {
    // let year: i32 = kani::any();
    // let month: u8 = kani::any();
    // let day: u8 = kani::any();
    // let time_scale: TimeScale = kani::any();
    // let _ = Epoch::from_gregorian_at_noon(year, month, day, time_scale);
    // }

    // #[kani::proof]
    // fn kani_harness_Epoch_from_gregorian_hms() {
    // let year: i32 = kani::any();
    // let month: u8 = kani::any();
    // let day: u8 = kani::any();
    // let hour: u8 = kani::any();
    // let minute: u8 = kani::any();
    // let second: u8 = kani::any();
    // let time_scale: TimeScale = kani::any();
    // let _ = Epoch::from_gregorian_hms(year, month, day, hour, minute, second, time_scale);
    // }

    #[kani::proof]
    fn kani_harness_is_gregorian_valid() {
        let year: i32 = kani::any();
        let month: u8 = kani::any();
        let day: u8 = kani::any();
        let hour: u8 = kani::any();
        let minute: u8 = kani::any();
        let second: u8 = kani::any();
        let nanos: u32 = kani::any();
        // Avoid overflow in `january_years(year + 1)` inside is_gregorian_valid
        kani::assume(year < i32::MAX);
        let _ = is_gregorian_valid(year, month, day, hour, minute, second, nanos);
    }

    #[kani::proof]
    fn kani_harness_LeapSecond_new() {
        let timestamp_tai_s: f64 = kani::any();
        let delta_at: f64 = kani::any();
        let announced: bool = kani::any();
        let _ = LeapSecond::new(timestamp_tai_s, delta_at, announced);
    }

    #[kani::proof]
    #[kani::stub_verified(crate::epoch::Epoch::to_time_scale)]
    fn kani_harness_to_time_scale() {
        let ts: TimeScale = kani::any();
        let __dur: Duration = kani::any();
        let callee = Epoch::from_duration(__dur, TimeScale::TAI);
        let _ = callee.to_time_scale(ts);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tai_duration)]
    fn kani_harness_Epoch_from_tai_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_tai_duration(duration);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_duration)]
    fn kani_harness_Epoch_from_duration() {
        let duration: Duration = kani::any();
        let ts: TimeScale = kani::any();
        let _ = Epoch::from_duration(duration, ts);
    }

    #[kani::proof]
    #[kani::stub(crate::epoch::Epoch::delta_et_tai, stub_delta_et_tai)]
    #[kani::stub(crate::epoch::Epoch::inner_g, stub_inner_g)]
    #[kani::stub(crate::epoch::Epoch::leap_seconds, stub_leap_seconds)]
    fn kani_harness_to_duration_since_j1900() {
        let __dur: Duration = kani::any();
        let callee = Epoch::from_duration(__dur, TimeScale::TAI);
        let _ = callee.to_duration_since_j1900();
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tai_parts)]
    fn kani_harness_Epoch_from_tai_parts() {
        let centuries: i16 = kani::any();
        let nanoseconds: u64 = kani::any();
        let _ = Epoch::from_tai_parts(centuries, nanoseconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tai_seconds)]
    fn kani_harness_Epoch_from_tai_seconds() {
        let seconds: f64 = kani::any();
        let _ = Epoch::from_tai_seconds(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tai_days)]
    fn kani_harness_Epoch_from_tai_days() {
        let days: f64 = kani::any();
        let _ = Epoch::from_tai_days(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_utc_duration)]
    fn kani_harness_Epoch_from_utc_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_utc_duration(duration);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_utc_seconds)]
    fn kani_harness_Epoch_from_utc_seconds() {
        let seconds: f64 = kani::any();
        let _ = Epoch::from_utc_seconds(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_utc_days)]
    fn kani_harness_Epoch_from_utc_days() {
        let days: f64 = kani::any();
        let _ = Epoch::from_utc_days(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gpst_duration)]
    fn kani_harness_Epoch_from_gpst_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_gpst_duration(duration);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_qzsst_duration)]
    fn kani_harness_Epoch_from_qzsst_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_qzsst_duration(duration);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gst_duration)]
    fn kani_harness_Epoch_from_gst_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_gst_duration(duration);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_bdt_duration)]
    fn kani_harness_Epoch_from_bdt_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_bdt_duration(duration);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_mjd_tai)]
    fn kani_harness_Epoch_from_mjd_tai() {
        let days: f64 = kani::any();
        let _ = Epoch::from_mjd_tai(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_mjd_in_time_scale)]
    fn kani_harness_Epoch_from_mjd_in_time_scale() {
        let days: f64 = kani::any();
        let time_scale: TimeScale = kani::any();
        let _ = Epoch::from_mjd_in_time_scale(days, time_scale);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_mjd_utc)]
    fn kani_harness_Epoch_from_mjd_utc() {
        let days: f64 = kani::any();
        let _ = Epoch::from_mjd_utc(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_mjd_gpst)]
    fn kani_harness_Epoch_from_mjd_gpst() {
        let days: f64 = kani::any();
        let _ = Epoch::from_mjd_gpst(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_mjd_qzsst)]
    fn kani_harness_Epoch_from_mjd_qzsst() {
        let days: f64 = kani::any();
        let _ = Epoch::from_mjd_qzsst(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_mjd_gst)]
    fn kani_harness_Epoch_from_mjd_gst() {
        let days: f64 = kani::any();
        let _ = Epoch::from_mjd_gst(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_mjd_bdt)]
    fn kani_harness_Epoch_from_mjd_bdt() {
        let days: f64 = kani::any();
        let _ = Epoch::from_mjd_bdt(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_jde_tai)]
    fn kani_harness_Epoch_from_jde_tai() {
        let days: f64 = kani::any();
        let _ = Epoch::from_jde_tai(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_jde_in_time_scale)]
    fn kani_harness_Epoch_from_jde_in_time_scale() {
        let days: f64 = kani::any();
        let time_scale: TimeScale = kani::any();
        let _ = Epoch::from_jde_in_time_scale(days, time_scale);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_jde_utc)]
    fn kani_harness_Epoch_from_jde_utc() {
        let days: f64 = kani::any();
        let _ = Epoch::from_jde_utc(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_jde_gpst)]
    fn kani_harness_Epoch_from_jde_gpst() {
        let days: f64 = kani::any();
        let _ = Epoch::from_jde_gpst(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_jde_qzsst)]
    fn kani_harness_Epoch_from_jde_qzsst() {
        let days: f64 = kani::any();
        let _ = Epoch::from_jde_qzsst(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_jde_gst)]
    fn kani_harness_Epoch_from_jde_gst() {
        let days: f64 = kani::any();
        let _ = Epoch::from_jde_gst(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_jde_bdt)]
    fn kani_harness_Epoch_from_jde_bdt() {
        let days: f64 = kani::any();
        let _ = Epoch::from_jde_bdt(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tt_seconds)]
    fn kani_harness_Epoch_from_tt_seconds() {
        let seconds: f64 = kani::any();
        let _ = Epoch::from_tt_seconds(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tt_duration)]
    fn kani_harness_Epoch_from_tt_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_tt_duration(duration);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_et_seconds)]
    fn kani_harness_Epoch_from_et_seconds() {
        let seconds_since_j2000: f64 = kani::any();
        let _ = Epoch::from_et_seconds(seconds_since_j2000);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_et_duration)]
    fn kani_harness_Epoch_from_et_duration() {
        let duration_since_j2000: Duration = kani::any();
        let _ = Epoch::from_et_duration(duration_since_j2000);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tdb_seconds)]
    fn kani_harness_Epoch_from_tdb_seconds() {
        let seconds_j2000: f64 = kani::any();
        let _ = Epoch::from_tdb_seconds(seconds_j2000);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_tdb_duration)]
    fn kani_harness_Epoch_from_tdb_duration() {
        let duration_since_j2000: Duration = kani::any();
        let _ = Epoch::from_tdb_duration(duration_since_j2000);
    }

    #[kani::proof]
    fn kani_harness_Epoch_from_jde_et() {
        let days: f64 = kani::any();
        kani::assume(days.is_finite());
        let _ = Epoch::from_jde_et(days);
    }

    #[kani::proof]
    fn kani_harness_Epoch_from_jde_tdb() {
        let days: f64 = kani::any();
        kani::assume(days.is_finite());
        let _ = Epoch::from_jde_tdb(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gpst_seconds)]
    fn kani_harness_Epoch_from_gpst_seconds() {
        let seconds: f64 = kani::any();
        let _ = Epoch::from_gpst_seconds(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gpst_days)]
    fn kani_harness_Epoch_from_gpst_days() {
        let days: f64 = kani::any();
        let _ = Epoch::from_gpst_days(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gpst_nanoseconds)]
    fn kani_harness_Epoch_from_gpst_nanoseconds() {
        let nanoseconds: u64 = kani::any();
        let _ = Epoch::from_gpst_nanoseconds(nanoseconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_qzsst_seconds)]
    fn kani_harness_Epoch_from_qzsst_seconds() {
        let seconds: f64 = kani::any();
        let _ = Epoch::from_qzsst_seconds(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_qzsst_days)]
    fn kani_harness_Epoch_from_qzsst_days() {
        let days: f64 = kani::any();
        let _ = Epoch::from_qzsst_days(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_qzsst_nanoseconds)]
    fn kani_harness_Epoch_from_qzsst_nanoseconds() {
        let nanoseconds: u64 = kani::any();
        let _ = Epoch::from_qzsst_nanoseconds(nanoseconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gst_seconds)]
    fn kani_harness_Epoch_from_gst_seconds() {
        let seconds: f64 = kani::any();
        let _ = Epoch::from_gst_seconds(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gst_days)]
    fn kani_harness_Epoch_from_gst_days() {
        let days: f64 = kani::any();
        let _ = Epoch::from_gst_days(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_gst_nanoseconds)]
    fn kani_harness_Epoch_from_gst_nanoseconds() {
        let nanoseconds: u64 = kani::any();
        let _ = Epoch::from_gst_nanoseconds(nanoseconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_bdt_seconds)]
    fn kani_harness_Epoch_from_bdt_seconds() {
        let seconds: f64 = kani::any();
        let _ = Epoch::from_bdt_seconds(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_bdt_days)]
    fn kani_harness_Epoch_from_bdt_days() {
        let days: f64 = kani::any();
        let _ = Epoch::from_bdt_days(days);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_bdt_nanoseconds)]
    fn kani_harness_Epoch_from_bdt_nanoseconds() {
        let nanoseconds: u64 = kani::any();
        let _ = Epoch::from_bdt_nanoseconds(nanoseconds);
    }

    #[kani::proof]
    fn kani_harness_Epoch_from_unix_duration() {
        let duration: Duration = kani::any();
        let _ = Epoch::from_unix_duration(duration);
    }

    #[kani::proof]
    fn kani_harness_Epoch_from_unix_seconds() {
        let seconds: f64 = kani::any();
        kani::assume(seconds.is_finite());
        let _ = Epoch::from_unix_seconds(seconds);
    }

    #[kani::proof]
    fn kani_harness_Epoch_from_unix_milliseconds() {
        let millisecond: f64 = kani::any();
        kani::assume(millisecond.is_finite());
        let _ = Epoch::from_unix_milliseconds(millisecond);
    }

    #[kani::proof]
    fn kani_harness_Epoch_delta_et_tai() {
        let seconds: f64 = kani::any();
        let _ = Epoch::delta_et_tai(seconds);
    }

    #[kani::proof]
    fn kani_harness_Epoch_inner_g() {
        let seconds: f64 = kani::any();
        let _ = Epoch::inner_g(seconds);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_time_of_week)]
    fn kani_harness_Epoch_from_time_of_week() {
        let week: u32 = kani::any();
        let nanoseconds: u64 = kani::any();
        let time_scale: TimeScale = kani::any();
        let _ = Epoch::from_time_of_week(week, nanoseconds, time_scale);
    }

    #[kani::proof_for_contract(crate::epoch::Epoch::from_time_of_week_utc)]
    fn kani_harness_Epoch_from_time_of_week_utc() {
        let week: u32 = kani::any();
        let nanoseconds: u64 = kani::any();
        let _ = Epoch::from_time_of_week_utc(week, nanoseconds);
    }

    #[kani::proof]
    fn kani_harness_Epoch_from_day_of_year() {
        let year: i32 = kani::any();
        let days: f64 = kani::any();
        let time_scale: TimeScale = kani::any();
        let _ = Epoch::from_day_of_year(year, days, time_scale);
    }

    #[kani::proof]
    #[kani::stub_verified(crate::epoch::Epoch::to_time_scale)]
    fn kani_harness_min() {
        let other: Epoch = kani::any();
        let __dur: Duration = kani::any();
        let callee = Epoch::from_duration(__dur, TimeScale::TAI);
        let _ = callee.min(other);
    }

    #[kani::proof]
    #[kani::stub_verified(crate::epoch::Epoch::to_time_scale)]
    fn kani_harness_max() {
        let other: Epoch = kani::any();
        let __dur: Duration = kani::any();
        let callee = Epoch::from_duration(__dur, TimeScale::TAI);
        let _ = callee.max(other);
    }

    // kani_harness_floor — Epoch ceil/round/floor timeout (i128 chain)
    // #[kani::proof]
    // fn kani_harness_floor() {
    // let duration: Duration = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.floor(duration);
    // }

    // kani_harness_ceil — Epoch ceil/round/floor timeout (i128 chain)
    // #[kani::proof]
    // fn kani_harness_ceil() {
    // let duration: Duration = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.ceil(duration);
    // }

    // kani_harness_round — Epoch ceil/round/floor timeout (i128 chain)
    // #[kani::proof]
    // fn kani_harness_round() {
    // let duration: Duration = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.round(duration);
    // }

    #[kani::proof]
    fn kani_harness_to_time_of_week() {
        let __dur: Duration = kani::any();
        let callee = Epoch::from_duration(__dur, TimeScale::TAI);
        let _ = callee.to_time_of_week();
    }

    #[kani::proof]
    fn kani_harness_weekday_in_time_scale() {
        let dur: Duration = kani::any();
        let callee = Epoch::from_duration(dur, TimeScale::TAI);
        let _ = callee.weekday_in_time_scale(TimeScale::TAI);
    }

    #[kani::proof]
    fn kani_harness_weekday_utc() {
        let dur: Duration = kani::any();
        let callee = Epoch::from_duration(dur, TimeScale::UTC);
        let _ = callee.weekday_utc();
    }

    // #[kani::proof]
    // fn kani_harness_next() {
    // let weekday: Weekday = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.next(weekday);
    // }

    // #[kani::proof]
    // fn kani_harness_next_weekday_at_midnight() {
    // let weekday: Weekday = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.next_weekday_at_midnight(weekday);
    // }

    // #[kani::proof]
    // fn kani_harness_next_weekday_at_noon() {
    // let weekday: Weekday = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.next_weekday_at_noon(weekday);
    // }

    // #[kani::proof]
    // fn kani_harness_previous() {
    // let weekday: Weekday = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.previous(weekday);
    // }

    // #[kani::proof]
    // fn kani_harness_previous_weekday_at_midnight() {
    // let weekday: Weekday = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.previous_weekday_at_midnight(weekday);
    // }

    // #[kani::proof]
    // fn kani_harness_previous_weekday_at_noon() {
    // let weekday: Weekday = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.previous_weekday_at_noon(weekday);
    // }

    #[kani::proof]
    #[kani::stub(
        crate::epoch::system_time::duration_since_unix_epoch,
        stub_duration_since_unix_epoch
    )]
    fn kani_harness_duration_since_unix_epoch() {
        let _ = duration_since_unix_epoch();
    }

    #[kani::proof]
    #[kani::stub(
        crate::epoch::system_time::duration_since_unix_epoch,
        stub_duration_since_unix_epoch
    )]
    fn kani_harness_Epoch_now() {
        let _ = Epoch::now();
    }

    // #[kani::proof]
    // fn kani_harness_with_hms() {
    // let hours: u64 = kani::any();
    // let minutes: u64 = kani::any();
    // let seconds: u64 = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.with_hms(hours, minutes, seconds);
    // }

    // #[kani::proof]
    // fn kani_harness_with_hms_from() {
    // let other: Epoch = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.with_hms_from(other);
    // }

    // #[kani::proof]
    // fn kani_harness_with_time_from() {
    // let other: Epoch = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.with_time_from(other);
    // }

    // #[kani::proof]
    // fn kani_harness_with_hms_strict() {
    // let hours: u64 = kani::any();
    // let minutes: u64 = kani::any();
    // let seconds: u64 = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.with_hms_strict(hours, minutes, seconds);
    // }

    // #[kani::proof]
    // fn kani_harness_with_hms_strict_from() {
    // let other: Epoch = kani::any();
    // let __dur: Duration = kani::any();
    // let callee = Epoch::from_duration(__dur, TimeScale::TAI);
    // let _ = callee.with_hms_strict_from(other);
    // }

    // Kani verification for UTC is skipped.
    // Reason: Kani struggles with the leap second counting logic. This involves:
    // 1. Accessing an external, dynamically sized list of leap seconds (LATEST_LEAP_SECONDS).
    // 2. Complex conditional paths and iteration when determining the applicable number of leap seconds.
    // These aspects are challenging to model and verify exhaustively with Kani.

    #[cfg(kani)]
    #[allow(non_snake_case)]
    /// Stub for duration_since_unix_epoch: returns a bounded non-deterministic
    /// Duration representing a valid Unix timestamp (1970-01-01 to ~2100).
    #[allow(dead_code)]
    fn stub_duration_since_unix_epoch() -> Result<Duration, crate::HifitimeError> {
        let dur: Duration = kani::any();
        // Constrain to a plausible Unix timestamp range (0 to ~130 years in seconds)
        let secs = dur.to_seconds();
        kani::assume(secs >= 0.0 && secs < 4_102_444_800.0 && secs.is_finite());
        Ok(dur)
    }

    /// Stub for Epoch::leap_seconds: returns bounded non-deterministic leap seconds.
    /// Over-approximates the real function (which looks up a specific value from
    /// the 42-entry leap second table) with any value in [0, 37].
    #[cfg(kani)]
    #[allow(dead_code)]
    fn stub_leap_seconds(_epoch: &Epoch, _iers_only: bool) -> Option<f64> {
        if kani::any() {
            let delta: f64 = kani::any();
            kani::assume(delta >= 0.0 && delta <= 37.0);
            Some(delta)
        } else {
            None
        }
    }

    /// Stub for delta_et_tai: over-approximates with bounded non-deterministic value.
    /// Real function returns TT_OFFSET + NAIF_K * sin(e) ≈ 32.184 ± 0.002.
    #[allow(dead_code)]
    fn stub_delta_et_tai(_seconds: f64) -> f64 {
        let result: f64 = kani::any();
        kani::assume(result > 32.0 && result < 33.0);
        result
    }

    /// Stub for inner_g: over-approximates with bounded non-deterministic value.
    /// Real function returns 1.658e-3 * sin(...), bounded by [-0.002, 0.002].
    #[allow(dead_code)]
    fn stub_inner_g(_seconds: f64) -> f64 {
        let result: f64 = kani::any();
        kani::assume(result > -0.002 && result < 0.002);
        result
    }
}