krabka_verified/recovery/
should_capture_first_downgrade.rs

1use {super::ReplayCursorDecision, crate::restore::restore_batch_step, creusot_std::prelude::*};
2
3/// Validate one decoded replay batch and compute its exclusive next cursor.
4///
5/// Compacted logs may contain forward gaps. Overlap, malformed spans, batches
6/// outside the captured replay bound, and an unrepresentable successor stop
7/// replay without advancing.
8#[ensures(match result {
9    ReplayCursorDecision::Advance(next_offset) => match batch {
10        Some((base, last_delta)) => cursor@ < end@
11            && last_delta@ >= 0
12            && base@ >= cursor@
13            && next_offset@ == base@ + last_delta@ + 1
14            && next_offset@ > cursor@
15            && next_offset@ <= end@,
16        None => false,
17    },
18    ReplayCursorDecision::Stop => match batch {
19        None => true,
20        Some((base, last_delta)) => cursor@ >= end@
21            || last_delta@ < 0
22            || base@ < cursor@
23            || base@ + last_delta@ + 1 > i64::MAX@
24            || base@ + last_delta@ + 1 > end@,
25    },
26})]
27#[must_use]
28pub fn replay_batch_cursor_decision(
29    cursor: i64,
30    end: i64,
31    batch: Option<(i64, i32)>,
32) -> ReplayCursorDecision {
33    if cursor >= end {
34        return ReplayCursorDecision::Stop;
35    }
36    let Some((base, last_delta)) = batch else {
37        return ReplayCursorDecision::Stop;
38    };
39    let Some(next) = restore_batch_step(cursor, base, last_delta) else {
40        return ReplayCursorDecision::Stop;
41    };
42    if next > end {
43        ReplayCursorDecision::Stop
44    } else {
45        ReplayCursorDecision::Advance(next)
46    }
47}
48
49/// Capture a metadata-version downgrade snapshot only for the first downgrade
50/// replay meets; a later downgrade never replaces the pending one.
51#[ensures(result == (!pending_exists && is_downgrade))]
52#[must_use]
53pub const fn should_capture_first_downgrade(pending_exists: bool, is_downgrade: bool) -> bool {
54    !pending_exists && is_downgrade
55}
krabka_verified/recovery/should_capture_first_downgrade.rs

krabka_verified/recovery/
should_capture_first_downgrade.rs
