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
// Executable modules for the Signal and RateLimit compositions and for the
// SelectThenActuate and TraversalBudgetComposition theorems. Each TLA+ action
// maps to one exclusive mutable method. Concurrent realizations must provide
// an equivalent atomic commit boundary.
//
// signal — Signal (named composition, Coordination family):
// change-detecting notification channel;
// PendingNotifiedDisjointness.
// rate_limit — RateLimit (named composition, Coordination family):
// per-window operation bound; WindowCountBound,
// WindowStartNotFuture.
// select_then_actuate — SelectThenActuate composition theorem: argmax
// selection coupled with actuation;
// TypeInvariant, ActuationScope, WinnerOptimality,
// CompositionInvariant.
// traversal_budget_composition — TraversalBudgetComposition theorem:
// budgeted traversal with a
// shared budget; TypeInvariant, CompositionInvariant
// (total_cost + budget_remaining = MaxBudget),
// AcceptedSubsetVisited.
//! Named-composition carriers and their proof relations.
/// Budget-coupled accepted-node snapshots.
/// Monotone-boundary bisection.
/// Budgeted union-find equivalence classes.
/// Master and sub-pool budget federation.
/// Fixed-window rate limiting.
/// Ordered additive and maximum reductions.
/// Registry-backed weighted relationship graphs.
/// Budgeted supported sampling.
/// Selection coupled to governed actuation.
/// Change notification with per-listener cursors.
/// Proof facade for traversal and budget coupling.
/// Graph traversal assembled from shared structure owners.