krabka_verified/wal/
batch_equal.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]
7#[requires(bases.len() == lasts.len())]
8#[requires(0 <= index && index <= bases.len())]
9#[variant(bases.len() - index)]
10fn exact_wal_batch_suffix(
11    bases: Seq<i64>,
12    lasts: Seq<i64>,
13    index: Int,
14    expected: Int,
15    target: Int,
16) -> bool {
17    pearlite! {
18        if index == bases.len() {
19            expected == target
20        } else {
21            bases[index]@ == expected
22                && bases[index] <= lasts[index]
23                && lasts[index] < i64::MAX
24                && exact_wal_batch_suffix(
25                    bases,
26                    lasts,
27                    index + 1,
28                    lasts[index]@ + 1,
29                    target,
30                )
31        }
32    }
33}
34
35/// Check that decoded WAL batches cover exactly one contiguous half-open range.
36#[cfg_attr(creusot, ensures(result == ([email protected]() == [email protected]()
37    && if start@ == target@ {
38        [email protected]() == 0
39    } else {
40        exact_wal_batch_suffix(bases@, lasts@, 0, start@, target@)
41    })))]
42#[cfg_attr(creusot, ensures(result == wal_batch_layout(bases@, lasts@, start@, target@)))]
43#[cfg_attr(creusot, ensures(result ==> forall<i: Int> 0 <= i && i < [email protected]()
44    ==> start@ <= bases@[i]@ && bases@[i]@ <= lasts@[i]@ && lasts@[i]@ < target@))]
45#[cfg_attr(creusot, ensures(result ==> forall<i: Int, j: Int>
46    0 <= i && i < j && j < [email protected]() ==> lasts@[i]@ < bases@[j]@))]
47#[must_use]
48pub fn exact_wal_batch_range(bases: &[i64], lasts: &[i64], start: i64, target: i64) -> bool {
49    if bases.len() != lasts.len() {
50        return false;
51    }
52    if start == target {
53        return matches!(bases.len(), 0);
54    }
55
56    let mut expected = start;
57    let mut i = 0usize;
58    #[cfg_attr(creusot, invariant(i@ <= [email protected]()))]
59    #[cfg_attr(creusot, invariant([email protected]() == [email protected]()))]
60    #[cfg_attr(creusot, invariant(exact_wal_batch_suffix(bases@, lasts@, 0, start@, target@)
61        == exact_wal_batch_suffix(bases@, lasts@, i@, expected@, target@)))]
62    #[cfg_attr(creusot, invariant(expected@ == if i@ == 0 { start@ } else { lasts@[i@ - 1]@ + 1 }))]
63    #[cfg_attr(creusot, invariant(start@ <= expected@))]
64    #[cfg_attr(creusot, invariant(forall<j: Int> 0 <= j && j < i@ ==>
65        start@ <= bases@[j]@ && bases@[j]@ <= lasts@[j]@ && lasts@[j]@ < expected@
66        && lasts@[j] < i64::MAX
67        && bases@[j]@ == if j == 0 { start@ } else { lasts@[j - 1]@ + 1 }))]
68    #[cfg_attr(creusot, invariant(forall<a: Int, b: Int>
69        0 <= a && a < b && b < i@ ==> lasts@[a]@ < bases@[b]@))]
70    #[cfg_attr(creusot, variant([email protected]() - i@))]
71    while i < bases.len() {
72        let (Some(&base), Some(&last)) = (bases.get(i), lasts.get(i)) else {
73            return false;
74        };
75        if base != expected || base > last {
76            return false;
77        }
78        let Some(next) = last.checked_add(1) else {
79            return false;
80        };
81        expected = next;
82        i += 1;
83    }
84    expected == target
85}
86
87// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
88#[cfg(creusot)]
89#[cfg_attr(test, mutants::skip)]
90#[logic(open)]
91// cargo-mutants: #[cfg(creusot)] mathematical layout; not compiled at runtime.
92pub fn wal_batch_layout(bases: Seq<i64>, lasts: Seq<i64>, start: Int, target: Int) -> bool {
93    pearlite! {
94        bases.len() == lasts.len() && if start == target {
95            bases.len() == 0
96        } else {
97            (forall<i: Int> 0 <= i && i < bases.len() ==>
98                bases[i] <= lasts[i] && lasts[i] < i64::MAX
99                && bases[i]@ == if i == 0 { start } else { lasts[i - 1]@ + 1 })
100            && target == if bases.len() == 0 { start } else { lasts[bases.len() - 1]@ + 1 }
101        }
102    }
103}
104
105/// Whole batches may cover an interior logical floor. They must still form
106/// an exact physical prefix ending at `target`; the first batch contains `start`.
107#[cfg_attr(creusot, ensures((result != None) == (
108    0 <= start@ && start@ <= target@ && [email protected]() == [email protected]()
109    && if start == target { [email protected]() == 0 } else {
110        [email protected]() > 0 && 0 <= bases@[0]@ && bases@[0]@ <= start@ && start@ <= lasts@[0]@
111        && wal_batch_layout(bases@, lasts@, bases@[0]@, target@)
112    }
113)))]
114#[cfg_attr(creusot, ensures(match result {
115    None => true,
116    Some(physical) => physical@ == (if [email protected]() == 0 { start@ } else { bases@[0]@ })
117        && 0 <= physical@ && physical@ <= start@ && start@ <= target@
118        && wal_batch_layout(bases@, lasts@, physical@, target@)
119        && (forall<i: Int> 0 <= i && i < [email protected]() ==>
120            physical@ <= bases@[i]@ && bases@[i]@ <= lasts@[i]@ && lasts@[i]@ < target@),
121}))]
122#[cfg_attr(creusot, ensures(match result {
123    None => true,
124    Some(_) => forall<i: Int, j: Int> 0 <= i && i < j && j < [email protected]() ==> lasts@[i]@ < bases@[j]@,
125}))]
126#[must_use]
127pub fn wal_covering_batch_range(
128    bases: &[i64],
129    lasts: &[i64],
130    start: i64,
131    target: i64,
132) -> Option<i64> {
133    if start < 0 || start > target || bases.len() != lasts.len() {
134        return None;
135    }
136    if start == target {
137        return matches!(bases.len(), 0).then_some(start);
138    }
139    let (Some(&first_base), Some(&first_last)) = (bases.first(), lasts.first()) else {
140        return None;
141    };
142    if first_base < 0 || first_base > start || first_last < start {
143        return None;
144    }
145    if !exact_wal_batch_range(bases, lasts, first_base, target) {
146        return None;
147    }
148    Some(first_base)
149}
150
151/// A nonempty checkpoint must end at the observed whole batch's successor.
152/// Its logical floor may lie inside a batch; an empty range is reset at that floor.
153#[ensures(result == (0 <= recovered_start@ && recovered_start@ <= start@
154    && start@ <= end@ && end@ <= recovered_end@
155    && (start == end || (match observed_last { Some(last) => last@ == end@ - 1, None => false }))))]
156#[must_use]
157pub fn wal_checkpoint_range_valid(
158    recovered_start: i64,
159    recovered_end: i64,
160    start: i64,
161    end: i64,
162    observed_last: Option<i64>,
163) -> bool {
164    0 <= recovered_start
165        && recovered_start <= start
166        && start <= end
167        && end <= recovered_end
168        && (start == end || observed_last == end.checked_sub(1))
169}
170
171/// Compare actual encoded batch bytes and their inclusive offset coordinates.
172/// Matching lengths or frontiers alone do not establish the same records.
173#[ensures(result == (left.0 == right.0 && left.1 == right.1 && left.2@ == right.2@))]
174#[must_use]
175pub fn wal_batch_equal(left: (i64, i64, &[u8]), right: (i64, i64, &[u8])) -> bool {
176    if left.0 != right.0 || left.1 != right.1 || left.2.len() != right.2.len() {
177        return false;
178    }
179    let mut i = 0usize;
180    #[invariant(i@ <= left.2@.len())]
181    #[invariant(forall<j: Int> 0 <= j && j < i@ ==> left.2@[j] == right.2@[j])]
182    #[variant(left.2@.len() - i@)]
183    while i < left.2.len() {
184        let (Some(left_byte), Some(right_byte)) = (left.2.get(i), right.2.get(i)) else {
185            return false;
186        };
187        if left_byte != right_byte {
188            return false;
189        }
190        i += 1;
191    }
192    true
193}
krabka_verified/wal/batch_equal.rs

krabka_verified/wal/
batch_equal.rs
