krabka_verified/list_offsets/
selection_decision.rs

1#[cfg(creusot)]
2use super::list_offsets_selection_model;
3use {
4    super::{ListOffsetsKind, ListOffsetsSelectionDecision, ListOffsetsSelectionFacts},
5    creusot_std::prelude::*,
6};
7
8/// Apply the common final clamp after any local, diskless, or remote lookup.
9///
10/// The contract pins every variant to the rule `list_offsets_selection_model`
11/// states.
12#[must_use]
13#[ensures(result == list_offsets_selection_model(facts))]
14pub const fn list_offsets_selection_decision(
15    facts: ListOffsetsSelectionFacts,
16) -> ListOffsetsSelectionDecision {
17    let mode = match facts.kind {
18        ListOffsetsKind::Unsupported => {
19            return ListOffsetsSelectionDecision::RejectMalformed;
20        }
21        ListOffsetsKind::Earliest | ListOffsetsKind::EarliestLocal => 0,
22        ListOffsetsKind::Latest => 1,
23        _ => 2,
24    };
25    if facts.candidate_offset < -1 || facts.candidate_epoch < -1 || facts.last_fetchable < 0 {
26        return ListOffsetsSelectionDecision::RejectMalformed;
27    }
28    if facts.candidate_offset == -1 {
29        return ListOffsetsSelectionDecision::Unknown;
30    }
31    let offset = if mode == 1 && facts.last_fetchable < facts.candidate_offset {
32        facts.last_fetchable
33    } else {
34        facts.candidate_offset
35    };
36    if mode == 2 && offset >= facts.last_fetchable {
37        return ListOffsetsSelectionDecision::Unknown;
38    }
39    ListOffsetsSelectionDecision::Resolved {
40        offset,
41        timestamp: facts.candidate_timestamp,
42        leader_epoch: facts.candidate_epoch,
43    }
44}
krabka_verified/list_offsets/selection_decision.rs

krabka_verified/list_offsets/
selection_decision.rs
