4.3.0: Relativistic time scales (TCG/TCB), Lunar Time (TL+TCL), thorough formal verification

[ChristopherRabotin]

New Features

• Timeseries: expose first and last Epochs without consuming iterator by @gwbres in Timeseries: expose first and last Epochs without consuming iterator #465
• Implement TCG and TCB Support by @ChristopherRabotin in Implement TCG and TCB Support #480
• Implement Lunar Time and Lunar Coordinated Time (experimental scales) by @ChristopherRabotin in Implement Lunar Time and Lunar Coordinated Time (experimental scales) #482

Bug fixes

• Enable strptime parsing for compact strings without separators by @ChristopherRabotin in Enable strptime parsing for compact strings without separators #464
• Fix Duration::PartialEq/Ord inconsistency by removing zero-crossing special case by @feliperodri in Fix Duration::PartialEq/Ord inconsistency by removing zero-crossing special case #473 -- Importantly: in hifitime < 4.3.0, negative durations were reported as equal; 4.3.0 changes that behavior for formality reasons
• fix: rewrite try_truncated_nanoseconds using total_nanoseconds() for correct boundary handling by @vmagueta in fix: rewrite try_truncated_nanoseconds using total_nanoseconds() for correct boundary handling #476

Improvements / Formal verification

• Add Function Contracts to 19 Hifitime Functions by @feliperodri in Add Function Contracts to 19 Hifitime Functions #467
• Fix 4 bugs found by Kani function contract proofs by @feliperodri in Fix 4 bugs found by Kani function contract proofs #466
• Add contracts to 49 Epoch initializers and 3 Duration accessors by @feliperodri in Add contracts to 49 Epoch initializers and 3 Duration accessors #468
• Clean up Kani verification — resolve all warnings, failures, and compilation errors by @feliperodri in Clean up Kani verification — resolve all warnings, failures, and compilation errors #474
• Resolve 20 timeout harnesses using stub_verified, cvc5, and TAI Epoch construction by @feliperodri in Resolve 20 timeout harnesses using stub_verified, cvc5, and TAI Epoch construction #477
• Resolve timeout harnesses with contracts, loop invariants, and compositional verification by @feliperodri in Resolve timeout harnesses with contracts, loop invariants, and compositional verification #479
• 153 proofs passing, delete redundant harnesses, add Duration::approx proof by @feliperodri in 153 proofs passing, delete redundant harnesses, add Duration::approx proof #481

New Contributors

• @feliperodri made their first contribution in Add Function Contracts to 19 Hifitime Functions #467
• @vmagueta made their first contribution in fix: rewrite try_truncated_nanoseconds using total_nanoseconds() for correct boundary handling #476

Full Changelog: 4.2.6...4.3.0

---

This discussion was created from the release 4.3.0: Relativistic time scales (TCG/TCB), Lunar Time (TL+TCL), thorough formal verification.