krabka_verified/retention/
coverage.rs

1use creusot_std::prelude::*;
2
3// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
4#[cfg(creusot)]
5#[cfg_attr(test, mutants::skip)]
6#[logic(open)]
7pub fn remote_ranges_valid(ranges: Seq<(i64, i64)>) -> bool {
8    pearlite! { forall<i: Int> 0 <= i && i < ranges.len() ==> ranges[i].0@ <= ranges[i].1@ }
9}
10
11// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
12#[cfg(creusot)]
13#[cfg_attr(test, mutants::skip)]
14#[logic(open)]
15pub fn remote_covers_offset(ranges: Seq<(i64, i64)>, offset: Int) -> bool {
16    pearlite! { exists<i: Int> 0 <= i && i < ranges.len() && ranges[i].0@ <= offset && offset <= ranges[i].1@ }
17}
18
19/// Find the greatest contiguous inclusive coverage rooted at `local_start`.
20///
21/// Sorted ranges may overlap or precede the anchor; obsolete disconnected
22/// prefixes cannot suppress a later anchored component. Reject malformed ranges
23/// anywhere in the listing. Metadata truth, copy completion and bytes are
24/// external.
25#[requires(forall<i: Int, j: Int> 0 <= i && i < j && j < [email protected]()
26    ==> ranges@[i].0@ <= ranges@[j].0@)]
27#[ensures(match result {
28    None => !remote_ranges_valid(ranges@)
29        || forall<i: Int> 0 <= i && i < [email protected]()
30            ==> local_start@ < ranges@[i].0@ || ranges@[i].1@ < local_start@,
31    Some(through) => remote_ranges_valid(ranges@) && local_start@ <= through@
32        && (exists<i: Int> 0 <= i && i < [email protected]() && through == ranges@[i].1)
33        && (forall<offset: Int> local_start@ <= offset && offset <= through@
34            ==> remote_covers_offset(ranges@, offset))
35        && forall<i: Int> 0 <= i && i < [email protected]() && ranges@[i].0@ <= through@ + 1
36            ==> ranges@[i].1@ <= through@,
37})]
38#[must_use]
39pub fn remote_covered_through(ranges: &[(i64, i64)], local_start: i64) -> Option<i64> {
40    let mut i = 0usize;
41    #[invariant(i@ <= [email protected]())]
42    #[invariant(forall<j: Int> 0 <= j && j < i@ ==> ranges@[j].0@ <= ranges@[j].1@)]
43    #[variant([email protected]() - i@)]
44    while i < ranges.len() {
45        if matches!(ranges.get(i), Some(&(start, end)) if start > end) {
46            return None;
47        }
48        i += 1;
49    }
50    let mut covered: Option<i64> = None;
51    i = 0;
52    #[invariant(i@ <= [email protected]())]
53    #[invariant(match covered {
54        None => forall<j: Int> 0 <= j && j < i@ ==> local_start@ < ranges@[j].0@ || ranges@[j].1@ < local_start@,
55        Some(through) => local_start@ <= through@
56            && (exists<j: Int> 0 <= j && j < i@ && through == ranges@[j].1)
57            && (forall<j: Int> 0 <= j && j < i@ ==> ranges@[j].1@ <= through@)
58            && forall<offset: Int> local_start@ <= offset && offset <= through@
59                ==> remote_covers_offset(ranges@, offset),
60    })]
61    #[variant([email protected]() - i@)]
62    while i < ranges.len() {
63        let Some(&(start, end)) = ranges.get(i) else {
64            break;
65        };
66        match covered {
67            None if start <= local_start && local_start <= end => covered = Some(end),
68            None => {}
69            Some(through) if start <= through.saturating_add(1) => {
70                if end > through {
71                    covered = Some(end);
72                }
73            }
74            Some(_through) => {
75                proof_assert!(forall<j: Int> i@ <= j && j < [email protected]() ==> ranges@[j].0@ > _through@ + 1);
76                return covered;
77            }
78        }
79        i += 1;
80    }
81    covered
82}
83
84#[cfg(test)]
85mod tests;
krabka_verified/retention/coverage.rs

krabka_verified/retention/
coverage.rs
