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
use PhantomData;
/// Evidence restricted under a scope's roster, branded by it.
///
/// A `Scoped` value is minted only by
/// [`Scope::restrict`](super::Scope::restrict),
/// [`Scope::restrict_dots`](super::Scope::restrict_dots), and
/// [`Scope::restrict_all`](super::Scope::restrict_all), and every scoped fold
/// keeps the same brand, so a value can only ever be combined with siblings from
/// the same scope. The brand carries no data; it is pure [`PhantomData`], and
/// the crate is `forbid(unsafe_code)` throughout.
///
/// `PartialOrd` is deliberately *not* implemented. Ordering is offered only in
/// method form ([`partial_cmp_scoped`](Scoped::partial_cmp_scoped),
/// [`happens_before`](Scoped::happens_before)) so the `<`, `<=`, `>=`, `>`
/// operators cannot be reached, and so generic code bounded on `PartialOrd`
/// cannot compare scoped evidence as if the verdict were global. The scoped
/// order is sound *within* the scope by PRD 0013's preservation law and
/// inexpressible across scopes by the brand.
///
/// # The brand certifies the invocation, not the roster value
///
/// Two scopes opened over *identical* rosters still do not unify: the brand is a
/// fresh invariant lifetime per [`with_scope`](super::with_scope) call, not a
/// function of the roster. This is deliberate and load-bearing. The soundness the
/// brand carries is "these two values were read under the *same act of
/// restriction*", and two separate `with_scope([1u32], ..)` calls are two acts,
/// even over the same station set: a caller who restricted under one and
/// compared under the other would be reasoning across a boundary the type cannot
/// see is safe. So a same-roster cross-scope comparison is a compile error too:
///
/// ```compile_fail
/// use minerva::metis::{with_scope, VersionVector};
///
/// let a = VersionVector::new();
/// let b = VersionVector::new();
/// with_scope([1u32], |first| {
/// let ra = first.restrict(&a);
/// // Same roster `[1u32]`, a *different* invocation: the brands are still
/// // distinct invariant lifetimes, so this does not typecheck. The brand
/// // tracks the call, never the roster value.
/// with_scope([1u32], |second| {
/// let rb = second.restrict(&b);
/// let _ = ra.happens_before(&rb);
/// });
/// });
/// ```