krabka_verified/

snapshot.rs

//! Snapshot-transfer chunk admission.

use {creusot_std::prelude::*, std::cmp::Ordering};

/// Pure decision for one snapshot response chunk.
#[krabka_macros::model_type]
pub enum SnapshotChunkDecision {
    Restart,
    Continue { next_position: i64 },
    Complete,
}

/// Admission result for a fully assembled snapshot at the controller boundary.
#[krabka_macros::model_type]
pub enum SnapshotInstallDecision {
    Reject,
    Stale,
    Install,
}

/// Classify a decoded, fully assembled snapshot against live controller state.
#[ensures(match result {
    SnapshotInstallDecision::Reject => downgrade_pending
        || snapshot_end@ < 0
        || snapshot_epoch@ < 0
        || log_end@ < 0,
    SnapshotInstallDecision::Stale => !downgrade_pending
        && snapshot_end@ >= 0
        && snapshot_epoch@ >= 0
        && log_end@ >= 0
        && snapshot_end@ <= log_end@,
    SnapshotInstallDecision::Install => !downgrade_pending
        && snapshot_end@ >= 0
        && snapshot_epoch@ >= 0
        && log_end@ >= 0
        && snapshot_end@ > log_end@,
})]
#[must_use]
pub fn snapshot_install_decision(
    downgrade_pending: bool,
    snapshot_end: i64,
    snapshot_epoch: i32,
    log_end: i64,
) -> SnapshotInstallDecision {
    if downgrade_pending || snapshot_end < 0 || snapshot_epoch < 0 || log_end < 0 {
        SnapshotInstallDecision::Reject
    } else if snapshot_end <= log_end {
        SnapshotInstallDecision::Stale
    } else {
        SnapshotInstallDecision::Install
    }
}

/// A checkpoint may prune only a nonnegative boundary already committed.
#[ensures(result == (snapshot_end@ >= 0 && snapshot_end@ <= committed_end@))]
#[must_use]
pub fn snapshot_prune_admission(snapshot_end: i64, committed_end: i64) -> bool {
    snapshot_end >= 0 && snapshot_end <= committed_end
}

/// Admit exactly the next bounded chunk for one fixed snapshot identity and size.
#[ensures(match result {
    SnapshotChunkDecision::Restart => !identity_matches
        || received@ < 0
        || chunk_len@ < 0
        || max_size@ < 0
        || declared_size@ < 0
        || declared_size@ > max_size@
        || position@ != received@
        || match fixed_size {
            Some(size) => size@ != declared_size@,
            None => false,
        }
        || received@ + chunk_len@ > declared_size@,
    SnapshotChunkDecision::Continue { next_position } => snapshot_chunk_shape_valid(identity_matches, fixed_size, received@, declared_size@, position@, chunk_len@, max_size@)
        && next_position@ == received@ + chunk_len@
        && next_position@ < declared_size@,
    SnapshotChunkDecision::Complete => snapshot_chunk_shape_valid(identity_matches, fixed_size, received@, declared_size@, position@, chunk_len@, max_size@)
        && received@ + chunk_len@ == declared_size@,
})]
#[must_use]
pub fn snapshot_chunk_admission(
    identity_matches: bool,
    fixed_size: Option<i64>,
    received: i64,
    declared_size: i64,
    position: i64,
    chunk_len: i64,
    max_size: i64,
) -> SnapshotChunkDecision {
    if !identity_matches
        || received < 0
        || chunk_len < 0
        || max_size < 0
        || declared_size < 0
        || declared_size > max_size
        || position != received
    {
        return SnapshotChunkDecision::Restart;
    }
    if let Some(size) = fixed_size
        && size != declared_size
    {
        return SnapshotChunkDecision::Restart;
    }
    let Some(next_position) = received.checked_add(chunk_len) else {
        return SnapshotChunkDecision::Restart;
    };
    match next_position.cmp(&declared_size) {
        Ordering::Greater => SnapshotChunkDecision::Restart,
        Ordering::Equal => SnapshotChunkDecision::Complete,
        Ordering::Less => SnapshotChunkDecision::Continue { next_position },
    }
}

// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
#[cfg(creusot)]
#[cfg_attr(test, mutants::skip)]
#[logic(open)]
/// A chunk continues one fixed identity and declared size at the exact received position.
fn snapshot_chunk_shape_valid(
    identity_matches: bool,
    fixed_size: Option<i64>,
    received: Int,
    declared_size: Int,
    position: Int,
    chunk_len: Int,
    max_size: Int,
) -> bool {
    pearlite! { identity_matches && received >= 0 && chunk_len >= 0 && max_size >= 0
    && declared_size >= 0 && declared_size <= max_size && position == received
    && match fixed_size { Some(size) => size@ == declared_size, None => true, } }
}

