krabka_verified/
stamp.rs

1//! Commit-stamp range-index decisions.
2
3#[cfg(creusot)]
4use creusot_std::prelude::{Int, Seq, invariant, logic};
5use creusot_std::prelude::{ensures, requires};
6
7/// Parallel inclusive ranges `[bases[i], lasts[i]]`, each ordered and each
8/// ending before the next begins.
9// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
10#[cfg(creusot)]
11#[cfg_attr(test, mutants::skip)]
12#[logic]
13pub fn sorted_disjoint(bases: Seq<i64>, lasts: Seq<i64>) -> bool {
14    pearlite! {
15        bases.len() == lasts.len()
16            && (forall<i: Int> 0 <= i && i < bases.len() ==> bases[i]@ <= lasts[i]@)
17            && (forall<i: Int> 1 <= i && i < bases.len() ==> lasts[i - 1]@ < bases[i]@)
18    }
19}
20
21/// The `index`th range of the parallel `bases` and `lasts`, or `None` past
22/// the end of either.
23#[ensures(match result {
24    Some((base, last)) => index@ < [email protected]() && index@ < [email protected]()
25        && base == bases@[index@] && last == lasts@[index@],
26    None => [email protected]() <= index@ || [email protected]() <= index@,
27})]
28fn stamp_range(bases: &[i64], lasts: &[i64], index: usize) -> Option<(i64, i64)> {
29    match (bases.get(index), lasts.get(index)) {
30        (Some(&base), Some(&last)) => Some((base, last)),
31        _ => None,
32    }
33}
34
35/// Validate sorted inclusive ranges as individually ordered and pairwise
36/// nonoverlapping.
37#[ensures(result == sorted_disjoint(bases@, lasts@))]
38#[must_use]
39pub fn stamp_ranges_valid(bases: &[i64], lasts: &[i64]) -> bool {
40    if bases.len() != lasts.len() {
41        return false;
42    }
43    let mut index = 0usize;
44    #[invariant(stamp_cursor_in_bounds(bases@, lasts@, index@))]
45    #[invariant(forall<i: Int> 0 <= i && i < index@ ==> bases@[i]@ <= lasts@[i]@)]
46    #[invariant(forall<i: Int> 1 <= i && i < index@ ==> lasts@[i - 1]@ < bases@[i]@)]
47    #[variant([email protected]() - index@)]
48    while index < bases.len() {
49        let Some((base, last)) = stamp_range(bases, lasts, index) else {
50            return false;
51        };
52        if base > last {
53            return false;
54        }
55        if index > 0 {
56            let Some(&previous_last) = lasts.get(index - 1) else {
57                return false;
58            };
59            if previous_last >= base {
60                return false;
61            }
62        }
63        index += 1;
64    }
65    true
66}
67
68/// Return the sorted insertion position for one nonoverlapping range.
69///
70/// `bases` and `lasts` must have equal lengths and describe sorted,
71/// individually ordered, pairwise nonoverlapping inclusive ranges. Use
72/// [`stamp_ranges_valid`] to check these preconditions before calling.
73///
74/// A `lasts` shorter than `bases` breaks the precondition and the answer is
75/// unspecified. Proof annotations do not validate inputs in ordinary Rust
76/// builds.
77#[requires(sorted_disjoint(bases@, lasts@))]
78#[ensures(match result {
79    Some(index) => index@ <= [email protected]()
80        && new_base@ <= new_last@
81        && (forall<i: Int> 0 <= i && i < index@ ==> lasts@[i]@ < new_base@)
82        && (index@ == [email protected]() || new_last@ < bases@[index@]@),
83    None => new_base@ > new_last@
84        || (exists<i: Int> 0 <= i && i < [email protected]()
85            && bases@[i]@ <= new_last@ && new_base@ <= lasts@[i]@),
86})]
87#[must_use]
88pub fn stamp_range_insertion_index(
89    bases: &[i64],
90    lasts: &[i64],
91    new_base: i64,
92    new_last: i64,
93) -> Option<usize> {
94    if new_base > new_last {
95        return None;
96    }
97    let mut index = 0usize;
98    #[invariant(stamp_cursor_in_bounds(bases@, lasts@, index@))]
99    #[invariant(forall<i: Int> 0 <= i && i < index@ ==> lasts@[i]@ < new_base@)]
100    #[variant([email protected]() - index@)]
101    while index < bases.len() {
102        let (base, last) = stamp_range(bases, lasts, index)?;
103        if new_last < base {
104            return Some(index);
105        }
106        if new_base <= last {
107            return None;
108        }
109        index += 1;
110    }
111    Some(index)
112}
113
114/// Find the first range with both exact inclusive boundaries.
115///
116/// `bases` and `lasts` must have equal lengths.
117///
118/// A `lasts` shorter than `bases` breaks the precondition and the answer is
119/// unspecified; equal lengths are a caller precondition, not a runtime check.
120#[requires(stamp_range_arrays_parallel(bases@, lasts@))]
121#[ensures(stamp_lookup_result(
122    result,
123    bases@,
124    lasts@,
125    StampLookupQuery::Exact { base: target_base, last: target_last },
126))]
127#[must_use]
128pub fn exact_stamp_range_index(
129    bases: &[i64],
130    lasts: &[i64],
131    target_base: i64,
132    target_last: i64,
133) -> Option<usize> {
134    let mut index = 0usize;
135    #[invariant(stamp_lookup_cursor_valid(
136        bases@,
137        lasts@,
138        index@,
139        StampLookupQuery::Exact { base: target_base, last: target_last },
140    ))]
141    #[variant([email protected]() - index@)]
142    while index < bases.len() {
143        let (base, last) = stamp_range(bases, lasts, index)?;
144        if base == target_base && last == target_last {
145            return Some(index);
146        }
147        index += 1;
148    }
149    None
150}
151
152/// Find the first inclusive range that covers `offset`.
153///
154/// The slices must have equal lengths; with a shorter `lasts` slice the answer
155/// is unspecified.
156#[requires(stamp_range_arrays_parallel(bases@, lasts@))]
157#[ensures(stamp_lookup_result(
158    result,
159    bases@,
160    lasts@,
161    StampLookupQuery::Covering { offset },
162))]
163#[must_use]
164pub fn covering_stamp_range_index(bases: &[i64], lasts: &[i64], offset: i64) -> Option<usize> {
165    let mut index = 0usize;
166    #[invariant(stamp_lookup_cursor_valid(
167        bases@,
168        lasts@,
169        index@,
170        StampLookupQuery::Covering { offset },
171    ))]
172    #[variant([email protected]() - index@)]
173    while index < bases.len() {
174        let (base, last) = stamp_range(bases, lasts, index)?;
175        if base <= offset && offset <= last {
176            return Some(index);
177        }
178        index += 1;
179    }
180    None
181}
182
183// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
184#[cfg(creusot)]
185#[cfg_attr(test, mutants::skip)]
186#[logic(open(crate))]
187/// Both parallel arrays contain every index before this scan cursor.
188pub(crate) fn stamp_cursor_in_bounds(bases: Seq<i64>, lasts: Seq<i64>, index: Int) -> bool {
189    pearlite! { index <= bases.len() && stamp_range_arrays_parallel(bases, lasts) }
190}
191
192// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
193#[cfg(creusot)]
194#[cfg_attr(test, mutants::skip)]
195#[logic(open)]
196/// Every listed stamp range has one inclusive end.
197pub fn stamp_range_arrays_parallel(bases: Seq<i64>, lasts: Seq<i64>) -> bool {
198    pearlite! { bases.len() == lasts.len() }
199}
200
201#[cfg(creusot)]
202#[derive(Clone, Copy)]
203pub(crate) enum StampLookupQuery {
204    Exact { base: i64, last: i64 },
205    Covering { offset: i64 },
206}
207
208// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
209#[cfg(creusot)]
210#[cfg_attr(test, mutants::skip)]
211#[logic(open(crate))]
212pub(crate) fn stamp_lookup_matches(query: StampLookupQuery, base: i64, last: i64) -> bool {
213    pearlite! { match query {
214        StampLookupQuery::Exact { base: target_base, last: target_last } =>
215            base@ == target_base@ && last@ == target_last@,
216        StampLookupQuery::Covering { offset } => base@ <= offset@ && offset@ <= last@,
217    } }
218}
219
220// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
221#[cfg(creusot)]
222#[cfg_attr(test, mutants::skip)]
223#[logic(open(crate))]
224pub(crate) fn no_stamp_lookup_before(
225    bases: Seq<i64>,
226    lasts: Seq<i64>,
227    count: Int,
228    query: StampLookupQuery,
229) -> bool {
230    pearlite! { forall<i: Int> 0 <= i && i < count
231    ==> !stamp_lookup_matches(query, bases[i], lasts[i]) }
232}
233
234// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
235#[cfg(creusot)]
236#[cfg_attr(test, mutants::skip)]
237#[logic(open(crate))]
238pub(crate) fn stamp_lookup_cursor_valid(
239    bases: Seq<i64>,
240    lasts: Seq<i64>,
241    index: Int,
242    query: StampLookupQuery,
243) -> bool {
244    pearlite! {
245        stamp_cursor_in_bounds(bases, lasts, index)
246            && no_stamp_lookup_before(bases, lasts, index, query)
247    }
248}
249
250// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
251#[cfg(creusot)]
252#[cfg_attr(test, mutants::skip)]
253#[logic(open(crate))]
254pub(crate) fn stamp_lookup_result(
255    result: Option<usize>,
256    bases: Seq<i64>,
257    lasts: Seq<i64>,
258    query: StampLookupQuery,
259) -> bool {
260    pearlite! { match result {
261        Some(index) => index@ < bases.len()
262            && stamp_lookup_matches(query, bases[index@], lasts[index@])
263            && no_stamp_lookup_before(bases, lasts, index@, query),
264        None => no_stamp_lookup_before(bases, lasts, bases.len(), query),
265    } }
266}
267
268#[cfg(test)]
269mod tests {
270    use super::{
271        covering_stamp_range_index, exact_stamp_range_index, stamp_range_insertion_index,
272        stamp_ranges_valid,
273    };
274
275    #[test]
276    fn range_decisions_cover_boundaries_retries_and_malformed_inputs() {
277        let bases = [0, 5, 10];
278        let lasts = [2, 7, 12];
279        assert2::assert!(stamp_ranges_valid(&bases, &lasts));
280        assert2::assert!(!stamp_ranges_valid(&[0, 5], &[2]));
281        assert2::assert!(!stamp_ranges_valid(&[3], &[2]));
282        assert2::assert!(!stamp_ranges_valid(&[0, 2], &[2, 4]));
283        assert2::assert!(stamp_range_insertion_index(&bases, &lasts, 3, 4) == Some(1));
284        assert2::assert!(stamp_range_insertion_index(&bases, &lasts, 8, 9) == Some(2));
285        assert2::assert!(stamp_range_insertion_index(&bases, &lasts, 2, 3).is_none());
286        assert2::assert!(stamp_range_insertion_index(&bases, &lasts, 4, 3).is_none());
287        assert2::assert!(exact_stamp_range_index(&bases, &lasts, 5, 7) == Some(1));
288        assert2::assert!(exact_stamp_range_index(&bases, &lasts, 5, 8).is_none());
289        assert2::assert!(covering_stamp_range_index(&bases, &lasts, 7) == Some(1));
290        assert2::assert!(covering_stamp_range_index(&bases, &lasts, 8).is_none());
291        assert2::assert!(stamp_ranges_valid(&[1], &[1]));
292        assert2::assert!(stamp_range_insertion_index(&[5], &[7], 1, 1) == Some(0));
293        assert2::assert!(stamp_range_insertion_index(&[5], &[7], 10, 10) == Some(1));
294        assert2::assert!(stamp_range_insertion_index(&[5], &[7], 5, 5).is_none());
295        assert2::assert!(stamp_range_insertion_index(&[5], &[7], 4, 5).is_none());
296    }
297}
krabka_verified/stamp.rs

krabka_verified/
stamp.rs
