krabka_verified/
vote.rs

1//! KIP-595 Vote wire and membership admission decisions.
2
3use creusot_std::prelude::*;
4
5/// Whether the signed Vote fields can be converted without aliasing a Kafka
6/// sentinel to a real node or epoch.
7#[krabka_macros::model_type]
8pub enum VoteWireDecision {
9    Reject,
10    Accept,
11}
12
13/// Whether unsigned consensus fields fit Kafka's signed Vote wire fields.
14#[krabka_macros::model_type]
15pub enum VoteEncodeDecision {
16    Reject,
17    Accept,
18}
19
20/// Every unsigned consensus field of a Vote fits Kafka's signed `int32` wire
21/// field, so encoding it neither clamps nor wraps into another identity or
22/// epoch.
23// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
24#[cfg(creusot)]
25#[cfg_attr(test, mutants::skip)]
26#[logic]
27pub fn vote_fields_fit_int32(
28    voter_id: u64,
29    candidate_id: u64,
30    candidate_epoch: u32,
31    last_epoch: u32,
32) -> bool {
33    pearlite! {
34        voter_id@ <= i32::MAX@
35            && candidate_id@ <= i32::MAX@
36            && candidate_epoch@ <= i32::MAX@
37            && last_epoch@ <= i32::MAX@
38    }
39}
40
41/// Reject values that would otherwise be clamped and alias another identity or
42/// epoch when encoded as Kafka `int32` fields.
43///
44/// The one ensures pins both variants: `Accept` exactly when
45/// `vote_fields_fit_int32` holds.
46#[ensures((result == VoteEncodeDecision::Accept)
47    == vote_fields_fit_int32(voter_id, candidate_id, candidate_epoch, last_epoch))]
48#[must_use]
49pub fn vote_encode_decision(
50    voter_id: u64,
51    candidate_id: u64,
52    candidate_epoch: u32,
53    last_epoch: u32,
54) -> VoteEncodeDecision {
55    if voter_id > 2_147_483_647
56        || candidate_id > 2_147_483_647
57        || candidate_epoch > 2_147_483_647
58        || last_epoch > 2_147_483_647
59    {
60        VoteEncodeDecision::Reject
61    } else {
62        VoteEncodeDecision::Accept
63    }
64}
65
66/// Every signed identity and epoch field of a Vote is a real value rather than
67/// a negative Kafka sentinel. Zero is a legitimate broker ID and epoch.
68// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
69#[cfg(creusot)]
70#[cfg_attr(test, mutants::skip)]
71#[logic]
72pub fn vote_fields_nonnegative(
73    voter_id: i32,
74    candidate_id: i32,
75    candidate_epoch: i32,
76    last_epoch: i32,
77) -> bool {
78    pearlite! {
79        voter_id@ >= 0 && candidate_id@ >= 0 && candidate_epoch@ >= 0 && last_epoch@ >= 0
80    }
81}
82
83/// Validate the signed identity and epoch fields before conversion to the
84/// unsigned consensus types. The one ensures pins both variants: `Accept`
85/// exactly when `vote_fields_nonnegative` holds.
86#[ensures((result == VoteWireDecision::Accept)
87    == vote_fields_nonnegative(voter_id, candidate_id, candidate_epoch, last_epoch))]
88#[must_use]
89pub fn vote_wire_decision(
90    voter_id: i32,
91    candidate_id: i32,
92    candidate_epoch: i32,
93    last_epoch: i32,
94) -> VoteWireDecision {
95    if voter_id < 0 || candidate_id < 0 || candidate_epoch < 0 || last_epoch < 0 {
96        VoteWireDecision::Reject
97    } else {
98        VoteWireDecision::Accept
99    }
100}
101
102/// Admission shared by binding votes and pre-votes before epoch/log checks.
103#[krabka_macros::model_type]
104pub enum VoteAdmissionDecision {
105    /// The Vote targets another voter and must be ignored without a reply.
106    IgnoreWrongTarget,
107    /// The target is local, but the local node or candidate lacks membership.
108    Deny,
109    /// The exact target and both membership requirements hold.
110    Consider,
111}
112
113/// Whom one Vote request is addressed to, against this node.
114#[krabka_macros::model_type]
115pub struct VoteTarget {
116    /// The `VoterId` the request is addressed to.
117    pub voter_id: u64,
118    /// This node's ID.
119    pub local_id: u64,
120    /// The request's `VoterDirectoryId` names this node's directory.
121    pub directory_matches: bool,
122}
123
124/// The cluster and voter-set memberships one Vote request needs.
125#[krabka_macros::model_type]
126pub struct VoteMembership {
127    /// The request carries no cluster ID, or this node's.
128    pub cluster_matches: bool,
129    /// This node is a voter.
130    pub local_is_voter: bool,
131    /// The candidate is a voter.
132    pub candidate_is_voter: bool,
133}
134
135/// Classify exact recipient and membership admission. The target alone
136/// decides `IgnoreWrongTarget`; for the exact target, the memberships decide
137/// between `Deny` and `Consider`.
138#[ensures((result == VoteAdmissionDecision::IgnoreWrongTarget)
139    == (target.voter_id@ != target.local_id@ || !target.directory_matches))]
140#[ensures((result == VoteAdmissionDecision::Deny) == (
141    target.voter_id@ == target.local_id@ && target.directory_matches
142        && (!membership.cluster_matches
143            || !membership.local_is_voter
144            || !membership.candidate_is_voter)
145))]
146#[ensures((result == VoteAdmissionDecision::Consider) == (
147    target.voter_id@ == target.local_id@ && target.directory_matches
148        && membership.cluster_matches
149        && membership.local_is_voter
150        && membership.candidate_is_voter
151))]
152#[must_use]
153pub fn vote_admission_decision(
154    target: VoteTarget,
155    membership: VoteMembership,
156) -> VoteAdmissionDecision {
157    if target.voter_id != target.local_id || !target.directory_matches {
158        VoteAdmissionDecision::IgnoreWrongTarget
159    } else if !membership.cluster_matches
160        || !membership.local_is_voter
161        || !membership.candidate_is_voter
162    {
163        VoteAdmissionDecision::Deny
164    } else {
165        VoteAdmissionDecision::Consider
166    }
167}
168
169#[cfg(test)]
170mod tests {
171    use {super::*, assert2::check};
172
173    #[yare::parameterized(
174        zeroes = { 0, 0, 0, 0, VoteWireDecision::Accept },
175        negative_voter = { -1, 0, 0, 0, VoteWireDecision::Reject },
176        negative_candidate = { 0, -1, 0, 0, VoteWireDecision::Reject },
177        negative_epoch = { 0, 0, -1, 0, VoteWireDecision::Reject },
178        negative_last_epoch = { 0, 0, 0, -1, VoteWireDecision::Reject },
179    )]
180    fn wire_fields_reject_negatives_without_rejecting_zero(
181        voter: i32,
182        candidate: i32,
183        epoch: i32,
184        last_epoch: i32,
185        expected: VoteWireDecision,
186    ) {
187        check!(vote_wire_decision(voter, candidate, epoch, last_epoch) == expected);
188    }
189
190    #[yare::parameterized(
191        signed_maximum = {
192            i32::MAX as u64,
193            i32::MAX as u64,
194            i32::MAX as u32,
195            i32::MAX as u32,
196            VoteEncodeDecision::Accept,
197        },
198        voter_overflow = { i32::MAX as u64 + 1, 0, 0, 0, VoteEncodeDecision::Reject },
199        candidate_overflow = { 0, i32::MAX as u64 + 1, 0, 0, VoteEncodeDecision::Reject },
200        epoch_overflow = { 0, 0, i32::MAX as u32 + 1, 0, VoteEncodeDecision::Reject },
201        last_epoch_overflow = { 0, 0, 0, i32::MAX as u32 + 1, VoteEncodeDecision::Reject },
202    )]
203    fn encode_fields_reject_values_above_signed_wire_maximum(
204        voter: u64,
205        candidate: u64,
206        epoch: u32,
207        last_epoch: u32,
208        expected: VoteEncodeDecision,
209    ) {
210        check!(vote_encode_decision(voter, candidate, epoch, last_epoch) == expected);
211    }
212
213    #[yare::parameterized(
214        other_voter = {
215            VoteTarget { voter_id: 1, local_id: 2, directory_matches: true },
216            VoteMembership { cluster_matches: true, local_is_voter: true, candidate_is_voter: true },
217            VoteAdmissionDecision::IgnoreWrongTarget,
218        },
219        zero_other_voter = {
220            VoteTarget { voter_id: 0, local_id: 1, directory_matches: true },
221            VoteMembership { cluster_matches: true, local_is_voter: true, candidate_is_voter: true },
222            VoteAdmissionDecision::IgnoreWrongTarget,
223        },
224        directory_mismatch = {
225            VoteTarget { voter_id: 1, local_id: 1, directory_matches: false },
226            VoteMembership { cluster_matches: true, local_is_voter: true, candidate_is_voter: true },
227            VoteAdmissionDecision::IgnoreWrongTarget,
228        },
229        exact_target = {
230            VoteTarget { voter_id: 0, local_id: 0, directory_matches: true },
231            VoteMembership { cluster_matches: true, local_is_voter: true, candidate_is_voter: true },
232            VoteAdmissionDecision::Consider,
233        },
234        cluster_mismatch = {
235            VoteTarget { voter_id: 1, local_id: 1, directory_matches: true },
236            VoteMembership { cluster_matches: false, local_is_voter: true, candidate_is_voter: true },
237            VoteAdmissionDecision::Deny,
238        },
239        local_not_voter = {
240            VoteTarget { voter_id: 1, local_id: 1, directory_matches: true },
241            VoteMembership { cluster_matches: true, local_is_voter: false, candidate_is_voter: true },
242            VoteAdmissionDecision::Deny,
243        },
244        candidate_not_voter = {
245            VoteTarget { voter_id: 1, local_id: 1, directory_matches: true },
246            VoteMembership { cluster_matches: true, local_is_voter: true, candidate_is_voter: false },
247            VoteAdmissionDecision::Deny,
248        },
249        valid_nonzero_target = {
250            VoteTarget { voter_id: 1, local_id: 1, directory_matches: true },
251            VoteMembership { cluster_matches: true, local_is_voter: true, candidate_is_voter: true },
252            VoteAdmissionDecision::Consider,
253        },
254    )]
255    fn admission_requires_the_exact_target_and_both_memberships(
256        target: VoteTarget,
257        membership: VoteMembership,
258        expected: VoteAdmissionDecision,
259    ) {
260        check!(
261            vote_admission_decision(target, membership) == expected,
262            "{target:?} {membership:?}"
263        );
264    }
265}
krabka_verified/vote.rs

krabka_verified/
vote.rs
