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
use proptest::prelude::*;
use super::fixtures::{
arb_seed, covered_dot_map, covered_dot_set, covered_inscribed, covered_metatheses,
covered_node, covered_scholia,
};
use super::harness::check_all_laws;
proptest! {
/// The foreign value-carrying store conforms to every trait law: survivor
/// law, commutativity, associativity, idempotence, bottom identity,
/// in-place agreement (`causal_merge_from`'s default body equals the pure
/// merge, S182), and fiber-wise restriction.
#[test]
fn prop_inscribed_conforms_to_the_axis(
a in arb_seed(), b in arb_seed(), c in arb_seed(),
roster in prop::collection::vec(0u32..4, 0..4),
) {
check_all_laws(
&covered_inscribed(&a),
&covered_inscribed(&b),
&covered_inscribed(&c),
&roster,
);
}
/// The bare presence store passes the same harness, pinning the harness
/// against the reference shape.
#[test]
fn prop_dot_set_conforms_to_the_axis(
a in arb_seed(), b in arb_seed(), c in arb_seed(),
roster in prop::collection::vec(0u32..4, 0..4),
) {
check_all_laws(
&covered_dot_set(&a),
&covered_dot_set(&b),
&covered_dot_set(&c),
&roster,
);
}
/// The composed store passes the same harness.
#[test]
fn prop_dot_map_conforms_to_the_axis(
a in arb_seed(), b in arb_seed(), c in arb_seed(),
roster in prop::collection::vec(0u32..4, 0..4),
) {
check_all_laws(
&covered_dot_map(&a),
&covered_dot_map(&b),
&covered_dot_map(&c),
&roster,
);
}
/// The sparse-product node passes the same harness: the product-closure
/// argument (every law inherited componentwise, the store-algebra note)
/// checked over every component at once, tag conflicts included.
#[test]
fn prop_node_conforms_to_the_axis(
a in arb_seed(), b in arb_seed(), c in arb_seed(),
roster in prop::collection::vec(0u32..4, 0..4),
) {
check_all_laws(
&covered_node(&a),
&covered_node(&b),
&covered_node(&c),
&roster,
);
}
/// The mark store passes the same harness: its instance is pure
/// delegation to the payload store, so this pins that the delegation
/// dropped no law (PRD 0021).
#[test]
fn prop_scholia_conforms_to_the_axis(
a in arb_seed(), b in arb_seed(), c in arb_seed(),
roster in prop::collection::vec(0u32..4, 0..4),
) {
check_all_laws(
&covered_scholia(&a),
&covered_scholia(&b),
&covered_scholia(&c),
&roster,
);
}
/// The move record passes the same harness: its instance is pure
/// delegation to the payload store (PRD 0022).
#[test]
fn prop_metatheses_conforms_to_the_axis(
a in arb_seed(), b in arb_seed(), c in arb_seed(),
roster in prop::collection::vec(0u32..4, 0..4),
) {
check_all_laws(
&covered_metatheses(&a),
&covered_metatheses(&b),
&covered_metatheses(&c),
&roster,
);
}
}