Skip to main content

krabka_verified/retention/
remote_floor.rs

1use {super::retention_delete_target, creusot_std::prelude::*};
2
3/// Extend a deletion floor through one completed whole-range delete.
4///
5/// A gap, malformed coordinates or an unrepresentable successor closes the
6/// contiguous run permanently. Completion and truthful metadata are host facts.
7#[ensures(current@ <= result.0@)]
8#[ensures(result.1 == (contiguous && current@ >= 0 && start@ >= 0
9    && start@ <= end@ && start@ <= current@ && end@ < i64::MAX@))]
10#[ensures(if result.1 { result.0@ == [email protected](end@ + 1) } else { result.0 == current })]
11#[ensures(forall<offset: Int> current@ <= offset && offset < result.0@
12    ==> start@ <= offset && offset <= end@)]
13#[must_use]
14pub fn remote_retention_floor_step(
15    current: i64,
16    contiguous: bool,
17    start: i64,
18    end: i64,
19) -> (i64, bool) {
20    if !contiguous || current < 0 || start < 0 || start > end || start > current {
21        return (current, false);
22    }
23    let Some(target) = retention_delete_target(Some(end)) else {
24        return (current, false);
25    };
26    (current.max(target), true)
27}