krabka_verified/features/
feature_update_decision.rs

1use super::{
2    FeatureKind, FeatureLevels, FeatureUpdateDecision, FeatureUpdateFacts, FeatureUpdateType,
3};
4#[cfg(creusot)]
5use creusot_std::prelude::*;
6
7crate::creusot_open_spec! {
8    /// The reference decision: the first failed rule in `updateFeature`'s
9    /// order, or what the admitted row does.
10    pub fn feature_update_model(facts: FeatureUpdateFacts) -> FeatureUpdateDecision {
11    pearlite! {
12        match facts.update_type {
13            None => FeatureUpdateDecision::UnknownUpdateType,
14            Some(update_type) => {
15                let requested = facts.levels.requested@;
16                let current = facts.levels.current@;
17                if requested < 0 {
18                    FeatureUpdateDecision::NegativeLevel
19                } else if !facts.all_nodes_support {
20                    FeatureUpdateDecision::UnsupportedByNode
21                } else if requested < current && update_type == FeatureUpdateType::Upgrade {
22                    FeatureUpdateDecision::DowngradeWithoutFlag
23                } else if requested > current && update_type != FeatureUpdateType::Upgrade {
24                    FeatureUpdateDecision::DowngradeToNewerLevel
25                } else {
26                    match facts.kind {
27                        FeatureKind::MetadataVersion { metadata_changed } =>
28                            if requested < current && metadata_changed {
29                                if update_type == FeatureUpdateType::UnsafeDowngrade {
30                                    FeatureUpdateDecision::UnsafeMetadataDowngrade
31                                } else {
32                                    FeatureUpdateDecision::LossyMetadataDowngrade
33                                }
34                            } else {
35                                FeatureUpdateDecision::EmitFeature
36                            },
37                        FeatureKind::KRaftVersion =>
38                            if update_type == FeatureUpdateType::Upgrade {
39                                FeatureUpdateDecision::UpgradeKRaft
40                            } else if requested != current {
41                                FeatureUpdateDecision::KRaftDowngrade
42                            } else {
43                                FeatureUpdateDecision::NoChange
44                            },
45                        FeatureKind::Other { dependencies_met } =>
46                            if dependencies_met {
47                                FeatureUpdateDecision::EmitFeature
48                            } else {
49                                FeatureUpdateDecision::DependencyUnmet
50                            },
51                    }
52                }
53            }
54        }
55    }
56    }
57}
58
59/// Decide one feature row from the host's facts.
60///
61/// A rejection names the first rule that fails in the order of Kafka's
62/// `FeatureControlManager.updateFeature`. A `metadata.version` downgrade is
63/// admitted only when no level between the two changed metadata, whatever the
64/// downgrade type, and an admitted `metadata.version` row never writes
65/// anything but its feature-level record.
66#[cfg_attr(creusot, ensures(result == feature_update_model(facts)))]
67#[cfg_attr(creusot, ensures(match facts.kind {
68    FeatureKind::MetadataVersion { metadata_changed } =>
69        (metadata_changed && result == FeatureUpdateDecision::EmitFeature)
70            ==> facts.levels.requested@ >= facts.levels.current@,
71    _ => true,
72}))]
73#[must_use]
74pub fn feature_update_decision(facts: FeatureUpdateFacts) -> FeatureUpdateDecision {
75    let Some(update_type) = facts.update_type else {
76        return FeatureUpdateDecision::UnknownUpdateType;
77    };
78    let FeatureLevels { requested, current } = facts.levels;
79    if requested < 0 {
80        return FeatureUpdateDecision::NegativeLevel;
81    }
82    if !facts.all_nodes_support {
83        return FeatureUpdateDecision::UnsupportedByNode;
84    }
85    let upgrade = matches!(update_type, FeatureUpdateType::Upgrade);
86    if requested < current && upgrade {
87        return FeatureUpdateDecision::DowngradeWithoutFlag;
88    }
89    if requested > current && !upgrade {
90        return FeatureUpdateDecision::DowngradeToNewerLevel;
91    }
92    match facts.kind {
93        FeatureKind::MetadataVersion { metadata_changed } => {
94            if requested < current && metadata_changed {
95                if matches!(update_type, FeatureUpdateType::UnsafeDowngrade) {
96                    FeatureUpdateDecision::UnsafeMetadataDowngrade
97                } else {
98                    FeatureUpdateDecision::LossyMetadataDowngrade
99                }
100            } else {
101                FeatureUpdateDecision::EmitFeature
102            }
103        }
104        FeatureKind::KRaftVersion => {
105            if upgrade {
106                FeatureUpdateDecision::UpgradeKRaft
107            } else if requested != current {
108                FeatureUpdateDecision::KRaftDowngrade
109            } else {
110                FeatureUpdateDecision::NoChange
111            }
112        }
113        FeatureKind::Other { dependencies_met } => {
114            if dependencies_met {
115                FeatureUpdateDecision::EmitFeature
116            } else {
117                FeatureUpdateDecision::DependencyUnmet
118            }
119        }
120    }
121}
krabka_verified/features/feature_update_decision.rs

krabka_verified/features/
feature_update_decision.rs
