krabka_verified/freeze/
replacement_decision.rs

1#[cfg(creusot)]
2use super::logic;
3use {
4    super::{FreezeReplacementDecision, FreezeReplacementFacts, FreezeStoredState},
5    creusot_std::prelude::*,
6};
7
8/// The replacement rule. A thaw of a scope with no committed freeze is
9/// `Missing`, and a record no newer than the committed one at its exact key is
10/// `Stale`; both are permanent refusals the committed image decides alone. An
11/// admissible record behind an uncommitted metadata tail is `InFlight`, the
12/// one refusal that clears once the tail commits, and otherwise it is
13/// `Append`.
14// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
15#[cfg(creusot)]
16#[cfg_attr(test, mutants::skip)]
17#[logic]
18fn freeze_replacement_model(facts: FreezeReplacementFacts) -> FreezeReplacementDecision {
19    pearlite! {
20        let admissible = match facts.stored {
21            FreezeStoredState::Missing => facts.incoming_frozen,
22            FreezeStoredState::Present { set_at_ms } => facts.incoming_set_at_ms@ > set_at_ms@,
23        };
24        if !admissible {
25            match facts.stored {
26                FreezeStoredState::Missing => FreezeReplacementDecision::Missing,
27                FreezeStoredState::Present { .. } => FreezeReplacementDecision::Stale,
28            }
29        } else if facts.uncommitted_tail {
30            FreezeReplacementDecision::InFlight
31        } else {
32            FreezeReplacementDecision::Append
33        }
34    }
35}
36
37/// Admit only a new freeze or a strictly newer exact-key replacement, with no
38/// uncommitted metadata tail; see `freeze_replacement_model`. The
39/// controller retries only `InFlight`, so every variant is pinned.
40#[ensures(result == freeze_replacement_model(facts))]
41#[must_use]
42pub fn freeze_replacement_decision(facts: FreezeReplacementFacts) -> FreezeReplacementDecision {
43    match facts.stored {
44        FreezeStoredState::Missing if !facts.incoming_frozen => FreezeReplacementDecision::Missing,
45        FreezeStoredState::Present { set_at_ms } if facts.incoming_set_at_ms <= set_at_ms => {
46            FreezeReplacementDecision::Stale
47        }
48        FreezeStoredState::Missing | FreezeStoredState::Present { .. } => {
49            if facts.uncommitted_tail {
50                FreezeReplacementDecision::InFlight
51            } else {
52                FreezeReplacementDecision::Append
53            }
54        }
55    }
56}
krabka_verified/freeze/replacement_decision.rs

krabka_verified/freeze/
replacement_decision.rs
