krabka_verified/
chain.rs

1//! Sequence and link continuity shared by append-only integrity chains.
2
3use creusot_std::prelude::*;
4
5/// Result of checking one chain link against the running position.
6#[krabka_macros::model_type(proof(DeepModel), runtime(Debug, Clone, Copy, PartialEq, Eq))]
7pub enum ChainStep {
8    /// The record did not carry the next expected sequence number.
9    SequenceMismatch,
10    /// The record did not link to the running chain head.
11    HeadMismatch,
12    /// The record is valid, but no later `u64` sequence number exists.
13    Exhausted,
14    /// The record is valid and the chain continues at this sequence number.
15    Continue(u64),
16}
17
18// cargo-mutants: #[cfg(creusot)] spec function; not compiled outside Creusot, so no test can tell.
19#[cfg(creusot)]
20#[cfg_attr(test, mutants::skip)]
21#[logic(open)]
22fn chain_rank_precedes(left: (i64, u64, bool), right: (i64, u64, bool), allow_ties: bool) -> bool {
23    pearlite! { left.0@ < right.0@ || (left.0@ == right.0@ &&
24    if allow_ties { left.1@ <= right.1@ } else { left.1@ < right.1@ }) }
25}
26
27/// Selects the eligible chain receipt with the greatest `(offset, sequence)`
28/// rank, preserving the first receipt when ranks tie.
29///
30/// The host keeps opaque chain heads and decoded metadata outside Creusot. It
31/// supplies only each receipt's ordering keys and whether that receipt is
32/// eligible to continue the chain.
33#[ensures(match result {
34    None => forall<i: Int> 0 <= i && i < [email protected]() ==> !candidates@[i].2,
35    Some(index) => index@ < [email protected]()
36        && candidates@[index@].2
37        && (forall<i: Int> 0 <= i && i < [email protected]() && candidates@[i].2 ==>
38            chain_rank_precedes(candidates@[i], candidates@[index@], true))
39        && (forall<i: Int> 0 <= i && i < index@ && candidates@[i].2 ==>
40            chain_rank_precedes(candidates@[i], candidates@[index@], false)),
41})]
42#[must_use]
43pub fn select_chain_tip(candidates: &[(i64, u64, bool)]) -> Option<usize> {
44    let mut best: Option<usize> = None;
45    let mut i = 0usize;
46    #[invariant(i@ <= [email protected]())]
47    #[invariant(match best {
48        None => forall<j: Int> 0 <= j && j < i@ ==> !candidates@[j].2,
49        Some(index) => index@ < i@
50            && candidates@[index@].2
51            && (forall<j: Int> 0 <= j && j < i@ && candidates@[j].2 ==>
52                chain_rank_precedes(candidates@[j], candidates@[index@], true))
53            && (forall<j: Int> 0 <= j && j < index@ && candidates@[j].2 ==>
54                chain_rank_precedes(candidates@[j], candidates@[index@], false)),
55    })]
56    #[variant([email protected]() - i@)]
57    while i < candidates.len() {
58        if let Some(&(candidate_time, candidate_seq, true)) = candidates.get(i) {
59            match best {
60                None => best = Some(i),
61                Some(current) => {
62                    if let Some(&(current_time, current_seq, _)) = candidates.get(current) {
63                        let newer = candidate_time > current_time
64                            || (candidate_time == current_time && candidate_seq > current_seq);
65                        if newer {
66                            best = Some(i);
67                        }
68                    }
69                }
70            }
71        }
72        i += 1;
73    }
74    best
75}
76
77/// Checks sequence and opaque-head continuity for one append-only chain link.
78///
79/// Hashing and signature verification stay in the host crates. They pass only
80/// whether the decoded previous head equals the independently recomputed head.
81#[ensures(actual_seq@ != expected_seq@ ==> result == ChainStep::SequenceMismatch)]
82#[ensures(actual_seq@ == expected_seq@ && !head_matches
83    ==> result == ChainStep::HeadMismatch)]
84#[ensures(actual_seq@ == expected_seq@ && head_matches && expected_seq@ == u64::MAX@
85    ==> result == ChainStep::Exhausted)]
86#[ensures(actual_seq@ == expected_seq@ && head_matches && expected_seq@ < u64::MAX@
87    ==> exists<next: u64> result == ChainStep::Continue(next)
88        && next@ == expected_seq@ + 1)]
89#[ensures(forall<next: u64> result == ChainStep::Continue(next)
90    ==> actual_seq@ == expected_seq@ && head_matches && next@ == expected_seq@ + 1)]
91#[must_use]
92pub fn chain_step(expected_seq: u64, actual_seq: u64, head_matches: bool) -> ChainStep {
93    if actual_seq != expected_seq {
94        ChainStep::SequenceMismatch
95    } else if !head_matches {
96        ChainStep::HeadMismatch
97    } else if expected_seq == u64::MAX {
98        ChainStep::Exhausted
99    } else {
100        ChainStep::Continue(expected_seq + 1)
101    }
102}
103
104#[cfg(test)]
105mod tests {
106    use {super::*, assert2::assert};
107
108    #[test]
109    fn chain_tip_uses_offset_then_sequence_and_ignores_ineligible_receipts() {
110        let candidates = [
111            (100, 7, true),
112            (200, 1, false),
113            (100, 9, true),
114            (90, u64::MAX, true),
115        ];
116        assert!(select_chain_tip(&candidates) == Some(2));
117        assert!(select_chain_tip(&[(0, 0, false)]) == None);
118        assert!(select_chain_tip(&[(5, 3, true), (5, 3, true)]) == Some(0));
119    }
120
121    #[test]
122    fn chain_step_is_exact_and_never_wraps() {
123        assert!(chain_step(4, 5, true) == ChainStep::SequenceMismatch);
124        assert!(chain_step(4, 4, false) == ChainStep::HeadMismatch);
125        assert!(chain_step(4, 4, true) == ChainStep::Continue(5));
126        assert!(chain_step(u64::MAX, u64::MAX, true) == ChainStep::Exhausted);
127    }
128}
krabka_verified/chain.rs

krabka_verified/
chain.rs
