minerva 0.2.0

Causal ordering for distributed systems
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116

//! Kani proof harnesses for the [`Span`](super::Span) algebra (S118, under
//! ruling R-9 as written: heap-free scalar arithmetic over fixed-width values,
//! exactly the shape the packed-stamp proofs own).
//!
//! Compiled only under `cargo kani` (`cfg(kani)`), never in a normal build,
//! test, clippy, or rustdoc pass. Each harness is a *total* proof over the full
//! symbolic input space; the always-on property tests in the module's `tests`
//! submodule sample the same laws (the assurance-ladder rule that a proven law
//! keeps its sampled gate).
//!
//! No path here constructs a collection, so the `BTreeMap` scope amendment does
//! not bite: the whole span algebra is arithmetic over `u32` and `NonZeroU64`.

use core::num::NonZeroU64;

use super::Span;

/// A symbolic non-zero `u64`: any dot value, `0` excluded by the type.
fn any_dot() -> NonZeroU64 {
    let raw: u64 = kani::any();
    kani::assume(raw != 0);
    // Safe by the assumption; `new` would branch, `new_unchecked` keeps the
    // harness a pure arithmetic obligation.
    NonZeroU64::new(raw).unwrap()
}

/// A symbolic valid span on `station`: `start <= end`, both non-zero.
fn any_span(station: u32) -> Span {
    let start = any_dot();
    let end = any_dot();
    kani::assume(start <= end);
    Span {
        station,
        start,
        end,
    }
}

/// `contains` agrees with the range arithmetic on the same station, and is
/// never true across stations, for every span and dot.
#[kani::proof]
fn contains_agrees_with_range() {
    let span = any_span(0);
    let dot = any_dot();
    let by_arith = span.start <= dot && dot <= span.end;
    assert_eq!(span.contains(0, dot), by_arith);
    // A dot on any other station is never contained.
    assert!(!span.contains(1, dot));
}

/// `len` is `end - start + 1`, at least one, and never overflows `u64`: the
/// subtraction cannot underflow (`start <= end`) and the increment cannot
/// overflow (`end - start < end <= u64::MAX`).
#[kani::proof]
fn len_never_overflows() {
    let span = any_span(0);
    let diff = span.end.get() - span.start.get();
    // The increment is proven not to overflow: `diff < end <= u64::MAX`.
    let len = diff.checked_add(1).expect("run cardinality fits u64");
    assert_eq!(span.len(), len);
    assert!(span.len() >= 1);
}

/// `coalesce` is commutative: on either order the two spans yield the same
/// union (or the same non-merge), for every pair on one station.
#[kani::proof]
fn coalesce_is_commutative() {
    let a = any_span(0);
    let b = any_span(0);
    match (a.coalesce(b), b.coalesce(a)) {
        (Ok(ab), Ok(ba)) => assert_eq!(ab, ba),
        // A non-merge returns the two inputs; the pair is symmetric.
        (Err((a1, b1)), Err((b2, a2))) => {
            assert_eq!(a1, a2);
            assert_eq!(b1, b2);
        }
        _ => kani::assert(
            false,
            "coalesce disagrees on mergeability across the argument order",
        ),
    }
}

/// `coalesce` is associative where every intermediate pair is defined: folding
/// three spans left or right yields the same union when both groupings merge.
#[kani::proof]
fn coalesce_is_associative_where_defined() {
    let a = any_span(0);
    let b = any_span(0);
    let c = any_span(0);
    // Left grouping `(a . b) . c` and right grouping `a . (b . c)`; the law is
    // stated over the runs where both groupings are fully defined.
    if let (Ok(ab), Ok(bc)) = (a.coalesce(b), b.coalesce(c))
        && let (Ok(left), Ok(right)) = (ab.coalesce(c), a.coalesce(bc))
    {
        assert_eq!(left, right);
    }
}

/// `split_at` then `coalesce` is identity: when the cut lands strictly inside
/// the run, the head and tail coalesce back to the original span.
#[kani::proof]
fn split_then_coalesce_is_identity() {
    let span = any_span(0);
    let seq = any_dot();
    let (head, tail) = span.split_at(seq);
    match tail {
        Some(tail) => {
            // A genuine split: the pieces abut and coalesce back to the whole.
            assert!(head.abuts(&tail));
            assert_eq!(head.coalesce(tail), Ok(span));
        }
        // A no-op split returns the whole run unchanged.
        None => assert_eq!(head, span),
    }
}