krabka_verified/
log_index.rs

1//! Sparse-index lookup kernels.
2//!
3//! These kernels come out of the `OffsetIndex` and `TimeIndex` of `krabka-log`,
4//! so that Creusot can verify them. They use hand-rolled binary searches, the
5//! canonical Creusot loop, and not `binary_search_by_key`. The proofs thus do
6//! not depend on a model of the std search.
7
8use creusot_std::prelude::*;
9
10/// A decoded sparse-index key and the coordinate it selects.
11#[krabka_macros::model_type(runtime(Clone, Copy, Debug, PartialEq, Eq, Hash))]
12pub struct IndexEntry<Key, Coordinate> {
13    pub key: Key,
14    pub coordinate: Coordinate,
15}
16
17impl<Key, Coordinate> IndexEntry<Key, Coordinate> {
18    /// Construct a decoded entry without changing its encoded field order.
19    #[ensures(result.key == key && result.coordinate == coordinate)]
20    #[must_use]
21    pub const fn new(key: Key, coordinate: Coordinate) -> Self { Self { key, coordinate } }
22}
23
24pub type OffsetEntry = IndexEntry<u32, u32>;
25pub type TimeEntry = IndexEntry<i64, u32>;
26pub(crate) type RangeEntry = IndexEntry<i64, i64>;
27
28#[cfg(creusot)]
29// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
30#[cfg_attr(test, mutants::skip)]
31#[logic(open)]
32fn time_keys_nondecreasing(entries: Seq<TimeEntry>) -> bool {
33    pearlite! {
34        forall<i: Int, j: Int> 0 <= i && i < j && j < entries.len()
35            ==> entries[i].key@ <= entries[j].key@
36    }
37}
38
39#[cfg(creusot)]
40// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
41#[cfg_attr(test, mutants::skip)]
42#[logic(open)]
43fn offset_keys_strictly_increasing(entries: Seq<OffsetEntry>) -> bool {
44    pearlite! {
45        forall<i: Int, j: Int> 0 <= i && i < j && j < entries.len()
46            ==> entries[i].key@ < entries[j].key@
47    }
48}
49
50krabka_macros::sorted_index_cursor! {
51    pub(crate) fn upper_offset_cursor(entries: &[OffsetEntry], target: u32) -> usize;
52    <=;
53}
54krabka_macros::sorted_index_cursor! {
55    pub(crate) fn upper_time_cursor(entries: &[TimeEntry], target: i64) -> usize;
56    <=;
57}
58krabka_macros::sorted_index_cursor! {
59    pub(crate) fn upper_range_cursor(entries: &[RangeEntry], target: i64) -> usize;
60    <=;
61}
62krabka_macros::sorted_index_cursor! {
63    pub(crate) fn lower_offset_cursor(entries: &[OffsetEntry], target: u32) -> usize;
64    <;
65}
66
67krabka_macros::index_floor_lookup! {
68    /// The position of the last entry at or below `target`, or zero.
69    /// Entries must be strictly sorted by relative offset.
70    pub fn offset_index_lookup(entries: &[OffsetEntry], target: u32) -> u32;
71    <; upper_offset_cursor;
72}
73krabka_macros::index_floor_lookup! {
74    /// The relative offset of the last entry at or below `target`, or zero.
75    /// Timestamps must be nondecreasing; equal timestamps are allowed.
76    pub fn time_index_lookup(entries: &[TimeEntry], target: i64) -> u32;
77    <=; upper_time_cursor;
78}
79
80/// A safe sparse starting offset for a forward scan seeking
81/// `timestamp >= target`.
82///
83/// Entries carry running maxima. Starting at an equal maximum could skip its
84/// first occurrence, so only a strictly smaller maximum may advance the scan.
85#[cfg_attr(creusot, requires(time_keys_nondecreasing(entries@)))]
86#[ensures((exists<i: Int> 0 <= i && i < [email protected]() && entries@[i].key@ < target_timestamp@)
87    ==> exists<i: Int> 0 <= i && i < [email protected]()
88        && entries@[i].key@ < target_timestamp@
89        && result@ == entries@[i].coordinate@
90        && (forall<j: Int> i < j && j < [email protected]()
91            ==> entries@[j].key@ >= target_timestamp@))]
92#[ensures((forall<i: Int> 0 <= i && i < [email protected]() ==> entries@[i].key@ >= target_timestamp@)
93    ==> result@ == 0)]
94#[must_use]
95pub fn time_index_scan_start(entries: &[TimeEntry], target_timestamp: i64) -> u32 {
96    let Some(before) = target_timestamp.checked_sub(1) else {
97        return 0;
98    };
99    time_index_lookup(entries, before)
100}
101
102/// The byte position of the first entry at or after `target`.
103///
104/// Returns `None` when every entry is below `target`. `entries` must be
105/// strictly sorted by relative offset.
106#[cfg_attr(creusot, requires(offset_keys_strictly_increasing(entries@)))]
107#[ensures((exists<i: Int> 0 <= i && i < [email protected]() && target@ <= entries@[i].key@)
108    ==> exists<i: Int> 0 <= i && i < [email protected]()
109        && target@ <= entries@[i].key@
110        && result == Some(entries@[i].coordinate)
111        && (forall<j: Int> 0 <= j && j < i ==> entries@[j].key@ < target@))]
112#[ensures((forall<i: Int> 0 <= i && i < [email protected]() ==> entries@[i].key@ < target@)
113    ==> result == None)]
114#[must_use]
115pub fn offset_index_position_at_or_after(entries: &[OffsetEntry], target: u32) -> Option<u32> {
116    let lo = lower_offset_cursor(entries, target);
117    let entry = entries.get(lo)?;
118    Some(entry.coordinate)
119}
120
121#[cfg(test)]
122mod tests {
123
124    use {
125        super::*,
126        proptest::{collection, prelude::*},
127        std::collections::BTreeSet,
128    };
129
130    fn offset_lookup_cases() -> impl Strategy<Value = (BTreeSet<u32>, u32)> {
131        (collection::btree_set(0u32..10_000, 0..64), 0u32..10_000)
132    }
133
134    fn offset_entries(rels: &BTreeSet<u32>) -> Vec<OffsetEntry> {
135        rels.iter()
136            .enumerate()
137            .map(|(i, rel)| {
138                IndexEntry::new(
139                    *rel,
140                    u32::try_from(i).expect("btree set length is bounded to 64") * 17,
141                )
142            })
143            .collect()
144    }
145
146    fn offset_floor_oracle(entries: &[OffsetEntry], target: u32) -> u32 {
147        match entries.binary_search_by_key(&target, |entry| entry.key) {
148            Ok(i) => entries[i].coordinate,
149            Err(0) => 0,
150            Err(i) => entries[i - 1].coordinate,
151        }
152    }
153
154    proptest! {
155        #[test]
156        fn lookup_matches_binary_search_oracle(
157            (rels, target) in offset_lookup_cases(),
158        ) {
159            // btree_set gives strictly-sorted unique keys, matching the
160            // OffsetIndex construction invariant.
161            let entries = offset_entries(&rels);
162            prop_assert_eq!(offset_index_lookup(&entries, target), offset_floor_oracle(&entries, target));
163        }
164
165        #[test]
166        fn time_lookup_matches_linear_oracle(
167            timestamps in collection::vec(-10_000i64..10_000, 0..64),
168            target in -10_000i64..10_000,
169        ) {
170            let mut timestamps = timestamps;
171            timestamps.sort_unstable();
172            let entries: Vec<TimeEntry> = timestamps
173                .iter()
174                .enumerate()
175                .map(|(i, timestamp)| {
176                    IndexEntry::new(*timestamp, u32::try_from(i).expect("timestamp list length is bounded to 64") * 17)
177                })
178                .collect();
179            let want = entries
180                .iter()
181                .rfind(|entry| entry.key <= target)
182                .map_or(0, |entry| entry.coordinate);
183            prop_assert_eq!(time_index_lookup(&entries, target), want);
184        }
185
186        #[test]
187        fn position_at_or_after_matches_linear_oracle(
188            (rels, target) in offset_lookup_cases(),
189        ) {
190            let entries = offset_entries(&rels);
191            let want = entries
192                .iter()
193                .find(|entry| entry.key >= target)
194                .map(|entry| entry.coordinate);
195            prop_assert_eq!(offset_index_position_at_or_after(&entries, target), want);
196        }
197    }
198
199    #[test]
200    fn empty_indexes_return_fallbacks() {
201        assert2::assert!(offset_index_lookup(&[], 42) == 0);
202        assert2::assert!(time_index_lookup(&[], 42) == 0);
203        assert2::assert!(offset_index_position_at_or_after(&[], 42) == None);
204    }
205
206    #[test]
207    fn position_at_or_after_exact_match() {
208        let entries = [
209            IndexEntry::new(10, 100),
210            IndexEntry::new(20, 200),
211            IndexEntry::new(30, 300),
212        ];
213        assert2::assert!(offset_index_position_at_or_after(&entries, 20) == Some(200));
214    }
215}
krabka_verified/log_index.rs

krabka_verified/
log_index.rs
