krabka_verified/transaction/
abort_rows.rs

1use creusot_std::prelude::*;
2
3/// Preserve every distinct wire `(producer_id, first_offset)` row exactly
4/// once. The caller has already selected the overlapping transactions.
5#[ensures([email protected]() <= [email protected]())]
6#[ensures(forall<i: Int> 0 <= i && i < [email protected]()
7    ==> exists<j: Int> 0 <= j && j < [email protected]() && result@[i] == rows@[j])]
8#[ensures(forall<i: Int> 0 <= i && i < [email protected]()
9    ==> exists<j: Int> 0 <= j && j < [email protected]() && rows@[i] == result@[j])]
10#[ensures(crate::sequence::distinct(result@))]
11#[must_use]
12pub fn unique_aborted_transaction_rows(rows: &[(i64, i64)]) -> Vec<(i64, i64)> {
13    let mut selected: Vec<(i64, i64)> = Vec::new();
14    let mut index = 0usize;
15    #[invariant(index@ <= [email protected]() && [email protected]() <= index@)]
16    #[invariant(forall<i: Int> 0 <= i && i < [email protected]()
17        ==> exists<j: Int> 0 <= j && j < index@ && selected@[i] == rows@[j])]
18    #[invariant(forall<i: Int> 0 <= i && i < index@
19        ==> exists<j: Int> 0 <= j && j < [email protected]() && rows@[i] == selected@[j])]
20    #[invariant(crate::sequence::distinct(selected@))]
21    #[variant([email protected]() - index@)]
22    while index < rows.len() {
23        let Some(&row) = rows.get(index) else {
24            break;
25        };
26        let mut scan = 0usize;
27        // ponytail: linear duplicate search; use an indexed set if abort
28        // lists become large enough to affect Fetch latency.
29        #[invariant(scan@ <= [email protected]())]
30        #[invariant(forall<j: Int> 0 <= j && j < scan@ ==> selected@[j] != row)]
31        #[variant([email protected]() - scan@)]
32        while scan < selected.len()
33            && !matches!(selected.get(scan), Some(kept) if kept.0 == row.0 && kept.1 == row.1)
34        {
35            scan += 1;
36        }
37        if scan == selected.len() {
38            selected.push(row);
39        }
40        index += 1;
41    }
42    selected
43}
krabka_verified/transaction/abort_rows.rs

krabka_verified/transaction/
abort_rows.rs
