krabka_verified/producer/
completion.rs

1use creusot_std::prelude::*;
2
3#[cfg(creusot)]
4mod coverage;
5
6// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
7#[cfg(creusot)]
8#[cfg_attr(test, mutants::skip)]
9#[logic(open)]
10pub fn completion_offset(ends: Seq<i64>, incoming: i64, index: Int) -> Int {
11    pearlite! { if index == ends.len() { incoming@ } else { ends[index]@ } }
12}
13
14/// Name source membership so coverage laws have a term for each old origin.
15// cargo-mutants: #[cfg(creusot)] logical predicate; not compiled outside Creusot.
16#[cfg(creusot)]
17#[cfg_attr(test, mutants::skip)]
18#[logic]
19#[ensures(result == (exists<j: Int> 0 <= j && j < selected.len() && selected[j]@ == source))]
20pub fn completion_source_selected(selected: Seq<usize>, source: Int) -> bool {
21    pearlite! { exists<j: Int> 0 <= j && j < selected.len() && selected[j]@ == source }
22}
23
24/// Merge a deferred data completion into the current epoch's retry window.
25///
26/// The returned indices name old batches, or `ends.len()` for the incoming
27/// batch. Equal physical offsets keep the existing metadata. Earlier
28/// completions cannot displace a newer batch; only the five greatest distinct
29/// offsets survive. A lower epoch preserves the old window and is rejected. The
30/// host supplies sorted retained batches and a truthful incoming batch.
31#[requires([email protected]() <= 5)]
32#[requires(current == None ==> [email protected]() == 0)]
33#[requires(crate::sequence::strictly_increasing(ends@))]
34#[ensures(result.0 == (completion_epoch_accepts(current, epoch)))]
35#[ensures(completion_window_bounded(result.1@, result.0))]
36#[ensures(forall<j: Int> 0 <= j && j < result.1@.len() ==>
37    result.1@[j]@ <= [email protected]()
38    && (result.1@[j]@ < [email protected]() ==> current != None
39        && match current { Some(value) => epoch@ <= value@, None => false })
40    && (result.1@[j]@ == [email protected]() ==> result.0
41        && !(match current { Some(value) => value == epoch
42            && exists<i: Int> 0 <= i && i < [email protected]() && ends@[i] == incoming, None => false })))]
43#[ensures(forall<i: Int, j: Int> 0 <= i && i < j && j < result.1@.len() ==>
44    completion_offset(ends@, incoming, result.1@[i]@)
45        < completion_offset(ends@, incoming, result.1@[j]@))]
46#[ensures(forall<i: Int> 0 <= i && i < [email protected]()
47    && (match current { Some(value) => epoch@ <= value@, None => false })
48    && !completion_source_selected(result.1@, i) ==>
49        five_completions_above(ends@, incoming, result.1@, ends@[i]@))]
50#[ensures(result.0 && !(exists<j: Int> 0 <= j && j < result.1@.len()
51    && completion_offset(ends@, incoming, result.1@[j]@) == incoming@) ==>
52        five_completions_above(ends@, incoming, result.1@, incoming@))]
53#[ensures(!result.0 ==> result.1@.len() == [email protected]()
54    && (forall<j: Int> 0 <= j && j < [email protected]() ==> result.1@[j]@ == j))]
55#[must_use]
56pub fn producer_completion_window(
57    current: Option<i16>,
58    epoch: i16,
59    ends: &[i64],
60    incoming: i64,
61) -> (bool, Vec<usize>) {
62    let count = ends.len();
63    let keep_old = matches!(current, Some(value) if epoch <= value);
64    let accepted = !matches!(current, Some(value) if value > epoch);
65    let mut position = 0usize;
66    #[invariant(position@ <= count@)]
67    #[invariant(forall<i: Int> 0 <= i && i < position@ ==> ends@[i]@ < incoming@)]
68    #[variant(count@ - position@)]
69    while position < count && matches!(ends.get(position), Some(&end) if end < incoming) {
70        position += 1;
71    }
72    proof_assert!(forall<i: Int> position@ <= i && i < count@ ==> incoming@ <= ends@[i]@);
73    let insert = accepted
74        && (!keep_old
75            || position == count
76            || !matches!(ends.get(position), Some(&end) if end == incoming));
77    let length = if keep_old { count } else { 0 } + usize::from(insert);
78    let first = length.saturating_sub(5);
79    let mut selected: Vec<usize> = Vec::with_capacity(length - first);
80    let mut ordinal = first;
81    #[invariant(first@ <= ordinal@ && ordinal@ <= length@ && [email protected]() == ordinal@ - first@)]
82    #[invariant(forall<j: Int> 0 <= j && j < [email protected]() ==> selected@[j]@ ==
83        if !keep_old || (insert && first@ + j == position@) { count@ }
84        else if insert && first@ + j > position@ { first@ + j - 1 }
85        else { first@ + j })]
86    #[variant(length@ - ordinal@)]
87    while ordinal < length {
88        let source = if !keep_old || (insert && ordinal == position) {
89            count
90        } else if insert && ordinal > position {
91            ordinal - 1
92        } else {
93            ordinal
94        };
95        selected.push(source);
96        ordinal += 1;
97    }
98    if !keep_old {
99        proof_assert!([email protected]() == 1 && selected@[0]@ == count@);
100        return (accepted, selected);
101    }
102    if !insert {
103        proof_assert!([email protected]() == [email protected]()
104            && (forall<j: Int> 0 <= j && j < [email protected]() ==> selected@[j]@ == j));
105        #[cfg(creusot)]
106        proof_assert!(coverage::lemma_identity_window(selected@));
107        // Expose source membership directly to the eviction postcondition.
108        proof_assert!(forall<i: Int> 0 <= i && i < [email protected]()
109            ==> completion_source_selected(selected@, i));
110        proof_assert!(accepted ==>
111            position@ < [email protected]() && selected@[position@]@ == position@ && ends@[position@] == incoming);
112        return (accepted, selected);
113    }
114    proof_assert!(forall<i: Int> position@ <= i && i < count@ ==> incoming@ < ends@[i]@);
115    proof_assert!(first@ == (if count@ == 5 { 1 } else { 0 })
116        && [email protected]() == [email protected]() + 1 - first@);
117    proof_assert!(forall<j: Int> 0 <= j && j < [email protected]() ==>
118        selected@[j]@ == if first@ + j == position@ { [email protected]() }
119        else if first@ + j > position@ { first@ + j - 1 } else { first@ + j });
120    #[cfg(creusot)]
121    proof_assert!(coverage::lemma_inserted_window(ends@, incoming, position@, first@, selected@));
122    (accepted, selected)
123}
124
125// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
126#[cfg(creusot)]
127#[cfg_attr(test, mutants::skip)]
128#[logic(open)]
129/// A physical completion is accepted only at the current epoch or a newer epoch.
130pub(crate) fn completion_epoch_accepts(current: Option<i16>, incoming: i16) -> bool {
131    pearlite! { match current { None => true, Some(previous) => previous@ <= incoming@ } }
132}
133
134// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
135#[cfg(creusot)]
136#[cfg_attr(test, mutants::skip)]
137#[logic(open)]
138/// A completion retains at most five entries and every accepted completion retains one.
139pub(crate) fn completion_window_bounded(selected: Seq<usize>, accepted: bool) -> bool {
140    pearlite! { selected.len() <= 5 && (accepted ==> selected.len() > 0) }
141}
142
143// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
144#[cfg(creusot)]
145#[cfg_attr(test, mutants::skip)]
146#[logic(open)]
147/// All five retained completions are strictly above the omitted source.
148fn five_completions_above(
149    ends: Seq<i64>,
150    incoming: i64,
151    selected: Seq<usize>,
152    candidate: Int,
153) -> bool {
154    pearlite! { selected.len() == 5 && (forall<j: Int> 0 <= j && j < selected.len() ==> candidate < completion_offset(ends, incoming, selected[j]@)) }
155}
krabka_verified/producer/completion.rs

krabka_verified/producer/
completion.rs
