-
Notifications
You must be signed in to change notification settings - Fork 220
Expand file tree
/
Copy pathinvariant.rs
More file actions
149 lines (143 loc) · 5.63 KB
/
invariant.rs
File metadata and controls
149 lines (143 loc) · 5.63 KB
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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
//! Marshal fuzz invariants.
//!
//! Each function asserts one property of the marshal-under-test against
//! the driver's shadow state. The orchestrator [`check_all`] runs them
//! in order; runner.rs only calls `check_all`.
//!
//! Conventions match the rest of the consensus fuzz crate: panics on
//! violation, with a message that includes the relevant shadow state so
//! libFuzzer's crash log is self-explanatory.
use commonware_consensus::{marshal::mocks::harness::TestHarness, types::Height};
use commonware_cryptography::Digestible;
use std::collections::{BTreeMap, HashSet};
/// Run every marshal invariant. Called from the driver at end of run.
pub fn check_all<H: TestHarness>(
ready_prefix: u64,
delivery_log: &[Height],
segment_bounds: &[usize],
segment_starts: &[u64],
expected_redeliveries: &[Vec<Height>],
application_blocks: &BTreeMap<Height, H::ApplicationBlock>,
canonical: &[H::TestBlock],
) {
check_ready_prefix_delivered(ready_prefix, delivery_log);
check_segment_ordering(segment_bounds, segment_starts, delivery_log);
check_redelivery_after_restart(expected_redeliveries, segment_bounds, delivery_log);
check_digest_fidelity::<H>(application_blocks, canonical);
}
/// Invariant: ready-prefix delivery.
///
/// Every height in `1..=ready_prefix` must appear at least once in
/// `delivery_log`. The driver advances `ready_prefix` only when an
/// above-floor `ReportFinalization` (or restart-triggered repair)
/// observes a complete chain back to height 1, which is precisely when
/// marshal is obliged to deliver the prefix.
pub fn check_ready_prefix_delivered(ready_prefix: u64, delivery_log: &[Height]) {
let delivered_set: HashSet<u64> = delivery_log.iter().map(|h| h.get()).collect();
for h in 1..=ready_prefix {
assert!(
delivered_set.contains(&h),
"marshal violated at-least-once delivery: ready height {h} never reached \
the application (ready_prefix={ready_prefix}, delivered={delivered_set:?})",
);
}
}
/// Invariant: per-segment in-order delivery.
///
/// Within each actor instance (segment between restarts) marshal must
/// deliver heights starting at `restored processed_height + 1` and
/// advance strictly by one. The driver pre-populates `segment_starts`
/// from each `setup.height` and `segment_bounds` from the delivery_log
/// positions at restart boundaries.
pub fn check_segment_ordering(
segment_bounds: &[usize],
segment_starts: &[u64],
delivery_log: &[Height],
) {
assert_eq!(
segment_bounds.len(),
segment_starts.len() + 1,
"segment bookkeeping inconsistency",
);
for (segment_idx, window) in segment_bounds.windows(2).enumerate() {
let (start_idx, end_idx) = (window[0], window[1]);
if start_idx == end_idx {
continue;
}
let segment = &delivery_log[start_idx..end_idx];
let expected_start = segment_starts[segment_idx];
assert_eq!(
segment[0].get(),
expected_start,
"segment #{segment_idx} must start at restored processed height + 1 \
({expected_start}), got {} (segment={:?})",
segment[0].get(),
segment,
);
for (offset, h) in segment.iter().enumerate() {
let expected = expected_start + offset as u64;
assert_eq!(
h.get(),
expected,
"marshal violated in-order delivery within segment #{segment_idx}: \
expected height {expected}, observed {} (segment={:?})",
h.get(),
segment,
);
}
}
}
/// Invariant: at-least-once across restart.
///
/// Each height that was pending ack at the moment of restart `i` must
/// reappear somewhere in `delivery_log[segment_bounds[i+1]..]`. Their
/// ack handles were never signaled, so marshal's persistent state
/// retains them as un-processed and the new instance is obliged to
/// redeliver.
pub fn check_redelivery_after_restart(
expected_redeliveries: &[Vec<Height>],
segment_bounds: &[usize],
delivery_log: &[Height],
) {
for (restart_idx, expected) in expected_redeliveries.iter().enumerate() {
if expected.is_empty() {
continue;
}
let post_restart_start = segment_bounds[restart_idx + 1];
let post_restart: HashSet<u64> = delivery_log[post_restart_start..]
.iter()
.map(|h| h.get())
.collect();
for h in expected {
assert!(
post_restart.contains(&h.get()),
"marshal violated at-least-once across restart: height {} was \
pending at restart #{} but was never redelivered \
(post-restart deliveries={post_restart:?})",
h.get(),
restart_idx + 1,
);
}
}
}
/// Invariant: digest fidelity.
///
/// Every block surfaced in `application.blocks()` must match the
/// canonical chain digest at its height. Re-emits after restart
/// overwrite the prior `BTreeMap` entry, so the latest delivery at each
/// height is the one we compare against canonical.
pub fn check_digest_fidelity<H: TestHarness>(
application_blocks: &BTreeMap<Height, H::ApplicationBlock>,
canonical: &[H::TestBlock],
) {
for (height, block) in application_blocks.iter() {
let canonical_block = &canonical[(height.get() - 1) as usize];
assert_eq!(
block.digest(),
H::digest(canonical_block),
"marshal delivered a block whose digest does not match the canonical \
chain at height {}",
height.get(),
);
}
}