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
use core::marker::PhantomData;
use super::Scoped;
use crate::metis::{Cut, DotSet, ScopedPeek, VersionVector};
impl<'brand> Scoped<'brand, DotSet> {
/// The scoped union: [`DotSet::merge`] of the two restrictions, staying in
/// the scope.
///
/// Restriction commutes with the have-set union exactly (PRD 0013), so the
/// fold stays scoped.
#[must_use]
pub fn merge(&self, other: &Self) -> Self {
Self {
value: self.value.merge(&other.value),
_brand: PhantomData,
}
}
/// The scoped intersection: [`DotSet::intersect`] of the two restrictions,
/// staying in the scope.
///
/// Restriction commutes with the have-set intersection exactly (PRD 0013),
/// so the fold stays scoped.
#[must_use]
pub fn intersect(&self, other: &Self) -> Self {
Self {
value: self.value.intersect(&other.value),
_brand: PhantomData,
}
}
/// The scoped floor: [`DotSet::floor`] of the restriction, staying in the
/// scope.
///
/// A per-station read, so it commutes with restriction exactly (PRD 0013);
/// the resulting cut stays branded because it is still a read over the same
/// roster, sound only there.
#[must_use]
pub fn floor(&self) -> Scoped<'brand, VersionVector> {
Scoped {
value: self.value.floor(),
_brand: PhantomData,
}
}
/// Leaves the scope, forgetting where the have-set was read.
///
/// The have-set instance of [`Scoped::<VersionVector>::forget`]: the brand
/// drops and the bare [`DotSet`] returns. The name is the warning.
#[must_use]
pub fn forget(self) -> DotSet {
self.value
}
/// The gap-free floor of the restriction *as a witnessed [`Cut`]*, without
/// dropping the brand.
///
/// The have-set floor is gap-free by construction (PRD 0012's interior), so
/// it is a genuine cut; wrapping it here mints the witness without a bare
/// [`Cut::floor_of`] call that would lose the scope. It stays branded because
/// it is still a read over the same roster: the floor commutes with
/// restriction exactly (PRD 0013, a per-station read), so
/// `scope.restrict_dots(&s).floor_cut()` is the scoped form of
/// `Cut::floor_of(&s.restrict(roster))`, sound only over the roster it was
/// read against. Distinct from [`floor`](Self::floor), which surrenders the
/// gap-freedom witness to a bare branded [`VersionVector`]; this keeps it.
#[must_use]
pub fn floor_cut(&self) -> Scoped<'brand, Cut> {
Scoped {
value: Cut::floor_of(&self.value),
_brand: PhantomData,
}
}
/// A borrowed, display-only read of the restricted have-set, without
/// escaping the brand.
///
/// The have-set instance of [`Scoped::<VersionVector>::peek`]: a
/// [`ScopedPeek`] for [`Debug`](core::fmt::Debug) rendering, with no
/// [`PartialOrd`] and no accessor, so no scoped read leaks out unbranded.
/// [`DotSet`] carries no order to smuggle, but the wrapper is uniform with
/// the vector peek and still refuses to hand back the inner reference.
#[must_use]
pub const fn peek(&self) -> ScopedPeek<'_, DotSet> {
ScopedPeek::new(&self.value)
}
}