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

extern crate alloc;

use crate::kairos::{Clock, Kairos, VirtualTimeSource};

#[test]
fn test_first_after_rolls_logical_ceiling() {
    // S86 regression, found by the Kani harness `after_dominates_previous_on_fresh_clock`:
    // a fresh clock's first receive of a stamp at the logical ceiling must roll into
    // physical exactly as the initialized fold does, or the mint ties the remote on
    // `(physical, logical)` and the kairotic/station tiebreak can order it *below*.
    let clock = Clock::with_default_config(VirtualTimeSource::new(5), 1).unwrap();
    let remote = Kairos::new(9, u16::MAX, 2, u16::MAX);
    let minted = clock.after(remote, 0u16);
    assert!(
        minted > remote,
        "after must dominate its input even at the remote's logical ceiling"
    );
    assert_eq!(minted.physical(), 10, "the ceiling rolls into physical");
    assert_eq!(minted.logical(), 0, "logical restarts after the roll");
}

#[test]
fn test_physical_ceiling_reading_is_not_uninitialized() {
    // Regression guard for S5: u64::MAX is an ordinary physical reading.
    let clock = Clock::with_default_config(VirtualTimeSource::new(u64::MAX), 1).unwrap();
    let t1 = clock.now(0u16);
    let t2 = clock.now(0u16);

    assert_eq!(t1.physical(), u64::MAX);
    assert_eq!(t2.physical(), u64::MAX);
    assert_eq!(t1.logical(), 0);
    assert_eq!(
        t2.logical(),
        1,
        "second stamp must advance logically, not reset to a fresh clock"
    );
    assert!(
        t2 > t1,
        "stamps must stay strictly monotonic at the u64 ceiling"
    );
}