1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
//! Polynomial Duration wrapper used in interpolation processes
use crate::Duration;
use core::fmt;
#[cfg(not(feature = "std"))]
use num_traits::Float;
#[cfg(doc)]
use crate::TimeScale;
#[cfg(feature = "serde")]
use serde_derive::{Deserialize, Serialize};
#[cfg(feature = "python")]
use pyo3::prelude::*;
#[cfg(feature = "python")]
use pyo3::types::PyType;
/// Interpolation [Polynomial] used for example in [TimeScale]
/// maintenance, precise monitoring or conversions.
#[derive(Debug, Clone, Copy, PartialEq, PartialOrd, Eq, Ord, Hash)]
#[cfg_attr(feature = "python", pyclass)]
#[cfg_attr(feature = "python", pyo3(module = "hifitime"))]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct Polynomial {
/// Constant offset [Duration], regardless of the interpolation interval
pub constant: Duration,
/// Rate or drift in seconds per second (s.s⁻¹) expressed as [Duration] for convenience.
/// It is a linear scaling factor of the interpolation interval.
pub rate: Duration,
/// Acceleration or drift change in s.s⁻², expressed as [Duration] for convenience.
/// It is a quadratic scaling of the interpolation interval.
pub accel: Duration,
}
impl From<(f64, f64, f64)> for Polynomial {
/// Converts (f64, f64, f64) triplet, oftentimes
/// noted (a0, a1, a2) as (offset (s), drift (s.s⁻¹), drift change (s.s⁻²))
/// to [Polynomial] structure, that allows precise [TimeScale] translation.
fn from(triplet: (f64, f64, f64)) -> Self {
Self {
constant: Duration::from_seconds(triplet.0),
rate: Duration::from_seconds(triplet.1),
accel: Duration::from_seconds(triplet.2),
}
}
}
impl From<Polynomial> for (f64, f64, f64) {
/// Converts [Polynomial] to (f64, f64, f64) triplet, oftentimes
/// noted (a0, a1, a2) as (offset (s), drift (s.s⁻¹), drift change (s.s⁻²)).
fn from(polynomial: Polynomial) -> Self {
(
polynomial.constant.to_seconds(),
polynomial.rate.to_seconds(),
polynomial.accel.to_seconds(),
)
}
}
#[cfg_attr(feature = "python", pymethods)]
impl Polynomial {
/// Calculate the correction (as [Duration] once again) from [Self] and given
/// the interpolation time interval
/// :type time_interval: Duration
/// :rtype: Duration
pub fn correction_duration(&self, time_interval: Duration) -> Duration {
let dt_s = time_interval.to_seconds();
let (a0, a1, a2) = (
self.constant.to_seconds(),
self.rate.to_seconds(),
self.accel.to_seconds(),
);
Duration::from_seconds(a0 + a1 * dt_s + a2 * dt_s.powi(2))
}
}
impl Polynomial {
/// Create a [Polynomial] structure that is only made of a static offset
pub fn from_constant_offset(constant: Duration) -> Self {
Self {
constant,
rate: Default::default(),
accel: Default::default(),
}
}
/// Create a [Polynomial] structure from a static offset expressed in nanoseconds
pub fn from_constant_offset_nanoseconds(nanos: f64) -> Self {
Self {
constant: Duration::from_nanoseconds(nanos),
rate: Default::default(),
accel: Default::default(),
}
}
/// Create a [Polynomial] structure from both static offset and rate of change:
pub fn from_offset_and_rate(constant: Duration, rate: Duration) -> Self {
Self {
constant,
rate,
accel: Default::default(),
}
}
/// Create a [Polynomial] structure from a static offset and drift,
/// in nanoseconds and nanoseconds.s⁻¹
pub fn from_offset_rate_nanoseconds(offset_ns: f64, drift_ns_s: f64) -> Self {
Self {
constant: Duration::from_nanoseconds(offset_ns),
rate: Duration::from_nanoseconds(drift_ns_s),
accel: Default::default(),
}
}
}
impl fmt::Display for Polynomial {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(
f,
"offset={} rate={} accel={}",
self.constant, self.rate, self.accel
)
}
}
#[cfg(feature = "python")]
#[cfg_attr(feature = "python", pymethods)]
impl Polynomial {
/// Create a [Polynomial] structure that is only made of a static offset
/// :type constant: Duration
/// :rtype: Polynomial
#[pyo3(name = "from_constant_offset")]
#[classmethod]
pub fn py_from_constant_offset(_cls: &Bound<'_, PyType>, constant: Duration) -> Self {
Self {
constant,
rate: Default::default(),
accel: Default::default(),
}
}
/// Create a [Polynomial] structure from a static offset expressed in nanoseconds
/// :type nanos: float
/// :rtype: Polynomial
#[pyo3(name = "from_constant_offset_nanoseconds")]
#[classmethod]
pub fn py_from_constant_offset_nanoseconds(_cls: &Bound<'_, PyType>, nanos: f64) -> Self {
Self {
constant: Duration::from_nanoseconds(nanos),
rate: Default::default(),
accel: Default::default(),
}
}
/// Create a [Polynomial] structure from both static offset and rate of change:
/// :type constant: Duration
/// :type rate: Duration
/// :rtype: Polynomial
#[pyo3(name = "from_offset_and_rate")]
#[classmethod]
pub fn py_from_offset_and_rate(
_cls: &Bound<'_, PyType>,
constant: Duration,
rate: Duration,
) -> Self {
Self {
constant,
rate,
accel: Default::default(),
}
}
/// Create a [Polynomial] structure from a static offset and drift, in nanoseconds and nanoseconds.s⁻¹
/// :type offset_ns: float
/// :type drift_ns_s: float
/// :rtype: Polynomial
#[pyo3(name = "from_offset_rate_nanoseconds")]
#[classmethod]
pub fn py_from_offset_rate_nanoseconds(
_cls: &Bound<'_, PyType>,
offset_ns: f64,
drift_ns_s: f64,
) -> Self {
Self {
constant: Duration::from_nanoseconds(offset_ns),
rate: Duration::from_nanoseconds(drift_ns_s),
accel: Default::default(),
}
}
#[cfg(feature = "python")]
fn __str__(&self) -> String {
format!("{self}")
}
#[cfg(feature = "python")]
fn __eq__(&self, other: Self) -> bool {
*self == other
}
}
#[cfg(kani)]
mod kani_verif {
use super::*;
/// Verifies Polynomial::correction_duration does not panic and returns
/// a normalized Duration.
/// Note: proof_for_contract fails with "return_value is not assignable"
/// error, likely a Kani limitation with pymethods impl blocks.
/// Using standalone proof with explicit assertion instead.
#[kani::proof]
#[kani::stub_verified(Duration::from_seconds)]
fn verify_polynomial_correction_duration() {
let constant: Duration = kani::any();
let rate: Duration = kani::any();
let accel: Duration = kani::any();
let interval: Duration = kani::any();
// Verification budget constraints (not function preconditions):
// Restrict to durations within ±1 century (~31.5 years) to ensure
// the polynomial evaluation a0 + a1*dt + a2*dt^2 stays finite.
// The function is correct for all Duration inputs, but without
// stub_verified(to_seconds), CBMC explores paths where to_seconds
// produces values that overflow the polynomial.
kani::assume(constant.to_parts().0 > -1 && constant.to_parts().0 < 1);
kani::assume(rate.to_parts().0 > -1 && rate.to_parts().0 < 1);
kani::assume(accel.to_parts().0 > -1 && accel.to_parts().0 < 1);
kani::assume(interval.to_parts().0 > -1 && interval.to_parts().0 < 1);
let poly = Polynomial {
constant,
rate,
accel,
};
let result = poly.correction_duration(interval);
let (c, n) = result.to_parts();
assert!(
n < crate::NANOSECONDS_PER_CENTURY
|| (c == i16::MAX && n == crate::NANOSECONDS_PER_CENTURY)
|| (c == i16::MIN && n == 0)
);
}
}