Skip to main content

krabka_verified/list_offsets/
timestamp_candidate.rs

1use creusot_std::prelude::*;
2
3/// Select the earliest matching record across two readable tiers.
4///
5/// Preserve its timestamp, prefer remote on equal offsets, and return no match
6/// exactly when neither tier found one. Tier lookup errors are handled by the
7/// caller before this choice.
8#[ensures((result == None) == (remote == None && local == None))]
9#[ensures(match result {
10    Some((offset, _)) => (result == remote || result == local)
11        && (match remote { Some((r, _)) => offset@ <= r@, None => true })
12        && (match local { Some((l, _)) => offset@ <= l@, None => true }),
13    None => true,
14})]
15#[ensures(match (remote, local) {
16    (Some((r, _)), Some((l, _))) => r@ <= l@ ==> result == remote,
17    _ => true,
18})]
19#[must_use]
20pub fn earliest_timestamp_candidate(
21    remote: Option<(i64, i64)>,
22    local: Option<(i64, i64)>,
23) -> Option<(i64, i64)> {
24    match (remote, local) {
25        (Some(r), Some(l)) if l.0 < r.0 => Some(l),
26        (Some(r), _) => Some(r),
27        (None, l) => l,
28    }
29}