krabka_verified/barrier/
cut_classification.rs

1#[cfg(creusot)]
2use super::logic;
3use {
4    super::{
5        BarrierCutClassification, BarrierMarkerFenceDecision, BarrierMarkerFenceFacts,
6        BarrierPlacementDecision, BarrierTargetCountDecision,
7    },
8    creusot_std::prelude::*,
9};
10
11/// Add a topic's exact positive partition count without wrapping.
12#[ensures(match result {
13    BarrierTargetCountDecision::Malformed => partition_count@ <= 0,
14    BarrierTargetCountDecision::Overflow => partition_count@ > 0
15        && total@ > i64::MAX@ - partition_count@,
16    BarrierTargetCountDecision::Expand { next } => partition_count@ > 0
17        && total@ <= i64::MAX@ - partition_count@
18        && next@ == total@ + partition_count@,
19})]
20#[must_use]
21pub fn barrier_target_count_decision(
22    total: i64,
23    partition_count: i32,
24) -> BarrierTargetCountDecision {
25    if partition_count <= 0 {
26        return BarrierTargetCountDecision::Malformed;
27    }
28    let count = i64::from(partition_count);
29    let Some(next) = total.checked_add(count) else {
30        return BarrierTargetCountDecision::Overflow;
31    };
32    BarrierTargetCountDecision::Expand { next }
33}
34
35/// The marker fence, in the order its refusals rank: facts that name no
36/// leadership generation at all (no image entry, or a negative epoch) are
37/// `Malformed`; a leader other than the expected one in the image or in the
38/// installed partition is `NotLeader`; a matching leader at another epoch is
39/// `FencedEpoch`; and only an exact match of all three is `Append`.
40// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
41#[cfg(creusot)]
42#[cfg_attr(test, mutants::skip)]
43#[logic]
44fn barrier_marker_fence_model(facts: BarrierMarkerFenceFacts) -> BarrierMarkerFenceDecision {
45    pearlite! {
46        if !facts.image_present
47            || facts.expected_epoch@ < 0
48            || facts.image_epoch@ < 0
49            || facts.current_epoch@ < 0
50        {
51            BarrierMarkerFenceDecision::Malformed
52        } else if facts.image_leader != facts.expected_leader
53            || facts.current_leader != facts.expected_leader
54        {
55            BarrierMarkerFenceDecision::NotLeader
56        } else if facts.image_epoch != facts.expected_epoch
57            || facts.current_epoch != facts.expected_epoch
58        {
59            BarrierMarkerFenceDecision::FencedEpoch
60        } else {
61            BarrierMarkerFenceDecision::Append
62        }
63    }
64}
65
66/// Require the metadata image and installed partition to name exactly the
67/// expected leader generation; see `barrier_marker_fence_model` for which
68/// refusal each mismatch gets.
69///
70/// The host maps the refusals to different wire codes, so every variant is
71/// pinned.
72#[ensures(result == barrier_marker_fence_model(facts))]
73#[must_use]
74pub fn barrier_marker_fence_decision(facts: BarrierMarkerFenceFacts) -> BarrierMarkerFenceDecision {
75    if !facts.image_present
76        || facts.expected_epoch < 0
77        || facts.image_epoch < 0
78        || facts.current_epoch < 0
79    {
80        return BarrierMarkerFenceDecision::Malformed;
81    }
82    if facts.image_leader != facts.expected_leader || facts.current_leader != facts.expected_leader
83    {
84        return BarrierMarkerFenceDecision::NotLeader;
85    }
86    if facts.image_epoch != facts.expected_epoch || facts.current_epoch != facts.expected_epoch {
87        return BarrierMarkerFenceDecision::FencedEpoch;
88    }
89    BarrierMarkerFenceDecision::Append
90}
91
92#[ensures((result == BarrierPlacementDecision::Accept) == (requested && offset@ >= 0))]
93#[must_use]
94pub fn barrier_placement_decision(requested: bool, offset: i64) -> BarrierPlacementDecision {
95    if requested && offset >= 0 {
96        BarrierPlacementDecision::Accept
97    } else {
98        BarrierPlacementDecision::Reject
99    }
100}
101
102#[ensures((result == BarrierCutClassification::Complete) == !has_missing)]
103#[must_use]
104pub fn barrier_cut_classification(has_missing: bool) -> BarrierCutClassification {
105    if has_missing {
106        BarrierCutClassification::Partial
107    } else {
108        BarrierCutClassification::Complete
109    }
110}
krabka_verified/barrier/cut_classification.rs

krabka_verified/barrier/
cut_classification.rs
