krabka_verified/
voter_set.rs

1//! `KRaft` voter-set wire admission.
2
3use creusot_std::prelude::*;
4
5/// Admission outcome for one voter carried by a `VotersRecord`.
6#[krabka_macros::model_type]
7pub enum VoterWireDecision {
8    NegativeId,
9    DirectoryMismatch,
10    InvalidEndpoint,
11    InvalidVersionRange,
12    Accept,
13}
14
15/// Validate the signed voter identity, exact directory translation, endpoint
16/// set, and inclusive supported-version range before conversion.
17#[ensures((result == VoterWireDecision::NegativeId) == (voter_id@ < 0))]
18#[ensures((result == VoterWireDecision::DirectoryMismatch) == (
19    voter_id@ >= 0 && !directory_id_exact
20))]
21#[ensures((result == VoterWireDecision::InvalidEndpoint) == (
22    voter_id@ >= 0 && directory_id_exact && (endpoint_count@ == 0 || !endpoints_valid)
23))]
24#[ensures((result == VoterWireDecision::InvalidVersionRange) == (
25    voter_id@ >= 0 && directory_id_exact && endpoint_count@ > 0 && endpoints_valid
26        && (min_supported_version@ < 0
27            || max_supported_version@ < 0
28            || min_supported_version@ > max_supported_version@)
29))]
30#[ensures((result == VoterWireDecision::Accept) == (
31    voter_id@ >= 0 && directory_id_exact && endpoint_count@ > 0 && endpoints_valid
32        && min_supported_version@ >= 0
33        && min_supported_version@ <= max_supported_version@
34))]
35#[must_use]
36pub fn voter_wire_decision(
37    voter_id: i32,
38    directory_id_exact: bool,
39    endpoint_count: usize,
40    endpoints_valid: bool,
41    min_supported_version: i16,
42    max_supported_version: i16,
43) -> VoterWireDecision {
44    if voter_id < 0 {
45        VoterWireDecision::NegativeId
46    } else if !directory_id_exact {
47        VoterWireDecision::DirectoryMismatch
48    } else if endpoint_count == 0 || !endpoints_valid {
49        VoterWireDecision::InvalidEndpoint
50    } else if min_supported_version < 0
51        || max_supported_version < 0
52        || min_supported_version > max_supported_version
53    {
54        VoterWireDecision::InvalidVersionRange
55    } else {
56        VoterWireDecision::Accept
57    }
58}
59
60/// Admission outcome for the outer `VotersRecord` collection.
61#[krabka_macros::model_type]
62pub enum VoterSetWireDecision {
63    UnsupportedRecordVersion,
64    Empty,
65    DuplicateId,
66    Accept,
67}
68
69/// Require the supported record version and a nonempty collection with one
70/// entry per voter ID.
71#[ensures((result == VoterSetWireDecision::UnsupportedRecordVersion)
72    == (record_version@ != 0))]
73#[ensures((result == VoterSetWireDecision::Empty)
74    == (record_version@ == 0 && voter_count@ == 0))]
75#[ensures((result == VoterSetWireDecision::DuplicateId) == (
76    record_version@ == 0 && voter_count@ > 0 && !voter_ids_unique
77))]
78#[ensures((result == VoterSetWireDecision::Accept) == (
79    record_version@ == 0 && voter_count@ > 0 && voter_ids_unique
80))]
81#[must_use]
82pub fn voter_set_wire_decision(
83    record_version: i16,
84    voter_count: usize,
85    voter_ids_unique: bool,
86) -> VoterSetWireDecision {
87    if record_version != 0 {
88        VoterSetWireDecision::UnsupportedRecordVersion
89    } else if voter_count == 0 {
90        VoterSetWireDecision::Empty
91    } else if !voter_ids_unique {
92        VoterSetWireDecision::DuplicateId
93    } else {
94        VoterSetWireDecision::Accept
95    }
96}
97
98#[cfg(test)]
99mod tests {
100    use {
101        super::{
102            VoterSetWireDecision, VoterWireDecision, voter_set_wire_decision, voter_wire_decision,
103        },
104        assert2::check,
105    };
106
107    #[yare::parameterized(
108        zero_id = { 0, true, 1, true, 0, 0, VoterWireDecision::Accept },
109        maximum_id = { i32::MAX, true, usize::MAX, true, 0, i16::MAX, VoterWireDecision::Accept },
110        negative_id = { -1, true, 1, true, 0, 0, VoterWireDecision::NegativeId },
111        directory_mismatch = { 0, false, 1, true, 0, 0, VoterWireDecision::DirectoryMismatch },
112        zero_endpoints = { 0, true, 0, true, 0, 0, VoterWireDecision::InvalidEndpoint },
113        invalid_endpoints = { 0, true, 1, false, 0, 0, VoterWireDecision::InvalidEndpoint },
114        negative_minimum = { 0, true, 1, true, -1, 0, VoterWireDecision::InvalidVersionRange },
115        negative_maximum = { 0, true, 1, true, 0, -1, VoterWireDecision::InvalidVersionRange },
116        inverted_range = { 0, true, 1, true, 1, 0, VoterWireDecision::InvalidVersionRange },
117    )]
118    fn voter_admission_classifies_every_invalid_boundary(
119        id: i32,
120        directory: bool,
121        count: usize,
122        endpoints: bool,
123        min: i16,
124        max: i16,
125        expected: VoterWireDecision,
126    ) {
127        check!(voter_wire_decision(id, directory, count, endpoints, min, max) == expected);
128    }
129
130    #[yare::parameterized(
131        one_member = { 0, 1, true, VoterSetWireDecision::Accept },
132        maximum_count = { 0, usize::MAX, true, VoterSetWireDecision::Accept },
133        negative_version = { -1, 1, true, VoterSetWireDecision::UnsupportedRecordVersion },
134        newer_version = { 1, 1, true, VoterSetWireDecision::UnsupportedRecordVersion },
135        empty = { 0, 0, true, VoterSetWireDecision::Empty },
136        duplicate_id = { 0, 2, false, VoterSetWireDecision::DuplicateId },
137    )]
138    fn voter_set_admission_requires_version_zero_and_unique_members(
139        version: i16,
140        count: usize,
141        unique: bool,
142        expected: VoterSetWireDecision,
143    ) {
144        check!(voter_set_wire_decision(version, count, unique) == expected);
145    }
146}
krabka_verified/voter_set.rs

krabka_verified/
voter_set.rs