#[cfg(test)]
mod tests {
    use {
        super::{
            SnapshotChunkDecision, SnapshotInstallDecision, snapshot_chunk_admission,
            snapshot_install_decision, snapshot_prune_admission,
        },
        assert2::check,
    };

    #[yare::parameterized(
        empty_stale = { false, 0, 0, 0, SnapshotInstallDecision::Stale },
        after_empty = { false, 1, 0, 0, SnapshotInstallDecision::Install },
        beyond_log_end = { false, 11, 3, 10, SnapshotInstallDecision::Install },
        at_log_end = { false, 10, 3, 10, SnapshotInstallDecision::Stale },
        before_log_end = { false, 9, 3, 10, SnapshotInstallDecision::Stale },
        pending = { true, 11, 3, 10, SnapshotInstallDecision::Reject },
        negative_end = { false, -1, 3, 10, SnapshotInstallDecision::Reject },
        negative_epoch = { false, 11, -1, 10, SnapshotInstallDecision::Reject },
        negative_log_end = { false, 11, 3, -1, SnapshotInstallDecision::Reject },
    )]
    fn install_admission_rejects_malformed_and_separates_stale_from_future(
        pending: bool,
        end: i64,
        epoch: i32,
        log_end: i64,
        expected: SnapshotInstallDecision,
    ) {
        check!(snapshot_install_decision(pending, end, epoch, log_end) == expected);
    }

    #[test]
    fn prune_admission_never_crosses_the_committed_frontier() {
        check!(snapshot_prune_admission(10, 10));
        check!(snapshot_prune_admission(9, 10));
        check!(!snapshot_prune_admission(11, 10));
        check!(!snapshot_prune_admission(-1, 10));
    }

    #[yare::parameterized(
        next_chunk = {
            true,
            None,
            0,
            6,
            0,
            3,
            10,
            SnapshotChunkDecision::Continue { next_position: 3 },
        },
        final_chunk = { true, Some(6), 3, 6, 3, 3, 10, SnapshotChunkDecision::Complete },
        empty_snapshot = { true, None, 0, 0, 0, 0, 10, SnapshotChunkDecision::Complete },
        empty_snapshot_at_zero_cap = { true, None, 0, 0, 0, 0, 0, SnapshotChunkDecision::Complete },
        exact_max_size = { true, None, 0, 10, 0, 10, 10, SnapshotChunkDecision::Complete },
        identity_changed = { false, Some(6), 3, 6, 3, 3, 10, SnapshotChunkDecision::Restart },
        fixed_size_changed = { true, Some(7), 3, 6, 3, 3, 10, SnapshotChunkDecision::Restart },
        position_replayed = { true, Some(6), 3, 6, 0, 3, 10, SnapshotChunkDecision::Restart },
        position_skipped = { true, Some(6), 3, 6, 2, 3, 10, SnapshotChunkDecision::Restart },
        chunk_starts_after_position = {
            true,
            Some(6),
            3,
            6,
            4,
            2,
            10,
            SnapshotChunkDecision::Restart,
        },
        chunk_exceeds_declared_size = {
            true,
            Some(6),
            3,
            6,
            3,
            4,
            10,
            SnapshotChunkDecision::Restart,
        },
        negative_received = { true, None, -1, 6, -1, 3, 10, SnapshotChunkDecision::Restart },
        negative_chunk_size = { true, None, 0, 6, 0, -1, 10, SnapshotChunkDecision::Restart },
        negative_max_size = { true, None, 0, 6, 0, 3, -1, SnapshotChunkDecision::Restart },
        negative_declared_size = { true, None, 0, -1, 0, 0, 10, SnapshotChunkDecision::Restart },
        exceeds_max_size = { true, None, 0, 11, 0, 1, 10, SnapshotChunkDecision::Restart },
        addition_overflow = {
            true,
            None,
            i64::MAX,
            i64::MAX,
            i64::MAX,
            1,
            i64::MAX,
            SnapshotChunkDecision::Restart,
        },
    )]
    fn chunk_admission_covers_retries_order_bounds_and_completion(
        identity_matches: bool,
        fixed_size: Option<i64>,
        received: i64,
        declared_size: i64,
        position: i64,
        chunk_len: i64,
        max_size: i64,
        expected: SnapshotChunkDecision,
    ) {
        check!(
            snapshot_chunk_admission(
                identity_matches,
                fixed_size,
                received,
                declared_size,
                position,
                chunk_len,
                max_size
            ) == expected
        );
    }
}