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
extern crate alloc;
use alloc::vec::Vec;
use super::{REPLICAS, arb_ops, run, station_of};
use proptest::prelude::*;
proptest! {
/// `owed` is exactly `state.delta_for(row)` for the peer's row.
#[test]
fn prop_owed_is_delta_for_against_the_row(ops in arb_ops()) {
let transcript = run(&ops);
let roster: Vec<u32> = (0..REPLICAS).map(station_of).collect();
for state in &transcript.live {
for tracker in &transcript.trackers {
for &peer in &roster {
let owed = tracker.owed(state, peer).expect("peer is on the roster");
let row = tracker.of(peer).expect("peer is on the roster");
let expected = state.delta_for(row);
prop_assert_eq!(owed, expected);
}
}
}
}
/// THE targeting theorem: for run-reached states, replica `owner` builds
/// the delta it owes `peer` off *its own tracker's* row for `peer`, and
/// merging that delta into `peer`'s true state reaches exactly what merging
/// `owner`'s full state would, for every ordered roster pair. Over-shipping
/// (a lagging row) is harmless; the row is a genuine lower bound because the
/// tracker only ever noted a sender's own context, which the sender
/// provably holds.
#[test]
fn prop_owed_delta_converges_like_the_full_state(ops in arb_ops()) {
let transcript = run(&ops);
for owner in 0..REPLICAS {
let state = &transcript.live[owner];
let tracker = &transcript.trackers[owner];
for peer_replica in 0..REPLICAS {
let peer = station_of(peer_replica);
let owed = tracker.owed(state, peer).expect("peer is on the roster");
let peer_true = &transcript.live[peer_replica];
let via_owed = peer_true.merge(&owed);
let via_full = peer_true.merge(state);
prop_assert_eq!(&via_owed, &via_full);
}
}
}
/// THE brand's soundness theorem: a row built only from `Received` evidence
/// (minted here by the receive path, `Composer::absorb`) is a genuine LOWER
/// BOUND on what the peer holds. For every run-reached tracker and every
/// roster peer, the peer's row is a subset of the peer's true context: every
/// dot the tracker vouches the peer has seen, the peer genuinely holds. This
/// is the property the type used to guard by prose; the `Received` brand
/// makes "notes sourced from received contexts stay lower bounds" a fact of
/// the receive path, since a peer's context is a lower bound on what it holds
/// and every note carried exactly such a context.
#[test]
fn prop_received_rows_stay_lower_bounds(ops in arb_ops()) {
let transcript = run(&ops);
for owner in 0..REPLICAS {
let tracker = &transcript.trackers[owner];
for peer_replica in 0..REPLICAS {
let peer = station_of(peer_replica);
let row = tracker.of(peer).expect("peer is on the roster");
let peer_true = transcript.live[peer_replica].context();
// The row never claims a dot the peer does not truly hold: the
// row merged into the peer's true context is exactly that context
// (the row is absorbed, adding nothing new).
let rejoin = peer_true.merge(row);
prop_assert_eq!(&rejoin, peer_true);
}
}
}
}