minerva 0.2.0

Causal ordering for distributed systems
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

extern crate alloc;

use alloc::boxed::Box;
use alloc::collections::BTreeSet;

use crate::metis::{Dot, DotSet, DotStore};

use super::Node;

/// The sparse-product instance of the open [`DotStore`] axis: every trait
/// law holds componentwise, so the product inherits them component by
/// component (the store-algebra note's product-closure argument, the same
/// reasoning that carries [`DotMap`](crate::metis::DotMap) as the indexed
/// product).
///
/// [`dots`](DotStore::dots) chains the four components (tag, register,
/// children, sequence), each exact by its own law and pairwise disjoint by
/// the write discipline, so the union is exact; [`is_bottom`](DotStore::is_bottom)
/// is the conjunction (a tag-only node is *not* bottom, which is what makes
/// emptiness representable; a fully deleted sequence keeps its skeleton and
/// is likewise not bottom, the [`Rhapsody`](crate::metis::Rhapsody) posture
/// inherited).
impl<K: Ord + Clone, V: Clone> DotStore for Node<K, V> {
    fn dots(&self) -> impl Iterator<Item = Dot> + '_ {
        // The map component's enumeration is type-erased because the node
        // recurses through it: an unboxed chain would make this opaque
        // iterator type a member of its own definition (the compiler's
        // E0275 cycle), so the one boxed leg is a type-level necessity, not
        // a cost choice. Depth stays caller-built (no wire frame exists to
        // let an adversary build it, the PRD 0020 duty).
        let children: Box<dyn Iterator<Item = Dot> + '_> = Box::new(self.children().dots());
        self.tag()
            .dots()
            .chain(self.register().dots())
            .chain(children)
            .chain(self.sequence().dots())
    }

    fn is_bottom(&self) -> bool {
        self.tag().is_bottom()
            && self.children().is_bottom()
            && self.register().is_bottom()
            && self.sequence().is_bottom()
    }

    fn causal_merge(&self, self_context: &DotSet, other: &Self, other_context: &DotSet) -> Self {
        // Componentwise under the same two pair contexts: the survivor
        // verdict for a dot is decided inside its component by the same
        // coverage test a flat store would run, and nothing is ever
        // discarded across components (the kind law's product leg, R-17).
        Self {
            tag: self
                .tag()
                .causal_merge(self_context, other.tag(), other_context),
            register: self
                .register()
                .causal_merge(self_context, other.register(), other_context),
            children: self
                .children()
                .causal_merge(self_context, other.children(), other_context),
            sequence: self
                .sequence()
                .causal_merge(self_context, other.sequence(), other_context),
        }
    }

    fn causal_merge_from(&mut self, self_context: &DotSet, other: &Self, other_context: &DotSet) {
        // The same componentwise fold in place: each component brings its own
        // cost seam (the sequence's delta-bounded S182 override; the
        // register and map components keep the pure default until a number
        // names them, the R-14 posture), and agreement with the pure form
        // holds because it holds per component.
        self.tag
            .causal_merge_from(self_context, other.tag(), other_context);
        self.register
            .causal_merge_from(self_context, other.register(), other_context);
        self.children
            .causal_merge_from(self_context, other.children(), other_context);
        self.sequence
            .causal_merge_from(self_context, other.sequence(), other_context);
    }

    fn restrict(&self, roster: impl IntoIterator<Item = u32>) -> Self {
        let roster: BTreeSet<u32> = roster.into_iter().collect();
        Self {
            tag: self.tag().restrict(roster.iter().copied()),
            register: self.register().restrict(roster.iter().copied()),
            children: self.children().restrict(roster.iter().copied()),
            sequence: self.sequence().restrict(roster.iter().copied()),
        }
    }

    fn novel_to(&self, context: &DotSet) -> Self {
        Self {
            tag: self.tag().novel_to(context),
            register: self.register().novel_to(context),
            children: self.children().novel_to(context),
            sequence: self.sequence().novel_to(context),
        }
    }

    fn novel_to_witnessed(&self, context: &DotSet, recording: &DotSet) -> Self {
        // Componentwise, the witness threading through the recursion and the
        // sequence (the two components that can carry recording state); the
        // flat leaves take their default. One flat witness serves the whole
        // shape because a dot lives under one component of one node only
        // (the cross-component write discipline).
        Self {
            tag: self.tag().novel_to_witnessed(context, recording),
            register: self.register().novel_to_witnessed(context, recording),
            children: self.children().novel_to_witnessed(context, recording),
            sequence: self.sequence().novel_to_witnessed(context, recording),
        }
    }
}