krabka_verified/
group_migration.rs

1//! Classic and consumer group migration admission and durable record plans.
2
3use creusot_std::prelude::*;
4
5#[krabka_macros::model_type]
6pub enum GroupMigrationDirection {
7    Upgrade,
8    Downgrade,
9}
10
11#[krabka_macros::model_type]
12pub enum GroupMigrationRecordAction {
13    Write,
14    Tombstone,
15}
16
17#[krabka_macros::model_type]
18pub struct GroupMigrationRecordPlan {
19    pub classic_group: GroupMigrationRecordAction,
20    pub next_gen_group: GroupMigrationRecordAction,
21    pub next_gen_target: GroupMigrationRecordAction,
22    pub member_metadata: GroupMigrationRecordAction,
23    pub target_member: GroupMigrationRecordAction,
24    pub current_member: GroupMigrationRecordAction,
25    pub member_count: usize,
26}
27
28// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
29#[cfg(creusot)]
30#[cfg_attr(test, mutants::skip)]
31#[logic(open)]
32fn migration_epoch_matches(input: Int, output: Int) -> bool {
33    pearlite! { output >= 0 &&
34    ((input >= 0 && output == input) || (input < 0 && output == 0)) }
35}
36
37/// Admit a classic-to-consumer upgrade exactly when the protocol and every
38/// member subscription have a consumer representation.
39///
40/// The returned epoch is the classic generation clamped to the first valid
41/// consumer epoch.
42#[ensures((result != None) == (consumer_protocol && every_subscription_decodable))]
43#[ensures(forall<epoch: i32> result == Some(epoch) ==>
44    migration_epoch_matches(generation@, epoch@))]
45#[must_use]
46pub fn classic_upgrade_epoch(
47    consumer_protocol: bool,
48    every_subscription_decodable: bool,
49    generation: i32,
50) -> Option<i32> {
51    if !consumer_protocol || !every_subscription_decodable {
52        return None;
53    }
54    Some(if generation < 0 { 0 } else { generation })
55}
56
57/// Admit a consumer-to-classic downgrade exactly when every member carries a
58/// classic facade. The returned classic generation is nonnegative and keeps
59/// every already-valid consumer epoch unchanged.
60#[ensures((result != None) == every_member_hosted_classic)]
61#[ensures(forall<epoch: i32> result == Some(epoch) ==>
62    migration_epoch_matches(group_epoch@, epoch@))]
63#[must_use]
64pub fn consumer_downgrade_epoch(
65    every_member_hosted_classic: bool,
66    group_epoch: i32,
67) -> Option<i32> {
68    if !every_member_hosted_classic {
69        return None;
70    }
71    Some(if group_epoch < 0 { 0 } else { group_epoch })
72}
73
74/// Select the exact keyed-record actions for one atomic migration batch.
75///
76/// An upgrade tombstones the classic group and writes the full next-gen group.
77/// A downgrade does the inverse. Both directions apply the same action to all
78/// three per-member next-gen record families.
79#[ensures(result.member_count@ == member_count@)]
80#[ensures(result.member_metadata == result.target_member)]
81#[ensures(result.target_member == result.current_member)]
82#[ensures(match direction {
83    GroupMigrationDirection::Upgrade =>
84        result.classic_group == GroupMigrationRecordAction::Tombstone
85            && result.next_gen_group == GroupMigrationRecordAction::Write
86            && result.next_gen_target == GroupMigrationRecordAction::Write
87            && result.member_metadata == GroupMigrationRecordAction::Write,
88    GroupMigrationDirection::Downgrade =>
89        result.classic_group == GroupMigrationRecordAction::Write
90            && result.next_gen_group == GroupMigrationRecordAction::Tombstone
91            && result.next_gen_target == GroupMigrationRecordAction::Tombstone
92            && result.member_metadata == GroupMigrationRecordAction::Tombstone,
93})]
94#[must_use]
95pub fn group_migration_record_plan(
96    direction: GroupMigrationDirection,
97    member_count: usize,
98) -> GroupMigrationRecordPlan {
99    match direction {
100        GroupMigrationDirection::Upgrade => GroupMigrationRecordPlan {
101            classic_group: GroupMigrationRecordAction::Tombstone,
102            next_gen_group: GroupMigrationRecordAction::Write,
103            next_gen_target: GroupMigrationRecordAction::Write,
104            member_metadata: GroupMigrationRecordAction::Write,
105            target_member: GroupMigrationRecordAction::Write,
106            current_member: GroupMigrationRecordAction::Write,
107            member_count,
108        },
109        GroupMigrationDirection::Downgrade => GroupMigrationRecordPlan {
110            classic_group: GroupMigrationRecordAction::Write,
111            next_gen_group: GroupMigrationRecordAction::Tombstone,
112            next_gen_target: GroupMigrationRecordAction::Tombstone,
113            member_metadata: GroupMigrationRecordAction::Tombstone,
114            target_member: GroupMigrationRecordAction::Tombstone,
115            current_member: GroupMigrationRecordAction::Tombstone,
116            member_count,
117        },
118    }
119}
120
121#[cfg(test)]
122mod tests {
123    use {
124        super::{
125            GroupMigrationDirection, GroupMigrationRecordAction, GroupMigrationRecordPlan,
126            classic_upgrade_epoch, consumer_downgrade_epoch, group_migration_record_plan,
127        },
128        assert2::{assert, check},
129    };
130
131    #[test]
132    fn representability_is_exact_and_epochs_do_not_overflow() {
133        check!(classic_upgrade_epoch(true, true, -1) == Some(0));
134        check!(classic_upgrade_epoch(true, true, i32::MAX) == Some(i32::MAX));
135        check!(classic_upgrade_epoch(false, true, 3).is_none());
136        check!(classic_upgrade_epoch(true, false, 3).is_none());
137
138        check!(consumer_downgrade_epoch(true, -1) == Some(0));
139        check!(consumer_downgrade_epoch(true, i32::MAX) == Some(i32::MAX));
140        assert!(consumer_downgrade_epoch(false, 3).is_none());
141    }
142
143    #[test]
144    fn record_plans_flip_every_key_family() {
145        use GroupMigrationRecordAction::{Tombstone, Write};
146
147        // (direction, member count, plan)
148        let cases = [
149            (
150                GroupMigrationDirection::Upgrade,
151                2,
152                GroupMigrationRecordPlan {
153                    classic_group: Tombstone,
154                    next_gen_group: Write,
155                    next_gen_target: Write,
156                    member_metadata: Write,
157                    target_member: Write,
158                    current_member: Write,
159                    member_count: 2,
160                },
161            ),
162            (
163                GroupMigrationDirection::Downgrade,
164                usize::MAX,
165                GroupMigrationRecordPlan {
166                    classic_group: Write,
167                    next_gen_group: Tombstone,
168                    next_gen_target: Tombstone,
169                    member_metadata: Tombstone,
170                    target_member: Tombstone,
171                    current_member: Tombstone,
172                    member_count: usize::MAX,
173                },
174            ),
175        ];
176        for (direction, member_count, plan) in cases {
177            check!(group_migration_record_plan(direction, member_count) == plan);
178        }
179    }
180}
krabka_verified/group_migration.rs

krabka_verified/
group_migration.rs
