krabka_verified/
remote_txn.rs

1//! Inclusive interval integrity for remote aborted-transaction indexes.
2
3use creusot_std::prelude::*;
4
5/// Whether an aborted-transaction entry intersects a requested offset range.
6#[krabka_macros::model_type]
7pub enum RemoteTxnOverlapDecision {
8    /// At least one interval is inverted.
9    Invalid,
10    /// Both intervals are valid and do not intersect.
11    Disjoint,
12    /// Both intervals are valid and intersect inclusively.
13    Overlap,
14}
15
16/// Classify the inclusive entry interval `[entry_start, entry_last]` against
17/// the inclusive query interval `[query_from, query_to]`.
18#[ensures(result == RemoteTxnOverlapDecision::Invalid
19    == (entry_start@ > entry_last@ || query_from@ > query_to@))]
20#[ensures(result == RemoteTxnOverlapDecision::Overlap
21    == (entry_start@ <= entry_last@
22        && query_from@ <= query_to@
23        && entry_start@ <= query_to@
24        && entry_last@ >= query_from@))]
25#[ensures(result == RemoteTxnOverlapDecision::Disjoint
26    == (entry_start@ <= entry_last@
27        && query_from@ <= query_to@
28        && (entry_start@ > query_to@ || entry_last@ < query_from@)))]
29#[must_use]
30pub fn remote_txn_overlap_decision(
31    entry_start: i64,
32    entry_last: i64,
33    query_from: i64,
34    query_to: i64,
35) -> RemoteTxnOverlapDecision {
36    if entry_start > entry_last || query_from > query_to {
37        RemoteTxnOverlapDecision::Invalid
38    } else if entry_start <= query_to && entry_last >= query_from {
39        RemoteTxnOverlapDecision::Overlap
40    } else {
41        RemoteTxnOverlapDecision::Disjoint
42    }
43}
44
45#[cfg(test)]
46mod tests {
47    use {super::*, assert2::check};
48
49    #[yare::parameterized(
50        before_range = { 10, 14, 0, 9, RemoteTxnOverlapDecision::Disjoint },
51        overlap_start = { 10, 14, 0, 10, RemoteTxnOverlapDecision::Overlap },
52        exact_single = { 10, 10, 10, 10, RemoteTxnOverlapDecision::Overlap },
53        overlap_end = { 10, 14, 14, 100, RemoteTxnOverlapDecision::Overlap },
54        after_range = { 10, 14, 15, 100, RemoteTxnOverlapDecision::Disjoint },
55        inverted_entry = { 14, 10, 0, 100, RemoteTxnOverlapDecision::Invalid },
56        inverted_query = { 10, 14, 100, 0, RemoteTxnOverlapDecision::Invalid },
57    )]
58    fn overlap_is_inclusive_and_invalid_intervals_fail_closed(
59        entry_start: i64,
60        entry_last: i64,
61        query_from: i64,
62        query_to: i64,
63        expected: RemoteTxnOverlapDecision,
64    ) {
65        check!(
66            remote_txn_overlap_decision(entry_start, entry_last, query_from, query_to) == expected
67        );
68    }
69}
krabka_verified/remote_txn.rs

krabka_verified/
remote_txn.rs
