krabka_verified/
epoch.rs

1//! Exact, overflow-safe advancement for signed metadata epochs.
2
3#[cfg(creusot)]
4use creusot_std::prelude::ensures;
5
6/// Return the exact successor of `current` when it fits below `maximum`.
7///
8/// The explicit maximum lets narrower host fields, such as Kafka `int32`
9/// epochs, use the same proved `i64` primitive as barrier epochs.
10#[must_use]
11#[cfg_attr(
12    creusot,
13    ensures(match result {
14        Some(next) => current@ < maximum@ && next@ == current@ + 1 && next@ <= maximum@,
15        None => current@ >= maximum@,
16    })
17)]
18pub const fn exact_epoch_successor(current: i64, maximum: i64) -> Option<i64> {
19    if current < maximum {
20        Some(current + 1)
21    } else {
22        None
23    }
24}
25
26#[cfg(test)]
27mod tests {
28    use super::exact_epoch_successor;
29
30    #[yare::parameterized(
31        negative = { -1, i64::from(i32::MAX), Some(0) },
32        zero = { 0, i64::from(i32::MAX), Some(1) },
33        ordinary = { 41, i64::from(i32::MAX), Some(42) },
34        maximum = { i64::from(i32::MAX) - 1, i64::from(i32::MAX), Some(i64::from(i32::MAX)) },
35        i64_max = { i64::MAX - 1, i64::MAX, Some(i64::MAX) },
36    )]
37    fn returns_the_exact_successor(current: i64, maximum: i64, expected: Option<i64>) {
38        assert2::assert!(exact_epoch_successor(current, maximum) == expected);
39    }
40
41    #[test]
42    fn rejects_the_maximum_and_values_above_it() {
43        assert2::assert!(exact_epoch_successor(i64::from(i32::MAX), i64::from(i32::MAX)).is_none());
44        assert2::assert!(exact_epoch_successor(i64::MAX, i64::MAX).is_none());
45        assert2::assert!(exact_epoch_successor(7, 6).is_none());
46    }
47}
krabka_verified/epoch.rs

krabka_verified/
epoch.rs
